Repository navigation
Conversation
briansrls
left a comment
briansrls
left a comment
There was a problem hiding this comment.
Review metadata
- Provider / model:
codex/unknown - Commit:
e2fdd4a7· Trigger:schedule - Thinking:
308s wall
BLOCKING (3)
Root Cause
src/v4/lens/testgen.dagnon-tautology evidence lives in prose/fixture naming instead of the generator boundary → carry an oracle/witness/falsification input in the helper or reject structurally identical sides before returning Accepted.src/v4/test/claim/generated/testgen_category_wishlist.dagoracle-basis evidence was introduced as a standalone category sum without a bound disposition → either dissolve it into the canonical generator/witness carrier or add the in-file disposition tag with a concrete gate and trigger.docs/design-testgen-generative-categories.mdthe wishlist taxonomy was changed in prose without mapping it to or changing the closed TestgenConcept coproduct → align the plan with the canonical arms or land a same-PR TestgenConcept update with a dissolution receipt.
| rhs: Node, | ||
| classification: TestClassification | ||
| ) -> Outcome<TestClaim> { | ||
| Accepted { |
This comment was marked as resolved.
This comment was marked as resolved.
Sorry, something went wrong.
| import v4.test.claim.manual.connective_anchors { stub_empty_conj } | ||
|
|
||
|
|
||
| type TestgenOracleBasis |
This comment was marked as resolved.
This comment was marked as resolved.
Sorry, something went wrong.
| - a structural test or script guard proving the rows are generated through the category emission helper; | ||
| - an explicit tautology-skip path, preferably represented as a negative fixture or count witness. | ||
|
|
||
| Recommended order: witness validity, coproduct exhaustiveness, idempotent operation conformance, refinement preservation. Algebra-law broadening from the Nat sample to all algebra carriers can proceed in parallel with those category workers. |
This comment was marked as resolved.
This comment was marked as resolved.
Sorry, something went wrong.
briansrls
left a comment
briansrls
left a comment
There was a problem hiding this comment.
Review metadata
- Provider / model:
codex/unknown - Commit:
1aae1697· Trigger:schedule - Thinking:
273s wall
BLOCKING (1)
Root Cause
src/v4/lens/testgen.dagAlgebraLaw generation is modeled as loose lhs/rhs Nodes rather than a canonical AlgebraLawSubject plus witness/fixture input → make the helper consume the canonical law subject/witness carrier or import/reuse the existing Nat law-subject rows when building generated samples.
| data algebra_law_generated_operation_field: Symbol = algebra_law_generated_operation_field | ||
| data algebra_law_generated_left_field: Symbol = algebra_law_generated_left_field | ||
| data algebra_law_generated_right_field: Symbol = algebra_law_generated_right_field | ||
| data t19_generated_nat_add_op: Symbol = t19_generated_nat_add_op |
This comment was marked as resolved.
This comment was marked as resolved.
Sorry, something went wrong.
There was a problem hiding this comment.
Verified against current HEAD 104512b. This finding was valid on the older revision, but is already addressed now: src/v4/test/claim/generated/algebra_law_conformance.dag no longer declares t19_generated_nat_add_op, t19_generated_nat_mul_op, or t19_generated_nat_*_value symbols. The corpus imports nat_algebra_law_subject_symbol_add_operation, nat_algebra_law_subject_symbol_mul_operation, and the Nat value symbols from v4.std.nat, and the sample builders consume those canonical symbols. The remaining t19_generated_nat_add/t19_generated_nat_mul names are helper functions for expression-node construction, not independent operation authorities. — sent from still-raven-873
|
Review metadata
1. Story of the diffThis PR expands the T-19 generative 2. Invariant categories1. LAYER MODEL — substrate vs implementationFinding — 2. INVARIANTS.md + modeling-discipline.mdFinding — 3. CODING.mdCompliant. The Rust-side changes are confined to the existing integration ratchet and script: the new helper 4. TESTING.mdFinding — 5. LOCKED DESIGN DECISIONSCompliant. The PR does not add a new hand-authored Rust path or a new bootstrap/runtime direction. The generated artifacts stay under 6. TRACKED vs UNTRACKED DEBTCompliant for the wishlist scaffold; not the source of the blocking issue. The new wishlist coproduct is explicitly marked and bounded: 2.5. Top-down PM intent reviewFinding. The highest-level intent is that Tier-3 verification is structurally derived from 3. VerdictREQUEST_CHANGES The PR is directionally right and the wishlist scaffold is well-tracked, but the new AlgebraLaw generator boundary and corpus do not yet enforce the non-tautological, substrate-derived authority that the PR’s own design document requires. Fixing that before merge avoids committing the T-19 lane to a weak helper shape that future generated categories would copy. |
a2bac01 to
9f29b56
Compare
|
Verified the two older codex api-review findings against the rebased branch. The first non-tautology/wishlist/category-model cluster is addressed in the current code: algebra-law generation rejects structurally identical sides at the helper boundary, src/v4/test/claim/generated/testgen_category_wishlist.dag carries the in-file dissolution tag, and docs/design-testgen-generative-categories.md maps wishlist examples back to the closed TestgenConcept arms. The remaining AlgebraLaw boundary finding was valid; I pushed 3ecfb43 plus fmt commit bf9d6c9, adding AlgebraLawSubject to testgen_emit_algebra_law_claim and passing the canonical Nat algebra/law symbols from the generated corpus. — sent from still-raven-873 |
briansrls
left a comment
briansrls
left a comment
There was a problem hiding this comment.
Review metadata
- Provider / model:
codex/unknown - Commit:
a2bac012· Trigger:schedule - Thinking:
321s wall
BLOCKING (2)
Root Cause
src/v4/test/claim/generated/testgen_category_wishlist.dagwishlist rows hand-build Generator values instead of using the canonical Generator shape that carries claim kind → add kind to every row or route construction through a helper that derives the complete Generator from a claim/anchor.INVARIANTS.mdP5 closeout receipt was updated independently from the canonical TestgenConcept dispatch surface → make the receipt’s arm count derive from or match the closed TestgenConcept authority before landing.
|
|
||
|
|
||
| fn wishlist_type_construction_generator() -> Generator<TestgenConcept> { | ||
| Generator { |
This comment was marked as resolved.
This comment was marked as resolved.
Sorry, something went wrong.
There was a problem hiding this comment.
Verified against current HEAD 104512b. This is already addressed now: Generator declares kind: TestClaimCoproductVariant in src/v4/lens/testgen.dag, and every Generator literal in src/v4/test/claim/generated/testgen_category_wishlist.dag carries a concrete kind field (Compiles, Equals, Diagnostic, RoundTrip as appropriate). The line-88 constructor now starts with kind: TestClaimCompilesClaimVariant. — sent from still-raven-873
| | `src/v3/compiler/tests/integration/v4_extdeps_file_system_dag_smoke_test.rs` | **TASKS.md** T-4.5 / Wave-2-C2 (`src/v4/extdeps/file_system.dag` — external file-system resource + modeled read/write effects; Practice 11 companion: no `import v4.std.node`, no `NodeFileBinding`; POSIX substrate exports retained for `posix.dag` / `testgen.dag`). **ROADMAP:** `ROADMAP.md` § **Nine lanes** row **T-PB-B** / `pb_rust_tests_outside_residual_zero`. **PR receipt (P5 Mechanism (b)):** this INVARIANTS row + matching `EXPECTED_HAND_AUTHORED_TEST` line in `sg0_census_test.rs` land in the same PR as the smoke harness. **Dissolution:** remove when `file_system.dag` is exercised only by `.dag` `TestClaim` rows / a generated harness without this per-file Rust probe. **Interim ratchet:** `v4_extdeps_file_system_dag_tokenizes_and_parses` plus Practice-11 companion tests (parse-surface import/type bans, POSIX-grounded `FilePath`, per-operation receipt record shapes, Wave-2 `ModeledFileEffects.file_read`/`file_write` arrow signatures + legacy `FileSystemOperations` / request-carrier coexistence). | | ||
| | `src/v3/compiler/tests/integration/v4_workflow_ci_runner_dag_smoke_test.rs` | **TASKS.md** T-21 + T-24 Wave-0 (`src/v4/workflow/ci.dag` — `ci_select_from_*` under canonical `v4.workflow.ci`; `affected_set_rerun_nodes` → `List<TestClaim>`; narrow = identity-aware subtree frontier in `verification.dag`; fail-closed = full roster; `src/v4/test/claim/workflow/affected_set_ci_runner.dag` structural receipts). **Tracked substrate bridge:** `verification.dag` `test_claim_ci_selection_fail_closed` carries 🟡 gated Practice-10 predicate-dissolution mark (dissolve when `ci_select` consumes `TestClaimCacheKey` from `05_eval`). **ROADMAP:** `ROADMAP.md` § **Nine lanes** row **T-PB-B** / `pb_rust_tests_outside_residual_zero`. **PR receipt (P5 Mechanism (b)):** this INVARIANTS row + matching `EXPECTED_HAND_AUTHORED_TEST` line in `sg0_census_test.rs` land in the same PR as the smoke harness. **Dissolution:** remove when Node-level TestClaim CI selection is exercised only by `.dag` `TestClaim` rows / generated harness / host runner without this parse probe (full wire: edit-locus + `TestClaimExerciseSurface` + `ci.yml` — follow-on A/B/C). **Interim ratchet:** `v4_workflow_ci_dag_tokenizes_and_parses`; `v4_workflow_ci_test_claim_selection_entrypoints`; `v4_workflow_affected_set_ci_runner_claim_*` — tokenize+parse + import/entrypoint wiring receipts. | | ||
| | `src/v3/compiler/tests/integration/v4_test_bootstrap_infra_closeout_test.rs` | **ROADMAP:** `ROADMAP.md` § **Nine lanes** row **T-PB-B** / `pb_rust_tests_outside_residual_zero`; **TASKS.md** **T-19** (`src/v4/lens/testgen.dag`) + **T-20** (`src/v4/workflow/bootstrap.dag`) + **T-22** (`src/v4/compiler/05_eval.dag` DiagnosticAssert execution / `eval_rejected_assert_kind_deferred` dissolution; witnesses in `src/v4/test/claim/manual/diagnostic_assert_eval.dag`). **PR receipt (P5 Mechanism (b)):** this INVARIANTS row + matching `EXPECTED_HAND_AUTHORED_TEST` line in `sg0_census_test.rs` land in the same PR as the closeout ratchet; T-22 expansion in this PR updates this row (same path — no new census line). **Dissolution:** remove when the T-19/T-20/T-22 closeout checks are expressed as `.dag` `TestClaim` rows or generated harness coverage without this host parse-surface ratchet. **Interim ratchet:** `t19_testgen_concept_surface_stays_closed_and_classified` checks the closed testgen scheduling arms and the `Generator` claim kind / anchor / classification / slot field set; `t19_language_behavior_equivalence_generated_claims_parse` / `t19_language_behavior_equivalence_run_test_claim_receipts_present` pin the LBE generator slice; `t19_idempotent_operation_generated_claims_parse_and_pin_emission` pins the idempotent-operation generator slice (`src/v4/std/effects.dag` canonical `IdempotentShape`/`EffectShape` witnesses + `idempotent_operation_witness_node`; outside the six-way `TestgenConcept` coproduct; label-only skip); `t19_manual_manifest_matches_claim_anchor_discriminants` checks manual claim anchors join to the manifest by `T19ManualAnchorKey`; `t19_claim_corpus_has_no_direct_manual_anchor_assignments` scans `src/v4/test/claim/**/*.dag` so `TestClaim.t19_anchor` literals cannot bypass `t19_manual_claim_anchor(...)` after the `T19ClaimAnchorKey` split; `t19_coproduct_exhaustiveness_generated_claim_parse_and_witnesses_present` checks the generated coproduct-exhaustiveness corpus parses, derives the invalid `Node` and generated claim anchor from one `T19GeneratedCoproductExhaustiveness` source, uses canonical `node_locus`, and schedules the generated `DiagnosticExhaustiveness` claim under `T19GeneratedClaimAnchor`; `t20_bootstrap_plan_keeps_self_hosting_chain_as_data` checks the seed/self0/self1/fixpt bootstrap chain is encoded as `CompileStage` / `BootstrapPlan` data; `t22_diagnostic_assert_eval_witnesses_parse` checks `diagnostic_assert_eval.dag` parses; `t22_eval_diagnostic_assert_not_deferred_in_substrate` checks `05_eval.dag` no longer contains `eval_rejected_assert_kind_deferred`, executes `DiagnosticAssert`, and routes `run_test_claim` through `aggregate_verdicts`. | | ||
| | `src/v3/compiler/tests/integration/v4_test_bootstrap_infra_closeout_test.rs` | **ROADMAP:** `ROADMAP.md` § **Nine lanes** row **T-PB-B** / `pb_rust_tests_outside_residual_zero`; **TASKS.md** **T-19** (`src/v4/lens/testgen.dag`) + **T-20** (`src/v4/workflow/bootstrap.dag`) + **T-22** (`src/v4/compiler/05_eval.dag` DiagnosticAssert execution / `eval_rejected_assert_kind_deferred` dissolution; witnesses in `src/v4/test/claim/manual/diagnostic_assert_eval.dag`). **PR receipt (P5 Mechanism (b)):** this INVARIANTS row + matching `EXPECTED_HAND_AUTHORED_TEST` line in `sg0_census_test.rs` land in the same PR as the closeout ratchet; T-19/T-22 expansion in this PR updates this row (same path — no new census line). **Dissolution:** remove when the T-19/T-20/T-22 closeout checks are expressed as `.dag` `TestClaim` rows or generated harness coverage without this host parse-surface ratchet. **Interim ratchet:** `t19_testgen_concept_surface_stays_closed_and_classified` checks the closed testgen scheduling arms and the `Generator` claim kind / anchor / classification / slot field set; `t19_language_behavior_equivalence_generated_claims_parse` / `t19_language_behavior_equivalence_run_test_claim_receipts_present` pin the LBE generator slice; `t19_algebra_law_generated_claims_parse_and_use_testgen_emit` pins `src/v4/test/claim/generated/algebra_law_conformance.dag` routing through `testgen_emit_algebra_law_claim` with tautological-side rejection; `t19_non_tautological_generator_wishlist_parse_and_pins_dispatch_rows` pins `src/v4/test/claim/generated/testgen_category_wishlist.dag` pending/dispatched generator-category rows; `t19_idempotent_operation_generated_claims_parse_and_pin_emission` pins the idempotent-operation generator slice (`src/v4/std/effects.dag` canonical `IdempotentShape`/`EffectShape` witnesses + `idempotent_operation_witness_node`; outside the seven-way `TestgenConcept` coproduct; label-only skip); `t19_manual_manifest_matches_claim_anchor_discriminants` checks manual claim anchors join to the manifest by `T19ManualAnchorKey`; `t19_claim_corpus_has_no_direct_manual_anchor_assignments` scans `src/v4/test/claim/**/*.dag` so `TestClaim.t19_anchor` literals cannot bypass `t19_manual_claim_anchor(...)` after the `T19ClaimAnchorKey` split; `t19_coproduct_exhaustiveness_generated_claim_parse_and_witnesses_present` checks the generated coproduct-exhaustiveness corpus parses, derives the invalid `Node` and generated claim anchor from one `T19GeneratedCoproductExhaustiveness` source, uses canonical `node_locus`, and schedules the generated `DiagnosticExhaustiveness` claim under `T19GeneratedClaimAnchor`; `t20_bootstrap_plan_keeps_self_hosting_chain_as_data` checks the seed/self0/self1/fixpt bootstrap chain is encoded as `CompileStage` / `BootstrapPlan` data; `t22_diagnostic_assert_eval_witnesses_parse` checks `diagnostic_assert_eval.dag` parses; `t22_eval_diagnostic_assert_not_deferred_in_substrate` checks `05_eval.dag` no longer contains `eval_rejected_assert_kind_deferred`, executes `DiagnosticAssert`, and routes `run_test_claim` through `aggregate_verdicts`. | |
This comment was marked as resolved.
This comment was marked as resolved.
Sorry, something went wrong.
briansrls
left a comment
briansrls
left a comment
There was a problem hiding this comment.
Review metadata
- Provider / model:
codex/unknown - Commit:
d24fbb41· Trigger:schedule - Thinking:
304s wall
✅ The current diff resolves the prior review concerns and I do not see a new blocking issue.
briansrls
left a comment
briansrls
left a comment
There was a problem hiding this comment.
Review metadata
- Provider / model:
codex/unknown - Commit:
104512bd· Trigger:schedule - Thinking:
276s wall
BLOCKING (1)
Root Cause
docs/design-testgen-generative-categories.mdThe design marks AlgebraLaw as a landed slice while the wishlist status model only moves LBE to dispatched → move the AlgebraLaw row to dispatched or explicitly scope it as a distinct broadening obligation, then update the count witnesses and guards.
| dispatch_key: t19_wishlist_type_construction_dispatch, | ||
| }, | ||
| TestgenWishlistRow { | ||
| generator: wishlist_algebra_law_generator(), |
This comment was marked as resolved.
This comment was marked as resolved.
Sorry, something went wrong.
|
Verified against current HEAD 960657c. This P5 finding is already satisfied: the PR body contains a dedicated |
briansrls
left a comment
briansrls
left a comment
There was a problem hiding this comment.
Review metadata
- Provider / model:
codex/unknown - Commit:
960657c4· Trigger:schedule - Thinking:
333s wall
BLOCKING (2)
Root Cause
src/v4/lens/testgen.dagManualAnchorKey to AlgebraLawSubject has no single checked projection → factor one AlgebraLawCase authority and have both the generator projection and emitter consume it.src/v4/lens/testgen.dagDiagnosticExhaustiveness gained subject data without an emitter API change → pass DiagnosticExhaustivenessSubject into testgen_emit_coproduct_exhaustiveness_claim or remove the field until it has a consumer.
| } | ||
|
|
||
|
|
||
| fn algebra_law_manual_claim_case(anchor: ManualAnchorKey) -> Outcome<AlgebraLawCase> { |
This comment was marked as resolved.
This comment was marked as resolved.
Sorry, something went wrong.
| type AlgebraLawCase { anchor: ClaimAnchorKey, subject: AlgebraLawSubject } | ||
|
|
||
|
|
||
| type DiagnosticExhaustivenessSubject { reason: Symbol } |
This comment was marked as resolved.
This comment was marked as resolved.
Sorry, something went wrong.
|
Verified against current HEAD 960657c. This is already addressed: |
|
Review metadata
1. Story of the diffThis PR advances T-19 test generation from “manual anchors plus ad hoc category notes” toward an explicit non-tautological 2. Invariant categories1. LAYER MODEL — Finding
But this same diff has the 2. INVARIANTS.md + modeling-discipline.md — FindingBoundary Discipline / single authority: the PR introduces a dispatch ledger, but the ledger contradicts the generated TestClaim surface it is supposed to summarize. 3. CODING.md — CompliantThe Rust changes are test-ratchet updates rather than production compiler logic, and the shell change is fail-closed: 4. TESTING.md — FindingThe new tests/scripts currently ratchet the stale dispatch state instead of catching it. 5. LOCKED DESIGN DECISIONS — N/ANo locked design decision is directly changed. The zero-floor / tests-as-data direction is preserved by adding 6. TRACKED vs UNTRACKED DEBT — Finding
2.5. Top-down PM intent reviewFinding. The PR’s PM-level intent is to formalize the generator wishlist and dispatch non-tautological generators; however, the new plan tells the next worker to land 3. VerdictREQUEST_CHANGES. The substantive implementation direction is good, especially the non-tautological AlgebraLaw helper and |
briansrls
left a comment
briansrls
left a comment
There was a problem hiding this comment.
Review metadata
- Provider / model:
codex/unknown - Commit:
15b9aa34· Trigger:schedule - Thinking:
340s wall
BLOCKING (1)
Root Cause
src/v4/test/claim/generated/testgen_category_wishlist.dagdispatched wishlist rows construct Generator metadata independently from the emitted/scheduled generator helpers → derive dispatched rows from those helpers or make the ledger carry only non-authoritative dispatch keys/oracle receipts.
| classification: TestClassification { tier: Tier2, layer: Unit }, | ||
| anchor: manual_claim_anchor(anchor: ManualAnchorAbsent), | ||
| slot: DiagnosticExhaustiveness { | ||
| subject: DiagnosticExhaustivenessSubject { |
This comment was marked as resolved.
This comment was marked as resolved.
Sorry, something went wrong.
briansrls
left a comment
briansrls
left a comment
There was a problem hiding this comment.
Review metadata
- Provider / model:
codex/unknown - Commit:
0109f769· Trigger:schedule - Thinking:
209s wall
BLOCKING (1)
Root Cause
src/v4/lens/testgen.dagtestgen_emit_algebra_law_claim needs both the emitted ClaimAnchorKey and derived AlgebraLawSubject → keep ManualAnchorKey as the single authority and derive manual_claim_anchor(anchor) plus AlgebraLawSubject at the emission site, or replace AlgebraLawCase with a closed law-specific carrier that cannot pair arbitrary fields.
| type AlgebraLawSubject { algebra: Symbol, inhabitant: Symbol, law: Symbol } | ||
|
|
||
|
|
||
| type AlgebraLawCase { anchor: ClaimAnchorKey, subject: AlgebraLawSubject } |
There was a problem hiding this comment.
BLOCKING: AlgebraLawCase stores anchor and subject as independent fields even though the subject must be derived from the manual algebra-law anchor, so mismatched law cases remain representable and violate Illegal States Unrepresentable/API-level enforcement.
|
Review metadata
1. Story of the diffThis PR tightens the T-19 “generated TestClaim categories” lane by turning the non-tautology framing into a concrete planning and generation surface. It adds a design note defining which 2. Invariant categories
2.5. Top-down PM intent reviewCompliant. The PM-level intent is preserved: the new design rule says generated claims must add evidence beyond the scheduling row, and the implementation enforces the first concrete AlgebraLaw guard by rejecting identical 3. VerdictREQUEST_CHANGES The PR’s direction is sound, and the added ratchets show the T-19 lane is being advanced deliberately. I would not merge it until the duplicate coproduct-exhaustiveness reason symbol is collapsed to one authority and |
Consolidates session/quiet-moth-603 into consolidated/correctness-sweep. Changes from PR #3557: - src/v4/lens/testgen.dag: add AlgebraLawCase type + algebra_law_manual_claim_case helper, testgen_emit_algebra_law_claim, add algebra_law_subject_for_manual_anchor (subset not already on main), add Generator.kind field - src/v4/test/claim/generated/algebra_law_conformance.dag: new generated corpus of Nat algebra law TestClaims (law_nat_add_left_identity, add_associativity, mul_annihilator) - src/v4/test/claim/generated/testgen_category_wishlist.dag: new dispatch ledger (3 pending + 4 dispatched non-tautological generator categories; TestgenOracleBasis type, dissolve-on-arrival) - docs/design-testgen-generative-categories.md: design doc for non-tautological generator categories - src/v4/std/verification.dag: add test_claim_coproduct_variant function - src/v3/compiler/tests/integration/v4_lens_testgen_dag_smoke_test.rs: expanded smoke receipts - src/v3/compiler/tests/integration/v4_test_bootstrap_infra_closeout_test.rs: new assertions for wishlist + algebra law case helpers - src/v4/TASKS.md: T-19 follow-up task entries - scripts/check_t19_testgen_activation.py: testgen activation check script - INVARIANTS.md: updated smoke-test receipt row for testgen - scripts/v4-mvp1-e2e-gate.sh: cargo run exit-status fix Conflict resolution: DiagnosticExhaustiveness variant shape conflict resolved in favour of HEAD (omitted_variant: TestClaimCoproductVariant from T-19 #3561). Branch's DiagnosticExhaustivenessSubject type removed; coproduct_exhaustiveness.dag and testgen_category_wishlist.dag updated to use HEAD's omitted_variant shape. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
…iler pipeline correctness (#3636) * squash-merge PR #3557: Generative TestClaim categories lane Consolidates session/quiet-moth-603 into consolidated/correctness-sweep. Changes from PR #3557: - src/v4/lens/testgen.dag: add AlgebraLawCase type + algebra_law_manual_claim_case helper, testgen_emit_algebra_law_claim, add algebra_law_subject_for_manual_anchor (subset not already on main), add Generator.kind field - src/v4/test/claim/generated/algebra_law_conformance.dag: new generated corpus of Nat algebra law TestClaims (law_nat_add_left_identity, add_associativity, mul_annihilator) - src/v4/test/claim/generated/testgen_category_wishlist.dag: new dispatch ledger (3 pending + 4 dispatched non-tautological generator categories; TestgenOracleBasis type, dissolve-on-arrival) - docs/design-testgen-generative-categories.md: design doc for non-tautological generator categories - src/v4/std/verification.dag: add test_claim_coproduct_variant function - src/v3/compiler/tests/integration/v4_lens_testgen_dag_smoke_test.rs: expanded smoke receipts - src/v3/compiler/tests/integration/v4_test_bootstrap_infra_closeout_test.rs: new assertions for wishlist + algebra law case helpers - src/v4/TASKS.md: T-19 follow-up task entries - scripts/check_t19_testgen_activation.py: testgen activation check script - INVARIANTS.md: updated smoke-test receipt row for testgen - scripts/v4-mvp1-e2e-gate.sh: cargo run exit-status fix Conflict resolution: DiagnosticExhaustiveness variant shape conflict resolved in favour of HEAD (omitted_variant: TestClaimCoproductVariant from T-19 #3561). Branch's DiagnosticExhaustivenessSubject type removed; coproduct_exhaustiveness.dag and testgen_category_wishlist.dag updated to use HEAD's omitted_variant shape. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com> * squash-merge PR #3587: compiler pipeline correctness sweep Consolidates session/deep-bear-704 into consolidated/correctness-sweep. AI-5 InferredFacts illegal-state dissolution: - src/v4/compiler/04_infer.dag: InferredFacts restructured from {resolved_type, inhabits, descent, canonical} to {grounding: CanonicalGrounding, descent}; new gate fn canonical_grounding_admits_infer_facts; new accessors inferred_facts_resolved_type/algebra_ref/canonical_witness/descent; inferred_facts_from_grounding returns Outcome<InferredFacts> - src/v4/std/constraints.dag: CanonicalGrounding as sole production path AI-7 TestClaimCacheKey restructuring: - src/v4/compiler/05_eval.dag: TestClaimCacheKey<T> carries hash_staging: TestClaimCacheKeyStagingPlaceholder; import non_empty from v4.std.algebra AI-13 SurfaceSugarKind scaffold marker upgrades: - src/v4/compiler/03_normalize.dag, 00_compile.dag: updated scaffold markers AI-14 LexPattern/GrammarExpr parallel ASTs: - src/v4/compiler/01_tokenize.dag: scaffold comments updated to HEAD standard AI-15/R1-2 translate source gap, R1-3 constraints singleton-MVP, R1-4 Lens apply_lens stub, R1-5 eval loop: - src/v4/compiler/06_translate.dag, 02_parse.dag: updates - src/v4/test/claim/lens_common/infer_fixture.dag: removes algebra_witness_symbol and canonical_evidence_symbol params; adds claim_canonical_grounding, claim_inferred_facts_witness, claim_inferred_facts_from_nodes Conflict resolution: eval conflicts resolved in favour of HEAD (T-22 Wave 2 #3611 is more complete); 01_tokenize.dag comment conflicts took HEAD's dissolution markers; 04_infer.dag took branch's explanatory comment for InferredFacts shape. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com> * fix: remove unused non_empty import from 05_eval.dag * fix: restore coproduct_exhaustiveness_missing_variant check (revert stale DiagnosticExhaustivenessSubject strings) Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com> * fix: drop stale t19_ prefix from wishlist check needle (symbol renamed in HEAD design) * fix: update coproduct_exhaustiveness check needles to omitted_variant design * fix: update 05_eval.dag to new InferredFacts API; drop t19_ prefix from algebra_law_anchor_mismatch - Replace dissolved inferred_facts_resolved_type_matches/inhabitance_well_grounded/canonical_well_grounded calls in eval_runtime_value_acceptance_witness with inferred_facts_resolved_type equality check and canonical_grounding_admits_infer_facts (new 04_infer.dag API) - Declare algebra_law_anchor_mismatch symbol and replace undefined t19_algebra_law_anchor_mismatch reference in testgen.dag Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com> * fix: enforce InferredFactsEntry node==grounding.node invariant; add T-19 AlgebraLaw receipt to TASKS.md Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com> * WIP: PM May 22 * fix: add facts.grounding.node == node guard in inferred_facts_for_eval Eval consumption point must verify the map hit is for the correct node. `canonical_grounding_admits_infer_facts` only checks grounding internal consistency; it does not guard against a map returning facts whose grounding.node diverges from the lookup key. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com> * fix: add P5 receipt for T-19 AlgebraLaw expansion in INVARIANTS.md SG-0 table Per INVARIANTS.md P5 Mechanism (b): expanded hand-Rust under src/v3/ requires a checkable receipt. The AlgebraLaw Nat corpus assertions in v4_test_bootstrap_infra_closeout_test.rs land in this PR; the deferral lane is TASKS.md §T-19 (algebra_law_conformance.dag corpus) + ROADMAP.md Nine lanes row T-PB-B. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com> * fix: make facts_map_from_entries fail-closed via Outcome Previously, facts_map_from_entries silently dropped InferredFactsEntry items where entry.node != entry.facts.grounding.node. This compensated for the free constructibility of InferredFactsEntry (P2 boundary gap) without surfacing the violation diagnostically. Now: the fold rejects with infer_canonical_grounding_incoherent_diagnostic on any invariant-violating entry, and infer() threads the Outcome. admitted_inferred_facts_entry remains the primary enforcement point; facts_map_from_entries is the secondary fail-closed gate that makes invariant violations visible as Rejected rather than silent drops. Addresses codex RC on bc16ae7: InferredFactsEntry remained freely constructible and map construction compensated with a nondiagnostic filter. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com> * fix: replace bare [] with typed helper in facts_map_from_entries The v4 compiler cannot infer the element type of [] when it appears as a record field value inside Accepted { value: [], ... }. Introduce empty_inferred_facts_entry_list() -> List<InferredFactsEntry> (matching the existing empty_edge_list / empty_canonical_symbol_set pattern) and use it as the fold init. Fixes Lens-CI semantic compile failure on d1299ea. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com> * fix: add P5 receipt for PR #3636 anchor-strip + AlgebraLaw subject helper guard in INVARIANTS.md - Updates Generator field name from t19_anchor to anchor in existing ratchet description - Appends PR #3636 same-file receipt: renamed tests, new kind/anchor assertions, assert_six_algebra_law_subject_paths_in_testgen, forbidden nat_algebra_law_subject_symbol_* checks, and generalized generator_field_ty / between helpers Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com> * fix: update stale T19-prefix type names in INVARIANTS.md testgen row - Rename test fn refs: t19_anchor_field_is_manual_key → anchor_field_is_claim_anchor_key, concept_projection_matches_claim_t19_anchor → _claim_anchor, generator_carries_claim_kind_and_classification → _classification_and_anchor - Update description: T19ManualAnchorKey → ManualAnchorKey, Generator.t19_anchor → Generator.anchor, T19ClaimAnchorKey → ClaimAnchorKey, TestClaim.t19_anchor → TestClaim.anchor, T19ManualClaimAnchor → ManualClaimAnchor, T19ManualAnchorAbsent → ManualAnchorAbsent, T19GeneratedClaimAnchor → GeneratedClaimAnchor - Update inline carrier description: Generator.t19_anchor: T19ClaimAnchorKey → Generator.anchor: ClaimAnchorKey Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com> * WIP: PM May 22 * fix: strip stale T19 names from closeout + testgen INVARIANTS rows (cursor RC #17566) Line 374 (v4_test_bootstrap_infra_closeout_test.rs): update 7 test fn names (t19_testgen_concept_surface_stays_closed_and_classified → testgen_..., etc.) and 6 type names (T19ManualAnchorKey → ManualAnchorKey, TestClaim.t19_anchor → .anchor, t19_manual_claim_anchor → manual_claim_anchor, T19GeneratedCoproductExhaustiveness, T19GeneratedClaimAnchor, T19ClaimAnchorKey). Line 383 (v4_lens_testgen_dag_smoke_test.rs): simplify PR #3636 receipt section to remove all from→to rename references; receipt now describes current ratchet state only. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com> * fix(04_infer): adapt merge-conflict resolution to our InferredFacts struct layout The merge of main (PR #3646) erroneously took code that references `facts.inhabits.algebra` and `inferred_facts_canonical_grounding_coherent`, both of which belong to main's refactored InferredFacts struct. Our branch carries `InferredFacts { grounding, descent }`, so the guards must use `inferred_facts_algebra_ref(facts: facts).algebra` and `canonical_grounding_admits_infer_facts(grounding: facts.grounding)` instead. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com> * WIP: PM May 22 * WIP: PM May 22 * WIP: PM May 22 * WIP: PM May 22 --------- Co-authored-by: Claude Sonnet 4.6 <noreply@anthropic.com>
1 participant
Summary
Formalizes the T-19 generative TestClaim wishlist and tautology discipline in
docs/design-testgen-generative-categories.md, mapped through the canonicalTestgenConceptarms rather than a second category authority.Implements the first non-LBE generator slice by adding
testgen_emit_algebra_law_claim, a generated Nat algebra-law corpus with three sample rows, and structural guards that pin the LBE receipts, algebra-law samples, and pending generator wishlist. The algebra-law helper now rejects tautologicallhs == rhssides before emittingEqualsClaim.P5 Receipt
P5 Mechanism (b): this expands the existing SG-0-registered hand-Rust closeout harness
src/v3/compiler/tests/integration/v4_test_bootstrap_infra_closeout_test.rswithout adding a new census path. The matchingINVARIANTS.md§SG-0 row is updated in this PR to name the new interim ratchets:t19_language_behavior_equivalence_generated_claims_parse,t19_algebra_law_generated_claims_parse_and_use_testgen_emit,t19_non_tautological_generator_wishlist_parse_and_pins_dispatch_rows, andt19_language_behavior_equivalence_run_test_claim_receipts_present. Dissolution remains the existing T-19/T-20/T-22 trigger: replace this host parse-surface ratchet with.dagTestClaim rows or generated harness coverage.Test plan
python3 scripts/check_t19_testgen_activation.py— passedcargo fmt --all --check— passedcargo test -p v3-compiler --test integration -- v4_test_bootstrap_infra_closeout_test::t19_algebra_law_generated_claims_parse_and_use_testgen_emit v4_test_bootstrap_infra_closeout_test::t19_non_tautological_generator_wishlist_parse_and_pins_dispatch_rows v4_test_bootstrap_infra_closeout_test::t19_language_behavior_equivalence_generated_claims_parse— passed via BuildBuddyDispatch
Created follow-on dashboard work items for witness-validity, coproduct-exhaustiveness, idempotent-operation, and refinement-preservation generators under this session.