val hash:
    a:Hash.hash_alg{S.hash_is_supported a}
  -> mHash:lbuffer uint8 (hash_len a)
  -> msgLen:size_t{v msgLen `less_than_max_input_length` a}
  -> msg:lbuffer uint8 msgLen ->
  Stack unit
  (requires fun h -> live h mHash /\ live h msg /\ disjoint msg mHash)
  (ensures  fun h0 _ h1 -> modifies (loc mHash) h0 h1 /\
    as_seq h1 mHash == Hash.hash a (as_seq h0 msg))
let hash a mHash msgLen msg =
  match a with
  | Hash.SHA2_256 -> Hacl.Streaming.SHA2.hash_256 msg msgLen mHash
  | Hash.SHA2_384 -> Hacl.Streaming.SHA2.hash_384 msg msgLen mHash
  | Hash.SHA2_512 -> Hacl.Streaming.SHA2.hash_512 msg msgLen mHash
val hash:
    a:Hash.hash_alg{S.hash_is_supported a}
  -> mHash:lbuffer uint8 (hash_len a)
  -> msgLen:size_t{v msgLen `less_than_max_input_length` a}
  -> msg:lbuffer uint8 msgLen ->
  Stack unit
  (requires fun h -> live h mHash /\ live h msg /\ disjoint msg mHash)
  (ensures  fun h0 _ h1 -> modifies (loc mHash) h0 h1 /\
    as_seq h1 mHash == Hash.hash a (as_seq h0 msg))
let hash a mHash msgLen msg =
match a with
| Hash.SHA2_256 -> Hacl.Streaming.SHA2.hash_256 msg msgLen mHash
| Hash.SHA2_384 -> Hacl.Streaming.SHA2.hash_384 msg msgLen mHash
| Hash.SHA2_512 -> Hacl.Streaming.SHA2.hash_512 msg msgLen mHash
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.hash_alg Prims.b2t Spec.RSAPSS.hash_is_supported Lib.Buffer.lbuffer Lib.IntTypes.uint8 Hacl.Impl.RSAPSS.MGF.hash_len Lib.IntTypes.size_t Hacl.Impl.RSAPSS.MGF.less_than_max_input_length Lib.IntTypes.v Lib.IntTypes.U32 Lib.IntTypes.PUB Hacl.Streaming.SHA2.hash_256 Prims.unit Hacl.Streaming.SHA2.hash_384 Hacl.Streaming.SHA2.hash_512
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

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

val hash:
    a:Hash.hash_alg{S.hash_is_supported a}
  -> mHash:lbuffer uint8 (hash_len a)
  -> msgLen:size_t{v msgLen `less_than_max_input_length` a}
  -> msg:lbuffer uint8 msgLen ->
  Stack unit
  (requires fun h -> live h mHash /\ live h msg /\ disjoint msg mHash)
  (ensures  fun h0 _ h1 -> modifies (loc mHash) h0 h1 /\
    as_seq h1 mHash == Hash.hash a (as_seq h0 msg))

[@CInline]
val hash:
    a:Hash.hash_alg{S.hash_is_supported a}
  -> mHash:lbuffer uint8 (hash_len a)
  -> msgLen:size_t{v msgLen `less_than_max_input_length` a}
  -> msg:lbuffer uint8 msgLen ->
  Stack unit
  (requires fun h -> live h mHash /\ live h msg /\ disjoint msg mHash)
  (ensures  fun h0 _ h1 -> modifies (loc mHash) h0 h1 /\
    as_seq h1 mHash == Hash.hash a (as_seq h0 msg))

    a: Spec.Hash.Definitions.hash_alg{Spec.RSAPSS.hash_is_supported a} ->
    mHash: Lib.Buffer.lbuffer Lib.IntTypes.uint8 (Hacl.Impl.RSAPSS.MGF.hash_len a) ->
    msgLen:
      Lib.IntTypes.size_t{Hacl.Impl.RSAPSS.MGF.less_than_max_input_length (Lib.IntTypes.v msgLen) a} ->
    msg: Lib.Buffer.lbuffer Lib.IntTypes.uint8 msgLen
  -> FStar.HyperStack.ST.Stack Prims.unit