val bn_from_uint_lemma: #t:limb_t -> len:size_pos -> x:limb t ->
  Lemma (bn_v (bn_from_uint len x) == uint_v x)
let bn_from_uint_lemma #t len x =
  let b = create len (uint #t 0) in
  let b = b.[0] <- x in
  bn_eval_split_i b 1;
  assert (bn_v b == bn_v (slice b 0 1) + pow2 (bits t) * bn_v (slice b 1 len));
  eq_intro (slice b 1 len) (create (len - 1) (uint #t 0));
  bn_eval_zeroes #t (len - 1) (len - 1);
  assert (bn_v b == bn_v (slice b 0 1));
  bn_eval1 (slice b 0 1)
val bn_from_uint_lemma: #t:limb_t -> len:size_pos -> x:limb t ->
  Lemma (bn_v (bn_from_uint len x) == uint_v x)
let bn_from_uint_lemma #t len x =
let b = create len (uint #t 0) in
let b = b.[ 0 ] <- x in
bn_eval_split_i b 1;
assert (bn_v b == bn_v (slice b 0 1) + pow2 (bits t) * bn_v (slice b 1 len));
eq_intro (slice b 1 len) (create (len - 1) (uint #t 0));
bn_eval_zeroes #t (len - 1) (len - 1);
assert (bn_v b == bn_v (slice b 0 1));
bn_eval1 (slice b 0 1)
Hacl.Spec.Bignum.Convert.fst.checked
prims.fst.checked Lib.Sequence.fsti.checked Lib.IntTypes.fsti.checked Lib.ByteSequence.fsti.checked Hacl.Spec.Bignum.Definitions.fst.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Math.Lemmas.fst.checked FStar.Classical.fsti.checked FStar.Calc.fsti.checked
Hacl.Spec.Bignum.Convert.fst
Hacl.Spec.Bignum.Definitions.limb_t Lib.IntTypes.size_pos Hacl.Spec.Bignum.Definitions.limb Hacl.Spec.Bignum.Definitions.bn_eval1 Lib.Sequence.slice Prims.unit Prims._assert Prims.eq2 Prims.nat Hacl.Spec.Bignum.Definitions.bn_v Prims.op_Subtraction Hacl.Spec.Bignum.Definitions.bn_eval_zeroes Lib.Sequence.eq_intro Lib.Sequence.create Lib.IntTypes.uint Lib.IntTypes.SEC Prims.int Prims.op_Addition FStar.Mul.op_Star Prims.pow2 Lib.IntTypes.bits Hacl.Spec.Bignum.Definitions.bn_eval_split_i Lib.Sequence.lseq Prims.l_and FStar.Seq.Base.seq Lib.Sequence.to_seq FStar.Seq.Base.upd Lib.Sequence.index Prims.l_Forall Prims.b2t Prims.op_LessThanOrEqual Prims.l_imp Prims.op_LessThan Prims.op_disEquality Prims.l_or FStar.Seq.Base.index Lib.Sequence.op_String_Assignment FStar.Seq.Base.create Lib.IntTypes.mk_int
module Hacl.Spec.Bignum.Convert

open FStar.Mul

open Lib.IntTypes
open Lib.Sequence
open Lib.ByteSequence

open Hacl.Spec.Bignum.Definitions


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

val bn_from_uint: #t:limb_t -> len:size_pos -> x:limb t -> lbignum t len
let bn_from_uint #t len x =
  let b = create len (uint #t 0) in
  b.[0] <- x

val bn_from_uint_lemma: #t:limb_t -> len:size_pos -> x:limb t ->
  Lemma (bn_v (bn_from_uint len x) == uint_v x)
val bn_from_uint_lemma: #t:limb_t -> len:size_pos -> x:limb t ->
  Lemma (bn_v (bn_from_uint len x) == uint_v x)
len: Lib.IntTypes.size_pos -> x: Hacl.Spec.Bignum.Definitions.limb t
  -> FStar.Pervasives.Lemma
    (ensures
      Hacl.Spec.Bignum.Definitions.bn_v (Hacl.Spec.Bignum.Convert.bn_from_uint len x) ==
      Lib.IntTypes.uint_v x)