ADR 0032 - Wire Boundary Contracts as Planning Resources

Treats Wire boundary contracts, not nodes themselves, as the local resources that rewrites, conditionals, and planning certificates must account for.

On this page
  1. Status
  2. Context
  3. Decision
  4. Consequences
  5. Positive
  6. Negative
  7. Obligations
  8. Semantic and Proof Obligations
  9. Documentation Obligations After Acceptance
  10. Alternatives considered
  11. Related

ADR 0032 - Wire Boundary Contracts as Planning Resources

Status

Proposed - establishes the resource vocabulary used by the follow-up Wire rewrite and conditionality ADRs.

Context

Wire already has strong global admission checks: rewrite proposals must fit the remaining budget, stay inside the registered executor and contract vocabulary, preserve topology validity, and materialize through the durable rewrite log. Lean also models proof-carrying rewrite chains whose per-step certificates lift to chain-level preservation.

Those mechanisms still leave an important semantic distinction implicit. A node is both an addressable runtime/provenance object and a boundary of port contracts. Rewrites and conditionals do not always consume the node as an object. A retained conditional owner stays visible for lineage, and an append continuation keeps the anchor computation in place. What must be accounted for locally is the boundary contract that the operation consumes, forwards, or transforms.

Treating the node itself as the linear resource is therefore too coarse. Treating only global predicates as the accounting surface is too diffuse. Wire needs a local vocabulary for the resources that graph operations spend and return.

Decision

Wire should treat boundary contracts as first-class planning resources. A rewrite, conditional selection, or planner certificate consumes or transforms a boundary obligation and must provide a witness for how the resulting graph satisfies the exposed contract.

The resource vocabulary is:

ResourceMeaningMode
Boundary obligationThe input/output contract boundary exposed by a node or graph expression.Linear unless explicitly guarded or optional.
Rewrite slotExclusive authority to transform a boundary at an anchor in one planning epoch.Linear.
Port obligationA concrete labeled input or output obligation within a boundary.Linear, affine, or graded according to port cardinality.
Branch-local obligationA boundary obligation inside a not-yet-selected conditional branch.Guarded affine.
Rewrite budgetThe natural-vector budget consumed by admitted structural change.Graded.
Namespace freshnessAuthority to allocate deterministic names under an anchor or namespace.Ghost planning resource.
Registry/contract witnessEvidence that introduced nodes stay within the registered boundary.Ghost proof resource.

This is a semantic layer over the existing graph algebra. Mokhov overlay and connect still describe the denotation of graph expressions. Boundary resources describe whether a graph operation is locally well-accounted before it is admitted or proved safe.

Consequences

Positive

  • Separates node identity from the contract obligation carried by the node boundary.
  • Gives later ADRs precise language for replacement, append, retained envelopes, and conditionals.
  • Makes it possible to state local no-double-spend and port-coverage obligations without relying only on global topology checks.
  • Matches the existing rewrite-budget model by treating budget as a graded resource rather than a boolean permission.

Negative

  • Adds another semantic layer that authors and implementers must keep distinct from graph equality.
  • Requires care around cardinality: not every port-like thing is exactly-once linear.
  • Does not by itself prove Haskell runtime correspondence or Lean-side construction witnesses.

Obligations

Semantic and Proof Obligations

  • Future rewrite and conditional specs should say which boundary obligation they consume and which boundary they produce.
  • Lean models should prefer resource-context predicates over ad hoc per-node token language.
  • Lean theorem target: resource-consumption faithfulness, stating that a valid operation consumes exactly the declared boundary resources.
  • Lean theorem target: per-epoch rewrite-slot uniqueness, stating that a rewrite slot is spent at most once in a planning epoch.
  • Lean theorem target: boundary preservation, stating that a valid operation preserves the exposed boundary promised by the operation.
  • ADR 0038 tracks the concrete theorem names and implementation issues for these proof targets.
  • Runtime prose should avoid claiming that nodes are linear resources. The stricter claim is that boundary obligations are locally accounted resources.
  • ADR 0039 places copy, move, and seal accounting in node egress obligations and port-resource rules. It does not permit programmable edge-local transformations.

Documentation Obligations After Acceptance

  • After acceptance, architecture chapters 03, 05, and 07 should introduce the boundary-resource vocabulary and cite this ADR stack.

Alternatives considered

  • Nodes as linear tokens - rejected as the canonical model because retained owners, append continuations, and provenance envelopes can keep node identity while transforming boundary obligations.
  • Global predicates only - rejected because global admission checks are necessary but do not express local resource consumption, guarded branch discard, or no-double-rewrite discipline.
  • Runtime leases only - rejected because leases can protect implementation state but do not state the source-language or proof-side contract semantics.