ADR 0035 - Wire Rewrite Algebra Forms

Separates conceptual boundary laws from their current Wire rewrite runtime realizations.

On this page
  1. Status
  2. Context
  3. Decision
  4. Consequences
  5. Positive
  6. Negative
  7. Obligations
  8. Alternatives considered
  9. Related

ADR 0035 - Wire Rewrite Algebra Forms

Status

Proposed - clarifies the conceptual rewrite taxonomy before further runtime or Lean changes.

Context

The rewrite reference currently exposes forms such as ExpandNode and AppendAfter. The current conditional runtime realizes selected latent branches through retained-anchor AppendAfter, which is operationally useful because the condition owner remains visible for lineage and the selected fragment materializes behind it.

That operational shape should not become the general mental model for expansion. If a rewrite claims to replace a node, the replacement graph must satisfy the original boundary contract of the node. Appending work after the node is sequencing, not substitution. The distinction matters for port obligations, provenance, and future Lean statements.

Decision

Wire should distinguish conceptual boundary laws from current runtime constructors.

The conceptual boundary laws are:

Conceptual boundary lawResource useContract effect
Contract-preserving substitutionConsumes one rewrite slot at the anchor and consumes the anchor boundary.The replacement graph must expose the consumed anchor boundary.
Append continuationConsumes one rewrite slot at the anchor while retaining the anchor node.The anchor satisfies its own output; the continuation consumes that output and produces a new downstream boundary.
Conditional branch actualizationConsumes one owner-bound actualization capability and the owner’s rewrite slot.The selected branch consumes its variant boundary and yields the common downstream boundary, realizing the guarded-affine collapse from ADR 0033.
Observation/instrumentationNo v1 resource path; a future form would need to consume an anchor slot.Observers must not consume or alter the anchor’s required boundary.

The current runtime realization is:

Boundary lawCurrent realizationNotes
Contract-preserving substitutionExpandNode anchor mode specv1 GraphRewrite constructor.
Append continuationAppendAfter anchor specv1 GraphRewrite constructor.
Conditional branch actualizationAppendAfter owner selectedFragmentCurrent retained-owner conditional lowering realizes the selected branch with ordinary rewrite machinery. SelectActualize owner selectedArm names the restricted capability from ADR 0034; it is not a v1 GraphRewrite constructor.
Observation/instrumentationNonePotential future boundary law only. It is not admitted by v1 and is not added by this ADR.

The conditional row names target resource semantics. In the current v1 realization, there is one ordinary AppendAfter admission; the owner-bound actualization capability is not a separately persisted runtime token.

AppendAfter remains a valid operational mechanism for the current retained-owner conditional implementation. It should not be described as the canonical semantics of node expansion. Expansion is substitution into an anchor boundary; conditional branch actualization is retained-owner branch collapse. Both can preserve provenance, but they preserve it through different laws.

ADR 0037 separates this conditional actualization law from the broader graph-denotation layer: latent branch families are not plain Mokhov graphs before resolution, even when the selected result lowers to ordinary graph composition.

Consequences

Positive

  • Prevents replacement and sequencing from being conflated.
  • Makes the original port contract of an expanded node explicit.
  • Lets the current conditional implementation keep using retained anchors without claiming that all rewrites are append-style.
  • Gives proof work clearer theorem targets for substitution, continuation, and selection.

Negative

  • May require renaming or documentation around existing constructors whose operational names are broader than their conceptual role.
  • Introduces more cases for admission docs and future mechanization.
  • Names observation/instrumentation only as a deferred boundary law, so any future implementation still needs a separate ADR and runtime-version bump.
  • Does not by itself change the current runtime representation.

Obligations

  • Rewrite docs should state which rewrite concept each runtime constructor realizes.
  • Rewrite docs should state which rewrite slot each admitted constructor spends.
  • Future constructors should be added only when they correspond to a distinct boundary law.
  • Observation/instrumentation must remain non-admitted until a follow-up ADR introduces a concrete constructor and admission rules.
  • Conditional lowering docs should treat retained-anchor AppendAfter as the current realization of branch actualization, not as the semantic definition of all conditionals.
  • Lean theorem targets: boundary preservation under substitution, append-continuation boundary preservation, and selection realization of guarded-affine collapse. Observation has no theorem target until a concrete constructor exists.
  • ADR 0038 tracks the concrete theorem names and implementation issues for these proof targets.

Alternatives considered

  • Use append as the universal rewrite model - rejected because replacement must discharge the original anchor boundary rather than merely run after the anchor.
  • Use substitution as the universal rewrite model - rejected because append continuations, observers, and retained conditional owners are legitimate non-substitutional graph operations.
  • Keep provenance only in side tables and erase retained owners - rejected because current operator and recovery surfaces benefit from lineage being visible in the graph evolution story.