Add `cancun` support - Githubissues

a16z / halmos

A symbolic testing tool for EVM smart contracts

GNU Affero General Public License v3.0

817 stars 68 forks source link

Add `cancun` support #290

Open pcaversaccio opened 6 months ago

pcaversaccio commented 6 months ago

halmos does currently not support the new EVM version cancun (example MCOPY):

↩ 0x5e 0x (error: HalmosException('Unsupported opcode 0x5e'))

In order to formally verify properties given this new EVM version, it would be useful to add support for this new version.

pcaversaccio commented 4 months ago

MCOPY got added here: https://github.com/a16z/halmos/pull/293.

karmacoma-eth commented 3 months ago

TODO:

[x] MCOPY (https://eips.ethereum.org/EIPS/eip-5656)
[ ] BLOBHASH (https://eips.ethereum.org/EIPS/eip-4844)
[ ] BLOBBASEFEE (https://eips.ethereum.org/EIPS/eip-7516)
[ ] TSTORE/TLOAD (https://eips.ethereum.org/EIPS/eip-1153)

source: https://github.com/ethereum/execution-specs/blob/master/network-upgrades/mainnet-upgrades/cancun.md

ByungHeonLEE commented 3 months ago

@karmacoma-eth working on the issue? would it be alright if I take over this task? implementing transient storage to develop TSTORE/TLOAD opcode with the existing storage code

karmacoma-eth commented 3 months ago

@ByungHeonLEE that would be great!

For TSTORE/TLOAD, the quick and dirty way to do it is to just use the existing SSTORE/SLOAD since atm everything exists in the context of a single transaction.

Longer term, we may want to support multiple transactions, in which case there will be a difference between transient and persistent storage, so it may be useful to have a transient tag on stored values.