val aff_point_store: res:lbuffer uint8 64ul -> p:aff_point -> Stack unit
  (requires fun h ->
    live h res /\ live h p /\ disjoint res p /\
    aff_point_inv h p)
  (ensures  fun h0 _ h1 -> modifies (loc res) h0 h1 /\
    as_seq h1 res == S.aff_point_store (as_aff_point_nat h0 p))
let aff_point_store res p =
  let px = aff_getx p in
  let py = aff_gety p in
  bn2_to_bytes_be4 res px py
val aff_point_store: res:lbuffer uint8 64ul -> p:aff_point -> Stack unit
  (requires fun h ->
    live h res /\ live h p /\ disjoint res p /\
    aff_point_inv h p)
  (ensures  fun h0 _ h1 -> modifies (loc res) h0 h1 /\
    as_seq h1 res == S.aff_point_store (as_aff_point_nat h0 p))
let aff_point_store res p =
let px = aff_getx p in
let py = aff_gety p in
bn2_to_bytes_be4 res px py
Hacl.Impl.P256.Point.fst.checked
Spec.P256.fst.checked prims.fst.checked Lib.RawIntTypes.fsti.checked Lib.IntTypes.fsti.checked Lib.Buffer.fsti.checked Hacl.Spec.P256.Montgomery.fsti.checked Hacl.Impl.P256.Finv.fsti.checked Hacl.Impl.P256.Field.fsti.checked Hacl.Impl.P256.Constants.fst.checked Hacl.Impl.P256.Bignum.fsti.checked Hacl.Bignum.Base.fst.checked FStar.UInt8.fsti.checked FStar.UInt64.fsti.checked FStar.UInt32.fsti.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.All.fst.checked FStar.HyperStack.fst.checked
Hacl.Impl.P256.Point.fst
Lib.Buffer.lbuffer Lib.IntTypes.uint8 FStar.UInt32.__uint_to_t Hacl.Impl.P256.Point.aff_point Hacl.Impl.P256.Bignum.bn2_to_bytes_be4 Prims.unit Hacl.Impl.P256.Bignum.felem Hacl.Impl.P256.Point.aff_gety Hacl.Impl.P256.Point.aff_getx
module Hacl.Impl.P256.Point

open FStar.Mul
open FStar.HyperStack.All
open FStar.HyperStack
module ST = FStar.HyperStack.ST

open Lib.IntTypes
open Lib.Buffer

open Hacl.Impl.P256.Bignum
open Hacl.Impl.P256.Field
open Hacl.Impl.P256.Constants

module S = Spec.P256
module SM = Hacl.Spec.P256.Montgomery
module FI = Hacl.Impl.P256.Finv

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

///  Create a point

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


let create_point () =
  create 12ul (u64 0)


[@CInline]
let make_base_point p =
  let x = getx p in
  let y = gety p in
  let z = getz p in
  make_g_x x;
  make_g_y y;
  make_fone z


[@CInline]
let make_point_at_inf p =
  let x = getx p in
  let y = gety p in
  let z = getz p in
  make_fzero x;
  make_fone y;
  make_fzero z


///  Check if a point is a point-at-infinity

