let hacl_sha2_256 = hacl_md SHA2_256
let hacl_sha2_256 =
hacl_md SHA2_256
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.MD.hacl_md Spec.Hash.Definitions.SHA2_256
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
val hacl_sha2_256 : Hacl.Streaming.Interface.block Prims.unit
Hacl.Streaming.Interface.block Prims.unit