val mgf_hash: a:Hash.hash_alg{S.hash_is_supported a} -> mgf_hash_st a
let mgf_hash a len mgfseed maskLen res =
  push_frame ();
  let mgfseed_counter = create (len +! 4ul) (u8 0) in
  update_sub mgfseed_counter 0ul len mgfseed;

  let hLen = hash_len a in
  let n = blocks maskLen hLen in
  let accLen = n *! hLen in
  let acc = create accLen (u8 0) in
  [@ inline_let]
  let a_spec = S.mgf_hash_a (v len) (v n) in
  let h0 = ST.get () in
  fill_blocks h0 hLen n acc a_spec
    (fun h i -> as_seq h mgfseed_counter)
    (fun _ -> loc mgfseed_counter)
    (fun h0 -> S.mgf_hash_f a (v len))
    (fun i ->
      let acc_i = sub acc (i *! hLen) hLen in
      mgf_hash_f a len i mgfseed_counter acc_i);
  copy res (sub acc 0ul maskLen);
  pop_frame ()
val mgf_hash: a:Hash.hash_alg{S.hash_is_supported a} -> mgf_hash_st a
let mgf_hash a len mgfseed maskLen res =
push_frame ();
let mgfseed_counter = create (len +! 4ul) (u8 0) in
update_sub mgfseed_counter 0ul len mgfseed;
let hLen = hash_len a in
let n = blocks maskLen hLen in
let accLen = n *! hLen in
let acc = create accLen (u8 0) in
[@@ inline_let ]let a_spec = S.mgf_hash_a (v len) (v n) in
let h0 = ST.get () in
fill_blocks h0
  hLen
  n
  acc
  a_spec
  (fun h i -> as_seq h mgfseed_counter)
  (fun _ -> loc mgfseed_counter)
  (fun h0 -> S.mgf_hash_f a (v len))
  (fun i ->
      let acc_i = sub acc (i *! hLen) hLen in
      mgf_hash_f a len i mgfseed_counter acc_i);
copy res (sub acc 0ul maskLen);
pop_frame ()
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.IntTypes.size_t Prims.l_and Prims.op_LessThanOrEqual Prims.op_Addition Lib.IntTypes.v Lib.IntTypes.U32 Lib.IntTypes.PUB Lib.IntTypes.max_size_t Hacl.Impl.RSAPSS.MGF.less_than_max_input_length Lib.Buffer.lbuffer Lib.IntTypes.uint8 Prims.op_LessThan FStar.Mul.op_Star Spec.RSAPSS.blocks Spec.Hash.Definitions.hash_length Prims.pow2 FStar.HyperStack.ST.pop_frame Prims.unit Lib.Buffer.copy Lib.Buffer.MUT Lib.Buffer.lbuffer_t Lib.IntTypes.int_t Lib.IntTypes.U8 Lib.IntTypes.SEC Lib.Buffer.sub Lib.IntTypes.uint_t FStar.UInt32.__uint_to_t Lib.Buffer.fill_blocks FStar.Monotonic.HyperStack.mem Lib.IntTypes.size_nat Lib.Buffer.as_seq Lib.IntTypes.op_Plus_Bang Lib.Buffer.loc LowStar.Monotonic.Buffer.loc LowStar.Monotonic.Buffer.loc_disjoint LowStar.Monotonic.Buffer.loc_includes LowStar.Monotonic.Buffer.address_liveness_insensitive_locs Spec.RSAPSS.mgf_hash_f FStar.Pervasives.Native.tuple2 Lib.Sequence.lseq Hacl.Impl.RSAPSS.MGF.mgf_hash_f Lib.IntTypes.op_Star_Bang FStar.HyperStack.ST.get Prims.nat Spec.RSAPSS.mgf_hash_a Lib.Buffer.create Lib.IntTypes.u8 Prims.eq2 Prims.int Prims.l_or Lib.IntTypes.range Prims.op_GreaterThan Prims.op_Subtraction Prims.op_Multiply Hacl.Spec.Bignum.Definitions.blocks Hacl.Bignum.Definitions.blocks Prims.op_GreaterThanOrEqual Hacl.Impl.RSAPSS.MGF.hash_len Lib.Buffer.update_sub Lib.IntTypes.add FStar.UInt32.uint_to_t FStar.UInt32.t FStar.HyperStack.ST.push_frame
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]
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


