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

Synthesizer of Super-optimized smart contracts

Application domain/field

• Smart contracts
• Blockchain
• Super-optimization
• Synthesis
• Ethereum
• Gas optimization
• Max-SMT

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