Grigoremalefizer: Happy to see you got it running. Did you manage to run
kteston all the tests?
ktest config.xmlin this folder: https://github.com/runtimeverification/erc20-semantics/tree/master/tests/imp
GrigoreNice. Verifying your token against the ERC20-K spec is highly non-trivial, @mal
GrigoreNice. Verifying your token against the ERC20-K spec is highly non-trivial, malefizer
Grigorethe spec tells you what needs to be verified: the 13 rules
Grigorewe verified some tokens in Solidity and Viper, but that was before the ERC20-K spec
GrigoreOne 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
malefizerHm, how do you verify if you don't have the spec?
Grigoreexactly, 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.
GrigoreHere are our previous proofs:
GrigoreFor example, we didn't consider the cases where you transfer to yourself
GrigoreWe'd like to develop automated translators from the ERC20-K spec to KEVM, and this was to generate automatically all the proof obligations.
GrigoreI would recommend you to first reproduce the proofs that KEVM comes with: https://github.com/kframework/evm-semantics