State, Effects, and Compatibility

Execution state

Each request i is modelled as a state tuple:

StateX_i = ( P_i, M_i, K_i, Q_i )

P_i: program position and continuation: the current ZIR operation, the frame stack, and pending unwinding.
M_i: request-owned mutable memory: every value and slot allocated in the request's region.
K_i: capability set: the effects this request may perform, each with type, scope and generation.
Q_i: remaining resource budget: a vector of instructions, bytes, open resources and wall time.

Shared immutable data S and the shared services are not part of X_i. S is a constant available to every transition; services are reached only through effects.

Transitions

Execution is a sequence of labelled steps. An action a is one ZIR operation: a pure computation, a memory operation on M_i, or an effect that names a capability.

StepX_i —a→ X_i′

MODEL D · Execution transitionsfig. 5

One step from state X_i under action a. The action either succeeds and produces X_i', faults because a needed capability is missing, exhausts the budget, or reaches termination. Only the first outcome continues; the others are defined, observable endings or errors.

A fault is not a terminal state. It transfers control to the program's error handling, exactly like a thrown exception, so the program may catch it and continue. Exhaustion and termination are terminal.

The isolation condition

IsolationMutableReach(M_i) ∩ MutableReach(M_j) = ∅ for i ≠ j

MutableReach(M_i) is the set of mutable cells reachable from request i's roots (its frames, its region, its reference slots and the object handles stored in them) without passing through an effect. The condition says no mutable cell is reachable from two requests.

Scope. The condition is about request-private memory only. It deliberately excludes shared immutable data, which may be reachable by everyone because it cannot change, and shared services, which are not reachable as memory at all: a request can only send them copied values through a capability. A cache that two requests use is therefore consistent with the condition, while a cached object handle that two requests both mutate is not.

Proposition 1 (preservation, sketch)

If the isolation condition holds for all pairs before a step, it holds after it.

Assumptions: every ZIR memory operation allocates only in the acting request's region; values crossing a service boundary are deep-copied; S is immutable after boot; handles are validated for owner and generation before dereference; native code accesses no region memory. Sketch: a step changes reachability only by allocating (new cells belong to M_i), by storing (both source and target already in M_i or S), or by receiving a service result (fresh copies in M_i). None adds a cell of M_j to the reach of i. The argument is only as strong as the assumptions; it is not a proof about any implementation.

Effects and authority

An effect action a names a capability c and an operation op. The rule has a success case and a failure case:

If c ∈ K_i, c's type permits op, c's scope includes the target, and c's generation is current, the service performs op and the step yields X_i′ with the copied result placed in M_i′.
Otherwise the step yields a fault: P_i′ is the program's error handler with a CapabilityError, M_i is unchanged except for the error object, K_i is unchanged, and the service is never contacted.

Proposition 2 (no unauthorised effect, sketch)

Every externally observable effect performed during request i corresponds to a step whose capability was in K_i at that step.

Assumptions: services are the only components able to perform external effects on a request's behalf; extension shims are counted as services and declare their capabilities; the engine has no other path to system calls during request execution. Logging by the engine itself is out of scope.

Resource accounting

BudgetQ_i′ = Q_i − cost(a), Q_i′ ≥ 0

Every action has a non-negative cost vector: instruction count, bytes allocated, resource handles opened, and wall time for effects that wait. The step is permitted only if every component stays non-negative. If any would go negative, the action is not performed and the request moves to Exhausted.

Exhaustion is not catchable by the program, by design: a handler that runs code would need budget the request no longer has. The engine runs the teardown sequence from TRACE B under a separate, fixed teardown allowance, then reports an error response. Budgets are configuration, not constants of the model, and choosing them well is an evaluation question.

Proposition 3 (bounded request, sketch)

A request performs at most Q_i⁰ units of each resource plus the fixed teardown allowance.

Assumptions: cost is charged before an action takes effect; costs are non-negative and complete (no free action has unbounded work); services account their work to the calling request; the clock used for wall-time budgets is monotonic.

Compatibility matrix

The matrix lists what each area of the ecosystem would demand of the design. It deliberately contains no pass rates: there is no implementation to measure.

Area	Concern	Proposed strategy	Evaluation method
Core semantics	Coercion, comparison, references, copy-on-write, destructor timing	Named ZIR operations per rule; reference counting for objects with destructors	Differential execution against the reference engine, including warnings
Standard library	Hundreds of functions with individual edge cases	Implement by usage frequency; unsupported functions fail loudly	Upstream language tests where licensing allows, plus generated inputs
Composer packages	Autoloading, static state, file-system assumptions	Autoload through a file capability; statics are request-scoped	Run package test suites under both engines and diff outcomes
Frameworks	Bootstrapping cost, container singletons, worker-mode resets	Freeze boot artefacts into shared immutable data; containers per request	Lifecycle tests: many sequential requests, assert no cross-request state
Database drivers	Native drivers, persistent connections, credentials	Pooled database service behind a capability; no credentials in the cell	Protocol-level tests and transaction-rollback-on-teardown checks
Reflection	Introspection of private state, attributes, closures	Supported read-only over region values; no reflection into services	Targeted suites for reflection APIs used by popular libraries
Dynamic loading	`eval`, computed `include`, runtime class creation	Run the pipeline at request time under the same checks and budget	Fuzz dynamic paths; assert budget accounting covers compilation
Native extensions	Unverifiable memory access, global state	Copying shim, declared capabilities, optional out-of-process hosting	Per-extension review; independent assessment of the shim