Where communities thrive


  • Join over 1.5M+ people
  • Join over 100K+ communities
  • Free without limits
  • Create your own community
People
Repo info
Activity
    matrixbot
    @matrixbot
    Grigore Welcome to the ERC20-K public channel. Please ask any questions here.
    matrixbot
    @matrixbot
    malefizer Ok got it running. How would I be able to verify mi token against the spec?
    Grigore malefizer: Happy to see you got it running. Did you manage to run ktest on all the tests?
    matrixbot
    @matrixbot
    Grigore I mean, ktest config.xml in this folder: https://github.com/runtimeverification/erc20-semantics/tree/master/tests/imp
    matrixbot
    @matrixbot
    malefizer Yes it worked
    Grigore Nice. Verifying your token against the ERC20-K spec is highly non-trivial, @mal
    Grigore Nice. Verifying your token against the ERC20-K spec is highly non-trivial, malefizer
    Grigore the spec tells you what needs to be verified: the 13 rules
    Grigore we verified some tokens in Solidity and Viper, but that was before the ERC20-K spec
    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
    malefizer Hm, how do you verify if you don't have the spec?
    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.
    matrixbot
    @matrixbot
    Grigore For example, we didn't consider the cases where you transfer to yourself
    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.
    matrixbot
    @matrixbot
    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?
    matrixbot
    @matrixbot
    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!)
    matrixbot
    @matrixbot
    malefizer Thanks
    snpdpy
    @snpdpy
    Hey, Is it possible to get a test ERC20 on the kovan testnet? faucet? thanks