val field_modulus_check: len:BN.meta_len t_limbs -> MA.bn_field_check_modulus_st t_limbs len
let field_modulus_check len n =
  MA.bn_field_check_modulus (km len) n
val field_modulus_check: len:BN.meta_len t_limbs -> MA.bn_field_check_modulus_st t_limbs len
let field_modulus_check len n =
MA.bn_field_check_modulus (km len) n
Hacl.GenericField32.fst.checked
prims.fst.checked Hacl.Bignum.Montgomery.fsti.checked Hacl.Bignum.MontArithmetic.fsti.checked Hacl.Bignum.fsti.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked
Hacl.GenericField32.fst
Hacl.Bignum.meta_len Hacl.GenericField32.t_limbs Hacl.Bignum.Definitions.lbignum Hacl.Bignum.MontArithmetic.bn_field_check_modulus Hacl.GenericField32.km Prims.bool
module Hacl.GenericField32

open FStar.Mul

module BN = Hacl.Bignum
module MA = Hacl.Bignum.MontArithmetic
module BM = Hacl.Bignum.Montgomery

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

inline_for_extraction noextract
let km (len:BN.meta_len t_limbs) =
  BM.mk_runtime_mont len
val field_modulus_check: len:BN.meta_len t_limbs -> MA.bn_field_check_modulus_st t_limbs len
len: Hacl.Bignum.meta_len Hacl.GenericField32.t_limbs
  -> Hacl.Bignum.MontArithmetic.bn_field_check_modulus_st Hacl.GenericField32.t_limbs len