Skip to content

Commit caf61b6

Browse files
dkcummingdkcumming
authored
Merge branch 'master' into verify-rust-std/challenge-0011
2 parents 311bea1 + 9cb1679 commit caf61b6

5 files changed

Lines changed: 202 additions & 201 deletions

File tree

‎README.md‎

Lines changed: 101 additions & 184 deletions
Original file line numberDiff line numberDiff line change
@@ -1,245 +1,162 @@
11
# MIR Semantics
22

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.
3+
`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.
44

5-
Also included is the `kmir` tool, a python script that acts as a front-end to the semantics.
5+
For semantics details and specialized workflows, see [Further Reading](#further-reading).
66

7+
## Quick Start
78

8-
## For Developers
9+
### Prerequisites
910

10-
### KMIR Setup
11-
12-
Pre-requisites:
13-
- `python >= 3.10`
11+
- [Python](https://www.python.org/) `>= 3.10`
1412
- [`uv`](https://docs.astral.sh/uv/)
15-
- `pip >= 20.0.2`
16-
- `gcc >= 11.4.0`
17-
- `cargo == nightly-2024-11-29`
18-
- K. The required K version is specified in `deps/k_release`. To install K, follow the steps available in [K's Quick Start instructions](https://github.com/runtimeverification/k?tab=readme-ov-file#quick-start).
13+
- [`pip`](https://pip.pypa.io/) `>= 20.0.2`
14+
- [`gcc`](https://gcc.gnu.org/) `>= 11.4.0`
15+
- [Rust](https://rustup.rs/) via `rustup`
16+
- [K Framework](https://github.com/runtimeverification/k?tab=readme-ov-file#quick-start), using the version pinned in [`deps/k_release`](deps/k_release)
1917

20-
```bash
21-
make build
22-
```
18+
### Clone and set up
2319

24-
Use `make` to run common tasks (see the [Makefile](Makefile) for a complete list of available targets).
20+
```bash
21+
git clone --recurse-submodules https://github.com/runtimeverification/mir-semantics.git
22+
cd mir-semantics
2523

26-
For interactive use, first sync the environment with `uv --directory kmir sync`, then either:
27-
- Run Python directly: `uv --directory kmir run python`
28-
- Activate the virtual environment: `source kmir/.venv/bin/activate` (on Unix/macOS) or `kmir\.venv\Scripts\activate` (on Windows)
29-
- Or directly run commands from `mir-semantics` root: `uv --directory kmir run kmir <COMMAND>`
24+
# If you cloned without --recurse-submodules:
25+
git submodule update --init --recursive
26+
```
3027

31-
### Stable-MIR-JSON Setup
28+
### Build
3229

33-
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.
30+
The pinned Rust toolchain and components are declared in [`rust-toolchain.toml`](rust-toolchain.toml) and installed automatically by `rustup` on first use.
3431

35-
#### Quick Start
3632
```bash
37-
git submodule update --init --recursive
33+
# Build K semantics definitions (required for kmir)
34+
make build
35+
36+
# Build stable-mir-json (required for SMIR generation, integration tests)
3837
make stable-mir-json
3938
```
4039

41-
#### Generating SMIR JSON Files
40+
`uv` will create and use the Python environment for the `kmir` project automatically.
4241

43-
After setting up stable-mir-json, you can generate SMIR JSON files from Rust source code:
42+
### Verify the setup
4443

45-
**Using the stable-mir-json tool directly:**
4644
```bash
47-
# For single files
48-
deps/.stable-mir-json/debug.sh -Zno-codegen your_file.rs
45+
# Just kmir
46+
uv --project kmir run kmir --help
4947

50-
# For cargo projects
51-
RUSTC=deps/.stable-mir-json/debug.sh cargo build
48+
# Full contributor check
49+
make smir-parse-tests
5250
```
5351

54-
**Using the convenience script:**
55-
```bash
56-
# Generate JSON file
57-
./scripts/generate-smir-json.sh your_file.rs .
52+
## Common Workflows
5853

