val scalarmult:
    shared:lbuffer uint8 32ul
  -> my_priv:lbuffer uint8 32ul
  -> their_pub:lbuffer uint8 32ul
  -> Stack unit
    (requires fun h0 ->
      live h0 shared /\ live h0 my_priv /\ live h0 their_pub /\
      disjoint shared my_priv /\ disjoint shared their_pub)
    (ensures  fun h0 _ h1 -> modifies (loc shared) h0 h1 /\
      as_seq h1 shared == Spec.Curve25519.scalarmult (as_seq h0 my_priv) (as_seq h0 their_pub))
let scalarmult shared my_priv their_pub =
  if EverCrypt.TargetConfig.hacl_can_compile_vale then
    let has_bmi2 = EverCrypt.AutoConfig2.has_bmi2 () in
    let has_adx = EverCrypt.AutoConfig2.has_adx () in
    if (has_bmi2 && has_adx) then
      Hacl.Curve25519_64.scalarmult shared my_priv their_pub
    else
      Hacl.Curve25519_51.scalarmult shared my_priv their_pub
  else
    Hacl.Curve25519_51.scalarmult shared my_priv their_pub
val scalarmult:
    shared:lbuffer uint8 32ul
  -> my_priv:lbuffer uint8 32ul
  -> their_pub:lbuffer uint8 32ul
  -> Stack unit
    (requires fun h0 ->
      live h0 shared /\ live h0 my_priv /\ live h0 their_pub /\
      disjoint shared my_priv /\ disjoint shared their_pub)
    (ensures  fun h0 _ h1 -> modifies (loc shared) h0 h1 /\
      as_seq h1 shared == Spec.Curve25519.scalarmult (as_seq h0 my_priv) (as_seq h0 their_pub))
let scalarmult shared my_priv their_pub =
if EverCrypt.TargetConfig.hacl_can_compile_vale
then
  let has_bmi2 = EverCrypt.AutoConfig2.has_bmi2 () in
  let has_adx = EverCrypt.AutoConfig2.has_adx () in
  if (has_bmi2 && has_adx)
  then Hacl.Curve25519_64.scalarmult shared my_priv their_pub
  else Hacl.Curve25519_51.scalarmult shared my_priv their_pub
else Hacl.Curve25519_51.scalarmult shared my_priv their_pub
EverCrypt.Curve25519.fst.checked
Vale.X64.CPU_Features_s.fst.checked prims.fst.checked LowStar.Buffer.fst.checked Hacl.Curve25519_64.fsti.checked Hacl.Curve25519_51.fsti.checked FStar.Pervasives.fsti.checked EverCrypt.TargetConfig.fsti.checked EverCrypt.AutoConfig2.fsti.checked
EverCrypt.Curve25519.fst
Lib.Buffer.lbuffer Lib.IntTypes.uint8 FStar.UInt32.__uint_to_t EverCrypt.TargetConfig.hacl_can_compile_vale Prims.op_AmpAmp Hacl.Curve25519_64.scalarmult Prims.unit Prims.bool Hacl.Curve25519_51.scalarmult EverCrypt.AutoConfig2.has_adx EverCrypt.AutoConfig2.has_bmi2
module EverCrypt.Curve25519

module B = LowStar.Buffer

[@ CInline ]
let has_adx_bmi2 (): Stack bool
  (fun _ -> True)
  (ensures (fun h0 b h1 ->
    B.(modifies B.loc_none h0 h1) /\
    (b ==> Vale.X64.CPU_Features_s.(adx_enabled /\ bmi2_enabled))))
=
  let has_bmi2 = EverCrypt.AutoConfig2.has_bmi2 () in
  let has_adx = EverCrypt.AutoConfig2.has_adx () in
  has_bmi2 && has_adx

#set-options "--max_fuel 0 --max_ifuel 0 --z3rlimit 50"
let secret_to_public pub priv =
  if EverCrypt.TargetConfig.hacl_can_compile_vale then
    let has_bmi2 = EverCrypt.AutoConfig2.has_bmi2 () in
    let has_adx = EverCrypt.AutoConfig2.has_adx () in
    if (has_bmi2 && has_adx) then
      Hacl.Curve25519_64.secret_to_public pub priv
    else
      Hacl.Curve25519_51.secret_to_public pub priv
  else
    Hacl.Curve25519_51.secret_to_public pub priv
val scalarmult:
    shared:lbuffer uint8 32ul
  -> my_priv:lbuffer uint8 32ul
  -> their_pub:lbuffer uint8 32ul
  -> Stack unit
    (requires fun h0 ->
      live h0 shared /\ live h0 my_priv /\ live h0 their_pub /\
      disjoint shared my_priv /\ disjoint shared their_pub)
    (ensures  fun h0 _ h1 -> modifies (loc shared) h0 h1 /\
      as_seq h1 shared == Spec.Curve25519.scalarmult (as_seq h0 my_priv) (as_seq h0 their_pub))

    shared: Lib.Buffer.lbuffer Lib.IntTypes.uint8 32ul ->
    my_priv: Lib.Buffer.lbuffer Lib.IntTypes.uint8 32ul ->
    their_pub: Lib.Buffer.lbuffer Lib.IntTypes.uint8 32ul
  -> FStar.HyperStack.ST.Stack Prims.unit