Sender | Message | Time |
---|---|---|
28 Nov 2022 | ||
It looks like you're already using solc-to-k , and the Foundry integration should be able to state all the properties you've posted here. | 15:46:48 | |
But allows you to work fully in-solidity. | 15:46:54 | |
True. I tried following the rewrites in evm.md and found that it halts around the place I describe in this issue: https://github.com/runtimeverification/evm-semantics/issues/1469 | 15:48:39 | |
I haven't used the foundry integration of kevm yet. But I will try it too. | 15:49:15 | |
As a (quick and hacky) workaround, you can modify KEVM to skip accessStorage step. | 15:57:42 | |
But that is obviously not desirable long-term. | 15:57:49 | |
You can do this like this:
rule k #accessStorage => . ... /k [priority(45)] | 15:58:09 | |
Note this is not in general sound. | 15:58:28 | |
But it will get you past this (rather silly) problem, so you can focus on more interesting things. | 15:58:43 | |
16 Dec 2022 | ||
07:24:35 | ||
19 Dec 2022 | ||
00:54:10 | ||
07:03:29 | ||
23 Dec 2022 | ||
09:29:08 | ||
11 Jan 2023 | ||
I have a question about how K parses to potential uses of reachability symbols. In reachability-symbols.md I can find one example (for "one-path next") of how a K rule is mapped to a reachability symbol, but for the others there isn't such a mapping given. In the bmc tests I can see that the Are there any more documentation sources and/or K examples of how these reachability symbols can be used during verification? Or how they are (implicitly) used during verification? | 13:10:21 | |
Hmmmm, well as far as I know, we translate the reachability arrow in claims to #wEF (weak exists finally), but I may be incorrect on that. DKJPMGMS do you know?
The other symbols I think do not have immediate use, but we did have a temporal model checker for K called KBMC that used them. I think 7MM1DXE0 may know about that? Not sure. | 18:23:09 | |
21:30:38 | ||
As far as I can remember, the semantics rules are translated into "one-path next" implications. reachablility claims are translated into either wEF or wAF implications. The haskell backend is capable of computing the all path next of a symbolic configuration. Together with some strategies, the haskell backend can be used to prove one-path/all-path reachablility claims. However, I don't think these reachability symbols explicitly appear in the execution of the haskell backend. In other words, the semantics of these symbols are hard-coded in the strategy implemented in the haskell backend. I think 7QGKQWE4 have some work on recovering the proof from the internal state of the haskell backend. In the proof, those symbol should reappear. | 21:30:39 | |
The "one-path next" symbol captures one-step execution steps. It specifies the underlying transition relation of every K semantics. All the other operators such as AG wEF and wAF are definable using one-path next and least/greatest fixpoints operations. Unfortunately, iirc their concrete definitions are not to be found in Kore because Kore doesn't support specifications of fixpoints yet.
Given that said, there is documentation about these reachability symbols. For one-path reachability wEF see https://github.com/runtimeverification/haskell-backend/blob/master/docs/2018-11-08-One-Path-Reachability-Proofs.md. For all-path reachability wAF see https://github.com/runtimeverification/haskell-backend/blob/master/docs/2019-03-28-All-Path-Reachability-Proofs.md. These two reachability relations are used in verification. This paper (https://fsl.cs.illinois.edu/publications/stefanescu-park-yuwen-li-rosu-2016-oopsla.html) explains both of them and discusses the K verification algorithms. | 21:55:43 | |
12 Jan 2023 | ||
That's right, we only use those modalities to parse claims accordingly and the strategies themselves are hardcoded in the backend. | 11:13:59 | |
13 Jan 2023 | ||
Thank you for the information | 10:20:34 | |
Hi all, we are looking for people with some experience in K.
| 10:41:11 | |
14:13:19 | ||
16 Jan 2023 | ||
12:15:46 | ||
21:47:07 | ||
18 Jan 2023 | ||
06:16:07 | ||
24 Jan 2023 | ||
21:16:40 | ||
27 Jan 2023 | ||
07:34:51 | ||
28 Jan 2023 | ||
09:54:31 | ||
2 Feb 2023 | ||
20:09:12 | ||
20:09:27 |