val lemma_get_upd_heap (h:vale_heap) (m:S.machine_heap) : Lemma
  (requires is_machine_heap_update (get_heap h) m)
  (ensures get_heap (upd_heap h m) == m)
let lemma_get_upd_heap h m = I.up_down_identity (_ih h) m
val lemma_get_upd_heap (h:vale_heap) (m:S.machine_heap) : Lemma
  (requires is_machine_heap_update (get_heap h) m)
  (ensures get_heap (upd_heap h m) == m)
let lemma_get_upd_heap h m =
I.up_down_identity (_ih h) m
Vale.PPC64LE.Memory_Sems.fst.checked
Vale.X64.Machine_Semantics_s.fst.checked Vale.X64.BufferViewStore.fsti.checked Vale.PPC64LE.Semantics_s.fst.checked Vale.PPC64LE.Memory.fst.checked Vale.PPC64LE.Memory.fst.checked Vale.PPC64LE.Machine_s.fst.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.PPC64LE.Memory_Sems.fst
Vale.Arch.HeapImpl.vale_heap Vale.Arch.MachineHeap_s.machine_heap Vale.Interop.up_down_identity Vale.Arch.HeapImpl._ih Prims.unit
module Vale.PPC64LE.Memory_Sems

open FStar.Mul
open Vale.Def.Prop_s
open Vale.Def.Opaque_s
open Vale.PPC64LE.Machine_s
open Vale.PPC64LE.Memory
open Vale.Def.Words_s
module I = Vale.Interop
module S = Vale.PPC64LE.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.PPC64LE.Memory
module IB = Vale.Interop.Base

let same_domain h m = Set.equal (IB.addrs_set (_ih h)) (Map.domain m)

let lemma_same_domains h m1 m2 = ()

let get_heap h = I.down_mem (_ih h)

let upd_heap h m = mi_heap_upd h m

//let lemma_upd_get_heap h = I.down_up_identity (_ih h)
val lemma_get_upd_heap (h:vale_heap) (m:S.machine_heap) : Lemma
  (requires is_machine_heap_update (get_heap h) m)
  (ensures get_heap (upd_heap h m) == m)
h: Vale.Arch.HeapImpl.vale_heap -> m: Vale.Arch.MachineHeap_s.machine_heap
  -> FStar.Pervasives.Lemma
      (requires
        Vale.Arch.MachineHeap_s.is_machine_heap_update (Vale.PPC64LE.Memory_Sems.get_heap h) m)
      (ensures Vale.PPC64LE.Memory_Sems.get_heap (Vale.PPC64LE.Memory_Sems.upd_heap h m) == m)