R-wave-boundary
Statement
outside batch: one ctx.down(msgs) = one wave; inside batch: accumulation until commit = one wave
Protocol
Active protocol rules.
Mechanical filter: active authority rule records in wave, runtime, graph, node, and control areas. Conformance rows are resolved from covered scenarios with all runtimes passing.
Area
wave
13 rulesR-dirty-before-data
Conformance
- C-1cross-graph diamond coalescets:pass · rust:pass · py:pass
- C-4mixed sync/async diamondts:pass · rust:pass · py:pass
Statement
every tier-3 (DATA/RESOLVED) emission is preceded by DIRTY in the same wave; the dispatcher synthesizes a [DIRTY] prefix when the caller omits it and the node is not already dirty; raw and framed emission paths are observationally identical on the wire
R-two-phase
Conformance
- C-1cross-graph diamond coalescets:pass · rust:pass · py:pass
- C-4mixed sync/async diamondts:pass · rust:pass · py:pass
Statement
DIRTY (phase 1) propagates through the entire reachable graph before DATA/RESOLVED (phase 2) begins — glitch-free diamond. Activation exemption: a compute fn's first run during subscribe() does not require a preceding DIRTY
R-diamond
Conformance
- C-1cross-graph diamond coalescets:pass · rust:pass · py:pass
- C-4mixed sync/async diamondts:pass · rust:pass · py:pass
Statement
diamond/fan-in: D recomputes exactly once after all changed deps settle in same wave
R-invalidate-idempotent
Conformance
- C-3INVALIDATE × ctx.state × onInvalidatets:pass · rust:pass · py:pass
Statement
INVALIDATE is broadcast at most once per node per wave (diamond fan-in cascades it once, not once per arriving path); an INVALIDATE arriving at an already-reset OR never-populated cache is a no-op — neither the cleanup hook nor the downstream broadcast fires again
R-sentinel
Statement
SENTINEL = absence-of-DATA, protocol-decidable; the concrete sentinel value is per-language (TS undefined/Rust None/Py sentinel)
R-push-subscribe
Statement
push-on-subscribe: in the SENTINEL state push [START]; in the dirty state push [START,DIRTY]; cached DATA is pushed to the new subscriber. START is the handshake — the first message any sink receives on a subscription, emitted before any other downstream delivery, not forwarded through intermediate nodes. EXCEPTION (R-pull / D55): a pull-mode node while QUIET pushes [START] ONLY — its cached value is NOT pushed on subscribe (it stays silent until demanded).
R-terminal
Statement
terminal-is-forever by default; resubscribable opt-in triggers a fresh-lifecycle reset. A late subscribe to a non-resubscribable terminal node is REJECTED (idiomatic error); to a resubscribable terminal node it resets the lifecycle (clears terminal/has-fired-once/DepRecords, drains pause lockset, re-arms first-run gate) before installing the sink. TEARDOWN does not block reset
R-deps-terminal
Conformance
- C-17an absorbed-error dep counts as TERMINAL for auto-COMPLETE (no wedge, order-independent)ts:pass · rust:pass · py:pass
Statement
completeWhenDepsComplete (default true): node auto-emits COMPLETE when ALL deps are TERMINAL — each dep has reached COMPLETE *or* an ABSORBED ERROR (errorWhenDepsError:false); an absorbed-error dep COUNTS as terminal-done (it is settled — no more input can arrive), it does NOT block completion (B42). Completion is 'all deps TERMINAL', NOT 'all deps Complete' and NOT 'ANY' (combineLatest semantics — fires once all sources settle). errorWhenDepsError (default true): node auto-emits ERROR when any dep errors (this auto-ERROR fires BEFORE the complete-check, so an error-terminal dep only reaches the completion logic when errorWhenDepsError:false has absorbed it). Terminal-emission operators (last/reduce) set completeWhenDepsComplete:false; rescue/catch operators set errorWhenDepsError:false and read ctx.depRecords[i].terminal explicitly. SCOPE: a dep TERMINAL = COMPLETE | ERROR; TEARDOWN is a destroy-cascade (tears the node down, not a settle) and does NOT count (B33-adjacent, out of scope). IMPL (TWO parts): (1) _allDepsComplete counts a TERMINAL dep as done — block only on a LIVE dep (TS `dep_terminal === undefined` blocks; NOT `!== true/Complete`), Rust all_deps_complete mirrors. (2) BOTH the COMPLETE receive-arm AND the absorbed-ERROR receive-arm (errorWhenDepsError:false) must check `completeWhenDepsComplete && all-deps-terminal -> COMPLETE`: the COMPLETE arm already does, but the ERROR-absorbed arm currently routes straight to _settleAfterAbsorbedTerminal/_maybeRun WITHOUT the check, so an absorbed-error dep terminating LAST would not fire the cascade — it must MIRROR the COMPLETE arm's check (Rust receive_from_dep ERROR arm same). Order-independent: whichever terminal lands last triggers the auto-COMPLETE.
R-reentrancy
Conformance
- C-6synchronous feedback cycle → ERRORts:pass · rust:pass · py:pass
Statement
a synchronous feedback cycle — a node fn that, during its invocation, transitively re-drives one of its own (direct or indirect) deps so the same node's fn would re-enter before its wave completes — is a wave-level protocol ERROR. Detection is node-local and free: a node refuses to enter its fn-run while its own in-wave flag (_insideRunWave) is already set, and throws; the graph layer catches the throw and converts it to [[ERROR, e]] down (D30 — value-level throw → graph-layer ERROR), located at a node ON the cycle (the value-level catch nearest the throw on the synchronous unwind — implementation-determined, NOT necessarily the re-entered node), aborting the wave. The core neither queues nor bounds-then-runs the cycle (reject, not iterate). Legitimate accumulation uses per-node ctx.state (e.g. scan): not a topological cycle, never re-enters. Async feedback that crosses a turn boundary via an async pool is out of scope — it is not synchronous re-entry and does not desync the wave. No numeric rerun-depth cap is needed (precise in-wave flag detection supersedes the blunt maxFnRerunDepth)
R-resolved-undirty
Conformance
- C-12occurrences stay DATA; RESOLVED is undirty-only (no equals-substitution)ts:pass · rust:pass · py:pass
Statement
RESOLVED is the UNDIRTY / no-occurrence settle: a node DIRTY'd in phase 1 that produces NO tier-3 value this wave emits exactly one RESOLVED to clear the downstream dirty (filter-reject / no-emit fn, zero-dep un-dirty, INVALIDATE at a never-populated cache, batch-rollback DIRTY-balance). RESOLVED NEVER substitutes for a DATA and NEVER signals 'value unchanged' -- every value-occurrence is emitted as DATA regardless of value-equality (no auto-equals-substitution; the substrate does not inspect per-wave DATA count for substitution). The undirty RESOLVED is SUBSTRATE-SYNTHESIZED: a value-level operator simply returns without emitting and the substrate emits the balancing RESOLVED (R-primary-api-clean -- operator bodies carry no protocol tier); an operator MAY emit its own DATA/RESOLVED explicitly as an escape hatch. Tier-3 wave exclusivity holds: one node's settle this wave is >=1 DATA (occurrence) XOR exactly 1 RESOLVED (undirty), never mixed. RESOLVED is preceded by DIRTY in the same wave (R-dirty-before-data) like DATA. Dedup (suppress an unchanged emission / skip an expensive recompute) is OPT-IN at the operator layer (distinctUntilChanged / fn early-return), never a substrate behavior; NodeOptions.equals does not exist.
R-terminal-settles-dirty
Conformance
- C-15a dep's terminal releases its in-wave DIRTY contribution (no wedge)ts:pass · rust:pass · py:pass
Statement
A dep's TERMINAL (COMPLETE/ERROR) RELEASES that dep's outstanding in-wave DIRTY contribution: if the dep went DIRTY this wave (phase 1) and has NOT yet settled with DATA/RESOLVED, the receiving node clears that dep's dirty flag and decrements its pending count — exactly as the DATA/RESOLVED/INVALIDATE arms do. This is the EXACTLY-ONE-SETTLE invariant: every dep that goes DIRTY in phase 1 has its contribution released in phase 2 by exactly one settle-class event in {DATA, RESOLVED, INVALIDATE, COMPLETE, ERROR}. It applies in the ABSORBED-terminal cases where the node stays live — completeWhenDepsComplete:false (last/reduce, the *Map higher-order operators) and errorWhenDepsError:false (rescue/catch, R-deps-terminal); the AUTO-CASCADE cases (completeWhenDepsComplete && all deps complete -> node COMPLETE; errorWhenDepsError && a dep errors -> node ERROR) make the node itself terminal, so pending is moot there. If releasing the terminal dep's contribution drains pending to 0 while the node has already broadcast DIRTY this wave AND no terminal cascade fires, the node SETTLES: it recomputes (-> DATA from the remaining live deps' latest values) or, producing no tier-3 value, the substrate synthesizes exactly one undirty RESOLVED (R-resolved-undirty) to balance the downstream DIRTY. WITHOUT this release, a dep that emits DIRTY-then-COMPLETE/ERROR-without-a-value strands pending>0 -> the node never recomputes/settles and the DIRTY it broadcast wedges the downstream cone (the deadlock R-invalidate-idempotent already prevents for the INVALIDATE case). Restores R-diamond / R-two-phase for a diamond whose one leg terminates mid-wave. SCOPE: COMPLETE/ERROR only; a TEARDOWN arriving at a dirtied dep is the terminal-relay question (R-teardown-complete / B33), out of scope here.
R-undirty-settle-timing
Conformance
- C-19undirty RESOLVED timing respects resumeAll and batchts:pass · rust:pass · py:pass
Statement
A substrate-synthesized undirty RESOLVED used to balance a previously broadcast DIRTY follows normal tier-3/4 delivery timing. In pausable:true default mode it may deliver immediately even while a pause lock is held; in pausable:'resumeAll' it is buffered and replayed on final-lock RESUME; inside an open batch it is deferred until the outermost batch commit. This applies to undirty RESOLVED produced by terminal dirty-release (R-terminal-settles-dirty) and by INVALIDATE dirty-clear paths. Implementations must not bypass the normal delivery path with a bare subscriber send for these balancing RESOLVEDs.
Area
node
3 rulesR-cleanup-hooks
Conformance
- C-14cleanup hooks are per-run (cleared + re-registered each fn run)ts:pass · rust:pass · py:pass
Statement
two cleanup hooks: ctx.onDeactivation(fn) (release external resources on deactivation) + ctx.onInvalidate(fn) (flush on INVALIDATE). onRerun (0 callsites) and onResubscribableReset (1 callsite → absorbed by ctx.state lifecycle) are cut. fn return value is freed for sugar mapping. PER-RUN LIFECYCLE (D28 clarification): both hook lists are CLEARED before each fn invocation and re-registered by the fn body — only the LATEST run's registrations are live (React effect-cleanup model). A re-run SUPERSEDES the prior run's hooks; superseded registrations are DISCARDED WITHOUT firing (consistent with the cut onRerun — there is no fire-on-rerun hook). So after K fn runs, an INVALIDATE fires onInvalidate exactly once (the current run's), and deactivation fires onDeactivation exactly once (NOT K times). Contract: a fn must (re-)register its cleanup on EVERY run that needs it (a registration guarded to a single run is dropped on the next run). A single-run node keeps its single registration (no re-run = no clear). deactivate() fires the live onDeactivation hooks then clears both lists.
R-ctx-state
Conformance
- C-3INVALIDATE × ctx.state × onInvalidatets:pass · rust:pass · py:pass
Statement
ctx.state = per-node private cross-wave state (implicit OK — node-private, not shared). Default fresh-lifecycle wipe; ctx.state.persist(on?) keeps across lifecycle. Shared/observable state must be an explicit node + dep (not ctx.state). INVALIDATE is lifecycle-continue (not fresh-lifecycle) so it does NOT wipe ctx.state — manual flush via onInvalidate
R-first-run-gate
Statement
compute fn first-fires only after every declared dep has settled (delivered ≥1 real DATA this or a prior wave) under partial:false — producing one combined initial wave. partial:true turns the gate OFF (fn fires as soon as dirty-dep-count hits 0; fn body MUST guard SENTINEL per dep). terminalAsRealInput:true also lets a dep terminal settle the gate (Reduce-class). The gate is first-run-only (has-called-fn-once); INVALIDATE does not re-arm it; a resubscribable terminal reset does
Area
control
3 rulesR-async-paused
Conformance
- C-2async-result arriving at paused nodets:pass · rust:pass · py:pass
- C-9pausable:false async source ignores PAUSE (keeps producing)ts:pass · rust:pass · py:pass
- C-10true-mode async leaf source delivers own production immediately under PAUSEts:pass · rust:pass · py:pass
Statement
an async result arriving at a paused node buffers and replays on final-lock RESUME -- BUT this is GATED by pausable mode (D44), not unconditional: it applies only when pausable in {true,'resumeAll'} and, in true mode, only to a COMPUTE node (deps>0). A pausable:false node never buffers (ignores PAUSE, keeps producing); a true-mode depless leaf source delivers its own async production immediately (R-pause-modes). The buffered result enters the node-level pause_lockset-scoped buffer (lock_id scope = node-level pause_lockset).
R-paused-invalidate
Conformance
- C-13INVALIDATE arriving at a paused compute nodets:pass · rust:pass · py:pass
Statement
INVALIDATE × PAUSE precedence (default/'true' mode). A dep's INVALIDATE arriving while a compute node N is paused: (1) PROPAGATES downstream immediately (consistent with immediate DIRTY — not buffered in default mode; the downstream's N-DIRTY is balanced by this INVALIDATE's dirty-clear); (2) SUPERSEDES that dep's buffered paused dep-wave — N clears the dep to SENTINEL + drops its pending change, then re-derives the pending-recompute flag from whether ANY dep still carries a buffered value-change (ATTRIBUTED). On final-lock RESUME N recomputes once with the latest dep values ONLY if some dep still has a live buffered change; if none remains the recompute is CANCELLED (N already settled to SENTINEL via its own INVALIDATE — it never recomputes against an all-SENTINEL dep set). A later DATA on the same dep re-arms the buffer ([DATA,INVALIDATE,DATA2] → recompute with DATA2). resumeAll mode buffers+replays tier-3/4 on its own path; this rule is the default-mode coalesce semantics.
R-teardown-terminal-relay
Conformance
- C-20TEARDOWN relays through terminal intermediatets:pass · rust:pass · py:pass
Statement
TEARDOWN relays through an already-terminal intermediate. A terminal node receiving upstream TEARDOWN forwards TEARDOWN downstream without emitting a new COMPLETE/ERROR, without clearing terminal, and without allowing post-terminal DATA/RESOLVED/INVALIDATE/COMPLETE/ERROR. A non-terminal node receiving TEARDOWN keeps R-teardown-complete behavior: synthesize COMPLETE before TEARDOWN unless the same wave already carries COMPLETE/ERROR. TEARDOWN is a destroy/unwire cascade, not a value/lifecycle resurrection.
Area
graph
3 rulesR-rewire
Conformance
- C-8intra-graph runtime rewirets:pass · rust:pass · py:pass
Statement
replaceDeps/subscribeDep/unsubscribeDep = runtime topology rewire, INTRA-graph only (D22 single causal domain; no inter-graph form — cross-graph wiring is only via the wire bridge). Surgical/Option-C: a dep in both old and new sets is left untouched (subscription + DepRecord survive); only removed deps unsubscribe + discard their DepRecord, only added deps fresh-subscribe; DepRecord-ref dispatch lets kept deps reorder freely. Across a rewire: the first-run gate (_hasCalledFnOnce) is PRESERVED, never re-armed (re-arming would re-gate unchanged deps); an added dep enters prevData=SENTINEL and the fn guards via prevData===SENTINEL; the activated compute-node cache is PRESERVED (R-rom-ram); pause lockset + buffer PRESERVED. An added dep with a cached DATA pushes [DIRTY,DATA] on subscribe (R-push-subscribe); a SENTINEL dep delivers START only. unsubscribeDep clears the removed dep's dirty contribution; if it was the sole dirty contributor and the node was dirty, the wave auto-settles. A removed dep's queued messages (DIRTY/DATA/INVALIDATE) are DRAINED — nothing strands downstream. Rejects: self-dependency; a cycle (DFS O(V+E)); a terminal this (completed/errored) for IMMEDIATE/external rewire; adding a non-resubscribable terminal dep (would wedge — resubscribable terminal deps are allowed). Deferred self-rewire queued before terminal is the D62 exception: R-rewire-deferred may apply subscribeDep/unsubscribeDep/replaceDeps after the owner becomes terminal, while terminal remains an output guard. unsubscribeDep to zero deps is allowed (degenerate fn-no-deps; cache preserved; no auto-deactivate). Mid-wave rewire (between dep deliveries) is allowed; mid-fn rewire (while the node's fn is executing, _insideRunWave) and reentrant rewire (another replaceDeps/subscribeDep/unsubscribeDep in flight) are REJECTED — a fn mutating its own topology mid-wave is the synchronous feedback-cycle ERROR (D37/R-reentrancy). Topology change does not bump a version counter (topology ≠ DATA). Every rewire API requires an explicit fn (fn-deps pairing: user fns read data[i]/prevData[i] positionally, so a dep-shape change must re-declare the fn). A SELF-triggered mutation (a fn changing its OWN deps in response to its own data) must use the deferred ctx.rewireNext path (R-rewire-deferred / D47), NOT an immediate in-fn call.
R-rewire-async-live-edge
Conformance
- C-21late async ctx emission uses live deps after rewirets:pass · rust:pass · py:pass
Statement
A ctx captured by an async pool callback routes through the node's LIVE topology at emission time. If the node is rewired after the async invocation starts and before the callback calls ctx.up/ctx.down, the callback observes the current dep set/fn shape, not an invocation-time dep snapshot. Removed deps are drained and receive no late ctx traffic; added deps participate if they are live at emission time. Terminal output guards still seal post-terminal down emission.
R-rewire-batch-boundary
Conformance
- C-22batch commit precedes rewire requested during open batchts:pass · rust:pass · py:pass
Statement
If replaceDeps/subscribeDep/unsubscribeDep is requested while an outer batch is open and the target node has an uncommitted batched tier-3/4 settle slice, the rewire is accepted but deferred until after the outermost batch commits. The pending batched wave commits first against the pre-rewire topology/fn shape; then queued rewire requests drain FIFO as fresh boundary waves. Topology mutation never applies to an uncommitted batch view, and old-shape pending DATA is never committed against the new dep set. Outside an open batch, immediate/external rewire remains immediate between waves.
Area
runtime
1 rulesR-graph-domain
Conformance
- C-1cross-graph diamond coalescets:pass · rust:pass · py:pass
- C-4mixed sync/async diamondts:pass · rust:pass · py:pass
Statement
graph = single-thread CONCURRENCY domain (the unit of concurrency, NOT the bound of causal influence). In-domain propagation is ONE synchronous causal wave: same-tick, glitch-free, diamonds RESOLVED-merged so a fan-in sees one consistent version of its source. Causal influence is NOT bounded by the graph — it CROSSES domains via the async wire bridge as DELAYED CONSISTENCY (a value produced in wave N is consumed one tick later in the peer domain; the two-phase wire gate preserves cross-domain consistency — wave_xgraph.tla L2.F). Compute parallelism is via pool callback (results serialize back to the domain's thread); true parallelism is via multiple graphs + wire bridge. Disjoint waves in the same graph do not parallelize (one concurrency domain = one dispatcher).