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
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
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 Lib.IntTypes.op_Plus_Bang FStar.UInt32.__uint_to_t Hacl.Impl.RSAPSS.MGF.hash_len Hacl.Impl.RSAPSS.MGF.hash Prims.unit Lib.Buffer.update_sub_f FStar.Monotonic.HyperStack.mem Lib.ByteSequence.nat_to_intseq_be Lib.IntTypes.U8 Lib.IntTypes.SEC Lib.Sequence.lseq Hacl.Impl.RSAPSS.MGF.counter_to_bytes Lib.Buffer.lbuffer_t Lib.Buffer.MUT Lib.IntTypes.int_t FStar.UInt32.uint_to_t FStar.UInt32.t Lib.Buffer.sub FStar.HyperStack.ST.get
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))
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))

    a: Spec.Hash.Definitions.hash_alg{Spec.RSAPSS.hash_is_supported a} ->
    len:
      Lib.IntTypes.size_t
        { Lib.IntTypes.v len + 4 <= Lib.IntTypes.max_size_t /\
          Hacl.Impl.RSAPSS.MGF.less_than_max_input_length (Lib.IntTypes.v len + 4) a } ->
    i: Lib.IntTypes.size_t ->
    mgfseed_counter: Lib.Buffer.lbuffer Lib.IntTypes.uint8 (len +! 4ul) ->
    block: Lib.Buffer.lbuffer Lib.IntTypes.uint8 (Hacl.Impl.RSAPSS.MGF.hash_len a)
  -> FStar.HyperStack.ST.Stack Prims.unit