val os2ip: #len:size_nat -> b:lbytes len -> Tot (res:nat{res < pow2 (8 * len)})
let os2ip #len b = nat_from_bytes_be b
val os2ip: #len:size_nat -> b:lbytes len -> Tot (res:nat{res < pow2 (8 * len)})
let os2ip #len b =
nat_from_bytes_be b
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
Lib.IntTypes.size_nat Lib.ByteSequence.lbytes Lib.ByteSequence.nat_from_bytes_be Lib.IntTypes.SEC Prims.nat Prims.b2t Prims.op_LessThan Prims.pow2 FStar.Mul.op_Star
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)

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

let mgf_hash_a (len:size_nat{len + 4 <= max_size_t}) (n:pos) (i:nat{i <= n}) = lbytes (len + 4)

val mgf_hash:
    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}
  -> mgfseed:lbytes len
  -> maskLen:size_pos{(blocks maskLen (Hash.hash_length a)) * Hash.hash_length a < pow2 32} ->
  Tot (lbytes maskLen)

let mgf_hash a len mgfseed maskLen =
  let mgfseed_counter = create (len + 4) (u8 0) in
  let mgfseed_counter = update_sub mgfseed_counter 0 len mgfseed in

  let hLen = Hash.hash_length a in
  let n = blocks maskLen hLen in
  let _, acc = generate_blocks #uint8 hLen n n (mgf_hash_a len n) (mgf_hash_f a len) mgfseed_counter in
  sub #uint8 #(n * hLen) acc 0 maskLen


(* Bignum convert functions *)
val os2ip: #len:size_nat -> b:lbytes len -> Tot (res:nat{res < pow2 (8 * len)})
b: Lib.ByteSequence.lbytes len -> res: Prims.nat{res < Prims.pow2 (8 * len)}