JAR: Join-Accumulate Refine

11.7. Memory Management🔗

MAP and UNMAP control which pages of a DATA cap are present in a VM's address space. Only the owning CNode can map/unmap — no aliasing across VMs.

🔗def
Jar.JAVM.Kernel.handleMap (state : KernelState) (vmIdx slot : Nat) :
  KernelState × DispatchResult
Jar.JAVM.Kernel.handleMap
  (state : KernelState)
  (vmIdx slot : Nat) :
  KernelState × DispatchResult

MAP pages of a DATA cap in its CNode. φ[7]=base_offset, φ[8]=page_offset, φ[9]=page_count, φ[10]=access (0=RO, 1=RW). In the Lean model, copies backing store pages into flat PVM Memory.

🔗def
Jar.JAVM.Kernel.handleUnmap (state : KernelState) (vmIdx slot : Nat) :
  KernelState × DispatchResult
Jar.JAVM.Kernel.handleUnmap
  (state : KernelState)
  (vmIdx slot : Nat) :
  KernelState × DispatchResult

UNMAP pages of a DATA cap. φ[7]=page_offset, φ[8]=page_count. Zeroes pages in PVM memory, marks inaccessible.