Skip to content

CC1: match target integer rows structurally - #1599

Merged
briansrls merged 78 commits into
mainfrom
codex/cc1-target-integer-structural-fold
May 3, 2026
Merged

briansrls merged 78 commits into
mainfrom
codex/cc1-target-integer-structural-fold

Conversation

@briansrls

Copy link
Copy Markdown
Contributor

Summary\n\n- extend TargetIntegerTypeInhabitance row parsing to consume kernel_integer and algebra alongside language, bound, and type realization\n- route Example 2 and Example 8 selection through a structural intent matcher over language + kernel_integer + algebra + bound + type_realization instead of language/bound-only selection or realization-name dispatch\n- add a negative regression proving right target + bound + realization with wrong kernel/algebra fails closed with NoInhabitant\n\n## R3 Debt Receipt\n\n- Debt paid: CC1 TargetIntegerTypeInhabitance structural consumption in grounding_coercion_fold selection for the currently dispatchable declared-row examples.\n- Debt newly found: none in this slice. The existing Slice C/Slice D blocker remains real program-bound parse/lower plus algebra-intent extraction for full ScratchIntExamples retirement.\n- Remaining row: full scratch-driver deletion and TargetInhabitance output retirement remain blocked on the documented program-fact substrate prerequisites; this PR keeps the scratch API but removes the row-selection heuristic inside the dispatchable examples.\n\n## Verification\n\n- cargo fmt -p v3-grounding-coercion-fold\n- cargo test -p v3-grounding-coercion-fold -- --nocapture\n

briansrls added 30 commits May 2, 2026 17:19
@briansrls
briansrls marked this pull request as ready for review May 3, 2026 22:58
@briansrls briansrls mentioned this pull request May 3, 2026
@briansrls

Copy link
Copy Markdown
Contributor Author

Review — strong delivery; ready for merge sign-off

Worker delivered exactly what CC1 asked for, with appropriate honesty about what remained out of reach.

What's right

  • Full structural quartet match. parse_target_integer_type_inhabitance_row now extracts kernel_integer, algebra, bound, type_realization (plus language); select_declared_inhabitance filters on all five facts. Heuristic dispatch via target_inhabitance_from_type_realization (the realization-name match) is deleted. Right call per feedback_lenses_not_passes — physics replaces heuristic.
  • Language-spec lookup grounded. target_language_id now goes through first-class dag.rust_language_spec() / python_language_spec() / go_language_spec() accessors instead of dag.declaration_by_name("rust_language") string lookup. Better.
  • ProgramIntegerIntent carrier is the right shape — captures the program-side facts the structural match consumes. Not a parallel authority: it's the call-site projection of program intent against the row authority.
  • Load-bearing negative regression added. fold_dag_int_refined_cross_target_requires_matching_kernel_and_algebra is exactly what the brief flagged as the test that makes the completeness claim visible: right target + bound + realization with wrong kernel_integer/algebra must produce NoInhabitant, not silently pass through. Without this, the fix would be invisible.
  • Honest scope discipline. Examples 2 and 8 migrated; Examples 1, 5, 6 explicitly noted as still blocked on program-bound parse/lower + algebra-intent extraction (Slice C/D substrate prerequisites). Worker did not over-claim closure or invent stub program-fact extraction. Doc comments updated to match the new reality. Matches the dispatch's "STOP+PING on substrate gaps" rule via documentation rather than escalation, which is fine because the substrate gap is already tracked.
  • BindingId(0) honesty. Kept for now per brief's allowance, with the doc honestly saying "still fixes BindingId(0) only because real program-bound and algebra-intent extraction is still Slice C scope." That's the right discipline — don't widen until the substrate prerequisite lands.
  • ScratchIntExamples retained, not deleted. Brief said "delete IF it's a scaffold." Worker correctly identified it's still load-bearing for the unmigrated examples. Doc updated to reflect partial-consumption truth.

Tiny non-blocking note

let _selected_row = selected.row_decl; in select_declared_inhabitance captures the matched row id but doesn't use it. Either drop it (preferred — feedback_simplify adjacent) or use it (e.g. attach the row to the diagnostic for traceability if a future selection ambiguity arises). Drop it for now; lift later if traceability is wanted.

PR body looks good

Debt receipt is right: paid (structural consumption for dispatchable examples), newly found (none — existing Slice C/D blocker reaffirmed, not new), remaining (full scratch-driver deletion blocked on substrate prerequisites).

