val load_pkey (modBits: modBits_t) : RK.rsapss_load_pkey_st t_limbs (ke modBits) modBits
let load_pkey (modBits:modBits_t) : RK.rsapss_load_pkey_st t_limbs (ke modBits) modBits =
  RK.rsapss_load_pkey (ke modBits) modBits RK.mk_runtime_rsapss_checks
val load_pkey (modBits: modBits_t) : RK.rsapss_load_pkey_st t_limbs (ke modBits) modBits
let load_pkey (modBits: modBits_t) : RK.rsapss_load_pkey_st t_limbs (ke modBits) modBits =
RK.rsapss_load_pkey (ke modBits) modBits RK.mk_runtime_rsapss_checks
Hacl.RSAPSS.fst.checked
Spec.RSAPSS.fst.checked Spec.Agile.Hash.fsti.checked prims.fst.checked Lib.IntTypes.fsti.checked Hacl.Impl.RSAPSS.MGF.fst.checked Hacl.Impl.RSAPSS.Keys.fst.checked Hacl.Impl.RSAPSS.fst.checked Hacl.Bignum.Montgomery.fsti.checked Hacl.Bignum.Exponentiation.fsti.checked Hacl.Bignum.Definitions.fst.checked Hacl.Bignum.fsti.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked
Hacl.RSAPSS.fst
Hacl.RSAPSS.modBits_t Hacl.Impl.RSAPSS.Keys.rsapss_load_pkey Hacl.RSAPSS.t_limbs Hacl.RSAPSS.ke Hacl.Impl.RSAPSS.Keys.mk_runtime_rsapss_checks Hacl.Impl.RSAPSS.Keys.rsapss_load_pkey_st
module Hacl.RSAPSS

open FStar.Mul
open Lib.IntTypes

module S = Spec.RSAPSS
module Hash = Spec.Agile.Hash

module RI = Hacl.Impl.RSAPSS
module RK = Hacl.Impl.RSAPSS.Keys

module BN = Hacl.Bignum
module BM = Hacl.Bignum.Montgomery
module BE = Hacl.Bignum.Exponentiation
module BD = Hacl.Bignum.Definitions

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

inline_for_extraction noextract
let t_limbs = U64

inline_for_extraction noextract
let modBits_t = RI.modBits_t t_limbs

inline_for_extraction noextract
let ke (modBits:modBits_t) =
  BE.mk_runtime_exp #t_limbs (BD.blocks modBits (size (bits t_limbs)))


private
[@CInline]
val load_pkey (modBits: modBits_t) : RK.rsapss_load_pkey_st t_limbs (ke modBits) modBits
modBits: Hacl.RSAPSS.modBits_t
  -> Hacl.Impl.RSAPSS.Keys.rsapss_load_pkey_st Hacl.RSAPSS.t_limbs (Hacl.RSAPSS.ke modBits) modBits