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
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
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
Lib.IntTypes.size_t Prims.b2t Prims.op_GreaterThan Lib.IntTypes.v Lib.IntTypes.U32 Lib.IntTypes.PUB Lib.IntTypes.op_Plus_Dot Lib.IntTypes.op_Slash_Dot Lib.IntTypes.op_Subtraction_Dot FStar.UInt32.__uint_to_t Prims.eq2 Prims.int Prims.l_or Lib.IntTypes.range Prims.l_and Prims.op_LessThanOrEqual Lib.IntTypes.max_size_t FStar.Mul.op_Star Hacl.Spec.Bignum.Definitions.blocks
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)}
x: Lib.IntTypes.size_t{Lib.IntTypes.v x > 0} -> m: Lib.IntTypes.size_t{Lib.IntTypes.v m > 0}
  -> r:
    Lib.IntTypes.size_t
      { Lib.IntTypes.v r ==
        Hacl.Spec.Bignum.Definitions.blocks (Lib.IntTypes.v x) (Lib.IntTypes.v m) }