Chapter 07 — Rewrites and Materialization

A static Circuit is enough only when the work is known at compile time. Planners discover a missing dimension; reviewers expand a node into validation branches; gatherers choose a retrieval strategy after seeing intermediate output. This chapter specifies how Cortex admits topology change without dissolving into arbitrary mutation. The answer is a rewrite: a bounded runtime topology modification over an existing Circuit, drawn from a closed algebra, metered in gas, admitted by the runtime, and materialized into durable state with an explicit audit trail. Rewrites obey the same vocabulary, endpoint-compatibility, and validity rules a compiled Wire source must satisfy, plus a structural resource budget the runtime enforces at admission time.

Core model

A rewrite is a structured proposal, not a mutation. A stage produces its ordinary output and a rewrite value from a closed algebra; the runtime validates, checks against the remaining budget, and admits or rejects with a structured reason. No stage writes to the graph directly.

Authorship is split: stages and planners propose; the runtime admits. Only the runtime mutates durable graph state, and only through the narrow algebra below.

Rewrite algebra

The algebra is intentionally narrow. Two constructors cover the highest-value dynamic patterns; additional forms are deferred until a real task requires them.

data GraphRewrite
  = ExpandNode   NodeId ExpansionMode SubgraphSpec
  | AppendAfter  NodeId SubgraphSpec

data ExpansionMode
  = ExpandReplaceNode
  | ExpandRetainNodeAsEnvelope

ExpandNode replaces a node with a subgraph — a planner turns a single step into a repair or evidence-gathering branch. AppendAfter inserts a subgraph downstream of a node — a reviewer queues validation once the anchor finishes. InsertBefore, PruneSubgraph, AddJoin, and ReplaceNode are recognized future forms but not part of the admitted alphabet.

Those constructors are the current runtime alphabet, not the full conceptual vocabulary. Cortex keeps the boundary laws explicit:

The conditional row names the resource law, not a separate v1 GraphRewrite constructor. The compiler-side vocabulary may call the restricted capability SelectActualize owner selectedArm, but the current runtime persists ordinary admitted rewrite rows for the selected branch.

A SubgraphSpec is a self-contained fragment: local topology, stage definitions for every local node, explicit entry nodes where inbound edges attach, explicit exit nodes where outbound edges continue. Entry and exit declarations are serialized lists but semantically sets, so duplicates are invalid. Validation rejects duplicate entry/exit nodes, missing definitions, orphan nodes, definitions outside the fragment, and any cycle in the resulting materialized graph. New nodes receive deterministic ids namespaced by their parent (planner:repair_branch_1:step_1), keeping identity stable across replay. Local inserted node ids cannot contain :, and the namespaced ids must be fresh against the current topology so namespace mapping cannot silently merge nodes.

Stages signal rewrites via a richer outcome:

data StageResult
  = StageComplete Aeson.Value
  | StageSuspend  SignalName
  | StageRewrite  Aeson.Value GraphRewrite

StageRewrite carries both the node’s durable output and the proposed edit; retained or appended subgraphs insert entry nodes that depend on that output, so a rewrite is “output and rewrite,” not “output or rewrite.” See Paper 3 for the formal substitution treatment.

Gas accounting

Gas is a structural-change budget, structural only; semantic weighting (latency, cost class, effect class) is deferred. The five dimensions:

data RewriteBudget = RewriteBudget
  { rbAddedNodesMax    :: Natural  -- nodes added
  , rbAddedEdgesMax    :: Natural  -- edges added
  , rbAddedDepthMax    :: Natural  -- depth added below any anchor
  , rbFrontierDeltaMax :: Natural  -- peak frontier breadth delta
  , rbRewriteOpsMax    :: Natural  -- admitted rewrite operations
  }

