val heap_ignore_ghost_machine (h: heap_impl) : heap_impl
let heap_ignore_ghost_machine (h:heap_impl) : heap_impl =
  coerce (heap_ignore_ghost (coerce h))
val heap_ignore_ghost_machine (h: heap_impl) : heap_impl
let heap_ignore_ghost_machine (h: heap_impl) : heap_impl =
coerce (heap_ignore_ghost (coerce h))
Vale.Arch.HeapLemmas.fsti.checked
Vale.Arch.MachineHeap_s.fst.checked Vale.Arch.HeapTypes_s.fst.checked Vale.Arch.HeapImpl.fsti.checked Vale.Arch.Heap.fsti.checked prims.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked
Vale.Arch.HeapLemmas.fsti
Vale.Arch.Heap.heap_impl Vale.Arch.HeapLemmas.coerce Vale.Arch.HeapImpl.vale_full_heap Vale.Arch.HeapLemmas.heap_ignore_ghost
module Vale.Arch.HeapLemmas
open FStar.Mul
open Vale.Arch.HeapTypes_s
open Vale.Arch.MachineHeap_s
open Vale.Arch.Heap
open Vale.Arch.HeapImpl

val lemma_heap_impl : squash (heap_impl == vale_full_heap)

val empty_vale_heap_layout_inner (h:vale_heap) : vale_heap_layout_inner
val empty_vale_heaplets (h:vale_heap) : vale_heaplets

let heap_ignore_ghost (vfh:vale_full_heap) : vale_full_heap =
  {vfh with
    vf_layout = {vfh.vf_layout with vl_inner = empty_vale_heap_layout_inner vfh.vf_heap};
    vf_heaplets = empty_vale_heaplets vfh.vf_heap;
  }

unfold let coerce (#b #a:Type) (x:a{a == b}) : b = x
val heap_ignore_ghost_machine (h: heap_impl) : heap_impl
h: Vale.Arch.Heap.heap_impl -> Vale.Arch.Heap.heap_impl