perf(#846): relational ranges take gpio-thin to 494 B — and the gate that could not see it

[avrabe]

Closes the last recoverable part of #846 (artifact RQ-57-GPIO): gale's
gpio-thin driver goes 502 B → 494 B, and the two CRL/CRH masks the issue
called "recoverable in principle, but not soundly today" are now proven.

Measured, on gale's real 656 B gpio.loom.wasm

	.text	residual and r12,#0x1f
opt-out (SYNTH_SHIFT_MASK_ELIDE=0)	534 B	10
before this PR (v0.52.0 → main)	502 B	3
after	494 B	1

Baseline re-measured on current main first — 502 B, matching the issue.

494, not the issue's 498. Each mask is a 4-byte and.w and the rewritten
lsl.w rD,rN,rK is the same width as lsl.w rD,rN,ip, so two elisions are
−8 B. The issue's "498 B remaining headroom" was arithmetically inconsistent
with its own 502 − 3×4 = 490 identity — 498 is one mask, not two. 490
remains unreachable and unsound, exactly as #846 established.

What the analysis is

The two survivors are the STM32 CRL/CRH idiom sel ? p*4 : p*4−32 where
p = pin & 0xf and sel = (p < 8). The result is < 32 on both arms, but
only through the correlation between sel and the range of p*4. No
value-range domain can see it: p*4 − 32 wraps to 0xFFFFFFE0 for p = 0,
so the meet of the two arms is all of u32 and Lt32Facts correctly declines.

Rather than reach for a relational domain — or, worse, a syntactic
sel ? x : x−32 matcher, exactly the patch-accretion the north star forbids —
phase 2 makes the correlation concrete. p = pin & 0xf can only take the
16 submask values of 0xf whatever pin is; evaluate the straight-line prefix
once per value and sel and p*4 are computed together in each case, so the
impossible combination (sel = 1 with p*4 ≥ 32) is never considered. Both
arms land in [0,28] in all 16 cases.

The abstraction over-approximates the reachable value set, so "every case
< 32" implies "always < 32" — the #682 invariant, discharged by enumeration
instead of by dataflow. Unmodeled ops drop to ⊤; one seed only (a second
masked-unknown is left ⊤ rather than Cartesian-producted — documented precision
limit, not a soundness one); straight-line prefix only; calls preserve tracked
[SP,#off] slots (the AAPCS premise synth's own allocator already depends on)
but drop every register; flags trusted for exactly the instruction after the
Cmp; register shift amounts are Rm<7:0>, not Rm & 31; Movt is RMW with
no defaulted prior; R12 lives exactly one instruction. Phase 2 runs on phase
1's output so no conclusion can rest on a movw phase 1 deleted.

The surviving mask is the load-bearing one

Verified by disassembling the shipped object, not assumed. At 0xd8:
and ip, r8, #0x1f on lsl.w r8, r6, #2 with r6 = ldr.w [sp,#0x24] — a
frame-reloaded raw param. For mode ≥ 8, mode << 2 ≥ 32; eliding it is
the #682 miscompile. It stays because the reload is ⊤.

Gate potency — and a gate that was blind

Every guard was mutated and the suite confirmed red: phase 2 disabled,
& 0xff → & 31, calls preserving registers, flags surviving instructions,
unplaceable stores keeping slots, unmodeled ops keeping slots, seed width
unbounded, movt assuming a zero prior. The movt control survived the
first draft of its test — the test was blind to it, and the unknown-prior
case was added because of that.

End-to-end negative control, run rather than assumed: force-eliding the
load-bearing mask produces the pre-#682 490 B / 0 masks object — the exact
miscompile — and gpio_thin_846_differential.py reported every check
matching, both at its old 75 and at its new 285. Only
i32_shift_mask_682_differential.py went red (6 mismatches).

The reason is structural, so no input to this driver can discriminate it: for
mode ≤u 6 the amount mode*4 ≤ 24 is already < 32; for mode >u 6 the
driver's own cmp r6,#6 ; ite hi discards the shift's result. The conditions
are complementary. That is now written into the script, the CI step and the
claims ledger rather than left for a future reader to assume.

Coverage

gpio_configure ran with mode hardcoded to 0x3, leaving the whole mode
domain of the driver's largest function unexercised — and this PR changes that
function's bytes. Added a mode sweep: 75 → 285 checks, 105 → 525 trace
events. Ledger pin, CI grep and the # ci-checks: floor moved with it.

Gates

• cargo test --workspace — 2796 passed, 0 failed; all 10 frozen anchors
  unchanged (phase 2 does not fire on control_step / flight_seam /
  flight_seam_flat / oracle_001), so no refreeze
• cargo clippy --workspace --all-targets -- -D warnings — clean
• cargo fmt --check — clean
• claim_check — 43/43
• gpio_thin_846_differential.py — 285/285, 494 B
• i32_shift_mask_682_differential.py — green on both paths
• 13 new adversarial unit tests, each proven potent by mutation

FEATURE_MATRIX (and its template) said "two gpio-thin CRL/CRH sites still
need relational ranges" — now false, so the claim was updated rather than
the ledger loosened.

Refs #846.

🤖 Generated with Claude Code

https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L

[codecov]

Codecov Report

❌ Patch coverage is 87.95987% with 72 lines in your changes missing coverage. Please review.

Files with missing lines	Patch %	Lines
crates/synth-synthesis/src/liveness.rs	87.95%	72 Missing ⚠️

📢 Thoughts on this report? Let us know!