let mod_inv_limb_st (t:limb_t) =
  n0:limb t ->
  Stack (limb t)
  (requires fun h -> True)
  (ensures  fun h0 r h1 -> modifies0 h0 h1 /\
    r == S.mod_inv_limb n0)
let mod_inv_limb_st (t: limb_t) =
n0: limb t
  -> Stack (limb t)
      (requires fun h -> True)
      (ensures fun h0 r h1 -> modifies0 h0 h1 /\ r == S.mod_inv_limb n0)
Hacl.Bignum.ModInvLimb.fsti.checked
prims.fst.checked Lib.IntTypes.fsti.checked Lib.Buffer.fsti.checked Hacl.Spec.Bignum.ModInvLimb.fsti.checked Hacl.Bignum.Definitions.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked
Hacl.Bignum.ModInvLimb.fsti
Hacl.Bignum.Definitions.limb_t Hacl.Bignum.Definitions.limb FStar.Monotonic.HyperStack.mem Prims.l_True Prims.l_and Lib.Buffer.modifies0 Prims.eq2 Hacl.Spec.Bignum.Definitions.limb Hacl.Spec.Bignum.ModInvLimb.mod_inv_limb
module Hacl.Bignum.ModInvLimb

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

open Lib.IntTypes
open Lib.Buffer

open Hacl.Bignum.Definitions

module S = Hacl.Spec.Bignum.ModInvLimb


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

inline_for_extraction noextract
val mod_inv_limb_st : t: Hacl.Bignum.Definitions.limb_t -> Type0
t: Hacl.Bignum.Definitions.limb_t -> Type0