val create_widefelem: unit -> StackInline widefelem
  (requires fun h -> True)
  (ensures  fun h0 f h1 ->
    stack_allocated f h0 h1 (LSeq.create 8 (u64 0)) /\
    wide_as_nat h1 f == 0)
let create_widefelem () =
  BD.bn_eval_zeroes #U64 8 8;
  create 8ul (u64 0)
val create_widefelem: unit -> StackInline widefelem
  (requires fun h -> True)
  (ensures  fun h0 f h1 ->
    stack_allocated f h0 h1 (LSeq.create 8 (u64 0)) /\
    wide_as_nat h1 f == 0)
let create_widefelem () =
BD.bn_eval_zeroes #U64 8 8;
create 8ul (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
Prims.unit Lib.Buffer.create Lib.IntTypes.uint64 FStar.UInt32.__uint_to_t Lib.IntTypes.u64 Lib.Buffer.lbuffer Hacl.Spec.Bignum.Definitions.bn_eval_zeroes Lib.IntTypes.U64 Hacl.Impl.P256.Bignum.widefelem
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)
val create_widefelem: unit -> StackInline widefelem
  (requires fun h -> True)
  (ensures  fun h0 f h1 ->
    stack_allocated f h0 h1 (LSeq.create 8 (u64 0)) /\
    wide_as_nat h1 f == 0)
_: Prims.unit -> FStar.HyperStack.ST.StackInline Hacl.Impl.P256.Bignum.widefelem