let bn_mod_slow_st (t:limb_t) (len:BN.meta_len t) =
    nBits:size_t
  -> n: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 res /\
    disjoint res n /\ disjoint res a /\

    1 < bn_v h n /\ bn_v h n % 2 = 1 /\
    v nBits / bits t < v len /\ pow2 (v nBits) < bn_v h n)
  (ensures  fun h0 r h1 -> modifies (loc res) h0 h1 /\
    bn_v h1 res == bn_v h0 a % bn_v h0 n)
let bn_mod_slow_st (t: limb_t) (len: BN.meta_len t) =
nBits: size_t -> n: 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 res /\ disjoint res n /\ disjoint res a /\ 1 < bn_v h n /\
          bn_v h n % 2 = 1 /\ v nBits / bits t < v len /\ pow2 (v nBits) < bn_v h n)
      (ensures fun h0 r 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 Lib.IntTypes.size_t Hacl.Bignum.Definitions.lbignum 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 Hacl.Bignum.Definitions.limb Lib.Buffer.disjoint Prims.b2t Prims.op_LessThan Hacl.Bignum.Definitions.bn_v Prims.op_Equality Prims.int Prims.op_Modulus Prims.op_Division Lib.IntTypes.v Lib.IntTypes.bits Prims.pow2 Lib.Buffer.modifies Lib.Buffer.loc Prims.eq2
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
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)


inline_for_extraction noextract
val bn_mod_slow_precomp:
    #t:limb_t
  -> k:AM.almost_mont t ->
  bn_mod_slow_precomp_st t k.AM.bn.BN.len

let bn_mod_slow_precomp #t k n mu r2 a res =
  let h0 = ST.get () in
  S.bn_mod_slow_precomp_lemma (as_seq h0 n) mu (as_seq h0 r2) (as_seq h0 a);
  [@inline_let] let len = k.AM.bn.BN.len in
  push_frame ();
  let a_mod = create len (uint #t #SEC 0) in
  let a1 = create (len +! len) (uint #t #SEC 0) in
  copy a1 a;
  AM.reduction n mu a1 a_mod;
  AM.to n mu r2 a_mod res;
  pop_frame ()


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