let ke (a:S.ffdhe_alg) =
  BE.mk_runtime_exp #t_limbs (BD.blocks (DH.ffdhe_len a) (size (numbytes t_limbs)))
let ke (a: S.ffdhe_alg) =
BE.mk_runtime_exp #t_limbs (BD.blocks (DH.ffdhe_len a) (size (numbytes t_limbs)))
Hacl.FFDHE.fst.checked
Spec.FFDHE.fst.checked prims.fst.checked Lib.IntTypes.fsti.checked Hacl.Impl.FFDHE.fst.checked Hacl.Bignum.Exponentiation.fsti.checked Hacl.Bignum.Definitions.fst.checked FStar.Pervasives.fsti.checked
Hacl.FFDHE.fst
Spec.FFDHE.ffdhe_alg Hacl.Bignum.Exponentiation.mk_runtime_exp Hacl.FFDHE.t_limbs Hacl.Bignum.Definitions.blocks Hacl.Impl.FFDHE.ffdhe_len Lib.IntTypes.size Lib.IntTypes.numbytes Hacl.Bignum.Exponentiation.exp
module Hacl.FFDHE

open Lib.IntTypes

module S = Spec.FFDHE
module DH = Hacl.Impl.FFDHE
module BD = Hacl.Bignum.Definitions
module BE = Hacl.Bignum.Exponentiation

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

inline_for_extraction noextract
let t_limbs = U64

inline_for_extraction noextract
val ke : a: Spec.FFDHE.ffdhe_alg -> Hacl.Bignum.Exponentiation.exp Hacl.FFDHE.t_limbs
a: Spec.FFDHE.ffdhe_alg -> Hacl.Bignum.Exponentiation.exp Hacl.FFDHE.t_limbs