Wire Reference — Pure Execution

Wire pure execution is the deterministic, authority-free calculation layer inside Wire. Authors use it for JSON-shaped transformations over upstream Wire values, not for model calls, tools, durable state, artifact writes, or host callbacks.

The source form is:

let acceptedItem = item: item.score >= 0.7;

node classify
  <- evidence: EvidenceSet;
  -> accepted: AcceptedSet = evidence.items |> filter acceptedItem;
  -> rejected: RejectedSet = evidence.items |> filter (item: !(acceptedItem item));

CorePure output equations are not @ executor applications. Authored @pure { ... } and retired pure (...) wrappers are rejected. The compiler lowers CorePure output equations to an internal native pure task because Pulse executes materialized tasks, but that lowering is not source-level authority.

Rule Sources

• §5.3 Pure Output Equations - authored pure node syntax, local bindings, output equation rules, and CorePure surface.
• §8 CorePure Expressions - compact expression grammar.
• Executors and the Alphabet - relationship between CorePure and the internal native pure evaluator.
• ADR 0020 - design decision and proof obligations.
• ADR 0050 - removal of the source-level pure (...) wrapper and the static/runtime residue split.
• ADR 0031 - node-local where <record-expr> ; binding surface.

Syntax

A pure node uses the clause form from the Wire grammar:

node <name>
  (<- <input-name> : <Contract>;)*
  (-> <output-name> : <Contract> = <corepure-expr>;)+
  (where <corepure-record-expr>;)?

A pure output equation declares one output port and its value:

-> label: Contract = <corepure_expr>;

The output label is the Wire routing label. The expression result is implicit; there is no return, no pure wrapper, and no separate map from result names to ports in source.

Rules:

• Only input ports may appear before pure output equations.
• The optional trailing where <record-expr> ; clause opens its record fields into all output equations.
• The where field set must be statically determinable: record literals, let ... in { ... }, references to let-bound records, and // merges of those shapes are admitted. Dynamic record shapes are rejected at admission.
• Each pure output equation declares exactly one output port.
• Sum-grouped outputs are not pure equation syntax.
• A pure node must declare at least one output equation.
• The equation set must match the declared output ports exactly.
• Dynamic loops, host scripts, JIT languages, model calls, tools, and IO belong behind @ executors, not inside CorePure.

Top-level delayed helpers are written as ordinary module let bindings whose right-hand side is a CorePure helper expression:

let acceptedItem = item: item.score >= 0.7;
let scoreThreshold = 0.7;

Module let is phase-neutral syntax. acceptedItem is a delayed CorePure helper function. scoreThreshold is an ordinary compile-time scalar, but because it is authority-free pure data, the compiler captures it into later delayed CorePure evaluation as a constant. Configured executor values and graph values are not capturable into CorePure.

Lowering

The compiler lowers one source pure node to one internal native pure task. It does not lower one task per output.

The internal task config has this shape:

{
  "bindings": ["<top-level delayed binding or captured constant AST>"],
  "where": "<optional node-local CorePure record expression AST>",
  "outputs": {
    "accepted": "<CorePure accepted expression AST>",
    "rejected": "<CorePure rejected expression AST>"
  }
}

Top-level bindings and the node-local where record are distinct scopes:

• top-level delayed helpers and captured pure-data constants are evaluated after builtins and input variables are installed;
• the where record is evaluated after top-level delayed bindings and captured constants;
• fields from the where record are opened into the output-evaluation environment;
• where fields may shadow top-level delayed bindings and captured constants;
• where fields may not collide with input port names;
• duplicate binding names are rejected within one scope;
• lambda parameter names must be unique within one lambda.

The internal task metadata records the native pure evaluator, but Wire source never names it with @.

The implemented config schema admits only bindings, where, and outputs. There is no source-authored CorePure budget field. where is omitted when the source node has no where-clause.

Input Binding

CorePure evaluates over JSON WireValue payloads.

Input binding rules:

• Every pure input must accept exactly one contract.
• Every pure input is cardinality-one; list-input aggregation is not part of the authored syntax.
• Repeated same-contract inputs must be explicitly labeled.
• A single unlabeled input is available as the variable in.
• Labeled inputs become variables with the same label.
• Input WireValues must have payload kind json.

For example:

node score
  <- evidence: EvidenceSet;
  <- weights: WeightSet;
  -> score: ScoreSet = {
    total = sum (zipWith (s: w: s * w) evidence.scores weights.values);
  };

