let tuint32 = UInt32.t
let tuint32 =
UInt32.t
Vale.PPC64LE.Memory.fst.checked
Vale.X64.Machine_s.fst.checked Vale.Lib.Seqs_s.fst.checked Vale.Lib.BufferViewHelpers.fst.checked Vale.Interop.Views.fsti.checked Vale.Interop.Types.fst.checked Vale.Interop.Base.fst.checked Vale.Interop.fsti.checked Vale.Def.Words_s.fsti.checked Vale.Def.Words.Seq_s.fsti.checked Vale.Def.Words.Four_s.fsti.checked Vale.Def.Types_s.fst.checked Vale.Def.Opaque_s.fsti.checked Vale.Arch.MachineHeap_s.fst.checked Vale.Arch.HeapImpl.fsti.checked Vale.Arch.Heap.fst.checked prims.fst.checked LowStar.Monotonic.Buffer.fsti.checked LowStar.ModifiesPat.fst.checked LowStar.Modifies.fst.checked LowStar.BufferView.Up.fsti.checked LowStar.BufferView.Down.fsti.checked FStar.UInt8.fsti.checked FStar.UInt64.fsti.checked FStar.UInt32.fsti.checked FStar.UInt16.fsti.checked FStar.Set.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Math.Lib.fst.checked FStar.Map.fsti.checked FStar.List.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked FStar.Heap.fst.checked FStar.Ghost.fsti.checked FStar.Classical.fsti.checked
Vale.PPC64LE.Memory.fst
FStar.UInt32.t
module Vale.PPC64LE.Memory
include Vale.Interop.Types
friend Vale.Arch.Heap
open Vale.Def.Opaque_s
open Vale.Arch.HeapImpl
open Vale.Arch.Heap
open Vale.Interop.Base
module IB = Vale.Interop.Base
module I = Vale.Interop
module HS = FStar.HyperStack
module HST = FStar.HyperStack.ST
module MB = LowStar.Monotonic.Buffer
module M = LowStar.Modifies
open LowStar.ModifiesPat
module UV = LowStar.BufferView.Up
module DV = LowStar.BufferView.Down
open Vale.Lib.BufferViewHelpers
module H = FStar.Heap
module S = Vale.Arch.MachineHeap_s

#reset-options "--initial_fuel 2 --max_fuel 2 --initial_ifuel 1 --max_ifuel 1"

let b8 = IB.b8

unfold let (.[]) = Map.sel
unfold let (.[]<-) = Map.upd

let get_heaplet_id h =
  h.heapletId

let tuint8 = UInt8.t
val tuint32 : Prims.eqtype
Prims.eqtype