Repository navigation
docs(T-PB-B-2): predicate-gapped G list for Testgen backlog - #727
Conversation
Non-landing brief. Enumerates the seven TestPredicate schema shapes needed to port the pipe_desugar-style G bucket (structural queries over the post-compile Dag) to .dag TestClaim values. Feeds Testgen manager backlog; no Rust deletion, no .dag drafts until Testgen schema lands or pre-approves. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
|
Review metadata
Verdict: APPROVE — docs-only brief adding a new non-landing file under |
|
Review metadata
Findings:
Verdict: APPROVE_WITH_COMMENTS — The brief is bounded, non-landing, and mostly consistent with the modeling/testgen direction. I’d tighten the diagnostic-phase gap before it becomes schema work. |
DiagnosticReference.kind already discriminates ParseError vs later phases (test_runner.rs:402) and FailsWithDiagnostic matches on it. A phase-pinning predicate would create a second authority for diagnostic phase, against INVARIANTS P2. Phase-pinning G tests move to the D bucket; list drops to six shapes. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
|
Review metadata
APPROVE — Docs-only addition of a single brief at |
|
Review metadata
Findings
Verdict |
Feedback (T-PB-B-2 / Testgen backlog)What works well
Small doc fixes before merge
Optional follow-ups (non-blocking)
Thanks — this is useful, actionable backlog input for the Testgen manager without touching code paths. |
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
…e shapes Codex reviewer flagged the 'ships today' list as risking a second schema authority. Split into (a) variants declared in src/v3/std/verification.dag vs (b) variants the runner evaluates today, pointing at verification.dag as the single authority. Also label the needs-schema header as 'six live shapes' for grep-consistency after the #7 retraction. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
|
Review metadata
Findings
Verdict APPROVE_WITH_COMMENTS — docs-only, non-landing brief; respects the "authority is |
|
Review metadata
Findings
Verdict: APPROVE_WITH_COMMENTS. The brief otherwise looks narrowly scoped and careful about avoiding second schema authority. |
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
briansrls
left a comment
There was a problem hiding this comment.
Review metadata
- Provider / model:
codex/unknown - Commit:
f6a0296d· Trigger:schedule - Thinking:
217s wall
BLOCKING (1)
Root Cause
docs/briefs/pb-b-2-predicate-gapped-g-list.mdrunner status was inferred from manager shorthand rather than verified against the actual runner dispatch table → update "What ships today" to distinguish schema-declared, runner-dispatched, and NYI predicates from src/v3/std/verification.dag and src/v3/compiler/src/test_runner.rs.
| Scaffold marker): `Compiles`, `FailsWithDiagnostic`, | ||
| `ExecuteCommand`, `ForAllTargets`, `LensOutputEquals`, | ||
| `DifferentialEquals`, `AlgebraicLaw`, `MockBackedInvariant`. | ||
| - **Runner-wired today** (per r1-testgen-manager working state): |
This comment was marked as resolved.
This comment was marked as resolved.
Sorry, something went wrong.
|
Review metadata
Docs-only brief. Non-landing, clearly scoped, no code changes. Verdict: APPROVE — pure documentation addition (one brief under |
|
Review metadata
Findings
Verdict: REQUEST_CHANGES. The brief is otherwise narrowly scoped and has the right authority-split framing, but the “what ships today” inventory needs to match the live schema/runner state before this becomes backlog input. |
Codex review flagged the "Runner-wired today" list as inferred from manager shorthand rather than verified against the actual dispatch table. Audit of src/v3/compiler/src/test_runner.rs:101 shows the runner matches five labels: Compiles, FailsWithDiagnostic, OutputEquals, PortHasState, CostBounded — everything else (including ExecuteCommand, ForAllTargets, LensOutputEquals, DifferentialEquals, AlgebraicLaw, MockBackedInvariant) returns NotYetImplemented. Update the brief to name three buckets explicitly: schema-declared, runner-dispatched, and schema-declared-but-NYI. Also tighten the D-bucket definition to "predicates the runner dispatches today" so runner-NYI predicates route to Testgen's runner-wiring backlog instead of being miscounted as directly portable. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
|
Verified finding against code and fixed in 0210229. Audit result: reviewer is correct. Runner dispatch at Fix: three explicit buckets in "What ships today" — schema-declared (11 variants in verification.dag), runner-dispatched (5, with file:line cite), schema-declared-but-NYI (6). Also tightened the D-bucket intro so runner-NYI predicates route to Testgen's runner-wiring backlog rather than being miscounted as directly portable. |
|
Review metadata
APPROVE — docs-only brief, narrowly scoped, explicitly non-landing. The author correctly splits schema-declared vs runner-dispatched authority (citing |
|
Review metadata
Findings
Verdict: REQUEST_CHANGES. The brief is narrowly scoped, but it currently codifies two schema-authority mistakes in the handoff document. Fixing those should be small: remove |
Codex review flagged two schema-authority mistakes: 1. Proposed predicate shapes repeated `program` inside TestPredicate, conflicting with the single-authority rule at verification.dag:169 where TestClaim.source / file_name name the program under test. Drop `program` from all six shapes and add an explicit "Program authority" note pointing at the enclosing claim. 2. The schema-declared list omitted `BehavioralObservation` (verification.dag:94). Add it to schema-declared and to the runner-NYI bucket so the brief mirrors the live schema. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
|
Both findings verified and fixed in 1a8cf75.
|
|
Review metadata
Docs-only PR. Content is self-consistent, cites real file:line authority ( Verdict: APPROVE — docs-only brief, no code, no substrate change. Authority splits are clean (schema = |
|
Review metadata
Findings:
Verdict: APPROVE_WITH_COMMENTS. The brief is otherwise narrow, explicitly non-authoritative, and avoids the program-authority duplication issue; I only see the missing count operand as worth tightening before Testgen consumes it. |
Non-blocking codex finding: the proposed shape declared only behavior_kind + count_rel, leaving the runner with no value to compare against. Add count: non-negative integer so the predicate carries sufficient boundary information for Testgen to evaluate. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
briansrls
left a comment
There was a problem hiding this comment.
Review metadata
- Provider / model:
codex/unknown - Commit:
02102293· Trigger:schedule - Thinking:
383s wall
BLOCKING (2)
Root Cause
docs/briefs/pb-b-2-predicate-gapped-g-list.mdpipe_desugar helper patterns were reduced to bind-rooted target/literal checks, dropping input-producer path facts → add a predicate that can name a root bind plus producer path/target, or narrow the unlock claim to only the direct cases.docs/briefs/pb-b-2-predicate-gapped-g-list.mdcount comparison was sketched as a local helper label instead of reusing the existing comparison-plus-bound shape from CostBounded → model it as behavior_kind plus ComparisonOp plus Int bound.
| - `m2_field_access_binding_test.rs` — #1 #2 #3 | ||
| - `m2_lens_cost_migration_test.rs` / `m2_lens_idempotency_*` / | ||
| `m2_lens_unused_parameters_migration_test.rs` / | ||
| `m2_lens_variant_payload_migration_test.rs` — #1 #2 #6 |
This comment was marked as resolved.
This comment was marked as resolved.
Sorry, something went wrong.
| imperative walks block port. | ||
|
|
||
| 5. **`DeclarationResolvedByStructure { program, name }`** — closes | ||
| the `AtomPayload::ResolvedByStructure(..)` / `ResolvedByName(..)` |
This comment was marked as resolved.
This comment was marked as resolved.
Sorry, something went wrong.
Blocking codex finding: shapes #2/#3 as authored started from a named Bind and reached only its direct inputs, so they could not express the nested producer chains in 3 of the 5 pipe_desugar tests — pipe_chains_left_to_right (outer double → inner add1), pipe_result_can_feed_later_addition (+ → negate), and pipe_result_can_feed_later_comparison (== → identity). The brief claimed those tests were covered, violating live-state accuracy. Generalize #2 and #3 with a producer_path: List<PortIndex> so the predicate walks value.produced_by → inputs[path[0]].produced_by → … (empty path = direct producer, which keeps the single-stage tests working without change). Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
|
Finding verified and fixed in eb63b97. Audit: reviewer is right. In pipe_desugar.rs, three of the five tests chain through nested
Shapes #2 and #3 as authored started from the bind and only reached direct inputs, so listing pipe_desugar as covered by #1/#2/#3/#5 overclaimed. Fix: generalize #2 and #3 with a |
Blocking codex finding: the prior shape introduced a new count_rel axis (Equals | AtLeast | AtMost) parallel to ComparisonOp, which is already declared at src/v3/std/substrate.dag:141 and consumed by CostBounded at verification.dag:91. That's parallel-representation debt against an existing single authority. Replace count_rel with comparator: ComparisonOp so the predicate reuses the authoritative operator enum. The count operand remains as added in the prior fix. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
|
Review metadata
Docs-only addition of a design brief. No code or schema changes; purely informational backlog for Testgen. Verdict: APPROVE — docs-only brief, narrowly scoped, carefully cross-references the authoritative schema ( |
|
Review metadata
Findings
Verdict: REQUEST_CHANGES. The split between schema-declared, runner-wired, and predicate-gapped tests looks otherwise consistent with the current runner/schema, but the new backlog brief should not introduce nonexistent carrier names while claiming it does not. |
Codex finding: the brief referenced OpKind and PortIndex, neither of which is the live carrier name. substrate.dag:160 declares OperatorKind; ports are PortId (substrate.dag:5), and Transform.inputs is List<PortId> (substrate.dag:267), so a producer-path step is a plain Int list index, not a distinct PortIndex type. Rename OpKind → OperatorKind in shape #2; respecify producer_path as List<Int> with a cite to the inputs field; update the "no new carrier types" non-ask to list the actual live names with file:line cites. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
|
Finding verified and fixed in 1a0ca55. Audit: live authority is Fix: renamed |
|
Review metadata
APPROVE — Pure docs PR adding a non-landing brief enumerating predicate-gapped tests. It's internally consistent: cites live authorities ( |
|
Review metadata
Verdict: APPROVE — this is a docs-only backlog brief, and it stays disciplined about single authority: schema lives in |
briansrls
left a comment
There was a problem hiding this comment.
Review metadata
- Provider / model:
codex/unknown - Commit:
1a0ca55a· Trigger:schedule - Thinking:
273s wall
BLOCKING (1)
Root Cause
docs/briefs/pb-b-2-predicate-gapped-g-list.mdmodule-level bucketing collapsed distinct assertion shapes → rewrite the unlock section per assertion family or add the missing predicate shapes before claiming these modules are covered
| gap, not as a phase-pinning predicate. | ||
|
|
||
| ## G-modules this list unlocks (non-exhaustive) | ||
|
|
There was a problem hiding this comment.
BLOCKING: The module unlock list overclaims coverage: entries like m2_field_access_binding_test.rs, m1_fn_external_body_reconciliation_test.rs, and the SG authority tests assert FieldBinding/ArrowBody/snapshot/harness facts that are not expressible by the six listed predicates, so the brief no longer describes the live G backlog accurately.
Blocking codex finding: the unlocks list overclaimed coverage. m2_field_access_binding_test.rs asserts on TypeRealization[_].FieldBinding[_] records (declaration-level, not Bind-rooted). m1_fn_external_body_reconciliation_test.rs discriminates ArrowBody::ExternalRealization vs Unparsed (also declaration-level). The SG authority tests are snapshot-drift and rustc-harness runs, not post-compile substrate queries. Split the section into two lists: modules the six shapes actually cover (Bind/Transform/port walks), and modules needing additional predicates (FieldBindingEquals, ArrowBodyKindIs) or routing to the runner-NYI ExecuteCommand/ForAllTargets path. Retract the >60% module-count claim, which was inflated by the overclaimed modules. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
|
Finding verified and fixed in 7e324d7. Audit: reviewer is right — the unlocks list overclaimed.
Fix: split the section in two. The first list keeps only modules the six shapes actually cover (Bind/Transform/port walks). The second list names the overclaimed modules with the specific additional predicates they need ( |
|
Review metadata
APPROVE — docs-only brief, adds a scoped backlog document with clear authority pointers (verification.dag, test_runner.rs:101, substrate.dag lines), explicitly avoids forking authority (program field, ComparisonOp reuse), and honestly retracts/narrows prior claims. No code changes; nothing in this diff touches substrate, runner, or schema. No violations observed. |
|
Review metadata
Verdict: APPROVE Docs-only diff is narrowly scoped, and the brief keeps |
Summary
docs/briefs/pb-b-2-predicate-gapped-g-list.md— the T-PB-B-2 "needs schema" 1-pager.TestPredicateshapes (seventh retracted per codex review —DiagnosticReference.kindis already the single authority for phase) needed to port thepipe_desugar.rs-style G bucket (post-compile structural queries) to.dagTestClaimvalues.main(declared insrc/v3/std/verification.dag) from runner-wired variants, pointing atverification.dagas the single schema authority..dagdrafts until Testgen schema lands.Test plan
🤖 Generated with Claude Code