Synthesis-Powered Optimization of Smart Contracts via Data Type Refactoring
summary
Tool called Solidare uses a small DSL plus optimal program synthesis (sketch generation, sketch completion, equivalence checking) and a static gas-cost proxy to refactor Solidity data types into new layouts. On benchmarks from Etherscan and GasStation it synthesizes functionally equivalent contracts in a median time under 1s (avg 21s), improves 18/20 Etherscan cases (avg ~60% gas saved) and 6/10 GasStation cases (up to ~10% reported), and typically rewrites about 53 lines changed across benchmarks.
AI-written summary · about
chapters (22)
- 0:00Smart contract optimization intro
- 1:23Gas efficiency in smart contracts
- 2:27Data layout for gas savings
- 3:29Synthesis-powered type refactoring
- 4:54Program synthesis challenges
- 5:59Tool overview and inputs
- 7:04Data type transformation example
- 8:31Type propagation in variables
- 9:12Code synthesis sketch generation
- 12:45Statement-level sketch details
- 13:28Sketch completion for gas optimality
- 14:32Synthesis constraint encoding
- 15:35Minimal failing subcontract
- 17:00Evaluation setup and benchmarks
- 18:03Code generation efficiency results
- 19:30Gas savings with Solitaire
- 20:52Code modification effort
- 21:56Conclusion and tool features
- 22:43Q&A
- 23:03Encoding expressions in synthesis
- 24:30Incentives for contract optimization
- 26:19Adapting to gas cost changes
related talks
21mSolType: Refinement Types for Arithmetic Overflow in Solidity
26mSolType: Refinement Types for Arithmetic Overflow in Solidity
25msolx: an LLVM-based Solidity toolchain
18mAsparagus: Automated Synthesis of Parametric Gas Upper-Bounds for Smart Contrac...
16mTips and Tricks to Deploy L1 Smart Contracts on Optimism
25mBehavioral simulation for smart contracts
38mIntroducing Core Solidity
21mScaffold-Eth, OpenZeppelin, and EVM Optimization