val ecp256dh_r:
    shared_secret:lbuffer uint8 64ul
  -> their_pubkey:lbuffer uint8 64ul
  -> private_key:lbuffer uint8 32ul ->
  Stack bool
  (requires fun h ->
    live h shared_secret /\ live h their_pubkey /\ live h private_key /\
    disjoint shared_secret their_pubkey /\ disjoint shared_secret private_key)
  (ensures fun h0 r h1 -> modifies (loc shared_secret) h0 h1 /\
    (let ss = S.ecdh (as_seq h0 their_pubkey) (as_seq h0 private_key) in
    (r <==> Some? ss) /\ (r ==> (as_seq h1 shared_secret == Some?.v ss))))
let ecp256dh_r shared_secret their_pubkey private_key =
  push_frame ();
  let tmp = create 16ul (u64 0) in
  let sk = sub tmp 0ul 4ul in
  let pk = sub tmp 4ul 12ul in

  let is_pk_valid = load_point_vartime pk their_pubkey in
  let is_sk_valid = load_qelem_conditional sk private_key in
  ecp256dh_r_ is_pk_valid shared_secret pk sk;
  pop_frame ();
  Hacl.Bignum.Base.unsafe_bool_of_limb is_sk_valid && is_pk_valid
val ecp256dh_r:
    shared_secret:lbuffer uint8 64ul
  -> their_pubkey:lbuffer uint8 64ul
  -> private_key:lbuffer uint8 32ul ->
  Stack bool
  (requires fun h ->
    live h shared_secret /\ live h their_pubkey /\ live h private_key /\
    disjoint shared_secret their_pubkey /\ disjoint shared_secret private_key)
  (ensures fun h0 r h1 -> modifies (loc shared_secret) h0 h1 /\
    (let ss = S.ecdh (as_seq h0 their_pubkey) (as_seq h0 private_key) in
    (r <==> Some? ss) /\ (r ==> (as_seq h1 shared_secret == Some?.v ss))))
let ecp256dh_r shared_secret their_pubkey private_key =
push_frame ();
let tmp = create 16ul (u64 0) in
let sk = sub tmp 0ul 4ul in
let pk = sub tmp 4ul 12ul in
let is_pk_valid = load_point_vartime pk their_pubkey in
let is_sk_valid = load_qelem_conditional sk private_key in
ecp256dh_r_ is_pk_valid shared_secret pk sk;
pop_frame ();
Hacl.Bignum.Base.unsafe_bool_of_limb is_sk_valid && is_pk_valid
Hacl.Impl.P256.DH.fst.checked
Spec.P256.fst.checked prims.fst.checked Lib.IntTypes.fsti.checked Lib.Buffer.fsti.checked Hacl.Impl.P256.Scalar.fsti.checked Hacl.Impl.P256.PointMul.fsti.checked Hacl.Impl.P256.Point.fsti.checked Hacl.Impl.P256.Bignum.fsti.checked Hacl.Bignum.Base.fst.checked FStar.UInt32.fsti.checked FStar.Pervasives.fsti.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.All.fst.checked FStar.HyperStack.fst.checked
Hacl.Impl.P256.DH.fst
Lib.Buffer.lbuffer Lib.IntTypes.uint8 FStar.UInt32.__uint_to_t Prims.op_AmpAmp Hacl.Spec.Bignum.Base.unsafe_bool_of_limb Lib.IntTypes.U64 Prims.bool Prims.unit FStar.HyperStack.ST.pop_frame Hacl.Impl.P256.DH.ecp256dh_r_ Lib.IntTypes.int_t Lib.IntTypes.SEC Hacl.Impl.P256.Scalar.load_qelem_conditional Lib.IntTypes.uint64 Hacl.Impl.P256.Point.load_point_vartime Lib.Buffer.lbuffer_t Lib.Buffer.MUT FStar.UInt32.uint_to_t FStar.UInt32.t Lib.Buffer.sub Lib.Buffer.create Lib.IntTypes.u64 FStar.HyperStack.ST.push_frame
module Hacl.Impl.P256.DH

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.Scalar
open Hacl.Impl.P256.Point
open Hacl.Impl.P256.PointMul

module S = Spec.P256

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

[@CInline]
let ecp256dh_i public_key private_key =
  push_frame ();
  let tmp = create 16ul (u64 0) in
  let sk = sub tmp 0ul 4ul in
  let pk = sub tmp 4ul 12ul in

  let is_sk_valid = load_qelem_conditional sk private_key in
  point_mul_g pk sk;
  point_store public_key pk;
  pop_frame ();
  Hacl.Bignum.Base.unsafe_bool_of_limb is_sk_valid


inline_for_extraction noextract
val ecp256dh_r_: is_pk_valid:bool -> ss:lbuffer uint8 64ul -> pk:point -> sk:felem -> Stack unit
  (requires fun h ->
    live h ss /\ live h pk /\ live h sk /\
    disjoint ss pk /\ disjoint ss sk /\ disjoint pk sk /\
    as_nat h sk < S.order /\ (is_pk_valid ==> point_inv h pk))
  (ensures fun  h0 _ h1 -> modifies (loc ss) h0 h1 /\
    as_seq h1 ss == (if is_pk_valid
    then S.point_store (S.point_mul (as_nat h0 sk) (from_mont_point (as_point_nat h0 pk)))
    else as_seq h0 ss))

let ecp256dh_r_ is_pk_valid ss pk sk =
  push_frame ();
  let ss_proj = create_point () in
  if is_pk_valid then begin
    point_mul ss_proj sk pk;
    point_store ss ss_proj end;
  pop_frame ()


[@CInline]
val ecp256dh_r:
    shared_secret:lbuffer uint8 64ul
  -> their_pubkey:lbuffer uint8 64ul
  -> private_key:lbuffer uint8 32ul ->
  Stack bool
  (requires fun h ->
    live h shared_secret /\ live h their_pubkey /\ live h private_key /\
    disjoint shared_secret their_pubkey /\ disjoint shared_secret private_key)
  (ensures fun h0 r h1 -> modifies (loc shared_secret) h0 h1 /\
    (let ss = S.ecdh (as_seq h0 their_pubkey) (as_seq h0 private_key) in
    (r <==> Some? ss) /\ (r ==> (as_seq h1 shared_secret == Some?.v ss))))

    shared_secret: Lib.Buffer.lbuffer Lib.IntTypes.uint8 64ul ->
    their_pubkey: Lib.Buffer.lbuffer Lib.IntTypes.uint8 64ul ->
    private_key: Lib.Buffer.lbuffer Lib.IntTypes.uint8 32ul
  -> FStar.HyperStack.ST.Stack Prims.bool