The K Framework User Group

110 Members
The K Framework (kframework.org) and its applications to smart contracts.  EVM: github.com/kframework/evm-semantics Viper: github.com/kframework/viper-semantics3 Servers

Load older messages

Timestamp Message
3 Dec 2018
11:48:14@_slack_runtimeverification_UDUFMGVPZ:matrix.orgryuya.nakamura I’m not sure but kprove seems to use the cache (of unification?). How can I make kprove avoid to use the cache? My team is using K in several computers and sometimes they show different results with the same bytecode and specs and I thought it’s because of the cache mechanism.
12:03:40@_slack_runtimeverification_UDUFMGVPZ:matrix.orgryuya.nakamura I thought the cache is included in somewhere at .build/k so I removed it (and .build/evm-semantics as well) and then tried kprove again but nothing changed.
12:16:54@_slack_runtimeverification_U7XNEMJHL:matrix.orgdenis.bogdanas Different results could be due to (1) functional rule non-determinism - several rules can apply for a specific term and resultis different depending which rule apply. Or (2) Z3 timeout. For 2d case look at the summary box at the end - the timeouts are presented there. there are otpions to increase timeout for z3 as well. 1st issue is much harder to debug, but you can do it with logging options. I doubt its due to caching. You can disable it with --cache-func false. Also disable cache-tostring if you wish. Look at kprove --help for instructions.
12:17:48@_slack_runtimeverification_U7XNEMJHL:matrix.orgdenis.bogdanas There are many sorts of caching by the way. In your next post you talk about parse cache. My message above is about function evaluation cache.
12:18:30@_slack_runtimeverification_U7XNEMJHL:matrix.orgdenis.bogdanas Latest k-gnosis also shows memory usage at each step and in summary box.
12:21:02@lev:matrix.orgequivrel ryuya.nakamura: Not sure if this is what you are experiencing, but we encountered some z3 timeout non-determinism in the past, which we are mitigating by using the flag --z3-tactic "(or-else (using-params smt :random-seed 3 :timeout 1000) (using-params smt :random-seed 2 :timeout 2000) (using-params smt :random-seed 1))"
12:22:46@lev:matrix.orgequivrelwhat does this is causes each z3 query to be attempted up to 3 times with different random seeds (1,2,3) and with increasing timeouts. we found that this covered all cases we encountered where z3 behaviour depended on the value of the seed.
12:23:36@lev:matrix.orgequivrelTo debug this I would track down the places where this is happening, and if indeed it's due to a z3 timeout then extract the full z3 query and test it separately with different seeds and timeouts to see if you can reproduce the non-determinism.
4 Dec 2018
00:31:02@_slack_runtimeverification_UDUFMGVPZ:matrix.orgryuya.nakamura 7XNEMJHL @equivrel Thank you so much. I’ll check them now. I investigated more specifically. I have been proved some specs of Vyper contract with various old K version at nrryuya/work/k/verified-vyper-contracts . I removed that repo, cloned, built and still the specs are proved. However, when I cloned the same commit at nrryuya/work/experiments/verified-vyper-contracts, all the specs failed. Also, my team tried with other two PCs and all the specs failed.
00:43:37@_slack_runtimeverification_UDUFMGVPZ:matrix.orgryuya.nakamura At first I suspected that only inside the nrryuya/work/k/verified-vyper-contracts directory the cache remains so I tried with --cache-func false and --cache-tostring false but specs are still proved.
00:44:13@_slack_runtimeverification_UDUFMGVPZ:matrix.orgryuya.nakamura One of the specs above is this https://gist.github.com/nrryuya/62ebd2b3204564a76fb96ec54535f045
15:14:20@_slack_runtimeverification_U7XNEMJHL:matrix.orgdenis.bogdanas Make sure you use the right version of KEVM. We refactored Makefile in latest commits. The required KEVM is in .kevm.rev files. Some projects use different versions of KEVM now ,they have their own .kevm.rev for that. Latest K-gnosis is good for all projects.
15:15:38@_slack_runtimeverification_U7XNEMJHL:matrix.orgdenis.bogdanas So is that a problem? Do you expect them to fail?
23:50:01@_slack_runtimeverification_UDUFMGVPZ:matrix.orgryuya.nakamura Thank you. We are using the k and kevm version written in this commit of verified-smart-contracts (https://github.com/runtimeverification/verified-smart-contracts/tree/fea6e4e8dc3192667201168dd4767574672d0b93).
23:51:43@_slack_runtimeverification_UDUFMGVPZ:matrix.orgryuya.nakamura I suspected that they should fail because in all the other environments we tried they fail and only my nrryuya/work/k/verified-vyper-contracts is wrong in some way.
23:58:28@_slack_runtimeverification_UDUFMGVPZ:matrix.orgryuya.nakamura We I stopped investigating about nrryuya/work/k/verified-vyper-contracts and as I mentioned in this issue (https://github.com/kframework/k/issues/202), we updated whole specs, lemmas with reference to the latest verified-smart-contracts (Most of the modification were to update to Constantinople) and specs get to be correctly proved in all environment.
5 Dec 2018
00:02:17@_slack_runtimeverification_UDUFMGVPZ:matrix.orgryuya.nakamura I can’t trust my nrryuya/work/k/verified-vyper-contracts so I’m using different directory. We are going to set up CI of kprove to make sure specs are proved in clean environment.
00:02:38@_slack_runtimeverification_UDUFMGVPZ:matrix.orgryuya.nakamura Anyway, thank you so much for your support.
7 Dec 2018
18:54:48@gkobeaga:matrix.orggkobeaga joined the room.
16 Dec 2018
03:09:19@_slack_runtimeverification_UDUFMGVPZ:matrix.orgryuya.nakamura Hi, I’m working on the verification of ERC721 (Non-fungible) token standard in Vyper and I’m stuck in java.lang.AssertionError error caused by contradiction in #if_#then_#else_#fi_K-EQUAL . The spec is this. https://gist.github.com/nrryuya/a5d0eff3e37ad025326b1fd8e31bf10b and the output of kprove is this.
Exception while evaluating functional term:
	#if_#then_#else_#fi_K-EQUAL(andBool(notBool_(==K(APPROVED_1424:Int,, Int(#"0"))),, ==K(APPROVED_1424:Int,, Int(#"0"))),, Int(#"4800"),, Int(#"0"))
and applying the rule
	rule #if_#then_#else_#fi_K-EQUAL(R_C_336:Bool,, R_B1_337:K,, R__10_338:K) => R_B1_337:K requires [R_C_336:Bool] ensures [Bool(#"true")] [Location: Optional[Location(751,8,751,56)], Optional[Source(/Users/nrryuya1/work/blockchain/LayerXcom/verified-vyper-contracts/k/.build/k/k-distribution/target/release/k/include/builtin/domains.k)]]

Exception message: java.lang.AssertionError

Exception while evaluating functional term:
	Rsstore(CONSTANTINOPLE_EVM(.KList),, Int(#"0"),, APPROVED_1424:Int,, APPROVED_1424:Int)
and applying the rule
	rule Rsstore(R_SCHED_802:Schedule,, R_NEW_803:Int,, R_CURR_800:Int,, R_ORIG_801:Int) => #if_#then_#else_#fi_K-EQUAL(andBool(andBool(_=/=Int__INT(R_CURR_800:Int,, R_NEW_803:Int),, ==Int(R_ORIG_801:Int,, R_CURR_800:Int)),, _==Int_(R_NEW_803:Int,, Int(#"0"))),, _  _EVM(Rsstoreclear_EVM(.KList),, R_SCHED_802:Schedule),, +Int(#if_#then_#else_#fi_K-EQUAL(_andBool_(_andBool_(_=/=Int__INT(R_CURR_800:Int,, R_NEW_803:Int),, _=/=Int__INT(R_ORIG_801:Int,, R_CURR_800:Int)),, _=/=Int__INT(R_ORIG_801:Int,, Int(#"0"))),, #if_#then_#else_#fi_K-EQUAL(_==Int_(R_CURR_800:Int,, Int(#"0")),, _-Int__INT(Int(#"0"),, _  _EVM(Rsstoreclear_EVM(.KList),, R_SCHED_802:Schedule)),, #if_#then_#else_#fi_K-EQUAL(_==Int_(R_NEW_803:Int,, Int(#"0")),,  _ _EVM(Rsstoreclear_EVM(.KList),, R_SCHED_802:Schedule),, Int(#"0"))),, Int(#"0")),, #if_#then_#else_#fi_K-EQUAL(_andBool_(_=/=Int__INT(R_CURR_800:Int,, R_NEW_803:Int),, _==Int_(R_ORIG_801:Int,, R_NEW_803:Int)),, _-Int__INT(#if_#then_#else_#fi_K-EQUAL(_==Int_(R_ORIG_801:Int,, Int(#"0")),, _  _EVM(Gsstoreset_EVM(.KList),, R_SCHED_802:Schedule),,  _ _EVM(Gsstorereset_EVM(.KList),, R_SCHED_802:Schedule)),, _  _EVM(Gsload_EVM(.KList),, R_SCHED_802:Schedule)),, Int(#"0")))) requires [ <_ >_EVM(Ghasdirtysstore_EVM(.KList),, R_SCHED_802:Schedule)] ensures [Bool(#"true")] [Location: Optional[Location(2200,10,2215,43)], Optional[Source(/Users/nrryuya1/work/blockchain/LayerXcom/verified-vyper-contracts/k/.build/evm-semantics/.build/java/evm.k)]]

Exception message: java.lang.AssertionError
(https://gist.github.com/nrryuya/cee476cf034a52748b52626f2a07418b#file-erc721-transferfrom-success-1-logs) By the number in pc cell, the corresponding Vyper code is this
    if self.idToApprovals[_tokenId] != ZERO_ADDRESS:
        # Reset approvals
        self.idToApprovals[_tokenId] = ZERO_ADDRESS
https://github.com/LayerXcom/verified-vyper-contracts/blob/master/contracts/erc721/ERC721.vy#L187 The problem in the output is here.
#if_#then_#else_#fi_K-EQUAL(_andBool_(notBool_(_==K_(APPROVED_1424:Int,, Int(#"0"))),, _==K_(APPROVED_1424:Int,, Int(#"0"))),, Int(#"4800"),, Int(#"0"))
(APPROVED is the symbol I set for self.idToApprovals[tokenId]) The above is contradictory so assertionError occurs in the in ConjunctiveFormula.java because of isFalseFromContradictions() check. https://github.com/kframework/k/blob/fad06744fd41d624e942f120517aef263686fdff/java-backend/src/main/java/org/kframework/backend/java/symbolic/ConjunctiveFormula.java#L811 My question is why K is doing such a contradictory inference? I’m not sure this is related to this but ==K_(_==K_(APPROVED_1424:Int,, Int(#"0")),, Bool(#"false")) is included in the equalities . https://gist.github.com/nrryuya/cee476cf034a52748b52626f2a07418b#file-erc721-transferfrom-success-1-logs-L305 Thank you always 🙇
K_VERSION   :=b65568ade007d54dd21667f4f56f2d7471bb6596
12:50:00@_slack_runtimeverification_U7XNEMJHL:matrix.orgdenis.bogdanas Your best chance is to run kprove in debug mode from Intellij and see what happens under the hood. When logs don't provide enough info that's the best solution. The most likely reason (thogh I need to konw the line on which AssertionError happens to be sure), is that context expects a term of sort Int, while #if... construct is of term K. It needs to evaluate to become Int. So you have to investigate why it doesn't evaluate.
13:28:30@lev:matrix.orgequivrel Or use klab :D
13:46:48@_slack_runtimeverification_UDUFMGVPZ:matrix.orgryuya.nakamura Thank you for replying. > to run kprove in debug mode from Intellij Yeah! I’m investigating with this. >(thogh I need to konw the line on which AssertionError happens to be sure K says java.lang.AssertionError at org.kframework.backend.java.symbolic.ConjunctiveFormula.implies(ConjunctiveFormula.java:848) https://gist.github.com/nrryuya/cee476cf034a52748b52626f2a07418b#file-erc721-transferfrom-success-1-logs-L366
13:49:15@_slack_runtimeverification_UDUFMGVPZ:matrix.orgryuya.nakamura Thank you! I’ve already tried klab and also attended DEVCON workshop. It is super great tool! My project (FVyper: https://github.com/LayerXcom/verified-vyper-contracts) targets Vyper contracts and thought klab doesn’t work with Vyper? If so, I’m willing to make pull-request to klab to support Vyper.
13:51:55@_slack_runtimeverification_UDUFMGVPZ:matrix.orgryuya.nakamura Also, in FVyper I’m planning to verify contracts like Plasma, state channel and need reachability in the cells which klab doesn’t support (e.g. accounts cell) so I adopted eDSL.
13:52:36@_slack_runtimeverification_U7XNEMJHL:matrix.orgdenis.bogdanas Thanks for link. I don't really know what can lead to AssertionError on that line:)
13:52:36@_slack_runtimeverification_UDUFMGVPZ:matrix.orgryuya.nakamura I might be misunderstanding, though.
13:53:27@_slack_runtimeverification_UDUFMGVPZ:matrix.orgryuya.nakamura I’ll back to you soon when I found something!
17 Dec 2018
03:01:14@_slack_runtimeverification_UDUFMGVPZ:matrix.orgryuya.nakamura I found that the same assertionError occurs with this simple code in both Solidity and Vyper.
data: uint256

def setZero():
    self.data = 0
pragma solidity ^0.5.0;

contract Test {
    uint256 data;
    function setZero() public {
        data = 0;

There are no newer messages yet.

Back to Room List