Here evidence and weights are CorePure variables containing the JSON payload values from the matching input ports.

Output Binding

Each output equation key in the lowered config is the declared output port name:

• -> accepted: AcceptedSet = accepted writes the accepted output.
• every output equation writes the declared output label with the same name in the lowered config.

CorePure produces JSON values. Runtime wrapping then validates and wraps each value through the declared Wire output contract. In practice, pure outputs should target contracts whose payload kind accepts JSON values.

Evaluation is all-or-nothing for the node: either every declared output is produced, or the pure task fails with a typed evaluator error.

In the node boundary normal form from ADR 0039, pure output equations are the visible egress adapter from the node-local CorePure environment to the declared output port environment.

CorePure Expressions

CorePure is a small Nix-like expression language over JSON values. It is not Nix, Haskell, or a host callback surface.

Implemented expression forms:

• literals: strings, numbers, booleans, null;
• lists and records;
• variables;
• field access: item.score;
• array/object indexing: items[0], record["field"];
• lambdas: item: item.score, score: weight: score * weight;
• function application: map f xs, zipWith f xs ys;
• partial application and pipes: items |> filter acceptedItem |> map scoreOf;
• unary ! and -;
• arithmetic +, -, *, /;
• comparisons ==, !=, <, <=, >, >=;
• boolean &&, ||;
• right-biased record merge //;
• non-recursive let ... in;
• if ... then ... else ...;
• string interpolation: "Score: ${item.score}".

/ uses finite Float64 division over numeric values. It never constructs an exact rational or Scientific quotient, so quotients such as 1 / 3 round to a finite float instead of forcing non-terminating decimal construction.

Disallowed:

• @ executor applications;
• IO, time, randomness, model calls, tool calls, memory queries, durable-state reads, or host callbacks;
• loops, recursion, fix, imports, paths, modules, or package access;
• exceptions other than typed deterministic evaluator errors.

Builtins

The implemented builtin environment is closed:

Every builtin is ordinary CorePure function application. Builtins do not receive host authority. Functions intended for pipe use are data-last.

Failure Surface

Pure execution fails deterministically. The evaluator reports typed failures, including:

• missing variables;
• division by zero;
• non-finite float division;
• unsupported pure input ports;
• repeated same-contract input ports without explicit labels;
• missing or ambiguous input values;
• non-JSON input payloads;
• output equations that do not match declared output ports;
• type mismatches;
• missing fields;
• out-of-bounds array indexes;
• calling a non-function;
• function arity mismatches;
• duplicate binding names within one scope;
• duplicate lambda parameters;
• invalid JSON passed to fromJson;
• where expressions that do not evaluate to records.

These failures are runtime pure-task failures after the graph has been admitted. Source and binding checks catch malformed pure tasks where possible, such as authored @pure, duplicate top-level names, unsupported pure ports, output port mismatch, where field/input-port collisions, and where-expressions whose field set is not statically determinable.

Benchmarking

The repository includes an opt-in Criterion benchmark for the implemented pure evaluator:

just bench-pure-wire

The benchmark is a scaffolding surface, not a normative language rule. It compares descriptive CorePure workloads, such as weighted scoring, eligibility filtering, risk adjustment, and label rollup, against direct Haskell implementations over the same pre-built JSON values. The Wire case does not parse JSON text inside the benchmark loop, but it does traverse JSON-shaped Aeson.Values through the CorePure interpreter. Ordinary benchmark runs print a compact Wire/Haskell comparison summary to stdout before Criterion’s detailed rows.

Hosts that repeatedly evaluate the same lowered pure task may prepare it once and then evaluate the prepared task against different input bundles. Preparation performs the static task checks; prepared evaluation still binds and validates runtime Wire inputs. The evaluator may use semantics-preserving fast paths for common collection closures, such as field projection and simple numeric zipWith, but those paths must preserve the same JSON output equality and pure error taxonomy as generic CorePure evaluation.

Boundary With Proofs

CorePure stays inside Wire’s deterministic expression layer. It preserves the executor authority boundary because the author cannot use it to name host capabilities or perform effects.

The proof-facing obligation is the lowering step:

• a source pure node lowers deterministically to one native pure task;
• the lowered output keys are exactly the declared Wire output ports;
• top-level delayed bindings, captured constants, and node-local where fields remain distinct scopes;
• evaluation depends only on input JSON values, closed builtins, and the CorePure AST;
• the result is wrapped through the declared Wire output contracts.

This keeps pure execution compatible with the theorem-side model while still giving authors a legible expression surface.