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. |