val bn_set_one4: f:felem -> Stack unit
  (requires fun h -> live h f)
  (ensures fun h0 _ h1 -> modifies (loc f) h0 h1 /\
    as_nat h1 f == 1)
let bn_set_one4 f =
  bn_make_u64_4 f (u64 1) (u64 0) (u64 0) (u64 0)
val bn_set_one4: f:felem -> Stack unit
  (requires fun h -> live h f)
  (ensures fun h0 _ h1 -> modifies (loc f) h0 h1 /\
    as_nat h1 f == 1)
let bn_set_one4 f =
bn_make_u64_4 f (u64 1) (u64 0) (u64 0) (u64 0)
Hacl.Impl.P256.Bignum.fst.checked
prims.fst.checked Lib.Sequence.fsti.checked Lib.IntTypes.fsti.checked Lib.ByteBuffer.fsti.checked Lib.Buffer.fsti.checked Hacl.Spec.Bignum.Definitions.fst.checked Hacl.Spec.Bignum.Convert.fst.checked Hacl.Spec.Bignum.fsti.checked Hacl.Bignum.Convert.fst.checked Hacl.Bignum.Base.fst.checked Hacl.Bignum.fsti.checked FStar.UInt32.fsti.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.All.fst.checked FStar.HyperStack.fst.checked FStar.Ghost.fsti.checked FStar.Calc.fsti.checked
Hacl.Impl.P256.Bignum.fst
Hacl.Impl.P256.Bignum.felem Hacl.Impl.P256.Bignum.bn_make_u64_4 Lib.IntTypes.u64 Prims.unit
module Hacl.Impl.P256.Bignum

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

open Lib.IntTypes
open Lib.Buffer

module BN = Hacl.Bignum
module SN = Hacl.Spec.Bignum
module BD = Hacl.Spec.Bignum.Definitions
module LSeq = Lib.Sequence

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

let bn_v_is_as_nat a =
  let open Lib.Sequence in
  let open Hacl.Spec.Bignum.Definitions in
  assert_norm (pow2 64 * pow2 64 = pow2 128);
  assert_norm (pow2 64 * pow2 64 * pow2 64 = pow2 192);

  calc (==) {
    bn_v a;
  (==) { bn_eval1 (slice a 0 1); bn_eval_split_i #U64 a 1 }
    v a.[0] + pow2 64 * bn_v (slice a 1 4);
  (==) { bn_eval_split_i #U64 (slice a 1 4) 1; bn_eval1 (slice a 1 2) }
    v a.[0] + pow2 64 * v a.[1] + pow2 64 * pow2 64 * bn_v (slice a 2 4);
  (==) { bn_eval_split_i #U64 (slice a 2 4) 1; bn_eval1 (slice a 2 3) }
    v a.[0] + pow2 64 * v a.[1] + pow2 64 * pow2 64 * v a.[2]
    + pow2 64 * pow2 64 * pow2 64 * bn_v (slice a 3 4);
  (==) { bn_eval1 (slice a 3 4) }
    v a.[0] + pow2 64 * v a.[1] + pow2 64 * pow2 64 * v a.[2]
    + pow2 64 * pow2 64 * pow2 64 * v a.[3];
  }


///  Create a bignum

let create_felem () =
  BD.bn_eval_zeroes #U64 4 4;
  create 4ul (u64 0)


let create_widefelem () =
  BD.bn_eval_zeroes #U64 8 8;
  create 8ul (u64 0)


let bn_make_u64_4 res a0 a1 a2 a3 =
  let h0 = ST.get () in
  upd res 0ul a0;
  let h1 = ST.get () in
  upd res 1ul a1;
  let h2 = ST.get () in
  upd res 2ul a2;
  let h3 = ST.get () in
  upd res 3ul a3;
  let h4 = ST.get () in
  BD.bn_upd_eval (as_seq h0 res) a0 0;
  BD.bn_upd_eval (as_seq h1 res) a1 1;
  BD.bn_upd_eval (as_seq h2 res) a2 2;
  BD.bn_upd_eval (as_seq h3 res) a3 3;
  bn_v_is_as_nat (as_seq h0 res)


///  Create zero and one

let bn_set_zero4 f =
  bn_make_u64_4 f (u64 0) (u64 0) (u64 0) (u64 0)
val bn_set_one4: f:felem -> Stack unit
  (requires fun h -> live h f)
  (ensures fun h0 _ h1 -> modifies (loc f) h0 h1 /\
    as_nat h1 f == 1)
f: Hacl.Impl.P256.Bignum.felem -> FStar.HyperStack.ST.Stack Prims.unit