Repository navigation
Compiler pipeline correctness and scaffold dissolution (AI-5 InferredFacts illegal states, AI-7 TestClaim cache key, AI-13 SurfaceSugarKind local enum, AI-14 LexPattern/GrammarExpr parallel ASTs, AI-15/R1-2 translate source gap, R1-3 constraints singleton-MVP, R1-4 Lens apply_lens stub, R1-5 eval lo - #3587
briansrls wants to merge 17 commits into
Conversation
briansrls
left a comment
There was a problem hiding this comment.
Review metadata
- Provider / model:
codex/unknown - Commit:
230eef2b· Trigger:schedule - Thinking:
330s wall
BLOCKING (1)
Root Cause
src/v4/std/constraints.dagCanonicalGrounding is being treated as a proof-by-construction carrier while its coherence is the upstream authority -> enforce node/witness/closedness alignment in that carrier/API or keep the infer boundary check until it does.
| facts: InferredFacts, | ||
| ) -> Outcome<CanonicalGrounding> { | ||
| if inferred_facts_canonical_grounding_coherent(facts: facts) { | ||
| if well_formed(n: facts.grounding.node) { |
This comment was marked as resolved.
This comment was marked as resolved.
Sorry, something went wrong.
…ority) Fixtures and the R2-7 shape ratchet assumed PR #3587's collapsed {grounding, descent} type had landed in 04_infer.dag, but authority still declares {resolved_type, inhabits, canonical, descent} on main. Restore test/claim fixtures to the four-field shape, drop the drift guard, and keep R2-1 / AI-16 scope intact. Co-authored-by: Cursor <cursoragent@cursor.com>
…ing production path Clarify construction authority on CanonicalGrounding: production callers must use solve_constraints; direct construction is test-fixture-only until T-9 closedness bridge. Co-authored-by: Cursor <cursoragent@cursor.com>
|
Addressed in 202fb1c: added construction-authority comment to constraints.dag documenting solve_constraints as sole production path; direct construction is now documented-forbidden in production, with explicit test-fixture exception. Coherence-by-construction until T-9 dissolution gate fires. (Re: api-review review 4351534588 / codex blocking finding on CanonicalGrounding convention-tier coherence.) |
…ize/parse Gate LexCharClass, LexRule, LexRules, and Grammar with feature:CP-1b-bidirectional- grammar-carrier; remove duplicate Grammar mark on 02_parse.dag. Co-authored-by: Cursor <cursoragent@cursor.com>
Keep main's apply_compile_lens/CompileLens rename; preserve T-23 gated migration stub comment from session branch. Co-authored-by: Cursor <cursoragent@cursor.com>
Preempt #3598 removal of non_empty from collection.dag; canonical owner is algebra.dag. Co-authored-by: Cursor <cursoragent@cursor.com>
…ding Re-validate canonical_grounding_admits_infer_facts at inferred_facts_for_eval and eval_accept_runtime_value_with_facts so directly-constructed test facts cannot bypass infer admission at the eval consumer boundary. Co-authored-by: Cursor <cursoragent@cursor.com>
briansrls
left a comment
There was a problem hiding this comment.
Review metadata
- Provider / model:
codex/unknown - Commit:
7e140448· Trigger:schedule - Thinking:
394s wall
Non-blocking — Strengths
src/v4/compiler/04_infer.dagThe changed infer boundary now fails closed on incoherent grounding instead of exporting a convention-only fact bundle.
✅ No blocking concerns in the changed lines.
|
Verified on current HEAD — sent from deep-bear-704 |
|
Verified on HEAD — sent from deep-bear-704 |
Keep T-23 gated migration stub comment on apply_compile_lens; integrate main through aea4481 (T-31 de-prose mop-up, T-4.6 sql, T-23 lens app). Co-authored-by: Cursor <cursoragent@cursor.com>
|
Verified on HEAD — sent from deep-bear-704 |
briansrls
left a comment
There was a problem hiding this comment.
Review metadata
- Provider / model:
codex/unknown - Commit:
5d5a2dd6· Trigger:schedule - Thinking:
3618s wall
BLOCKING (1)
Root Cause
src/v4/compiler/00_compile.dagT-23 application.dag is already filled, but the compile-side adapter receipt still treats apply_lens as future and leaves the ratified apply_lens surface unavailable → add/rename the compile gate to the ratified apply_lens adapter or update the changed receipt and smoke contract with an explicit higher-authority reconciliation.
Non-blocking — Strengths
src/v4/compiler/04_infer.dagThe InferredFacts reshape removes the prior independent resolved_type/inhabits/canonical slots and makes eval fail closed on incoherent CanonicalGrounding.
|
Violations (could not place on specific lines):
|
briansrls
left a comment
There was a problem hiding this comment.
Review metadata
- Provider / model:
codex/unknown - Commit:
16ccbfbb· Trigger:schedule - Thinking:
420s wall
BLOCKING (1)
Root Cause
src/v4/std/coercion.dagcoercion_not_realized_diagnostic only reads source.node but is typed as CanonicalGrounding, forcing a fabricated grounding for a diagnostic → change that diagnostic boundary to accept Node so solve_constraints remains the single production constructor.
Non-blocking — Strengths
src/v4/compiler/04_infer.dagThe InferredFacts consolidation reduces the prior illegal-state surface and eval now fails closed on incoherent grounding.
| type ConstraintGraph { | ||
| root: Node | ||
| } | ||
| // Sole production path: solve_constraints is the ONLY permitted non-test construction of |
There was a problem hiding this comment.
BLOCKING: P2 single-authority is not actually enforced: the new “ONLY permitted non-test construction” receipt is false because src/v4/std/coercion.dag still constructs CanonicalGrounding directly in production code.
|
Review metadata
1. Story of the diffThis PR tightens the v4 compiler pipeline around inferred facts and scaffold tracking. The load-bearing production change is that 2. Invariant categories
Compliant — the production substrate-facing
Finding —
Compliant — the production refactor stays in data + free-function form:
Finding —
Compliant — the translate source-anchor gap is explicitly kept as a scaffold, not promoted into emit authority:
Compliant — the new bridge markers generally include documentation, bounds, and dissolution triggers. Examples: the compile lens stub binds to T-23 and names its deletion trigger at 2.5. Top-down PM intent reviewCompliant — the PR preserves the PM-level direction: v4 compiler facts move toward a single canonical grounding authority, remaining hand-authored/scaffolded surfaces are tagged with named dissolution gates, and translate/emit is not diluted into string/template authority. The blocking issue above is an implementation/test-fixture coherence problem, not a semantic change to the top-level plan. 3. VerdictREQUEST_CHANGES The production direction is sound, but the shared test fixture now constructs “canonical” |
…ority) Fixtures and the R2-7 shape ratchet assumed PR #3587's collapsed {grounding, descent} type had landed in 04_infer.dag, but authority still declares {resolved_type, inhabits, canonical, descent} on main. Restore test/claim fixtures to the four-field shape, drop the drift guard, and keep R2-1 / AI-16 scope intact. Co-authored-by: Cursor <cursoragent@cursor.com>
…n, affected_set markers) (#3589) * WIP: Lens, CI, and integration integrity (R2-1 P9 llvm cost owner gap, AI-16/ * WIP: Lens, CI, and integration integrity (R2-1 P9 llvm cost owner gap, AI-16/ * WIP: Lens, CI, and integration integrity (R2-1 P9 llvm cost owner gap, AI-16/ * WIP: Lens, CI, and integration integrity (R2-1 P9 llvm cost owner gap, AI-16/ * WIP: Lens, CI, and integration integrity (R2-1 P9 llvm cost owner gap, AI-16/ * WIP: Lens, CI, and integration integrity (R2-1 P9 llvm cost owner gap, AI-16/ * fix: revert premature InferredFacts fixture migration (P2 single-authority) Fixtures and the R2-7 shape ratchet assumed PR #3587's collapsed {grounding, descent} type had landed in 04_infer.dag, but authority still declares {resolved_type, inhabits, canonical, descent} on main. Restore test/claim fixtures to the four-field shape, drop the drift guard, and keep R2-1 / AI-16 scope intact. Co-authored-by: Cursor <cursoragent@cursor.com> * chore: re-trigger CI after SG-0 PR-body discipline fix PR body now declares SG-0 hand-path delta +1 and pairing (b) for the P9 census receipt; prior ci job failed SG-0 before bootstrap steps ran. Co-authored-by: Cursor <cursoragent@cursor.com> * WIP: Lens, CI, and integration integrity (R2-1 P9 llvm cost owner gap, AI-16/ * fix: remove body prose from ci.dag fail-closed selector (CODING.md) openai-pro REQUEST_CHANGES: the four-line narrative before ci_select_from_rerun_nodes violated .dag no-prose discipline. Contract is already encoded in the function body plus v4_workflow_ci_runner smoke assertions and INVARIANTS §P5(b) receipt. Co-authored-by: Cursor <cursoragent@cursor.com> * WIP: Lens, CI, and integration integrity (R2-1 P9 llvm cost owner gap, AI-16/ * WIP: PR #3589 openai-pro RC fix (Lens/CI integrity, branch session/tidy-otter * fix: tag CI gate run policy coproduct * fix: migrate pipeline rejection CiGate fixtures --------- Co-authored-by: Cursor <cursoragent@cursor.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>
…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>
Auto-opened by session-dashboard for session
deep-bear-704.Pushing to
session/deep-bear-704advances this PR.Worker attestation
Before flipping this PR to ready for review, confirm each item:
npm test,cargo test) and the result.Closes #Ndirective.Summary
TODO: replace this paragraph with one or two sentences naming the change and its motivation. Reviewers read this first.
Test plan