val mgf_hash_f:
    a:Hash.hash_alg{hash_is_supported a}
  -> len:size_nat{len + 4 <= max_size_t /\ (len + 4) `Hash.less_than_max_input_length` a}
  -> i:size_nat
  -> mgfseed_counter:lbytes (len + 4) ->
  lbytes (len + 4) & lbytes (Hash.hash_length a)
let mgf_hash_f a len i mgfseed_counter =
  let counter = nat_to_intseq_be 4 i in
  let mgfseed_counter = update_sub mgfseed_counter len 4 counter in
  let block = Hash.hash a mgfseed_counter in
  mgfseed_counter, block
val mgf_hash_f:
    a:Hash.hash_alg{hash_is_supported a}
  -> len:size_nat{len + 4 <= max_size_t /\ (len + 4) `Hash.less_than_max_input_length` a}
  -> i:size_nat
  -> mgfseed_counter:lbytes (len + 4) ->
  lbytes (len + 4) & lbytes (Hash.hash_length a)
let mgf_hash_f a len i mgfseed_counter =
let counter = nat_to_intseq_be 4 i in
let mgfseed_counter = update_sub mgfseed_counter len 4 counter in
let block = Hash.hash a mgfseed_counter in
mgfseed_counter, block
Spec.RSAPSS.fst.checked
Spec.Agile.Hash.fsti.checked prims.fst.checked Lib.Sequence.fsti.checked Lib.RawIntTypes.fsti.checked Lib.NatMod.fsti.checked Lib.LoopCombinators.fsti.checked Lib.IntTypes.fsti.checked Lib.ByteSequence.fsti.checked FStar.UInt8.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Math.Lemmas.fst.checked FStar.Calc.fsti.checked
Spec.RSAPSS.fst
Spec.Hash.Definitions.hash_alg Prims.b2t Spec.RSAPSS.hash_is_supported Lib.IntTypes.size_nat Prims.l_and Prims.op_LessThanOrEqual Prims.op_Addition Lib.IntTypes.max_size_t Spec.Hash.Definitions.less_than_max_input_length Lib.ByteSequence.lbytes FStar.Pervasives.Native.Mktuple2 Spec.Hash.Definitions.hash_length Lib.Sequence.lseq Lib.IntTypes.int_t Lib.IntTypes.U8 Lib.IntTypes.SEC Spec.Hash.Definitions.hash_length' Spec.Agile.Hash.hash Prims.eq2 Lib.Sequence.sub Prims.l_Forall Prims.nat Prims.l_or Prims.op_LessThan FStar.Seq.Base.index Lib.Sequence.to_seq Lib.Sequence.index Lib.Sequence.update_sub Lib.IntTypes.uint_t Lib.Sequence.seq Lib.Sequence.length Prims.pow2 Prims.op_Multiply Lib.ByteSequence.nat_from_intseq_be Lib.ByteSequence.nat_to_intseq_be FStar.Pervasives.Native.tuple2
module Spec.RSAPSS

open FStar.Mul
open Lib.IntTypes

open Lib.NatMod
open Lib.Sequence
open Lib.ByteSequence
open Lib.LoopCombinators

module Hash = Spec.Agile.Hash

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

(**
 RFC spec of RSA-PSS: https://tools.ietf.org/html/rfc8017#section-8.1
 List of supported hash functions: https://tools.ietf.org/html/rfc8446#appendix-B.3.1.3
 Mask generation function: https://tools.ietf.org/html/rfc8017#page-67
*)

///
/// Auxillary functions
///

val blocks: x:size_pos -> m:size_pos -> Tot (r:size_pos{x <= m * r})
let blocks x m = (x - 1) / m + 1

val xor_bytes: #len:size_pos -> b1:lbytes len -> b2:lbytes len -> Tot (lbytes len)
let xor_bytes #len b1 b2 = map2 (fun x y -> x ^. y) b1 b2

let hash_is_supported (a:Hash.hash_alg) : Tot bool =
  match a with
  | Hash.SHA2_256 -> true
  | Hash.SHA2_384 -> true
  | Hash.SHA2_512 -> true
  | _ -> false

(* Mask Generation Function *)
val mgf_hash_f:
    a:Hash.hash_alg{hash_is_supported a}
  -> len:size_nat{len + 4 <= max_size_t /\ (len + 4) `Hash.less_than_max_input_length` a}
  -> i:size_nat
  -> mgfseed_counter:lbytes (len + 4) ->
  lbytes (len + 4) & lbytes (Hash.hash_length a)
val mgf_hash_f:
    a:Hash.hash_alg{hash_is_supported a}
  -> len:size_nat{len + 4 <= max_size_t /\ (len + 4) `Hash.less_than_max_input_length` a}
  -> i:size_nat
  -> mgfseed_counter:lbytes (len + 4) ->
  lbytes (len + 4) & lbytes (Hash.hash_length a)

    a: Spec.Hash.Definitions.hash_alg{Spec.RSAPSS.hash_is_supported a} ->
    len:
      Lib.IntTypes.size_nat
        { len + 4 <= Lib.IntTypes.max_size_t /\
          Spec.Hash.Definitions.less_than_max_input_length (len + 4) a } ->
    i: Lib.IntTypes.size_nat ->
    mgfseed_counter: Lib.ByteSequence.lbytes (len + 4)
  -> Lib.ByteSequence.lbytes (len + 4) *
    Lib.ByteSequence.lbytes (Spec.Hash.Definitions.hash_length a)