val hash_512: Hacl.Hash.Definitions.hash_st SHA2_512
let hash_512 input input_len dst =
  [@inline_let]
  let dst: lbuffer uint8 (Hacl.Hash.Definitions.hash_len SHA2_512) = dst in
  let ib = ntup1 input in
  let rb = ntup1 dst in
  let h0 = ST.get() in
  loc_multi1 rb;
  hash #SHA2_512 #M32 sha512_init sha512_update_nblocks sha512_update_last sha512_finish rb input_len ib;
  let h1 = ST.get() in
  Hacl.Spec.SHA2.Equiv.hash_agile_lemma #SHA2_512 #M32 (v input_len) (as_seq_multi h0 ib);
  assert ((as_seq_multi h1 rb).(|0|) == as_seq h1 dst)
val hash_512: Hacl.Hash.Definitions.hash_st SHA2_512
let hash_512 input input_len dst =
[@@ inline_let ]let dst:lbuffer uint8 (Hacl.Hash.Definitions.hash_len SHA2_512) = dst in
let ib = ntup1 input in
let rb = ntup1 dst in
let h0 = ST.get () in
loc_multi1 rb;
hash #SHA2_512
  #M32
  sha512_init
  sha512_update_nblocks
  sha512_update_last
  sha512_finish
  rb
  input_len
  ib;
let h1 = ST.get () in
Hacl.Spec.SHA2.Equiv.hash_agile_lemma #SHA2_512 #M32 (v input_len) (as_seq_multi h0 ib);
assert ((as_seq_multi h1 rb).(| 0 |) == as_seq h1 dst)
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
LowStar.Buffer.buffer Lib.IntTypes.uint8 Lib.IntTypes.size_t Prims.b2t Prims.op_Equality Prims.int Prims.l_or Prims.op_GreaterThanOrEqual Lib.IntTypes.range Lib.IntTypes.U32 LowStar.Monotonic.Buffer.length LowStar.Buffer.trivial_preorder Lib.IntTypes.v Lib.IntTypes.PUB Hacl.Hash.Definitions.hash_t Spec.Hash.Definitions.SHA2_512 Prims._assert Prims.eq2 FStar.Seq.Base.seq Prims.nat FStar.Seq.Base.length Hacl.Hash.Definitions.hash_len Lib.IntTypes.int_t Lib.IntTypes.U8 Lib.IntTypes.SEC Lib.MultiBuffer.op_Lens_Access FStar.Seq.Properties.lseq Hacl.Spec.SHA2.Vec.lanes Hacl.Spec.SHA2.Vec.M32 Lib.MultiBuffer.as_seq_multi Lib.Buffer.as_seq Lib.Buffer.MUT Prims.unit Hacl.Spec.SHA2.Equiv.hash_agile_lemma FStar.Monotonic.HyperStack.mem FStar.HyperStack.ST.get Hacl.Impl.SHA2.Generic.hash Hacl.SHA2.Scalar32.sha512_init Hacl.SHA2.Scalar32.sha512_update_nblocks Hacl.SHA2.Scalar32.sha512_update_last Hacl.SHA2.Scalar32.sha512_finish Lib.MultiBuffer.loc_multi1 Lib.NTuple.ntuple Lib.Buffer.lbuffer_t Lib.NTuple.ntup1 Lib.Buffer.lbuffer
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
the hash via `update_224`."]
let finish_224 = F.mk_finish hacl_sha2_224 () (state_t_224.s ()) (G.erased unit)
let free_224: F.free_st hacl_sha2_256 (G.hide ()) (state_t_256.s ()) (G.erased unit) = fun p -> free_256 p

[@@ Comment
"Hash `input`, of len `input_len`, into `dst`, an array of 28 bytes."]
val hash_224: Hacl.Hash.Definitions.hash_st SHA2_224
let hash_224 input input_len dst =
  [@inline_let]
  let dst: lbuffer uint8 (Hacl.Hash.Definitions.hash_len SHA2_224) = dst in
  let ib = ntup1 input in
  let rb = ntup1 dst in
  let h0 = ST.get() in
  loc_multi1 rb;
  hash #SHA2_224 #M32 sha224_init sha224_update_nblocks sha224_update_last sha224_finish rb input_len ib;
  let h1 = ST.get() in
  Hacl.Spec.SHA2.Equiv.hash_agile_lemma #SHA2_224 #M32 (v input_len) (as_seq_multi h0 ib);
  assert ((as_seq_multi h1 rb).(|0|) == as_seq h1 dst)

// SHA2-512
// --------

inline_for_extraction noextract
let alloca_512 = F.alloca hacl_sha2_512 () (state_t_512.s ()) (G.erased unit)
let create_in_512 = F.create_in hacl_sha2_512 () (state_t_512.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_512`. 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_512 = F.copy hacl_sha2_512 () (state_t_512.s ()) (G.erased unit)

let init_512 = F.init hacl_sha2_512 (G.hide ()) (state_t_512.s ()) (G.erased unit)

[@@ CInline ]
private
let update_384_512 = F.update hacl_sha2_512 (G.hide ()) (state_t_512.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_512`
(since the last call to `init_512`) exceeds 2^125-1 bytes.

This function is identical to the update function for SHA2_384.";
]
let update_512: F.update_st hacl_sha2_512 (G.hide ()) (state_t_512.s ()) (G.erased unit) = fun p input input_len -> update_384_512 p input input_len

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

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

This function is identical to the free function for SHA2_384.";
]
let free_512 = F.free hacl_sha2_512 (G.hide ()) (state_t_512.s ()) (G.erased unit)

[@@ Comment
"Hash `input`, of len `input_len`, into `dst`, an array of 64 bytes."]
val hash_512: Hacl.Hash.Definitions.hash_st SHA2_512
val hash_512: Hacl.Hash.Definitions.hash_st SHA2_512
Hacl.Hash.Definitions.hash_st Spec.Hash.Definitions.SHA2_512