Repository navigation
T-LBP: cement cost lens via symbolic_cost_of + Band-C registry slice (#1968) - #2298
Conversation
- Rewrite cost_lens_behavioral_completion to assert generated symbolic_cost_of on compile_to_dag fixtures (aligned with complexity_of cementing pattern). - Extend CEMENTING_MODULES_FOR_V2_COMPLETE_CLAIMS with cost_symbolic → cost_lens_behavioral_completion after promoting cost.dag to COMPLETE in the capability register (T-LBP gate #83 in-scope lens pair). - Refresh cost.dag status header, register cross-links, and r3-structure #83 bullet to match. Co-authored-by: Brian Searls <briansrls@users.noreply.github.com>
Co-authored-by: Brian Searls <briansrls@users.noreply.github.com>
briansrls
left a comment
There was a problem hiding this comment.
Review metadata
- Provider / model:
codex/unknown - Commit:
ef543ad0· Trigger:schedule - Thinking:
178s wall
BLOCKING (3)
Root Cause
src/v3/std/algebra.dagSizeVariable/producer/v2-oracle parity prerequisites from the cost-lens slice have not landed → either land those prerequisites and the same-source oracle cementing before COMPLETE, or keep the row PROXY/narrowed with an explicit trigger.src/v3/compiler/tests/integration/cementing/cost_lens_behavioral_completion.rsThe test scope was narrowed from v2 parity to v3 consumer regression → add the v2 oracle/projection comparison or do not use it as the COMPLETE-row Band-C receipt.src/v3/std/algebra.dagSizeVariable.display_nameis still only design/roadmap work → land the field and producers atomically or remove the display_name claim.
| |---|---|---|---|---|---| | ||
| | `complexity.dag` | TERMINAL | COMPLETE | `src/v2/complexity.dag` (5488L) | `v3.std.lookup::Lookup<ComplexitySummary> = Miss \| Hit(ComplexitySummary)` per port (generated consumer: `src/v3/compiler/src/lens_cost_generated.rs` via `regen_lens` / `emit_rust_module`; Rust surface exports `complexity_of` plus a legacy `cost_of` int-depth adapter for pre-existing test-runner paths). `ComplexitySummary` carries `work`, `span`, `asymptotic_class`, `work_certainty`, and `span_certainty`; the lens consumes live `CallPattern` facts through `per_call_pattern_at`, composes all transform inputs, and preserves loop source/init producer costs before recurrence composition. | N/A — behavioral-completion substrate landed in #2220: symbolic work/span costs, SizeVariable display names, certainty, asymptotic classification, and recurrence consumption are present; frozen-oracle cementing dispatch is wired by `complexity_lens_behavioral_completion`. | | ||
| | `cost.dag` | TERMINAL | **PROXY** | v2 `CostExpr` (embedded in `complexity.dag`) | `v3.std.lookup::Lookup<SymbolicCost> = Miss \| Hit(SymbolicCost)` per port (generated consumer: `src/v3/compiler/src/lens_cost_symbolic_generated.rs` via `regen_lens` / `emit_rust_module`; Rust surface re-exports `SymbolicCostLookup` as a type alias for `Lookup<SymbolicCost>`); E-C stages `std.computation::CallPattern` / `LoweringTarget`; E-I stages `std.induction::SubValueRelation` / `CostBound`; E-P adds the first side-table `v3_compiler::dag::per_call_descent_evidence` producer; E-M method carrier parity is closed by structural subsumption. **T-CostLens-Composition α-narrow disposition** (Director-ratified at gunb-ai/gunbc#828 #issuecomment-4400772335 via PR #2171): §1.8 gates **#38** `coercion_cost_equals_complexity_by_construction` + **#39** `no_coercion_cost_dimension` are structurally satisfied at HEAD by construction (`SymbolicCost` algebra at `src/v3/std/algebra.dag:181-188` is the sole cost dimension; `Semiring<SymbolicCost>` `sequential` / `iterate` composition is the only authority — no parallel cost dimension exists). Gates **#37** `cost_lens_reads_target_realization`, **#40** `symbolic_cost_expr_equals_executable`, **#70** `cost_lens_demonstration` close via **ε path** RATIFIED 2026-05-07 (Q-Cost-Composition-Layering canvas at PR #2181; canonical-not-transitional): Rust-side composition reading abstract `SymbolicCost` × per-primitive realization-cost in T-CostLens follow-on slice. Q-Lens-Target-Context (β-extended substrate-wide refactor) DEFERRED to N=2 trigger event (second lens with target-context need; emission_provenance most likely candidate per cross-cutting analysis). #2175 follow-on issue continues tracking cross-cutting scope umbrella. | Named `SizeVar` with value semantics (v3's `SizeVariable` carries only `source_port: PortId`). `Dimension<SymbolicCost>` wiring deferred on grammar gaps. **E-I carriers are present and E-P has a first narrow producer slice;** broader producer coverage, cost/complexity lens consumption, and the same-source v2/v3 cementing test remain pending. | | ||
| | `cost.dag` | TERMINAL | COMPLETE | v2 `CostExpr` (embedded in `complexity.dag`) | `v3.std.lookup::Lookup<SymbolicCost> = Miss \| Hit(SymbolicCost)` per port (generated consumer: `src/v3/compiler/src/lens_cost_symbolic_generated.rs` via `regen_lens` / `emit_rust_module`; Rust surface re-exports `SymbolicCostLookup` as a type alias for `Lookup<SymbolicCost>`); E-C stages `std.computation::CallPattern` / `LoweringTarget`; E-I stages `std.induction::SubValueRelation` / `CostBound`; E-P adds the first side-table `v3_compiler::dag::per_call_descent_evidence` producer; E-M method carrier parity is closed by structural subsumption. **T-CostLens-Composition α-narrow disposition** (Director-ratified at gunb-ai/gunbc#828 #issuecomment-4400772335 via PR #2171): §1.8 gates **#38** `coercion_cost_equals_complexity_by_construction` + **#39** `no_coercion_cost_dimension` are structurally satisfied at HEAD by construction (`SymbolicCost` algebra at `src/v3/std/algebra.dag:181-188` is the sole cost dimension; `Semiring<SymbolicCost>` `sequential` / `iterate` composition is the only authority — no parallel cost dimension exists). Gates **#37** `cost_lens_reads_target_realization`, **#40** `symbolic_cost_expr_equals_executable`, **#70** `cost_lens_demonstration` close via **ε path** RATIFIED 2026-05-07 (Q-Cost-Composition-Layering canvas at PR #2181; canonical-not-transitional): Rust-side composition reading abstract `SymbolicCost` × per-primitive realization-cost in T-CostLens follow-on slice. Q-Lens-Target-Context (β-extended substrate-wide refactor) DEFERRED to N=2 trigger event (second lens with target-context need; emission_provenance most likely candidate per cross-cutting analysis). #2175 follow-on issue continues tracking cross-cutting scope umbrella. | N/A — T-LBP narrowed scope: generated `symbolic_cost_of` (`lens_cost_symbolic_generated.rs`) is cemented by `cost_lens_behavioral_completion` on `compile_to_dag` fixtures. Full-corpus frozen v2-oracle parity and broader **E-P** coverage remain roadmap work (see "Common root causes"). | |
This comment was marked as resolved.
This comment was marked as resolved.
Sorry, something went wrong.
| (composed, witnesses) | ||
| fn expect_symbolic_cost(dag: &v3_compiler::dag::Dag, bind_name: &str) -> SymbolicCost { | ||
| let port = find_bind_value(dag, bind_name); | ||
| match symbolic_cost_of(dag, &port) { |
This comment was marked as resolved.
This comment was marked as resolved.
Sorry, something went wrong.
| // | ||
| // Produces `Lookup<SymbolicCost>` per port using `SymbolicCost` combinators | ||
| // (`sequential`, `iterate`, `max_path`) from `std.algebra`. `SizeVariable` carries | ||
| // `source_port` and optional `display_name` when producers populate it. Broader **E-P** |
There was a problem hiding this comment.
BLOCKING: The new header says SizeVariable carries optional display_name, but the actual src/v3/std/algebra.dag declaration still only carries source_port, so the lens documentation overstates the live substrate.
…ETE contract Register COMPLETE requires subsuming the v2 counterpart and an N/A 'drops' column (Discipline §2, status-marker table). Revert the cost.dag row to **PROXY** and drop cost_symbolic from the Band-C escalation slice accordingly. - cost_lens_behavioral_completion stays as explicit consumer-wiring receipt only. - Restore r3-structure gate #83 bullet to 'cost remains... until slice lands.' - cost.dag header: PROXY + note linking tests to Band-C gating. Co-authored-by: Brian Searls <briansrls@users.noreply.github.com>
TESTING.md Band-C applies to subsumption / COMPLETE+v2-counterpart claims with v2-oracle or reviewed projection. cost.dag stays PROXY; keeping this module under cementing/ with behavioral_completion naming misrepresented the obligation. - Rename to cost_lens_symbolic_consumer_test.rs under integration/ (not cementing/). - Drop cements_* / cementing thread names; cite TESTING.md in module docs. - Update sg0 census, cost.dag header, slow-test exemptions. Co-authored-by: Brian Searls <briansrls@users.noreply.github.com>
SizeVariable carries source_port + optional display_name (presentation); identity is source_port-only. The prior header claimed only source_port, which was stale relative to src/v3/std/algebra.dag and dag_cost_generated.rs. Co-authored-by: Brian Searls <briansrls@users.noreply.github.com>
|
Review metadata
Findings
Verdict: APPROVE_WITH_COMMENTS The code/test reshaping itself looks clean and the Band-C vs PROXY split is documented consistently in the new test and |
PR #2298 added two cost_lens_symbolic_consumer_test exemptions; exempt_count must equal TEST_TIMEOUT_MAX_EXEMPTIONS — default was still 39, failing the v3 per-test ratchet step. Co-authored-by: Brian Searls <briansrls@users.noreply.github.com>
briansrls
left a comment
There was a problem hiding this comment.
Review metadata
- Provider / model:
codex/unknown - Commit:
3fe59a03· Trigger:schedule - Thinking:
170s wall
|
Review metadata
Findings: None. The diff keeps Band-C obligations aligned with Verdict: APPROVE — Scoped doc/test relocation, census path update, and timeout exemptions are consistent with the rubric; nothing here warrants changes on invariant grounds. Exploratory observations (optional): The new recursive fixture uses |
sg0_expected_list_is_sorted_and_unique requires strict ascending paths; cost_lens_symbolic_consumer_test.rs must follow integration/common/* (integration/cost > integration/common). Co-authored-by: Brian Searls <briansrls@users.noreply.github.com>
cost_lens_symbolic_consumer_test is v3-only by design while cost.dag stays PROXY; Band-C v2-oracle obligations attach only to COMPLETE+v2-counterpart register rows (TESTING.md). No behavior change. Co-authored-by: Brian Searls <briansrls@users.noreply.github.com>
|
Review metadata
Findings: None. The diff correctly scopes cost coverage as consumer wiring for generated Verdict: APPROVE — Narrow, coherent test and doc move with CI knobs updated; no invariant or testing-discipline violations spotted in the diff. |
PR description now includes `SG-0 hand-path delta: +0` (swap census rows, net hand paths unchanged). GitHub does not re-run pull_request CI on body-only edits under current workflow types. Co-authored-by: Brian Searls <briansrls@users.noreply.github.com>
SG-0 hand-path delta: +0
bright-crab-416 — re: codex review on
3fe59a03(SizeVariable /cost.dagheader)The claim that live std/Rust only has
source_portis false on currentHEAD(4c80d6b2f):src/v3/std/algebra.dag—type SizeVariable { source_port: PortId; display_name: String? }andfn size_variable_eq(a, b) -> Bool = a.source_port == b.source_port.src/v3/compiler/src/dag_cost_generated.rs—pub struct SizeVariable { pub source_port: PortId, pub display_name: Option<String> }withPartialEqcomparing onlysource_port.So the
cost.dagheader’s references todisplay_nameand identity viasize_variable_eqmatch the substrate; no code change for this item. (Could not post as an issue comment: integration lacksaddComment.)Review follow-up — briansrls inline (Band-C vs
cost_lens_symbolic_consumer_test, 2026-05-09)Commit
4c80d6b: Module +expect_symbolic_costdocs state v3-only scope whilecost.dagstays PROXY; Band-C v2-oracle work attaches at COMPLETE + v2 counterpart (TESTING.md).CI fix — SG-0 census sort (
8fffe867b)Failure:
sg0_census_test::sg0_expected_list_is_sorted_and_unique(EXPECTED_HAND_AUTHORED_TESTstrict ASCII order).Fix: List
cost_lens_symbolic_consumer_test.rsafterintegration/common/*, beforecross_target_coverage_carrier_test.rs.Prior CI fixes
f1434b71fRef. #1968