Each admitted rewrite consumes a natural-valued RewriteCost computed statically from its SubgraphSpec; admission draws only against remaining budget. Negative serialized values are invalid before admission. Runaway rewrite elaboration becomes a runtime impossibility rather than an executor-discipline problem. Gas is visible in run history: operators can inspect remaining budget, each rewrite’s cost, and the rewrite that exhausted a dimension.

Latent branches use selected-cost accounting in the current runtime. A compiled branch family is validated as a closed set of possibilities, but unselected arms do not prepay or consume runtime rewrite budget. The selected arm consumes ordinary rewrite budget when it is actualized. This is deliberately weaker than a reserved-capacity policy: Cortex does not yet guarantee that every compiled latent arm can still materialize after unrelated rewrites have spent the remaining budget.

Admission policy

Admission is the runtime’s gate. A proposal is admitted only when every check passes:

1. Vocabulary bounds. Every node instance references a registered executor; every port contract is a registered ContractId. No executors or contracts outside the closed alphabet.
2. Endpoint compatibility. Every new edge connects ports whose contracts are compatible under the port-semantic rules of Chapter 05. Authored inputs are cardinality-one; any aggregation must be represented by explicit transformation nodes.
3. Topology validity. The post-application materialized graph remains a DAG. The anchor exists in the current topology and definition map, and the current definition domain exactly covers the current topology. Entry/exit sets are non-empty and duplicate-free where the rewrite form requires them. Local inserted node ids are delimiter-free, and their namespaced ids are fresh. Definition-domain updates follow the anchor disposition: replacement deletes the anchor definition before overlaying inserted definitions; retention and append keep the old domain and overlay inserted definitions. No orphans, no dangling references.
4. Resource bounds. Estimated RewriteCost fits within the remaining budget on every dimension.
5. Runtime policy. The anchor, the run, and the task type permit rewrites of this form. Planner nodes may be restricted to a subset of the algebra.

A proposal that fails any check is rejected with a structured reason (invalid_rewrite, rewrite_budget_exceeded, vocabulary_violation, cycle_introduced, …). Default policy is fail-fast: the node and run fail with a legible error. Task-specific fallback modes — structured-output-only continuation, operator escalation — are deferred.

Admission is deterministic per frontier wave. Multiple frontier nodes may emit proposals in the same wave. The runtime serializes admission through a shared admission gate and shared remaining budget, persists admitted rewrite rows individually with monotone rewrite ids, and materializes admitted rows in rewrite-id order after frontier classification. This is deterministic ordered admission, not a proof that same-wave rewrites commute or can be treated as one concurrent semantic step. See Chapter 06 for scheduler-loop placement and blocked-graph diagnostics.

This boundary is architectural, not just procedural. Within one materialized topology, Pulse can reduce node-local facts concurrently over the current frontier. Rewrite admission is different: it is the coordinated phase where topology-changing proposals are checked against the ambient graph, the remaining budget, and the other proposals in flight. The phase boundary therefore separates coordination-friendly fact reduction from coordinated topology change.

The proof contract leads the implementation. The runtime admission path must construct the same natural budget vectors, duplicate-free entry/exit sets, topology-diff facts, and definition-domain update shape used by the mechanized rewrite model, or reject the proposal before materialization.

Materialization

Admission and application are separate events with crash-safety obligations between them. The normative durability contract:

• The rewrite log is append-only. Each entry carries the accepted rewrite specification, the anchor’s output needed to replay into inserted entry nodes, the static cost, and a monotone rewrite id.
• The graph state carries the watermark (highest rewrite id materialized) and the remaining budget. Materialization applies node-state changes, budget consumption, and watermark advance in one atomic commit.
• Admitted lineage may exist beyond the watermark. That means “admitted but not yet applied to the materialized graph”, not “applied and omitted”.
• Resume reconstructs the materialized graph only through the watermark. If lineage exists beyond it, resume deterministically finishes materialization before any scheduling decision.

