let finish_224 = F.mk_finish hacl_sha2_224 () (state_t_224.s ()) (G.erased unit)
let finish_224 =
F.mk_finish hacl_sha2_224 () (state_t_224.s ()) (G.erased unit)
Hacl.Streaming.SHA2.fst.checked
Spec.Hash.Definitions.fst.checked prims.fst.checked Lib.NTuple.fsti.checked Lib.MultiBuffer.fst.checked Lib.IntTypes.fsti.checked Lib.Buffer.fsti.checked Hacl.Streaming.MD.fst.checked Hacl.Streaming.Interface.fsti.checked Hacl.Streaming.Functor.fsti.checked Hacl.Spec.SHA2.Vec.fst.checked Hacl.Spec.SHA2.Equiv.fst.checked Hacl.SHA2.Scalar32.fst.checked Hacl.Impl.SHA2.Generic.fst.checked Hacl.Hash.Definitions.fst.checked FStar.Pervasives.fsti.checked FStar.HyperStack.ST.fsti.checked FStar.Ghost.fsti.checked
Hacl.Streaming.SHA2.fst
Hacl.Streaming.Functor.mk_finish Prims.unit Hacl.Streaming.SHA2.hacl_sha2_224 Hacl.Streaming.Interface.__proj__Stateful__item__s Hacl.Streaming.SHA2.state_t_224 FStar.Ghost.erased
module Hacl.Streaming.SHA2

// NOTE: if you get errors trying to load this file in interactive mode because
// a tactic fails in Hacl.Streaming.MD (even though Hacl.Streaming.MD works
// totally fine in interactive mode!!), run:
//     NODEPEND=1 make -j obj/Hacl.Streaming.MD.fst.checked

open FStar.HyperStack.ST

/// A streaming version of MD-based hashes

#set-options "--max_fuel 0 --max_ifuel 0 --z3rlimit 100"

module G = FStar.Ghost
module F = Hacl.Streaming.Functor

open Spec.Hash.Definitions
open Hacl.Streaming.Interface
open Hacl.Streaming.MD

/// Instantiations of the streaming functor for specialized SHA2 algorithms.
///
/// Some remarks:
///
/// - we don't bother with using the abstraction feature since we verified
///   clients like miTLS go through EverCrypt.Hash.Incremental

inline_for_extraction noextract
let hacl_sha2_224 = hacl_md SHA2_224
inline_for_extraction noextract
let hacl_sha2_256 = hacl_md SHA2_256
inline_for_extraction noextract
let hacl_sha2_384 = hacl_md SHA2_384
inline_for_extraction noextract
let hacl_sha2_512 = hacl_md SHA2_512

inline_for_extraction noextract
let state_t_224 = state_t SHA2_224
inline_for_extraction noextract
let state_t_256 = state_t SHA2_256
inline_for_extraction noextract
let state_t_384 = state_t SHA2_384
inline_for_extraction noextract
let state_t_512 = state_t SHA2_512

/// Type abbreviations - for pretty code generation
let state_sha2_224 = Hacl.Streaming.MD.state_32
let state_sha2_256 = Hacl.Streaming.MD.state_32
let state_sha2_384 = Hacl.Streaming.MD.state_64
let state_sha2_512 = Hacl.Streaming.MD.state_64

open Lib.Buffer
open Lib.IntTypes
open Lib.NTuple
open Lib.MultiBuffer
open Hacl.Spec.SHA2.Vec
open Hacl.SHA2.Scalar32
open Hacl.Impl.SHA2.Generic
module ST = FStar.HyperStack.ST

// SHA2-256
// --------

inline_for_extraction noextract
let alloca_256 = F.alloca hacl_sha2_256 () (state_t_256.s ()) (G.erased unit)

