Beyond parity: proof-carrying specialization + optimal-alloc to BEAT LLVM (0.7× target)

[avrabe]

Follow-on to #428. The synth#428 levers took gale's dissolved gust_mix 2.81×→1.81× vs native LLVM. Reaching parity (~1.0×) is the remaining #428/#471 work (leaf-prologue shrink + an algebraic fold of 256*x>>8 → x, which synth currently emits literally). This issue is about beating LLVM — target 0.70× — using information LLVM structurally lacks.

(a) Proof-carrying specialization. gale primitives ship machine-checked invariants (Verus/Rocq/Kani): value ranges, no-overflow, no-alias. If synth consumes these as premises (carried in the IR by loom — see loom issue), it can specialize per-composition. Worked example: gust_mix is clamp(ch+476, 1000, 2000); a composition that proves ch ∈ [524,1524] makes both clamp branches dead → the function collapses to add r0,#476; bx lr. LLVM never emits that — it never had the bound. That single elision goes below 1.0×.

(b) Optimal register allocation for functions under a size threshold (the common case for dissolved primitives) — exact/exhaustive coloring where LLVM bails to linear-scan heuristics. The dissolve guarantees small, whole-known functions; exploit it.

The claim this enables: verified code faster than the unverified native build, because the proof is an optimization input. Full analysis + the tiered path + kill-criterion (gust_codegen_bench ratio <1.0 then ≤0.70, correctness bit-identical — elision sound only under the proven bound): gale benches/gust/optimization/BEAT-LLVM-0.7x.md (PR pulseengine/gale#119). Pairs with loom + meld issues (fact-passing contract across the pipeline).

[avrabe]

Update from the gale on-silicon gate (synth 0.16.0 adopted).

I re-dissolved gale's whole dissolved surface with v0.16.0 and confirmed it is
byte-identical to v0.15.1 on every gale artifact (not just synth's falcon frozen
gate): gust_kernel.wasm → 1282 B .text (gust_mix 40 B, gust_poll 754 B) and the
meld-fused fused.wasm → 640 B, 8 fns incl run-demo — cmp-identical, and
internally deterministic across repeat runs. 0.16 is a completeness release (the >8-param
AAPCS stack-arg path for the falcon component); it correctly does not move gale's
≤8-param kernels. Good — it means the baseline is frozen, so the next lever's effect
will be cleanly measurable on gust_codegen_bench.

So the standing number is unchanged: dissolved gust_mix 0.725 ticks/call vs native
LLVM 0.40 = 1.81×; driver-class uart-thin shows 0% from the #428 arithmetic levers
(its cost is the leaf prologue + 24 B frame + redundant stack round-trips, paid per
hot-loop call — disasm on #428).

The timely recommendation: the optimized-path / VCR-RA fixes that just landed in the
0.16 cycle — #495 (callee-saved r4–r8 AAPCS prologue), #497 (block/br_if branch
landing), #502 (decline-to-direct on R4–R8 exhaustion) — are exactly the substrate for
part (b) here (optimal alloc on small whole-known functions) and for the leaf-prologue
shrink (#471) that takes gust_mix toward parity. Please prioritize making the optimized
path selectable on the shipped --relocatable --all-exports flow (today that flow uses
the direct select_with_stack selector — confirmed against 0.16's compile --help: there
is no opt-level/optimized-path flag yet). The moment it's selectable I will measure it on
gust_mix + uart-thin + control_step on gust_codegen_bench and on real STM32F100 silicon
(DWT CYCCNT) and post the before/after here — that's the cheap parity-confirmation you can't
get without an on-silicon consumer.

Part (a) (proof-carrying clamp elision → below 1.0×) still gates on the loom fact-passing
contract (loom#240); part (b) is now unblocked-pending-CLI. Kill-criterion unchanged:
gust_codegen_bench ratio <1.0 then ≤0.70, bit-identical over [0,2047].

[avrabe]

The 0.7× floor is now measured — it's 0.45×. I built an isolated micro-bench
(gust_floor_bench, gale PR pulseengine/gale#121) that times three lowerings of
gust_mix over the same proven-range inputs under qemu -icount (deterministic,
re-run-identical):

lowering	fn-only ticks/call	ratio vs native
native (LLVM, full clamp)	0.50	1.00×
dissolved today (synth 0.15.1≡0.16.0)	0.825	1.65× (in-range; full-domain 1.81×)
proof-carrying floor (add #476)	0.225	0.45×

So part (a) isn't hypothetical: eliding the dead clamp under a proven ch∈[524,1524]
takes gust_mix to 0.45× of native LLVM — past the 0.7× target — and it's a
lowering LLVM structurally cannot reach. The bench carries a soundness gate (exit-
coded): mix_proven ≡ mix_native ≡ gust_mix over the bound, and only over the
bound — that side-condition is the contract synth would consume.

The span to capture is 0.825 → 0.225 (3.7×) on this one function. Concretely
what synth needs from the pipeline: a per-function premise (value-range / no-overflow)
attached to the IR — loom#240 is the carrier — that the selector treats as a fact to
specialize against (dead-branch elimination first, then the optimal-alloc of part (b)
on the shrunk function). When you have a prototype of either, gale will measure it on
gust_floor_bench (qemu) and on real STM32F100 silicon (DWT CYCCNT) and post
before/after. Kill-criterion holds: shipped dissolved lane <1.0 then ≤0.70, bit-
identical under the proven bound.