let vec8 = L.lbuffer UInt8.t
let vec8 =
L.lbuffer UInt8.t
Test.NoHeap.fsti.checked
Test.Lowstarize.fst.checked Spec.Hash.Definitions.fst.checked prims.fst.checked LowStar.BufferOps.fst.checked LowStar.Buffer.fst.checked FStar.UInt8.fsti.checked FStar.UInt32.fsti.checked FStar.Pervasives.fsti.checked FStar.Int32.fsti.checked FStar.HyperStack.ST.fsti.checked EverCrypt.Hash.fsti.checked C.String.fsti.checked C.Loops.fst.checked
Test.NoHeap.fsti
Test.Lowstarize.lbuffer FStar.UInt8.t
module Test.NoHeap

module H = EverCrypt.Hash
module B = LowStar.Buffer
module L = Test.Lowstarize

open FStar.HyperStack.ST
val vec8 : Type0
Type0