val x_mod_2: x:felem -> Stack uint64
  (requires fun h -> live h x)
  (ensures  fun h0 z h1 -> h0 == h1 /\ v z < 2 /\
    v z == F51.as_nat h0 x % 2)
let x_mod_2 x =
  let x0 = x.(0ul) in
  let z  = x0 &. u64 1 in
  mod_mask_lemma x0 1ul;
  Lib.IntTypes.Compatibility.uintv_extensionality (u64 1) (mod_mask #U64 1ul);
  z
val x_mod_2: x:felem -> Stack uint64
  (requires fun h -> live h x)
  (ensures  fun h0 z h1 -> h0 == h1 /\ v z < 2 /\
    v z == F51.as_nat h0 x % 2)
let x_mod_2 x =
let x0 = x.(0ul) in
let z = x0 &. u64 1 in
mod_mask_lemma x0 1ul;
Lib.IntTypes.Compatibility.uintv_extensionality (u64 1) (mod_mask #U64 1ul);
z
Hacl.Impl.Ed25519.RecoverX.fst.checked
Spec.Ed25519.fst.checked Spec.Curve25519.fst.checked prims.fst.checked Lib.RawIntTypes.fsti.checked Lib.IntTypes.Compatibility.fst.checked Lib.IntTypes.fsti.checked Lib.Buffer.fsti.checked Hacl.Spec.Curve25519.Field51.Definition.fst.checked Hacl.Impl.Ed25519.Pow2_252m2.fst.checked Hacl.Impl.Ed25519.Field51.fst.checked Hacl.Bignum25519.fsti.checked FStar.UInt8.fsti.checked FStar.UInt64.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.All.fst.checked
Hacl.Impl.Ed25519.RecoverX.fst
Hacl.Bignum25519.felem Prims.unit Lib.IntTypes.Compatibility.uintv_extensionality Lib.IntTypes.U64 Lib.IntTypes.SEC Lib.IntTypes.u64 Lib.IntTypes.mod_mask FStar.UInt32.__uint_to_t Lib.IntTypes.mod_mask_lemma Lib.IntTypes.int_t Lib.IntTypes.op_Amp_Dot Lib.IntTypes.uint64 Lib.Buffer.op_Array_Access Lib.Buffer.MUT
module Hacl.Impl.Ed25519.RecoverX

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

open Lib.IntTypes
open Lib.Buffer

open Hacl.Bignum25519

module F51 = Hacl.Impl.Ed25519.Field51
module S51 = Hacl.Spec.Curve25519.Field51.Definition

module SC = Spec.Curve25519
module SE = Spec.Ed25519

#reset-options "--z3rlimit 50 --max_fuel 0 --max_ifuel 0"

inline_for_extraction noextract
let elemB = lbuffer uint64 5ul

val is_0: x:elemB -> Stack bool
  (requires fun h -> live h x /\ F51.as_nat h x == F51.fevalh h x)
  (ensures  fun h0 b h1 -> h0 == h1 /\
    (b <==> (F51.fevalh h0 x == SC.zero)))

[@CInline]
let is_0 x =
  let open Lib.RawIntTypes in
  let open FStar.UInt64 in
  let x0 = x.(0ul) in
  let x1 = x.(1ul) in
  let x2 = x.(2ul) in
  let x3 = x.(3ul) in
  let x4 = x.(4ul) in
  (u64_to_UInt64 x0 =^ 0uL &&
   u64_to_UInt64 x1 =^ 0uL &&
   u64_to_UInt64 x2 =^ 0uL &&
   u64_to_UInt64 x3 =^ 0uL &&
   u64_to_UInt64 x4 =^ 0uL)


inline_for_extraction noextract
val gte_q: x:elemB -> Stack bool
  (requires fun h -> live h x /\
    F51.felem_fits h x (1, 1, 1, 1, 1))
  (ensures  fun h0 b h1 -> h0 == h1 /\
    (b <==> (F51.as_nat h0 x >= SC.prime)))

let gte_q x =
  let open Lib.RawIntTypes in
  let open FStar.UInt64 in
  let x0 = x.(0ul) in
  let x1 = x.(1ul) in
  let x2 = x.(2ul) in
  let x3 = x.(3ul) in
  let x4 = x.(4ul) in
  (u64_to_UInt64 x0 >=^ 0x7ffffffffffeduL &&
   u64_to_UInt64 x1 =^ 0x7ffffffffffffuL &&
   u64_to_UInt64 x2 =^ 0x7ffffffffffffuL &&
   u64_to_UInt64 x3 =^ 0x7ffffffffffffuL &&
   u64_to_UInt64 x4 =^ 0x7ffffffffffffuL)


val mul_modp_sqrt_m1: x:elemB -> Stack unit
  (requires fun h -> live h x /\ F51.mul_inv_t h x)
  (ensures  fun h0 _ h1 -> modifies (loc x) h0 h1 /\
    F51.mul_inv_t h1 x /\
    F51.fevalh h1 x == F51.fevalh h0 x `SC.fmul` SE.modp_sqrt_m1)

[@CInline]
let mul_modp_sqrt_m1 x =
  [@inline_let] let (x0, x1, x2, x3, x4) =
    (u64 0x00061b274a0ea0b0,
    u64 0x0000d5a5fc8f189d,
    u64 0x0007ef5e9cbd0c60,
    u64 0x00078595a6804c9e,
    u64 0x0002b8324804fc1d) in

  push_frame();
  let sqrt_m1 = create 5ul (u64 0) in
  make_u64_5 sqrt_m1 x0 x1 x2 x3 x4;
  assert_norm (S51.as_nat5 (x0, x1, x2, x3, x4) == SE.modp_sqrt_m1);
  fmul x x sqrt_m1;
  pop_frame()


inline_for_extraction noextract
val x_mod_2: x:felem -> Stack uint64
  (requires fun h -> live h x)
  (ensures  fun h0 z h1 -> h0 == h1 /\ v z < 2 /\
    v z == F51.as_nat h0 x % 2)
val x_mod_2: x:felem -> Stack uint64
  (requires fun h -> live h x)
  (ensures  fun h0 z h1 -> h0 == h1 /\ v z < 2 /\
    v z == F51.as_nat h0 x % 2)
x: Hacl.Bignum25519.felem -> FStar.HyperStack.ST.Stack Lib.IntTypes.uint64