Repository navigation
Substrate T-CostLens-Composition behavioral completion (γ-ratified) — recreated [supersedes #1957] - #2283
Conversation
…post-#2271 Per Substrate Mgr disposition (a) at gunbc#2068 c#4410044549 — partial mechanical fix-forward to unblock cross-lane PRs blocked on main-green post-PR-#2271 merge (T-LBP complexity-lens substrate completion). This PR addresses 2 of 6 reported failures (the mechanical ones): 1. **SG-0 census** (`sg0_v3_test_hand_authored_subratchet`): added `cementing/complexity_lens_behavioral_completion.rs` to EXPECTED_HAND_AUTHORED_TEST per existing per-cementing-test discipline. Comment cites PR #2271 origin + register-promotion context. 2. **Parse manifest** (`handwritten_parse_snapshot_matches_manifest`): refreshed 4 row hashes for substrate-widening files — `src/v3/spec/rust.dag` (170→173 items), `src/v3/std/algebra.dag` (47→55), `std/computation.dag` (18→20), `std/induction.dag` (56→62). Refresh test couldn't write to my worktree under buildbuddy shim; hand-transcribed from failing-test `left:` payload via python diff extraction. **Out of scope** (per Mgr disposition (a) — investigated separately): - Item 1 (m1_substrate stack overflow) — substantive investigation - Item 3 (r1_canonical lens bytes) — worker-call on shape post-widening - Item 4 (m2_lens_cost_migration end-to-end) — same shape - Item 6 (slow-test ratchet) — new tests measured at <2s each, not exemption-required at HEAD Refs: #2074 c#4409948664 (PB Mgr signal); gunbc#2068 c#4410044549 (Mgr disposition); PR #2271 (T-LBP origin). Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Three substantive items deferred initially per Mgr disposition (a) at gunbc#2068 c#4410044549 — turned out simpler than feared once the substrate-widening shape was clear: 1. **m1_substrate_test::substrate_accessor_rust_binding_invariants** (item 1): expected count 7→8 + name list adds `per_call_pattern_at` (new substrate accessor at `src/v3/std/computation.dag:67-69` introduced by PR #2271). 2. **r1_canonical_complexity_lens_bytes_*** (item 3): canonical lens bytes assertion + test name updated from `cost_of`/`compute_costs` → `complexity_of`/`compute_summaries` reflecting PR #2271's BEHAVIORALLY COMPLETE widening per `docs/v3-lens-capability-register.md:40` row promotion. Test renamed `..._include_cost_of` → `..._declare_complexity_of` per gpt-5-5-pro APPROVE_WITH_COMMENTS (sha 0d477e5) test-naming discipline. 3. **m2_lens_cost_migration::complexity_dag_runs_end_to_end** (item 4): harness-source format changed `emitted::cost_of` → `v3_compiler::lens_cost::cost_of`. The legacy `cost_of` adapter still exists at `src/v3/compiler/src/lib.rs:3362` (per register row "Rust surface exports complexity_of plus a legacy cost_of int-depth adapter") but lives at the top-level `lens_cost` module path, not inside the regen-emitted `mod emitted` block. CI not re-runnable locally on buildbuddy shim (parallel-test SIGABRT); counting on PR CI for verification. Refs: #2074 c#4409948664; gunbc#2068 c#4410044549; PR #2271. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
…ty_of; sg0 + test_runner takes main wording)
|
Review metadata
Verdict: APPROVE Diff is small and narrowly scoped. I didn’t find a concrete violation of the pinned invariants or modeling/testing guidance in the changed lines: the new |
|
Review metadata
Findings
Nothing in this diff touches substrate VerdictAPPROVE_WITH_COMMENTS — The row walker matches declared meta tags via existing Exploratory observations (optional)
|
|
Review metadata
Verdict: APPROVE — clean, narrowly scoped Slice 1a.2. This adds a Rust-side Minor observations (non-blocking):
|
briansrls
left a comment
There was a problem hiding this comment.
Review metadata
- Provider / model:
codex/unknown - Commit:
b3d14e0a· Trigger:schedule - Thinking:
227s wall
BLOCKING (1)
Root Cause
src/v3/std/emit_model.dag*Realization.cost is still modeled as unconstrained Int → move it to a nonnegative/Nat cost carrier or have the new row walker fail closed before inserting negative costs.
|
Violations (could not place on specific lines):
|
|
Review metadata
1. Story of the diffThis PR keeps the 2. Invariant categories
Compliant — no new Dag/substrate type or Dag mutation is introduced; the new module is an implementation-side substrate consumer that reads declared facts via generated meta accessors (
Finding (NON-BLOCKING, implementation API):
Compliant — the new boundary has an explicit signature,
Compliant — the diff adds focused behavior tests for the new public reader: type realization cost (
Compliant — the diff does not silently diverge from the ε factoring; it says the row walker “stays Rust-side per ε ratification” and that
Compliant — the deferred work is named and bounded: Slice 1a.2 is the row walker, Slice 1b parameterizes the concrete cost-fold consumer ( 3. VerdictAPPROVE_WITH_COMMENTS The landed behavior is coherent, fail-closed, and covered at the right integration seam. The only issue I see is the small public-carrier duplication between |
|
Review metadata
Verdict: APPROVE — clean Rust-side implementation slice (1a.2) of the documented T-CostLens-Composition ε path; substrate untouched, scoped to a host-side row walker. What I checked
Minor observations (non-blocking)
|
|
Verified against current head — sent from fierce-ram-21 |
|
Review metadata
Findings: none. Verdict: APPROVE — Slice 1a.2 is narrow and clean. The new Exploratory observations:
|
|
Verified against current head — sent from fierce-ram-21 |
|
Fixed the invalid-language fail-closed gap in head — sent from fierce-ram-21 |
|
Verified against current head — sent from fierce-ram-21 |
briansrls
left a comment
There was a problem hiding this comment.
Review metadata
- Provider / model:
codex/unknown - Commit:
1987d69d· Trigger:schedule - Thinking:
193s wall
✅ No new blocking concerns in the current diff.
|
Verified against current head — sent from fierce-ram-21 |
|
Verified against current head — sent from fierce-ram-21 |
|
Review metadata
1. Story of the diffThis PR advances 2. Invariant categories
Compliant — substrate-adjacent consumer, not a substrate schema change: the new code reads existing
Compliant — fail-closed and illegal-states pressure are handled at the API boundary:
Compliant — the main API has explicit dependencies and a typed result shape:
Compliant — the PR adds targeted behavior tests for the new contract: negative cost rejection (
Compliant — the diff does not silently diverge from the ratified ε layering; it explicitly states that Slice 1a.2 is a Rust-side row walker and that the composition of abstract
Compliant — the staged shape is documented and bounded: 3. VerdictAPPROVE. The PR keeps realization rows as the single authority, adds a typed fail-closed Rust consumer for the ε path, and backs the new behavior with focused regression coverage. I did not find a diff-citable substrate or invariant violation that warrants changes. |
|
Verified against current head — sent from fierce-ram-21 |
briansrls
left a comment
There was a problem hiding this comment.
Review metadata
- Provider / model:
codex/unknown - Commit:
0dbee39a· Trigger:schedule - Thinking:
273s wall
briansrls
left a comment
There was a problem hiding this comment.
Review metadata
- Provider / model:
codex/unknown - Commit:
38083bec· Trigger:schedule - Thinking:
226s wall
Non-blocking — Strengths
src/v3/compiler/src/lib.rsThe row walker rejects malformed realization rows and negative costs through typed RealizationCostError variants instead of fabricating defaults.
|
Verified against GitHub review-thread state after the 2026-05-09T21:20:15Z review: prior P5 receipt comment No code or PR-body change needed for this repeated/stale finding. Current checks are green at head — sent from fierce-ram-21 |
…-main-red-fix # Conflicts: # docs/briefs/r3-evaluator-tc3-d4-eval-step-producer-worker.md
|
Verified against current head |
Closes #2141
Summary
Adds the Rust-side
v3_compiler::realization_costrow walker for the T-CostLens-Composition epsilon path. The table reads existing*Realizationdeclarations by meta tag and language, indexes typed realization-cost keys, rejects malformed/duplicate/negative rows fail-closed, and keeps.dagcost composition deferred to the next slice.Updates the cost-lens comments and capability register so the live state is explicit: Slice 1a.2 supplies target-realization row walking;
SymbolicCost × per-target realization-costcomposition remains follow-on work.Per-PR dissolution gate (required for new/expanded hand-Rust under
v3/)T-PB-A/T-PB-B SG-0 ratchet split; concrete ROADMAP rowROADMAP.mdSG-0 ratchet split is structural, which assigns non-test hand-Rust to T-PB-A and Rust-authored tests to T-PB-B: https://github.com/gunb-ai/gunbc/blob/main/ROADMAP.md#L175. This PR expands existing hand-Rust surfaces (src/v3/compiler/src/lib.rsplussrc/v3/compiler/tests/integration/lens_cost_target_realization_test.rs) without editing the SG-0 census, so dissolution is explicitly deferred to the SG-0 ratchet split rather than claimed as a same-PR shrink.SG-0 net-shrink discipline (required when
sg0_census_test.rschanges)Not applicable; this PR does not edit
src/v3/compiler/tests/integration/sg0_census_test.rs.Test plan
cargo fmt --check— passed.cargo test -p v3-compiler --test integration lens_cost_target_realization -- --nocapture— passed.cargo test -p v3-compiler --test integration sg0_v3_ -- --nocapture— passed.cargo test -p v3-compiler realization_cost_table_rejects_negative_cost_rows -- --nocapture— passed.fmt,ci,v3;self_host_ratchetskipped).