let bn_check_mod_inv_prime_st (t:limb_t) (len:BN.meta_len t) =
    n:lbignum t len
  -> a:lbignum t len ->
  Stack (limb t)
  (requires fun h -> live h n /\ live h a /\ disjoint n a)
  (ensures  fun h0 r h1 -> modifies0 h0 h1 /\
    r == S.bn_check_mod_inv_prime (as_seq h0 n) (as_seq h0 a))
let bn_check_mod_inv_prime_st (t: limb_t) (len: BN.meta_len t) =
n: lbignum t len -> a: lbignum t len
  -> Stack (limb t)
      (requires fun h -> live h n /\ live h a /\ disjoint n a)
      (ensures
        fun h0 r h1 -> modifies0 h0 h1 /\ r == S.bn_check_mod_inv_prime (as_seq h0 n) (as_seq h0 a))
Hacl.Bignum.ModInv.fst.checked
prims.fst.checked LowStar.Ignore.fsti.checked Lib.NatMod.fsti.checked Lib.IntTypes.fsti.checked Lib.Buffer.fsti.checked Hacl.Spec.Bignum.ModInv.fst.checked Hacl.Spec.Bignum.Definitions.fst.checked Hacl.Bignum.Montgomery.fsti.checked Hacl.Bignum.Exponentiation.fsti.checked Hacl.Bignum.Definitions.fst.checked Hacl.Bignum.fsti.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked
Hacl.Bignum.ModInv.fst
Hacl.Bignum.Definitions.limb_t Hacl.Bignum.meta_len Hacl.Bignum.Definitions.lbignum Hacl.Bignum.Definitions.limb FStar.Monotonic.HyperStack.mem Prims.l_and Lib.Buffer.live Lib.Buffer.MUT Lib.Buffer.disjoint Lib.Buffer.modifies0 Prims.eq2 Hacl.Spec.Bignum.Definitions.limb Hacl.Spec.Bignum.ModInv.bn_check_mod_inv_prime Lib.IntTypes.v Lib.IntTypes.U32 Lib.IntTypes.PUB Lib.Buffer.as_seq
module Hacl.Bignum.ModInv

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

open Lib.IntTypes
open Lib.Buffer

open Hacl.Bignum.Definitions

module ST = FStar.HyperStack.ST
module S = Hacl.Spec.Bignum.ModInv

module BN = Hacl.Bignum
module BE = Hacl.Bignum.Exponentiation
module BM = Hacl.Bignum.Montgomery
module SD = Hacl.Spec.Bignum.Definitions

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

inline_for_extraction noextract
val bn_check_mod_inv_prime_st : t: Hacl.Bignum.Definitions.limb_t -> len: Hacl.Bignum.meta_len t -> Type0
t: Hacl.Bignum.Definitions.limb_t -> len: Hacl.Bignum.meta_len t -> Type0