let n_bytes = n_limbs `FStar.UInt32.mul` 4ul
let n_bytes =
n_limbs `FStar.UInt32.mul` 4ul
Hacl.Bignum256_32.fsti.checked
prims.fst.checked Lib.IntTypes.fsti.checked Hacl.Bignum.SafeAPI.fst.checked Hacl.Bignum.MontArithmetic.fsti.checked Hacl.Bignum.Definitions.fst.checked Hacl.Bignum.Convert.fst.checked Hacl.Bignum.fsti.checked FStar.UInt32.fsti.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked
Hacl.Bignum256_32.fsti
FStar.UInt32.mul Hacl.Bignum256_32.n_limbs FStar.UInt32.__uint_to_t
module Hacl.Bignum256_32

open FStar.Mul

module BN = Hacl.Bignum
module BS = Hacl.Bignum.SafeAPI
module MA = Hacl.Bignum.MontArithmetic

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

inline_for_extraction noextract
let t_limbs: Hacl.Bignum.Definitions.limb_t = Lib.IntTypes.U32

inline_for_extraction noextract
let n_limbs: BN.meta_len t_limbs = 8ul
val n_bytes : FStar.UInt32.t
FStar.UInt32.t