[avrabe]

VCR-TIER-001 increment 1 — the enforcing gate over RQ-59-TIERCENSUS's findings, wired into CI. 52 of the 80 Rocq-proved rules emit a pseudo-op whose multi-instruction encoder expansion the proof never sees; an atomic model of such an expansion is a silent claim that the expansion is scratch-free. That claim shipped false twice, on two register tiers (#1021 R11, #1048 operand homes) — and the wired i64_shr_599 value differential passed on the miscompiling binary, because the value tier is structurally blind to the class. This gate checks the claim itself, by execution.

Refs #242, Refs #1021, Refs #1048.

Base

Based on origin/fix/i64-shift-amt-clobber-1048 at c2bc4235 (PR #1054, OPEN at branch time) — #1054 rewrites the same expansion surfaces this gate executes, so basing off main would both conflict and gate the unfixed bytes. Merge #1054 first; this PR then lands the gate that keeps its class closed.

What landed — extend, not rebuild

1. Declared scratch contracts — expansion_scratch_contract in crates/synth-backend/src/arm_encoder.rs is the single declaration site, next to the expansions: the registers beyond {declared results} ∪ {R12} an expansion may leave modified. The census dump example serializes it (scratch_contract), replacing its per-instance declared_temps hand column — which was already stale on this base: it still declared the shifts' r5 and the bit-counts' r3 as clobberable after RQ-59-I64SHIFT (#1048): i64 shift/bit-count expansions destroyed their own operands — R12-only rewrite on both backends, operand-preservation now checker-visible #1054 deleted exactly those writes, so a regression reintroducing the thumb-2 + a32: i64 variable-shift expansions CLOBBER the shift-amount pair (in-place '& 63' mask + amt-32 into the home high register) — re-reading the amount after i64.shl/shr_u/shr_s returns a mangled value, both selectors (execution-confirmed) #1048 class would have been masked by the declaration that mirrored it. A pseudo-op with no declaration defaults to results-only — the strictest reading, the same claim the atomic model makes.
2. The canary gate — scripts/repro/expansion_canary_gate_1021.py reuses the census's unicorn/capstone runner (execute() grew an ambient override; no second runner). Every ArmOp variant the shipped rule table emits (77 instances, completeness-gated against generated.rs) is executed on both Thumb-2 and A32, real encoder bytes, all non-operand registers canaried (R11 = 0xB11B11B1, one recognizable value per register) over the census valuations incl. the non-fixed-point shift amount. Asserted per instance/backend: nothing outside {results} ∪ {contract} ∪ {R12} moved; SP restored; memory confined to the expansion's own stack red-zone (a store through a corrupted base faults on the unmapped canary address); full capstone decode; and no declared contract register goes unexercised — an over-broad contract cannot hollow the gate.
3. CI wiring — # ci-status: wired, # ci-checks: emulations >= 1200 (measured 1386 via oracle_run.py), a step in the repro-sweep-selector-oracle job. oracle_wiring_check.py and claim_check.py both green.

Potency — two reds, two tiers, re-proven on every CI run

The committed fixtures hold the real old encoders' bytes (generated in worktrees at the named commits; no byte hand-written), and the gate's default invocation requires them to red on exactly the pinned registers, both directions. Literal output:

$ python3 scripts/repro/expansion_canary_gate_1021.py --dump scripts/repro/expansion_canary_1021_red_pre1039.json
dump leg: 77 instances, 19 pseudo variants
violations: I64Clz:['r3']; I64Ctz:['r3']; I64Popcnt:['r3']; I64Shl:['r4', 'r5']; I64ShrS:['r4', 'r5']; I64ShrU:['r4', 'r5']; Popcnt:['r11']
exit=1

Reserved-global tier (encoders at 708ae34b, pre-#1039): Popcnt clobbers r11, the linear-memory base — the #1021 mechanism — on both backends.

$ python3 scripts/repro/expansion_canary_gate_1021.py --dump scripts/repro/expansion_canary_1021_red_pre1054.json
dump leg: 77 instances, 19 pseudo variants
violations: I64Clz:['r3']; I64Ctz:['r3']; I64Popcnt:['r3']; I64Shl:['r4', 'r5']; I64ShrS:['r4', 'r5']; I64ShrU:['r4', 'r5']
exit=1

Caller-operand tier (encoders at origin/main c960903e, #1039 in / #1048 out): the shifts destroy their own amount registers (r4, r5), the bit-counts the operand's home hi (r3) — and Popcnt is absent: the gate discriminates the #1039 fix rather than redding everything old.

A third negative control on the checker itself: swapping a fixture's instances for clean HEAD bytes makes the run exit 1 with POTENCY FAILED on caller-operand tier ... expected exactly ... observed NONE — the potency assertion can itself fail.

Green leg and the derived unguarded set

live leg: 77 instances, 19 pseudo variants (both backends, canaried)
live violations beyond contract: NONE
...
EXPANSION CANARY GATE: GREEN — every rule-emitted expansion is contract-clean on
both backends, and both negative-control tiers red exactly as pinned

The census's unguarded-clobber set is pinned at EMPTY — stronger than the "does not grow" its header promised (header updated to point at this gate). Census re-run on this base: 80 rules, 52 pseudo-emitting, 19 pseudo variants, r12-only net clobbers everywhere, all four headline sets NONE.

Hand-written vs derived

• The contract values are intent declarations by nature (a contract read off the bytes would rubber-stamp any clobber) — but the table is empty: no per-op hand entry exists today, every op sits on the strictest default, and the gate's unexercised-contract check bites any future over-declaration.
• Hand-pinned: the fixtures' expected violation sets (measured from the old encoders' executed bytes at fixture creation, exact-equality asserted) and the representative operand choice in the dump example (pre-existing; no derivation can pick operands).

What this gate provably cannot cover

• Register-aliasing-dependent defects: one non-aliased operand assignment per variant shape. The thumb-2 + a32: i64 variable-shift expansions CLOBBER the shift-amount pair (in-place '& 63' mask + amt-32 into the home high register) — re-reading the amount after i64.shl/shr_u/shr_s returns a mangled value, both selectors (execution-confirmed) #1048 defects were operand-position defects, which non-aliased operands catch; a clobber that only manifests when e.g. rd == rm is outside the instance table. Extending shapes over aliased assignments is a named follow-up, not silently claimed.
• CPSR/flag effects: no flag contract exists to check against (the atomic model carries no flag state); SetCond consumers read flags immediately after.
• Valuation-gated clobbers: three census input sets (masked/large/zero shift paths). A clobber triggered only outside them needs a new valuation, added in the census.
• Scope is the rule-table-emitted ARM/A32 surface — the same 52-rule surface the census measured; selector-synthesized sequences outside ArmOp expansions are the value-tier differentials' territory.

Housekeeping

• cargo fmt / clippy --workspace --all-targets -D warnings / cargo test --workspace / python3 scripts/claim_check.py claims.yaml all green locally (exit codes gated).
• Two prose ratchets (mirror_marker_files, mirror_obligation_files) initially caught my comments using the words "mirrored"/"second source of truth"; reworded rather than waived — the ceilings did not move.
• No artifacts/release-v0.60.yaml exists yet; the rivet entry for this increment is left to the coordinator's v0.60 planning file rather than creating the release file from a lane.

🤖 Generated with Claude Code

https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L

[codecov]

Codecov Report

❌ Patch coverage is 0% with 4 lines in your changes missing coverage. Please review.

Files with missing lines	Patch %	Lines
crates/synth-backend/src/arm_encoder.rs	0.00%	4 Missing ⚠️

📢 Thoughts on this report? Let us know!