Simulations for the system instructions - Githubissues

formal-land / coq-of-python

Translate Python code to Coq code for formal verification. Applied to the reference implementation of Ethereum in Python.

MIT License

29 stars 0 forks source link

Simulations for the system instructions #21

Open clarus opened 3 months ago

clarus commented 3 months ago

Add simulations for the system instructions in https://github.com/ethereum/execution-specs/blob/master/src/ethereum/paris/vm/instructions/system.py There are many dependencies that can be axiomatized.

[ ] generic_create
[ ] create
[ ] create2
[ ] return_
[ ] generic_call
[ ] call
[ ] callcode
[ ] selfdestruct
[ ] delegatecall
[ ] staticcall
[ ] revert