feat(#242): VCR-RA-003 across-JOIN on the numeric-branch optimized path#819
feat(#242): VCR-RA-003 across-JOIN on the numeric-branch optimized path#819avrabe wants to merge 2 commits into
Conversation
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 Report❌ Patch coverage is
📢 Thoughts on this report? Let us know! |
|
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 Root cause: R8 is live-in at function entry (the validator's reg_effect sees the prologue push) and read again at the Two fixes attempted and REJECTED (both break soundness, verified against the red-first gate):
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 |
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
NotAttemptedon 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 stillNotAttempted(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