Skip to content

feat(#242): VCR-RA-003 across-JOIN on the numeric-branch optimized path#819

Draft
avrabe wants to merge 2 commits into
mainfrom
feat/50-ra003-optimized-joins
Draft

feat(#242): VCR-RA-003 across-JOIN on the numeric-branch optimized path#819
avrabe wants to merge 2 commits into
mainfrom
feat/50-ra003-optimized-joins

Conversation

@avrabe

@avrabe avrabe commented Jul 17, 2026

Copy link
Copy Markdown
Contributor

v0.50 Lane 2. Closes the v0.49 named residual: the whole-function allocation validator's across-JOIN invariant (invariant 4, MUST-availability fixpoint) previously loud-flagged NotAttempted on the OPTIMIZED path's pre-resolved numeric branches (BOffset/BCondOffset). Now a resolved-offset join-CFG builder decodes those targets to predecessor indices, so the fixpoint runs there too — "whole-function" holds on the DEFAULT shipping path, not just direct/label branches.

Red-first (non-vacuous): ra003_numeric_red_across_join_clobber_is_caught (a value in different locations on two numeric-branch paths into a join → Violation, was NotAttempted before). Green: both-paths-define / dominator-defined / loop-back-edge → Consistent. Decline-honesty kept: off-boundary + mixed-stream + genuinely-unresolvable offsets still NotAttempted (decline>guess). 24 ra003 tests total (18→24).

Frozen 10/10 byte-identical (validator emits nothing; control_step 0x00210A55, flight_algo 0x07FDF307). 648 lib tests green, clippy -D clean, fmt clean, claims 25/25, rivet clean.

Salvaged from an API-stalled authoring agent (uncommitted WIP) — re-verified every gate from scratch before committing.

🤖 Generated with Claude Code

Extends invariant 4 (join MUST-availability fixpoint) past the direct/label
path to the optimized numeric-branch path: a resolved-offset join-CFG builder
decodes BOffset/BCondOffset targets to predecessor indices, so the availability
fixpoint runs there too — the "whole-function" allocation validator now holds on
the DEFAULT shipping path, not just direct branches. NotAttempted stays only for
genuinely-unresolvable offsets (decline>guess). 6 new ra003_numeric_* tests
(red across-join clobber CAUGHT; green both-paths/dominator/loop-back-edge
Consistent; off-boundary + mixed-stream decline). 648 lib tests green, frozen
10/10 byte-identical (validator emits nothing), 25/25 claims.

Salvaged from an API-stalled agent (uncommitted WIP, re-verified from scratch:
build + 24 ra003 tests + frozen + clippy + fmt + claim gate all green).

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
@codecov

codecov Bot commented Jul 17, 2026

Copy link
Copy Markdown

Codecov Report

❌ Patch coverage is 90.20772% with 33 lines in your changes missing coverage. Please review.

Files with missing lines Patch % Lines
crates/synth-synthesis/src/liveness.rs 90.20% 33 Missing ⚠️

📢 Thoughts on this report? Let us know!

@avrabe
avrabe marked this pull request as draft July 22, 2026 03:24
@avrabe

avrabe commented Jul 22, 2026

Copy link
Copy Markdown
Contributor Author

Converting to draft — the optimized-path join enforcement isn't ready, and this must not weaken the VCR-RA-003 acceptance oracle.

CI surfaced a real false-positive: on cf_shapes_500.wat::ifelse (a br_if if/else that push {r5,lr}…stores…pop {r5,pc}), the numeric-branch across-JOIN check hard-errors JoinValueNotAvailable { reg: R8, join_block: 3 } on valid code — over-rejecting a correct compile. This was latent salvage debt (the authoring agent died before running vcr_ra_003_phase2_join_call.py; my salvage ran the unit tests + frozen but not this differential — the lesson: salvage must run the lane's OWN repro).

Root cause: R8 is live-in at function entry (the validator's reg_effect sees the prologue push) and read again at the pop {…pc} epilogue join, but is never re-def'd on a straight-line arm — so a MUST-availability check over the numeric-branch join CFG flags it as unavailable.

Two fixes attempted and REJECTED (both break soundness, verified against the red-first gate):

  1. Hardcode R4–R8 into entry_seed → masks the ra003_*_red_across_join_clobber_is_caught tests (a fixed set can't distinguish 'holds a defined caller value' from 'clobbered on one arm').
  2. Seed entry_seed with live_in[0] → fixes the FP (repro 0 false-positives) but STILL silences both red-first tests (their synthetic clobber register is itself entry-live, so seeding masks it).

A change that greens the repro but stops catching real clobbers is worse than the FP. The correct discriminator (available-at-entry iff preserved — pushed-in-prologue and popped-at-exit, vs merely entry-live) needs proper analysis, not a maintenance-tick patch on the soundness component.

Disposition: the pre-#819 behavior (optimized-path numeric-branch joins → honest NotAttempted) is CORRECT; #819 regresses it to over-rejection. Deferring to a proper lane with cf_shapes_500::ifelse pinned as a red-first fixture from the start. The join-CFG-builder infrastructure + 6 ra003_numeric_* tests here are salvageable groundwork for that redo.

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