let less_than_max_input_length = Spec.Hash.Definitions.less_than_max_input_length
let less_than_max_input_length =
Spec.Hash.Definitions.less_than_max_input_length
Hacl.Impl.RSAPSS.MGF.fst.checked
Spec.RSAPSS.fst.checked Spec.Hash.Definitions.fst.checked Spec.Agile.Hash.fsti.checked prims.fst.checked Lib.Sequence.fsti.checked Lib.IntTypes.fsti.checked Lib.ByteSequence.fsti.checked Lib.Buffer.fsti.checked Hacl.Streaming.SHA2.fst.checked Hacl.Hash.Definitions.fst.checked Hacl.Bignum.Definitions.fst.checked FStar.UInt32.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked
Hacl.Impl.RSAPSS.MGF.fst
Spec.Hash.Definitions.less_than_max_input_length
module Hacl.Impl.RSAPSS.MGF

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

open Lib.IntTypes
open Lib.Buffer

open Hacl.Bignum.Definitions

module ST = FStar.HyperStack.ST
module S = Spec.RSAPSS
module BSeq = Lib.ByteSequence
module LSeq = Lib.Sequence

module Hash = Spec.Agile.Hash

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

val hash_len: a:Hash.hash_alg{S.hash_is_supported a} -> Tot (res:size_t{v res == Hash.hash_length a})
[@CInline]
let hash_len a =
  Hacl.Hash.Definitions.hash_len a

inline_for_extraction noextract
let max_input_length = Hash.max_input_length
val less_than_max_input_length : l: Prims.int -> a: Spec.Hash.Definitions.hash_alg -> Prims.bool
l: Prims.int -> a: Spec.Hash.Definitions.hash_alg -> Prims.bool