let lbignum = Hacl.Bignum.Definitions.lbignum
let lbignum =
Hacl.Bignum.Definitions.lbignum
Hacl.Bignum4096.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.Bignum4096.fsti
Hacl.Bignum.Definitions.lbignum
module Hacl.Bignum4096

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.U64

inline_for_extraction noextract
let n_limbs: BN.meta_len t_limbs = 64ul

inline_for_extraction noextract
let n_bytes = n_limbs `FStar.UInt32.mul` 8ul

// A static assert that the number of bytes vs number of blocks matches. This is
// important for bn_to_bytes_be which takes a number of bytes, not a number of
// limbs. (It would be nice to fix this.)
let _ = assert_norm (Hacl.Bignum.Definitions.blocks n_bytes 8ul = n_limbs)

let _ = assert_norm (4096ul = Lib.IntTypes.(size (bits t_limbs)) `FStar.UInt32.mul` n_limbs)
val lbignum : t: Hacl.Bignum.Definitions.limb_t -> len: Lib.IntTypes.size_t -> Type0
t: Hacl.Bignum.Definitions.limb_t -> len: Lib.IntTypes.size_t -> Type0