Skip to content

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

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

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.

@avrabe

avrabe commented Jul 23, 2026

Copy link
Copy Markdown
Contributor Author

Closing this draft — it won't merge as-is, and the board should carry only the release PR.

Why closed, not merged: the salvaged optimized-path across-JOIN extension over-rejects valid code (false JoinValueNotAvailable{R8} on cf_shapes_500::ifelse — a push {r5,lr}…pop {r5,pc} if/else). Two entry_seed fixes were tried and BOTH masked the red-first across-join clobber tests (verified), so shipping either would weaken the VCR-RA-003 acceptance oracle. The pre-existing behavior (optimized-path numeric-branch joins → honest NotAttempted) is correct; this PR regresses it.

Not lost: the join-CFG-builder infrastructure + the 6 ra003_numeric_* tests stay on branch feat/50-ra003-optimized-joins as groundwork. The proper redo is tracked (with cf_shapes_500::ifelse pinned as a red-first fixture and the correct 'available-at-entry iff PRESERVED — pushed-prologue AND popped-exit' discriminator) — it'll land as a fresh, correctly-gated lane in the v0.51 allocator-endgame work, not this branch. Closing keeps the tracker honest.

@avrabe avrabe closed this Jul 23, 2026
avrabe added a commit that referenced this pull request Jul 23, 2026
… endgame begins (#845)

* chore(release): v0.50.0 — cross-backend verified core + the allocator endgame begins (7-lane hub)

Wave 1: VCR-RA-003 RV32 alloc-validator (#815/#821), VCR-RA-003 ARM optimized-path
joins deferred (#819→redo), VCR-WASM i64 batch Qed 585→591 (#814). Wave 2: RV32
memory.size/grow parity (#841), WCET ph5 data-dep masked-ceiling certs (#839),
aarch64 void-block CF (#842), soundness sweep (WIP deferred), native i64 rem_u/rem_s
modeling via ordeal-0.12 Urem/bvsrem (#844), #837 frame-backing i64-param, and the
headline VCR-DEC-001 graph-colouring allocator spike flag-off (#843) — validated by
VCR-RA-003, flag-off byte-identical. Plus ci auto-merge for dependabot (#838).
Pin sweep 0.49.0→0.50.0; status.json/FEATURE_MATRIX regenerated; 25/25 claims;
frozen 10/10.

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

* revert(verify): i64.rem_u/rem_s native BvTerm::Urem/bvsrem model (#844) — solver hang

#844 replaced the I64RemU/I64RemS HAVOC in arm_semantics with a real 64-bit
`dividend.bvsrem/bvurem(&divisor)`. That query is the hardest bitvector class
there is, and it HANGS both solvers: the pure-Rust ordeal default (→ the CI
"Test" job) and the Z3 differential (→ the "Z3 Verification" job). Both jobs
have run 4-6h and timed out on EVERY CI run since #844 landed — the last green
CI on main was 2026-07-20 (61acec9). Confirmed independently: the L8 rem test
produced no output (hung) in salvage, and a separate agent's full workspace run
reached 107 test binaries / 0 failures and stalled only on this synth-verify
rem SMT test.

This restores the pre-#844 havoc model (byte-invisible — verify-only, no
codegen change, frozen anchors untouched by construction) to un-hang CI and
unblock the v0.50.0 tag. Native i64 rem re-lands in v0.51 behind a per-query
solver timeout so a hard bvurem degrades to `unknown` instead of hanging the
whole suite. Tracking: #848 (re-land behind a per-query solver timeout).

The term.rs/solver.rs BvTerm::Urem enum arms stay — they are the #836
ordeal-0.12 enum-completeness handlers (harmless; nothing in verify now
generates the variant).

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

* fix(#849): pin ordeal =0.9.1 — 0.12 bvsrem/bvsdiv perf regression HANGS CI

ROOT CAUSE of the 4-6h CI hangs (both the ordeal-default Test job and the Z3
Verification job) that have red-mained `main` since 2026-07-20: the ordeal
0.9.1 -> 0.12.0 dependabot bump (#825). 0.12 has a solver-performance
regression on bvsrem/bvsdiv that hangs div/rem trap-preservation VCs — even
the pre-existing 32-bit `rems_single_zero_guard_is_exactly_right` (I32RemS
Sdiv+Mls, #753/v0.43) hangs >240s on 0.12 but runs <1s on 0.9.1.

The last GREEN CI on main (61acec9, 2026-07-20 21:45:27) used ordeal 0.9.1 —
#825 merged 3 seconds later. NO commit with ordeal 0.12 has ever passed CI;
every subsequent lane auto-merged on the required-gate subset while Test/Z3
timed out. #844 (native i64 rem via 0.12 bvsrem/bvurem) made it far worse and
was reverted (db0f1f2, re-land #848); this pin is the actual fix.

Changes:
- crates/synth-verify/Cargo.toml: ordeal "0.12.0" -> "=0.9.1" (exact
  last-green pin; do-not-bump note added). Cargo.lock: ordeal + ordeal-lrat
  0.12.0 -> 0.9.1.
- Remove the four #836 `BvTerm::Urem` match arms (term.rs x3, z3-gated
  solver.rs x1) — that variant exists only in ordeal 0.12.

Verified: `cargo test -p synth-verify` = 236 tests, 0 failed, ~41s (was >6h
timeout on 0.12). Byte-invisible — verify-only, no codegen change, frozen
anchors untouched by construction.

Follow-ups (tracked, non-blocking): report the bvsrem/bvsdiv regression
upstream to ordeal; tighten .github/workflows/dependabot-auto-merge.yml (#838)
to HOLD 0.x MINOR bumps (0.9->0.12 is breaking by 0.x semver but dependabot
classified it "minor" and auto-merged it). See #849.

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

* docs(changelog): v0.50.0 — replace #844 i64-rem entry with the ordeal =0.9.1 pin (#849)

#844's native i64 rem value model was reverted (it depended on ordeal 0.12,
which has the bvsrem/bvsdiv perf regression that hangs CI). The real v0.50.0
change is the ordeal =0.9.1 pin. Do not advertise a reverted feature.

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

* fix(oracle): rv32 mem-size/grow — read symbols from ELF .symtab, not disasm text

The `rv32 memory.size / memory.grow execution oracle` (#841, VCR-SEL-005) has
FAILED on every CI run it actually executed — "FAIL — no symbol for export sz
([])" — the `syms` map came back EMPTY on the ubuntu runner. It located function
offsets by regex-parsing `synth disasm` TEXT (`^([0-9a-f]{8}) <(\w+)>:`), which
matched nothing on Linux for the `--relocatable` RISC-V object even though it
matched on macOS. It was merged ungated: main CI has been timing out since
2026-07-20 (ordeal-0.12 hang, #849), so this job was CANCELLED on every prior
run and its true `failure` never surfaced until the hang was fixed.

The codegen is correct — the oracle passes in every local configuration
(fresh binary, old + latest wasmtime 47.0.1). Only the symbol LOOKUP was
host-fragile. Fix: read function offsets from the ELF SYMBOL TABLE via
pyelftools (`.symtab`, `st_value` = offset within `.text` for a relocatable
object) — host-independent, the documented differential-harness lesson. The
`.text` bytes were already read via pyelftools; this just does the addresses
the same way. Drop the now-unused `re` import.

Verified: same addresses, oracle still PASS locally (sz=3/grow0=3/grow2=-1).
No codegen/frozen change.

Follow-up (non-blocking): 10 other repro oracles still regex-parse disasm text
(add_imm_large, bulk_memory_374, control_step_riscv, div_const, ...) — they pass
on CI today but carry the same latent host-dependency; harden them to symtab.

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

---------

Co-authored-by: Claude Opus 4.8 <noreply@anthropic.com>
avrabe added a commit that referenced this pull request Jul 28, 2026
…819 redo)

The numeric (optimized-path) join CFG seeds entry availability with the
PRESERVED callee-saved set — pushed-in-prologue AND popped-at-every-exit —
fixing the #819 false JoinValueNotAvailable{R8} hard-error on valid code
(cf_shapes_500::ifelse dead result-mov of a void function) WITHOUT touching
the label path's strict semantics (label red-first clobber tests keep their
teeth). Not merely-entry-live: the seed is anchored to the save/restore
contract and is empty on push-less functions, so garbage reads of
never-established registers stay Violations.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
avrabe added a commit that referenced this pull request Jul 28, 2026
RED: never-established callee-saved read at a numeric join (with prologue,
R6 outside the push set) + push-less contract-empty seed; GREEN: the
preserved one-arm-redef ifelse class (red-first-inverted), both-paths-define,
dominator-defined, loop back-edge universe-init; DECLINE: off-boundary
target + mixed label/numeric stream. Existing label ra003 clobber tests
untouched and still red-catching (26/26 ra003 green).

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
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