let bn_check_modulus_st (t:limb_t) (len:BN.meta_len t) =
  n:lbignum t len ->
  Stack (limb t)
  (requires fun h -> live h n)
  (ensures  fun h0 r h1 -> modifies0 h0 h1 /\
    r == S.bn_check_modulus (as_seq h0 n))
let bn_check_modulus_st (t: limb_t) (len: BN.meta_len t) =
n: lbignum t len
  -> Stack (limb t)
      (requires fun h -> live h n)
      (ensures fun h0 r h1 -> modifies0 h0 h1 /\ r == S.bn_check_modulus (as_seq h0 n))
Hacl.Bignum.Montgomery.fsti.checked
prims.fst.checked Lib.IntTypes.fsti.checked Lib.Buffer.fsti.checked Hacl.Spec.Bignum.Montgomery.fsti.checked Hacl.Bignum.ModInvLimb.fsti.checked Hacl.Bignum.Definitions.fst.checked Hacl.Bignum.fsti.checked FStar.Tactics.Typeclasses.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked
Hacl.Bignum.Montgomery.fsti
Hacl.Bignum.Definitions.limb_t Hacl.Bignum.meta_len Hacl.Bignum.Definitions.lbignum Hacl.Bignum.Definitions.limb FStar.Monotonic.HyperStack.mem Lib.Buffer.live Lib.Buffer.MUT Prims.l_and Lib.Buffer.modifies0 Prims.eq2 Hacl.Spec.Bignum.Definitions.limb Hacl.Spec.Bignum.Montgomery.bn_check_modulus Lib.IntTypes.v Lib.IntTypes.U32 Lib.IntTypes.PUB Lib.Buffer.as_seq
module Hacl.Bignum.Montgomery

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.Montgomery
module BN = Hacl.Bignum

include Hacl.Bignum.ModInvLimb

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


inline_for_extraction noextract
val bn_check_modulus_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