59-
# Generate with visualization (PNG, PDF, DOT)
60-
./scripts/generate-smir-json.sh your_file.rs . png
61-
./scripts/generate-smir-json.sh your_file.rs . pdf
62-
./scripts/generate-smir-json.sh your_file.rs . dot
63-
```
54+
### Task-to-command map
6455

65-
For more information on testing, installation, and general usage of this tool, please check [Stable-MIR-JSON's repository](https://github.com/runtimeverification/stable-mir-json/).
56+
| Task | Command | Notes |
57+
| --- | --- | --- |
58+
| Build the semantics | `make build` | Requires K and the Python prerequisites. |
59+
| Build `stable-mir-json` in-tree | `make stable-mir-json` | Requires initialized submodules and the pinned Rust nightly. |
60+
| Run unit tests | `make test-unit` | Python-only tests under `kmir/src/tests/unit`. |
61+
| Run integration tests | `make test-integration` | Depends on `stable-mir-json` and `build`. |
62+
| Check Stable MIR parsing | `make smir-parse-tests` | Compiles Rust test programs to SMIR JSON and parses them with `kmir`. |
6663

67-
## Usage
64+
`make test-integration` already depends on `make stable-mir-json` and `make build`, so it is the full contributor path for integration coverage.
6865

69-
Use `--help` with each command for more details.
66+
## Using `kmir`
7067

71-
### Basic Commands
68+
Every subcommand supports `--help` for the full option list.
7269

73-
**`kmir run`** - Execute a Rust program from SMIR JSON or directly from source
74-
```bash
75-
# Run from SMIR JSON file
76-
uv --project kmir run kmir run --file path/to/program.smir.json
70+
| Command | Purpose |
71+
| --- | --- |
72+
| `kmir run` | Execute a Rust program from SMIR JSON |
73+
| `kmir prove-rs` | Prove properties of a Rust source file (recommended entry point) |
74+
| `kmir show` | Inspect a proof graph — nodes, deltas, rules, statistics |
75+
| `kmir view` | Interactive proof viewer |
76+
| `kmir prune` | Remove a node (and its subtree) from a proof |
77+
| `kmir section-edge` | Split a proof edge into finer sections |
78+
| `kmir link` | Link multiple SMIR JSON files into one |
79+
| `kmir info` | Show type information from a SMIR JSON file |
7780

78-
# Run with verbose output
79-
uv --project kmir run kmir run --file path/to/program.smir.json --verbose
80-
```
81+
### Typical proof workflow
8182

82-
**`kmir prove-rs`** - Directly prove properties of Rust source code (recommended)
8383
```bash
84-
# Basic proof
85-
uv --project kmir run kmir prove-rs path/to/program.rs
84+
# 1. Run a proof
85+
uv --project kmir run kmir prove-rs program.rs --proof-dir ./proofs --verbose
8686

87-
# Detailed proof with output
88-
uv --project kmir run kmir prove-rs path/to/program.rs --verbose --proof-dir ./proof_dir
89-
```
87+
# 2. Overview — see all leaves and statistics
88+
uv --project kmir run kmir show proof_id --proof-dir ./proofs --leaves --statistics
9089

91-
**`kmir gen-spec`** - Generate K specification from SMIR JSON
92-
```bash
93-
uv --project kmir run kmir gen-spec path/to/program.smir.json --output-file path/to/spec.k
94-
```
90+
# 3. Zoom into specific nodes / transitions
91+
uv --project kmir run kmir show proof_id --proof-dir ./proofs --nodes "4,5" --node-deltas "4:5"
9592

96-
**`kmir link`** - Link together multiple SMIR JSON files
97-
```bash
98-
# Link multiple SMIR JSON files into a single output file
99-
uv --project kmir run kmir link file1.smir.json file2.smir.json file3.smir.json --output-file linked.smir.json
93+
# 4. See which K rules fired on an edge
94+
uv --project kmir run kmir show proof_id --proof-dir ./proofs --rules "4:5"
10095

101-
# Use default output filename (linker_output.smir.json)
102-
uv --project kmir run kmir link file1.smir.json file2.smir.json
96+
# 5. Full detail for deep debugging
97+
uv --project kmir run kmir show proof_id --proof-dir ./proofs --nodes "5" \
98+
--full-printer --no-omit-static-info --no-omit-current-body
10399
```
104100

105-
**`kmir info`** - Inspect SMIR JSON metadata (currently: types)
106-
```bash
107-
# Show information about specific type IDs in a SMIR JSON
108-
uv --project kmir run kmir info path/to/program.smir.json --types "1,2,3"
109-
110-
# Notes
111-
# - The --types option accepts a comma-separated list of numeric Stable MIR type IDs.
112-
# - Output format: one line per requested type, e.g.:
113-
# Type Ty(1): Int(....)
114-
# Type Ty(2): StructT(name=..., adt_def=..., fields=[...])
115-
# - If --types is omitted, the command currently produces no output.
116-
```
101+
### Debugging a stuck or failing proof
117102

118-
### Analysis Commands
103+
When a proof does not close, the typical cycle is **inspect → refine → re-prove**:
119104

120-
**`kmir show`** - Display proof information with advanced filtering options
121105
```bash
122-
# Basic usage
123-
uv --project kmir run kmir show proof_id --proof-dir ./proof_dir
124-
125-
# Show specific nodes only
126-
uv --project kmir run kmir show proof_id --proof-dir ./proof_dir --nodes "1,2,3"
127-
128-
# Show node deltas (transitions between specific nodes)
129-
uv --project kmir run kmir show proof_id --proof-dir ./proof_dir --node-deltas "1:2,3:4"
106+
# Narrow down where things go wrong — break on every function call
107+
uv --project kmir run kmir prove-rs program.rs --proof-dir ./proofs \
108+
--break-on-calls --max-depth 200
130109

