Checked State graph definitions

Evidence correction: historical kill counts from the native Core-1 mutation runner before 9a63b70ff4 are withdrawn pending fresh replay. Stale binaries could produce false kills. This qualifies all such counts below; see docs/mutation-evidence.md. Test inventories are not execution evidence.

Status: source, package linking, checked artifact admission, reflection, and live-store execution are implemented for this bounded Int64 graph profile. The existing scalar State transition and Store.transact APIs remain available.

Definition profile

A non-portable compiled state message with no parameters, an Int64 output, and exactly the state effect can declare a bounded graph:

module example.graph;
public value Graph {
  public compiled state message add(type: Class<Self>, a: Int64, b: Int64)
    -> Int64 effects { state } { return a + b; }

  public compiled state message definition(type: Class<Self>)
    -> Int64 effects { state } {
    let total: Int64 = State.derived(30, Graph.add, 10, 20);
    let previous: Int64 = State.delay(20, 30, 0);
    let root: Int64 = State.cell(10, 7);
    return total;
  }
}

State.cell(id, initial) declares a mutable root. State.derived(id, Type.target, dependency...) declares one or two dependencies and a public compiled scalar State target with matching Int64 parameters and result. Targets can be imported; their checked call closure cannot require external effects or contract assertions. Contract-bearing definitions and reachable targets reject; unrelated helpers do not affect admission. State.delay(id, dependency, initial) declares an explicit seeded previous-committed-epoch edge. Initializers are signed literals spanning Int64, including -9223372036854775808; this closed signed-literal position does not change the shared grammar for ordinary expressions.

Node IDs are positive Int64 declaration labels, not live cell handles or transaction capabilities. Bindings select graph outputs; arithmetic belongs in the pure derived targets, not the definition. Definitions cannot execute as scalar transitions and cannot synthesize live store authority. Runtime cell and topic handles carry a process-local store identity. A handle from another or closed store cannot bind to the same local position in a new store. Their existing uint64 ABI is unchanged; handle values are not portable artifact identities.

Definitions contain 1–256 value nodes and topics combined, with at least one value node. Forward dependencies are permitted. Every dependency must resolve in the same graph. Duplicate IDs and instantaneous cycles reject, including disconnected cycles. Delay incoming edges break instantaneous cycles. Among ready nodes, the deterministic schedule chooses increasing node ID, independently of declaration order.

Source-declared topics

Definitions can also declare bounded event topics with explicit policies:

let events: Int64 = State.topic(90, 2, drop_oldest, cancel);

The arguments are a positive declaration label, capacity from 1 through 4096, an overflow name (reject_newest, drop_oldest, fail_transaction), and a subscriber-failure name (continue, cancel, stop_drain). All are required; unknown names, numeric policy selectors, and implicit defaults reject. Topic labels share the definition’s unique label namespace with value nodes, but topics cannot be dependencies or selected outputs. The declaration binding is checked metadata, not a scalar value or live topic handle.

Live execution

zl_state_store_open_graph_i64_v2 selects one public checked definition and creates an owned store. It retains a validated module copy, so callers may destroy the source module immediately. Graph label lookup returns an instance-scoped cell handle; node and output snapshot APIs expose committed values and versions. Derived and delay handles are read-only. Declared topics are created with fresh store-bound handles and their checked policies. zl_state_store_graph_topic_i64_v2 resolves a label, and topic count and snapshot APIs expose declarations, policies, and committed queue counts. Additional host-created topics are not included in graph enumeration.

Initialization evaluates the derived nodes and uses each delay’s seed without advancing any version. A failed initial calculation returns ZL-STATE-0001 without publishing a store. Each successful transaction atomically commits root writes, affected derived values, delay values, versions, and queued events. A committed root write advances its version even when its value is unchanged; an empty transaction does not write roots. Affected derived nodes advance once per committed evaluation, rather than once per staged write. Delay nodes sample their dependency’s previous committed value on every successful transaction, including an empty transaction. Failed calculations advance nothing, enqueue nothing, and permit a later recovery transaction. Snapshots during a transition expose the previous commit. Subscribers run only when the owner explicitly drains events after the commit.

The reference executor recursively evaluates dependencies from immutable committed values and staged writes; it does not read the stored schedule. The compiled live executor follows the independently checked topological schedule and uses materialized scalar evaluators. Neither path requires LLVM.

The CLI exposes bounded source/artifact execution:

zlc state-run --edition=core-1 --preview=state \
  --selector=example.graph.Graph.definition --executor=compiled \
  --step=10:10 --step=noop --step=10:2 graph.zl

