| 14 Dec 2017 |
 Grigore | Welcome to the ERC20-K public channel. Please ask any questions here. | 01:39:20 |
|  frankleeman joined the room. | 05:41:31 |
| 16 Dec 2017 |
|  malefizer joined the room. | 07:42:33 |
| malefizer | Ok got it running. How would I be able to verify mi token against the spec? | 17:01:27 |
| Grigore | malefizer: Happy to see you got it running. Did you manage to run ktest on all the tests? | 17:05:42 |
| Grigore | I mean, ktest config.xml in this folder: https://github.com/runtimeverification/erc20-semantics/tree/master/tests/imp | 17:07:17 |
| malefizer | Yes it worked | 17:29:27 |
| Grigore | Nice. Verifying your token against the ERC20-K spec is highly non-trivial, @mal | 17:30:20 |
| Grigore | Nice. Verifying your token against the ERC20-K spec is highly non-trivial, malefizer | 17:30:28 |
| Grigore | the spec tells you what needs to be verified: the 13 rules | 17:30:46 |
| Grigore | we verified some tokens in Solidity and Viper, but that was before the ERC20-K spec | 17:32:08 |
| Grigore | One thing I suggest, as a start, is to try to run all the tests at ahttps://github.com/runtimeverification/erc20-semantics/tree/master/tests/imp with your implementation and make sure you get the same results; of course, you would need to translate them to your language | 17:33:05 |
| malefizer | Hm, how do you verify if you don't have the spec? | 17:33:16 |
| Grigore | exactly, that was the problem before! we only verified 6 of the rules, which we thought at the time was all we have to prove. That's why I created the ERC20-K, to make it clear what needs to be verified. | 17:34:09 |
| Grigore | Here are our previous proofs:
https://github.com/kframework/evm-semantics/blob/master/proofs/hkg.md | 17:35:01 |
| Grigore | For example, we didn't consider the cases where you transfer to yourself | 17:35:46 |
| Grigore | We'd like to develop automated translators from the ERC20-K spec to KEVM, and this was to generate automatically all the proof obligations. | 17:37:08 |
| Grigore set their display name to Grigore. | 17:38:40 |
| Grigore set a profile picture. | 17:38:50 |
| malefizer | Ok that means I have to compile solidity use the kevm to run it and erc20 needs to translate into kevm annotation. Then somehow verification happens. But how? | 17:45:33 |
| Grigore | I would recommend you to first reproduce the proofs that KEVM comes with: https://github.com/kframework/evm-semantics
Feel free to ask questions about KEVM on the other channel (https://riot.im/app/#/room/#k:matrix.org), which is being monitored by the KEVM people.
Then, once you can reproduce those, we can discuss how to translate the ERC20-K specs to the EVM-level (we have not done that yet, so it is all new and shiny!) | 17:50:36 |
| malefizer | Thanks | 18:08:06 |
| 5 Sep 2018 |
|  ethme joined the room. | 16:13:32 |
| 25 Aug 2019 |
|  @faabler:matrix.org joined the room. | 15:48:49 |
|  Slack Integration set their display name to Slack Integration. | 15:48:50 |
| @faabler:matrix.org left the room. | 15:49:00 |
| 19 Feb 2020 |
| Grigorechanged room power levels. | 22:05:12 |
| 18 Sep 2020 |
|  @gitter_grosu:matrix.org left the room. | 16:50:17 |
| 10 Dec 2020 |
|  @gitterbot:matrix.org set their display name to Gitter Integration (legacy). | 19:13:04 |
| 19 Jan 2021 |
|  gitter-badger (The Gitter Badger) joined the room. | 17:05:18 |
