Skip to Content.
Sympa Menu

coq-club - [Coq-Club] semantics of EVM bytecode

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] semantics of EVM bytecode


Chronological Thread 
  • From: Abhishek Anand <abhishek.anand.iitg AT gmail.com>
  • To: coq-club <coq-club AT inria.fr>
  • Subject: [Coq-Club] semantics of EVM bytecode
  • Date: Wed, 11 Sep 2024 13:08:32 -0400
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=abhishek.anand.iitg AT gmail.com; spf=Pass smtp.mailfrom=abhishek.anand.iitg AT gmail.com; spf=None smtp.helo=postmaster AT mail-wm1-f51.google.com
  • Ironport-data: A9a23:asO9taIvBEjZ/bE8FE+RE5QlxSXFcZb7ZxGr2PjKsXjdYENS1zEEn GYcCj/XOavYZmWmc4gka4mw8U9VvZLSndcwSgEd+CA2RRqmi+KVXIXDdh+Y0wC6d5CYEho/t 63yTvGacajYm1eF/k/F3oDJ9CU6j+fSLlbFILasEjhrQgN5QzsWhxtmmuoo6qZlmtHR7zml4 LsemOWBfgb9s9JIGjhMsf7b+Uo25K6aVA4w5zTSW9gb5DcyqFFOVPrzFYnpR1PkT49dGPKNR uqr5NlVKUuEl/uFIorNfofTKiXmcJaKVeS9oiY+t5yZv/R3jndaPpDXmxYrQRw/Zz2hx7idw TjW3HC6YV9B0qbkwIzxX/TEes3X0GIvFLLveBCCXcKvI0LucFXr6tRUDmIMIogF3+hbXWdI7 OYgN2VYBvyDr7reLLOTT+BtgoE8KZCuMt5G/H5nyj7dALAtRpWrr6fiv4cJmmdtwJkUTbCDP qL1ahI3BPjESxRFOlYMCJ892u6uj3/zNTxZtF29qq8+4myVxwt0uFToGIOFIILUGJwIxC50o EqYw32gBitAEeDc0GKp1l61uf7+jAb0Ddd6+LqQs6QCbEeo7mcUEVgdUUaxieKoj1a3HdNZM U0dvCQ0xZXe72SuR9j5GgK9+TuK40daVN1XHOk3rgqKz8I4/jqkO4TNdRYZAPROiSP8bWVCO vKhxrsF2RQHXHyppXOhGnO8qDqzPW0KKDZHa3JdCwQC5Nbnrcc4iRenohOP1kKqpoWdJN0y6 2niQOsCa3E7gssC1qH99lfC695pjoacVRY7v207QUr8hj6Up+eZi0iA5l3S7PIGJ4GcJrVEU L7ohODGhN0z4VqxeOBhjQnD8HxFJxpIDdEEvWNSIg==
  • Ironport-hdrordr: A9a23:L+tyj6CfOqYi4gjlHemh55DYdb4zR+YMi2TDtnoBLiC9F/bzqy nApoV56faZslYssRIb+OxoWpPwI080nKQdieIs1NyZLWzbUQWTXeVfBEjZrwEI2ReSygeQ78 hdmmFFZuHNMQ==
  • Ironport-phdr: A9a23:5PwBehQKOF2IPFAZpDnYREPSINpsopiWAWYlg6HPa5pwe6iut67vI FbYra00ygOSBcOCtKsP0rKI+4nbGkU+or+580o+OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF 95DXlI2t1uyMExSBdqsLwaK+i764jEdAAjwOhRoLerpBIHSk9631+ev8JHPfglEnjWwbL1uI BmssAnctNQajYR/JqotyxbCv2dFdflRyW50Kl2fmArx6N238JB/7Spbpugv99RHUaX0fqQ4S aJXATE7OG0r58PlqAfOQxKX6nQTTmsZnBxIAxPY7B7hRZf+rjH6tutm1yaEO8D9UK05Vi6j7 6dvTx/olTsHOjsk+2zZlsB8kKRWqw+nqhdiwYDbfZuVOeJxca3dc90URndPUNhNWCFaGIywc 5ECAvAdMepErYTwoUYFoxukBQmrAePi0iNFiWT23a07yOQhER/J3A89FN8StnTbttP1O7oPW u2y1qbH1jXDb/JN2Tf99ofIcQotruuKXb1qd8re1FMjFwLEjlWMpozoJDyV1uEXvGia6+psT /6gi2kiqwxopDWk28gjhJXTiI0P1lDE6Tt2wJwzJdCgVkJ1YdGqHIVQuiyVNIZ4TN0vTWFnt ig11rEIt5C2cDYWxZk5xxPRZOGLfpWW7x/+W+icJSt0iXZqdr6imRu//k6twfDyWMmz1VZFt CtFkt/Uu3AIyRPc98mHSuZ4/ku7xTmP0AXT5vlLIUA1iarbK4MhzaUqmpUPtkTDGzf6l1nxj K+McEUr5Oyo6+D9brr4u5CcKol5gRz9PKQ2gsGzH/g0PwwUU2WY+emwzqDv8VP6TblQjvA6j 6/Uu43EKMQfu665GBNV3Zg56xiiDjen0coXkGEbIF9DZRmJlZLmO0vUL/D9Ffq/g0qjkDNsx /3eO73uGJTNLnzanLbveLZx9ldQyAQzwNxC/Z5UBbYBIPX8Wk/1qtPUFAM2Mwuxw+r/CdV90 J0RWX6XD6OHLK/ftUWE6+EvLuWWeYMZpjXwJ+Il6vLzlXM5nEUSfait3ZsZcnC4GfFmLl2Db nX3gtcBEHwKvgogQ+zpklGNSzhTaGy0X60h/D07CYOmDZvMRo22j7yB2T20HpxSZmxcFl+MF nLoe52CW/gXcC2SONNukiQYVbi9TI8szQyiuBfgy7V7NurU5jEYtZX72ddp4O3TjAg++iBwD 8SAyG6AVHp0n2MNRz8uxq9zu019ylGZ0ah5mfNUD9JT5+kaGjs9YJXb1qlxD834ElbKec7MQ 1K7SP2nByswR5Q/2YldTVx6HoCLhBDCxCqnAPc8kbWNCNRg+6jc3mPxKsU7wnDP0qVnjlg6T eNAMGSnguh08A2FVN2BqFmQi6v/LfdU5yXK7mrWlQJm3WldWQ90C+DeWGwHI1HRppL/71/DS LmnDfImNBFAwIiMMPgCccXn2HNBQvqrI9HCeySpgW7lDByIx6iMYYmscmMU2imbCUkYnCgc+ H+HMU41ASLy63nGAmlWHEn0K1jp7fE4rXq6SkEuyATfZkdh1qG19x1TjPqVTf9V37MYtw8ur jx1GBC22NeFQ8GYqV9He6NRKcg4/E8B1W/dsFllOYe8Kql5mlMEWwF+vkeryBAuT4sdyI4lq 3QlyAc0IqWduL9YXxWf2524erjeK22ouQuqd7aTwFbVltCf5qYI7v087VTlpgCgUEQ4oT1h1 JFO3n2Q64+vbkJaWI/tUksx6xlxpq3LKig76YTO0HRwMK6y+jbc0tMtDeEhx16uZdBaeK+DE QbzFYUdCa3MYKQjkViodRIJP6Zb8qcyM4WndueJ8KGuNedk2jmhiCUP4Yxw1F6N6zspUvTBj PNni7mT2gqKUSu5jU/06Jim39AZI2hITizikHuBZsYZfKB5cIcVBH37JsS2wo87nJvxQztC8 1XlAVoa2civcB7Ublrn3AQW215ExB7v0Sa+0TFwlCkk66SF2ymbie3odBscOmNIAmBkhFHgZ 4m1k98yU02hbgxvnxygrxWfpeATtOFkIm/fTF0dNSH8L2B5Uqaz8LOEashDrpIprSp/X+G1Y FTcQbn46Uh/sWurDy5VwzY1cCuvs5PykklhiW6TG310qWLQZcB6wRq3CMX0ffdKxXJGQSB5j WOSHV2gJ5yz+t7SkZ7fs+e4XmbnV5tJcCCtw5nS/Ce84GRrB1W4kZXR0pXuGwg7yi/21J9jU yzOoFD9Y5Xk/6u/OONjOEJvARfw5tF7FYd3joYrzMtIiD5K29PMpypBzD67OM4+u+q2dHcXQ D8X39PZqBPo3kFuNDPBxo70UGmc3to0YtC7Zm0M3Sdup8tOCaqS8PlFhX4v+gv+/V+XOKIt2 GpEmp5MoDYAjuoEuRQg1HCYC7EWRwxDODD00g6P5Ja4pblWY2Cmdf6x0lB/lJavFuLnwEkUV XDnd5MlBSI14N94NQeG2Xfz65rkddqWZNQasBHSkhbcgMBaLZswkrwBgi8tagef9TU1jvU2i xBjx8TwtYKHKn5t8aH/CxhRMDGzZsIP9RniiK9fmoCd2IXlTfADUn0bGZDvS/yvCjcbs//qY h2PHDMLoXCeAbPDHAWb5RQuvzfVHpusLX3SOGgBwIAoWkyGPEIGylNxPn1yjtsjGwut3sCkb Epp+mVb+AvjshUVguNwa0ukDyGG9V/uMGtrDsDYdkYe7xketRmJd5bFtaQqQXkeptr4/WnvY iSaf1gaUz9PAxTeQQilZv70vZHB67TKWLT4daefJ+XW77QZDa/AxIrzgNQ8uW/QcJzeZD86S KRrvygLFXFhR5aGx3NWEXFRz2SVKJfF7Bakpn8u9pD5qau0HlKpvczVUvNTKYk9ok/tx/7Sa 6jIwn4+cGg9tNtExGeUmuJHjRhC1mc3LWnrSfNZ6mbMVP6CwPYJSUNLLXoibo0QqPttlghVZ ZyB042zjOUpyKVvTQ8CDA2E+Inhc8UOJyvV2ErvIkGNOfzGIDTKx5uyeqagUfhKi+4SsRSsu DGdGkulPzKZljCvWQr9eedLxDqWOhBTouTfOl5kFHTjQdT6axa6LM4/jDs4xqcxj2/LMmhUO CZ1ckdEpLmdpS1ChfA3F2tE53tjZe6K/kTRp/HfMYoTuOB3Dz5ckutb5DElzuIQ4nwdAvNyn yTWo5hlpFTn2uiDxzx7UQZf/zZGgIXY2Ccqca7d95RGRTPF5EdXtTTWW0lM/oE1TIC26MUyg pDVman+KSlP6YfR9MoYXY3PLd6fdWAmOlzvESLVCw0MSXiqM3vejgpTiqL3lDXdo54kp5zrg JdLRKVcUQl/H/kaC19lEd9EKZF+WD9ikL+Hg+YH4HO/qF/aQ8AQ7fWlHrqCRO7iLjqUl+wOf xwT3bbxNpgeLKX+0k1mL0Z/xcHERhOWUtdKrSlsKAQzpQ8elRo2Bn120EXjZAS35XYVHvPhh R86hDx1ZuE1/Svt6VM6TrIvjCQ1mUg1397ihGLJGNYeBKi1VIBSTSHzshpoWnsaawN8bAn3g kk9cTmZHvReiLxvcW0tgwjZ68MnJA==
  • Ironport-sdr: 66e1cec0_fTCQyZZ9Fo75XOv0tbVwM1C7hMIEB9TBqheSat3RTfLvvqn iZqGLohFeN0PNDhsSgsUia4q3umdQ6IUxcxcCGw==

I am looking for a Coq formalization of the operational semantics of EVM bytecode.
So far, I have found the following:

1) https://medium.com/@pirapira/ethereum-virtual-machine-for-coq-v0-0-2-d2568e068b18
This work is over 5 years old and does not cover the recent revisions to ETH.

2) https://github.com/runtimeverification/evm-semantics
This semantics seems to cover the latest revisions, however, it is defined in the K framework and I have not found a K to Coq translator.

Are there other projects in this space that either directly define the semantics in Coq or can be easily converted to Coq?

Thanks,



Archive powered by MHonArc 2.6.19+.

Top of Page