val rsapss_verify:
    a:Hash.hash_alg{S.hash_is_supported a}
  -> modBits:modBits_t ->
  RI.rsapss_verify_st t_limbs (ke modBits) a modBits
let rsapss_verify a modBits eBits pkey saltLen sgntLen sgnt msgLen msg =
  RI.rsapss_verify (ke modBits) a modBits eBits pkey saltLen sgntLen sgnt msgLen msg
val rsapss_verify:
    a:Hash.hash_alg{S.hash_is_supported a}
  -> modBits:modBits_t ->
  RI.rsapss_verify_st t_limbs (ke modBits) a modBits
let rsapss_verify a modBits eBits pkey saltLen sgntLen sgnt msgLen msg =
RI.rsapss_verify (ke modBits) a modBits eBits pkey saltLen sgntLen sgnt msgLen msg
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
Spec.Hash.Definitions.hash_alg Prims.b2t Spec.RSAPSS.hash_is_supported Hacl.RSAPSS.modBits_t Lib.IntTypes.size_t Hacl.Spec.RSAPSS.pkey_len_pre Hacl.RSAPSS.t_limbs Lib.IntTypes.v Lib.IntTypes.U32 Lib.IntTypes.PUB Hacl.Bignum.Definitions.lbignum Lib.IntTypes.op_Plus_Bang Lib.IntTypes.op_Star_Bang FStar.UInt32.__uint_to_t Hacl.Bignum.Definitions.blocks Lib.IntTypes.size Lib.IntTypes.bits Lib.Buffer.lbuffer Lib.IntTypes.uint8 Hacl.Impl.RSAPSS.rsapss_verify Hacl.RSAPSS.ke Prims.bool
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]
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

private
[@CInline]
let load_skey (modBits:modBits_t) : RK.rsapss_load_skey_st t_limbs (ke modBits) modBits =
  RK.rsapss_load_skey (ke modBits) modBits RK.mk_runtime_rsapss_checks (load_pkey modBits)


[@@ Comment "Sign a message `msg` and write the signature to `sgnt`.

@param a Hash algorithm to use. Allowed values for `a` are ...
  - Spec_Hash_Definitions_SHA2_256,
  - Spec_Hash_Definitions_SHA2_384, and
  - Spec_Hash_Definitions_SHA2_512.
@param modBits Count of bits in the modulus (`n`).
@param eBits Count of bits in `e` value.
@param dBits Count of bits in `d` value.
@param skey Pointer to secret key created by `Hacl_RSAPSS_new_rsapss_load_skey`.
@param saltLen Length of salt.
@param salt Pointer to `saltLen` bytes where the salt is read from.
@param msgLen Length of message.
@param msg Pointer to `msgLen` bytes where the message is read from.
@param sgnt Pointer to `ceil(modBits / 8)` bytes where the signature is written to.

@return Returns true if and only if signing was successful."]
val rsapss_sign:
    a:Hash.hash_alg{S.hash_is_supported a}
  -> modBits:modBits_t ->
  RI.rsapss_sign_st t_limbs (ke modBits) a modBits

let rsapss_sign a modBits eBits dBits skey saltLen salt msgLen msg sgnt =
  RI.rsapss_sign (ke modBits) a modBits eBits dBits skey saltLen salt msgLen msg sgnt


[@@ Comment "Verify the signature `sgnt` of a message `msg`.

@param a Hash algorithm to use. Allowed values for `a` are ...
  - Spec_Hash_Definitions_SHA2_256,
  - Spec_Hash_Definitions_SHA2_384, and
  - Spec_Hash_Definitions_SHA2_512.
@param modBits Count of bits in the modulus (`n`).
@param eBits Count of bits in `e` value.
@param pkey Pointer to public key created by `Hacl_RSAPSS_new_rsapss_load_pkey`.
@param saltLen Length of salt.
@param sgntLen Length of signature.
@param sgnt Pointer to `sgntLen` bytes where the signature is read from.
@param msgLen Length of message.
@param msg Pointer to `msgLen` bytes where the message is read from.

@return Returns true if and only if the signature is valid."]
val rsapss_verify:
    a:Hash.hash_alg{S.hash_is_supported a}
  -> modBits:modBits_t ->
  RI.rsapss_verify_st t_limbs (ke modBits) a modBits
val rsapss_verify:
    a:Hash.hash_alg{S.hash_is_supported a}
  -> modBits:modBits_t ->
  RI.rsapss_verify_st t_limbs (ke modBits) a modBits
a: Spec.Hash.Definitions.hash_alg{Spec.RSAPSS.hash_is_supported a} -> modBits: Hacl.RSAPSS.modBits_t
  -> Hacl.Impl.RSAPSS.rsapss_verify_st Hacl.RSAPSS.t_limbs (Hacl.RSAPSS.ke modBits) a modBits