val bn_mod_slow_precomp:
    #t:limb_t
  -> #len:BN.bn_len t
  -> n:lbignum t len
  -> mu:limb t
  -> r2:lbignum t len
  -> a:lbignum t (len + len) ->
  lbignum t len
let bn_mod_slow_precomp #t #len n mu r2 a =
  let a_mod = BAM.bn_almost_mont_reduction n mu a in
  let res = BM.bn_to_mont n mu r2 a_mod in
  res
val bn_mod_slow_precomp:
    #t:limb_t
  -> #len:BN.bn_len t
  -> n:lbignum t len
  -> mu:limb t
  -> r2:lbignum t len
  -> a:lbignum t (len + len) ->
  lbignum t len
let bn_mod_slow_precomp #t #len n mu r2 a =
let a_mod = BAM.bn_almost_mont_reduction n mu a in
let res = BM.bn_to_mont n mu r2 a_mod in
res
Hacl.Spec.Bignum.ModReduction.fst.checked
prims.fst.checked Lib.Sequence.fsti.checked Lib.IntTypes.fsti.checked Hacl.Spec.Montgomery.Lemmas.fst.checked Hacl.Spec.Bignum.Montgomery.fsti.checked Hacl.Spec.Bignum.Definitions.fst.checked Hacl.Spec.Bignum.AlmostMontgomery.fsti.checked Hacl.Spec.Bignum.fsti.checked Hacl.Spec.AlmostMontgomery.Lemmas.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Math.Lemmas.fst.checked FStar.Calc.fsti.checked
Hacl.Spec.Bignum.ModReduction.fst
Hacl.Spec.Bignum.Definitions.limb_t Hacl.Spec.Bignum.bn_len Hacl.Spec.Bignum.Definitions.lbignum Hacl.Spec.Bignum.Definitions.limb Prims.op_Addition Hacl.Spec.Bignum.Montgomery.bn_to_mont Hacl.Spec.Bignum.AlmostMontgomery.bn_almost_mont_reduction
module Hacl.Spec.Bignum.ModReduction

open FStar.Mul

open Lib.IntTypes
open Lib.Sequence

open Hacl.Spec.Bignum.Definitions

module M = Hacl.Spec.Montgomery.Lemmas
module AM = Hacl.Spec.AlmostMontgomery.Lemmas

module BM = Hacl.Spec.Bignum.Montgomery
module BAM = Hacl.Spec.Bignum.AlmostMontgomery
module BN = Hacl.Spec.Bignum

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

///  Modular reduction based on Montgomery arithmetic

val bn_mod_slow_precomp:
    #t:limb_t
  -> #len:BN.bn_len t
  -> n:lbignum t len
  -> mu:limb t
  -> r2:lbignum t len
  -> a:lbignum t (len + len) ->
  lbignum t len
val bn_mod_slow_precomp:
    #t:limb_t
  -> #len:BN.bn_len t
  -> n:lbignum t len
  -> mu:limb t
  -> r2:lbignum t len
  -> a:lbignum t (len + len) ->
  lbignum t len

    n: Hacl.Spec.Bignum.Definitions.lbignum t len ->
    mu: Hacl.Spec.Bignum.Definitions.limb t ->
    r2: Hacl.Spec.Bignum.Definitions.lbignum t len ->
    a: Hacl.Spec.Bignum.Definitions.lbignum t (len + len)
  -> Hacl.Spec.Bignum.Definitions.lbignum t len