Use --executor=reference for the independent stepper, or replace the source path with a checked .zlm artifact. The JSON result has schema zerglang.state-graph-run/1, an initial observation, and one observation per step. Each includes status, State error code, selected output, and all nodes sorted by declaration label. Failed steps are recorded and execution continues. Input is limited to 4 MiB and 64 steps; an empty step sequence is valid. --diagnostics=json provides JSON configuration and admission errors. Opting into --runtime-observation selects zerglang.state-graph-run/2 and adds the bounded metadata-only runtime projection to each observation. Without that flag the existing v1 output is unchanged.

Topic emission, subscriptions, callbacks, and stale-compute publication remain explicit runtime API operations; topic declarations do not install callbacks or emit events automatically. Source syntax for automatically installed reactions and outboxes is not implemented; the bounded benchmark adapter below explicitly binds checked Algorithm handlers to runtime subscriptions. The CLI supports one root write or an empty transaction per step; the runtime API supports atomic multi-root writes and events in the same transaction.

Explicit runtime policies

Topic construction requires positive capacity and recognized overflow and subscriber-failure policies. The policies have distinct observable behavior:

Overflow policy	Full topic queue	Cell/graph commit
REJECT_NEWEST	Discard excess new events	Commit
DROP_OLDEST	Evict the oldest event of this topic	Commit
FAIL_TRANSACTION	Preserve the existing queue	Roll back the entire transaction

A failing subscriber can continue, be deactivated without consuming its owned handle, or stop the drain with an error. Stopping consumes the current event and retains later queued events for a subsequent drain. Continue and cancel isolate the failure from other subscribers.

Compute publication explicitly selects reject, accept, merge, or recompute when the observed version differs from the committed version. Merge and recompute require a successful caller-supplied resolver for a stale result; a missing or failing resolver preserves both root and derived snapshots. Fresh results publish directly without invoking stale-only resolution. Zero-capacity topics and unknown policy values reject without publishing state.

Artifact and inspection

Schema 2.24 / ZLA2 1.16 is selected for checked State graphs without topics. The allocation is separate from the frozen Core-1 edition registry, in spec/extensions/core1-state-graph.json. Existing artifact bytes and older schema API ranges are unchanged. zl_zlm2_wire_schema_v6(24, ...) and zlc zlm2-schema --minor=24 expose its descriptor; the CLI default stays 2.20. Schema 2.25 / ZLA2 1.17 is selected for graphs with declared topics, allocated separately in spec/extensions/core1-state-topic.json. zl_zlm2_wire_schema_v7(25, ...) and zlc zlm2-schema --minor=25 expose this descriptor. Older descriptor bytes and API ranges are unchanged; a topic artifact cannot masquerade as 2.24.

Semantic kinds state-cell, state-derived, and state-delay retain the definition. Configuration is canonical metadata in generated call carriers; typed derived targets remain ordinary checked calls. No live authority is serialized. Graph definitions have no scalar executable rows. Decoding checks carrier shape, reconstructs dependencies, rejects cycles, and rebuilds the schedule from the retained checked semantic tree. It also rebuilds State scalar targets from that tree and rejects any serialized constant, operator, input, or output row that disagrees with the checked body.

Reflection adds state_graph for a definition, with its selected output, topological order, and nodes (IDs, kinds, initial values, dependencies, and derived target selectors). Node configuration participates in body identity; changing a seed changes the body, not the declared callable contract. For topic-bearing definitions, state_graph.topics records each declaration’s label, capacity, overflow policy, and subscriber-failure policy. These checked facts participate in body identity and survive package linking and normalization.

Verification

The frontend and CLI tests cover source and package round trips, malformed rehashed dependencies, cycle rejection, node-count bounds, signed initializer limits, body identity, and non-admission as scalar transitions. Generated properties cover declaration permutation, artifact normalization, and closed descriptor allocations. Native callback and subscription contracts separately have 14 sanitizer-backed runtime mutation controls, including cross-store cell and topic rejection.

The graph gate has 20 behavior-mapped controls for duplicate and unknown IDs, cycle rejection, delay semantics, deterministic scheduling, initializer and output preservation, bounds, decoded admission, scalar non-admission, and payload layout, canonical derived scalar bodies, and explicit topic policy preservation and bounds. Both offline CI workflows run it and the graph properties.

Live tests compare source/artifact and both executors across DAG updates, delayed feedback, empty transactions, signed limits, failure rollback, multi-root/event atomicity, foreign handles, and source-module destruction. Generated epoch sequences check expected arithmetic and version laws as well as differential agreement. The sanitizer-backed state-live mutation gate has 21 controls for scheduling, delay reads and seeds, versions, write admission, rollback, label resolution, module ownership, CLI bounds and values, and topic instantiation and observable queue/policy facts.

