val legacy_alloca: alloca_st (|SHA1, ()|)
let legacy_alloca () =
  B.alloca_of_list Spec.init_as_list
val legacy_alloca: alloca_st (|SHA1, ()|)
let legacy_alloca () =
B.alloca_of_list Spec.init_as_list
Hacl.Hash.Core.SHA1.fst.checked
Spec.SHA1.fst.checked Spec.SHA1.fst.checked Spec.Hash.Definitions.fst.checked Spec.Agile.Hash.fst.checked prims.fst.checked LowStar.ImmutableBuffer.fst.checked LowStar.Buffer.fst.checked Lib.IntTypes.fsti.checked Lib.ByteSequence.fsti.checked Lib.ByteBuffer.fsti.checked Hacl.Hash.PadFinish.fsti.checked Hacl.Hash.Definitions.fst.checked FStar.UInt32.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.List.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked FStar.Ghost.fsti.checked FStar.Classical.fsti.checked C.Loops.fst.checked
Hacl.Hash.Core.SHA1.fst
Prims.unit LowStar.Buffer.alloca_of_list Lib.IntTypes.int_t Lib.IntTypes.U32 Lib.IntTypes.SEC Spec.SHA1.init_as_list LowStar.Monotonic.Buffer.mbuffer LowStar.Buffer.trivial_preorder Prims.l_and Prims.eq2 Prims.nat LowStar.Monotonic.Buffer.length FStar.Pervasives.normalize_term FStar.List.Tot.Base.length Prims.b2t Prims.op_Negation LowStar.Monotonic.Buffer.g_is_null Hacl.Hash.Definitions.state Prims.Mkdtuple2 Spec.Hash.Definitions.hash_alg Hacl.Hash.Definitions.m_spec Spec.Hash.Definitions.SHA1
module Hacl.Hash.Core.SHA1

open Lib.IntTypes
module B = LowStar.Buffer
module IB = LowStar.ImmutableBuffer
module HS = FStar.HyperStack
module HST = FStar.HyperStack.ST
module Spec = Spec.SHA1
module U32 = FStar.UInt32

open Hacl.Hash.Definitions
open Spec.Hash.Definitions

friend Spec.SHA1
friend Spec.Agile.Hash

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

(** Top-level constant arrays for the MD5 algorithm. *)
let _h0 = IB.igcmalloc_of_list HS.root Spec.init_as_list

noextract inline_for_extraction
val legacy_alloca: alloca_st (|SHA1, ()|)
Hacl.Hash.Definitions.alloca_st (| Spec.Hash.Definitions.SHA1, () |)