(* Mask Generation Function *)
inline_for_extraction noextract
val counter_to_bytes:
    i:size_t
  -> counter:lbuffer uint8 4ul ->
  Stack unit
  (requires fun h -> live h counter)
  (ensures  fun h0 _ h1 -> modifies (loc counter) h0 h1 /\
    as_seq h1 counter == BSeq.nat_to_intseq_be 4 (v i))

let counter_to_bytes i c =
  let h0 = ST.get () in
  c.(0ul) <- to_u8 (i >>. 24ul);
  c.(1ul) <- to_u8 (i >>. 16ul);
  c.(2ul) <- to_u8 (i >>. 8ul);
  c.(3ul) <- to_u8 i;
  let h1 = ST.get () in
  BSeq.index_nat_to_intseq_be #U8 #SEC 4 (v i) 0;
  BSeq.index_nat_to_intseq_be #U8 #SEC 4 (v i) 1;
  BSeq.index_nat_to_intseq_be #U8 #SEC 4 (v i) 2;
  BSeq.index_nat_to_intseq_be #U8 #SEC 4 (v i) 3;
  LSeq.eq_intro (as_seq h1 c) (BSeq.nat_to_intseq_be 4 (v i))


inline_for_extraction noextract
val mgf_hash_f:
    a:Hash.hash_alg{S.hash_is_supported a}
  -> len:size_t{v len + 4 <= max_size_t /\ (v len + 4) `less_than_max_input_length` a}
  -> i:size_t
  -> mgfseed_counter:lbuffer uint8 (len +! 4ul)
  -> block:lbuffer uint8 (hash_len a) ->
  Stack unit
  (requires fun h -> live h mgfseed_counter /\ live h block /\ disjoint mgfseed_counter block)
  (ensures  fun h0 _ h1 -> modifies (loc mgfseed_counter |+| loc block) h0 h1 /\
    (as_seq h1 mgfseed_counter, as_seq h1 block) == S.mgf_hash_f a (v len) (v i) (as_seq h0 mgfseed_counter))

let mgf_hash_f a len i mgfseed_counter block =
  let h0 = ST.get () in
  update_sub_f h0 mgfseed_counter len 4ul
    (fun h -> BSeq.nat_to_intseq_be 4 (v i))
    (fun _ ->
      let c = sub mgfseed_counter len 4ul in
      counter_to_bytes i c);
  hash a block (len +! 4ul) mgfseed_counter


inline_for_extraction noextract
let mgf_hash_st (a:Hash.hash_alg{S.hash_is_supported a}) =
  len:size_t{v len + 4 <= max_size_t /\ (v len + 4) `less_than_max_input_length` a}
  -> mgfseed:lbuffer uint8 len
  -> maskLen:size_t{0 < v maskLen /\ S.blocks (v maskLen) (Hash.hash_length a) * Hash.hash_length a < pow2 32}
  -> res:lbuffer uint8 maskLen ->
  Stack unit
  (requires fun h -> live h mgfseed /\ live h res /\ disjoint res mgfseed)
  (ensures  fun h0 _ h1 -> modifies (loc res) h0 h1 /\
    as_seq h1 res == S.mgf_hash a (v len) (as_seq h0 mgfseed) (v maskLen))

#push-options "--z3rlimit 100"
val mgf_hash: a:Hash.hash_alg{S.hash_is_supported a} -> mgf_hash_st a
[@CInline]
val mgf_hash: a:Hash.hash_alg{S.hash_is_supported a} -> mgf_hash_st a
a: Spec.Hash.Definitions.hash_alg{Spec.RSAPSS.hash_is_supported a}
  -> Hacl.Impl.RSAPSS.MGF.mgf_hash_st a