let bn_mod_slow_precomp_st (t:limb_t) (len:BN.meta_len t) =
     n:lbignum t len
  -> mu:limb t
  -> r2:lbignum t len
  -> a:lbignum t (len +! len)
  -> res:lbignum t len ->
  Stack unit
  (requires fun h ->
    live h n /\ live h a /\ live h r2 /\ live h res /\
    disjoint res n /\ disjoint res a /\ disjoint res r2 /\ disjoint r2 n /\

    SM.bn_mont_pre (as_seq h n) mu /\
    bn_v h r2 == pow2 (2 * bits t * v len) % bn_v h n)
  (ensures  fun h0 _ h1 -> modifies (loc res) h0 h1 /\
    bn_v h1 res == bn_v h0 a % bn_v h0 n)
let bn_mod_slow_precomp_st (t: limb_t) (len: BN.meta_len t) =

    n: lbignum t len ->
    mu: limb t ->
    r2: lbignum t len ->
    a: lbignum t (len +! len) ->
    res: lbignum t len
  -> Stack unit
      (requires
        fun h ->
          live h n /\ live h a /\ live h r2 /\ live h res /\ disjoint res n /\ disjoint res a /\
          disjoint res r2 /\ disjoint r2 n /\ SM.bn_mont_pre (as_seq h n) mu /\
          bn_v h r2 == pow2 ((2 * bits t) * v len) % bn_v h n)
      (ensures fun h0 _ h1 -> modifies (loc res) h0 h1 /\ bn_v h1 res == bn_v h0 a % bn_v h0 n)
Hacl.Bignum.ModReduction.fst.checked
prims.fst.checked Lib.IntTypes.fsti.checked Lib.Buffer.fsti.checked Hacl.Spec.Bignum.Montgomery.fsti.checked Hacl.Spec.Bignum.ModReduction.fst.checked Hacl.Spec.Bignum.Definitions.fst.checked Hacl.Bignum.Montgomery.fsti.checked Hacl.Bignum.Definitions.fst.checked Hacl.Bignum.AlmostMontgomery.fsti.checked Hacl.Bignum.fsti.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked
Hacl.Bignum.ModReduction.fst
Hacl.Bignum.Definitions.limb_t Hacl.Bignum.meta_len Hacl.Bignum.Definitions.lbignum Hacl.Bignum.Definitions.limb Lib.IntTypes.op_Plus_Bang Lib.IntTypes.U32 Lib.IntTypes.PUB Prims.unit FStar.Monotonic.HyperStack.mem Prims.l_and Lib.Buffer.live Lib.Buffer.MUT Lib.Buffer.disjoint Hacl.Spec.Bignum.Montgomery.bn_mont_pre Lib.IntTypes.v Lib.Buffer.as_seq Prims.eq2 Prims.int Hacl.Bignum.Definitions.bn_v Prims.op_Modulus Prims.pow2 FStar.Mul.op_Star Lib.IntTypes.bits Lib.Buffer.modifies Lib.Buffer.loc
module Hacl.Bignum.ModReduction

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.ModReduction

module BN = Hacl.Bignum
module AM = Hacl.Bignum.AlmostMontgomery
module BM = Hacl.Bignum.Montgomery
module SM = Hacl.Spec.Bignum.Montgomery
module BD = Hacl.Spec.Bignum.Definitions

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

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