8 Members
Formal Executable Specification of ERC20 in K (Blog: https://runtimeverification.com/blog/?p=496 , Github: https://github.com/runtimeverification/erc20-semantics)1 Servers

Load older messages

Timestamp Message
14 Dec 2017
01:13:00@_slack_runtimeverification_U5FNFKKC5:matrix.orggrigore.rosuRedacted or Malformed Event
01:15:48@Grigore:matrix.orgGrigore changed the room topic to "" from "".
01:17:56@Grigore:matrix.orgGrigore changed the room name to "" from "".
01:17:56@Grigore:matrix.orgGrigore 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:06Room Avatar Renderer.
01:19:00@Grigore:matrix.orgGrigore set the room name to "ERC20-K".
01:25:13@gitter_grosu:matrix.org@gitter_grosu:matrix.orgRedacted or Malformed Event
01:39:20@Grigore:matrix.orgGrigoreWelcome to the ERC20-K public channel. Please ask any questions here.
05:41:31@frankleeman:matrix.orgfrankleeman joined the room.
16 Dec 2017
07:42:33@malefizer:matrix.orgmalefizer joined the room.
17:01:27@malefizer:matrix.orgmalefizerOk got it running. How would I be able to verify mi token against the spec?
17:05:42@Grigore:matrix.orgGrigore malefizer: Happy to see you got it running. Did you manage to run ktest on all the tests?
17:07:17@Grigore:matrix.orgGrigore I mean, ktest config.xml in this folder: https://github.com/runtimeverification/erc20-semantics/tree/master/tests/imp
17:29:27@malefizer:matrix.orgmalefizerYes it worked
17:30:20@Grigore:matrix.orgGrigoreNice. Verifying your token against the ERC20-K spec is highly non-trivial, @mal
17:30:28@Grigore:matrix.orgGrigore Nice. Verifying your token against the ERC20-K spec is highly non-trivial, malefizer
17:30:46@Grigore:matrix.orgGrigorethe spec tells you what needs to be verified: the 13 rules
17:32:08@Grigore:matrix.orgGrigorewe verified some tokens in Solidity and Viper, but that was before the ERC20-K spec
17:33:05@Grigore:matrix.orgGrigoreOne 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:matrix.orgmalefizer Hm, how do you verify if you don't have the spec?
17:34:09@Grigore:matrix.orgGrigoreexactly, 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:matrix.orgGrigoreHere are our previous proofs: https://github.com/kframework/evm-semantics/blob/master/proofs/hkg.md
17:35:46@Grigore:matrix.orgGrigoreFor example, we didn't consider the cases where you transfer to yourself
17:37:08@Grigore:matrix.orgGrigoreWe'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:matrix.orgGrigore set their display name to Grigore.
17:38:50@Grigore:matrix.orgGrigore set a profile picture.
17:45:33@malefizer:matrix.orgmalefizerOk 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:matrix.orgGrigoreI 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!)
5 Sep 2018
16:13:32@ethme:matrix.orgethme joined the room.

There are no newer messages yet.

Back to Room List