let quad32 = Vale.Def.Types_s.quad32
let quad32 =
Vale.Def.Types_s.quad32
Vale.X64.Memory.fsti.checked
Vale.X64.Machine_s.fst.checked Vale.Lib.Map16.fsti.checked Vale.Def.Words_s.fsti.checked Vale.Def.Types_s.fst.checked Vale.Def.Prop_s.fst.checked Vale.Arch.HeapTypes_s.fst.checked Vale.Arch.HeapImpl.fsti.checked prims.fst.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Map.fsti.checked FStar.BigOps.fsti.checked
Vale.X64.Memory.fsti
Vale.Def.Types_s.quad32
module Vale.X64.Memory
include Vale.Arch.HeapTypes_s
open FStar.Mul
open Vale.Def.Prop_s
open Vale.X64.Machine_s
open Vale.Arch.HeapImpl
module Map16 = Vale.Lib.Map16

unfold let vale_heap = vale_heap
unfold let vale_full_heap = vale_full_heap
unfold let heaplet_id = heaplet_id

[@va_qattr]
let get_vale_heap (vhi:vale_full_heap) : vale_heap = vhi.vf_heap

[@va_qattr]
let set_vale_heap (vfh:vale_full_heap) (vh:vale_heap) : vale_full_heap =
  {vfh with vf_heap = vh}

let vale_full_heap_equal (h1 h2:vale_full_heap) =
  h1.vf_layout == h2.vf_layout /\
  h1.vf_heap == h2.vf_heap /\
  Map16.equal h1.vf_heaplets h2.vf_heaplets

val get_heaplet_id (h:vale_heap) : option heaplet_id

unfold let nat8 = Vale.Def.Words_s.nat8
unfold let nat16 = Vale.Def.Words_s.nat16
unfold let nat32 = Vale.Def.Words_s.nat32
val quad32 : Prims.eqtype
Prims.eqtype