val to_aff_point_x (x:felem) (p:point) : Stack unit
  (requires fun h ->
    live h p /\ live h x /\ disjoint p x /\
    point_inv h p)
  (ensures  fun h0 _ h1 -> modifies (loc x) h0 h1 /\
    inv_fully_reduced h1 x /\
    as_nat h1 x == fst (S.to_aff_point (point_eval h0 p)))
let to_aff_point_x x p =
  push_frame ();
  let x1, z1 = getx p, getz p in
  let zinv = create_felem () in
  finv zinv z1;
  fmul x x1 zinv;
  let h = ST.get () in
  assert (inv_lazy_reduced2 h x);
  BL.normalize5_lemma (1,1,1,1,2) (as_felem5 h x);
  fnormalize x x;
  pop_frame ()
val to_aff_point_x (x:felem) (p:point) : Stack unit
  (requires fun h ->
    live h p /\ live h x /\ disjoint p x /\
    point_inv h p)
  (ensures  fun h0 _ h1 -> modifies (loc x) h0 h1 /\
    inv_fully_reduced h1 x /\
    as_nat h1 x == fst (S.to_aff_point (point_eval h0 p)))
let to_aff_point_x x p =
push_frame ();
let x1, z1 = getx p, getz p in
let zinv = create_felem () in
finv zinv z1;
fmul x x1 zinv;
let h = ST.get () in
assert (inv_lazy_reduced2 h x);
BL.normalize5_lemma (1, 1, 1, 1, 2) (as_felem5 h x);
fnormalize x x;
pop_frame ()
Hacl.Impl.K256.Point.fst.checked
Spec.K256.Lemmas.fsti.checked Spec.K256.fst.checked prims.fst.checked Lib.Sequence.fsti.checked Lib.RawIntTypes.fsti.checked Lib.IntTypes.fsti.checked Lib.ByteSequence.fsti.checked Lib.Buffer.fsti.checked Hacl.Spec.K256.Field52.Lemmas.fsti.checked Hacl.Spec.K256.Field52.fst.checked Hacl.K256.Field.fsti.checked Hacl.Impl.K256.Finv.fst.checked FStar.UInt8.fsti.checked FStar.UInt32.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Math.Lemmas.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked FStar.Ghost.fsti.checked
Hacl.Impl.K256.Point.fst
Hacl.K256.Field.felem Hacl.Impl.K256.Point.point FStar.HyperStack.ST.pop_frame Prims.unit Hacl.K256.Field.fnormalize Hacl.Spec.K256.Field52.Lemmas.normalize5_lemma FStar.Pervasives.Native.Mktuple5 Prims.nat Hacl.K256.Field.as_felem5 Prims._assert Hacl.K256.Field.inv_lazy_reduced2 FStar.Monotonic.HyperStack.mem FStar.HyperStack.ST.get Hacl.K256.Field.fmul Hacl.Impl.K256.Finv.finv Hacl.K256.Field.create_felem FStar.Pervasives.Native.tuple2 FStar.Pervasives.Native.Mktuple2 Hacl.Impl.K256.Point.getz Hacl.Impl.K256.Point.getx FStar.HyperStack.ST.push_frame
module Hacl.Impl.K256.Point

open FStar.HyperStack
open FStar.HyperStack.ST
open FStar.Mul

open Lib.IntTypes
open Lib.Buffer

module ST = FStar.HyperStack.ST
module LSeq = Lib.Sequence
module BSeq = Lib.ByteSequence

module S = Spec.K256
module SL = Spec.K256.Lemmas
module BI = Hacl.Spec.K256.Field52
module BL = Hacl.Spec.K256.Field52.Lemmas

open Hacl.K256.Field
open Hacl.Impl.K256.Finv

#set-options "--z3rlimit 50 --fuel 0 --ifuel 0"

///  Create a point

let create_aff_point () =
  create 10ul (u64 0)


let create_point () =
  create (3ul *! 5ul) (u64 0)


let make_point_at_inf p =
  SL.to_aff_point_at_infinity_lemma ();
  let px, py, pz = getx p, gety p, getz p in
  set_zero px;
  set_one py;
  set_zero pz


let make_g g =
  let gx, gy, gz = getx g, gety g, getz g in

  [@inline_let]
  let x =
   (u64 0x2815b16f81798,
    u64 0xdb2dce28d959f,
    u64 0xe870b07029bfc,
    u64 0xbbac55a06295c,
    u64 0x79be667ef9dc) in

  assert_norm (0x79be667ef9dc < max48);
  assert_norm (0xe1108a8fd17b4 < max52);
  assert_norm (S.g_x == as_nat5 x);
  make_u52_5 gx x;

  [@inline_let]
  let y =
   (u64 0x7d08ffb10d4b8,
    u64 0x48a68554199c4,
    u64 0xe1108a8fd17b4,
    u64 0xc4655da4fbfc0,
    u64 0x483ada7726a3) in

  assert_norm (S.g_y == as_nat5 y);
  make_u52_5 gy y;

  set_one gz


let copy_point out p =
  let px, py, pz = getx p, gety p, getz p in
  let ox, oy, oz = getx out, gety out, getz out in
  copy_felem ox px;
  copy_felem oy py;
  copy_felem oz pz


///  Conversion functions between affine and projective coordinates

let to_proj_point p p_aff =
  let x, y = aff_getx p_aff, aff_gety p_aff in
  let x1, y1, z1 = getx p, gety p, getz p in
  copy x1 x;
  copy y1 y;
  set_one z1


[@CInline]
let to_aff_point p_aff p =
  push_frame ();
  let x, y = aff_getx p_aff, aff_gety p_aff in
  let x1, y1, z1 = getx p, gety p, getz p in
  let zinv = create_felem () in
  finv zinv z1;
  fmul x x1 zinv;
  fmul y y1 zinv;
  let h = ST.get () in
  assert (inv_lazy_reduced2 h x);
  assert (inv_lazy_reduced2 h y);

  BL.normalize5_lemma (1,1,1,1,2) (as_felem5 h x);
  BL.normalize5_lemma (1,1,1,1,2) (as_felem5 h y);
  fnormalize x x;
  fnormalize y y;
  pop_frame ()


[@CInline]
val to_aff_point_x (x:felem) (p:point) : Stack unit
  (requires fun h ->
    live h p /\ live h x /\ disjoint p x /\
    point_inv h p)
  (ensures  fun h0 _ h1 -> modifies (loc x) h0 h1 /\
    inv_fully_reduced h1 x /\
    as_nat h1 x == fst (S.to_aff_point (point_eval h0 p)))
x: Hacl.K256.Field.felem -> p: Hacl.Impl.K256.Point.point -> FStar.HyperStack.ST.Stack Prims.unit