[@@ Comment
"Allocate initial state for the SHA2_256 hash. The state is to be freed by
calling `free_256`."]
let create_in_256 = F.create_in hacl_sha2_256 () (state_t_256.s ()) (G.erased unit)

[@@ Comment
"Copies the state passed as argument into a newly allocated state (deep copy).
The state is to be freed by calling `free_256`. Cloning the state this way is
useful, for instance, if your control-flow diverges and you need to feed
more (different) data into the hash in each branch."]
let copy_256 = F.copy hacl_sha2_256 () (state_t_256.s ()) (G.erased unit)

[@@ Comment
"Reset an existing state to the initial hash state with empty data."]
let init_256 = F.init hacl_sha2_256 (G.hide ()) (state_t_256.s ()) (G.erased unit)

[@@ CInline ]
private
let update_224_256 = F.update hacl_sha2_256 (G.hide ()) (state_t_256.s ()) (G.erased unit)

[@@ Comment
"Feed an arbitrary amount of data into the hash. This function returns 0 for
success, or 1 if the combined length of all of the data passed to `update_256`
(since the last call to `init_256`) exceeds 2^61-1 bytes.

This function is identical to the update function for SHA2_224.";
]
let update_256: F.update_st hacl_sha2_256 (G.hide ()) (state_t_256.s ()) (G.erased unit) = fun p input input_len -> update_224_256 p input input_len

[@@ Comment
"Write the resulting hash into `dst`, an array of 32 bytes. The state remains
valid after a call to `finish_256`, meaning the user may feed more data into
the hash via `update_256`. (The finish_256 function operates on an internal copy of
the state and therefore does not invalidate the client-held state `p`.)"]
let finish_256 = F.mk_finish hacl_sha2_256 () (state_t_256.s ()) (G.erased unit)

[@@ Comment
"Free a state allocated with `create_in_256`.

This function is identical to the free function for SHA2_224."]
let free_256 = F.free hacl_sha2_256 (G.hide ()) (state_t_256.s ()) (G.erased unit)

[@@ Comment
"Hash `input`, of len `input_len`, into `dst`, an array of 32 bytes."]
val hash_256: Hacl.Hash.Definitions.hash_st SHA2_256
let hash_256 input input_len dst =
  [@inline_let]
  let dst: lbuffer uint8 (Hacl.Hash.Definitions.hash_len SHA2_256) = dst in
  let ib = ntup1 input in
  let rb = ntup1 dst in
  let h0 = ST.get() in
  loc_multi1 rb;
  hash #SHA2_256 #M32 sha256_init sha256_update_nblocks sha256_update_last sha256_finish rb input_len ib;
  let h1 = ST.get() in
  Hacl.Spec.SHA2.Equiv.hash_agile_lemma #SHA2_256 #M32 (v input_len) (as_seq_multi h0 ib);
  assert ((as_seq_multi h1 rb).(|0|) == as_seq h1 dst)

// SHA2-224
// --------

inline_for_extraction noextract
let alloca_224 = F.alloca hacl_sha2_224 () (state_t_224.s ()) (G.erased unit)
let create_in_224 = F.create_in hacl_sha2_224 () (state_t_224.s ()) (G.erased unit)
let init_224 = F.init hacl_sha2_224 (G.hide ()) (state_t_224.s ()) (G.erased unit)
// We assume verified clients will rely on Spec.SHA2.Lemmas to prove that update_224 has the same effect as update_256.
let update_224: F.update_st hacl_sha2_256 (G.hide ()) (state_t_256.s ()) (G.erased unit) = fun p input input_len -> update_224_256 p input input_len

[@@ Comment
"Write the resulting hash into `dst`, an array of 28 bytes. The state remains
valid after a call to `finish_224`, meaning the user may feed more data into
val finish_224 : Hacl.Streaming.Functor.finish_st Hacl.Streaming.SHA2.hacl_sha2_224
  ()
  (Stateful?.s Hacl.Streaming.SHA2.state_t_224 ())
  (FStar.Ghost.erased Prims.unit)
Hacl.Streaming.Functor.finish_st Hacl.Streaming.SHA2.hacl_sha2_224
  ()
  (Stateful?.s Hacl.Streaming.SHA2.state_t_224 ())
  (FStar.Ghost.erased Prims.unit)