VCR-DEC-001 increment 3: graph-colouring allocator colours ACROSS CALLS — 57 of 68 declines taken, measured (#242) - #896
Merged
Conversation
… AND validator (#242) Increment 2's second-largest decline bucket was `call` / `call-indirect` (68 of the measured corpus): a `bl` had no modeled effect, so the join CFG builder refused the whole function. This increment models the AAPCS call boundary. ONE definition, TWO consumers — deliberately. `liveness::call_effect` states the contract once: defs = {R0,R1,R2,R3,R12,LR} (call-clobbered) uses = {R0,R1,R2,R3} + a `blx`'s target (arguments, conservatively all four — the callee signature is invisible here, and guessing an arity would silently corrupt a call whose argument we then recoloured) and it is consumed by BOTH `graph_alloc::joins` (liveness / interference / identity pins) AND `validate_cfg_rewrite`'s backward transfer. Modeling it in the pass alone would have been the #872 defect verbatim — the lane brief's own hazard: "a validator treating `bl` as effect-free would accept a non-identity equation across it", i.e. it would certify its own pass's "live value parked in call-clobbered scratch" miscompile. Before this commit `validate_cfg_rewrite` did exactly that (non-straight-line ops were required identical and then given NO effect). Deliberately NOT widening `reg_effect`: its `None`-on-call is load-bearing for the shipping pipeline (`body_uses_callee_saved`'s fail-safe prologue, `shrink_callee_saved_saves`' decline, VCR-RA-003 invariant 1), so widening it would move shipped bytes. `call_effect` is a separate, additive function. Pass side: `bl`/`blx` classify as FALL-THROUGH (interior, not a terminator); their webs are identity-pinned like a `Push`/`Pop` register list (#888) and the op is emitted VERBATIM with a re-check that both rename maps are the identity (`call-operand-recoloured` declines otherwise). Single-block functions containing a call are taken here too — increment 1 structurally cannot, since a call is not `is_straight_line`. Still declined by name: the HIGH-LEVEL `Call`/`CallIndirect` pseudo-ops (expanded downstream into a bounds guard + table load + result move, so the footprint here is not the one that ships). MEASURED (scripts/repro/vcr_dec_001_join_alloc_measure.py, ARM repro corpus): relocatable inc2 -46 B / -25 cyc, 275 applied -> inc3 -100 B / -33 cyc, 307 applied; 24 functions shrank (was 8), 0 cycle regressions self-contained inc2 -70 B / -9 cyc, 81 applied -> inc3 -120 B / -17 cyc, 108 applied; 27 shrank (was 10), 0 cycle regressions Decline histogram: `call` 57 -> 0 (taken); `call-indirect` 11 -> 11 (renamed `call-indirect-pseudo`, still out of scope). Flag stays OFF by default: frozen anchors 10/10 byte-identical, the flag-off path never enters this module. RED-FIRST, with the mutation that attributes the rejection to the call model: `cfg_validator_rejects_a_live_value_recoloured_across_a_call` shows R4->R2 across a `bl` is REJECTED (DefClobbersEquation) while the IDENTICAL rename over the IDENTICAL instructions with the `bl` DELETED is ACCEPTED — so the rejection comes from the call contract and nothing else. Plus: R4->R5 (callee-saved, both saved) accepted; a renamed call ARGUMENT rejected; the pass proven to colour a post-call temporary into scratch and to keep a cross-call value callee-saved. Co-Authored-By: Claude <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
… floor (#242) The AAPCS call contract is SHARED by the pass and `validate_cfg_rewrite` on purpose (two hand-maintained copies would be the VCR-ORACLE mirror-pinning failure mode) — which means neither validator can catch an error IN the contract itself. Only execution can. So the join execution differential grows a CALL population covering both halves of the contract: CLOBBER half — a value live ACROSS a `bl` must not be homed in caller-saved scratch: local_promote_cross_call::cross_call and intra_module_callee_saved::a (both written precisely so a caller-saved home is observably wrong), plus stack_canary_687::recurse (self-recursion: every activation re-enters the same allocation). ARGUMENT half — the registers a call READS must still hold what the callee expects: call_5args::caller and call_6_7args::call6/call7, whose callees pack each argument into its own nibble, so ANY dropped/shifted/mis-assigned argument changes the result. Harness changes: * AAPCS argument passing: 0-3 in R0-R3 (was R0-R2), 4+ on an 8-byte-aligned stack with the fifth at [sp,#0]. Without this the 5/6/7-arg fixtures would look like miscompiles. * `contains_call()` verifies a case's `is_call_shape` DECLARATION against the emitted Thumb bytes (bl imm / blx reg). A fixture whose call got inlined away can no longer inflate the increment-3 population while testing nothing. * Its own non-vacuity FLOOR: <4 divergent call-containing functions FAILS, and the machine-readable summary line carries CALLSHAPES= so the CI awk pins the same floor (#890 — exit 0 alone is never trusted). Result: 56/56 checks, 19 engaged functions of which 6 are call shapes. Co-Authored-By: Claude <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
…ANGELOG (#242) MUTATION MATRIX over the shared AAPCS contract (`liveness::call_effect`), run to find out what each half is actually buying: uses = [] KILLED by cfg_validator_rejects_a_renamed_call_argument (unit) and by the execution differential (5 wrong results: call6(1,2,3,4,5,6) -> 0x00651321 vs 0x00654321) once the churn bias is replaced by a churn-MAXIMISING one. Control: the churn-maximising bias ALONE, contract intact, gives 0 wrong results — so the failure is attributable to the contract, not to the bias. defs = [] SURVIVES. Documented, not papered over: with the conservative `uses` intact the two halves OVERLAP for the R0-R8 pool (a value live across a call must be defined above it, and the argument equation then collides with the rewritten definition). `defs`' independent duties today are the non-pool {R12,LR} and keeping the PASS from proposing colourings the oracle would only reject. The `call_effect` doc now warns that an arity-precise `uses` — the obvious next reach win — makes `defs` the SOLE soundness guard for R0-R3, so the two must be narrowed/tested together. both = [] (the pre-increment-3 effect-free `bl` — the briefed hazard) KILLED by three unit tests. `cfg_validator_rejects_a_renamed_call_argument` was sharpened after the matrix showed the original R0-staged/`bx lr` form was vacuous w.r.t. the call model: `bx lr`'s STRICT exit seed demanded R0 all by itself. It now stages R3 and renames to R2 inside a `pop {…,pc}` frame, where BOTH are dead-out per `cfg_exit_observable`, so only the argument use can reject it. Also: the measure script's docstring no longer claims the self-contained half "must be flat" (it is not, and was not in increment 2 either — 108 functions apply there now), and names the decline histogram as the actionable output that picks the next increment. Verification by REAL exit code: cargo fmt --check 0, clippy --workspace --all-targets -D warnings 0, cargo test --workspace 0 (frozen anchors 10/10), claim_check 34/34, byte differential 0, execution differential 0 (56/56, CALLSHAPES=6). Co-Authored-By: Claude <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
Codecov Report❌ Patch coverage is
📢 Thoughts on this report? Let us know! |
avrabe
added a commit
that referenced
this pull request
Jul 30, 2026
…NGELOG after rebase Two fixes on top of the rebase onto main (which now carries L4 #896 and the bare-pipefail hardening #900). 1. **wat2wasm was missing.** Both failing sweeps died with `FileNotFoundError: 'wat2wasm'`. That is the gate DOING ITS JOB: these 63 oracles had never run in CI, so their host dependencies had never been discovered — exactly the class that made the #881 VFP oracle fail on the runner while passing locally (#850). Several fixtures build their .wasm from .wat at test time. wabt installed in all four sweep jobs. 2. **Restored this lane's CHANGELOG entries.** My conflict resolution kept the `# ci-status:` header lines plus main's side, which is correct for the repro scripts and WRONG for an additive CHANGELOG — it silently dropped all four of the lane's bullets. Recovered verbatim from the pre-rebase branch and merged with the existing entry. Caught by counting bullets after the rebase rather than trusting that a clean `rebase --continue` meant a clean result. Rebase conflict in vcr_dec_001_join_alloc_execution_differential.py resolved keeping BOTH sides: L4's updated "increments 2+3" docstring and this lane's ci-status header. Co-Authored-By: Claude <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
avrabe
added a commit
that referenced
this pull request
Jul 30, 2026
…nual / 0 undeclared (#894) * feat(#890): oracle-wiring gate — declared ci-status per repro script (step 1/5) Adds scripts/oracle_wiring_check.py: every scripts/repro/*.py|*.sh must carry exactly one `# ci-status:` declaration (wired | manual (<category>) — reason | unwired — reason), and a `wired` declaration is VERIFIED against .github/workflows/*.yml so a green board can never sit on top of an inert gate. Step 1 declares the 82 scripts a workflow already references. The remaining 70 are UNDECLARED and the gate is red on them by construction — classified next. Co-Authored-By: Claude <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L * feat(#890): classify all 152 repro scripts — 7 manual with real reasons (step 2/5) Read and classified the 70 scripts no workflow referenced. 63 of them run green against a freshly built synth right now (verified locally, one at a time) and are wired in the next step; 7 are genuinely manual and say WHY, in a closed category vocabulary (measurement / scratch / external-input) rather than free text. Three enabling fixes fall out of the audit: * base_cse / leaf_dead_frame / load_store_big_offset_382 / uxth_fold hardcoded ./target/{debug,release}/synth; they now honour $SYNTH (same literal default) so CI can point them at its own build. * sret_decide_differential printed "MISMATCH <-- BUG" and still exited 0 — wiring it as-is would have added a gate that CANNOT fail. The verdict is now the exit status (proved: mutating the -35 expectation to -34 gives rc=1). The gate is deliberately still red: 63 files declare `wired` while no workflow references them. That is the exact defect being fixed, and it is now MACHINE VISIBLE instead of requiring a 150-file read. Co-Authored-By: Claude <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L * feat(#890): wire 63 forgotten oracles + CI-wire the gate itself (step 3/5) Four new sweep jobs (selector / memory / rv32 / wcet) plus one step in the existing fact-spec job run the 63 differentials that were sitting in scripts/repro/ with nothing executing them. Every one was verified green locally against a freshly built synth before being wired — the compile line comes from each harness's own documented Run: block. Highlights of what was NOT being gated: the six mem757_* red-first reconstructions of gale's wrong-segment miscompile (#757); every RV32 oracle for a regression gale found on real silicon (#220/#226/#232/#317/#343); all four WCET soundness cross-checks — the only thing that EXECUTES the fixtures and checks bound_cycles >= executed_instructions, i.e. the evidence behind the "sound WCET bound" claim; and the #494 rem_u identity differential behind the beat-clang headline. The gate itself is wired IN THE SAME COMMIT, as a step in claim-check — an ALREADY-REQUIRED context on main. A brand-new job would not be required, so it could sit red for weeks without blocking anything: the exact failure mode. It uses `set -o pipefail` and re-reads its own JSON summary to assert a non-zero wired count over a non-empty script set, so a run that measured nothing fails instead of greening on exit 0. Co-Authored-By: Claude <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L * feat(#890): ratchet the manual/unwired budgets + policy doc (step 4/5) claims.yaml SYNTH-ORACLE-WIRING-890 pins the totals the header comments cannot express: wired >= 145 (a FLOOR — the oracle surface must not be emptied by deleting harnesses instead of fixing them), manual <= 7 (a ceiling on the legitimate escape hatch), unwired <= 0 (a ceiling of ZERO — a new un-wired oracle is a red build, not a backlog entry). Proved by mutation: flipping one wired script to manual fails BOTH the floor and the ceiling legs. This generalizes SYNTH-GPIO-846-ORACLE-CI-WIRED, which hand-pins exactly one script's CI wiring — the instance-at-a-time shape #890 exists to replace. Also hardens the gate after a mutation found a real defect in it: `pipefail` without `-e` let the INERT-GATE mutation green the CI step, because the shell's status is its last command's. The step now sets `-euo pipefail` explicitly and the summary carries `wired_unreferenced` + `failures` so the verdict is reachable from the summary alone, never from exit 0. scripts/repro/ORACLE_WIRING.md documents the mechanism, argues header-over- manifest, itemizes the manual seven, and carries the four-mutation transcript (each run executes the step extracted VERBATIM from ci.yml, so there is no drift between what was proved and what CI runs). Co-Authored-By: Claude <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L * fix(#890): a COMMENT mention must not count as wired (step 5/5) The gate derived "referenced by a workflow" from a raw grep of the .yml, so a mention in a COMMENT satisfied it — a gate satisfiable by prose, which is the exact failure shape #890 exists to reject. References now come from the PARSED workflow: each step's `run:` body plus its `with:`/`env:` values. A workflow that will not parse is a hard error, never a silent pass. No script changed status (verified before the change: zero of the 145 wired were wired by a comment alone), so this is pure future-proofing — but the diagnostic now says WHY: "It IS mentioned in ci.yml, but only in a COMMENT — prose does not run an oracle." Mutation matrix against the final gate, each run executing the step extracted VERBATIM from ci.yml (no drift between what was proved and what CI runs): baseline EXIT 0 M1 un-declare a script EXIT 1 UNDECLARED M2 declare wired, no reference at all EXIT 1 the gate is INERT M3 delete a wired oracle's CI step EXIT 1 the gate is INERT M4 gate's glob matches nothing EXIT 1 VACUOUS ['total<100'] M5 reference demoted to a comment EXIT 1 only in a COMMENT M6 manual reason replaced with "TODO" EXIT 1 needs a REAL reason restored EXIT 0 Co-Authored-By: Claude <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L * docs(#890): record the REAL CI-red evidence for the oracle-wiring gate A gate that has never been seen to fire is indistinguishable from one that cannot — which is the #890 thesis applied to #890 itself. So both required mutations were run through GitHub, not just locally: a throwaway branch carrying only the two mutations turned the real `Claim Check` job red at the Oracle wiring gate step (PR #895, closed unmerged, branch deleted). oracle wiring: 152 repro scripts — 145 wired, 6 manual, 0 unwired(debt), 1 UNDECLARED FAIL ... mem757_ptr_base_copy_differential.py: UNDECLARED ... FAIL ... wake_path_differential.py: declares `wired` but NO workflow references it — the gate is INERT ... ##[error]Process completed with exit code 1. Co-Authored-By: Claude <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L * docs(#890): the gate docstring says PARSED-workflow, matching the implementation Co-Authored-By: Claude <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L * fix(#890): scope the dangling-reference check to the executable surface The reverse check (a workflow step running a repro script that no longer exists) scanned the RAW .yml, so a stale mention in a COMMENT would have been reported as a "dangling CI step" — a false red, and the wrong diagnosis: untidy prose is not a broken gate. It now scans the same executable surface the forward check uses. Proved still live by mutation: adding a step that runs a nonexistent script fails with the dangling-step message (EXIT 1). Co-Authored-By: Claude <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L * ci(#890): install wabt in the four repro sweeps; restore the lane CHANGELOG after rebase Two fixes on top of the rebase onto main (which now carries L4 #896 and the bare-pipefail hardening #900). 1. **wat2wasm was missing.** Both failing sweeps died with `FileNotFoundError: 'wat2wasm'`. That is the gate DOING ITS JOB: these 63 oracles had never run in CI, so their host dependencies had never been discovered — exactly the class that made the #881 VFP oracle fail on the runner while passing locally (#850). Several fixtures build their .wasm from .wat at test time. wabt installed in all four sweep jobs. 2. **Restored this lane's CHANGELOG entries.** My conflict resolution kept the `# ci-status:` header lines plus main's side, which is correct for the repro scripts and WRONG for an additive CHANGELOG — it silently dropped all four of the lane's bullets. Recovered verbatim from the pre-rebase branch and merged with the existing entry. Caught by counting bullets after the rebase rather than trusting that a clean `rebase --continue` meant a clean result. Rebase conflict in vcr_dec_001_join_alloc_execution_differential.py resolved keeping BOTH sides: L4's updated "increments 2+3" docstring and this lane's ci-status header. Co-Authored-By: Claude <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L --------- Co-authored-by: Claude <noreply@anthropic.com>
avrabe
added a commit
that referenced
this pull request
Jul 30, 2026
…242, #896) L4 (#896) taught the graph allocator to colour ACROSS CALLS, taking 57 of 68 `call` declines. My gate declined every one of them (`NotAttempted { reason: "call" }`), which would have taken increment 3's reach to zero — L4's own `colours_across_a_call` was the visible symptom. Modelled rather than exempted. `abi_gate` still treats `NotAttempted` as a DECLINE; what changed is that a call is no longer un-analyzable. - `classify` gains `Cf::CallOp`, keyed on `liveness::call_effect` returning `Some` rather than on a variant list, so this classifier and the pass's notion of "a call this allocator may colour across" CANNOT DRIFT. Reusing L4's single definition is the point: two divergent call models would be a fresh instance of the shared-blind-spot class this module attacks. - A call FALLS THROUGH (it does not end a basic block) and is required byte-identical on both sides — the same rule `validate_cfg_rewrite` enforces, so `blx`'s target register is never renamed under us. - The forward walk needed no special case, which is the design paying off: each clobbered register `{R0-R3, R12, LR}` is rebound to a FRESH `Def(call_i, k)` node whose operands are the PRE-CALL argument values, while `R4-R11`/`SP` flow through untouched. So a call result is an opaque value equal across the sides exactly when the same callee got the same arguments, and a value the rewrite parked in caller-saved scratch across the call is rebound to the call's own node — it can no longer bisimulate with what the original delivers at the return. That is L4's warning discharged as a VALUE disagreement, with no liveness reasoning anywhere: `recolouring_a_live_value_into_caller_saved_across_a_call_is_violated`. - `Call`/`CallIndirect` PSEUDO-ops still decline (`call-pseudo-op`): they expand downstream into a guard + table load + `blx`, so this stream's register footprint is not the final code's. 6 new unit gates: a call is modelled not declined; callee-saved → other callee-saved holds; the caller-saved-across-a-call recolour is VIOLATED; returning the call result directly holds; renaming what feeds an argument is VIOLATED (this is what `call_effect`'s `uses` buy); a rewritten call target declines. The pre-existing mid-block decline test was repointed at `BrTable`, since `bl` is no longer the unanalyzable case. Also documented: a call's MEMORY effect is not modelled — a restatement of the standing memory limitation at the place it is easiest to forget. Sound for a renames-only rewrite (both sides run the same callee at the same point); not a claim about the callee's effects. cargo fmt --check / clippy --workspace --all-targets -D warnings / test --workspace: all exit 0, incl. L4's `colours_across_a_call`. Co-Authored-By: Claude <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
avrabe
added a commit
that referenced
this pull request
Jul 30, 2026
… tree (#242) Context-only rebase — the two SEMANTIC edits are byte-identical (empty `cfg_exit_observable`; drop the churn bias in `color_webs_biased`). Increment 3 (#896) moved the surrounding lines, so the old hunks no longer applied and the acceptance script FATAL'd rather than silently skipping. Co-Authored-By: Claude <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
avrabe
added a commit
that referenced
this pull request
Jul 30, 2026
The call model changes all three headline measurements, so all three are re-derived rather than left stale. - Corpus reach: 275 applied / -46 B -> 307 applied / -100 B relocatable (-120 B self-contained). That is increment 3's result TO THE BYTE: the gate composes with #896 at zero cost, still zero false rejections. - Shipping-path audit: Holds 376 -> 422, NotAttempted 241 -> 195, Violated 0 (unchanged). ~61 % -> ~68 % of the default path now carries a proven observable return contract. The 62 `call` declines are GONE, not reclassified; `unmodeled-op` rose 159 -> 174 because functions that used to stop at the call now get further and reach an FP / i64-pair op instead. The decline MOVED, it did not vanish — said in both the script docstring and the CHANGELOG, because "declines dropped by 46" would be the flattering half of the truth. - HOLDS_FLOOR 340 -> 400. A floor left at the pre-call-model value would have silently absorbed losing the entire call model again, which is the same absorbed-regression failure the floor exists to prevent. FEATURE_MATRIX honest summary re-derived via the sanctioned `claim_check.py --emit-status` (never hand-edited, #805). claim_check: 35/35 hold. fmt / clippy -D warnings / test --workspace: exit 0. Frozen anchors 10/10. Co-Authored-By: Claude <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
avrabe
added a commit
that referenced
this pull request
Aug 4, 2026
… check that fails differently (#242) (#897) * VCR-VER-004: the ABI observable-contract validator — a check that fails differently (#242) v0.53's VCR-DEC-001 lane proved BY MUTATION that emptying `cfg_exit_observable` — the exit contract the join-aware graph allocator and its own CFG validator SHARE — emits code leaving the return value in the wrong register, and that BOTH per-compilation validators accept it (`validate_cfg_rewrite` -> Ok, VCR-RA-003 `validate_final_allocation` -> Consistent). Only execution caught it. Two independent-LOOKING instruments, one shared blind spot. This is the first step of the response: a validator built on a different axis, not a second file on the same axis. `abi_contract::validate_abi_contract(orig, rewritten)`: - OBLIGATION CANNOT BE EMPTIED. The exit obligation is RETURN_CONTRACT_REGS = [R0, R1] — a constant of the AAPCS, hard-named here. Deleting `cfg_exit_observable` outright would not change one line of this check. - FORWARD, so it is structurally incapable of the v0.53 fail-open mode. `validate_cfg_rewrite` is a backward MUST-analysis whose obligation set is a VARIABLE, and the empty set is a fixpoint. A forward symbolic evaluation always produces exactly one value for R0 at each return, so there is always exactly one obligation per sink. There is no seed to shrink. - EVIDENCE IS A VALUE, not a register-name pair. Per side independently, build a value graph over Init(r) / Def(i,k) / Phi(b,n) nodes and compare by GREATEST-FIXPOINT BISIMULATION (partition refinement). On a deterministic term graph bisimilarity is equality of the infinite unfoldings, so loops and back edges are handled coinductively — no unrolling. - TAKES NOTHING FROM THE PASS. The signature is (orig, rewritten): the CFG is re-derived here from BOTH streams' label-form branch structure and the two must agree. The v0.50 join attempt failed by letting the pass hand the checker its own seed. - Init(r) is ONE node shared by both sides — that is the AAPCS PARAMETER half of the anchor, so reading a param out of the wrong register is a value change too. Documented in-module, not hidden: memory is not in the obligation (a store-only misrename is a named false NEGATIVE — the class `validate_cfg_rewrite` DOES cover when its seed is intact; the two instruments are complementary); `reg_effect` is still shared, so a mismodeled op remains a common blind spot; and the reason there is no SMT solver (for a renames-only rewrite the terms are ground applications of the same uninterpreted operators, so a query would decide exactly the structural equality the refinement already computes — and the synth-verify dependency edge runs the wrong way). 18 unit gates, including two FAIL-OPEN bugs this module's own red-first testing found and fixed: a `bl` that is not a block ENDER was walked past as a no-op, and every op is now classified wherever it sits. Pure addition — not yet wired into any pass, so zero emitted bytes change. Co-Authored-By: Claude <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L * VCR-VER-004: wire the ABI contract as a second, independent acceptance gate + the mutation repro (#242) The instrument from the previous commit is now LOAD-BEARING, and v0.53's exact mutation is re-runnable as a committed artifact. - graph_alloc: both entry points (increment 1 straight-line, increment 2 joins) now require BOTH the dataflow validator AND `abi_contract::validate_abi_contract`. `NotAttempted` is a DECLINE, not an accept: if a decline counted as acceptance, a change that made the check universally inapplicable would disable it SILENTLY — the vacuity failure this lane exists to prevent. So: a function this pass applies to has been ABI-contract-certified, or it was not applied. - graph_alloc: announce the dataflow ACCEPT under SYNTH_GRAPH_ALLOC_STATS before the second gate runs. That line is what makes the new gate's rejection non-vacuous: it is an OBSERVATION that the pre-VCR-VER-004 compiler would have emitted the rewrite. - scripts/repro/mutations/v053_shared_exit_contract.patch: v0.53's mutation verbatim (empty `cfg_exit_observable` + drop the churn bias), committed so the red-first evidence is the ACTUAL mutation, not a reconstruction. - scripts/repro/vcr_ver_004_instrument_independence.py: applies that patch, rebuilds, and asserts on ONE compilation of ONE fixture that (1) validate_cfg_rewrite ACCEPTS, (2) VCR-RA-003 says Consistent, (3) VCR-VER-004 REJECTS with a concrete violation naming the ABI result register, and (4) the miscompile is therefore not emitted. It also asserts the BASELINE direction first — the unmutated compiler must still APPLY and must NOT be rejected — so a false-rejection regression fails the script before it ever reaches the mutation. Always restores the tree. MEASURED, on the whole ARM repro corpus (relocatable / label-form): functions measured 617, graph-alloc APPLIED 275, bytes 40822 -> 40776 (-46, -0.11%), 8 shrank / 1 grew which is v0.53's result to the BYTE. The gate — conservative enough to require BOTH R0 and R1 for every function, and to decline whenever it cannot analyze — costs ZERO reach on the unmutated compiler. The join execution differential is unchanged at 38/38, ENGAGED=13. Under the mutation: ENGAGED drops to 0, no wrong result is emitted, and the compiler names the reason — `Violated { sink: 81, reg: R0 }` on brif_outer_740::poll, the function that returned 0x1111 instead of its parameter. Frozen anchors unaffected: SYNTH_GRAPH_ALLOC is flag-off, so no shipped byte can move. Co-Authored-By: Claude <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L * VCR-VER-004: CI-wire the independence oracle + make two synthetic fixtures well-formed (#242) - ci.yml: `instrument-independence-oracle`, an ISOLATED job (the script mutates the tree and rebuilds). `set -o pipefail`, a machine-readable 4/4 assertion AND a non-zero OK-count grep (#890), plus a final `git diff --exit-code` so a mutation can never persist into the repo. - The script's own RED-FIRST evidence is now recorded in its docstring and is reproducible: change `abi_gate` to treat `Violated` as an accept, rebuild with the mutation applied, and the compiler prints `whole-function colouring APPLIED (validated)` and EMITS the miscompile (assertions (3) and (4) both fail). With the gate intact it declines. Verified by running it. - graph_alloc unit fixtures: two synthetic bodies had NO return terminator, so the new gate declined them. Fixed by making the fixtures WELL-FORMED FUNCTIONS (append the `pop {r4, pc}` epilogue), NOT by weakening the check — a stream with no return sink has no ABI contract to check, and passing it would be exactly the vacuous-green failure this lane exists to prevent. The appended epilogue sits at an index after every def index the second test reasons about, so its non-vacuity argument is untouched. This is the only false-REJECTION the gate produced anywhere: 617 real corpus functions, 275 applied, byte-identical to v0.53. cargo fmt --check / clippy --workspace --all-targets -D warnings / test --workspace: all exit 0. Frozen anchors 10/10. Co-Authored-By: Claude <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L * VCR-VER-004: measure the SHIPPING allocator against the ABI contract, and pin the result (#242) The gate so far guards the flag-OFF graph-colouring spike. Users do not compile with that. This asks the same question of `reallocate_function_post_exhaust` — the allocator every `synth compile` runs — and turns the answer into an enforced CI floor. MEASURED (617 corpus functions, --relocatable): Holds 376 · NotAttempted 241 · Violated 0 declines: unmodeled-op 159, call 62, indirect-call 11, numeric-offset-branch 9 So a value-level, ABI-anchored, forward check can PROVE the observable return contract on 61% of the shipping path today, with ZERO false rejections against an allocator that is frozen-pinned and execution-differentialed — i.e. known-good. - arm_backend: `SYNTH_ABI_CONTRACT_AUDIT=1`, report-only. Report-only DELIBERATELY: making it gate the default path means hard-erroring a user's compile on a checker whose false-positive rate is MEASURED, not proven. The honest sequence is measure first, flip on evidence — and this is the measurement. - scripts/repro/vcr_ver_004_shipping_path_audit.py + CI: asserts ZERO Violated (a violation is either a real shipping miscompile or a false rejection by the new instrument — neither may pass silently) and a pinned Holds FLOOR of 340, so a change that makes the checker see LESS of the shipping path is visible rather than absorbed. Coverage is the honest weak point of a checker that declines on calls and unmodeled ops, so coverage is what gets pinned. RED-FIRST by real exit code, both directions: a stub binary emitting a `Violated` line -> exit 1 naming the fixture; a stub emitting NOTHING -> exit 1 on the vacuity assertion, so a stale binary or an un-wired hook cannot pass while gating nothing. Real binary -> exit 0. cargo fmt --check / clippy --workspace --all-targets -D warnings / test --workspace: all exit 0. Report-only hook, so no emitted byte moves. Co-Authored-By: Claude <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L * docs(VCR-VER-004): CHANGELOG entry + close the v0.53 residual in the honest summary (#242) The FEATURE_MATRIX honest summary already recorded this exact residual — "a wrong-return-register rewrite is accepted by validate_cfg_rewrite AND VCR-RA-003 *both*, caught only by execution". It is now marked CLOSED STATICALLY, with the evidence (a CI job re-running v0.53's own mutation), and — more importantly — with what the lane did NOT close spelled out rather than implied away: * gate on the flag-OFF spike; on the DEFAULT path an audit held to a CI floor (Holds 376 / NotAttempted 241 / Violated 0 of 617), because hard-erroring a user's compile on a checker whose false-positive rate is MEASURED rather than proven is a flip that wants its own evidence; * memory is not in the obligation — a store-only misrename is a false NEGATIVE here, and is the class validate_cfg_rewrite covers when its seed is intact (complementary, not redundant); * `reg_effect` is still shared, so a MISMODELED OP remains a blind spot common to all three instruments. Until synth-verify's independent ArmSemantics is pinned against it, "three independent validators" would be an OVERCLAIM, and the summary says so. docs/status/FEATURE_MATRIX.md regenerated with the sanctioned `claim_check.py --emit-status` (never hand-edited, #805); the diff is additive only. claim_check: 34/34 hold. Co-Authored-By: Claude <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L * VCR-VER-004: model the AAPCS call effect — compose with increment 3 (#242, #896) L4 (#896) taught the graph allocator to colour ACROSS CALLS, taking 57 of 68 `call` declines. My gate declined every one of them (`NotAttempted { reason: "call" }`), which would have taken increment 3's reach to zero — L4's own `colours_across_a_call` was the visible symptom. Modelled rather than exempted. `abi_gate` still treats `NotAttempted` as a DECLINE; what changed is that a call is no longer un-analyzable. - `classify` gains `Cf::CallOp`, keyed on `liveness::call_effect` returning `Some` rather than on a variant list, so this classifier and the pass's notion of "a call this allocator may colour across" CANNOT DRIFT. Reusing L4's single definition is the point: two divergent call models would be a fresh instance of the shared-blind-spot class this module attacks. - A call FALLS THROUGH (it does not end a basic block) and is required byte-identical on both sides — the same rule `validate_cfg_rewrite` enforces, so `blx`'s target register is never renamed under us. - The forward walk needed no special case, which is the design paying off: each clobbered register `{R0-R3, R12, LR}` is rebound to a FRESH `Def(call_i, k)` node whose operands are the PRE-CALL argument values, while `R4-R11`/`SP` flow through untouched. So a call result is an opaque value equal across the sides exactly when the same callee got the same arguments, and a value the rewrite parked in caller-saved scratch across the call is rebound to the call's own node — it can no longer bisimulate with what the original delivers at the return. That is L4's warning discharged as a VALUE disagreement, with no liveness reasoning anywhere: `recolouring_a_live_value_into_caller_saved_across_a_call_is_violated`. - `Call`/`CallIndirect` PSEUDO-ops still decline (`call-pseudo-op`): they expand downstream into a guard + table load + `blx`, so this stream's register footprint is not the final code's. 6 new unit gates: a call is modelled not declined; callee-saved → other callee-saved holds; the caller-saved-across-a-call recolour is VIOLATED; returning the call result directly holds; renaming what feeds an argument is VIOLATED (this is what `call_effect`'s `uses` buy); a rewritten call target declines. The pre-existing mid-block decline test was repointed at `BrTable`, since `bl` is no longer the unanalyzable case. Also documented: a call's MEMORY effect is not modelled — a restatement of the standing memory limitation at the place it is easiest to forget. Sound for a renames-only rewrite (both sides run the same callee at the same point); not a claim about the callee's effects. cargo fmt --check / clippy --workspace --all-targets -D warnings / test --workspace: all exit 0, incl. L4's `colours_across_a_call`. Co-Authored-By: Claude <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L * chore(VCR-VER-004): re-generate the v0.53 mutation patch against L4's tree (#242) Context-only rebase — the two SEMANTIC edits are byte-identical (empty `cfg_exit_observable`; drop the churn bias in `color_webs_biased`). Increment 3 (#896) moved the surrounding lines, so the old hunks no longer applied and the acceptance script FATAL'd rather than silently skipping. Co-Authored-By: Claude <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L * docs(VCR-VER-004): re-pin every number after the call model (#242, #896) The call model changes all three headline measurements, so all three are re-derived rather than left stale. - Corpus reach: 275 applied / -46 B -> 307 applied / -100 B relocatable (-120 B self-contained). That is increment 3's result TO THE BYTE: the gate composes with #896 at zero cost, still zero false rejections. - Shipping-path audit: Holds 376 -> 422, NotAttempted 241 -> 195, Violated 0 (unchanged). ~61 % -> ~68 % of the default path now carries a proven observable return contract. The 62 `call` declines are GONE, not reclassified; `unmodeled-op` rose 159 -> 174 because functions that used to stop at the call now get further and reach an FP / i64-pair op instead. The decline MOVED, it did not vanish — said in both the script docstring and the CHANGELOG, because "declines dropped by 46" would be the flattering half of the truth. - HOLDS_FLOOR 340 -> 400. A floor left at the pre-call-model value would have silently absorbed losing the entire call model again, which is the same absorbed-regression failure the floor exists to prevent. FEATURE_MATRIX honest summary re-derived via the sanctioned `claim_check.py --emit-status` (never hand-edited, #805). claim_check: 35/35 hold. fmt / clippy -D warnings / test --workspace: exit 0. Frozen anchors 10/10. Co-Authored-By: Claude <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L * chore(#890): declare the two VCR-VER-004 oracles `# ci-status: wired` L1's oracle-wiring gate landed on main after this lane wrote its scripts, so they had no `# ci-status:` header and Claim Check went red: oracle wiring: 154 repro scripts — 145 wired, 7 manual, 0 unwired, 2 UNDECLARED FAIL vcr_ver_004_instrument_independence.py: UNDECLARED FAIL vcr_ver_004_shipping_path_audit.py: UNDECLARED The gate working on its first real encounter, exactly as intended. `wired` is the honest declaration here, verified rather than assumed -- each has a real `ci.yml` reference. Gate now: 154 scripts, 147 wired, 7 manual, 0 unwired, 0 UNDECLARED, exit 0. Co-Authored-By: Claude <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L --------- Co-authored-by: Claude <noreply@anthropic.com>
This was referenced Aug 5, 2026
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
v0.54 lane L4 — VCR-DEC-001 increment 3 (epic #242, the North Star allocator endgame).
Flag-off measurement spike. Do not merge before the coordinator sequences the lane fan-in.
What
Increment 2 (v0.53) colours across if/else joins. Its second-largest decline
bucket was
call/call-indirect— 68 of the measured corpus — because ablhad no modeled effect and the join CFG builder refused the whole function.This increment models the AAPCS call boundary and takes 57 of the 68.
The hazard, and how it is closed
The lane brief named it: "calls need the AAPCS clobber contract modelled in
BOTH the pass AND the validator — a validator treating
blas effect-free wouldaccept a non-identity equation across it." That was not hypothetical:
validate_cfg_rewritedid exactly that (a non-straight-line op was requiredidentical and then given NO effect), so an equation
(R4, R2)demanded after acall sailed straight through it.
liveness::call_effectnow states the contract once:and BOTH consumers read that one definition — the pass (
graph_alloc::joinsliveness / interference / identity pins) and the oracle
(
validate_cfg_rewrite's backward transfer). Sharing is deliberate: twohand-maintained copies would be the VCR-ORACLE mirror-pinning failure mode. The
honest consequence — neither validator can catch an error in the contract —
is what the execution differential is for.
reg_effectis deliberately NOT widened: itsNone-on-call is load-bearing forthe shipping pipeline (fail-safe prologue,
shrink_callee_saved_saves' decline,VCR-RA-003 invariant 1), so widening it would move shipped bytes.
Calls are emitted verbatim, with both rename maps re-checked as the identity
(
call-operand-recoloureddeclines otherwise). Single-block functionscontaining a call are taken too — increment 1 structurally cannot, since a call
is not
is_straight_line.Measured (the deliverable)
scripts/repro/vcr_dec_001_join_alloc_measure.py, ARM repro corpus. Bytes fromthe ELF symtab, cycles from
--emit-wcetsound bounds.Zero WCET-bound regressions on either path (12 bounds shrank, 0 grew).
Decline histogram (relocatable)
unmodeled-opsingle-blockcallidentity-colouringcall-indirectcall-indirect-pseudo)unreachable-blocknumeric-branchOf the 57 taken, 32 became applied colourings; the other 25 moved on to the NEXT
construct they contain (a numeric branch, an unmodeled i64/FP op, or an identity
colouring) — a decline that MOVED, never one that was deleted. The residual 11
are the high-level
Call/CallIndirectpseudo-ops, expanded downstream intoa bounds guard + table load + result move, so the register footprint here is not
the one that ships; they stay declined by name.
Gates
SYNTH_GRAPH_ALLOCunset never enters the module; frozenanchors byte-identical 10/10 (
frozen_codegen_bytes.rs+vcr_dec_001_graph_alloc_differential.pyproperty 1).validate_cfg_rewriteclean on every emitted function(observed via
SYNTH_RA003_VERBOSE, not inferred from an exit code).Necessary, not sufficient — see below.
Mutation evidence
The contract is shared, so only execution can catch an error in it. A matrix over
its two halves:
uses = [](argument half)cfg_validator_rejects_a_renamed_call_argument. Execution: 5 wrong results —call6(1,2,3,4,5,6)returns0x00651321vs wasmtime's0x00654321— once the churn bias is replaced by a churn-maximising one that stops masking it.validate_cfg_rewriteAND VCR-RA-003 both accept the mutant.defs = []anduses = [](the pre-increment-3 effect-freebl— the briefed hazard)defs = []alonecall_effect, not papered over — see below.The surviving mutant is a finding, not a hole. With the conservative
usesintact the two halves OVERLAP for the R0-R8 pool: a value live across a call must
be defined above it, and the
(r, r)argument equation the call generates thencollides with the rewritten definition. So
defs' independent duties today are(a) the non-pool
{R12, LR}and (b) keeping the PASS from proposing colouringsthe oracle would only reject — reach, not soundness. That flips the moment
usesis narrowed: an arity-precise argument set (the obvious next reach win —an unused argument register currently stays live all the way back from the call
and blocks that colour) makes
defsthe sole soundness guard for R0-R3. Thecall_effectdoc says so, in those words, next to the constants.Also fixed by the matrix:
cfg_validator_rejects_a_renamed_call_argumentwasoriginally vacuous w.r.t. the call model — its
bx lrSTRICT exit seed demandedR0 all by itself. It now stages R3 and renames to R2 inside a
pop {…,pc}framewhere both are dead-out per
cfg_exit_observable, so only the argument usecan reject it.
Execution differential (CI-wired, same commit)
New CALL population covering both halves:
local_promote_cross_call::cross_callandintra_module_callee_saved::a(both written so a caller-saved home isobservably wrong) + the self-recursive
stack_canary_687::recurse.call_5args::caller,call_6_7args::call6/call7, whosecallees pack each argument into its own nibble, so any dropped, shifted or
mis-assigned argument changes the result.
Harness: AAPCS argument passing (0-3 in R0-R3, 4+ on an 8-byte-aligned stack —
without it the 5/6/7-arg fixtures would look like miscompiles); every declared
call shape is verified to really CONTAIN a
bl/blxin its emitted bytes(self-declaration checked against bytes); its own non-vacuity floor of ≥4
divergent call-containing functions, re-asserted by the CI
awkfrom the newCALLSHAPES=summary field (#890). 56/56 checks, 19 engaged functions, 6 callshapes.
Verification (REAL exit codes)
cargo fmt --check0 ·cargo clippy --workspace --all-targets -D warnings0 ·cargo test --workspace0 ·claim_check.py34/34 ·vcr_dec_001_graph_alloc_differential.py0 ·vcr_dec_001_join_alloc_execution_differential.py0.Named follow-ups (not done here, deliberately)
usesis the mainreach cost: an argument register with no in-function definition stays live
from the entry to the call and blocks that colour across the whole prefix.
Requires threading callee signatures into the allocator. Read the
defswarning above before doing it.
shrink_callee_saved_savesis leaf-only (it declines on anyreg_effect == Noneop, i.e. every call), so evacuating R4-R8 in a call-containingfunction does not shrink its prologue today — increment 3's size win comes
from encoding widths, not from the push/pop lever that drove increment 2.
Widening it would change SHIPPING bytes, so it is out of scope for a flag-off
spike; it is where the next chunk of this reach converts into bytes.
Call/CallIndirectpseudo-ops (11 declines) need the allocator to runafter their expansion, or the expansion's register footprint modeled.
🤖 Generated with Claude Code
https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L