10.1. Capability Types🔗

Six capability variants: five program types and one protocol type. Copyable types (UNTYPED, CODE, CALLABLE, Protocol) can be duplicated via COPY and propagated to child VMs via CREATE bitmask. Move-only types (DATA, HANDLE) require MOVE for cross-CNode transfer.

inductive type

Jar.JAVM.Cap.Cap : Type
Jar.JAVM.Cap.Cap : Type

A capability in the cap table.

Constructors

untyped (u : Jar.JAVM.Cap.UntypedCap) : Jar.JAVM.Cap.Cap

data (d : Jar.JAVM.Cap.DataCap) : Jar.JAVM.Cap.Cap

code (c : Jar.JAVM.Cap.CodeCap) : Jar.JAVM.Cap.Cap

handle (h : Jar.JAVM.Cap.HandleCap) : Jar.JAVM.Cap.Cap

callable (c : Jar.JAVM.Cap.CallableCap) : Jar.JAVM.Cap.Cap

protocol (p : Jar.JAVM.Cap.ProtocolCap) : Jar.JAVM.Cap.Cap

def

Jar.JAVM.Cap.Cap.isCopyable : Jar.JAVM.Cap.Cap → Bool
Jar.JAVM.Cap.Cap.isCopyable :
  Jar.JAVM.Cap.Cap → Bool

Whether a capability type supports COPY.

def

Jar.JAVM.Cap.Cap.tryCopy : Jar.JAVM.Cap.Cap → Option Jar.JAVM.Cap.Cap
Jar.JAVM.Cap.Cap.tryCopy :
  Jar.JAVM.Cap.Cap →
    Option Jar.JAVM.Cap.Cap

Create a copy of this cap (only for copyable types).

def

Jar.JAVM.Cap.CapRef : Type
Jar.JAVM.Cap.CapRef : Type

Indirection encoding: u32 byte-packed HANDLE chain.

byte 0: target cap slot (0-255)
byte 1: indirection level 0 (0x00 = end, 1-255 = HANDLE slot)
byte 2: indirection level 1 (0x00 = end, 1-255 = HANDLE slot)
byte 3: indirection level 2 (0x00 = end, 1-255 = HANDLE slot)

Slot 0 (IPC) cannot be used for indirection. (u8 as u32) = local slot.

inductive type

Jar.JAVM.Cap.Access : Type
Jar.JAVM.Cap.Access : Type

Memory access mode, set at MAP time.

Constructors

ro : Jar.JAVM.Cap.Access

rw : Jar.JAVM.Cap.Access

10.1.1. DATA: Physical Pages (Move-Only, Partial Mapping)🔗

DATA caps represent physical memory pages with exclusive mapping. Only one CNode can map a DATA cap at a time — no aliasing, no reference counting. Access mode (RO/RW) and base offset are set on first MAP and fixed thereafter. Individual pages within the cap can be mapped or unmapped independently via a per-page bitmap, enabling demand paging: a parent VM maps pages one at a time through HANDLE indirection.

MOVE to a different CNode auto-unmaps all pages. DROP auto-unmaps and leaks pages.

structure

Jar.JAVM.Cap.DataCap : Type
Jar.JAVM.Cap.DataCap : Type

DATA capability: physical pages with exclusive mapping and per-page bitmap.

Move-only. Each DATA cap has a single base_offset (set on first MAP) and a per-page mapped bitmap tracking which pages are present in the address space. Page P maps to address base_offset + P * 4096.

Constructor

Jar.JAVM.Cap.DataCap.mk

Fields

backingOffset : Nat

Offset into the backing memfd (in pages).

pageCount : Nat

Number of pages.

baseOffset : Option Nat

Base offset in address space (set on first MAP, fixed thereafter). None = unmapped.

access : Option Jar.JAVM.Cap.Access

Access mode (set on first MAP, fixed thereafter).

mappedBitmap : Array Bool

Per-page mapped bitmap. True = page present in address space.

