This document defines the current protocol-machine instruction set in rust/machine/src/instr.rs.
The protocol machine groups instructions by execution concern.
Family Instructions
Communication Send, Receive, Offer, ChooseSession lifecycle Open, CloseEffect and guard Invoke, Acquire, ReleaseSpeculation Fork, Join, AbortOwnership and knowledge Transfer, Tag, CheckControl Set, Move, Jump, Spawn, Yield, Halt
All register operands are bounds-checked at runtime. Out-of-range reads or writes fail with Fault::OutOfRegisters.
Instruction Fields Runtime effect
Sendchan, valEmits a send on the endpoint in chan. Payload routing is decided through the effect handler path. Receivechan, dstReads one message from the partner edge and writes the payload to dst. Offerchan, labelPerforms internal choice and emits the selected label. Choosechan, tableReads a label and branches by jump table entry.
Instruction Fields Runtime effect
Openroles, local_types, handlers, dstsAllocates a new session, initializes local type state per role, binds edge handlers, and writes endpoint handles to destination registers. ClosesessionCloses the referenced session and emits close and epoch events.
Instruction Fields Runtime effect
InvokeactionExecutes an effect step through the bound handler for the session. Acquirelayer, dstAttempts guard acquisition and writes evidence to dst when granted. Releaselayer, evidenceReleases a guard layer using previously issued evidence.
Instruction Fields Runtime effect
ForkghostEnters speculation scope tied to a ghost session identifier. Joinnone Commits speculative state when reconciliation checks pass. Abortnone Restores scoped checkpoint state and exits speculation.
Instruction Fields Runtime effect
Transferendpoint, target, bundleTransfers endpoint ownership and associated proof bundle to a target coroutine. Tagfact, dstTags a local knowledge fact and returns the result in dst. Checkknowledge, target, dstChecks a fact under the active flow policy and writes the check result to dst.
Instruction Fields Runtime effect
Setdst, valWrites an immediate value to a register. Movedst, srcCopies a register value. JumptargetPerforms an unconditional jump. Spawntarget, argsSpawns a child coroutine with copied argument registers. Yieldnone Yields back to the scheduler. Haltnone Terminates coroutine execution.
rust/machine/src/compiler.rs exposes compile(local_type: &LocalTypeR) -> Vec<Instr>.
The compiler emits communication instructions, Invoke, and control-flow instructions. It does not emit session lifecycle, guard, speculation, or ownership opcodes.
LocalTypeR nodeEmission pattern
single-branch Send Send then Invoke then continuationmulti-branch Send deterministic Offer on first branch then continuation single-branch Recv Receive then Invoke then continuationmulti-branch Recv Choose with patched jump table then branch blocksMurecords loop target then compiles body VarJump to loop target if bound, otherwise HaltEndHalt
The compiler is intentionally simple. Full ISA coverage is provided by direct bytecode construction and runtime loaders.