val make_qone: f:felem -> Stack unit
  (requires fun h -> live h f)
  (ensures  fun h0 _ h1 -> modifies (loc f) h0 h1 /\
    as_nat h1 f < S.order /\
    qmont_as_nat h1 f == 1)
let make_qone f =
  [@inline_let] let f0 = u64 0xc46353d039cdaaf in
  [@inline_let] let f1 = u64 0x4319055258e8617b in
  [@inline_let] let f2 = u64 0x0 in
  [@inline_let] let f3 = u64 0xffffffff in
  assert_norm (v f0 + v f1 * pow2 64 + v f2 * pow2 128 + v f3 * pow2 192 < S.order);
  assert_norm (v f0 + v f1 * pow2 64 + v f2 * pow2 128 + v f3 * pow2 192 == SM.to_qmont 1);
  SM.lemma_to_from_qmont_id 1;
  bn_make_u64_4 f f0 f1 f2 f3
val make_qone: f:felem -> Stack unit
  (requires fun h -> live h f)
  (ensures  fun h0 _ h1 -> modifies (loc f) h0 h1 /\
    as_nat h1 f < S.order /\
    qmont_as_nat h1 f == 1)
let make_qone f =
[@@ inline_let ]let f0 = u64 0xc46353d039cdaaf in
[@@ inline_let ]let f1 = u64 0x4319055258e8617b in
[@@ inline_let ]let f2 = u64 0x0 in
[@@ inline_let ]let f3 = u64 0xffffffff in
assert_norm (v f0 + v f1 * pow2 64 + v f2 * pow2 128 + v f3 * pow2 192 < S.order);
assert_norm (v f0 + v f1 * pow2 64 + v f2 * pow2 128 + v f3 * pow2 192 == SM.to_qmont 1);
SM.lemma_to_from_qmont_id 1;
bn_make_u64_4 f f0 f1 f2 f3
Hacl.Impl.P256.Scalar.fst.checked
Spec.P256.fst.checked prims.fst.checked Lib.IntTypes.fsti.checked Lib.ByteBuffer.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
Hacl.Impl.P256.Scalar.fst
Hacl.Impl.P256.Bignum.felem Hacl.Impl.P256.Bignum.bn_make_u64_4 Prims.unit Hacl.Spec.P256.Montgomery.lemma_to_from_qmont_id FStar.Pervasives.assert_norm Prims.eq2 Prims.int Prims.op_Addition Lib.IntTypes.v Lib.IntTypes.U64 Lib.IntTypes.SEC FStar.Mul.op_Star Prims.pow2 Hacl.Spec.P256.Montgomery.to_qmont Prims.b2t Prims.op_LessThan Spec.P256.PointOps.order Lib.IntTypes.int_t Lib.IntTypes.range Lib.IntTypes.u64
module Hacl.Impl.P256.Scalar

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

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

///  Create one

[@CInline]
val make_qone: f:felem -> Stack unit
  (requires fun h -> live h f)
  (ensures  fun h0 _ h1 -> modifies (loc f) h0 h1 /\
    as_nat h1 f < S.order /\
    qmont_as_nat h1 f == 1)
f: Hacl.Impl.P256.Bignum.felem -> FStar.HyperStack.ST.Stack Prims.unit