val sub: len:Ghost.erased _ -> MA.bn_field_sub_st t_limbs len
let sub len k aM bM cM =
  let len = field_get_len k in
  MA.bn_field_sub (km len) k aM bM cM
val sub: len:Ghost.erased _ -> MA.bn_field_sub_st t_limbs len
let sub len k aM bM cM =
let len = field_get_len k in
MA.bn_field_sub (km len) k aM bM cM
Hacl.GenericField64.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.GenericField64.fst
FStar.Ghost.erased Hacl.Bignum.meta_len Hacl.GenericField64.t_limbs Hacl.Bignum.MontArithmetic.pbn_mont_ctx Hacl.Bignum.Definitions.lbignum FStar.Ghost.reveal Hacl.Bignum.MontArithmetic.bn_field_sub Hacl.GenericField64.km Prims.unit Hacl.GenericField64.field_get_len
module Hacl.GenericField64

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

let field_modulus_check len n =
  MA.bn_field_check_modulus (km len) n

let field_init len r n =
  MA.bn_field_init len (km len).BM.precomp r n

let field_free k =
  MA.bn_field_free k

let field_get_len k =
  MA.bn_field_get_len k

let to_field len k a aM =
  let len = field_get_len k in
  MA.bn_to_field (km len) k a aM

let from_field len k aM a =
  let len = field_get_len k in
  MA.bn_from_field (km len) k aM a

let add len k aM bM cM =
  let len = field_get_len k in
  MA.bn_field_add (km len) k aM bM cM
val sub: len:Ghost.erased _ -> MA.bn_field_sub_st t_limbs len
len: FStar.Ghost.erased (Hacl.Bignum.meta_len Hacl.GenericField64.t_limbs)
  -> Hacl.Bignum.MontArithmetic.bn_field_sub_st Hacl.GenericField64.t_limbs (FStar.Ghost.reveal len)