ADR 0021 - Wire Source Elaborates to Circuits

Makes circuits the single semantic target for Wire source and relocates CorePure into the elaboration phase.

On this page
  1. Status
  2. Context
  3. Decision
  4. Maximal Static Reduction
  5. Static Graph Boundary
  6. Runtime Residue
  7. Follow-On Composition Decision
  8. Alternatives considered
  9. Consequences
  10. Positive
  11. Negative
  12. Obligations
  13. Implementation sequence
  14. Related

ADR 0021 - Wire Source Elaborates to Circuits

Status

Proposed - this ADR scopes the next Wire phase after pure output equations. If accepted, it supersedes ADR 0020’s decision to defer full Wire-to-circuit unification.

Context

ADR 0020 made pure output equations legible, but it still treats CorePure mostly as the language inside pure (...). That keeps the first implementation narrow, but Wire still has two nearby authoring concepts:

  • topology expressions that produce circuits;
  • pure expressions that produce values inside a runtime pure executor.

The next phase should make that distinction semantic rather than syntactic. Authors should be able to write constants, pure helpers, node bodies, and eventually composition expressions in one Wire source language, while the compiler decides which parts can be reduced before runtime and which parts must remain as runtime executor vertices.

This must not weaken the graph guarantees from ADR 0005 and ADR 0009. Admission witnesses, predecessor hashes, and rewrite budgets must still attach to a fixed post-elaboration circuit, not to runtime-discovered topology.

Decision

Wire source should elaborate to circuits as its executable semantic target. Expressions in topology position denote circuits:

  • a literal denotes a constant circuit with no inputs and one typed output;
  • a node declaration denotes a circuit with declared input and output ports;
  • future composition expressions compose circuits at the topology layer.

File-level pure helpers remain CorePure value bindings. They do not denote standalone circuits at the binding site. Instead, they are inlined at each use site and either reduced during elaboration or embedded in runtime residue according to the dependencies at that use.

CorePure becomes an elaborator phase, not a separate language that exists only inside pure (...). The compiler uses one CorePure evaluator in two phases:

  • elaboration-time evaluation for expressions whose dependencies are statically known;
  • runtime pure execution for residue that depends on input port values.

The same evaluator semantics apply in both phases: deterministic results, typed errors, closed stdlib, and explicit budget accounting.

Maximal Static Reduction

The elaborator must reduce every sub-expression it can statically reduce. A binding is folded if and only if its right-hand side is statically reducible. There is no compiler discretion to leave a known pure value for runtime.

This rule keeps runtime budget a property of the source program rather than of implementation choice. A statically reducible expression that fails, such as a bad index or division by zero, fails during elaboration instead of being deferred.

For the first implementation, maximal static reduction is a compiler-discipline rule. A later proof-oriented slice should state it formally and connect it to budget conservation.

Static Graph Boundary

Topology elaboration completes before runtime evaluation begins. After elaboration, the executable circuit has a fixed vertex set:

  • constant outputs are baked into the circuit;
  • runtime executor vertices are explicit executor invocations;
  • predecessor hashes, rewrite admission witnesses, and budget annotations attach to the post-elaboration circuit.

Runtime pure execution may evaluate values, but it may not create new topology.

Runtime Residue

ADR 0050 resolves the runtime residue spelling: CorePure output expressions are written directly and are delayed only when they depend on input ports.

-> port: T = <corepure-expr>
-> port: T = @executor (<expr>)

The compiler still distinguishes internal native pure residue from registered executor authority: CorePure has no @; authority-bearing work uses @.

Follow-On Composition Decision

ADR 0028 resolves the file-level expression port-label and topology composition questions deferred by this ADR. File-level helpers such as let greeting = "Hello" remain CorePure value bindings, not circuits with anonymous or binding-named output ports. Topology composition uses the circuit operators defined there.

Alternatives considered

  • Keep CorePure only inside pure (...). Rejected for the next phase because it preserves an artificial split between ordinary Wire constants and pure runtime programs.
  • Defer unmarked runtime pure execution. Rejected by ADR 0050. Direct CorePure equations are now the source form; authority-bearing work remains explicit through @.
  • Allow runtime topology creation. Rejected because it would break the static graph property required by rewrite admission and predecessor hashing.

Consequences

Positive

  • Wire gets one semantic target: source elaborates to circuits.
  • Constant and helper expressions use the same evaluator as runtime pure expressions.
  • Static reduction becomes visible and testable rather than an implementation convenience.
  • Existing graph proofs can continue to quantify over the post-elaboration circuit.

Negative

  • The elaborator must distinguish static dependencies from input-dependent residue.
  • Compiler tests must assert maximal static reduction, not just final runtime behavior.
  • Some tempting authoring sugar remains deferred until the elaborator boundary is implemented.

Obligations

  • Implement Wire AST to circuit elaboration before runtime evaluation.
  • Reject statically known typed CorePure failures during elaboration.
  • Add tests that statically reducible bindings are folded.
  • Add tests that input-dependent residue becomes explicit runtime executor vertices.
  • Keep the runtime executor surface from creating topology.

Implementation sequence

The immediate implementation slice is:

  1. Parse the node and output grammar from ADR 0022.
  2. Implement the CorePure expression surface from ADR 0023.
  3. Elaborate Wire AST into a post-elaboration circuit, including maximal static reduction.
  4. Route runtime CorePure residue through the existing native pure executor path.
  5. Add the closed stdlib needed by the first pure examples.

Topology composition primitives are specified separately by ADR 0028 and can be implemented after the node/elaborator slice when multi-node examples require them.