Zeppelin and Vyper on IMap

[denisadiaconescu]

No description provided.

[denisadiaconescu]

The spec for transferFrom-success-1 on zeppelin is failing without the lemma rule hash2(K1,V1) =/=Int hash2(K2,V2) => K1 =/=Int K2 orBool V1 =/=Int V2. Later, when we have more time, we can investigate further if the lemma can be dropped by adding further requirements in the spec.

[daejunpark]

which text editor are you using? no EOL doesn't look good.

[anvacaru]

VS Code. I am not sure why there is no EOL

[daejunpark]

first, you should use this KEVM version:
https://github.com/kframework/evm-semantics/commits/e2492651b03e8d7b0b0789592ad7bac96a72ef5b

forget about keq branches from now on. it's the temporary version available when you started this work. now you should use the above KEVM version. please make sure the current spec works with the version. also, if you made any changes to the KEVM for this spec, let me know.

[daejunpark]

second, you should not change this global .build directory, which affects all other specs. you should create a new .build directory to which zeppelin and vyper Makefiles refer.

[dwightguth]

I'm not remotely comfortable with the fact that you are recommending people use a several months old commit of evm that happens to also contain changes that were never upstreamed. This is a huge antipattern that is going to bite us in the foot at some point. At the next planning meeting I would like us to discuss a plan to transition all the verification work to the master branches of k and evm. It can wait until we finish the current deadline if necessary but we should NOT start verifying any new contracts until this is done.