val add: len:BN.meta_len t_limbs -> BN.bn_add_eq_len_st t_limbs len
let add len a b res =
  (ke len).BE.bn.BN.add a b res
val add: len:BN.meta_len t_limbs -> BN.bn_add_eq_len_st t_limbs len
let add len a b res =
(ke len).BE.bn.BN.add a b res
Hacl.Bignum64.fst.checked
prims.fst.checked Hacl.Bignum.Montgomery.fsti.checked Hacl.Bignum.MontArithmetic.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.Pervasives.fsti.checked FStar.Mul.fst.checked
Hacl.Bignum64.fst
Hacl.Bignum.meta_len Hacl.Bignum64.t_limbs Hacl.Bignum.Definitions.lbignum Hacl.Bignum.__proj__Mkbn__item__add Hacl.Bignum.Exponentiation.__proj__Mkexp__item__bn Hacl.Bignum64.ke Hacl.Spec.Bignum.Base.carry
module Hacl.Bignum64

open FStar.Mul

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

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

inline_for_extraction noextract
let kam (len:BN.meta_len t_limbs) =
  AM.mk_runtime_almost_mont #t_limbs len

inline_for_extraction noextract
let ke (len:BN.meta_len t_limbs) =
  BE.mk_runtime_exp #t_limbs len
val add: len:BN.meta_len t_limbs -> BN.bn_add_eq_len_st t_limbs len
len: Hacl.Bignum.meta_len Hacl.Bignum64.t_limbs
  -> Hacl.Bignum.bn_add_eq_len_st Hacl.Bignum64.t_limbs len