val bn_v_is_as_nat: a:LSeq.lseq uint64 4 ->
  Lemma (let (s0, s1, s2, s3) = LSeq.(a.[0], a.[1], a.[2], a.[3]) in
    BD.bn_v a == v s0 + v s1 * pow2 64 + v s2 * pow2 128 + v s3 * pow2 192)
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];
  }
val bn_v_is_as_nat: a:LSeq.lseq uint64 4 ->
  Lemma (let (s0, s1, s2, s3) = LSeq.(a.[0], a.[1], a.[2], a.[3]) in
    BD.bn_v a == v s0 + v s1 * pow2 64 + v s2 * pow2 128 + v s3 * pow2 192)
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 ];
}
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
Lib.Sequence.lseq Lib.IntTypes.uint64 FStar.Calc.calc_finish Prims.nat Prims.eq2 Hacl.Spec.Bignum.Definitions.bn_v Lib.IntTypes.U64 Prims.op_Addition Lib.IntTypes.v Lib.IntTypes.SEC Lib.Sequence.op_String_Access FStar.Mul.op_Star Prims.pow2 Prims.Cons FStar.Preorder.relation Prims.Nil Prims.unit FStar.Calc.calc_step Prims.op_Subtraction Lib.Sequence.slice FStar.Calc.calc_init FStar.Calc.calc_pack Hacl.Spec.Bignum.Definitions.bn_eval_split_i Hacl.Spec.Bignum.Definitions.bn_eval1 Prims.squash FStar.Pervasives.assert_norm Prims.b2t Prims.op_Equality Prims.int
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"
val bn_v_is_as_nat: a:LSeq.lseq uint64 4 ->
  Lemma (let (s0, s1, s2, s3) = LSeq.(a.[0], a.[1], a.[2], a.[3]) in
    BD.bn_v a == v s0 + v s1 * pow2 64 + v s2 * pow2 128 + v s3 * pow2 192)
a: Lib.Sequence.lseq Lib.IntTypes.uint64 4
  -> FStar.Pervasives.Lemma
    (ensures
      (let _ = a.[ 0 ], a.[ 1 ], a.[ 2 ], a.[ 3 ] in
        (let FStar.Pervasives.Native.Mktuple4 #_ #_ #_ #_ s0 s1 s2 s3 = _ in
          Hacl.Spec.Bignum.Definitions.bn_v a ==
          Lib.IntTypes.v s0 + Lib.IntTypes.v s1 * Prims.pow2 64 + Lib.IntTypes.v s2 * Prims.pow2 128 +
          Lib.IntTypes.v s3 * Prims.pow2 192)
        <:
        Type0))