let machine_heap = Map.t int nat8
let machine_heap =
Map.t int nat8
Vale.Arch.MachineHeap_s.fst.checked
Vale.Def.Words_s.fsti.checked Vale.Def.Words.Two_s.fsti.checked Vale.Def.Words.Four_s.fsti.checked Vale.Def.Types_s.fst.checked Vale.Def.Prop_s.fst.checked Vale.Def.Opaque_s.fsti.checked prims.fst.checked FStar.Set.fsti.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Map.fsti.checked
Vale.Arch.MachineHeap_s.fst
FStar.Map.t Prims.int Vale.Def.Types_s.nat8
module Vale.Arch.MachineHeap_s

open FStar.Mul
open Vale.Def.Prop_s
open Vale.Def.Opaque_s
open Vale.Def.Words_s
open Vale.Def.Words.Two_s
open Vale.Def.Words.Four_s
open Vale.Def.Types_s

unfold let (.[]) = Map.sel
unfold let (.[]<-) = Map.upd
val machine_heap : Type0
Type0