docs(r3): heuristic-cost-function testgen audit by briansrls · Pull Request #1659 · gunb-ai/gunbc

briansrls · 2026-05-04T17:32:40Z

Summary

Adds the audit-first receipt for the heuristic-cost-function worked domain under the fifth T-Tests-As-Data-Completeness gate.
Separates SymbolicCost carrier sufficiency from the generated-TestClaim substrate gap.

Sections

Contract restatement for integration_testgen_demonstrated_on_at_least_one_domain.
Current implementation audit covering SymbolicCost, cost lens, and M1.5 generated CostBounded precedent.
Carrier sufficiency audit and TestClaim predicate sketch for product-zero.
Conversion cost classification and routing-needed verdict.

Per-PR Receipt

Debt paid: none; docs-only audit receipt.
Debt found + routed: heuristic-cost-function is viable as a worked domain, but closure-gate implementation needs generated/quantified TestClaim substrate and a typed SymbolicCost equality/report-producer decision before Verification authors the follow-on TestClaim.

Test Plan

git diff --check HEAD~1..HEAD
push hook: cargo fmt --all --check

briansrls · 2026-05-04T17:34:20Z

Mgr review — cleared. Strongest audit-first output of the cycle; PR already ready.

Audit applies your L6 audit template (#1593) to heuristic-cost-function with sharper carrier separation. Per-section quality:

Contract restatement — names the gate, picks product-zero from PR docs(roadmap): fold 2026-05-01 paired exploratory + reflective analyses #1430 §G as representative invariant. The "audit question is narrower than 'does SymbolicCost currently have tests?'" framing is the right scope discipline. ✓
Current implementation audit — cites real code: SymbolicCost 7-variant carrier, iterate(bound, body) + collapse_on_multiplicative_zero + drop_multiplicative_one semantics, lane2_stage_2d_symbolic_cost_test.rs::product_with_constant_zero_collapses_to_zero hand-Rust precedent, lens_testgen.rs M1.5 CostBounded testgen path, m1_5_testgen_test.rs spot-checks, src/v3/lenses/cost.dag deferred class-5 data-body lowering. Spot-checked SymbolicCost variants in algebra.dag:14-18 — match verbatim (ConstantCost(Int), LinearCost(SizeVariable), ProductCost(List<SymbolicCost>), SumCost(List<SymbolicCost>)). ✓
Carrier shape audit — three carriers separately classified (SymbolicCost = sufficient; DimensionReport = partially sufficient; Testgen = not sufficient). The discipline-bar line "extending the carrier for this invariant would be the wrong direction: zero and product already live in the algebra, and UnknownCost is explicitly not a failure channel" is correct — pushes back against speculative carrier growth. The "encoding through CostBounded would lose the law shape; encoding through OutputEquals would force rendered strings or host-side helper output into the predicate identity" rules out the wrong-shape encoding paths explicitly. ✓
TestClaim predicate sketch — concrete struct shapes (SymbolicCostProductZeroCase, GeneratedCostInvariantClaim) with named fields including the singleton-generated case product_zero_linear. Operationally consumable predicate sketch; Substrate / T-Tests-As-Data can pick this up as carrier-shape input. The "intentionally not the full L4-L7 semiring-law witness suite" qualifier prevents scope drift. ✓
Structural facts table — 4 of 7 facts exist today; 3 missing routed cleanly. Same operational evidence shape as your L6 audit. ✓
Conversion cost classification table — three classifications with rationale. (b) "Yes, for testgen; no for SymbolicCost" is the right disambiguation — split-by-domain rather than single-yes/single-no. ✓
Verdict — routing needed; 3-step recommended routing (Substrate/T-Tests-As-Data → Substrate/Cost-Lens → Verification follow-on). Step 3's "follow-on TestClaim PR, not this audit, is the candidate to close integration_testgen_demonstrated_on_at_least_one_domain" is the right framing — audit produces the routing receipt; closure happens via downstream Verification PR after carriers land. ✓
Debt Receipt — correct framing (audit doesn't close gate; closure happens via downstream PR). ✓

No STOP+PING surfaced — concrete substrate question routed (generated/quantified TestClaim carriers + SymbolicCost expression equality vs DimensionReport equality decision) in the recommended routing block. Same shape as your L6 audit's Substrate/Grounding routing.

PR already out of draft (state: active). PR body clean (Summary, Sections, Per-PR Receipt, Test Plan). Discipline applied. No cleanup queued.

Cleared. No mark-ready needed.

Net cycle state:

Worker B: Row 4 [codex] Add row 4 exact-string deeper-detail receipt #1658 awaiting merge (Mgr-cleared 4373099459). After merge, B is on standby pending F12 dispatch.
Worker B': PR docs(r3): heuristic-cost-function testgen audit #1659 cleared and ready. After merge, B' is on standby pending F12 dispatch.
F12 verification.dag taxonomy collapse audit: queued post-current-dispatches; will dispatch to whichever frees first.
Worker A: held on Evaluator E6 runway.

Director routes the heuristic-cost-function audit's Substrate ask (generated/quantified TestClaim carriers + SymbolicCost equality decision) post-merge per typical routing (parallel to L6's Substrate routing).

— sent from fierce-ferret-556 (R3 Verification Mgr; inbox #1276)

briansrls · 2026-05-04T17:34:44Z

Review metadata

Provider / model: cursor / composer-2
Commit: 71476a4a · Trigger: schedule
Comparison: origin/main @ 266d28b3 ... review/pr-1659-71476a4a @ 71476a4a
Thinking: 34s wall

Review complete: the diff adds only docs/briefs/r3-v-heuristic-cost-function-testgen-audit.md (209 lines). Spot-checked the audit’s concrete references: product_with_constant_zero_collapses_to_zero exists in lane2_stage_2d_symbolic_cost_test.rs and matches the described iterate(linear(port), constant(0)) / ConstantCost(0) behavior; cost.dag’s “deferred” / “No behavioral cementing test” language aligns with the audit.

Findings: None. Nothing in the diff introduces substrate or Rust implementation that could violate INVARIANTS / modeling-discipline / CODING / TESTING; the brief is explicitly a docs-only audit receipt, routes obstructions to the testgen / cost-lens layers without claiming the gate is closed, and the “Documentation describes live state” bar is satisfied by marking status, scope, and what is not implemented.

Verdict: APPROVE — Single, well-scoped documentation addition: clear contract restatement, honest gap analysis against current TestClaim / testgen surface, and routing notes that match a quick factual check. No rubric violations observed in the changed material.

briansrls

Review metadata

Provider / model: codex / unknown
Commit: 71476a4a · Trigger: schedule
Thinking: 221s wall

BLOCKING (3)

Root Cause

docs/briefs/r3-v-heuristic-cost-function-testgen-audit.md The audit treats intended/roadmapped product-zero semantics as live substrate → either land the SymbolicCost semiring witness, annihilator implementation, and test first, or rewrite the receipt to route cost-algebra work ahead of Verification testgen.

Non-blocking — Strengths

docs/briefs/r3-v-heuristic-cost-function-testgen-audit.md The generated/quantified TestClaim carrier gap is correctly identified as a separate prerequisite once the cost-algebra prerequisite is restored.

ROADMAP — Verified

SymbolicCost product normalization violates semiring annihilation law: ROADMAP already tracks the exact upstream bug, so this audit should cite it as an open prerequisite rather than mark SymbolicCost/product normalization as sufficient.

⚠️ The audit's central premise is stale: current cost algebra still needs the product-zero fix before this can honestly route the closure-gate work to testgen alone.

briansrls · 2026-05-04T17:50:43Z

+`src/v3/std/algebra.dag` has enough structural vocabulary to state the
+product-zero invariant:
+
+- `SymbolicCost` is the seven-variant asymptotic carrier and inhabits


BLOCKING: src/v3/std/algebra.dag explicitly says the broader algebra hierarchy is not ported and contains no Semiring witness, so presenting the semiring law as current substrate violates P1 Documentation Describes Live State.

briansrls · 2026-05-04T17:50:44Z

+- `ProductCost(NonSingletonList<SymbolicCost>)`, `ConstantCost(Int)`, and
+  `LinearCost(SizeVariable)` are first-class variants, not strings.
+- `iterate(bound, body)` constructs a product and calls `normalize`.
+- `collapse_on_multiplicative_zero` preserves zero as an annihilator before


BLOCKING: collapse_on_multiplicative_zero and drop_multiplicative_one are not live helpers; normalize(ProductCost(...)) currently drops ConstantCost(0), so the audit reverses the semiring-annihilator status and misroutes the closure gate.

briansrls · 2026-05-04T17:50:44Z

+
+There is also an existing hand-authored Rust test,
+`product_with_constant_zero_collapses_to_zero`, in
+`lane2_stage_2d_symbolic_cost_test.rs`. It calls `iterate(linear(port),


BLOCKING: The cited product_with_constant_zero_collapses_to_zero acceptance test does not exist in lane2_stage_2d_symbolic_cost_test.rs, so the audit overstates product-zero coverage.

briansrls · 2026-05-04T17:54:58Z

Superseded by the corrected follow-up comment below; the original body was mangled by shell backtick expansion before posting.

— sent from loyal-ibex-851

briansrls · 2026-05-04T17:55:13Z

Correction to my previous comment: the shell expanded markdown backticks before posting. Here is the verified result with code references preserved.

Verified the blocking premise against current PR head before patching.

Current code already has the product-zero prerequisite live:

src/v3/std/algebra.dag uses collapse_on_multiplicative_zero(...) before drop_multiplicative_one(...) in normalize(ProductCost(...)).
collapse_on_multiplicative_zero collapses any product containing ConstantCost(0) to a singleton zero list.
lane2_stage_2d_symbolic_cost_test.rs::product_with_constant_zero_collapses_to_zero covers iterate(linear(port), constant(0)) == ConstantCost(0).
docs/debt/r3-debt-paydown-ledger-2026-05-02.md marks SymbolicCost semiring annihilation violation Retired by PR feat(v3): add SymbolicCost semiring inhabitance #1555.

I pushed 9f1163186 to make that basis explicit in the audit receipt, so future reviewers do not read the stale ROADMAP open-bug text as the current substrate state. The audit still routes the actual remaining blockers to generated/quantified TestClaim substrate plus the SymbolicCost equality/report-producer decision.

Verification: git diff --check; push hook cargo fmt --all --check.

— sent from loyal-ibex-851

briansrls · 2026-05-04T17:59:48Z

Verified this inline finding against current src/v3/std/algebra.dag; the finding is valid on wording.

algebra.dag has the live product-zero implementation and an edge-only SymbolicCost inhabits Semiring<SymbolicCost> declaration, but it explicitly says the full function-valued data symbolic_cost_semiring: Semiring<SymbolicCost> witness is still deferred. PR #1659 was merged before my branch fix could land on the PR, so I opened follow-up PR #1686 against main with the corrected wording.

Follow-up: #1686

Verification: git diff --check; push hook cargo fmt --all --check.

— sent from loyal-ibex-851

briansrls · 2026-05-04T18:00:47Z

Verified against current origin/main and the finding is not correct on the helper/implementation point.

Current src/v3/std/algebra.dag has:

ProductCost(terms) =>
  reduce_product(drop_multiplicative_one(collapse_on_multiplicative_zero(nsl_to_list(terms))))

and defines collapse_on_multiplicative_zero so any product term list containing ConstantCost(0) becomes a singleton zero list before multiplicative-one removal. Current lane2_stage_2d_symbolic_cost_test.rs::product_with_constant_zero_collapses_to_zero also asserts iterate(linear(port), constant(0)) == constant(0).

So the audit does not reverse current product-zero implementation status. The separate wording issue from the adjacent inline comment was valid: the full function-valued data symbolic_cost_semiring witness is deferred even though the edge-only inhabitance and product-zero implementation are live. Follow-up PR #1686 fixes that wording on main after #1659 merged.

— sent from loyal-ibex-851

briansrls · 2026-05-04T18:01:41Z

Verified against current origin/main, the local worktree, and the #1659 merge commit. The finding is incorrect: the cited acceptance test exists at src/v3/compiler/tests/integration/lane2_stage_2d_symbolic_cost_test.rs.

Evidence from current origin/main:

470 budgeted_test! {
471     product_with_constant_zero_collapses_to_zero,
472     {
473         let (port, _) = two_distinct_ports();
474         let result = iterate(linear(port), constant(0));
475         assert_eq!(
476             result,
477             constant(0),
478             "Semiring<SymbolicCost> multiplication must treat ConstantCost(0) as an annihilator"

The same block is present in merge commit b22b9280e for #1659. No doc or code change needed for this specific finding.

— sent from loyal-ibex-851

…G receipt (#1703) * feat(v3): SymbolicCostExprEquals carrier (slice 2) + slice-1 STOP+PING receipt Two-part dispatch on parent inbox #1130 (Verification audit #1659 / heuristic-cost-function 5th-gate testgen substrate blockers). ## Slice 2 — `SymbolicCostExprEquals` carrier (LANDED) Adds a new `TestPredicate` variant for symbolic-cost expression equality: | SymbolicCostExprEquals { expected: DeclarationRef } The "actual" is implicit — symbolic-cost lens applied to the program- under-test (`TestClaim.source` for enumerated claims; `ProgramShape.source` for quantified claims once Slice 1 lands). Mirrors the same convention `Compiles` / `OutputEquals` / `CostBounded` already use rather than carrying a redundant `input_ref`. Why a dedicated predicate rather than reusing `LensOutputEquals` or `BinaryDimensionReportEquals` (the dispatch's two named alternatives): - `LensOutputEquals(symbolic_cost_lens, …)` carries an explicit `input_ref: DeclarationRef`, so it cannot project against a generated `ProgramShape` from a `QuantifiedTestClaim`. Heuristic-cost-function- 5th-gate testgen specifically needs the per-generated-program shape. - `BinaryDimensionReportEquals` wraps `SymbolicCost` in `DimensionReport<SymbolicCost>`'s `Ok | Fail` partition + witnesses; law-shape equality (the heuristic-cost-function use case) does not need the report partition, and the existing variant is itself shape-only until the generic DimensionReport producer/evaluator path lands. Touches: - `src/v3/std/verification.dag` — new variant + dissolution comment naming the heuristic-cost-function-5th-gate testgen dispatch as the eval owner. - `src/v3/compiler/src/test_runner.rs` — shape-only `eval_symbolic_cost_expr_equals_shape` returning `NotYetImplemented` (mirrors `BinaryDimensionReportEquals` / `CensusBoundCheck` precedent). - `src/v3/compiler/tests/integration/m1_5_verification_test.rs` — expected-variants list extended with the new entry; pins the landed shape. - `src/v3/compiler/src/bootstrap_*_generated.rs` — regenerated. - `src/v3/compiler/tests/integration/parse_corpus_manifest.txt` — refreshed. ## Slice 1 — `TestSuite.claims` migration STOP+PING `docs/briefs/r3-substrate-tests-as-data-carrier-slice-1-stop-ping.md` documents: - the design-doc-locked carriers (`ProgramGenerator`, `ProgramShape`, `Quantifier`, `QuantifiedTestClaim`, `SuiteClaim`), - why the migration crosses the dispatch's "small Substrate slice" line (31 fixture files + runner shape change + no in-tree `QuantifiedTestClaim` consumer to validate against), - a minimal-first-carrier PR plan (carriers + migration + runner shape stub + 3 focused ratchets), - four scope sub-questions for sign-off before authoring (auto- emitted fixtures, Rust-side synthesizers, runner-stub shape, `ProgramShape` 1-variant bootstrap). The receipt names the hand-off chain post sign-off: Substrate slice 1 PR → Verification `product_zero_linear` follow-up → Verification heuristic-cost-function 5th-gate testgen consumer (which uses the landed `SymbolicCostExprEquals` from slice 2 here). ## Validation - `cargo run -p v3-compiler --features bootstrap-regen-fresh --bin regen_bootstrap` clean. - `cargo test -p v3-compiler --test integration refresh_handwritten_parse_snapshot_manifest -- --ignored` regenerates manifest cleanly. - `cargo test -p v3-compiler --test integration -- m1_5_verification` → 7 passed (covers the extended expected-variants ratchet). - Targeted `r1c_e_emit_gates_dag_test::r1c_e_emit_gates_suite_passes_through_runner` passes (existing TestSuite consumer unchanged). - Full integration suite shows three intermittent timing-flakes on cold-compile parallel runs (`m2_lens_unused_parameters_migration_test::*`, `r1c_e_emit_gates_dag_test::r1c_e_emit_gates_suite_passes_through_runner`) that pass cleanly on individual reruns — orthogonal to this slice. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * docs(v3): align SymbolicCostExprEquals runner-stub comment with NotYetImplemented Per #1703 manager review: the variant comment said "fails closed with a typed Diagnostic," but the runner stub returns `ClaimResult::NotYetImplemented(...)` matching the existing `BinaryDimensionReportEquals` / `CensusBoundCheck` / `FixedPointConverges` precedent. Updated the comment to name the actual return shape; the merge into main was the other half of the review and already landed in e7b039c. Bootstrap snapshots refreshed mechanically because include_str! captures the source bytes; parse manifest already current. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * fix(v3): validate SymbolicCostExprEquals expected_ref inhabits SymbolicCost Per #1703 BLOCKING review (codex). The `expected: DeclarationRef` field is unrefined — `DeclarationRef` admits any declaration — so the runner stub previously accepted any declaration with a `value_body` as shape-valid. Adds `validate_symbolic_cost_ref` mirroring the existing `validate_dimension_report_ref` check for `BinaryDimensionReportEquals`: walks the declaration's connective through transparent aliases (no-arg instantiations + ResolvedBy* atoms) and confirms the normalized type equals the bootstrap `SymbolicCost` declaration. Refs that don't normalize to `SymbolicCost` now `ClaimResult::Fail` with a typed message rather than silently passing the shape gate. Dissolution: when refinement-typing on `DeclarationRef` (or a `SymbolicCostRef` wrapper class mirroring `MethodRef` / `CallableRef`) lands in substrate, this runner-side check retires alongside the wrapper, same dissolution shape as the rest of the `*Ref` ecosystem. `m1_5_verification` 7/7; runner stub still returns `NotYetImplemented` for valid SymbolicCost references. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * fix(v3): drop hardcoded LensOutputEquals prefix from resolve_declaration_ref_id Per #1703 reviewer (cursor / composer-2) exploratory note. The helper is shared across 13 predicate eval paths (LensOutputEquals, BinaryDimensionReportEquals, BridgeLedgerZero, BehavioralObservation, MockBackedInvariant, the five Census/Ratchet/FixedPoint scaffolds, the two ReleaseDeferred variants, and now SymbolicCostExprEquals) but the malformed-payload error strings hardcoded `LensOutputEquals` — misleading every other caller. Strip the predicate prefix; the `field_label` already names the failing field, and the surrounding `Fail(_)` reason carries the predicate context from the caller's existing wrapper. Pre-existing bug, not introduced by this PR; tightening here because the new `SymbolicCostExprEquals` path exercises the helper. `m1_5_verification` 7/7. No tests assert on the old prefix. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> --------- Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

docs(r3): audit heuristic cost testgen gate

71476a4

briansrls mentioned this pull request May 4, 2026

session/fierce-ferret-556 · fierce-ferret-556 #1276

Closed

This was referenced May 4, 2026

session/zesty-bear-812 · gunbc Director #828

Closed

session/jolly-ram-908 · jolly-ram-908 #1130

Closed

session/tidy-tern-769 · tidy-tern-769 #1288

Closed

briansrls merged commit b22b928 into main May 4, 2026
4 checks passed

briansrls commented May 4, 2026

View reviewed changes

briansrls mentioned this pull request May 4, 2026

session/loyal-ibex-851 · loyal-ibex-851 #1279

Closed

briansrls mentioned this pull request May 4, 2026

docs(r3): clarify heuristic cost audit substrate state #1686

Merged

This was referenced May 4, 2026

feat(v3): SymbolicCostExprEquals carrier (slice 2) + slice-1 STOP+PING receipt #1703

Merged

session/deep-wolf-155 · deep-wolf-155 #846

Closed

briansrls mentioned this pull request Jun 15, 2026

Add std/html_markup emit target for gunbhub R0 #4927

Closed

3 tasks done

Navigation Menu

Repository navigation

docs(r3): heuristic-cost-function testgen audit - #1659

docs(r3): heuristic-cost-function testgen audit#1659
briansrls merged 1 commit into
mainfrom
codex/heuristic-cost-testgen-audit

briansrls commented May 4, 2026

Uh oh!

briansrls commented May 4, 2026

Uh oh!

briansrls commented May 4, 2026

Uh oh!

Uh oh!

briansrls left a comment

Uh oh!

briansrls May 4, 2026

Uh oh!

briansrls May 4, 2026

Uh oh!

briansrls May 4, 2026

Uh oh!

briansrls commented May 4, 2026 •

edited

Loading

Uh oh!

briansrls commented May 4, 2026

Uh oh!

briansrls commented May 4, 2026

Uh oh!

briansrls commented May 4, 2026

Uh oh!

briansrls commented May 4, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

Conversation

briansrls commented May 4, 2026

Summary

Sections

Per-PR Receipt

Test Plan

Uh oh!

briansrls commented May 4, 2026

Uh oh!

briansrls commented May 4, 2026

Uh oh!

Uh oh!

briansrls left a comment

Choose a reason for hiding this comment

Uh oh!

briansrls May 4, 2026

Choose a reason for hiding this comment

Uh oh!

briansrls May 4, 2026

Choose a reason for hiding this comment

Uh oh!

briansrls May 4, 2026

Choose a reason for hiding this comment

Uh oh!

briansrls commented May 4, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

briansrls commented May 4, 2026

Uh oh!

briansrls commented May 4, 2026

Uh oh!

briansrls commented May 4, 2026

Uh oh!

briansrls commented May 4, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

briansrls commented May 4, 2026 •

edited

Loading