CX: soundness fixes + PERF-6 + complexity enabled

ROADMAP.md

@@ -88,7 +88,7 @@ Previously eliminated:
 | Lint | `cargo clippy --workspace -- -D warnings` | GREEN |
 | Tests | `cargo test -p v2-compiler-tests` | GREEN (316 pass, 0 fail, 44 ignored) |
 | Full DSL | `full_dsl_compiles -- --ignored` | GREEN (93 dsl + 29 v2) |
-| Diagnostic ratchet | `strict_compile_diagnostic_count -- --ignored` | 314 (all complexity violations) |
+| Diagnostic ratchet | `strict_compile_diagnostic_count -- --ignored` | 314 (0 self-compile diagnostics) |
 | L1 ratchet | `scripts/l1-ratchet.sh --check` | 37 (target: 0) |
 | Stage0 freshness | `scripts/check-stage0-freshness.sh` | GREEN (blocking) |
 
@@ -98,7 +98,7 @@ Previously eliminated:
 |--------|---------|--------|-------|
 | Self-compile diagnostics | 314 | 0 | All indirect-recursion complexity violations |
 | L1 type knowledge | 37 | 0 | Down from 70; name-based workarounds tracked for M4 |
-| Complexity violations | 164 | 0 | Down from 315; unfinished algebraic grounding |
+| Complexity violations | 0 | 0 | GREEN — CostUnknown deleted, all costs concrete (PR #336) |
 | Emitted Rust errors | 0 | 0 | GREEN |
 | DSL complexity ratchet | 2 | 0 | stack_size + fold_stack (deferred to CX lane) |
 
@@ -697,10 +697,12 @@ then deleted. `Node.name` field deleted.
 
 ## CX: Complexity Analyzer (Lane 3)
 
-**Status:** Down from 315 → 164 (main) → 76 after PR #318.
+**Status:** Down from 315 → 164 (main) → 76 after PR #318 → 313 after PR #336.
 Phase 1-2 complete (RecursionPattern deleted, all classifiers return LoweringTarget).
 CX-N: var threading, type-directed dimension selection, algebra-to-dimension bridge.
-Ratchet at 325.
+0 violations — CostUnknown deleted, all costs concrete (PR #336).
+Complexity analysis re-enabled in compile pipeline.
+PR #336: soundness fixes, graph extraction, is_valid_proof, CostUnknown deletion.
 
 **Root cause:** The analyzer maintains parallel heuristic classifiers
 instead of consuming the structural facts already modeled in std/.
@@ -770,32 +772,34 @@ remaining path is sound. Work accomplished:
 - SCC parameter name unification in emit_pattern (CX-Q/CX-R)
 - Soundness fixes: branching_only, all_safe, any-argument fabrication
 
-### Review feedback (deferred — 15 items from PR #318)
-
-Per Review Queue Discipline, these are recorded but not stacked:
-
-**Theme A: Heuristic descent recognizers** (read structural facts instead)
-- `complexity.dag:1962` — child-descent hardcodes `"children"` and list-methods
-- `complexity.dag:2056` — `is_tree_size_preserving_wrapper` hardcodes callee name
-- `complexity.dag:2088` — hardcoded `rt_type`, `param_node_type_expr`, `field_binding_pattern` as sub-value extractors
-- `complexity.dag:2170` — treats any `param.field` as descent without structural witness
-- `complexity.dag:2244` — `is_match_option_descent` is shape heuristic for missing Option/Result facts
-- `complexity.dag:2312` — `lambda_param_names |> last` heuristic for missing method-signature facts
-
-**Theme B: Producer patches** (fix analyzer root cause instead)
-- `02_parse.dag:2759` — `node_to_name_str` split to make SCC shape friendlier
-- `04_types.dag:418` — optional-cardinality split to make analyzer see Same edge
-
-**Theme C: Fabrication / scope issues** (unsound)
-- `complexity.dag:275` — `ParserResultDirectState` duplicates state-progress fact
-- `complexity.dag:1382` — filtering `ProgressSame` self-edges fabricates acyclicity
-- `complexity.dag:2346` — `val_inner_vars` leaks arm-local bindings into outer scope
-- `complexity.dag:3061` — `branching_proof_safe` fallback fabricates LinearRecursion
-- `same_progress_subgraph_has_cycle` drops self-loops for 1-node SCCs
-
-**Theme D: Boundary / testing**
-- `tests/pipeline.rs:2505` — diagnostic tests read workspace source tree (not hermetic)
-- `05_emit_rust.dag:1334` — `emit_variant_pattern` returns empty string on impossible input
+### Review feedback (15 items from PR #318 — 10 resolved, 5 remaining)
+
+**Theme A: Heuristic descent recognizers** (6 items)
+- [x] #1-4: Already data-driven via `function_size_effects`, `node_field_roles`,
+  `AlgebraMethodSemantics` tables (fixed in PR #328, stale line numbers)
+- [~] #5: `is_match_option_descent` — documented assumption (PR #336).
+  Full fix deferred to CX-D (coproduct projection metadata in std/)
+- [~] #6: `lambda_param_names |> last` — replaced by `iteration_element_name`
+  (PR #336). Direct template lookup deferred: emitter inlines cross-module
+  AlgebraTypeTemplate variants into caller, breaking compilation.
+  Structural fact confirmed in std/algebra.dag CallableOf declarations.
+
+**Theme B: Producer patches** (2 items)
+- [ ] `02_parse.dag:2759` — `node_to_name_str` split. Deferred until P4.1
+  (wrapper transparency in SCC edge classification)
+- [x] `04_types.dag:418` — not a patch; proper cardinality design
+
+**Theme C: Fabrication / scope issues** (5 items — all fixed in PR #336)
+- [x] `ParserResultDirectState` field renamed `progress` → `input` (consistency)
+- [x] `same_progress_subgraph_has_cycle` now detects 1-node ProgressSame self-loops
+- [x] `val_inner_vars` scope leak fixed — arm-local bindings no longer escape
+- [x] `branching_proof_safe` accepts lexicographic proofs (checks first dimension)
+- [x] Self-loop detection matches `proof_has_non_descending_cycle` pattern
+
+**Theme D: Boundary / testing** (2 items)
+- [ ] `tests/pipeline.rs:2505` — diagnostic tests non-hermetic (larger scope, deferred)
+- [x] `05_emit_rust.dag:1334` — `emit_variant_pattern` checks `fielded_variants`
+  when all bindings are wildcards (PR #336)
 
 ### Dependency chain
 
@@ -851,9 +855,10 @@ CX-D (model facts in std/)
   Dead `skip()` ExprCall handlers removed (inference bridge normalizes).
   **(PR #328)**
   Deferred: `is_valid_proof` stub in termination.dag (blocked on
-  bootstrap); `ParserResultDirectState` duplication (refactoring);
-  `branching_proof_safe` only accepts TreeSize/ListLength (extend to
-  lexicographic).
+  graph utility extraction to `std/graph.dag` — import direction
+  prevents termination.dag from calling SCC detection in complexity.dag).
+  `ParserResultDirectState` field renamed (PR #336).
+  `branching_proof_safe` now accepts lexicographic proofs (PR #336).
 - **CX-B**: CostExpr/SizeExpr dissolution — cost expressions become flat
   products of SizeBounds from `std/computation.dag`'s lowering table.
   **Partial.** `CostShape` type moved to `dsl/std/algebra.dag`, declared
@@ -911,12 +916,17 @@ lanes — any lane can introduce a regression.
   block emission — not yet an unconditional gate. Convergence proof
   (pass-1 = pass-2) remains in `bootstrap_fixed_point` (`#[ignore]`,
   not yet a CI gate — expensive: two full builds + two compiles).
-- **PERF-3**: Track self-compile memory. The CX OOM root cause was
-  repeated complexity classification on large compiles, not raw budget.
-  Add a memory-usage ratchet or at minimum log peak RSS during
-  `performance_ratchet`. **Blocked-by: CX-E** (complexity analysis
-  currently disabled for memory; can't validate memory ratchet until
-  CX is re-enabled and the classification OOM is resolved).
+- **PERF-3**: Self-compile complexity analysis. CX-E resolved (0 violations,
+  CostUnknown deleted). OOM remains on full self-compile (~1600 functions):
+  complexity analysis disabled in compile.dag for memory. Root causes (PR #336):
+  (1) CostExpr tree blowup — mitigated by eager simplification in cost_seq/cost_par
+  (2) Redundant body walks — mitigated by pre-computing all recursion patterns
+      in build_complexity_report before the cost phase
+  (3) Persistent map threading — each cache_summary creates a new Rc<CostInternTable>
+      with cloned map (not yet addressed)
+  (4) Rc-based CostExpr accumulation — ~1000 nodes per function × 1600 functions
+      (not yet addressed — requires arena allocation or structural sharing)
+  Next: profile peak RSS to identify which of (3)/(4) dominates.
 - **PERF-4**: Test suite wall-clock ratchet. Current: ~270s for 271
   tests. Budget TBD. Individual tests >2s are suspect (per project
   convention). Add per-test timing visibility.
@@ -925,10 +935,104 @@ lanes — any lane can introduce a regression.
   than wall-clock time. More deterministic, catches algorithmic
   regressions independent of machine load.
 
+### PERF-6: Dependency-modeled computation (no redundancy, no retention)
+
+**Thesis:** Re-derivation and over-retention are symptoms of the same
+root cause: the pipeline doesn't model computation dependencies. When
+it doesn't know what depends on what, it re-computes (redundancy) and
+retains everything (over-retention) because it can't prove when a value
+is safe to drop or when a walk is redundant.
+
+**Two manifestations:**
+
+1. **Redundant work** — same function body walked N times by different
+   analyses that could share a single traversal.
+2. **Over-retention** — intermediate values (CostExpr trees, descent var
+   maps) kept in memory after all consumers have read them, because
+   the pipeline has no concept of "transit vs result."
+
+The general principle: if you can't express "this value is no longer
+needed," you can't drop it. Every `Map<String, X>` that accumulates
+full intermediate state and never prunes is an instance.
+
+**Current instances (self-compile, ~1600 functions):**
+
+Redundant work:
+- `classify_recursion_pattern` walks body 2-3× (proof dimensions)
+- `construct_scc_termination_proof` walks body 5-6× per SCC member
+- `collect_descent_vars` walks body 1× per param per dimension
+- `max_path_self_calls` walks body 1× (could be cached)
+
+Over-retention:
+- `CostInternTable.summaries` holds full CostExpr trees for ALL 1600
+  functions simultaneously. Each tree is ~1000 Rc nodes. Consumers
+  only need the classified string ("O(n)"), not the tree. But there's
+  no transit/result distinction — everything is retained.
+- Processing order is declaration order, not topological (callee-first).
+  Topological order would allow dropping callee summaries after all
+  callers are processed. The SCC computation already provides this order.
+
+**Mitigation (PR #336):**
+- Pre-compute all recursion patterns before cost phase
+- Eager simplification in cost composition (prevent CostExpr blowup)
+- Single-function patterns stored in scc_index (avoid re-classification)
+
+**Endgame:** Two structural changes:
+1. **Single-walk analysis:** Each function body walked ONCE → produces a
+   `FunctionAnalysis` record with all facts (proof, descent vars, cost).
+   Redundant walks become unrepresentable.
+2. **Transit/result distinction:** Intermediate values (CostExpr trees)
+   classified eagerly and dropped. The report stores classifications,
+   not trees. `CostInternTable` becomes a transit cache with pruning,
+   not a permanent accumulator. Functions processed in topological order
+   so callees can be dropped when all callers are done.
+
 ### Acceptance
 
 `performance_ratchet` and `bootstrap_stage0_to_stage1` running in CI.
 No test >2s without justification. Self-compile time tracked per-PR.
+Self-compile complexity analysis runs without OOM (PERF-3 + PERF-6).
+
+### CX-NEXT: Cost algebra as compositional data modeling
+
+**Status:** Design direction established (PR #336 discussion). Not yet implemented.
+
+**Core problem:** `SizeExpr` and `CostExpr` are parallel expression algebras.
+SizeExpr reinvents Add/Max/Log as size-specific variants instead of deriving
+them from existing std/ concepts. This is the same anti-pattern as building
+a mini-language inside the cost analyzer instead of composing facts from the
+data model.
+
+**Design direction:**
+- **Sizes are facts, not expressions.** A collection's size is a structural
+  fact (Layer 3 in MODELING.md), not a symbolic expression. The cost algebra
+  should reference sizes by identity, not by re-encoding them in SizeExpr.
+- **CostLog should emerge from iteration structure.** Divide-and-conquer
+  (n → n/2) produces log₂(n) iterations — this should emerge from the
+  recursion pattern, not from a hand-placed CostLog primitive. Remove CostLog
+  from CostExpr; add SizeLog to SizeExpr (or better: derive it from the
+  descent evidence in SizeBound).
+- **SizeBound should carry descent type.** Currently `ArithmeticParam` drops
+  whether descent is subtraction (linear: n iterations) or division
+  (logarithmic: log n iterations). Preserving `ArithmeticDescent { op, by }`
+  in SizeBound lets `bounded_recursive_cost` produce the correct iteration
+  count without adding ad-hoc SizeExpr variants.
+- **ExplicitCount should preserve the literal.** `ExplicitCount { n: 5 }`
+  should produce `SizeConst { value: 5 }`, not `SizeConst { value: 1 }`.
+  The constant IS the bound — collapsing it to 1 loses information. Only
+  asymptotic normalization (formatting) should collapse constants.
+
+**Open review feedback (PR #336, deferred to follow-up):**
+- #8-9: `dfs_finish_order`/`dfs_collect_component` — visited-set-bounded
+  recursion needs worklist primitive (ROADMAP I1/I2)
+- #10: CostExtern — needs stdlib cost contract system
+- #11: `iteration_element_name` — positional heuristic, needs cross-module
+  template lookup (CG-2/CG-3)
+- #13-14: `is_valid_proof` / `proof_has_non_descending_cycle` — proof
+  validation gaps in std/graph.dag
+- #15: SCC zero-placeholder — standard fixed-point technique, but should be
+  documented as such (not silent fabrication)
+- #16: `SizeConst(1)` for ExplicitCount — loses literal bound
 
 ---
 

dsl/std/computation.dag

@@ -241,8 +241,11 @@ fn lower_call_pattern(pattern: CallPattern) -> LoweringTarget {
   }
 }
 
-// Extract the parameter name from a SizeBound, or none for bounds without
-// a named parameter (ExplicitCount, Forever).
+// Extract the parameter name from a SizeBound, or none for constant bounds.
+// Named bounds (TreeSize, CollectionSize, ArithmeticParam) have a parameter
+// that varies with input — these produce O(n)-class costs.
+// Constant bounds (ExplicitCount, Forever) are fixed values — they produce
+// O(1)-class costs because the iteration count doesn't depend on input size.
 fn size_bound_param(bound: SizeBound) -> String? {
   match bound {
     TreeSize { param: p }       => Some { value: p }
@@ -253,6 +256,31 @@ fn size_bound_param(bound: SizeBound) -> String? {
   }
 }
 
+// Is this bound a constant (iteration count doesn't depend on input)?
+// Forever and ExplicitCount are constants — the machine can only iterate
+// a fixed number of times regardless of input size.
+fn is_constant_bound(bound: SizeBound) -> Bool {
+  match bound {
+    ExplicitCount { n: _ } => true
+    Forever                => true
+    _                      => false
+  }
+}
+
+// Get the constant value for a constant bound.
+// ExplicitCount returns the developer-specified literal.
+// Forever returns 1 (machine max — asymptotically constant).
+// Precondition: is_constant_bound(bound) must be true.
+// Non-constant bounds return 0 (identity for SizeConst in CostSum)
+// to fail visibly rather than fabricating a plausible value.
+fn constant_bound_value(bound: SizeBound) -> Int {
+  match bound {
+    ExplicitCount { n: count } => count
+    Forever                    => 1
+    _                          => 0
+  }
+}
+
 // =========================================================================
 // Computation profile: enrichment for expression patterns
 //