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)))
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)
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)))
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)
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.Impl.Ed25519.RecoverX.elemB Prims.op_AmpAmp FStar.UInt64.op_Equals_Hat Lib.RawIntTypes.u64_to_UInt64 FStar.UInt64.__uint_to_t Prims.bool Lib.IntTypes.int_t Lib.IntTypes.U64 Lib.IntTypes.SEC Lib.Buffer.op_Array_Access Lib.Buffer.MUT Lib.IntTypes.uint64 FStar.UInt32.__uint_to_t
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]
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)))
x: Hacl.Impl.Ed25519.RecoverX.elemB -> FStar.HyperStack.ST.Stack Prims.bool