JAR: Join-Accumulate Refine

10.5. ecalli / ecall Dispatch🔗

Two PVM instructions for all capability operations:

ecalli(imm): CALL a cap. The u32 immediate encodes the subject cap slot with indirection. phi[7..11] = 5 args, phi[12] = object cap (u32, indirection). The compiler can optimize local protocol cap calls via the original bitmap (inline the handler if the slot is unmodified, generic dispatch otherwise).

ecall: management ops + dynamic CALL. phi[11] = operation code, phi[12] packs subject (low u32) and object (high u32) with indirection. Always goes to kernel dispatch — compiler cannot inline.

phi[7..10] have the same meaning in both instructions.

🔗inductive type
Jar.JAVM.Cap.EcalliOp : Type
Jar.JAVM.Cap.EcalliOp : Type

ecalli immediate decoding. ecalli is CALL-only — subject cap from the u32 immediate (with indirection encoding). Management ops use ecall.

Constructors

call (capRef : Jar.JAVM.Cap.CapRef) : Jar.JAVM.Cap.EcalliOp

CALL cap at the resolved slot.

🔗inductive type
Jar.JAVM.Cap.EcallOp : Type
Jar.JAVM.Cap.EcallOp : Type

ecall operation codes (from φ[11]).

Subject and object cap references are packed in φ[12] as two u32 values with indirection encoding: subject = low u32, object = high u32.

Constructors

call : Jar.JAVM.Cap.EcallOp

Dynamic CALL (same semantics as ecalli, dynamic subject).

map : Jar.JAVM.Cap.EcallOp

MAP pages of a DATA cap in its CNode.

unmap : Jar.JAVM.Cap.EcallOp

UNMAP pages of a DATA cap in its CNode.

split : Jar.JAVM.Cap.EcallOp

SPLIT a DATA cap.

drop : Jar.JAVM.Cap.EcallOp

DROP (destroy) a cap.

move : Jar.JAVM.Cap.EcallOp

MOVE a cap between CNodes.

copy : Jar.JAVM.Cap.EcallOp

COPY a cap between CNodes (copyable types only).

downgrade : Jar.JAVM.Cap.EcallOp

DOWNGRADE a HANDLE to CALLABLE.

setMaxGas : Jar.JAVM.Cap.EcallOp

SET_MAX_GAS on a HANDLE.

dirty : Jar.JAVM.Cap.EcallOp

Read dirty bitmap of a child's DATA cap.

resume : Jar.JAVM.Cap.EcallOp

RESUME a FAULTED VM.

unknown : Jar.JAVM.Cap.EcallOp

Unknown/invalid op.

🔗def
Jar.JAVM.Cap.decodeEcalli (imm : UInt32) : Jar.JAVM.Cap.EcalliOp
Jar.JAVM.Cap.decodeEcalli (imm : UInt32) :
  Jar.JAVM.Cap.EcalliOp

Decode an ecalli immediate. Always a CALL.

🔗def
Jar.JAVM.Cap.decodeEcall (op : Nat) : Jar.JAVM.Cap.EcallOp
Jar.JAVM.Cap.decodeEcall (op : Nat) :
  Jar.JAVM.Cap.EcallOp

Decode an ecall operation from φ[11].

🔗inductive type
Jar.JAVM.Cap.DispatchResult : Type
Jar.JAVM.Cap.DispatchResult : Type

Result of CALL dispatch.

Constructors

continue_ : Jar.JAVM.Cap.DispatchResult

Continue execution of active VM.

protocolCall (slot : Nat) (regs : Jar.JAVM.Registers)
  (gas : Nat) : Jar.JAVM.Cap.DispatchResult

Protocol cap called — host should handle.

rootHalt (value : Nat) : Jar.JAVM.Cap.DispatchResult

Root VM halted normally.

rootPanic : Jar.JAVM.Cap.DispatchResult

Root VM panicked.

rootOutOfGas : Jar.JAVM.Cap.DispatchResult

Root VM out of gas.