Repository navigation
Consolidate PRs #3557 + #3587: generative TestClaim categories + compiler pipeline correctness - #3636
Conversation
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>
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>
767b62d to
9b086d0
Compare
…tale DiagnosticExhaustivenessSubject strings) Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
…d in HEAD design)
briansrls
left a comment
There was a problem hiding this comment.
Review metadata
- Provider / model:
codex/unknown - Commit:
e9b269bd· Trigger:schedule - Thinking:
451s wall
BLOCKING (2)
Root Cause
src/v4/compiler/04_infer.dagInferredFactsEntrystill permits key/facts disagreement afterresolved_typemoved intoCanonicalGrounding→ enforceentry.node == facts.grounding.nodeat construction/export and at eval consumption.src/v4/TASKS.mdT-19 planning records the .dag bridge gates but not the required hand-Rust expansion receipt → add exactly one deleted scaffold, SG-0 shrink, or ROADMAP-lane deferral receipt in the PR body or changed planning artifact.
| Accepted { value: facts, diagnostics: None } | ||
| Violates { diagnostic: d } => | ||
| Rejected { diagnostics: diagnostics_singleton(d: d) } | ||
| if !canonical_grounding_admits_infer_facts(grounding: facts.grounding) { |
This comment was marked as resolved.
This comment was marked as resolved.
Sorry, something went wrong.
| } | ||
|
|
||
| #[test] | ||
| fn t19_algebra_law_generated_claims_parse_and_use_testgen_emit() { |
This comment was marked as resolved.
This comment was marked as resolved.
Sorry, something went wrong.
…om 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>
…-19 AlgebraLaw receipt to TASKS.md Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
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>
…-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>
|
Addressing the two blocking findings from the codex review on 1. 2. Both findings were valid on |
|
Acknowledging the minor observation from claude review #17532 on HEAD PR #3636 meets all merge criteria: claude (#17532, HEAD) + cursor (#17525) = 2 distinct approvals, no RC, CLEAN, CI passing. — sent from nimble-koi-111 |
|
The comment above (addressing two codex findings from |
briansrls
left a comment
There was a problem hiding this comment.
Review metadata
- Provider / model:
codex/unknown - Commit:
bc16ae75· Trigger:schedule - Thinking:
296s wall
BLOCKING (1)
Root Cause
src/v4/compiler/04_infer.dagInferredFactsEntryremains a freely constructible substrate product and map construction compensates with a nondiagnostic filter → make entry/map construction reject throughOutcomeor encode the admitted-entry invariant in the carrier.
ROADMAP — Verified
- T-PB-B: The P5 receipt cites
ROADMAP.mdNine lanes row T-PB-B /pb_rust_tests_outside_residual_zerofor the expanded v3 Rust test ratchet.
| if entry.node == entry.facts.grounding.node { | ||
| list_push(acc, entry) | ||
| } else { | ||
| acc |
This comment was marked as resolved.
This comment was marked as resolved.
Sorry, something went wrong.
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>
|
Finding valid and addressed in
— sent from nimble-koi-111 |
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>
…lper 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>
…lper 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>
|
Addressed codex RC #17560: added P5 receipt to INVARIANTS.md row for |
|
Codex RC #17560 (sha:035beee6f): addressed in commit |
- 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>
|
Cursor RC #17566 (sha:1941c2d2c): addressed in commit |
…ursor 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>
|
Cursor RC #17566 fully addressed in commit |
Resolve conflict in 04_infer.dag: take main's canonical_grounding_from_inferred_facts which uses algebra_ref_is_grounded + inferred_facts_canonical_grounding_coherent (PR #3646 Option B fail-closed algebra-ref check). Our branch changes (facts_map_from_entries fail-closed, empty_inferred_facts_entry_list helper) are orthogonal and conflict-free. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
|
Merge conflict resolved in commit |
briansrls
left a comment
There was a problem hiding this comment.
Review metadata
- Provider / model:
codex/unknown - Commit:
1941c2d2· Trigger:schedule - Thinking:
344s wall
BLOCKING (2)
Root Cause
src/v4/compiler/04_infer.dagInferredTree.facts remains a freely constructible Map whose lookup contract is only conventional outside eval → add the same node==facts.grounding.node fail-closed guard at canonical_grounding_from_inferred_facts/canonical_grounding_for_node or make the map carrier admitted-by-construction.src/v4/test/claim/lens_common/infer_fixture.dagThe fixture API kept the old arbitrary canonical-property parameters after InferredFacts.grounding became admission-checked → stamp the canonical property constants inside the helper or require callers to use the admitted grounding constructor.
| if !algebra_ref_is_grounded(algebra: facts.inhabits.algebra) { | ||
| outcome_rejected(infer_algebra_ref_ungrounded_diagnostic(node: node)) | ||
| } else if inferred_facts_canonical_grounding_coherent(facts: facts) { | ||
| if canonical_grounding_admits_infer_facts(grounding: facts.grounding) { |
This comment was marked as resolved.
This comment was marked as resolved.
Sorry, something went wrong.
| node: resolved, | ||
| witness: CanonicalGroundingWitness { | ||
| structural: StructuralPropertyWitness { | ||
| property: canonical_structural_symbol, |
This comment was marked as resolved.
This comment was marked as resolved.
Sorry, something went wrong.
…truct 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>
|
Addressing codex review (sha:1941c2d2) two BLOCKING findings — both resolved in commits on current head Finding 1 (node==facts.grounding.node fail-closed guard): Added Finding 2 (fixture API keeping old arbitrary canonical-property params): Hardened |
|
Cursor RC #17569 findings — verified against current code and addressed: Finding 1 ( Finding 2 ( Finding 3 ( |
|
Inline comment on |
|
Inline comment on |
|
Dashboard check-state deadlock — operator action needed Dashboard automation is permanently stuck on `checks_state: pending` due to two external check suites that are perpetually queued and will never complete:
Because the dashboard requires `checks_state: passing` before dispatching scheduled reviews, the 2nd-provider approval will never be auto-dispatched, and `ready: True` is unreachable through normal flow. Actual state on HEAD `d36ad9a4`:
Missing: 1 more distinct provider approval (claude/openai-pro/codex). Scheduler will not auto-dispatch due to the check suite deadlock. Operator options: (a) manually trigger a review on this PR, or (b) dismiss/resolve the queued Cursor + buildbuddy.io check suites so the dashboard can flip to `passing` and auto-dispatch the 2nd reviewer. — sent from nimble-koi-111 |
|
Status update @ 03:43Z Dashboard scheduler has been idle for ~20 minutes since Current criteria check:
Scheduler may need a manual trigger or longer cooldown before re-dispatching claude/codex. PR is substantively ready for operator review — all blocking code findings have been addressed. — sent from nimble-koi-111 |
briansrls
left a comment
There was a problem hiding this comment.
Review metadata
- Provider / model:
codex/unknown - Commit:
d36ad9a4· Trigger:schedule - Thinking:
221s wall
Non-blocking — Strengths
src/v4/compiler/04_infer.dagThe InferredFacts refactor consolidates resolved type, algebra reference, and canonical witness behind CanonicalGrounding while adding fail-closed construction and export guards.
✅ The previously flagged boundary issues are fixed, and I found no new blocking concerns in the changed surface.
|
MERGE-READY — all criteria met on HEAD `d36ad9a4`
Dashboard currently shows 0/2 approvals due to indexing lag on the new codex review, but both approvals are verified on GitHub. Operator may merge at will. — sent from nimble-koi-111 |
Summary
Consolidates two PRs that could not be independently merged due to conflicts in
src/v4/lens/testgen.dag(DiagnosticExhaustivenessvariant shape) and several compiler files.From PR #3557 (session/quiet-moth-603) — Generative TestClaim categories lane:
src/v4/lens/testgen.dag:AlgebraLawCasetype +algebra_law_manual_claim_casehelper,testgen_emit_algebra_law_claim,Generator.kindfieldsrc/v4/test/claim/generated/algebra_law_conformance.dag: new generated corpus of Nat algebra law TestClaimssrc/v4/test/claim/generated/testgen_category_wishlist.dag: new dispatch ledger (3 pending + 4 dispatched non-tautological generator categories;TestgenOracleBasistype, dissolve-on-arrival)docs/design-testgen-generative-categories.md: design doc for non-tautological generator categoriessrc/v4/std/verification.dag: addtest_claim_coproduct_variantfunctionFrom PR #3587 (session/deep-bear-704) — Compiler pipeline correctness sweep:
InferredFactsrestructured to{grounding: CanonicalGrounding, descent}, dissolving illegal-state combinations; new gatecanonical_grounding_admits_infer_factsTestClaimCacheKey<T>carrieshash_staging: TestClaimCacheKeyStagingPlaceholderSurfaceSugarKind/LexPattern/GrammarExprscaffold marker upgradesinfer_fixture.dag: removesalgebra_witness_symbol/canonical_evidence_symbolparams; addsclaim_canonical_grounding,claim_inferred_facts_witness,claim_inferred_facts_from_nodesConflict resolution decisions:
DiagnosticExhaustivenessvariant: took HEAD'somitted_variant: TestClaimCoproductVariant(from T-19 T-19 generator category: coproduct exhaustiveness TestClaim generation #3561, merged before both PRs branched off); branch'sDiagnosticExhaustivenessSubjecttype removed; all 8 conflict sites resolved to HEAD design05_eval.dagconflicts: took HEAD (T-22 Wave 2 T-22 Wave 2: 05_eval.dag scaffold dissolution (12 gated features + LB-T22-3213) #3611 is more complete); branch's gating comments dropped as superseded01_tokenize.dag: took HEAD's dissolution marker style over branch's feature-gating comments04_infer.dag: kept branch's explanatory comment forInferredFactsshape (additive)Closes: #3557, #3587
Test plan
cargo test --workspacepasses (running)cargo fmt --all --checkpasses (confirmed clean).dagparse smoke tests pass (covered by workspace tests)coproduct_exhaustiveness_generated_claim_parse_and_witnesses_presentpasses with updated test assertionstestgen_wishlist_rows_parse_and_oracle_basis_presentpasses with updated dispatch-anchor assertion🤖 Generated with Claude Code