You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Copy file name to clipboardExpand all lines: README.md
+9-7Lines changed: 9 additions & 7 deletions
Original file line number
Diff line number
Diff line change
@@ -1,12 +1,8 @@
1
1
# MIR Semantics
2
2
3
-
In this repository, we provide a model of RustMIR in K.
3
+
In this repository, we provide a model of the semantics of Rust's Stable MIR in K to enable symbolic execution of Rust programs and proofs of program properties.
4
4
5
-
NOTE: This project is currently under reconstruction with changes and work outlined in [Polkadot Referendum #749](https://polkadot.subsquare.io/referenda/749). Some features you may be familiar with (concrete execution and symbolic execution) are currently removed while project foundations are improved.
6
-
7
-
Currently, the project is working to stabilize the serialized output of stable MIR (see our current [Rust PR](https://github.com/rust-lang/rust/pull/126963)) and develop the semantics for this output.
8
-
9
-
If you would like to try a legacy version of the project, [this blog post](https://runtimeverification.com/blog/introducing-kmir) has a tutorial on how to get started. However, it is important to install a legacy version for this to work, so when the tutorial prompts to install the latest version of KMIR with `kup install kmir`, this should be replaced instead with `kup install kmir --version v0.2.21`
5
+
Also included is the `kmir` tool, a python script that acts as a front-end to the semantics.
10
6
11
7
12
8
## For Developers
@@ -25,7 +21,7 @@ For interactive use, spawn a shell with `poetry -C kmir/ shell` (after `poetry -
25
21
26
22
### Stable-MIR-JSON Setup
27
23
28
-
At the moment, to interact with some of KMIR functionalities, it is necessary to provide the tool with a serialized JSON of a Rust program's Stable MIR. To be able to extract these serialized SMIR JSONs, you can use the `Stable-MIR-JSON` tool, setting it up with the following commands:
24
+
To interact with some of KMIR functionalities, it is necessary to provide the tool with a serialized JSON of a Rust program's Stable MIR. To be able to extract these serialized SMIR JSONs, you can use the `Stable-MIR-JSON` tool, setting it up with the following commands:
29
25
30
26
```Rust
31
27
gitsubmoduleupdate--init--recursive
@@ -47,3 +43,9 @@ Use `--help` with each command for more details.
47
43
`kmir prove run` to run the prover on a spec generated by `gen-spec`.
48
44
49
45
`kmir prove view` to run the KCFG visualizer and inspect the proof steps.
46
+
47
+
### Supporters
48
+
49
+
KMIR / mir-semantics is supported by funding from the following sources:
50
+
-[Polkadot Open Gov](https://polkadot.subsquare.io/referenda/749)
0 commit comments