val heaplet_upd_f (vfh: vale_full_heap) (mh': machine_heap) (k: heaplet_id) : vale_heap
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 heaplet_upd_f (vfh: vale_full_heap) (mh': machine_heap) (k: heaplet_id) : vale_heap
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'
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.HeapImpl.vale_full_heap Vale.Arch.MachineHeap_s.machine_heap Vale.Arch.HeapImpl.heaplet_id Vale.Arch.HeapImpl.mi_heap_upd FStar.Map.t Prims.int Vale.Def.Words_s.nat8 FStar.Map.concat Vale.Def.Types_s.nat8 FStar.Map.restrict FStar.Set.set FStar.Set.intersect Vale.Arch.HeapImpl.__proj__Mkvale_heap_layout_inner__item__vl_heaplet_sets Vale.Arch.HeapImpl.__proj__Mkvale_heap_layout__item__vl_inner Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_layout FStar.Map.domain Vale.Arch.HeapImpl.__proj__ValeHeap__item__mh Vale.Arch.HeapImpl.vale_heap Vale.Lib.Map16.sel Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets
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
val heaplet_upd_f (vfh: vale_full_heap) (mh': machine_heap) (k: heaplet_id) : vale_heap

    vfh: Vale.Arch.HeapImpl.vale_full_heap ->
    mh': Vale.Arch.MachineHeap_s.machine_heap ->
    k: Vale.Arch.HeapImpl.heaplet_id
  -> Vale.Arch.HeapImpl.vale_heap