10.1.2. UNTYPED: Bump Allocator🔗

UNTYPED is a bump allocator for physical page allocation. Copyable — multiple VMs can hold copies and allocate independently. CALL on UNTYPED = RETYPE: carves pages from the pool and returns an unmapped DATA cap at a caller-specified destination slot. Pages are never returned (leaky by design). Placed at fixed slot 254; omitted when memory\_pages == 0.

structure

Jar.JAVM.Cap.UntypedCap : Type
Jar.JAVM.Cap.UntypedCap : Type

UNTYPED capability: bump allocator. Copyable (shared offset).

Constructor

Jar.JAVM.Cap.UntypedCap.mk

Fields

offset : Nat

Current bump offset (in pages).

total : Nat

Total pages available.

10.1.3. CODE: Compiled PVM Code🔗

CODE caps hold compiled PVM bytecode (interpreter or recompiler backend). Harvard architecture — code is not in the data address space. Each CODE cap owns a 4GB virtual window shared by all VMs running that code. CALL on CODE = CREATE: produces a new VM with a HANDLE. The CREATE bitmask copies caps from the CODE cap's CNode (not the caller's), so cap replacements propagate automatically to children.

structure

Jar.JAVM.Cap.CodeCap : Type
Jar.JAVM.Cap.CodeCap : Type

CODE capability: compiled PVM code. Copyable.

Constructor

Jar.JAVM.Cap.CodeCap.mk

Fields

id : Nat

Unique identifier within invocation.

10.1.4. HANDLE and CALLABLE: VM References🔗

HANDLE is the unique owner of a VM — not copyable, provides CALL plus management operations via ecall (DOWNGRADE, SET_MAX_GAS, DIRTY, RESUME). CALLABLE is a copyable entry point — CALL only. DOWNGRADE(HANDLE) creates a CALLABLE with the HANDLE's current gas limit baked in. Different CALLABLEs to the same VM can have different gas ceilings.

RESUME (ecall op 0x0D) restarts a FAULTED VM with fresh gas, preserving registers and PC. This enables the pager pattern: parent fixes the environment (maps missing pages via indirection), then RESUMEs the child transparently.

structure

Jar.JAVM.Cap.HandleCap : Type
Jar.JAVM.Cap.HandleCap : Type

HANDLE capability: VM owner. Unique, not copyable.

Provides CALL (run VM) plus management ops via ecall: DOWNGRADE, SET_MAX_GAS, DIRTY, RESUME.

Constructor

Jar.JAVM.Cap.HandleCap.mk

Fields

vmId : Nat

VM index in the kernel's VM pool.

maxGas : Option Nat

Per-CALL gas ceiling (inherited by DOWNGRADEd CALLABLEs).

structure

Jar.JAVM.Cap.CallableCap : Type
Jar.JAVM.Cap.CallableCap : Type

CALLABLE capability: VM entry point. Copyable.

Constructor

Jar.JAVM.Cap.CallableCap.mk

Fields

vmId : Nat

VM index in the kernel's VM pool.

maxGas : Option Nat

Per-CALL gas ceiling.

10.1.5. Protocol Caps🔗

Protocol caps are kernel-handled services (storage, preimages, transfers, etc.) invoked via CALL — identical interface to calling a VM. Any protocol cap can be replaced with a CALLABLE to a wrapper VM, enabling transparent policy enforcement. The child code is identical either way.

structure

Jar.JAVM.Cap.ProtocolCap : Type
Jar.JAVM.Cap.ProtocolCap : Type

Protocol capability: kernel-handled, replaceable with CALLABLE.

Constructor

Jar.JAVM.Cap.ProtocolCap.mk

Fields

id : Nat

Protocol cap ID.

inductive type

Jar.JAVM.Cap.ManifestCapType : Type
Jar.JAVM.Cap.ManifestCapType : Type

Cap entry type in the blob manifest.

Constructors

code : Jar.JAVM.Cap.ManifestCapType

data : Jar.JAVM.Cap.ManifestCapType