val bn_is_lt_prime_mask4: f:felem -> Stack uint64
  (requires fun h -> live h f)
  (ensures  fun h0 r h1 -> modifies0 h0 h1 /\
    (if as_nat h0 f < S.prime then v r = ones_v U64 else v r = 0))
let bn_is_lt_prime_mask4 f =
  let h0 = ST.get () in
  push_frame ();
  let tmp = create_felem () in
  make_prime tmp;
  let c = bn_sub4 tmp f tmp in
  assert (if v c = 0 then as_nat h0 f >= S.prime else as_nat h0 f < S.prime);
  pop_frame ();
  u64 0 -. c
val bn_is_lt_prime_mask4: f:felem -> Stack uint64
  (requires fun h -> live h f)
  (ensures  fun h0 r h1 -> modifies0 h0 h1 /\
    (if as_nat h0 f < S.prime then v r = ones_v U64 else v r = 0))
let bn_is_lt_prime_mask4 f =
let h0 = ST.get () in
push_frame ();
let tmp = create_felem () in
make_prime tmp;
let c = bn_sub4 tmp f tmp in
assert (if v c = 0 then as_nat h0 f >= S.prime else as_nat h0 f < S.prime);
pop_frame ();
u64 0 -. c
Hacl.Impl.P256.Field.fst.checked
Spec.P256.fst.checked prims.fst.checked Lib.IntTypes.fsti.checked Lib.Buffer.fsti.checked Hacl.Spec.P256.Montgomery.fsti.checked Hacl.Spec.Bignum.Definitions.fst.checked Hacl.Impl.P256.Constants.fst.checked Hacl.Impl.P256.Bignum.fsti.checked Hacl.Bignum256.fst.checked Hacl.Bignum.Montgomery.fsti.checked FStar.UInt32.fsti.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Math.Lemmas.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.All.fst.checked FStar.HyperStack.fst.checked FStar.Calc.fsti.checked
Hacl.Impl.P256.Field.fst
Hacl.Impl.P256.Bignum.felem Lib.IntTypes.op_Subtraction_Dot Lib.IntTypes.U64 Lib.IntTypes.SEC Lib.IntTypes.u64 Lib.IntTypes.uint64 Prims.unit FStar.HyperStack.ST.pop_frame Prims._assert Prims.op_Equality Prims.int Lib.IntTypes.v Prims.b2t Prims.op_GreaterThanOrEqual Hacl.Impl.P256.Bignum.as_nat Spec.P256.PointOps.prime Prims.bool Prims.op_LessThan Lib.IntTypes.int_t Hacl.Impl.P256.Bignum.bn_sub4 Hacl.Impl.P256.Constants.make_prime Hacl.Impl.P256.Bignum.create_felem FStar.HyperStack.ST.push_frame FStar.Monotonic.HyperStack.mem FStar.HyperStack.ST.get
module Hacl.Impl.P256.Field

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.Constants

module S = Spec.P256
module SM = Hacl.Spec.P256.Montgomery

module BD = Hacl.Spec.Bignum.Definitions
module BM = Hacl.Bignum.Montgomery

friend Hacl.Bignum256

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

///  Create zero and one

[@CInline]
let make_fzero n =
  bn_set_zero4 n;
  assert_norm (SM.to_mont 0 = 0);
  SM.lemma_to_from_mont_id 0


[@CInline]
let make_fone n =
  // 0xfffffffeffffffffffffffffffffffff000000000000000000000001
  [@inline_let] let n0 = u64 0x1 in
  [@inline_let] let n1 = u64 0xffffffff00000000 in
  [@inline_let] let n2 = u64 0xffffffffffffffff in
  [@inline_let] let n3 = u64 0xfffffffe in
  assert_norm (v n0 + v n1 * pow2 64 + v n2 * pow2 128 + v n3 * pow2 192 < S.prime);
  assert_norm (v n0 + v n1 * pow2 64 + v n2 * pow2 128 + v n3 * pow2 192 == SM.to_mont 1);
  SM.lemma_to_from_mont_id 1;
  bn_make_u64_4 n n0 n1 n2 n3


///  Comparison
val bn_is_lt_prime_mask4: f:felem -> Stack uint64
  (requires fun h -> live h f)
  (ensures  fun h0 r h1 -> modifies0 h0 h1 /\
    (if as_nat h0 f < S.prime then v r = ones_v U64 else v r = 0))
f: Hacl.Impl.P256.Bignum.felem -> FStar.HyperStack.ST.Stack Lib.IntTypes.uint64