ζ

ROADMAP.md

@@ -543,6 +543,40 @@ Three illegal-state boundaries dissolved, in order: the old `Bool + String?` adm
 
 Cleared (prior PR #521): `DerivedOpEffect { method, path_template, shape }` collapsed into `OperationEffect { operation_name, shape }`. The `method` / `path_template` fields were never consumed downstream — both the modifier check and obligation generator project through `shape` alone, and the `ReadEffect` variant already encodes "method was GET/HEAD/OPTIONS." `derive_op_effect` now returns `OperationEffect?` directly, so Stage 2b's `compose_effects` consumes the same shape derivation produces. Future diagnostic rendering that wants the originating method/path should attach a separate evidence carrier to the diagnostic, not smuggle transport facts onto the effect record.
 
+### Lane 2 Stage 2d — symbolic cost (✅ Shipped)
+
+**DB-7 symbolic-cost algebra and per-Behavior lens landed.** Authority: [`design-symbolic-cost-algebra.md`](docs/design-symbolic-cost-algebra.md). Three .dag files + a Rust mirror + acceptance tests:
+
+- `src/v3/std/algebra.dag` — `SymbolicCost` coproduct (7 variants: Constant / Linear / Polynomial / Product / Sum / Log / Unknown) with a stamped 4-pattern dissolution receipt, `SizeVariable { source_port }`, `sequential` / `iterate` / `max_path` composition, `normalize` (drop zero, single-term reduction, `Linear(v) * Linear(v) → Polynomial(v, 2)` collapse), `dominates` partial order.
+- `src/v3/std/dimensions.dag` — minimal `Dimension<Carrier>` + `Witness<Carrier>` types for Stage 2f's future generic walker. Full DB-3 abstraction (`analyze`, `DimensionReport`, bootstrap discovery) lands in 2f per its design doc's own sequencing.
+- `src/v3/lenses/cost.dag` — per-Behavior lowering: Value → Constant(0); Transform → sequential(1, Σ inputs); Branch → sequential(1, condition, max_path(arms)); Loop → iterate(LinearCost(source), body); Bind → passthrough. Forward-fold accumulator pattern mirrors `lenses/complexity.dag`; `MissingCost` short-circuits every composition wrapper so malformed references never silently substitute a zero leaf.
+- Rust mirror in `src/v3/compiler/src/dag.rs`: `SymbolicCost` / `SizeVariable` carriers and `sequential` / `iterate` / `max_path` / `normalize` / `dominates` functions — needed because `emit_rust_module`'s `is_bootstrap_file` filter excludes `src/v3/std/` declarations from Rust emission; same pattern `Behavior` / `LoopBound` use.
+- `src/v3/compiler/src/lens_cost_symbolic_generated.rs` via `regen_lens_cost_symbolic` binary. Exposed as `v3_compiler::lens_cost_symbolic::{symbolic_cost_of, SymbolicCostEntry, SymbolicCostLookup}`.
+- Acceptance fixture: `src/v3/compiler/tests/lane2_stage_2d_symbolic_cost_test.rs` (20 tests). Covers Value/Transform/Branch/Loop lowering; recursive-fn body-cost fact-flow (PR #537 briansrls/codex BLOCKING); zero-drop normalization; `Linear(v) * Linear(v) → Polynomial(v, 2)` nested-fold fingerprint; cross-variable product stays `Product`; composite-dominance child-walk (PR #537 codex P2); `max_path` three-way step preserving incomparable branches (PR #537 briansrls BLOCKING) with an order-independence pin; dominance partial order (Unknown / Linear / Log / Polynomial degree ordering); `max_path` dominant-selection; checked-in generated-module snapshot guard.
+
+**Loop cost for `LoopBound::Descent` clusters uses `LoopNode.source` as the size-variable carrier.** The cluster's `members: NonSingletonList<MemberDescent>` and `intra_cluster_calls` carry the descent witnesses needed for the termination proof (#519), but the loop's own `source` port is the runtime value being descended upon — which is the honest recursion-depth bound for both `Cardinality` and `Descent` bounds. Richer per-member analysis (distinguishing list-descent from bounded-integer descent so `Descent` clusters report `ConstantCost` for bounded-int descent instead of `LinearCost`) is a Stage 2d follow-up, flagged in DB-7 §"Recursion depth bounds".
+
+**Substrate gap flagged for 2f pre-work: `data symbolic_cost_dimension: Dimension<SymbolicCost> = { ... }` is DEFERRED to Stage 2f.** v3's surface grammar rejects record literals inside `data X: T = { ... }` bodies (DOWNSTREAM_REQUIREMENTS.md class-5 gap #3) and record / match / lambda inside `fn X { body }` block-bodied definitions simultaneously, which both shapes the `Dimension` record's field-carrying receipt pattern requires. The lens ships its behavior-variant lowering as the authority in the interim; Stage 2f materializes the `Dimension<SymbolicCost>` instance alongside the grammar extensions that unlock it. Rationale + authority: DB-7 §"Dimension<SymbolicCost> wiring" documents the target shape; cost.dag's closing comment block records the grammar-gap waypoint.
+
+**Build-script change (documented load-order fix).** `src/v3/compiler/build.rs` now prioritizes `list.dag` and `substrate.dag` ahead of alphabetical order within `STAGED_FILES`. Structural-recursion termination analysis walks a recursing argument back to its declared `Disj` connective via `structural_binding_info_for_variant`; the walk only succeeds after the declaring file has been phase-2 lowered, so std files that recursively descend over `List<T>` or `Behavior` variants (post-2d: `src/v3/std/algebra.dag` and `src/v3/lenses/cost.dag`) need their dependencies loaded first. Without the priority list, alphabetical order put `algebra.dag` and `dimensions.dag` ahead of `list.dag`/`substrate.dag`, and their recursive helpers failed termination against placeholder connectives. Same pattern the spec loader already uses to pin `v3_l1.dag` first.
+
+**Acceptance-test infra migration (documented side effect).** Pre-existing tests that queried `dag.nodes().iter().find_map(Behavior::as_transform)` etc. on the `compile_to_dag` output assumed the bootstrap Dag contributed no `Transform` / `Branch` / `Loop` / `Bind` nodes before the user's source lowered. Lane 2 Stage 2d invalidates that assumption — `src/v3/std/algebra.dag`'s lowered bodies contribute many nodes. Eleven tests across four files migrated to filter by `span.file` (or subtract a bootstrap baseline) so they pin the user-code count/shape rather than the global node list: m0_acceptance's `test_let_binding_produces_dag_shape` (1); m1_substrate_test's `m17_operator_lowers_to_structural_transform_target`, `m17_comparison_operator_lowers_to_structural_transform_target`, `m17_user_function_call_lowers_to_callable_target`, `m18_r15_match_on_aliased_sum_type_compiles`, `m18_r13_mutual_recursion_poisons_callers`, `mutual_recursion_planner_ignores_callable_parameter_shadowing` (6); m1_3_emit_rust_test's three reflected-harness fixtures `rustc_roundtrip_emitted_module_matches_reflected_behavior_payloads`, `rustc_roundtrip_emitted_module_compares_reflected_port_ids_in_list_contains`, `rustc_roundtrip_emitted_module_returns_user_record_list_from_reflected_binds` (3); emit_rust.rs lib test `render_field_project_constructs_owned_list_from_borrowed_nodes` (1). This is a general test-authoring hygiene rule for every future std-module consumer to consider — a dedicated walker in Lane 1e would emit typed span-filtered iterators and dissolve the hand-written `.filter(|t| t.span.file == ...)` idiom.
+
+**Follow-up — `ProductCost` / `SumCost` NSL lift (not blocking, post-normalize-≥2-invariant gates graduation).** `SymbolicCost::ProductCost(List<SymbolicCost>)` and `SymbolicCost::SumCost(List<SymbolicCost>)` admit `[]` and singleton inputs at construction time; `normalize` already reduces both back to scalar variants, so the post-normalize canonical shape has `len ≥ 2`. Lift the field type to `NonSingletonList<SymbolicCost>` (Track 9 vocabulary) so the `≥ 2 elements` fact becomes structural instead of a convention enforced only by `reduce_sum` / `reduce_product`. **Dissolution trigger:** the first call site that needs to pattern-match two guaranteed children without a `len() >= 2` check (likely a richer `normalize` variant or a multi-variable dominance rule). **Yellow-flag threshold: when a second normalization helper is added** — two such helpers is the moment the invariant becomes worth encoding at the type level.
+
+**Follow-up — `PolynomialCost.degree` typed carrier (not blocking, degree-arithmetic surface gates graduation).** `PolynomialCost { var, degree: Int }` — post-normalize, `degree >= 2` (degree = 1 collapses to `Linear`, degree = 0 to `Constant`). The raw `Int` admits 0, 1, and negatives; the domain constraint is behavioral, not structural. Replace with a typed carrier (`NonNegativeInt` at minimum; `DegreeAtLeastTwo` ideally). **Dissolution trigger:** DB-7's degree-arithmetic surface lands (multi-variable polynomial composition like `Polynomial(n, 2) * Polynomial(m, 3) = Polynomial<mixed>`), which needs numeric operations on `degree` and is the natural moment to introduce the typed carrier. **Yellow-flag threshold: 1 month** after the first degree-arithmetic fixture lands on the lens side.
+
+**Follow-up — `LinearCost(v)` vs `PolynomialCost(v, 1)` canonicalization (not blocking, normalization-step extension gates graduation).** The two variants encode the same asymptotic fact; `dominates` and `normalize` explicitly pattern-match on both (`payload.degree <= 1` in the Polynomial-vs-Linear arm). Representation duality (audit Q6). Pick one canonical form — either dissolve `LinearCost` into `PolynomialCost(_, 1)`, OR constrain `PolynomialCost.degree ≥ 2` so `Linear` is the sole degree-1 surface. **Dissolution trigger:** the same normalization extension that introduces the `DegreeAtLeastTwo` typed carrier above — both items collapse cleanly when normalization collapses Linear↔Polynomial(_, 1) as a structural invariant. **Yellow-flag threshold: graduates alongside the typed-degree follow-up** (coupled dissolution).
+
+**Follow-up — `dominates` composite branches .dag↔Rust divergence (not blocking, cross-type mutual-recursion gates graduation).** Rust `src/v3/compiler/src/dag.rs::dominates` correctly walks children for `ProductCost` / `SumCost` (codex-flagged patch on this PR). The `.dag` authority `src/v3/std/algebra.dag::dominates` returns `False` conservatively for composites because #519's mutual-recursion termination analyzer only accepts cluster members sharing a descent parameter type — the list-iterating helper would descend on `List<SymbolicCost>` while `dominates` descends on `SymbolicCost`, so the cluster can't form. Rust composite-dominance is the authority; .dag is an over-approximation. **Dissolution trigger:** substrate extension letting a mutual-recursion cluster admit cross-type members with per-member structural-descent witnesses (list-head / list-tail descent alongside variant-payload descent). Likely a Lane 1e or later addition to the termination-proof surface. **Yellow-flag threshold: 2 months** or whenever a second .dag↔Rust divergence shows up — the divergence between authorities is only tolerable as long as it's isolated to this single call.
+
+**Follow-up — `build.rs` load-order priority list bootstrap scaffold (not blocking, type-readiness signal gates graduation).** `src/v3/compiler/build.rs` prioritizes `list.dag` and `substrate.dag` ahead of alphabetical order so `structural_binding_info_for_variant` sees populated `Disj` connectives when downstream std files (Lane 2 Stage 2d's `algebra.dag` and the lens) are lowered. This is a bootstrap scaffold: the phase-order prerequisite lives in a filename priority list instead of flowing structurally from the declarations/import graph. **Dissolution trigger:** termination analysis grows a type-readiness signal (phase-1 declaration with fully-populated variant-list, rather than requiring phase-2-lowered body) so `structural_binding_info_for_variant` can succeed regardless of file order. When that lands, the priority list collapses to the empty default. **Yellow-flag threshold: whenever a third std file joins the priority list** — two entries is scaffold, three signals the rule is load-bearing enough to need structural lift.
+
+**Follow-up — symbolic-cost lens fixed-point cycle coverage (not blocking, `compile_stage_snapshots` extension gates graduation).** `src/v3/compiler/src/lens_cost_symbolic_generated.rs` is currently out of the `l1_5_fixed_point_test.rs` / `compile_stage_snapshots` stage-replay loop — that loop iterates pipeline stages (`parse` → `lower` → `infer` → `compute_ownership` → `emit` → `lens_complexity`) but does not include `lens_cost_symbolic` as a stage. Staleness today is guarded only by `cost_generated_module_matches_checked_in_snapshot` in `tests/lane2_stage_2d_symbolic_cost_test.rs`, which re-emits the module and compares against the checked-in file. That's drift protection, but narrower than the fixed-point cycle Complexity / Provenance / Structural-Resolution / Unused-Parameters get. **Dissolution trigger:** first-class stage registration for symbolic cost in `pipeline.dag` (adds a `lens_cost_symbolic` stage + realization), mirroring the existing `lens_complexity` wiring. When that lands, the lens's generated file automatically participates in the fixed-point comparison. **Yellow-flag threshold: 1 month** or whenever a second Stage 2d lens wants regen coverage.
+
+**Follow-up — hand-maintained `SymbolicCost` Rust mirror drift ratchet (not blocking, authority unification gates graduation).** PR #537 ChatGPT review (`sha:0f8c215c0`) call-out: the `SymbolicCost` / `SizeVariable` carriers + the composition functions (`sequential`, `iterate`, `max_path`, `normalize`, `dominates`, `reduce_sum`, `reduce_product`, `combine_binary_product`, `drop_dominated_in_sum`) are hand-maintained in `src/v3/compiler/src/dag.rs` because `emit_rust_module`'s `is_bootstrap_file` filter excludes `src/v3/std/` declarations from Rust emission. The scope is bounded (9 fns + 2 carrier types) and the current surface matches `src/v3/std/algebra.dag` modulo the documented composite-dominance gap (Follow-up above). The risk is future consumers attaching to the Rust mirror and not noticing when it drifts from the .dag authority — "declaration is the implementation" gets quietly replaced by "declaration + stronger hand-maintained Rust version" as the operating pattern. **Dissolution trigger:** the same substrate extension that closes the composite-dominance gap — once termination analysis admits cross-type mutual-recursion clusters, the .dag side matches Rust's richness and the hand-maintained mirror becomes `emit_rust_module`-generated like every other substrate type. Until then, a lightweight ratchet (e.g., a test that greps `src/v3/compiler/src/dag.rs` for fn signatures starting with `SymbolicCost::*` / `pub fn sequential|iterate|...` and cross-checks the count against `src/v3/std/algebra.dag` top-level `fn` decls) would catch silent expansion of the Rust surface. **Yellow-flag threshold: when a tenth hand-maintained fn is added to the mirror** — nine current fns is the baseline; a tenth without matching .dag growth is the signal that the scaffold is growing faster than the authority and needs explicit ratchet wiring.
+
+
 ### Lane 1 Stage 1b
 
 **Deferral: 1b full implementation (M).** 1b's first attempt escalated (PR #495 shipped 1a; 1b code was reverted). Root cause: `.dag` linear-walk bodies for substrate accessors polluted every user DAG. DB-14 codifies the correct pattern (ExternalRealization mirroring pipeline.dag). Unblocked once DB-14 (PR #497) lands. Design: [design-substrate-external-primitives.md](docs/design-substrate-external-primitives.md) (DB-14). Acceptance in DB-14 §Acceptance.

src/v3/compiler/build.rs

@@ -131,7 +131,19 @@ fn main() {
     println!("cargo:rerun-if-changed={}", spec_dir.display());
     println!("cargo:rerun-if-changed={}", compiler_dir.display());
 
-    let staged_entries = collect_dag_entries(&std_dir, &[]);
+    // Structural-recursion termination analysis walks a recursing
+    // argument back to its declared Disj connective (see
+    // `structural_binding_info_for_variant` in `lower.rs`). The walk
+    // only succeeds after the declaring file has been phase-2 lowered,
+    // so `std/list.dag` (declares `List<element> = Empty | Cons {...}`)
+    // and `std/substrate.dag` (declares `Behavior = Value | Transform
+    // | Branch | Loop | Bind`) must land before any sibling std file
+    // that recursively descends over those variants. Without this
+    // priority list, alphabetical order puts `algebra.dag` and
+    // `dimensions.dag` ahead of `list.dag`/`substrate.dag`, and their
+    // recursive helpers fail termination against placeholder
+    // connectives.
+    let staged_entries = collect_dag_entries(&std_dir, &["list.dag", "substrate.dag"]);
     let spec_entries = collect_dag_entries(&spec_dir, &["v3_l1.dag"]);
     let compiler_entries = collect_dag_entries(&compiler_dir, &["pipeline.dag"]);
     let staged_generated =

src/v3/compiler/src/bin/regen_lens_cost_symbolic.rs

@@ -0,0 +1,50 @@
+// Regen driver for `src/v3/lenses/cost.dag` — Lane 2 Stage 2d
+// symbolic-cost lens (DB-7). Mirrors the shape of
+// `regen_lens_cost.rs` (the structural-cost lens) so the two stay
+// reviewable side by side.
+//
+// Output: `src/v3/compiler/src/lens_cost_symbolic_generated.rs`.
+
+use std::io::Write;
+use std::path::PathBuf;
+use std::process::{Command, Stdio};
+
+use v3_compiler::compile_to_dag;
+use v3_compiler::emit_rust::emit_rust_module;
+
+fn main() {
+    let lens_path = PathBuf::from(env!("CARGO_MANIFEST_DIR"))
+        .join("..")
+        .join("lenses")
+        .join("cost.dag");
+    let source = std::fs::read_to_string(&lens_path).expect("read cost.dag");
+    let dag =
+        compile_to_dag(&source, lens_path.to_string_lossy().as_ref()).expect("cost.dag compiles");
+    let raw = emit_rust_module(&dag).expect("emit lens module");
+    let header = "// AUTO-GENERATED from `src/v3/lenses/cost.dag` via\n\
+                  // `emit_rust_module`. Regenerate instead of hand-editing.\n\n";
+    let combined = format!("{header}{raw}");
+
+    let mut child = Command::new("rustfmt")
+        .arg("--emit")
+        .arg("stdout")
+        .stdin(Stdio::piped())
+        .stdout(Stdio::piped())
+        .spawn()
+        .expect("spawn rustfmt");
+    child
+        .stdin
+        .as_mut()
+        .unwrap()
+        .write_all(combined.as_bytes())
+        .unwrap();
+    let output = child.wait_with_output().expect("rustfmt");
+    assert!(output.status.success(), "rustfmt failed");
+    let formatted = String::from_utf8(output.stdout).expect("utf8");
+
+    let out_path = PathBuf::from(env!("CARGO_MANIFEST_DIR"))
+        .join("src")
+        .join("lens_cost_symbolic_generated.rs");
+    std::fs::write(&out_path, &formatted).expect("write lens_cost_symbolic_generated.rs");
+    println!("wrote {}", out_path.display());
+}