val make_fzero: n:felem -> Stack unit
  (requires fun h -> live h n)
  (ensures  fun h0 _ h1 -> modifies (loc n) h0 h1 /\
    as_nat h1 n < S.prime /\
    fmont_as_nat h1 n == 0)
let make_fzero n =
  bn_set_zero4 n;
  assert_norm (SM.to_mont 0 = 0);
  SM.lemma_to_from_mont_id 0
val make_fzero: n:felem -> Stack unit
  (requires fun h -> live h n)
  (ensures  fun h0 _ h1 -> modifies (loc n) h0 h1 /\
    as_nat h1 n < S.prime /\
    fmont_as_nat h1 n == 0)
let make_fzero n =
bn_set_zero4 n;
assert_norm (SM.to_mont 0 = 0);
SM.lemma_to_from_mont_id 0
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 Hacl.Spec.P256.Montgomery.lemma_to_from_mont_id Prims.unit FStar.Pervasives.assert_norm Prims.b2t Prims.op_Equality Prims.int Hacl.Spec.P256.Montgomery.to_mont Hacl.Impl.P256.Bignum.bn_set_zero4
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]
val make_fzero: n:felem -> Stack unit
  (requires fun h -> live h n)
  (ensures  fun h0 _ h1 -> modifies (loc n) h0 h1 /\
    as_nat h1 n < S.prime /\
    fmont_as_nat h1 n == 0)
n: Hacl.Impl.P256.Bignum.felem -> FStar.HyperStack.ST.Stack Prims.unit