 | 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-semantics | 42 Servers |
| 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-semantics | 42 Servers |
| Timestamp | Message | |
|---|---|---|
| 23 Mar 2020 | ||
| 19:42:06 |  rikard.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 |  dwight.guth | I mean, if it's getting stuck after one step, it's not even reaching the final state |
| 19:56:37 | dwight.guth | unless the final state only takes one step |
| 19:57:36 | dwight.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 | rikard.hjort | In this case, the proof looks like this: ``` |
| 14:32:22 | rikard.hjort | #reverseLoop being a macro |
| 14:35:06 | rikard.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 | some questions in KEVM eDSL.md#hashedLocation({COMPILER}, {_BALANCES}, OWNER) |-> BAL means balance[OWNER] is BALbut the below means #hashedLocation({COMPILER}, {_SUPPLY}, .IntList) |-> TOTAL means supply[ ] is TOTAL ?.IntList is a list composed by integer but now is empty? thanks. |
| 05:09:56 | ricky2862 | * some questions in KEVM eDSL.md#hashedLocation({COMPILER}, {_BALANCES}, OWNER) |-> BAL means balance[OWNER] is BALbut the below means #hashedLocation({COMPILER}, {_SUPPLY}, .IntList) |-> TOTAL means supply[ ] is TOTAL ?.IntList is a list composed by integer but now is empty? thanks. |
| 08:07:38 |  everett.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 | In bihu exampleThe order of spec definition in KEVM, is nature language→pseudo code→solidity level→EVM 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 | everett.hildenbrandt | Usually we don't write a solidity level spec. |
| 10:13:39 | everett.hildenbrandt | But sometimes we make a high-level model in K, which contains abstract state description and transition system. |
| 10:14:48 | everett.hildenbrandt | Which may be what you're thinking of. But I don't it's the case for Bihu. |
| 10:19:45 | ricky2862 | You mean that write *-spec.ini directly and use the source code (Solidity) to generate *-spec.k ? |
| 27 Mar 2020 | ||
| 15:43:51 | rikard.hjort | In domains.k, I noticed and |
| 16:05:24 | dwight.guth | they are not |
| 16:05:39 | dwight.guth | they are not defined if the second argument is negative |
| 16:13:11 | rikard.hjort | Ah, of course |
| 16:14:37 | dwight.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 |  Wei Tang changed their display name from Wei Tang to Wei Tang (back on Wed!). | |
| 31 Mar 2020 | ||
| 10:51:10 |  asymmetric set a profile picture. | |
| 11:03:55 | asymmetric removed their profile picture. | |
| 16:03:12 | Wei Tang changed their display name from Wei Tang (back on Wed!) to Wei Tang. | |
| 1 Apr 2020 | ||
| 20:43:42 | rikard.hjort | Why does the prover consider this a possibility?
notBool ( Bytes2Int ( ADDRESS , LE , Unsigned ) in_keys ( Bytes2Int ( ADDRESS , LE , Unsigned ) ,-> BALANCE:Int
CONTRACT_STORAGE ) )
#Equals
true |
| 20:43:58 | rikard.hjort | I get branching on whether this is true or false |
| 20:54:02 | rikard.hjort | Hmm, maybe. Something like rule X in_keys ((X ,-> _) M) => true [simplification]? |
| 20:55:29 | rikard.hjort | There is this one:
rule K1 in_keys(M K2 ,-> _) => true requires K1 ==K K2 orBool K1 in_keys(M) |
| 20:56:09 | rikard.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 | rikard.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. |