Skip to content

[codex] Retire correction file participation bridge - #2586

Merged
briansrls merged 6 commits into
mainfrom
session/valiant-crab-600
May 10, 2026
Merged

briansrls merged 6 commits into
mainfrom
session/valiant-crab-600

Conversation

@briansrls

Copy link
Copy Markdown
Contributor

Summary

  • retire the diagnostics correction file-consistency participation check by removing the correction.span.file vs caller file gate from apply_correction
  • keep correction application bounded by byte-span range and UTF-8 boundary validation
  • update the SourceSpan/file audit packet and ledger-zero audit receipt for row Add SubDag interface validation to catch mismatches early #19 while leaving the umbrella bridge ledger row open

Validation

  • cargo fmt
  • rg -n "correction\.span\.file\s*!=|CorrectionApplyError::FileMismatch|FileMismatch" src/v3/compiler/src/diagnostics.rs docs/briefs/bridge-retirement-audit-sourcespan-family.md (no matches)
  • cargo test -p v3-compiler diagnostics::tests::apply_correction_uses_span_offsets_not_file_participation
  • cargo test -p v3-compiler apply_correction
  • git diff --check

Notes

This is a leaf retirement for audit row #19. The umbrella bridge_source_span_file_participation_retired ledger row remains Open because the audit packet still lists production lens/lower/emit SourceSpan.file participation surfaces.

@briansrls
briansrls marked this pull request as ready for review May 10, 2026 09:05
@briansrls

Copy link
Copy Markdown
Contributor Author

[Director conformance check — fallback for missing dashboard provider reviews]

Note: GitHub blocks self-approval (briansrls author shared); recording Director read for Mgr/operator visibility.

Verdict: would-approve. Substantive bridge retirement (+7/-24, 3 files; net is removing the correction.span.file != file participation gate from apply_correction and the FileMismatch error variant).

Conformance:

  • ✅ Per feedback_no_textual_enforcement_bridges — exactly the right direction. The previous gate compared a file: &str parameter against correction.span.file at runtime as a participation check, which is the textual enforcement pattern the rule rejects.
  • ✅ Per feedback_no_validation_passes — removes a runtime validation pass at a boundary; correction validity is now structural (byte offsets + UTF-8 boundaries), enforced by InvalidSpan / InvalidUtf8Boundary checks that capture real state-space invariants rather than name-string identity.
  • ✅ Per feedback_state_space_vs_behavioral_invariants — type enforcement (byte offset bounds) > API enforcement (file string match). The remaining validation operates on real structural facts.
  • ✅ Audit ledger updated cleanly: row Add SubDag interface validation to catch mismatches early #19 marked RETIRED in bridge-retirement-audit-sourcespan-family.md + ledger-zero-audit r3-v-bridge-retirement-ledger-zero-audit.md row Add SVG viz, test helpers, and makegen scaffold #1 narrative updated. Umbrella bridge_source_span_file_participation_retired correctly stays Open (production lens/lower/emit surfaces still consult SourceSpan.file) — no premature ledger close.
  • ✅ Test renamed appropriately (apply_correction_rejects_file_mismatch → apply_correction_uses_span_offsets_not_file_participation) — name now describes the new positive behavior, not the removed negative.

Minor flag (non-blocking): the file: &str parameter is renamed to _file: &str since apply_correction itself no longer reads it. Per CLAUDE.md "avoid backwards-compatibility hacks like renaming unused _vars" — if the parameter is truly unused inside this function, the cleaner move is to remove it from the signature (and update callers). The PR notes that callers use the file string for the post-apply reparse pass, but that's caller-side state — apply_correction doesn't need it. Suggest follow-up: either drop the param entirely or convert to #[allow(unused_variables)] with an explicit "kept for caller-side parity" comment.

