JAR: Join-Accumulate Refine

10.3. Cap Table🔗

Each VM has a 256-slot cap table (u8 index), forming a CNode. Slot layout:

  • [0]: IPC slot — CALL on [0] = REPLY; caps passed via CALL arrive here

  • [1..28]: Protocol caps (GAS=1, FETCH=2, ..., QUOTA=28; gaps at 10-14 reserved)

  • [29..63]: Program caps (within CREATE bitmask range, u64 covers slots 0-63)

  • [64..253]: Program caps

  • [254]: UNTYPED (fixed slot, omitted when memory_pages == 0)

  • [255]: free

Child VMs receive caps from the parent: slots 0-63 via CREATE bitmask (from the CODE cap's CNode, copyable types only), slots 64-254 via MOVE after creation.

The per-CNode original bitmap (256 bits) tracks which protocol cap slots are unmodified. The compiler uses this for fast-path inlining of protocol calls.

🔗def
Jar.JAVM.Cap.ipcSlot : Nat
Jar.JAVM.Cap.ipcSlot : Nat

IPC slot index. CALL on slot 0 = REPLY.

🔗structure
Jar.JAVM.Cap.CapTable : Type
Jar.JAVM.Cap.CapTable : Type

Cap table: 256 slots indexed by u8. Each VM's cap table is a CNode.

The original bitmap tracks which protocol cap slots are unmodified (for compiler fast-path inlining of ecalli on protocol caps).

Constructor

Jar.JAVM.Cap.CapTable.mk

Fields

slots : Array (Option Jar.JAVM.Cap.Cap)
originalBitmap : Array Bool

Per-slot original bitmap (256 bits). True = slot holds original kernel-populated protocol cap. Set to false on DROP, MOVE-in, or MOVE-out.

🔗def
Jar.JAVM.Cap.CapTable.empty : Jar.JAVM.Cap.CapTable
Jar.JAVM.Cap.CapTable.empty :
  Jar.JAVM.Cap.CapTable
🔗def
Jar.JAVM.Cap.CapTable.get (t : Jar.JAVM.Cap.CapTable) (idx : Nat) :
  Option Jar.JAVM.Cap.Cap
Jar.JAVM.Cap.CapTable.get
  (t : Jar.JAVM.Cap.CapTable)
  (idx : Nat) : Option Jar.JAVM.Cap.Cap
🔗def
Jar.JAVM.Cap.CapTable.set (t : Jar.JAVM.Cap.CapTable) (idx : Nat)
  (c : Jar.JAVM.Cap.Cap) : Jar.JAVM.Cap.CapTable
Jar.JAVM.Cap.CapTable.set
  (t : Jar.JAVM.Cap.CapTable) (idx : Nat)
  (c : Jar.JAVM.Cap.Cap) :
  Jar.JAVM.Cap.CapTable
🔗def
Jar.JAVM.Cap.CapTable.take (t : Jar.JAVM.Cap.CapTable) (idx : Nat) :
  Jar.JAVM.Cap.CapTable × Option Jar.JAVM.Cap.Cap
Jar.JAVM.Cap.CapTable.take
  (t : Jar.JAVM.Cap.CapTable)
  (idx : Nat) :
  Jar.JAVM.Cap.CapTable ×
    Option Jar.JAVM.Cap.Cap
🔗def
Jar.JAVM.Cap.CapTable.isEmpty (t : Jar.JAVM.Cap.CapTable) (idx : Nat) :
  Bool
Jar.JAVM.Cap.CapTable.isEmpty
  (t : Jar.JAVM.Cap.CapTable)
  (idx : Nat) : Bool
🔗def
Jar.JAVM.Cap.CapTable.setOriginal (t : Jar.JAVM.Cap.CapTable)
  (idx : Nat) (c : Jar.JAVM.Cap.Cap) : Jar.JAVM.Cap.CapTable
Jar.JAVM.Cap.CapTable.setOriginal
  (t : Jar.JAVM.Cap.CapTable) (idx : Nat)
  (c : Jar.JAVM.Cap.Cap) :
  Jar.JAVM.Cap.CapTable

Set a cap and mark it as original (for kernel init of protocol caps).

🔗def
Jar.JAVM.Cap.maxIndirectionDepth : Nat
Jar.JAVM.Cap.maxIndirectionDepth : Nat

Maximum indirection depth (3 levels).