let is_full_update (vfh:vale_full_heap) (h':vale_heap) (hid:heaplet_id) (mh':machine_heap) (mt':memtaint) =
  is_machine_heap_update (heap_get (coerce vfh)) mh' /\ (
    let vfh' = coerce (heap_upd (coerce vfh) mh' mt') in
    mem_inv vfh' /\
    vfh'.vf_layout == vfh.vf_layout /\
    vfh'.vf_heaplets == Map16.upd vfh.vf_heaplets hid h'
  )
let is_full_update
      (vfh: vale_full_heap)
      (h': vale_heap)
      (hid: heaplet_id)
      (mh': machine_heap)
      (mt': memtaint)
     =
is_machine_heap_update (heap_get (coerce vfh)) mh' /\
(let vfh' = coerce (heap_upd (coerce vfh) mh' mt') in
  mem_inv vfh' /\ vfh'.vf_layout == vfh.vf_layout /\
  vfh'.vf_heaplets == Map16.upd vfh.vf_heaplets hid h')
Vale.PPC64LE.Memory_Sems.fsti.checked
Vale.PPC64LE.Semantics_s.fst.checked Vale.PPC64LE.Memory.fsti.checked Vale.PPC64LE.Machine_s.fst.checked Vale.Lib.Seqs.fsti.checked Vale.Lib.Map16.fsti.checked Vale.Def.Types_s.fst.checked Vale.Def.Prop_s.fst.checked Vale.Arch.Types.fsti.checked Vale.Arch.MachineHeap_s.fst.checked Vale.Arch.HeapImpl.fsti.checked Vale.Arch.Heap.fsti.checked prims.fst.checked FStar.Set.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Map.fsti.checked
Vale.PPC64LE.Memory_Sems.fsti
Vale.PPC64LE.Memory.vale_full_heap Vale.PPC64LE.Memory.vale_heap Vale.PPC64LE.Memory.heaplet_id Vale.Arch.MachineHeap_s.machine_heap Vale.PPC64LE.Memory.memtaint Prims.l_and Vale.Arch.MachineHeap_s.is_machine_heap_update Vale.Arch.Heap.heap_get Vale.PPC64LE.Memory_Sems.coerce Vale.Arch.Heap.heap_impl Vale.PPC64LE.Memory.mem_inv Prims.eq2 Vale.Arch.HeapImpl.vale_heap_layout Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_layout Vale.Lib.Map16.map16 Vale.Arch.HeapImpl.vale_heap Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets Vale.Lib.Map16.upd Vale.Arch.HeapImpl.vale_full_heap Vale.Arch.Heap.heap_upd Prims.logical
module Vale.PPC64LE.Memory_Sems

open FStar.Mul
open Vale.Def.Prop_s
open Vale.Def.Types_s
open Vale.Arch.Types
open Vale.Arch.HeapImpl
open Vale.Arch.Heap
open Vale.Arch.MachineHeap_s
open Vale.PPC64LE.Machine_s
open Vale.PPC64LE.Memory
open Vale.Lib.Seqs
module S = Vale.PPC64LE.Semantics_s
module Map16 = Vale.Lib.Map16

val same_domain (h:vale_heap) (m:S.machine_heap) : prop0

val lemma_same_domains (h:vale_heap) (m1:S.machine_heap) (m2:S.machine_heap) : Lemma
  (requires same_domain h m1 /\ Set.equal (Map.domain m1) (Map.domain m2))
  (ensures same_domain h m2)

val get_heap (h:vale_heap) : GTot (m:S.machine_heap{same_domain h m})

val upd_heap (h:vale_heap) (m:S.machine_heap{is_machine_heap_update (get_heap h) m}) : GTot vale_heap

//val lemma_upd_get_heap (h:vale_heap) : Lemma (upd_heap h (get_heap h) == h)
//  [SMTPat (upd_heap h (get_heap 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)

unfold let coerce (#b #a:Type) (x:a{a == b}) : b = x

val lemma_heap_impl : squash (heap_impl == vale_full_heap)

val lemma_heap_get_heap (h:vale_full_heap) : Lemma
  (heap_get (coerce h) == get_heap (get_vale_heap h))
  [SMTPat (heap_get (coerce h))]

val lemma_heap_taint (h:vale_full_heap) : Lemma
  (heap_taint (coerce h) == full_heap_taint h)
  [SMTPat (heap_taint (coerce h))]

let is_full_read (#t:base_typ) (h1 h2:vale_heap) (b:buffer t) (i:int) =
  buffer_addr b h1 == buffer_addr b h2 /\
  buffer_read b i h1 == buffer_read b i h2 /\
  valid_buffer_read h1 b i  // needed to trigger "index = i" in valid_mem_operand64/valid_mem_operand128
val is_full_update : vfh: Vale.PPC64LE.Memory.vale_full_heap ->
    h': Vale.PPC64LE.Memory.vale_heap ->
    hid: Vale.PPC64LE.Memory.heaplet_id ->
    mh': Vale.Arch.MachineHeap_s.machine_heap ->
    mt': Vale.PPC64LE.Memory.memtaint
  -> Prims.logical

    vfh: Vale.PPC64LE.Memory.vale_full_heap ->
    h': Vale.PPC64LE.Memory.vale_heap ->
    hid: Vale.PPC64LE.Memory.heaplet_id ->
    mh': Vale.Arch.MachineHeap_s.machine_heap ->
    mt': Vale.PPC64LE.Memory.memtaint
  -> Prims.logical