131-
# Show additional deltas after the main output, and also print rules for those edges
132-
uv --project kmir run kmir show proof_id --proof-dir ./proof_dir --node-deltas "1:2" --node-deltas-pro "3:4"
110+
# Or break only when a specific function is entered
111+
uv --project kmir run kmir prove-rs program.rs --proof-dir ./proofs \
112+
--break-on-function "my_module::suspect_fn"
133113

134-
# Display full node information (default is compact)
135-
uv --project kmir run kmir show proof_id --proof-dir ./proof_dir --full-printer
114+
# Split a large edge to find the exact divergence point
115+
uv --project kmir run kmir section-edge proof_id "4,5" --proof-dir ./proofs --sections 4
136116

137-
# Show static information cells (functions, types, etc.)
138-
uv --project kmir run kmir show proof_id --proof-dir ./proof_dir --no-omit-static-info
117+
# Prune a bad subtree and re-run
118+
uv --project kmir run kmir prune proof_id 5 --proof-dir ./proofs
119+
uv --project kmir run kmir prove-rs program.rs --proof-dir ./proofs
139120

140-
# Show current body cell content
141-
uv --project kmir run kmir show proof_id --proof-dir ./proof_dir --no-omit-current-body
142-
143-
# Omit specific cells from output
144-
uv --project kmir run kmir show proof_id --proof-dir ./proof_dir --omit-cells "cell1,cell2"
145-
146-
# Combine multiple options for detailed analysis
147-
uv --project kmir run kmir show proof_id --proof-dir ./proof_dir --full-printer --no-omit-static-info --nodes "1,2" --verbose
121+
# Export a proof subgraph as a reusable K module
122+
uv --project kmir run kmir show proof_id --proof-dir ./proofs --to-module lemma.json --minimize-proof
123+
# then re-prove with the lemma
124+
uv --project kmir run kmir prove-rs program.rs --proof-dir ./proofs --add-module lemma.json
148125
```
149126

150-
**`kmir view`** - Detailed view of proof results
151-
```bash
152-
uv --project kmir run kmir view proof_id --proof-dir ./proof_dir --verbose
153-
```
127+
Other useful `prove-rs` break flags: `--break-every-step`, `--break-every-terminator`, `--break-on-thunk`, `--terminate-on-thunk`.
154128

155-
**Rules within `kmir show`** - Show rules applied between nodes
156-
```bash
157-
uv --project kmir run kmir show proof_id --proof-dir ./proof_dir --rules "SOURCE:TARGET[,SOURCE:TARGET...]"
158-
```
159-
160-
### Recommended Workflow
161-
162-
1. **Setup Environment**:
163-
```bash
164-
make stable-mir-json # Setup stable-mir-json
165-
make build # Build K definitions
166-
```
167-
168-
2. **Direct Proof** (Recommended):
169-
```bash
170-
uv --project kmir run kmir prove-rs your_file.rs --verbose --proof-dir ./proof_dir
171-
```
172-
173-
3. **View Results**:
174-
```bash
175-
# Quick overview (compact format, static info hidden)
176-
uv --project kmir run kmir show proof_id --proof-dir ./proof_dir
177-
178-
# Detailed analysis with full information
179-
uv --project kmir run kmir show proof_id --proof-dir ./proof_dir --full-printer --no-omit-static-info
180-
181-
# Focus on specific nodes
182-
uv --project kmir run kmir show proof_id --proof-dir ./proof_dir --nodes "1,2,3"
183-
184-
# Interactive view
185-
uv --project kmir run kmir view proof_id --proof-dir ./proof_dir --verbose
186-
```
187-
188-
4. **Analyze Rules**:
189-
```bash
190-
uv --project kmir run kmir show proof_id --proof-dir ./proof_dir --rules "1:3"
191-
```
192-
193-
### Advanced Show Usage Examples
194-
195-
**Debugging workflow:**
196-
```bash
197-
# 1. Start with a quick overview
198-
uv --project kmir run kmir show my_proof --proof-dir ./proofs
129+
### Generate Stable MIR JSON manually
199130