The watermark makes crash recovery explicit at the rewrite boundary: without it, raw lineage replay cannot distinguish “persisted but not yet applied” from “applied and reflected.” Watermark-based materialization requires a Runtime/checkpoint version bump; pre-watermark rewrite-capable runs are legacy and not guaranteed resumable.

Hydration of rewritten stages is keyed by stage-template identity (durable executable identity) and verified against stage-action identity, not by scanning ad-hoc stage ids. Duplicate template ids in a materialized plan are rejected unless they map to the same action and identical policy metadata. See the rewrite materialization and recovery plan for the formal treatment of the materialization boundary and recovery invariants.

For selected branches, recovery replays the same admitted selected rewrite from durable state. It does not materialize unselected alternatives and does not invent a separate “discard branch” event. If branch selection occurred but materialization did not finish, resume must finish the admitted selected branch before scheduling against the new topology.

Provenance of rewrite events

This chapter covers provenance of structural events; provenance of values flowing through edges belongs to Chapter 08.

Every material graph evolution event is explainable after the fact. For each rewrite the runtime persists: the proposing node id and stage result, the raw GraphRewrite proposal, the admission decision (admitted, or rejected-with-reason), the cost and post-admission remaining budget, the structural diff applied, and any operator override. Rejected rewrites are not silently discarded — rejection rows are part of the audit trail. Operator surfaces expose the current materialized graph, rewrite history per run, and any blocked or waiting reasons introduced by rewrites.

Boundaries and invariants

This layer enforces:

• stages and planners propose; only the runtime admits.
• rewrites stay inside the closed executor alphabet, contract registry, endpoint compatibility, DAG validity, and the five-dimensional gas budget.
• conceptual boundary laws stay distinct even when v1 realizes them through the same runtime constructor. Substitution, append continuation, and branch actualization consume different boundary resources.
• same-wave rewrite proposals are admitted in deterministic order against shared remaining budget; ordinary node execution across the frontier is still concurrent.
• latent branch actualization follows selected-cost semantics: only the selected branch spends rewrite budget and becomes live; unselected branches remain sealed alternatives for the artifact.
• the rewrite log is append-only, and watermark and remaining budget update atomically with the node-state changes they imply.
• static DAGs and linear stage paths remain valid programs — a run with no rewrites is a degenerate case, not a special mode.

It delegates graph algebra to Chapter 04, scheduling and checkpointing to Chapter 06, value-envelope provenance to Chapter 08, and Wire grammar and configured-executor rules to Chapter 05.

Extensibility

New rewrite forms enter by adding constructors to GraphRewrite and extending the validator — not by letting stages emit arbitrary edits. InsertBefore, PruneSubgraph, AddJoin, and ReplaceNode lie along this path. New latent structural control operators are separate: each needs its own boundary law, actualization authority, budget policy, recovery story, and theorem target before it can lower into ordinary rewrite materialization. Richer gas dimensions (semantic weighting, effect classes, irreversibility boundaries) enter by extending RewriteBudget and the static cost estimator with a matching durability migration. Hierarchical subgraphs — composite nodes owning nested budgets — are the planned composition extension once the flat algebra has been proven on a real task. Planner integration proceeds by registering planner-capable nodes with a policy-gated, budget-aware contract, not by loosening admission checks.

Related

• ./03-formalism-stack.md, ./04-graph-and-circuit.md, ./05-wire-language.md, ./06-pulse-runtime.md, ./08-artifacts-and-provenance.md
• ../Reference/terminology.md — normative vocabulary.
• ../Reference/rewrites.md — normative rewrite algebra and boundary laws.
• ../Reference/Wire/conditionality.md — select(...), guarded-affine collapse, and selected-cost branch actualization.
• ../ADRs/0034-wire-pure-select-actualization-authority.md — pure selectors and restricted actualization authority.
• ../Roadmap/Plans/rewrite-materialization-and-recovery.md, ../Publications/Paper-3-graph-substitution-semantics/manuscript.md — formal treatment.