fix(#923): ArmSemantics silently no-oped 87 of 222 ArmOps — the verifier passed a lowering that is wrong on silicon

[avrabe]

Lane 9 of the v0.57 hub, artifact RQ-57-ARMSEM, issue #923 step 2 ("write the tests the split says are real"). The brief pointed at crates/synth-verify/src/arm_semantics.rs — measured in v0.56 at 47.4 % line coverage, the largest genuine coverage gap in the repo — and said: if you find the MODEL is wrong rather than merely untested, that outranks all the coverage work.

It was wrong. In both directions.

The finding

ArmSemantics::encode_op's _ => {} default arm left the state UNCHANGED for any op it had no arm for — 87 of ArmOp's 222 variants.

The clearest instance is a shipped rule, not a hypothetical. sel_dsl::generated::rule_i32_rotl is default-on and Rocq-proved (VcrSelRules.rule_i32_rotl_correct, Qed), and it emits exactly:

RSB rs, rm, #32
ROR rd, rn, rs

Both of those instructions were in the dropped 87. The Rocq proof was never in question; the SMT model simply executed neither instruction, so its opinion of this rule was worth nothing in either direction — it could not have caught a wrong rotl, and it did reject the right one.

The same silent default is a false-ACCEPT channel, which is the direction that matters: a lowering that computes the right value and then destroys it is invisible to the value VC. Measured on v0.57 main, through the public API synth verify itself uses (TranslationValidator::verify_rule → verify_equivalence):

i32.add  →  ADD r0,r0,r1 ; UXTB r0,r0        =>  Verified

That sequence returns (x + y) & 0xFF on silicon. Graded honestly: latent, not a live miscompile — the CLI's own rule table uses only 8 ops (Add/Sub/Mul/And/Orr/Eor/Cmp/SetCond), all modeled, and declines shift rules explicitly. It is reachable through the public API and through any future rule, which is exactly how #682 got in.

The sharper half, and why this is a defect in shipped code rather than a gap: the trap path had already noticed the hazard. exec_trap_subset_op's doc says encode_op's silent default "must never green-wash a trap derivation". But its defence was a hand-maintained allowlist mirroring encode_op's match arms, and the mirror had drifted — Rsb (that same rotl instruction), I32TruncF32S and I32TruncF32U were all allowlisted to DELEGATE to a model that does not implement them. The guard was inert for exactly those three.

And the false-ALARM side explains a comment the repo has been living with: the shipped i32.shl lowering AND r1,#31 ; LSL r0,r0,r1 came back Invalid. That is the real reason the CLI rule table declines every shift rule, under a comment blaming "a different ARM op encoding."

The fix

1. One source of truth, not two. The default arm now RECORDS the first unmodeled op in ArmState::unmodeled instead of ignoring it. The modeled set stays defined solely by encode_op's match arms, so it cannot rot. The value VC turns a set field into UnsupportedOperation; exec_trap_subset_op re-checks it after every delegation, closing the Rsb hole generically — for future allowlist entries too.

Those are the only two non-test consumers of encode_op (verified by grep): translation_validator.rs's value VC and the trap subset. expansion_validator.rs has its own executor over decoded machine words and never touches encode_op; fact_spec.rs's encode_op calls are WasmSemantics, a different model.

2. Register-amount shifts modeled FAITHFULLY. ARMv7-M A7.7.68/70/12/117 give shift_n = UInt(Rm<7:0>) — the low EIGHT bits, not Rm mod 32 and not all 32. This is the #682 class. WASM's mod-32 rule belongs to the LOWERING (the selector's AND #31), never to the ARM model.

3. Modeled alongside, all shipped-selector ops: Rsb, Sxtb/Sxth/Uxtb/Uxth, I32TruncF32S/I32TruncF32U. Cmn/Movw/Movt had a DUPLICATE model inside exec_trap_subset_op; that copy is deleted and they delegate to the single one. D registers in new_symbolic were allocated 32 bits wide; they are 64-bit registers.

4. Both of this crate's ARM models now state the same shift rule. validator_pattern.rs fed the raw 32-bit Rm under a comment conflating ARM's Rm<7:0> with WASM's mod-32. That one can only false-ALARM, never false-accept (for the model to bless a lowering the amount must be in [0,31], exactly where the two coincide) — no verdict changes, confirmed by the suite. Fixed anyway: two models stating different rules for one instruction means at most one of them is evidence, and a reader cannot tell which.

Verdicts, same entry point

sequence	before	after
shipped Rocq-proved rule_i32_rotl (RSB+ROR)	Invalid	Verified
ADD;UXTB for i32.add (wrong on silicon)	Verified	Invalid + counterexample
ADD;POP (genuinely unmodeled)	Verified	Err(UnsupportedOperation), names the op
5 shipped shift/rotate lowerings	Invalid	Verified
unmasked LSL for i32.shl	Invalid	Invalid — witness Rm = 0x4000_0080

That last witness is one only the <7:0> rule can produce: Rm mod 32 = 0 (WASM: identity) but Rm<7:0> = 128 ≥ 32 (ARM: zero).

The tests

25 tests, written against ARMv7-M (DDI 0403E.b), never against the model's own output. Two disciplines:

• Independent oracle — expected values come from Rust (signed vs unsigned comparison, wrapping arithmetic, count_ones/leading_zeros/reverse_bits, IEEE-754 <). A second implementation, not a mirror.
• Discriminating vectors — chosen to SEPARATE the ARM rule from the ones it gets confused with. With Rn = 1, Rm = 0x100 gives 1 under Rm<7:0> and under mod-32 but 0 under raw-32; Rm = 0x120 gives 0 under Rm<7:0> but 1 under mod-32. Together they pin <7:0> against BOTH wrong readings.

Prioritised by consequence: register-shift masking; update_flags_sub/update_flags_add and all ten condition codes (every i32 comparison and the cmp→select lever ride on these, and CMN drives the i32.div_s INT_MIN/−1 overflow guard, so a wrong C or V there is a wrong TRAP — update_flags_add had ZERO coverage); the ordered VFP compares behind the #709/#756 trunc guards (NaN makes every ordered relation false, Ge included; ±0.0 compare equal; negatives order by decreasing magnitude); 64-bit carry/borrow and the lexicographic compares' UNSIGNED low-word tiebreak.

The rotl test calls the shipped generator rather than transcribing its output, and asserts the emitted SHAPE before the verdict — so a change to the rule reaches the assertion instead of drifting away from it.

Deliberately NOT asserted, and said so in the file header: SDIV/UDIV by zero. ARM yields 0, SMT-LIB bvsdiv/bvudiv are total and yield something else, WASM traps, and the value clause is asserted only on the non-trapping path by the trap-gated VC. Pinning either answer would turn a scoped exclusion into a false claim.

Potency, checked rather than assumed

The first 24 passed on the first run — which is exactly when to ask whether they can fail. Eight mutations of the model, each confirmed present before and absent after replacement, each turning the suite RED: raw-32 shift amount (3 tests red), CMP carry polarity (2), CMN carry polarity, MOVT clobbering the low half, F32 Ge dropping its NaN exclusion, i64.lt_s using a signed low-word tiebreak, SXTB zero-extending, and removing the #923 unmodeled-op check.

The 25th (rotl) is not covered by that sweep, and shouldn't be claimed as such: ROR by raw Rm and by Rm<7:0> agree (period 32, and 256 is a multiple of 32), so the shift mutation cannot reach it. Its red-first evidence is the measured Invalid → Verified transition above; the discriminating mutation would be deleting the Rsb arm.

Coverage

cargo llvm-cov -p synth-verify --summary-only, identical command before and after, the "after" taken on this branch's HEAD:

	lines	regions
before	1179/2481 = 47.52 %	52.55 %
after	1475/2548 = 57.89 %	62.23 %

The brief's "2481 lines, 47.4 %" reproduced exactly — 2481 is llvm-cov's coverable-line count, not wc -l (3606). Not comparable to the CI job's --workspace figure, and -p also excludes CI's separate --features z3-solver,arm run.

Residual, stated not hidden

73 ArmOp variants remain unmodeled (was 87): 41 MVE vector ops, 32 others — flag-setting/carry forms (Adds/Adc/Subs/Sbc/Mla), subword and symbol memory, branch and stack ops. All 73 now DECLINE loudly instead of passing. Three docs asserted encode_op is "a genuinely second model of the same operations"; that claim was more generous than the code, and is amended with the measured before/after in the same PR (FEATURE_MATRIX via its template; artifacts/status.json unchanged).

Gates

Run locally without a pipe: cargo test --workspace ✅ · cargo clippy --workspace --all-targets -D warnings ✅ · cargo fmt --check ✅ · claim_check 43/43 ✅. The last two commits add a test and docs; clippy/fmt/claim_check were re-run on the final tree, and CI's Test job covers the workspace run against the merge.

Based on cb80e60c. No [Unreleased] edit, no version bump, no status.json regeneration. PR only — not to be merged by this lane.

🤖 Generated with Claude Code

https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L

[codecov]

Codecov Report

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

Files with missing lines	Patch %	Lines
crates/synth-verify/src/arm_semantics.rs	95.45%	4 Missing ⚠️

📢 Thoughts on this report? Let us know!