val mont_check:BM.bn_check_modulus_st t_limbs n_limbs
val mont_check:BM.bn_check_modulus_st t_limbs n_limbs
let mont_check: BM.bn_check_modulus_st t_limbs n_limbs =
  BM.bn_check_modulus
module Hacl.Bignum4096

open FStar.Mul

module BN = Hacl.Bignum
module BM = Hacl.Bignum.Montgomery
module AM = Hacl.Bignum.AlmostMontgomery
module BE = Hacl.Bignum.Exponentiation
module BR = Hacl.Bignum.ModReduction
module BI = Hacl.Bignum.ModInv

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

let add: BN.bn_add_eq_len_st t_limbs n_limbs =
  BN.bn_add_eq_len n_limbs

let sub: BN.bn_sub_eq_len_st t_limbs n_limbs =
  BN.bn_sub_eq_len n_limbs

let add_mod: BN.bn_add_mod_n_st t_limbs n_limbs =
  BN.bn_add_mod_n n_limbs

let sub_mod: BN.bn_sub_mod_n_st t_limbs n_limbs =
  BN.bn_sub_mod_n n_limbs

let mul (a:lbignum t_limbs n_limbs) : BN.bn_karatsuba_mul_st t_limbs n_limbs a =
  BN.bn_karatsuba_mul n_limbs a
  //BN.bn_mul n_limbs n_limbs a

let sqr (a:lbignum t_limbs n_limbs) : BN.bn_karatsuba_sqr_st t_limbs n_limbs a =
  BN.bn_karatsuba_sqr n_limbs a
  //BN.bn_sqr n_limbs a
  //BN.bn_mul n_limbs n_limbs a a

inline_for_extraction noextract
instance bn_inst: BN.bn t_limbs = {
  BN.len = n_limbs;
  BN.add;
  BN.sub;
  BN.add_mod_n = add_mod;
  BN.sub_mod_n = sub_mod;
  BN.mul;
  BN.sqr
}
/
prims.fst.checked Hacl.Bignum.Montgomery.fsti.checked Hacl.Bignum.ModReduction.fst.checked Hacl.Bignum.ModInv.fst.checked Hacl.Bignum.Exponentiation.fsti.checked Hacl.Bignum.Convert.fst.checked Hacl.Bignum.AlmostMontgomery.fsti.checked Hacl.Bignum.fsti.checked FStar.UInt32.fsti.checked FStar.Tactics.Typeclasses.fsti.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked
Hacl.Bignum4096.fst
Hacl.Bignum.Montgomery.bn_check_modulus_st Hacl.Bignum4096.t_limbs Hacl.Bignum4096.n_limbs
Hacl.Bignum.Montgomery.bn_check_modulus Hacl.Bignum4096.t_limbs Hacl.Bignum4096.n_limbs
let mont_check:BM.bn_check_modulus_st t_limbs n_limbs =
  
BM.bn_check_modulus