let hacl_sha1 = hacl_md SHA1
let hacl_sha1 =
hacl_md SHA1
Hacl.Streaming.SHA1.fst.checked
Spec.Hash.Definitions.fst.checked prims.fst.checked Hacl.Streaming.MD.fst.checked Hacl.Streaming.Interface.fsti.checked Hacl.Streaming.Functor.fsti.checked Hacl.Hash.SHA1.fsti.checked Hacl.Hash.Definitions.fst.checked FStar.Pervasives.fsti.checked FStar.HyperStack.ST.fsti.checked FStar.Ghost.fsti.checked
Hacl.Streaming.SHA1.fst
Hacl.Streaming.MD.hacl_md Spec.Hash.Definitions.SHA1
module Hacl.Streaming.SHA1

/// WARNING: this file is here for legacy purposes only. You SHOULD NOT use
/// it in new code.

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 SHA1
///
/// Some remarks:
///
/// - we don't bother with using the abstraction feature since we verified
///   clients like miTLS go through EverCrypt.Hash.Incremental
val hacl_sha1 : Hacl.Streaming.Interface.block Prims.unit
Hacl.Streaming.Interface.block Prims.unit