PV2 syrupgenerates optimized EVM bytecode to transform the source into the target stack

Synthesizer of Super-optimized smart contracts

Application domain/field

Type of tool

Optimizer? Synthesis tool?

Expected input

Stack Functional Specification (SFS). This describes the source and target stack of the Ethereum Virtual Machine (EVM).

Format:

.json file

Expected output

If successful, it outputs optimized EVM bytecode to transform the source into the target stack.

Internals

"Super-optimization is a technique that tries to find the best translation of a block of code by trying all possible sequences of instructions that produce the same result." In the case of smart contracts, one tries to optimize the gas usage. Gas is the fee required to successfully conduct a transaction or execute a smart contract. It supports the following Max-SMT solvers: Z3, Barcelogic and OptiMathSAT. It uses EthIR to generate control flow graphs of the analyzed contracts.

Comments

License: Apache-2.0
Smart contract Synthesis

Links

Last commit date

14 May 2020

Related papers

https://doi.org/10.1007/978-3-030-53288-8_10 (CAV '20)

Last publication date

14 July 2020

ProVerB specific

View/edit source (Markdown)



ProVerB is a part of SLEBoK. Last updated: July 2022.