val heap_upd (hi:heap_impl) (mh':machine_heap) (mt':memTaint_t) : Pure heap_impl
  (requires is_machine_heap_update (heap_get hi) mh')
  (ensures fun hi -> heap_get hi == mh' /\ heap_taint hi == mt')
let heap_upd hi mh' mt' =
  let h' = mi_heap_upd hi.vf_heap mh' in
  let hs' = Map16.init vale_heap (heaplet_upd_f hi mh') in
  {
    vf_layout = {hi.vf_layout with vl_taint = mt'};
    vf_heap = h';
    vf_heaplets = hs';
  }
val heap_upd (hi:heap_impl) (mh':machine_heap) (mt':memTaint_t) : Pure heap_impl
  (requires is_machine_heap_update (heap_get hi) mh')
  (ensures fun hi -> heap_get hi == mh' /\ heap_taint hi == mt')
let heap_upd hi mh' mt' =
let h' = mi_heap_upd hi.vf_heap mh' in
let hs' = Map16.init vale_heap (heaplet_upd_f hi mh') in
{ vf_layout = { hi.vf_layout with vl_taint = mt' }; vf_heap = h'; vf_heaplets = hs' }
Vale.Arch.Heap.fst.checked
Vale.Lib.Map16.fsti.checked Vale.Interop.fsti.checked Vale.Arch.HeapImpl.fst.checked Vale.Arch.HeapImpl.fst.checked prims.fst.checked FStar.Set.fsti.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Map.fsti.checked FStar.Ghost.fsti.checked
Vale.Arch.Heap.fst
Vale.Arch.Heap.heap_impl Vale.Arch.MachineHeap_s.machine_heap Vale.Arch.HeapTypes_s.memTaint_t Vale.Arch.HeapImpl.Mkvale_full_heap Vale.Arch.HeapImpl.Mkvale_heap_layout Vale.Arch.HeapImpl.__proj__Mkvale_heap_layout__item__vl_inner 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.Lib.Map16.init Vale.Arch.Heap.heaplet_upd_f Vale.Arch.HeapImpl.mi_heap_upd Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heap
module Vale.Arch.Heap
open FStar.Mul
open Vale.Interop
open Vale.Arch.HeapImpl
module Map16 = Vale.Lib.Map16
friend Vale.Arch.HeapImpl

let heap_impl = vale_full_heap

let heap_get hi = hi.vf_heap.mh

let heap_taint hi = hi.vf_layout.vl_taint

// Update heaplet k with mh', but only for the addresses that k owns (addresses not owned by k remain unmodified)
let heaplet_upd_f (vfh:vale_full_heap) (mh':machine_heap) (k:heaplet_id) : vale_heap =
  let hk = Map16.sel vfh.vf_heaplets k in
  let mhk = hk.mh in
  let dom_upd = Set.intersect (vfh.vf_layout.vl_inner.vl_heaplet_sets k) (Map.domain mhk) in
  let mhk' = Map.concat mhk (Map.restrict dom_upd mh') in
  mi_heap_upd hk mhk'
val heap_upd (hi:heap_impl) (mh':machine_heap) (mt':memTaint_t) : Pure heap_impl
  (requires is_machine_heap_update (heap_get hi) mh')
  (ensures fun hi -> heap_get hi == mh' /\ heap_taint hi == mt')

    hi: Vale.Arch.Heap.heap_impl ->
    mh': Vale.Arch.MachineHeap_s.machine_heap ->
    mt': Vale.Arch.HeapTypes_s.memTaint_t
  -> Prims.Pure Vale.Arch.Heap.heap_impl