val heap_ignore_ghost (vfh: vale_full_heap) : vale_full_heap
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;
  }
val heap_ignore_ghost (vfh: vale_full_heap) : vale_full_heap
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
}
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.HeapImpl.vale_full_heap Vale.Arch.HeapImpl.Mkvale_full_heap Vale.Arch.HeapImpl.Mkvale_heap_layout Vale.Arch.HeapLemmas.empty_vale_heap_layout_inner Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heap Vale.Arch.HeapImpl.__proj__Mkvale_heap_layout__item__vl_taint Vale.Arch.HeapImpl.vale_heap_layout Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_layout Vale.Arch.HeapLemmas.empty_vale_heaplets
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
val heap_ignore_ghost (vfh: vale_full_heap) : vale_full_heap
vfh: Vale.Arch.HeapImpl.vale_full_heap -> Vale.Arch.HeapImpl.vale_full_heap