let salt_len_t (a:Hash.fixed_len_alg) =
  saltLen:size_t{8 + Hash.hash_length a + v saltLen <= max_size_t /\ (8 + Hash.hash_length a + v saltLen) `less_than_max_input_length` a}
let salt_len_t (a: Hash.fixed_len_alg) =
saltLen:
size_t
  { 8 + Hash.hash_length a + v saltLen <= max_size_t /\
    (8 + Hash.hash_length a + v saltLen) `less_than_max_input_length` a }
Hacl.Impl.RSAPSS.Padding.fst.checked
Spec.RSAPSS.fst.checked Spec.Hash.Definitions.fst.checked Spec.Agile.Hash.fsti.checked prims.fst.checked Lib.Sequence.fsti.checked Lib.RawIntTypes.fsti.checked Lib.IntTypes.fsti.checked Lib.ByteBuffer.fsti.checked Lib.Buffer.fsti.checked Hacl.Impl.RSAPSS.MGF.fst.checked Hacl.Bignum.Definitions.fst.checked FStar.UInt8.fsti.checked FStar.UInt32.fsti.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked
Hacl.Impl.RSAPSS.Padding.fst
Spec.Hash.Definitions.fixed_len_alg Lib.IntTypes.size_t Prims.l_and Prims.b2t Prims.op_LessThanOrEqual Prims.op_Addition Spec.Hash.Definitions.hash_length Lib.IntTypes.v Lib.IntTypes.U32 Lib.IntTypes.PUB Lib.IntTypes.max_size_t Hacl.Impl.RSAPSS.Padding.less_than_max_input_length
module Hacl.Impl.RSAPSS.Padding

open FStar.HyperStack
open FStar.HyperStack.ST
open FStar.Mul

open Lib.IntTypes
open Lib.Buffer

open Hacl.Impl.RSAPSS.MGF

module ST = FStar.HyperStack.ST
module LSeq = Lib.Sequence

module Hash = Spec.Agile.Hash
module S = Spec.RSAPSS
module BD = Hacl.Bignum.Definitions


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

inline_for_extraction noextract
let less_than_max_input_length = Spec.Hash.Definitions.less_than_max_input_length

inline_for_extraction noextract
val salt_len_t : a: Spec.Hash.Definitions.fixed_len_alg -> Type0
a: Spec.Hash.Definitions.fixed_len_alg -> Type0