val point_store: res:lbuffer uint8 64ul -> p:point -> Stack unit
  (requires fun h ->
    live h res /\ live h p /\ disjoint res p /\
    point_inv h p)
  (ensures  fun h0 _ h1 -> modifies (loc res) h0 h1 /\
    as_seq h1 res == S.point_store (point_eval h0 p))
let point_store out p =
  push_frame ();
  let p_aff = create_aff_point () in
  to_aff_point p_aff p;
  aff_point_store out p_aff;
  pop_frame ()
val point_store: res:lbuffer uint8 64ul -> p:point -> Stack unit
  (requires fun h ->
    live h res /\ live h p /\ disjoint res p /\
    point_inv h p)
  (ensures  fun h0 _ h1 -> modifies (loc res) h0 h1 /\
    as_seq h1 res == S.point_store (point_eval h0 p))
let point_store out p =
push_frame ();
let p_aff = create_aff_point () in
to_aff_point p_aff p;
aff_point_store out p_aff;
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
Lib.Buffer.lbuffer Lib.IntTypes.uint8 FStar.UInt32.__uint_to_t Hacl.Impl.K256.Point.point FStar.HyperStack.ST.pop_frame Prims.unit Hacl.Impl.K256.Point.aff_point_store Hacl.Impl.K256.Point.to_aff_point Hacl.Impl.K256.Point.aff_point Hacl.Impl.K256.Point.create_aff_point 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]
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 ()


///  Is a point in affine coordinates on the curve

inline_for_extraction noextract
val compute_expected_y2 (y2 x:felem) : Stack unit
  (requires fun h ->
    live h x /\ live h y2 /\ disjoint x y2 /\
    inv_fully_reduced h x)
  (ensures  fun h0 _ h1 -> modifies (loc y2) h0 h1 /\
   (let xn = as_nat h0 x in inv_fully_reduced h1 y2 /\
   as_nat h1 y2 == S.fadd (S.fmul (S.fmul xn xn) xn) S.b))

let compute_expected_y2 y2 x =
  push_frame ();
  let b = create_felem () in
  make_u52_5 b (make_b_k256 ());
  let h0 = ST.get () in
  assert (inv_fully_reduced h0 b /\ as_nat h0 b = S.b);

  fsqr y2 x;
  fmul y2 y2 x;
  let h1 = ST.get () in
  assert (inv_lazy_reduced2 h1 y2);
  assert (let xn = as_nat h0 x in
    feval h1 y2 == S.fmul (S.fmul xn xn) xn);

  BL.fadd5_lemma (1,1,1,1,2) (1,1,1,1,1) (as_felem5 h1 y2) (as_felem5 h1 b);
  fadd y2 y2 b;
  let h1 = ST.get () in
  assert (felem_fits5 (as_felem5 h1 y2) (2,2,2,2,3));

  fnormalize y2 y2;
  BL.normalize5_lemma (2,2,2,2,3) (as_felem5 h1 y2);
  pop_frame ()


inline_for_extraction noextract
val is_y_sqr_is_y2_vartime (y2 y:felem) : Stack bool
  (requires fun h ->
    live h y /\ live h y2 /\ disjoint y y2 /\
    inv_fully_reduced h y2 /\ inv_fully_reduced h y)
  (ensures fun h0 b h1 -> modifies0 h0 h1 /\
    b == (as_nat h0 y2 = S.fmul (as_nat h0 y) (as_nat h0 y)))

let is_y_sqr_is_y2_vartime y2 y =
  push_frame ();
  let y2_comp = create_felem () in

  fsqr y2_comp y;
  let h0 = ST.get () in
  assert (inv_lazy_reduced2 h0 y2);
  fnormalize y2_comp y2_comp;
  BL.normalize5_lemma (1,1,1,1,2) (as_felem5 h0 y2_comp);

  let res = is_felem_eq_vartime y2 y2_comp in
  pop_frame ();
  res


[@CInline]
let is_on_curve_vartime p =
  push_frame ();
  let y2_exp = create_felem () in
  let x, y = aff_getx p, aff_gety p in
  compute_expected_y2 y2_exp x;
  let res = is_y_sqr_is_y2_vartime y2_exp y in
  pop_frame ();
  res


let is_proj_point_at_inf_vartime p =
  push_frame ();
  let tmp = create_felem () in
  let pz = getz p in

  let h0 = ST.get () in
  assert (inv_lazy_reduced2 h0 (gsub p 10ul 5ul));
  BL.normalize5_lemma (1,1,1,1,2) (as_felem5 h0 pz);
  fnormalize tmp pz;
  let b = is_felem_zero_vartime tmp in
  pop_frame ();
  b


///  Point negation

[@CInline]
let point_negate out p =
  let h0 = ST.get () in
  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 oz pz;

  BL.fnegate5_lemma (1,1,1,1,2) (as_felem5 h0 py) (u64 2);
  make_u52_5 oy (BI.fnegate5 (py.(0ul), py.(1ul), py.(2ul), py.(3ul), py.(4ul)) (u64 2));
  let h1 = ST.get () in
  assert (felem_fits5 (as_felem5 h1 oy) (4,4,4,4,4));
  assert (as_nat h1 oy == 4 * S.prime - as_nat h0 py);
  BL.normalize_weak5_lemma (4,4,4,4,4) (as_felem5 h1 oy);
  fnormalize_weak oy oy;
  let h2 = ST.get () in
  assert (feval h2 ox == feval h0 px);
  assert (feval h2 oz == feval h0 pz);
  assert (feval h2 oy == (4 * S.prime - as_nat h0 py) % S.prime);
  Math.Lemmas.modulo_addition_lemma (- as_nat h0 py) S.prime 4;
  Math.Lemmas.lemma_mod_sub_distr 0 (as_nat h0 py) S.prime;
  assert (feval h2 oy == (- feval h0 py) % S.prime)


[@CInline]
let point_negate_conditional_vartime p is_negate =
  if is_negate then point_negate p p


///  Point load and store functions

[@CInline]
let aff_point_store out p =
  let px = aff_getx p in
  let py = aff_gety p in

  let h0 = ST.get () in
  update_sub_f h0 out 0ul 32ul
    (fun h -> BSeq.nat_to_bytes_be 32 (as_nat h0 px))
    (fun _ -> store_felem (sub out 0ul 32ul) px);

  let h1 = ST.get () in
  update_sub_f h1 out 32ul 32ul
    (fun h -> BSeq.nat_to_bytes_be 32 (as_nat h1 py))
    (fun _ -> store_felem (sub out 32ul 32ul) py);

  let h2 = ST.get () in
  let px = Ghost.hide (BSeq.nat_to_bytes_be 32 (as_nat h0 px)) in
  let py = Ghost.hide (BSeq.nat_to_bytes_be 32 (as_nat h0 py)) in
  LSeq.eq_intro (as_seq h2 out) (LSeq.concat #_ #32 #32 px py)


[@CInline]
val point_store: res:lbuffer uint8 64ul -> p:point -> Stack unit
  (requires fun h ->
    live h res /\ live h p /\ disjoint res p /\
    point_inv h p)
  (ensures  fun h0 _ h1 -> modifies (loc res) h0 h1 /\
    as_seq h1 res == S.point_store (point_eval h0 p))
res: Lib.Buffer.lbuffer Lib.IntTypes.uint8 64ul -> p: Hacl.Impl.K256.Point.point
  -> FStar.HyperStack.ST.Stack Prims.unit