The public runtime policy tests exhaust all nine overflow/subscriber-failure combinations for both source-declared and host-created topics, plus healthy-subscriber isolation, all four stale-result policies, resolver failures, fresh-result behavior, and invalid policy bounds. They run against both executors. Source-topic ownership tests cover multiple topic labels, queue visibility during staging, full-queue rollback, namespace separation, module destruction, store closure with pending events, and rejection of foreign or label-forged handles. The runtime mutation gate has 28 controls: 14 for callback admission, handle authority, and lifetime, and 14 for explicit policy behavior.

Bounded benchmark State sequences

The separately pinned ZL256 0.7.0 corpus promotes all 20 remaining State scaffolds using this adapter, with 102 authored cases across both executors. The published Task/6 schema closes input and trace fields; the typed loader additionally checks exact numeric bounds, selected source membership and semantic observation consistency.

Benchmark task revision 6 uses the separately versioned zerglang.benchmark-exec/9 request. Each case selects source_path, source_files, and a qualified graph selector from its pinned source pool, input_kind (source or roundtrip), lifetime (retain or release), and state_steps. Both state-reference and state-compiled execute the same sequence. Legacy task and request revisions retain their earlier contracts.

The profile supports 0–64 explicit steps. A transaction step has action: transact, writes, events, and outcome: commit | rollback. Writes and events are arrays of at most 16 {id, value} pairs using declaration labels and exact signed Int64 values. The typed task input requires integer values; the native wire carries their canonical decimal strings. Each step enters the real public transaction API. It does not evaluate a fixture-specific model or accept an expected result from the request.

The state-graph-trace response records initial committed output, nodes sorted by label, topics with their explicit policies, and queue counts. Every step records its actual status and State error, the committed output and queue count observed during staging, and the complete post-step observation. Failed steps remain visible and later steps can recover. release destroys the caller’s module before the sequence; the live graph’s owned checked copy remains valid. Callback bindings own a separate checked module copy, including when the input has already been serialized and reloaded. Closing the store makes subsequent after observations null; transactions, drains, and new subscriptions then reject, while owned subscriptions can still be cancelled. Request and response budgets remain 64 KiB. An oversized trace returns one harness error, never a truncated success document.

Additional actions have closed, action-specific fields:

Action	Required fields beyond action
subscribe	subscription (1–64), topic label, delivery
cancel	subscription
drain, dispatch, close	None
publish	node, observed_version, candidate, policy, resolver

Subscriptions use observe, reenter, reaction, or outbox delivery. Only reaction and outbox require a handler: an exact qualified public root Algorithm entry with two Int64 parameters, an Int64 result, and no effects or capabilities. Reaction handlers use the checked Algorithm interpreter; the State executor choice controls graph and State resolver evaluation, not an Algorithm LLVM claim. Duplicate active subscription labels reject. Explicit cancellation consumes the owned handle, including after policy cancellation or store closure, and a cancelled label can subsequently be reused.

drain uses the real runtime queue and subscriber-failure policy. Its deliveries record the subscription, event, committed output snapshot visible at delivery, status, optional result, and diagnostic. Rollback emits no events; callbacks never run during staging. The reenter probe attempts a nested transaction and records the actual reentry rejection. A reaction receives (event, captured_output) and runs during post-commit delivery.

An outbox delivery only copies the event, snapshot, and checked handler binding into a request-local owned record. dispatch executes those records later and reports dispatches; neither a later commit nor subscription cancellation or store closure changes their captured values. Each record is consumed after one attempt, including handler failure; an empty second dispatch reports no rows. Both drain and dispatch report outbox_pending. There are at most 256 delivery rows per action and 256 queued outbox records, within the shared response budget. This is an in-memory benchmark adapter, not durable storage, retries, network delivery, or an external-effect implementation.

publish passes the selected root cell, observed UInt64 version, Int64 candidate, and explicit reject, accept, merge, or recompute policy to the public runtime. Reject/accept require resolver: none; merge/recompute require an exact qualified public checked Int64 State resolver with two parameters and no authority beyond State. The public zl_module_state_transition_signature_i64_v2 API validates that supported signature without running it. Resolvers execute only for stale results and receive (current_cell, candidate). Invalid bindings reject before publication; evaluation faults leave committed values and versions unchanged.

