| 14 Dec 2017 |
| 01:13:00 |  grigore.rosu | Redacted or Malformed Event |
| 01:15:48 | |  Grigore changed the room topic to "" from "". |
| 01:17:56 | | Grigore changed the room name to "" from "". |
| 01:17:56 | | Grigore set the room topic to "Formal Executable Specification of ERC20 in K (Blog: https://runtimeverification.com/blog/?p=496 , Github: https://github.com/runtimeverification/erc20-semantics)". |
| 01:18:06 | | Room Avatar Renderer. |
| 01:19:00 | | Grigore set the room name to "ERC20-K". |
| 01:25:13 |  @gitter_grosu:matrix.org | Redacted or Malformed Event |
| 01:39:20 | Grigore | Welcome to the ERC20-K public channel. Please ask any questions here. |
| 05:41:31 | |  frankleeman joined the room. |
| 16 Dec 2017 |
| 07:42:33 | |  malefizer joined the room. |
| 17:01:27 | malefizer | Ok got it running. How would I be able to verify mi token against the spec? |
| 17:05:42 | Grigore | malefizer: Happy to see you got it running. Did you manage to run ktest on all the tests? |
| 17:07:17 | Grigore | I mean, ktest config.xml in this folder: https://github.com/runtimeverification/erc20-semantics/tree/master/tests/imp |
| 17:29:27 | malefizer | Yes it worked |
| 17:30:20 | Grigore | Nice. Verifying your token against the ERC20-K spec is highly non-trivial, @mal |
| 17:30:28 | Grigore | Nice. Verifying your token against the ERC20-K spec is highly non-trivial, malefizer |
| 17:30:46 | Grigore | the spec tells you what needs to be verified: the 13 rules |
| 17:32:08 | Grigore | we verified some tokens in Solidity and Viper, but that was before the ERC20-K spec |
| 17:33:05 | 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:16 | malefizer | Hm, how do you verify if you don't have the spec? |
| 17:34:09 | 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:35:01 | Grigore | Here are our previous proofs:
https://github.com/kframework/evm-semantics/blob/master/proofs/hkg.md |
| 17:35:46 | Grigore | For example, we didn't consider the cases where you transfer to yourself |
| 17:37:08 | 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:38:40 | | Grigore set their display name to Grigore. |
| 17:38:50 | | Grigore set a profile picture. |
| 17:45:33 | 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:50:36 | 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!) |
| 18:08:06 | malefizer | Thanks |
| 5 Sep 2018 |
| 16:13:32 | |  ethme joined the room. |
