halmos icon indicating copy to clipboard operation
halmos copied to clipboard

Published 20 hours ago • verified publisher icon a16z

Add `cancun` support

Open pcaversaccio opened this issue 1 year ago • 4 comments

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 avatar May 17 '24 13:05 pcaversaccio

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

pcaversaccio avatar Jun 26 '24 09:06 pcaversaccio

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)
  • [x] TSTORE/TLOAD (https://eips.ethereum.org/EIPS/eip-1153) #463

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

0xkarmacoma avatar Jul 24 '24 17:07 0xkarmacoma

@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

ByungHeonLEE avatar Jul 25 '24 07:07 ByungHeonLEE

@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.

0xkarmacoma avatar Jul 25 '24 16:07 0xkarmacoma