(* https://crypto.stackexchange.com/questions/43869/point-at-infinity-and-error-handling*)
val lemma_mont_is_point_at_inf: p:S.proj_point{let (_, _, z) = p in z < S.prime} ->
  Lemma (S.is_point_at_inf p == S.is_point_at_inf (from_mont_point p))

let lemma_mont_is_point_at_inf p =
  let px, py, pz = p in
  SM.lemma_from_mont_zero pz


[@CInline]
let is_point_at_inf p =
  let h0 = ST.get () in
  lemma_mont_is_point_at_inf (as_point_nat h0 p);
  let pz = getz p in
  bn_is_zero_mask4 pz


[@CInline]
let is_point_at_inf_vartime p =
  let h0 = ST.get () in
  lemma_mont_is_point_at_inf (as_point_nat h0 p);
  let pz = getz p in
  bn_is_zero_vartime4 pz


///  Create a copy of a point

let copy_point res p =
  copy res p


///  Point conversion between Projective and Affine coordinates representations

[@CInline]
let to_aff_point res p =
  push_frame ();
  let zinv = create_felem () in
  let px = getx p in
  let py = gety p in
  let pz = getz p in

  let x = aff_getx res in
  let y = aff_gety res in

  FI.finv zinv pz;
  fmul x px zinv;
  fmul y py zinv;
  from_mont x x;
  from_mont y y;
  pop_frame ()


[@CInline]
let to_aff_point_x res p =
  push_frame ();
  let zinv = create_felem () in
  let px = getx p in
  let pz = getz p in

  FI.finv zinv pz;
  fmul res px zinv;
  from_mont res res;
  pop_frame ()


[@CInline]
let to_proj_point res p =
  let px = aff_getx p in
  let py = aff_gety p in

  let rx = getx res in
  let ry = gety res in
  let rz = getz res in
  let h0 = ST.get () in
  SM.lemma_to_from_mont_id (as_nat h0 px);
  SM.lemma_to_from_mont_id (as_nat h0 py);
  to_mont rx px;
  to_mont ry py;
  make_fone rz


///  Check if a point is on the curve

inline_for_extraction noextract
val compute_rp_ec_equation: x:felem -> res:felem -> Stack unit
  (requires fun h ->
    live h x /\ live h res /\ disjoint x res /\
    as_nat h x < S.prime)
  (ensures fun h0 _ h1 -> modifies (loc res) h0 h1 /\ as_nat h1 res < S.prime /\
    (let x = fmont_as_nat h0 x in
    fmont_as_nat h1 res ==
      S.fadd (S.fadd (S.fmul (S.fmul x x) x) (S.fmul S.a_coeff x)) S.b_coeff))

let compute_rp_ec_equation x res =
  push_frame ();
  let tmp = create_felem () in
  fcube res x;
  make_a_coeff tmp;
  fmul tmp tmp x;
  fadd res tmp res;
  make_b_coeff tmp;
  fadd res tmp res;
  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 /\
    as_nat h y2 < S.prime /\ as_nat h y < S.prime)
  (ensures fun h0 b h1 -> modifies (loc y) h0 h1 /\
    b == (fmont_as_nat h0 y2 = S.fmul (fmont_as_nat h0 y) (fmont_as_nat h0 y)))

let is_y_sqr_is_y2_vartime y2 y =
  fsqr y y; // y = y * y
  let r = feq_mask y y2 in
  Hacl.Bignum.Base.unsafe_bool_of_limb r


// y *% y =?= x *% x *% x +% a_coeff *% x +% b_coeff
[@CInline]
let is_on_curve_vartime p =
  push_frame ();
  let rp = create_felem () in
  let tx = create_felem () in
  let ty = create_felem () in
  let px = aff_getx p in
  let py = aff_gety p in
  let h0 = ST.get () in
  to_mont tx px;
  to_mont ty py;

  SM.lemma_to_from_mont_id (as_nat h0 px);
  SM.lemma_to_from_mont_id (as_nat h0 py);
  compute_rp_ec_equation tx rp;
  let r = is_y_sqr_is_y2_vartime rp ty in
  pop_frame ();
  r


///  Point load and store functions
val aff_point_store: res:lbuffer uint8 64ul -> p:aff_point -> Stack unit
  (requires fun h ->
    live h res /\ live h p /\ disjoint res p /\
    aff_point_inv h p)
  (ensures  fun h0 _ h1 -> modifies (loc res) h0 h1 /\
    as_seq h1 res == S.aff_point_store (as_aff_point_nat h0 p))
res: Lib.Buffer.lbuffer Lib.IntTypes.uint8 64ul -> p: Hacl.Impl.P256.Point.aff_point
  -> FStar.HyperStack.ST.Stack Prims.unit