claude
8688a60ded
The single-file ledger had grown to 2968 lines / ~42k tokens, mixing current design law with accreted history: 59 cycle-stamped realization blocks, 18 [HISTORY] passages, 22 supersession markers, and the C10 / C22 / C24 reframe sagas layered several supersessions deep. A code-grounding audit (31 agents, adversarially verified) confirmed 11 defects stated as current truth: stale crate homes from the C28 #288 roster split (cost nodes, PositionManagement, PositionEvent, Session), the renamed InputSpec->PortSpec, the pre-#241 project model in C16 and the open-threads section, a stale HarnessKind retirement deferral in C24, and three C28-internal inconsistencies. New shape, per the ailang precedent: - INDEX.md stays the sole addressable entry point: foundation, external components, a C-id-keyed contract map (one line per contract), and only the genuinely open architectural threads. - contracts/cNN-<slug>.md carries each contract's current truth only: Guarantee / Forbids / Why with ratified refinements integrated, plus a code-anchored Current state. All confirmed defects are fixed here; crate anchors were re-verified against the tree. - contracts/cNN-<slug>.history.md (18 sidecars) and INDEX.history.md preserve every superseded block verbatim, stamps and issue refs intact, under a frozen-record banner. Nothing was deleted: superseded design intent remains an addressable working-tree artifact, off the per-cycle audit walk. - Ledger discipline is now stated in INDEX.md: live files are edited in place at cycle close, superseded text moves verbatim to the sidecar, and a supersession marker in a live file is itself an audit finding. Every contract file was verified against its old text by an independent zero-loss pass (statement-by-statement) plus a code-accuracy spot check; C-ids and contract titles are unchanged, so existing C-id citations in code, tests, and issues resolve as before.
78 lines
5.2 KiB
Markdown
78 lines
5.2 KiB
Markdown
# C23 — Graph compilation and behaviour-preserving optimisation
|
|
|
|
**Guarantee.** The bootstrap (C19) is a **compilation**: it lowers a param-generic,
|
|
named **blueprint** (the authoring source — nodes, composites, strategy, harness;
|
|
C8/C9/C20) into a flat, type-erased **`FlatGraph`** — the frozen runnable instance
|
|
(C7) — **wired by raw index, not by name** (`Edge { from, to, slot, from_field }`).
|
|
Composites are **inlined** at this step (C9): the composite *boundary* dissolves
|
|
entirely (there is no composite in the flat graph). The blueprint's field /
|
|
input-role *names* are **non-load-bearing** — the wiring resolves by index, and names
|
|
survive at most as **informative debug symbols** (exactly as `FieldSpec.name` already
|
|
is, C8), kept for tracing / rendering (C9 graph-as-data) but carrying no run
|
|
semantics. The flat graph is then the target of **behaviour-preserving optimisation**
|
|
— any transform that leaves every observable sink trace bit-identical (C1 is the
|
|
correctness invariant) — on two levels:
|
|
|
|
- **intra-graph** (within one graph): **common-subexpression elimination** — two
|
|
identical nodes (same type, same bound params, same input source) merge to one with
|
|
output fan-out, so fractal composition (C9) costs no redundant compute — and
|
|
**dead-node elimination** — a node on no path to a sink is dropped. Pure-consumer
|
|
sinks (C8, no output) are never CSE candidates, so their out-of-graph side effects
|
|
are preserved by construction.
|
|
- **across the sweep family** (over the family of flat graphs one blueprint yields
|
|
under a param sweep, C12): the sub-graph whose nodes carry **no swept param** and
|
|
whose inputs are **all sweep-invariant** (transitively from the sources — same data
|
|
window) is **loop-invariant** w.r.t. the sweep and is computed **once**; its output
|
|
is materialised as a recorded stream (C11) shared read-only across the sweep
|
|
instances (`Arc<[T]>`, C12). Only the parameter-dependent suffix re-runs per sweep
|
|
point — loop-invariant code motion over the sweep loop.
|
|
|
|
The compilation also carries one structural gate that **is** load-bearing:
|
|
**param-namespace injectivity**. `check_param_namespace_injective` runs over the
|
|
`param_space()` name projection before name resolution, reads the **boundary** name
|
|
projection — the by-name authoring address space — and rejects a duplicated path
|
|
(`CompileError::DuplicateParamPath`). This makes the authoring address space
|
|
injective **without** making names load-bearing in the flat graph: node names qualify
|
|
the param path at construction and are dropped at lowering (the flat graph stays
|
|
wired by raw index).
|
|
|
|
**Forbids.** Any "optimisation" that changes an observable trace (it breaks C1);
|
|
optimising over a representation that is not graph-as-data — an opaque trait-object
|
|
interior (the rejected nested-composite reading of C9) cannot be analysed or
|
|
rewritten across its boundary, so it forecloses both levels.
|
|
|
|
**Why.** Determinism (C1) is not merely an audit property; it is the **licence** for
|
|
these rewrites — a behaviour-preserving transform is only meaningful because "same
|
|
input → bit-identical run" makes "same result" decidable, and a sweep-invariant
|
|
sub-graph is reproducible enough to compute once and share. The flat graph
|
|
representation (C19) is the necessary condition: only a flat, inspectable
|
|
graph-as-data — with each node's declared param-ranges (C8) — lets the compiler
|
|
identify identical sub-expressions, dead nodes, and the sweep-invariant frontier.
|
|
This is precisely why a composite is an inlining (C9) and not a runtime sub-engine:
|
|
the flat graph is what makes the whole graph optimisable.
|
|
|
|
## Current state
|
|
|
|
The flat-graph **representation** — blueprint → inline / compile → flat instance — is
|
|
the load-bearing substrate, built **first**, and is realized: `Composite::compile`
|
|
emits the first-class `FlatGraph` (C19). The per-node param declarations the
|
|
sweep-level pass presupposes carry `name` + `kind` (C8); the swept *range* is still
|
|
pending (#32/C20), as is the sweep orchestration itself (C12/C21).
|
|
|
|
The **optimisation passes** — intra-graph CSE/DCE and sweep-invariant hoisting — are
|
|
**deferred, behaviour-preserving follow-on work**; no pass exists yet
|
|
(`Composite::compile` in `crates/aura-engine/src/blueprint.rs` adds none). Each is
|
|
gated by a "flat graph with pass ≡ flat graph without pass, bit-identical run" test
|
|
(C1). The one compilation-time structural check that is **live** today is the
|
|
param-namespace injectivity gate above — `check_param_namespace_injective`, defined in
|
|
`crates/aura-engine/src/blueprint.rs` and applied at that file's own compile entry
|
|
points (`compile`, `compile_with_params`, and the `bind` paths) as well as from
|
|
`construction.rs`'s `finish`, raising `CompileError::DuplicateParamPath`.
|
|
|
|
## See also
|
|
- [C1](c01-determinism.md) — the bit-identity correctness invariant that licences every rewrite.
|
|
- [C8](c08-node-contract.md) — `FieldSpec.name` as the non-load-bearing precedent and the per-node param declarations.
|
|
- [C9](c09-fractal-composition.md) — inlining vs runtime sub-engine.
|
|
- [C11](c11-sources-record-replay.md), [C12](c12-atomic-sim-unit.md) — recorded-stream sharing and the sweep family.
|
|
- [C19](c19-bootstrap.md) — the flat-graph representation this optimises.
|