research(gust): the 0.7× roadmap — meld/loom/synth beating LLVM#119
Open
avrabe wants to merge 1 commit into
Open
research(gust): the 0.7× roadmap — meld/loom/synth beating LLVM#119avrabe wants to merge 1 commit into
avrabe wants to merge 1 commit into
Conversation
… just match it
Sets the bar at dissolved/native = 0.70x (30% faster than native LLVM), the
wasm-LTO leapfrog thesis as a measurable goal. Grounded in the gust_mix disasm
(synth 0.15.0, 1.81x today):
- gust_mix is algebraically clamp(ch+476, 1000, 2000); synth emits the literal
256*x>>8 (never folds to x), a 6-reg leaf prologue, and a redundant uxth.
- Tier 1 (-> ~1.0x parity): algebraic mid-end fold + optimal leaf prologue
(synth#428/#471) + branchless clamp. "Do what LLVM does."
- Tier 2 (-> 0.7x, BEAT LLVM): use what LLVM structurally lacks —
(a) PROOF-CARRYING FACTS: loom carries Verus value-ranges/no-alias as IR
premises; synth specializes per-composition (e.g. a proven ch range makes
BOTH clamp branches dead -> gust_mix collapses to `add #476`, which LLVM
will never emit because it never had the proof);
(b) OPTIMAL regalloc on tiny whole-known functions where LLVM bails to heuristics;
(c) whole-program specialization after meld fusion (cross-TU value flow LLVM
can't see).
The claim: verified code FASTER than the unverified native build, because the
proof is an optimization input. Kill-criterion: gust_codegen_bench ratio < 1.0
then <= 0.70, correctness bit-identical (clamp elision sound only under the bound).
Filed to synth/loom/meld.
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
This was referenced Jun 25, 2026
Codecov Report✅ All modified and coverable lines are covered by tests. 📢 Thoughts on this report? Let us know! |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Sets the bar at 0.70× (dissolved 30% faster than native LLVM) — the leapfrog thesis as a measurable goal — grounded in the gust_mix disasm.
Tier 1 (→1.0× parity): algebraic fold (
256*x>>8 → x), optimal leaf prologue (synth#428/#471), branchless clamp.Tier 2 (→0.7×, beat LLVM): what LLVM can't have — proof-carrying facts (loom carries Verus ranges → synth elides clamp branches per-composition; a proven
chrange collapses gust_mix toadd #476), optimal regalloc on tiny functions, whole-program specialization after meld fusion.The claim: verified code faster than the native build because the proof is an optimization input. Filed to synth/loom/meld. Kill-criterion in-doc.
🤖 Generated with Claude Code