val h0 (i: U32.t{U32.v i < 5})
    : HST.Stack uint32
      (requires (fun _ -> True))
      (ensures (fun h res h' -> B.modifies B.loc_none h h' /\ res == Seq.index Spec.init (U32.v i)))
val h0 (i: U32.t{U32.v i < 5})
    : HST.Stack uint32
      (requires (fun _ -> True))
      (ensures (fun h res h' -> B.modifies B.loc_none h h' /\ res == Seq.index Spec.init (U32.v i)))
let h0 (i: U32.t { U32.v i < 5 } ) : HST.Stack uint32
  (requires (fun _ -> True))
  (ensures (fun h res h' ->
    B.modifies B.loc_none h h' /\
    res == Seq.index Spec.init (U32.v i)
  ))
= IB.recall_contents _h0 Spec.init;
  B.index _h0 i
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
let alloca () =
  B.alloca_of_list Spec.init_as_list

(* We read values from constant buffers through accessors to isolate
   all recall/liveness issues away. Thus, clients will not need to
   know that their output buffers be disjoint from our constant
   immutable buffers. *)
/
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
i: FStar.UInt32.t{FStar.UInt32.v i < 5} -> FStar.HyperStack.ST.Stack Lib.IntTypes.uint32
FStar.UInt32.t Prims.b2t Prims.op_LessThan FStar.UInt32.v LowStar.Monotonic.Buffer.index Lib.IntTypes.int_t Lib.IntTypes.U32 Lib.IntTypes.SEC LowStar.ImmutableBuffer.immutable_preorder Hacl.Hash.Core.SHA1._h0 Prims.unit LowStar.ImmutableBuffer.recall_contents Spec.SHA1.init Lib.IntTypes.uint32 FStar.Monotonic.HyperStack.mem Prims.l_True Prims.l_and LowStar.Monotonic.Buffer.modifies LowStar.Monotonic.Buffer.loc_none Prims.eq2 Lib.IntTypes.sec_int_t FStar.Seq.Base.index Spec.Hash.Definitions.word Spec.Hash.Definitions.SHA1
let h0 (i: U32.t{U32.v i < 5})
    : HST.Stack uint32
      (requires (fun _ -> True))
      (ensures (fun h res h' -> B.modifies B.loc_none h h' /\ res == Seq.index Spec.init (U32.v i))) =
  
IB.recall_contents _h0 Spec.init;
B.index _h0 i