VCR-VER-004: instrument independence — the ABI observable contract, a check that fails differently (#242)

[avrabe]

The finding this responds to

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 — makes the compiler emit code leaving the return value in the wrong register, and that both per-compilation validators accept it:

instrument	verdict on the mutated rewrite
validate_cfg_rewrite (the pass's acceptance oracle)	Ok
VCR-RA-003 validate_final_allocation	Consistent
execution vs wasmtime	wrong results

Two independent-looking instruments, one shared blind spot. That is #872 one level up, and it undercuts a claim this project leans on publicly: that per-compilation validation is an independent check on the code generator.

The thesis, and what it produced

Independence is not obtained by writing a second checker, only by checking a different WAY. Both existing instruments reason about liveness/dataflow equations over register names, backward, seeded from a shared table. Agreeing costs them almost nothing.

abi_contract::validate_abi_contract(orig, rewritten) differs on four axes:

1. Its obligation cannot be emptied. RETURN_CONTRACT_REGS = [R0, R1] — a constant of the AAPCS, hard-named in the module's own source. Deleting cfg_exit_observable outright would not change one line of it.
2. It is forward, so it is structurally incapable of v0.53's fail-open mode. validate_cfg_rewrite is a backward MUST-analysis whose obligation set is a variable, and ∅ is a fixpoint — an empty seed means zero obligations means vacuous green. A forward evaluation always produces exactly one value for R0 at each return. There is no seed to shrink.
3. Its evidence is a value, not a name-pair. Per side independently: a value graph (Init(r) / Def(i,k) / Phi(b,n)) compared by greatest-fixpoint bisimulation. On a deterministic term graph that is equality of the infinite unfoldings, so loops and back edges are handled coinductively — no unrolling. Init(r) is one node shared by both sides: the AAPCS parameter half of the anchor.
4. It takes nothing from the pass. The CFG is re-derived from both streams and the two must agree. The v0.50 join attempt failed precisely by letting the pass hand the checker its own seed.

Result — the mutation is caught statically

Re-running v0.53's exact mutation (committed as scripts/repro/mutations/v053_shared_exit_contract.patch, not reconstructed), on one compilation of one fixture:

OK   baseline: join colouring applies AND the ABI contract holds
OK   (1) validate_cfg_rewrite ACCEPTS the mutated rewrite
OK   (2) VCR-RA-003 validate_final_allocation reports Consistent
OK   (3) VCR-VER-004 REJECTS: result register R0 holds a different value at the return terminator (instr 81)
OK   (4) the function DECLINES to the shipping allocator — not emitted
VCR-VER-004-INDEPENDENCE ASSERTIONS=4/4

brif_outer_740::poll is the function that returned 0x1111 instead of its parameter. Assertion (1) is load-bearing: it is what makes (3) non-vacuous, because it observes that the pre-VCR-VER-004 compiler would have emitted this.

Red-first, verified: make abi_gate treat Violated as an accept, rebuild with the mutation applied, and the compiler prints whole-function colouring APPLIED (validated) and emits the miscompile again. The gate is load-bearing, not decorative.

False rejection: none

The brief's other warning (v0.50's spurious JoinValueNotAvailable{R8}) was taken seriously. Over the ARM repro corpus:

	increment 3 alone (#896)	with the gate
functions measured	617	617
graph-alloc applied	307	307
bytes (relocatable)	40822 → 40722 (−100)	40822 → 40722 (−100)
bytes (self-contained)	−120	−120

Increment 3's result to the byte — and the check is conservative enough to demand both R0 and R1 for every function and to treat NotAttempted as a decline. The only false rejections anywhere were two synthetic unit fixtures with no return terminator; those were fixed by making the fixtures well-formed functions, not by weakening the check.

Measured against the shipping allocator, not just the flag-off spike

SYNTH_ABI_CONTRACT_AUDIT=1 on reallocate_function_post_exhaust — the allocator every synth compile runs:

functions audited (--relocatable) : 617
  Holds 422 · NotAttempted 195 · Violated 0
  declines: unmodeled-op 174, indirect-call-pseudo-op 11, numeric-offset-branch 10

The observable return contract proven on ~68 % of the shipping path, zero false rejections against a known-good allocator. Held to a CI floor (zero violations + a pinned Holds count, so lost coverage is visible rather than absorbed), red-first in both directions including the vacuity case where the hook is not wired at all.

Follow-up: composed with L4 / increment 3 (#896) — calls are now modelled

Increment 3 taught the allocator to colour across calls, taking 57 of 68 call declines. This gate declined every one of them (NotAttempted { reason: "call" }), which would have taken increment 3's reach to zero — its own colours_across_a_call test was the visible symptom.

Fixed by modelling the call, not by weakening abi_gate (NotAttempted is still a decline). The AAPCS effect is reused from liveness::call_effect — the one definition the pass and validate_cfg_rewrite already share — because two divergent call models would be a fresh instance of the very blind-spot class this lane attacks.

The forward design needed no special case: each clobbered register {R0-R3, R12, LR} is rebound to a fresh node whose operands are the pre-call argument values, while R4-R11/SP flow through. So a call result is opaque and equal across the sides exactly when the same callee got the same arguments, and a value the rewrite parked in caller-saved scratch across a call is rebound to the call's own node — it can no longer bisimulate with what the original delivers at the return. Increment 3's warning ("a validator treating bl as effect-free would accept a non-identity equation across it") is discharged as a value disagreement, with no liveness reasoning. Call/CallIndirect pseudo-ops still decline.

Re-verified after the change:

• the v0.53 mutation is still REJECTED — 4/4, Violated { sink: 81, reg: R0 } (the mutation patch was regenerated against increment 3's tree; the two semantic edits are byte-identical, only context moved);
• corpus reach = increment 3's numbers exactly, 307 applied / −100 B, zero false rejections;
• shipping path: Holds 376 → 422, NotAttempted 241 → 195, Violated 0 (~61 % → ~68 %). The 62 direct-call declines are gone, not reclassified; unmodeled-op rose 159 → 174 because functions that used to stop at the call now reach an FP / i64-pair op instead. The decline moved, it did not vanish. HOLDS_FLOOR raised 340 → 400 so a floor left at the pre-call-model value cannot silently absorb losing the model again.

6 new unit gates, including the caller-saved-across-a-call recolour (VIOLATED) and renaming what feeds a call argument (VIOLATED — this is what call_effect's uses buy).

What this does NOT close — in FEATURE_MATRIX, not just in my head

• Gate only on the flag-off spike. On the default path it is an audit. 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 — the class validate_cfg_rewrite does cover when its seed is intact. Complementary, not redundant. Pinned by a unit test so it cannot drift silently.
• The op model is still shared via liveness::reg_effect. A mismodeled op remains a blind spot common to all three. This closes the shared-contract hole, not the shared-op-model hole. synth-verify's ArmSemantics::encode_op is a genuinely second model; until it is pinned against reg_effect, "three independent validators" would be an overclaim — and the honest summary says so.

No SMT, no opt-out — both deliberate

A renames-only rewrite changes no opcode and no immediate, so both sides' terms are ground applications of the same uninterpreted operators; deciding equality is congruence closure with no side conditions — exactly the structural equality the refinement already computes. A solver would cost a dependency (and the synth-verify → synth-synthesis edge runs the wrong way) to decide the same thing. An opt-out env var would be a footgun, not evidence.

Verification

cargo fmt --check / clippy --workspace --all-targets -D warnings / cargo test --workspace — all exit 0 by real exit code. Frozen anchors 10/10. claim_check 34/34. docs/status/FEATURE_MATRIX.md regenerated with the sanctioned --emit-status, never hand-edited (#805). Two CI jobs added, both set -o pipefail + non-zero-count greps (#890).

Two fail-open bugs in the new checker were found by its own red-first testing and fixed: a bl that was not a block ender was walked past as a no-op, and unclassified control flow could slip through as "straight-line with no effect".

🤖 Generated with Claude Code

https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L

[codecov]

Codecov Report

❌ Patch coverage is 90.75044% with 53 lines in your changes missing coverage. Please review.

Files with missing lines	Patch %	Lines
crates/synth-synthesis/src/abi_contract.rs	92.81%	39 Missing ⚠️
crates/synth-synthesis/src/graph_alloc.rs	58.33%	10 Missing ⚠️
crates/synth-backend/src/arm_backend.rs	33.33%	4 Missing ⚠️

📢 Thoughts on this report? Let us know!