let _h0 = IB.igcmalloc_of_list HS.root Spec.init_as_list
let _h0 =
IB.igcmalloc_of_list HS.root Spec.init_as_list
Hacl.Hash.Core.MD5.fst.checked
Spec.MD5.fst.checked Spec.MD5.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.fst.checked Hacl.Hash.Definitions.fst.checked FStar.UInt32.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked FStar.Ghost.fsti.checked C.Loops.fst.checked
Hacl.Hash.Core.MD5.fst
LowStar.ImmutableBuffer.igcmalloc_of_list Lib.IntTypes.int_t Lib.IntTypes.U32 Lib.IntTypes.SEC FStar.Monotonic.HyperHeap.root Spec.MD5.init_as_list LowStar.ImmutableBuffer.libuffer FStar.Pervasives.normalize_term Prims.nat FStar.List.Tot.Base.length FStar.Seq.Properties.seq_of_list Prims.l_and Prims.eq2 FStar.Monotonic.HyperHeap.rid LowStar.Monotonic.Buffer.frameOf LowStar.ImmutableBuffer.immutable_preorder LowStar.Monotonic.Buffer.recallable
module Hacl.Hash.Core.MD5

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

module U32 = FStar.UInt32

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

friend Spec.MD5
friend Hacl.Hash.PadFinish
friend Spec.Agile.Hash
val _h0 : b:
LowStar.ImmutableBuffer.libuffer (Lib.IntTypes.int_t Lib.IntTypes.U32 Lib.IntTypes.SEC)
  (FStar.Pervasives.normalize_term (FStar.List.Tot.Base.length Spec.MD5.init_as_list))
  (FStar.Seq.Properties.seq_of_list Spec.MD5.init_as_list)
  { LowStar.Monotonic.Buffer.frameOf b == FStar.Monotonic.HyperHeap.root /\
    LowStar.Monotonic.Buffer.recallable b }
b:
LowStar.ImmutableBuffer.libuffer (Lib.IntTypes.int_t Lib.IntTypes.U32 Lib.IntTypes.SEC)
  (FStar.Pervasives.normalize_term (FStar.List.Tot.Base.length Spec.MD5.init_as_list))
  (FStar.Seq.Properties.seq_of_list Spec.MD5.init_as_list)
  { LowStar.Monotonic.Buffer.frameOf b == FStar.Monotonic.HyperHeap.root /\
    LowStar.Monotonic.Buffer.recallable b }