In some bytecode (e.g ERC-20, Deposit, wETH), some code segments are similar in the sense that they are the same sequences of instructions but at different addresses.
This code segments could be merged by an optimiser. To do so we just need to
identify the segments
prove (with the Dafny-EVM) that they are equivalent (for every input state, they compute the same output state, of course except for PC)
To do
In a first phase we can try to identify the equivalent code segments, and how much code could be saved by merging them.
In a later stage, build an optimiser that:
checks (with Dafny + Dafny-EVM) that two code segments are equivalent
merges them are re-arranges the code (say of the savings in code size are worth doing so).
In some bytecode (e.g ERC-20, Deposit, wETH), some code segments are similar in the sense that they are the same sequences of instructions but at different addresses.
This code segments could be merged by an optimiser. To do so we just need to
To do
In a first phase we can try to identify the equivalent code segments, and how much code could be saved by merging them.
In a later stage, build an optimiser that: