11.4. Capability Indirection Resolution🔗

Cap slot references use a u32 HANDLE-chain encoding (up to 3 levels of indirection). Resolution walks the chain, validating each intermediate HANDLE's target VM is accessible (non-RUNNING, non-WAITING).

def

Jar.JAVM.Kernel.resolveCapRef (state : KernelState) (capRef : UInt32) :
  Option (Nat × Nat)
Jar.JAVM.Kernel.resolveCapRef
  (state : KernelState)
  (capRef : UInt32) : Option (Nat × Nat)

Resolve a u32 cap reference with HANDLE-chain indirection. byte 0 = target slot, bytes 1-3 = HANDLE chain (0x00 = end). Returns (vm_index, cap_slot) or none.

def

Jar.JAVM.Kernel.resolveOrWhat (state : KernelState) (capRef : UInt32) :
  KernelState × Option (Nat × Nat)
Jar.JAVM.Kernel.resolveOrWhat
  (state : KernelState)
  (capRef : UInt32) :
  KernelState × Option (Nat × Nat)

Resolve or set WHAT.