val same_domain (h:vale_heap) (m:S.machine_heap) : prop0
let same_domain h m = Set.equal (IB.addrs_set (_ih h)) (Map.domain m)
val same_domain (h:vale_heap) (m:S.machine_heap) : prop0
let same_domain h m =
Set.equal (IB.addrs_set (_ih h)) (Map.domain m)
Vale.X64.Memory_Sems.fst.checked
Vale.X64.Memory.fst.checked Vale.X64.Memory.fst.checked Vale.X64.Machine_Semantics_s.fst.checked Vale.X64.Machine_s.fst.checked Vale.X64.BufferViewStore.fsti.checked Vale.Lib.BufferViewHelpers.fst.checked Vale.Interop.Views.fsti.checked Vale.Interop.Heap_s.fst.checked Vale.Interop.Base.fst.checked Vale.Interop.fsti.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 Vale.Arch.MachineHeap.fsti.checked Vale.Arch.HeapImpl.fsti.checked Vale.Arch.Heap.fsti.checked prims.fst.checked LowStar.Monotonic.Buffer.fsti.checked LowStar.BufferView.Up.fsti.checked LowStar.BufferView.Down.fsti.checked FStar.UInt8.fsti.checked FStar.UInt64.fsti.checked FStar.Set.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Option.fst.checked FStar.Mul.fst.checked FStar.Map.fsti.checked FStar.List.fst.checked FStar.Classical.fsti.checked
Vale.X64.Memory_Sems.fst
Vale.Arch.HeapImpl.vale_heap Vale.Arch.MachineHeap_s.machine_heap FStar.Set.equal Prims.int Vale.Interop.Heap_s.addrs_set Vale.Arch.HeapImpl._ih FStar.Map.domain Vale.Def.Types_s.nat8 Vale.Def.Prop_s.prop0
module Vale.X64.Memory_Sems

open FStar.Mul
open Vale.Def.Prop_s
open Vale.Def.Opaque_s
open Vale.X64.Machine_s
open Vale.X64.Memory
open Vale.Def.Words_s
module I = Vale.Interop
module S = Vale.X64.Machine_Semantics_s
module MB = LowStar.Monotonic.Buffer
module UV = LowStar.BufferView.Up
module DV = LowStar.BufferView.Down
open Vale.Lib.BufferViewHelpers
open Vale.Arch.HeapImpl
open Vale.Arch.Heap

friend Vale.X64.Memory
module IB = Vale.Interop.Base
val same_domain (h:vale_heap) (m:S.machine_heap) : prop0
h: Vale.Arch.HeapImpl.vale_heap -> m: Vale.Arch.MachineHeap_s.machine_heap -> Vale.Def.Prop_s.prop0