The K Framework User Group

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

Load older messages

Timestamp Message
23 Mar 2020
19:42:06@_slack_runtimeverification_UFTN1UV4H:matrix.orgrikard.hjort It would be nice to be able to get some highlight/printout of where exactly the matching with the final state fails.
19:56:31@_slack_runtimeverification_U5GE6G57G:matrix.orgdwight.guth I mean, if it's getting stuck after one step, it's not even reaching the final state
19:56:37@_slack_runtimeverification_U5GE6G57G:matrix.orgdwight.guth unless the final state only takes one step
19:57:36@_slack_runtimeverification_U5GE6G57G:matrix.orgdwight.guth the question isn't so much, why didn't the final state succeed, it's, why didn't the second step of the proof succeed?
24 Mar 2020
14:31:35@_slack_runtimeverification_UFTN1UV4H:matrix.orgrikard.hjort In this case, the proof looks like this: ```
14:32:22@_slack_runtimeverification_UFTN1UV4H:matrix.orgrikard.hjort #reverseLoop being a macro
14:35:06@_slack_runtimeverification_UFTN1UV4H:matrix.orgrikard.hjort If I change the k cell to the following, it doesn't get stuck immediately.
    rule  k  #reverseLoop => br 0 ~> label [ .ValTypes ] { #reverseLoop } .ValStack ...  /k 
Here the RHS will rewrite to just #reverseLoop in the next step, i.e. it's the last step before we go back to the beginning of the loop.
25 Mar 2020
05:08:40@ricky2862:matrix.orgricky2862 some questions in KEVM eDSL.md
#hashedLocation({COMPILER}, {_BALANCES}, OWNER) |-> BAL means balance[OWNER] is BAL
but the below means
#hashedLocation({COMPILER}, {_SUPPLY}, .IntList) |-> TOTAL means supply[ ] is TOTAL ?
.IntList is a list composed by integer but now is empty?
05:09:56@ricky2862:matrix.orgricky2862 * some questions in KEVM eDSL.md
#hashedLocation({COMPILER}, {_BALANCES}, OWNER) |-> BAL means balance[OWNER] is BAL
but the below means
#hashedLocation({COMPILER}, {_SUPPLY}, .IntList) |-> TOTAL means supply[ ] is TOTAL ?
.IntList is a list composed by integer but now is empty?
08:07:38@_slack_runtimeverification_U8T2RJ802:matrix.orgeverett.hildenbrandt Yes, that's correct. The empty intlist is because the totalSupply variable in the contract is not an array (which needs indices), but just a value.
09:59:49@ricky2862:matrix.orgricky2862 In bihu example
The order of spec definition in KEVM, is nature languagepseudo codesolidity levelEVM level right?
but I find that the original source code (Solidity) and solidity level in the spec definition is the same.
where did I get wrong
10:13:14@_slack_runtimeverification_U8T2RJ802:matrix.orgeverett.hildenbrandt Usually we don't write a solidity level spec.
10:13:39@_slack_runtimeverification_U8T2RJ802:matrix.orgeverett.hildenbrandt But sometimes we make a high-level model in K, which contains abstract state description and transition system.
10:14:48@_slack_runtimeverification_U8T2RJ802:matrix.orgeverett.hildenbrandt Which may be what you're thinking of. But I don't it's the case for Bihu.
10:19:45@ricky2862:matrix.orgricky2862 You mean that write *-spec.ini directly and use the source code (Solidity) to generate *-spec.k ?
27 Mar 2020
15:43:51@_slack_runtimeverification_UFTN1UV4H:matrix.orgrikard.hjort In domains.k, I noticed and >Int are not marked functional. Any reason for that? Are they not total? ```
16:05:24@_slack_runtimeverification_U5GE6G57G:matrix.orgdwight.guth they are not
16:05:39@_slack_runtimeverification_U5GE6G57G:matrix.orgdwight.guth they are not defined if the second argument is negative
16:13:11@_slack_runtimeverification_UFTN1UV4H:matrix.orgrikard.hjort Ah, of course
16:14:37@_slack_runtimeverification_U5GE6G57G:matrix.orgdwight.guth in theory we could make this case defined, but then there would be an inconsistency with MInt, and MInt we definitely don't want to make that case defined because we want to make sure that we can translate >MInt into native bit shift instructions in llvm
29 Mar 2020
19:36:03@sorpaas:matrix.parity.ioWei Tang changed their display name from Wei Tang to Wei Tang (back on Wed!).
31 Mar 2020
10:51:10@asymmetric:matrix.dapp.org.ukasymmetric set a profile picture.
11:03:55@asymmetric:matrix.dapp.org.ukasymmetric removed their profile picture.
16:03:12@sorpaas:matrix.parity.ioWei Tang changed their display name from Wei Tang (back on Wed!) to Wei Tang.
1 Apr 2020
20:43:42@_slack_runtimeverification_UFTN1UV4H:matrix.orgrikard.hjort Why does the prover consider this a possibility?
    notBool ( Bytes2Int ( ADDRESS , LE , Unsigned ) in_keys ( Bytes2Int ( ADDRESS , LE , Unsigned ) ,-> BALANCE:Int
20:43:58@_slack_runtimeverification_UFTN1UV4H:matrix.orgrikard.hjort I get branching on whether this is true or false
20:54:02@_slack_runtimeverification_UFTN1UV4H:matrix.orgrikard.hjort Hmm, maybe. Something like rule X in_keys ((X ,-> _) M) => true [simplification]?
20:55:29@_slack_runtimeverification_UFTN1UV4H:matrix.orgrikard.hjort There is this one: rule K1 in_keys(M K2 ,-> _) => true requires K1 ==K K2 orBool K1 in_keys(M)
20:56:09@_slack_runtimeverification_UFTN1UV4H:matrix.orgrikard.hjort Is my rule unsound? Is it possible that X is not int the keys of (X ,-> Y) MAP?
2 Apr 2020
11:19:37@_slack_runtimeverification_UFTN1UV4H:matrix.orgrikard.hjort I added these two rules, and it is still branching
    rule K1 in_keys ((K2 ,-> _) M) => true  requires K1 ==K K2 [simplification]
    rule Bytes2Int(ADDR, ENDIANNESS, SIGNEDNESS) ==K Bytes2Int(ADDR, ENDIANNESS, SIGNEDNESS) => true [simplification]
The second one is just an extra sanity check---I assume it's a theorem for all functions.

There are no newer messages yet.

Back to Room List