In this repository, we provide a model of Rust MIR in K.
NOTE: This project is currently under reconstruction with changes and work outlined in Polkadot Referendum #749. Some features you may be familiar with (concrete execution and symbolic execution) are currently removed while project foundations are improved.
Currently the project is working to stablise serialised output of stable MIR (see our current Rust PR), and develop the semantics for this output.
If you would like to try a legacy version of the project, this blog post has a tutorial to get started with. However it is important to install a legacy version for this to work, and 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
Prerequsites: python >= 3.10, pip >= 20.0.2, poetry >= 1.3.2.
make build
pip install dist/*.whlUse make to run common tasks (see the Makefile for a complete list of available targets).
make build: Build wheel
For interactive use, spawn a shell with poetry -C kmir/ shell (after poetry -C kmir/ install), then run an interpreter.
Use --help with each command for more details.
kmir run to load an SMIR json generated by the stable-mir-json tool.
kmir gen-spec to take an SMIR json and create a K specification module that ensures termination of the program.
kmir prove to run the prover on a spec generated by gen-spec.