val bn_v: #t:limb_t -> #len:size_t -> h:mem -> b:lbignum t len -> GTot nat
let bn_v #t #len h b = S.bn_v #t #(v len) (as_seq h b)
val bn_v: #t:limb_t -> #len:size_t -> h:mem -> b:lbignum t len -> GTot nat
let bn_v #t #len h b =
S.bn_v #t #(v len) (as_seq h b)
Hacl.Bignum.Definitions.fst.checked
prims.fst.checked Lib.IntTypes.fsti.checked Lib.Buffer.fsti.checked Hacl.Spec.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.Definitions.fst
Hacl.Bignum.Definitions.limb_t Lib.IntTypes.size_t FStar.Monotonic.HyperStack.mem Hacl.Bignum.Definitions.lbignum Hacl.Spec.Bignum.Definitions.bn_v Lib.IntTypes.v Lib.IntTypes.U32 Lib.IntTypes.PUB Lib.Buffer.as_seq Lib.Buffer.MUT Hacl.Bignum.Definitions.limb Prims.nat
module Hacl.Bignum.Definitions

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

open Lib.IntTypes
open Lib.Buffer

module S = Hacl.Spec.Bignum.Definitions

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

inline_for_extraction noextract
val blocks: x:size_t{v x > 0} -> m:size_t{v m > 0} -> r:size_t{v r == S.blocks (v x) (v m)}
let blocks x m = (x -. 1ul) /. m +. 1ul

inline_for_extraction noextract
val blocks0: x:size_t -> m:size_t{v m > 0} -> r:size_t{v r == S.blocks0 (v x) (v m)}
let blocks0 x m = if x =. 0ul then 1ul else (x -. 1ul) /. m +. 1ul

inline_for_extraction noextract
let limb_t = S.limb_t

inline_for_extraction noextract
let limb (t:limb_t) = S.limb t

inline_for_extraction noextract
let lbignum (t:limb_t) len = lbuffer (limb t) len

noextract
val bn_v: #t:limb_t -> #len:size_t -> h:mem -> b:lbignum t len -> GTot nat
h: FStar.Monotonic.HyperStack.mem -> b: Hacl.Bignum.Definitions.lbignum t len
  -> Prims.GTot Prims.nat