val bn_from_uint:
    #t:limb_t
  -> len:size_t{0 < v len}
  -> x:limb t
  -> b:lbignum t len ->
  Stack unit
  (requires fun h -> live h b)
  (ensures  fun h0 _ h1 -> modifies (loc b) h0 h1 /\
    as_seq h1 b == S.bn_from_uint (v len) x)
let bn_from_uint #t len x b =
  memset b (uint #t 0) len;
  b.(0ul) <- x
val bn_from_uint:
    #t:limb_t
  -> len:size_t{0 < v len}
  -> x:limb t
  -> b:lbignum t len ->
  Stack unit
  (requires fun h -> live h b)
  (ensures  fun h0 _ h1 -> modifies (loc b) h0 h1 /\
    as_seq h1 b == S.bn_from_uint (v len) x)
let bn_from_uint #t len x b =
memset b (uint #t 0) len;
b.(0ul) <- x
Hacl.Bignum.Convert.fst.checked
prims.fst.checked LowStar.Ignore.fsti.checked LowStar.Buffer.fst.checked Lib.Sequence.fsti.checked Lib.IntTypes.fsti.checked Lib.ByteBuffer.fsti.checked Lib.Buffer.fsti.checked Hacl.Spec.Bignum.Convert.fst.checked Hacl.Bignum.Definitions.fst.checked FStar.UInt32.fsti.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked
Hacl.Bignum.Convert.fst
Hacl.Bignum.Definitions.limb_t Lib.IntTypes.size_t Prims.b2t Prims.op_LessThan Lib.IntTypes.v Lib.IntTypes.U32 Lib.IntTypes.PUB Hacl.Bignum.Definitions.limb Hacl.Bignum.Definitions.lbignum Lib.Buffer.op_Array_Assignment FStar.UInt32.__uint_to_t Prims.unit Lib.Buffer.memset Lib.IntTypes.uint Lib.IntTypes.SEC
module Hacl.Bignum.Convert

open FStar.HyperStack
open FStar.HyperStack.ST
open FStar.Mul

open Lib.IntTypes
open Lib.Buffer
open Lib.ByteBuffer

open Hacl.Bignum.Definitions

module ST = FStar.HyperStack.ST
module LSeq = Lib.Sequence

module S = Hacl.Spec.Bignum.Convert

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

inline_for_extraction noextract
val bn_from_uint:
    #t:limb_t
  -> len:size_t{0 < v len}
  -> x:limb t
  -> b:lbignum t len ->
  Stack unit
  (requires fun h -> live h b)
  (ensures  fun h0 _ h1 -> modifies (loc b) h0 h1 /\
    as_seq h1 b == S.bn_from_uint (v len) x)
val bn_from_uint:
    #t:limb_t
  -> len:size_t{0 < v len}
  -> x:limb t
  -> b:lbignum t len ->
  Stack unit
  (requires fun h -> live h b)
  (ensures  fun h0 _ h1 -> modifies (loc b) h0 h1 /\
    as_seq h1 b == S.bn_from_uint (v len) x)

    len: Lib.IntTypes.size_t{0 < Lib.IntTypes.v len} ->
    x: Hacl.Bignum.Definitions.limb t ->
    b: Hacl.Bignum.Definitions.lbignum t len
  -> FStar.HyperStack.ST.Stack Prims.unit