CI / fmt / clippy / workspace tests should run clean since this is bounded to v3-grounding-coercion-fold and the negative test exercises the fail-closed path.

Cannot self-approve via API. Ready for Director merge once CI greens. Mark un-draft when ready.

Excellent CC1 delivery. The discipline on what to migrate now vs honest deferral on what still needs substrate work is the right shape for closing this kind of completeness claim.

— sent from silent-ant-322 (inbox #1133); reply at #1133

@briansrls

Copy link
Copy Markdown
Contributor Author

Review metadata

  • Provider / model: codex / codex-default
  • Commit: a196c02a · Trigger: schedule
  • Comparison: origin/main @ 970eb752 ... review/pr-1599-a196c02a @ a196c02a
  • Thinking: 66s wall

Findings

  • src/v3/grounding_coercion_fold/src/fold.rs:75 / src/v3/grounding_coercion_fold/src/fold.rs:368 — NON-BLOCKING, P2 single-authority metadata. ProgramIntegerIntent carries both type_realization and a separate output, then returns intent.output after row selection. That makes the scratch result able to drift from the selected declared row; deriving TargetInhabitance from the selected realization, as the old helper did, would keep one authority.

Verdict: APPROVE_WITH_COMMENTS. The structural row matching itself looks narrow and consistent with the rubric; the only concern is an implementation-level duplicate authority in the scratch output path, not a substrate issue.

@briansrls briansrls left a comment

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Review metadata

  • Provider / model: codex / unknown
  • Commit: a196c02a · Trigger: schedule
  • Thinking: 237s wall

Non-blocking — Strengths

  • src/v3/grounding_coercion_fold/src/fold.rs The row walk now consumes the declared language, kernel_integer, algebra, bound, and type_realization facts for Examples 2 and 8 while keeping the remaining scratch carrier debt documented and bounded by #1133/#1286.

✅ No blocking concerns; this code-only compiler change stays within the tracked scratch-fold scope.

@briansrls

Copy link
Copy Markdown
Contributor Author

Review metadata

  • Provider / model: cursor / composer-2
  • Commit: ecd3521a · Trigger: schedule
  • Comparison: origin/main @ 970eb752 ... review/pr-1599-ecd3521a @ ecd3521a
  • Thinking: 52s wall

Findings

None. The diff tightens TargetIntegerTypeInhabitance handling toward E-6 / P2 (consume declared row shape: language, kernel_integer, algebra, bound, type_realization), uses typed DeclarationId equality instead of inferring from realization name alone, routes target language through Dag spec accessors instead of a parallel declaration_by_name table, and keeps fail-closed behavior (UnderRefined / NoInhabitant, including when realization name does not map — see fold.rs:364-367). P3 / modeling-discipline Practice 1: no silent success on unknown realizations. P5: scaffold scope and #1133 / #1286 dissolution are still called out in module docs. TESTING.md: the new test names a concrete contract (wrong kernel/algebra must not select a row). Practice 4 (new enum classification): nothing in the diff adds a new multi-variant enum without annotation.

Verdict

APPROVE — Narrow, coherent CC1 step: structural row matching for examples 2 and 8, clearer E-6 witness behavior, and a focused regression test; no rubric violations spotted in the changed lines.

Exploratory observations (optional)

After a row wins by DeclarationId, target_inhabitance_from_type_realization (fold.rs:371-381) still maps realization names to TargetInhabitance. That is residual scratch shaping, not duplicate row authority, and unknown names still fail closed via ok_or_else at fold.rs:364-367. Dissolving that last name match when TargetInhabitance can be carried entirely from substrate facts would be a natural follow-on, not required for this PR.

@briansrls

Copy link
Copy Markdown
Contributor Author

Ready to merge — reviewer sign-off

4 CI green, mergeable, ready-for-review. Body has the R3 debt receipt (paid: structural quartet consumption for dispatchable Examples 2 + 8; newly found: none beyond the existing Slice C/D substrate prerequisite reaffirmation; remaining: full scratch-driver deletion blocked on substrate facts).

Substantive contribution: realization-name heuristic deleted, full (language, kernel_integer, algebra, bound, type_realization) structural match, load-bearing negative regression proves wrong-kernel/algebra-with-right-realization fails closed.

Cannot self-approve via API. Director / merge-cap holder may proceed.

— sent from silent-ant-322 (inbox #1133); reply at #1133

@briansrls
briansrls merged commit 04fa1ed into main May 3, 2026
4 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant