RT Conference Proceedings
T1 Synthesis of Super-Optimized Smart Contracts Using Max-SMT
A1 Albert Albiol, Elvira María
A1 Gordillo Alguacil, Pablo
A1 Rubio, Albert
A1 Schett, Maria A.
AB With the advent of smart contracts that execute on the blockchain ecosystem, a new mode of reasoning is required for developers that must pay meticulous attention to the gas spent by their smart contracts, as well as for optimization tools that must be capable of effectively reducing the gas required by the smart contracts. Super-optimization is a technique which attempts to find the best translation of a block of code by trying all possible sequences of instructions that produce the same result. This paper presents a novel approach for super-optimization of smart contracts based on Max-SMT which is split into two main phases: (i) the extraction of a stack functional specification from the basic blocks of the smart contract, which is simplified using rules that capture the semantics of the arithmetic, bit-wise, relational operations, etc. (ii) the synthesis of optimized blocks which, by means of an efficient Max-SMT encoding, finds the bytecode blocks with minimal gas cost whose stack functional specification is equal (modulo commutativity) to the extracted one. Our experimental results are very promising: we are able to optimize 55.41 % of the blocks, and prove that 34.28 % were already optimal, for more than 61 000 blocks from the most called 2500 Ethereum contracts.
SN 9783030532871
SN 9783030532888
SN 0302-9743
SN 1611-3349
YR 2020
FD 2020-07-14
LK https://hdl.handle.net/20.500.14352/96459
UL https://hdl.handle.net/20.500.14352/96459
LA eng
DS Docta Complutense
RD 6 abr 2025