let heaplet_id = n:nat{n < 16}
let heaplet_id =
n: nat{n < 16}
Vale.Arch.HeapImpl.fsti.checked
Vale.Lib.Map16.fsti.checked Vale.Arch.HeapTypes_s.fst.checked prims.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked
Vale.Arch.HeapImpl.fsti
Prims.nat Prims.b2t Prims.op_LessThan
module Vale.Arch.HeapImpl
open FStar.Mul
open Vale.Arch.HeapTypes_s
module Map16 = Vale.Lib.Map16

(**
Define abstract (or mostly abstract) types for use by Vale.X64.Decls.fsti.

Note: the untrusted memory definitions are split among 3 modules:
- Vale.Arch.HeapImpl
- Vale.Arch.Heap
- Vale.X64.Memory
This splitting is done to avoid circular module dependencies.
*)
val heaplet_id : Type0
Type0