coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: mukesh tiwari <mukeshtiwari.iiitm AT gmail.com>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] semantics of EVM bytecode
- Date: Wed, 11 Sep 2024 18:24:15 +0100
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=mukeshtiwari.iiitm AT gmail.com; spf=Pass smtp.mailfrom=mukeshtiwari.iiitm AT gmail.com; spf=None smtp.helo=postmaster AT mail-wr1-f42.google.com
- Ironport-data: A9a23:P3v/XavpD24WWfMmVkI9WFuZLefnVJVfMUV32f8akzHdYApBsoF/q tZmKWCCaPrcazT2f413PYy08ExSv8fTmt83SVRtqn8wHngVgMeUXt7xwmXYb3rDdJWbJK5Ex 5xDMYeYdJhcolv0/ErF3m3J9CEkvU2wbuOgTrSCYEidfCc8IA85kxVvhuUltYBhhNm9Emult Mj7yyHlEAbNNwVcbCRNs8pvlDs15K6u4GJB5wRkDRx2lAa2e0c9XMp3yZ6ZdCOQrrl8RoaSW +vFxbelyWLVlz9F5gSNz94X2mVTKlLjFVDmZkh+A8BOsTAezsAG6ZvXAdJHAathZ5plqPgqo DlFncTYpQ7EpcQgksxFO/VTO3kW0aGrZNYriJVw2CCe5xSuTpfi/xlhJE0uANID9uptOFt13 6w3FxkPZVetocvjldpXSsE07igiBMziPYdapWs5iD+FV7ApRpfMR6iM7thdtNsyrpoWTLCOO oxDM2MpME6ojx5nYj/7DLo7geSlnXnjciJRslPTpKs2/237wwl40byrO93QEjCPbZwFxBjG+ DOerwwVBDkxDIWywDGo1kuch9/KtDj6W5tLSpKno6sCbFq7gzZ75ActfVC8uLyyjlO0c8lOL lQdvCsot6k7skKxJuQRRDW9qX+A+wEGAp9eT7d85waKxa7ZpQ2eAwDoUwJ8VTDvj+duLRRC6 7NDt4qB6ZFH6dV5lVr1GnaoQTKO1ew9KGYDYWobV1JA7YW55o40iR3LQ5BoF6vdYhgZ393v6 2jikcT8r+x7YQ03O2GT8lXOgjbqrZ/MJuLwzhuCRXqrt2uVe6b8D7FFKjHnATJoI4OQT13Ht 38B8yRbACbiErnV/BGwrC4x8H1FKhpL3PAwQbKiInX5ywmQxg==
- Ironport-hdrordr: A9a23:s5So7qoHuXUjcbQYY9fer10aV5oceYIsimQD101hICG9E/bo9f xG+c5w6faaskd3ZJhNo6HiBEDEewKlyXcK2/hrAV7SZniChILAFugLhuvfKn/bakvDH4ZmtJ uIGJIObOEYY2IK9PoSIzPVLz/j+rS6GWyT6ts2t00dNz2CopsP0ztE
- Ironport-phdr: A9a23:YhFWkx1YwnLFiPfcsmDOrg0yDhhOgF0UFjAc5pdvsb9SaKPrp82kY BeHo6wy1RSQBdWTwskHotSVmpijY1BI2YyGvnEGfc4EfD4+ouJSoTYdBtWYA1bwNv/gYn9yN s1DUFh44yPzahANS47xaFLIv3K98yMZFAnhOgppPOT1HZPZg9iq2+yo9JDebRlEiCCgbb5wM Rm6ohjdutUVjIB/Nqs/1xzFr2dHdOhR2W5mP1WfkQri6Myt5pBj6SNQu/wg985ET6r3erkzQ KJbAjo7LW07/dXnuhbfQwSB4HscSXgWnQFTAwfZ9hH6X4z+vTX8u+FgxSSVJ8z2TbQzWTS/8 6dmTQLjhSkbOzIl9mzcl8p9h79Zrh28vRxy247ab52aO/RjcK3dc80USmhCUMhWTCFOGJ+wb 44VAuoBIepUsY/wrEYOoxukAgmsAfviyjpVhn/1w6I6yOQhGhza3AwhEdMBqm7UrNToP6oVV OC10arIwivYb/NWxTf96YbJfQo7ofGNR75wcMvRyUgzFwPAlViQponlMCmU1uQJqWSU8+1gV ee2hmMhtgp+rSShyN02hYnVmoIa1ErE9SNhzYg6JdO1SUB1bcOnHZZOtCyXKoV7T8IsTWxou Ss216EKt5C7ciQW1pgqxQPSZvibfoWV4R/vSeacLDd7iX54er+ygQu5/0anyu35TMa00VBKo zJektnUrHAN1hrT6seZRftn5EuuxTGP1wXL5uFLIEA0iarbK4M6zbIqipUTtkHDEjfzmErok aCWd1gk+u2y5+v7ZbXmo4eQOJNzigHkNKQhhMi/AeAiPgcQQmeb5OKx36Dg803hWLhGkOE6n 63DvJ3ZJckXvLC1DxFI3oo55BuzES+q3MkWkHQFNl5Idx2Kg5L0N1zPIf30F+qzjlWynDpt2 vvLILnhAojWLnjfjrjhZ6tz609dyQUt1d1T+5RZAawbLv3pQE/+rtnYAwc5MwOqx+bnD81w1 oYEVmKOBq+VKa3TsUWV6u42LemBa5EZtCzyK/gi4P7ugns5lkEHcaa12psXbWi0HvVgI0qHf XrhmskNHXsOswYkT+HniEeOXSBNa3qvRa4x6S83BJqjDYjZR4CthLKB3D28Hp1Tfm1GD02ME XT2eIWfW/cMdCOSI8F7nTweVLitUY4h1RCvtA/mzrpqNeXU+igCupLi0Nh5/fHclRY39TBsC cSSyHmCT3tokWMQWz82wKd/rFRgxluby6h3n+RYFcBP5/NOSgo1KZncz/VjB9/uXgLBY8yGR U29QtSmBDExVsg+z8UPY0Z7AdWijwrM0zCkA78PxPS3A8k/9buZ1HzsLe58zWzH3e8vlQoIW MxKYGi7haNk90DPBpHAiUTRw6O3dqkH3DLM626ZzCyPvUBEVSZ/VKzEWTYUYU6A/oex3V/LU 7L7UedvCQBG08PXcsOiC/XshFRCHrL4PcjGJni2kCG2DAqJwbWFaMzrfX8c1WPTEhtMiBgdq FCBMwV2HSK9uyTGFjU7EE/sbljs7ehhoWm6CE41zh2PR0Jk3ruxvBUSgK/UUOsdi4oNozxps DBoBBC41tPSBcCHol9kYaZRetMh4UhOz2Oftg18IpmIIKVrh1pYeANy7Av1zxsiLIJGnIAxq W8yigp/LaXNyFRaazaRxoz9IJXSI2j2uQ+1MuvYhguY39GR9aMCrv8/rj0PpSmPEUwvuzVi2 thRiT6H44nSSRAVWtT3W1o28B5zo/fbZDM87sXazy8kN678qTLE198zYYltgh+9Y9dSNr+FH w7uAoUbAcapMukjh1muaFoNIulT8Kc+O87ueeGB3eanO+NpnTTuimoigsg111+P+jF8Vu/X1 owEhfCZ3xeCfzj5hVal9MvwnMEMZD0fGHa+1TmxHJRYNcgQNc4ADWajJdHyx80r3ca8HS4Fs gT5XhVagpzMG1LadVH20AxO2F5CpHWmnXH91Dloi3QzqaHZ2iXSwuPkfR5BO2hRRWAkg02/R Or8x90cQkWsaBAk0RW/4kOvja1Gp6lkL3XSXk5Sfm73LmB+V4O/s7ODZ4hE75Zi4kA1GKysJ EuXTLLwuU5Q1j7gEnBe2DEkfiur/JT4ngB/oG2YJXd36nHefIsjoHWXrMyZTvlX0D0cQSB+g jSCHVmwMe6i+tCMnovCuOSzP464fqVaajKjjYaJtS/hoHZvHQX6hfe43NvuDQk91yb/kdhsT yTB6hjmMMHn0KGzMOQveUcNZhe07td5F5p+joovjYsRn3kbh4mQ1XUCmGb3d95c3OryYWEMS jgC39POqFK9iQszczTTndu/Ci/Vy9AEBZHyem4M3yMh881GQLyZ6rBJh2o9o1a1qx7Qfekom z4czfU073tJy+oNuQcr0mCcGuVIRRgebXGqzU7RqYzk/8A1LC61fLO91VRzh4WkBbCG+ERHX WrhP40lFml259l+N1TF1Dvy7JvlcZ/ed4F21FXcnhHeguxSMJ90mOANgH8tPH/+sGYl1+8kh AZvm5C7vZSCA2po9aO9RBVfM3emAqFbsiGolqtYksuMisqqA5ZsATUXXYThV/PuETMTqfHPO AOHETl6oXCeU+m6f0fX+AJtqHTBFIquPnecKSwCzNlscxKaIVRWnAEeWDhp1o58DA2hw9btN Vto/j1ErECtsQNCk6g7Unu3GneavgqjbS04DYSSPAYDpB8X/F/baISf9r4hRHwep8z56lbRd SrDIF4URWARBh7aWxa5ZeLovIeYtbDfX7vbTbOGYK3S+7IAEa7Qn9T3lNMhpW7EN93TbCc8S adniwwTBTYhXJ6B0zQXF35IzWSUM4jC9U36omou/qXduLzqQF69utfJUuEPd40po1fv3++CL 7LC3X4pb28HidVcgyePkuFX3UZO2XgxLH/0QOhG7WiVC/uO/80fRx8DN3EpbJoOv/96h1Mdf 5ac04y916Yk3KRsVREYBRq4y5vvPYtTcim8LA+VXh/Vcu7ddHuQmYevJvrtLN8YxPNdsxn60 dqCO2nkODnL1zzgVhT1dPpJkDneJhtV/oe0bhdqD2HnCtPgcByydtFt33UwxvUvi3XGOHR5U 3A0el5RrrCW8SJTg+luU21H4H1/KOCYmiGfp+DGI5cSuPFvD2x6jeVfqHg9zrJU6mlDSpkX0 GPKqcVypli9juSV4j9uUR4LtSwSwYzX5wNtPqLW8pQGUnHBvVoM4WiWFxUWto5lB9no6MUyg pDEkKP+LisH8sqBp5NNQZiJbpjdaTx9a0mMenacFgYOQD+1OHuKgkVclKvX7XiJtt0grZOqn pMSS7hdXVhzF/UAC00jEsZRRfU/Fj4ij7Ofi9YFoHSkqxyEDsBHvZ3cVu6THvz1KXCYjLhYY jMHxLr5KcIYMYixiCkAIhFq2Z/HHUbdR4UHuip6cgo9u1lA6lB7R2w3nl3/M0ajvCVVGvmzk Ro7zAB5ZK5+kVWkq0dyLV3MqiwqlUA3ktiwmjGdfgn6K6KoVJ1XAS7536DeGpz+SgdxKwa1m B49XN8hb71UhrpkM2tsjV2E0XOuMftVTKkBfwVJgP/LPbMn1lNTrijhzkhCt7OtNA==
- Ironport-sdr: 66e1d256_mNXsWUMYh/HsTQQkzb76+tUHll7cVtxfKeSZA6S+NgPxJoy Gz81SfL9/Q7noBY4feCe2av4SnUj0sosL/r4KFg==
Hi Abhishek,
Another one [1] and the related Coq formalisation [2].
Best,
Mukesh
[1] https://link.springer.com/chapter/10.1007/978-3-031-37709-9_9#Sec3
On 11 Sep 2024, at 18:08, Abhishek Anand <abhishek.anand.iitg AT gmail.com> wrote: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.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,-- Abhishekhttp://www.cs.cornell.edu/~aa755/
- [Coq-Club] semantics of EVM bytecode, Abhishek Anand, 09/11/2024
- Re: [Coq-Club] semantics of EVM bytecode, mukesh tiwari, 09/11/2024
Archive powered by MHonArc 2.6.19+.