 | 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-semantics | 3 Servers |
| 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-semantics | 3 Servers |
| Timestamp | Message | |
|---|---|---|
| 3 Dec 2018 | ||
| 11:48:14 |  ryuya.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 | ryuya.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 |  denis.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 | denis.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 | denis.bogdanas | Latest k-gnosis also shows memory usage at each step and in summary box. |
| 12:21:02 |  equivrel | 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 | equivrel | what 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 | equivrel | To 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 | ryuya.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 | ryuya.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 | ryuya.nakamura | One of the specs above is this https://gist.github.com/nrryuya/62ebd2b3204564a76fb96ec54535f045 |
| 15:14:20 | denis.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 | denis.bogdanas | So is that a problem? Do you expect them to fail? |
| 23:50:01 | ryuya.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 | ryuya.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 | ryuya.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 | ryuya.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 | ryuya.nakamura | Anyway, thank you so much for your support. |
| 7 Dec 2018 | ||
| 18:54:48 |  gkobeaga joined the room. | |
| 16 Dec 2018 | ||
| 03:09:19 | ryuya.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 🙇 |
| 03:12:25 | ryuya.nakamura | K_VERSION :=b65568ade007d54dd21667f4f56f2d7471bb6596 KEVM_VERSION:=5d3bbb6d9dd3a2913201071937cb3f00d66832b0 |
| 12:50:00 | denis.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 | equivrel | Or use klab :D |
| 13:46:48 | ryuya.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 | ryuya.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 | ryuya.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 | denis.bogdanas | Thanks for link. I don't really know what can lead to AssertionError on that line:) |
| 13:52:36 | ryuya.nakamura | I might be misunderstanding, though. |
| 13:53:27 | ryuya.nakamura | I’ll back to you soon when I found something! |
| 17 Dec 2018 | ||
| 03:01:14 | ryuya.nakamura | I found that the same assertionError occurs with this simple code in both Solidity and Vyper.
data: uint256
@public
def setZero():
self.data = 0
pragma solidity ^0.5.0;
contract Test {
uint256 data;
function setZero() public {
data = 0;
}
}
|