Carry Verus value-range/no-alias facts as IR premises + algebraic mid-end — feed synth's beat-LLVM specialization

[avrabe]

Part of the meld→loom→synth 0.70× (beat-LLVM) roadmap (gale benches/gust/optimization/BEAT-LLVM-0.7x.md (PR pulseengine/gale#119)). Two asks:

1. Algebraic mid-end. gale's dissolved gust_mix is algebraically clamp(ch+476,1000,2000) but synth emits the literal 256*(ch-1024)>>8 (~6 wasted instrs LLVM folds away). loom is the natural place to strength-reduce/constant-fold 256*x>>8 → x and propagate the offset before synth lowers. Biggest single instruction-count win toward parity.

2. Carry proof-carrying facts. The leapfrog past parity needs the machine-checked invariants (Verus/Rocq/Kani value-ranges, no-overflow, no-alias, bounded indices) attached to the dissolved functions as IR premises (assume-style / range / nonnull / noalias annotations), derived from the specs + whole-composition analysis. synth consumes them to specialize (clamp-branch elision, type narrowing, check elision) — optimizations LLVM can't make because it has no proofs. This is the fact-passing contract that lets the verified pipeline beat the unverified one. See the synth + meld issues for the consuming/producing ends.

[avrabe]

Downstream payoff now quantified. gale measured the floor that this fact-carrying
contract enables (gale PR pulseengine/gale#121, gust_floor_bench, qemu -icount):
eliding gust_mix's dead clamp under a proven ch∈[524,1524] takes it from 0.825 →
0.225 ticks/call = 0.45× of native LLVM (past the 0.7× goal), bit-identical under
the bound.

The whole win gates on loom carrying the premise: gale primitives prove the range
(Verus/Rocq/Kani), but synth can only specialize if the fact survives the
component→fuse→inline pipeline as an IR premise on the relevant value. That's this
issue. The minimal contract synth needs (see synth#494): a per-value
range/no-overflow/no-alias premise that the algebraic mid-end preserves through
inline + meld fusion, so the dead clamp is provably dead at selection time. When
there's a prototype, gale will re-measure end-to-end (qemu + STM32F100 DWT) on the
same bench.