SuperStack: Superoptimization of Stack-Bytecode via Greedy, Constraint-Based, and SAT(…)
summary
SuperStack implements a stack-bytecode superoptimizer that combines a greedy bound-refinement that cuts search bounds (example reduced 13→10), a MaxSAT-based encoding for weighted objectives, and domain-specific dominance constraints. The tool targets WebAssembly and EVM, evaluates on >500,000 extracted sequences, and reports 4–6× faster search with 2–3× more instruction/gas savings than prior superoptimizers, and often reduces optimization time to one quarter while producing verified equivalent, smaller sequences.
AI-written summary · about
chapters (9)
- 0:00SuperStack optimizer intro
- 1:03Stack optimization example
- 3:09Super optimization framework
- 5:56Stack operations overview
- 6:16Extracting optimization sequences
- 7:18Greedy algorithm for bounds
- 8:42SAT encoding for search
- 11:09Experimental results
- 14:41Future work and conclusion
related talks
23mSynthesizing Efficient Super-Instruction Sets for Ethereum Virtual Machine
14mDataflow-Based Pruning for Speeding up Superoptimization
15mLightweight On-Stack Replacement in Languages with Unstructured Loops
47mHow an Optimizing Compiler Works
19mMinotaur: A SIMD-Oriented Synthesizing Superoptimizer
30mHow to solve stack too deep errors: a Yul to EVM pipeline
41mConcatenative programming and stack-based languages
39mAsk Me Anything with Alex Aiken