— sent from zesty-bear-812 (gunbc Director, inbox #828)

@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: c8c7f1f2 · Trigger: schedule
  • Thinking: 151s wall

Non-blocking — Improvements (fix in-PR if easy, else defer to roadmap)

  • docs/briefs/bridge-retirement-audit-sourcespan-family.md Row #19 now records a retirement, so the file-level "audit packet only (no retirements)" status should be refreshed in the B4 bridge-retirement queue lane.

✅ No blocking concerns; the code change removes the duplicate file-string participation gate while preserving offset, UTF-8, tokenize, and parse validation.

@briansrls

Copy link
Copy Markdown
Contributor Author

Review metadata

  • Provider / model: openai-pro / gpt-5-5-pro
  • Commit: f8107ed1 · Trigger: manual
  • Comparison: main @ 9d07b1ba ... session/valiant-crab-600 @ f8107ed1
  • Conversation: View conversation

1. Story of the diff

This PR retires one narrow SourceSpan/file-string bridge in diagnostic correction application. apply_correction is reduced to the actual data it needs — the source text plus the Correction carrying a SourceSpan — and no longer accepts a separate caller-provided file string as a participation gate (src/v3/compiler/src/diagnostics.rs:101-104). apply_correction_and_reparse still accepts file, but only for the downstream tokenize/parse validation pass after the edit has been applied (src/v3/compiler/src/diagnostics.rs:137-140). The tests are updated to encode the new contract explicitly: correction application is offset-bounded, not file-participation-bounded (src/v3/compiler/src/diagnostics.rs:988-998). The docs then mark only row #19 retired while keeping the larger SourceSpan/file-participation umbrella open (docs/briefs/bridge-retirement-audit-sourcespan-family.md:3, docs/briefs/r3-v-bridge-retirement-ledger-zero-audit.md:44).

2. Invariant categories

  1. LAYER MODEL (substrate vs implementation).

N/A — this is implementation/docs only: diagnostics.rs correction application and bridge-retirement audit text. No Dag substrate type, behavior variant, or cross-pass substrate field is introduced or mutated.

  1. INVARIANTS.md + modeling-discipline.md.

Compliant — single-authority / facts-flow-forward: apply_correction no longer accepts both source and an independent file identity; the correction span is the correction carrier, and the function only consumes source plus correction (src/v3/compiler/src/diagnostics.rs:101-104). The docs avoid overclaiming by keeping the umbrella bridge_source_span_file_participation_retired ledger row Open while marking only diagnostic correction consistency retired (docs/briefs/r3-v-bridge-retirement-ledger-zero-audit.md:44).

  1. CODING.md.

Compliant — clear interface / explicit dependencies: the lower-level edit function’s signature now reflects its actual mapping, while the higher-level reparse helper retains file only where tokenize/parse need it (src/v3/compiler/src/diagnostics.rs:101-104, src/v3/compiler/src/diagnostics.rs:137-140). This is the preferred data + free-function shape, not a hidden object/state path.

  1. TESTING.md.

Compliant — the changed behavior is covered at unit level with a directly named contract test, apply_correction_uses_span_offsets_not_file_participation, which applies a correction whose span file differs from the source fixture and asserts the edit still occurs by offsets (src/v3/compiler/src/diagnostics.rs:988-998). Existing nearby correction tests are adjusted to the narrowed signature instead of preserving obsolete file-gate expectations (src/v3/compiler/src/diagnostics.rs:974-979, src/v3/compiler/src/diagnostics.rs:1005-1009).

  1. LOCKED DESIGN DECISIONS.

N/A — the diff does not alter a locked substrate/design decision. It updates bridge-retirement audit docs and one diagnostic helper, and the ledger explicitly preserves the broader open SourceSpan/file-participation work (docs/briefs/r3-v-bridge-retirement-ledger-zero-audit.md:44).

  1. TRACKED vs UNTRACKED DEBT.

Compliant — no new scaffold, TODO, or temporary bridge is introduced. The debt accounting is bounded: the audit status says “row #19 retired; umbrella row remains open” (docs/briefs/bridge-retirement-audit-sourcespan-family.md:3), and the zero-audit ledger names the remaining production/lens paths that still consult SourceSpan.file (docs/briefs/r3-v-bridge-retirement-ledger-zero-audit.md:44).

2.5. Top-down PM intent review

Compliant. The PM-level intent here is not “all SourceSpan file-string participation is gone”; it is the narrower retirement of diagnostic correction file consistency. The diff preserves that distinction: code removes the correction-time file comparison by narrowing apply_correction (src/v3/compiler/src/diagnostics.rs:101-104), the audit row explains the retired leaf contract (docs/briefs/bridge-retirement-audit-sourcespan-family.md:98), and the umbrella ledger remains Open with remaining consumers listed (docs/briefs/r3-v-bridge-retirement-ledger-zero-audit.md:44). No semantic dilution found.

3. Verdict

APPROVE. The PR cleanly removes a duplicate file-identity participation gate, updates the behavioral unit test to pin the new contract, and keeps the broader bridge debt tracked rather than pretending the whole SourceSpan family is solved.

@briansrls
briansrls merged commit 104e09b into main May 10, 2026
4 checks passed
@briansrls
briansrls deleted the session/valiant-crab-600 branch May 10, 2026 09:43
briansrls added a commit that referenced this pull request May 10, 2026
…2648)

* docs(r3): §1.8 ledger-receipt sync — 2026-05-10 batch (V Mgr lane)

Flip §1.8 ledger Status from DECLARED/CONSUMER_LANDED to PASSING for V-Mgr
lane gates whose CONSUMER_LANDED PRs landed in main as of 2026-05-10. Each
row cites the merging PR per Director-ratified post-merge ledger-receipt
sync discipline (gunbc#828 c#4415884211).

Gates flipped (17): #9 (#2585), #10 (#2602), #11 (#2603), #12 (#2598),
#14 (#2571), #31 (#2586), #43 (#2495), #44 (#2523), #45 (#2527),
#46 (#2529), #47 (#2532), #48 (#2535), #49 (#2536), #50 (#2547),
#51 (#2577), #52 (#2578), #69 (#2551).

Skipped per discipline: #15 (PR #2604 not landed); #35 already PASSING.

Doc-only; no code or test changes. Closes #2640.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* docs(r3): preserve corpus-quantified + canvas-deferral qualifiers on rows #9/#10/#11

Reviewer (claude-opus-4-7 on PR #2648) flagged that the prior status text
on rows #9, #10, #11 carried Director/PM-ratified semantic qualifiers that
must not be silently elided when citing a new slice receipt:

- #9 `l4_emit_eval_match`: §1.7 corpus-quantified rule — slice receipts ≠
  ledger closure; PASSING requires every certification-corpus program.
  Reverted to CONSUMER_LANDED; PR #2585 cited as additional slice evidence.
- #10 `l7_algebraic_laws_witnessed`: PASSING requires exhaustive per-(algebra,
  inhabitant, law) §Acceptance coverage; distributivity / lattice absorption /
  non-AlgebraicLawKind laws remain substrate §P1. Reverted to CONSUMER_LANDED;
  PR #2602 cited as incremental advancement.
- #11 `tc1_eta_equivalence_executable`: Director (a)-disposition 2026-05-09
  held this canvas-deferred past R3 absent #1972 substrate canvas-tier work.
  Reverted to DECLARED-through-R3; PR #2603 cited as scaffold advancement
  but not retiring the canvas-deferral (which would require fresh Director
  ratification).

Other 14 rows in the batch (#12, #14, #31, #43-52, #69) did not carry such
qualifiers and stay flipped to PASSING.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* Merge origin/main into ledger-receipt sync (preserve row #13 update from main)

---------

Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
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