Public tests cover rollback, backpressure, derived arithmetic faults and recovery, invalid/read-only labels, empty and boundary-size sequences, pinned source selection, typed input rejection, and comparison with independently authored trace oracles. Generated transaction sequences check rollback identity and version laws across both executors and representations. Additional tests cover all nine source overflow/subscriber-failure combinations, one-time deferred delivery, reentry, cancellation, closure, binding admission, stale policies, and an independently authored callback trace oracle. Generated sequences check that post-commit records preserve their captured values across later commits, cancellation, closure, and dispatch. The sanitizer-backed state-sequence mutation gate contains 35 behavior-mapped controls for the transport, callbacks, qualified State signature/entry boundaries, and checked linked carriers. Both offline workflows run it and the generated sequence properties.

These checks do not promote the scaffolded State benchmark fixtures. Complete policy-bearing corpus execution and its independent observations remain separate work.

Rich State source follow-up (ZER5-229)

The 2026-09-09 audit leaves ZER5-229 in Icebox pending its named ZER5-227 first-class typed result/host-boundary prerequisite. The native live-store policies, atomic multi-write/event transactions and explicit benchmark handler bindings above remain implemented. They do not constitute automatic checked source installation of reactions/outbox handlers, arbitrary typed schemas or structured transition evaluation. ZER5-26’s bounded delivery is not reopened.

Reproduced boundary

Public probes used the clean archived compiler/library at 3cf6d107e4b899500b0c79cd2461a87a866fa8b8, version 0.1.1-preview.4, Apple Clang 17.0.0 on arm64 macOS with LLVM disabled. Worktree 18be520578 differed only through subsequent documentation commits.

Probe	Observed result
Int64 root and explicitly configured source topic	Accepted
State.cell(10, true)	ZL-STATE-0001: State graph initial value requires an Int64 literal
Local Cell<Int64> annotation	ZL-TYPE-0001: type does not resolve to a supported scalar or enum
Omitted topic subscriber-failure policy	ZL-STATE-0001: State.topic requires an explicit subscriber-failure policy
Scalar transition return item * item with input -6	Both executors return 36, source and checked round-trip
Transition with if/else returning the absolute value	Compiles and round-trips; both transition admissions reject with ZL-DOMAIN-0003: message has no dedicated checked scalar region

The transition harness uses only public compilation, checked serialization and zl_module_state_transition_run_i64_v2; it does not substitute host arithmetic for an unsupported region. The live CLI control graph, with --runtime-observation --step=noop, retains output 7/version 0 and reports one topic, zero pending events and zero subscriptions in both executors, initially and after the commit. A topic declaration alone installs no handler.

The existing State runtime, graph frontend/live execution, owner authority, policies, topics, callbacks, subscriptions and observation groups passed 9/9 in 5.91 seconds with 90-second per-test deadlines and --no-tests=error. These include existing Python-driven native wrappers, not a new ZDE UI campaign. Complete logs, transition harness, source probes and CLI projections are retained in /private/tmp/zerglang-229-state-audit.4Sk4uR/.

Required source/runtime work

The parser’s closed State graph dispatch currently contains only cell, derived, delay and topic. Derived targets and graph outputs are Int64; the shared scalar-region lowering does not materialize structured control flow. Native subscriber and stale-publication callbacks are explicit owner- bound API calls. src/benchmark_state_callbacks.inc separately validates requested checked handler selectors and owns its request-local outbox. That adapter is not a source subscription declaration, durable outbox or network delivery service.

Resume with ZER5-227-compatible typed schemas, owner/error contracts and checked handler bindings, then implement and verify:

• Structured transition regions in both independent evaluators. Multiple candidate writes/events commit together or leave values, versions and queues unchanged; untaken faulting branches do not run. No callback, Intent, network or device action may execute during an active or aborted transaction.
• Explicit source subscriptions and post-commit reaction/outbox bindings, with owned subscriber lifetime, cancellation/closure and failed-drain semantics. Preserve captured committed values and exact reachable handler identities across source, packages and checked artifacts.
• Explicit stale-result reject/accept/merge/recompute policy bound to the correct live store and checked resolver. Wrong/stale owners, missing policy, failed resolvers, unsupported borrowed results and cycles without delay reject observably without publishing partial state.
• Public failing acceptance cases followed by generated atomicity, order, ownership and relocation properties and behavior-mapped mutations. Extend ZER5-241’s canonical snapshot and visible ZDE tests to show newly admitted committed versus staged/pending events, source subscriptions and failed drains; the existing metadata-only profile does not imply new semantics.

The source/runtime addition must be explicitly versioned without changing old graph bytes or implying distributed durability. This documentation-only audit uses the test-first/mutation exception and changes no runtime, artifact, corpus, publication or activation state.