200-
# 2. Focus on problematic nodes (e.g., nodes 5, 6, 7)
201-
uv --project kmir run kmir show my_proof --proof-dir ./proofs --nodes "5,6,7"
131+
After `make stable-mir-json`:
202132

203-
# 3. Examine transitions between specific nodes
204-
uv --project kmir run kmir show my_proof --proof-dir ./proofs --node-deltas "5:6,6:7"
205-
206-
# 4. Get full details for deep debugging
207-
uv --project kmir run kmir show my_proof --proof-dir ./proofs --nodes "6" --full-printer --no-omit-static-info --no-omit-current-body
208-
```
209-
210-
**Performance analysis:**
211133
```bash
212-
# Hide verbose cells but show execution flow
213-
uv --project kmir run kmir show my_proof --proof-dir ./proofs --omit-cells "locals,heap" --verbose
134+
# Single file
135+
deps/.stable-mir-json/debug.sh -Zno-codegen your_file.rs
136+
137+
# Cargo project
138+
RUSTC=deps/.stable-mir-json/debug.sh cargo build
214139

215-
# Focus on function calls and type information
216-
uv --project kmir run kmir show my_proof --proof-dir ./proofs --no-omit-static-info --omit-cells "currentBody"
140+
# Convenience script (also supports png/pdf/dot visualization)
141+
./scripts/generate-smir-json.sh <rust-file> <output-dir> [png|pdf|dot]
217142
```
218143

219-
### Command Options
144+
## Troubleshooting
220145

221-
Most commands support:
222-
- `--verbose, -v`: Detailed output
223-
- `--debug`: Debug information
224-
- `--proof-dir DIR`: Directory for proof results
225-
- `--max-depth DEPTH`: Maximum execution depth
226-
- `--max-iterations ITERATIONS`: Maximum iterations
146+
- **Rust toolchain errors**: The toolchain is declared in [`rust-toolchain.toml`](rust-toolchain.toml) and should install automatically on first use. If not, run `rustup toolchain install nightly-2024-11-29 --component llvm-tools --component rustc-dev --component rust-src`.
147+
- **`deps/stable-mir-json` is missing**: Run `git submodule update --init --recursive`.
148+
- **Not sure which `make` target to run**: `make build` for basic `kmir`; add `make stable-mir-json` for SMIR generation; `make test-integration` for the full suite.
227149

228-
**`kmir show` specific options:**
229-
- `--nodes NODES`: Comma separated list of node IDs to show (e.g., "1,2,3")
230-
- `--node-deltas DELTAS`: Comma separated list of node deltas in format "source:target" (e.g., "1:2,3:4")
231-
- `--node-deltas-pro DELTAS`: Additional node deltas (same format as `--node-deltas`). Equivalent to "print the corresponding deltas again, and automatically print the rules for these edges".
232-
- `--rules EDGES`: Comma separated list of edges in format "source:target". Prints rules for each edge in Markdown link format `[label](file:///abs/path#LstartLine)` when available
233-
- `--omit-cells CELLS`: Comma separated list of cell names to omit from output
234-
- `--full-printer`: Display the full node in output (default is compact)
235-
- `--no-omit-static-info`: Display static information cells (functions, start-symbol, types, adt-to-ty)
236-
- `--no-omit-current-body`: Display the `<currentBody>` cell completely
237-
- `--smir-info SMIR_INFO`: Path to SMIR JSON file to improve debug messaging
150+
## Further Reading
238151

239-
For complete options, use `--help` with each command.
152+
- [docs/semantics-of-mir.md](docs/semantics-of-mir.md)
153+
- [docs/example-mir-execution-flow.md](docs/example-mir-execution-flow.md)
154+
- [docs/dev/adding-intrinsics.md](docs/dev/adding-intrinsics.md)
155+
- [docs/feature-checklist.md](docs/feature-checklist.md)
156+
- [Stable-MIR-JSON repository](https://github.com/runtimeverification/stable-mir-json/)
240157

241-
### Supporters
158+
## Supporters
242159

243-
KMIR / mir-semantics is supported by funding from the following sources:
160+
KMIR / mir-semantics is supported by funding from:
244161
- [Polkadot Open Gov](https://polkadot.subsquare.io/referenda/749)
245162
- Solana

0 commit comments

Comments
 (0)