mir-semantics models the semantics of Rust Stable MIR in K. The repository also ships kmir, a Python CLI for building the semantics, running programs, generating specs, and inspecting proofs.
For semantics details and specialized workflows, see Further Reading.
- Python
>= 3.10 uvpip>= 20.0.2gcc>= 11.4.0- Rust via
rustup - K Framework, using the version pinned in
deps/k_release
git clone --recurse-submodules https://github.com/runtimeverification/mir-semantics.git
cd mir-semantics
# If you cloned without --recurse-submodules:
git submodule update --init --recursiveThe pinned Rust toolchain and components are declared in rust-toolchain.toml and installed automatically by rustup on first use.
# Build K semantics definitions (required for kmir)
make build
# Build stable-mir-json (required for SMIR generation, integration tests)
make stable-mir-jsonuv will create and use the Python environment for the kmir project automatically.
# Just kmir
uv --project kmir run kmir --help
# Full contributor check
make smir-parse-tests| Task | Command | Notes |
|---|---|---|
| Build the semantics | make build |
Requires K and the Python prerequisites. |
Build stable-mir-json in-tree |
make stable-mir-json |
Requires initialized submodules and the pinned Rust nightly. |
| Run unit tests | make test-unit |
Python-only tests under kmir/src/tests/unit. |
| Run integration tests | make test-integration |
Depends on stable-mir-json and build. |
| Check Stable MIR parsing | make smir-parse-tests |
Compiles Rust test programs to SMIR JSON and parses them with kmir. |
make test-integration already depends on make stable-mir-json and make build, so it is the full contributor path for integration coverage.
Every subcommand supports --help for the full option list.
| Command | Purpose |
|---|---|
kmir run |
Execute a Rust program from SMIR JSON |
kmir prove-rs |
Prove properties of a Rust source file (recommended entry point) |
kmir show |
Inspect a proof graph — nodes, deltas, rules, statistics |
kmir view |
Interactive proof viewer |
kmir prune |
Remove a node (and its subtree) from a proof |
kmir section-edge |
Split a proof edge into finer sections |
kmir link |
Link multiple SMIR JSON files into one |
kmir info |
Show type information from a SMIR JSON file |
# 1. Run a proof
uv --project kmir run kmir prove-rs program.rs --proof-dir ./proofs --verbose
# 2. Overview — see all leaves and statistics
uv --project kmir run kmir show proof_id --proof-dir ./proofs --leaves --statistics
# 3. Zoom into specific nodes / transitions
uv --project kmir run kmir show proof_id --proof-dir ./proofs --nodes "4,5" --node-deltas "4:5"
# 4. See which K rules fired on an edge
uv --project kmir run kmir show proof_id --proof-dir ./proofs --rules "4:5"
# 5. Full detail for deep debugging
uv --project kmir run kmir show proof_id --proof-dir ./proofs --nodes "5" \
--full-printer --no-omit-static-info --no-omit-current-bodyWhen a proof does not close, the typical cycle is inspect → refine → re-prove:
# Narrow down where things go wrong — break on every function call
uv --project kmir run kmir prove-rs program.rs --proof-dir ./proofs \
--break-on-calls --max-depth 200
# Or break only when a specific function is entered
uv --project kmir run kmir prove-rs program.rs --proof-dir ./proofs \
--break-on-function "my_module::suspect_fn"
# Split a large edge to find the exact divergence point
uv --project kmir run kmir section-edge proof_id "4,5" --proof-dir ./proofs --sections 4
# Prune a bad subtree and re-run
uv --project kmir run kmir prune proof_id 5 --proof-dir ./proofs
uv --project kmir run kmir prove-rs program.rs --proof-dir ./proofs
# Export a proof subgraph as a reusable K module
uv --project kmir run kmir show proof_id --proof-dir ./proofs --to-module lemma.json --minimize-proof
# then re-prove with the lemma
uv --project kmir run kmir prove-rs program.rs --proof-dir ./proofs --add-module lemma.jsonOther useful prove-rs break flags: --break-every-step, --break-every-terminator, --break-on-thunk, --terminate-on-thunk.
After make stable-mir-json:
# Single file
deps/.stable-mir-json/debug.sh -Zno-codegen your_file.rs
# Cargo project
RUSTC=deps/.stable-mir-json/debug.sh cargo build
# Convenience script (also supports png/pdf/dot visualization)
./scripts/generate-smir-json.sh <rust-file> <output-dir> [png|pdf|dot]- Rust toolchain errors: The toolchain is declared in
rust-toolchain.tomland should install automatically on first use. If not, runrustup toolchain install nightly-2024-11-29 --component llvm-tools --component rustc-dev --component rust-src. deps/stable-mir-jsonis missing: Rungit submodule update --init --recursive.- Not sure which
maketarget to run:make buildfor basickmir; addmake stable-mir-jsonfor SMIR generation;make test-integrationfor the full suite.
- docs/semantics-of-mir.md
- docs/example-mir-execution-flow.md
- docs/dev/adding-intrinsics.md
- docs/feature-checklist.md
- Stable-MIR-JSON repository
KMIR / mir-semantics is supported by funding from:
- Polkadot Open Gov
- Solana
