docs: streamline README and improve CLI --help descriptions

README.md

@@ -1,245 +1,162 @@
 # MIR Semantics
 
-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.
+`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.
 
-Also included is the `kmir` tool, a python script that acts as a front-end to the semantics.
+For semantics details and specialized workflows, see [Further Reading](#further-reading).
 
+## Quick Start
 
-## For Developers
+### Prerequisites
 
-### KMIR Setup
-
-Pre-requisites:
-- `python >= 3.10`
+- [Python](https://www.python.org/) `>= 3.10`
 - [`uv`](https://docs.astral.sh/uv/)
-- `pip >= 20.0.2`
-- `gcc >= 11.4.0`
-- `cargo == nightly-2024-11-29`
-- 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).
+- [`pip`](https://pip.pypa.io/) `>= 20.0.2`
+- [`gcc`](https://gcc.gnu.org/) `>= 11.4.0`
+- [Rust](https://rustup.rs/) via `rustup`
+- [K Framework](https://github.com/runtimeverification/k?tab=readme-ov-file#quick-start), using the version pinned in [`deps/k_release`](deps/k_release)
 
-```bash
-make build
-```
+### Clone and set up
 
-Use `make` to run common tasks (see the [Makefile](Makefile) for a complete list of available targets).
+```bash
+git clone --recurse-submodules https://github.com/runtimeverification/mir-semantics.git
+cd mir-semantics
 
-For interactive use, first sync the environment with `uv --directory kmir sync`, then either:
-- Run Python directly: `uv --directory kmir run python`
-- Activate the virtual environment: `source kmir/.venv/bin/activate` (on Unix/macOS) or `kmir\.venv\Scripts\activate` (on Windows)
-- Or directly run commands from `mir-semantics` root: `uv --directory kmir run kmir <COMMAND>`
+# If you cloned without --recurse-submodules:
+git submodule update --init --recursive
+```
 
-### Stable-MIR-JSON Setup
+### Build
 
-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.
+The pinned Rust toolchain and components are declared in [`rust-toolchain.toml`](rust-toolchain.toml) and installed automatically by `rustup` on first use.
 
-#### Quick Start
 ```bash
-git submodule update --init --recursive
+# Build K semantics definitions (required for kmir)
+make build
+
+# Build stable-mir-json (required for SMIR generation, integration tests)
 make stable-mir-json
 ```
 
-#### Generating SMIR JSON Files
+`uv` will create and use the Python environment for the `kmir` project automatically.
 
-After setting up stable-mir-json, you can generate SMIR JSON files from Rust source code:
+### Verify the setup
 
-**Using the stable-mir-json tool directly:**
 ```bash
-# For single files
-deps/.stable-mir-json/debug.sh -Zno-codegen your_file.rs
+# Just kmir
+uv --project kmir run kmir --help
 
-# For cargo projects
-RUSTC=deps/.stable-mir-json/debug.sh cargo build
+# Full contributor check
+make smir-parse-tests
 ```
 
-**Using the convenience script:**
-```bash
-# Generate JSON file
-./scripts/generate-smir-json.sh your_file.rs .
+## Common Workflows
 
-# Generate with visualization (PNG, PDF, DOT)
-./scripts/generate-smir-json.sh your_file.rs . png
-./scripts/generate-smir-json.sh your_file.rs . pdf
-./scripts/generate-smir-json.sh your_file.rs . dot
-```
+### Task-to-command map
 
-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/).
+| 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`. |
 
-## Usage
+`make test-integration` already depends on `make stable-mir-json` and `make build`, so it is the full contributor path for integration coverage.
 
-Use `--help` with each command for more details.
+## Using `kmir`
 
-### Basic Commands
+Every subcommand supports `--help` for the full option list.
 
-**`kmir run`** - Execute a Rust program from SMIR JSON or directly from source
-```bash
-# Run from SMIR JSON file
-uv --project kmir run kmir run --file path/to/program.smir.json
+| 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 |
 
-# Run with verbose output
-uv --project kmir run kmir run --file path/to/program.smir.json --verbose
-```
+### Typical proof workflow
 
-**`kmir prove-rs`** - Directly prove properties of Rust source code (recommended)
 ```bash
-# Basic proof
-uv --project kmir run kmir prove-rs path/to/program.rs
+# 1. Run a proof
+uv --project kmir run kmir prove-rs program.rs --proof-dir ./proofs --verbose
 
-# Detailed proof with output
-uv --project kmir run kmir prove-rs path/to/program.rs --verbose --proof-dir ./proof_dir
-```
+# 2. Overview — see all leaves and statistics
+uv --project kmir run kmir show proof_id --proof-dir ./proofs --leaves --statistics
 
-**`kmir gen-spec`** - Generate K specification from SMIR JSON
-```bash
-uv --project kmir run kmir gen-spec path/to/program.smir.json --output-file path/to/spec.k
-```
+# 3. Zoom into specific nodes / transitions
+uv --project kmir run kmir show proof_id --proof-dir ./proofs --nodes "4,5" --node-deltas "4:5"
 
-**`kmir link`** - Link together multiple SMIR JSON files
-```bash
-# Link multiple SMIR JSON files into a single output file
-uv --project kmir run kmir link file1.smir.json file2.smir.json file3.smir.json --output-file linked.smir.json
+# 4. See which K rules fired on an edge
+uv --project kmir run kmir show proof_id --proof-dir ./proofs --rules "4:5"
 
-# Use default output filename (linker_output.smir.json)
-uv --project kmir run kmir link file1.smir.json file2.smir.json
+# 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-body
 ```
 
-**`kmir info`** - Inspect SMIR JSON metadata (currently: types)
-```bash
-# Show information about specific type IDs in a SMIR JSON
-uv --project kmir run kmir info path/to/program.smir.json --types "1,2,3"
-
-# Notes
-# - The --types option accepts a comma-separated list of numeric Stable MIR type IDs.
-# - Output format: one line per requested type, e.g.:
-#   Type Ty(1): Int(....)
-#   Type Ty(2): StructT(name=..., adt_def=..., fields=[...])
-# - If --types is omitted, the command currently produces no output.
-```
+### Debugging a stuck or failing proof
 
-### Analysis Commands
+When a proof does not close, the typical cycle is **inspect → refine → re-prove**:
 
-**`kmir show`** - Display proof information with advanced filtering options
 ```bash
-# Basic usage
-uv --project kmir run kmir show proof_id --proof-dir ./proof_dir
-
-# Show specific nodes only
-uv --project kmir run kmir show proof_id --proof-dir ./proof_dir --nodes "1,2,3"
-
-# Show node deltas (transitions between specific nodes)
-uv --project kmir run kmir show proof_id --proof-dir ./proof_dir --node-deltas "1:2,3:4"
+# 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
 
-# Show additional deltas after the main output, and also print rules for those edges
-uv --project kmir run kmir show proof_id --proof-dir ./proof_dir --node-deltas "1:2" --node-deltas-pro "3:4"
+# 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"
 
-# Display full node information (default is compact)
-uv --project kmir run kmir show proof_id --proof-dir ./proof_dir --full-printer
+# 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
 
-# Show static information cells (functions, types, etc.)
-uv --project kmir run kmir show proof_id --proof-dir ./proof_dir --no-omit-static-info
+# 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
 
-# Show current body cell content
-uv --project kmir run kmir show proof_id --proof-dir ./proof_dir --no-omit-current-body
-
-# Omit specific cells from output
-uv --project kmir run kmir show proof_id --proof-dir ./proof_dir --omit-cells "cell1,cell2"
-
-# Combine multiple options for detailed analysis
-uv --project kmir run kmir show proof_id --proof-dir ./proof_dir --full-printer --no-omit-static-info --nodes "1,2" --verbose
+# 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.json
 ```
 
-**`kmir view`** - Detailed view of proof results
-```bash
-uv --project kmir run kmir view proof_id --proof-dir ./proof_dir --verbose
-```
+Other useful `prove-rs` break flags: `--break-every-step`, `--break-every-terminator`, `--break-on-thunk`, `--terminate-on-thunk`.
 
-**Rules within `kmir show`** - Show rules applied between nodes
-```bash
-uv --project kmir run kmir show proof_id --proof-dir ./proof_dir --rules "SOURCE:TARGET[,SOURCE:TARGET...]"
-```
-
-### Recommended Workflow
-
-1. **Setup Environment**:
-   ```bash
-   make stable-mir-json  # Setup stable-mir-json
-   make build  # Build K definitions
-   ```
-
-2. **Direct Proof** (Recommended):
-   ```bash
-   uv --project kmir run kmir prove-rs your_file.rs --verbose --proof-dir ./proof_dir
-   ```
-
-3. **View Results**:
-   ```bash
-   # Quick overview (compact format, static info hidden)
-   uv --project kmir run kmir show proof_id --proof-dir ./proof_dir
-
-   # Detailed analysis with full information
-   uv --project kmir run kmir show proof_id --proof-dir ./proof_dir --full-printer --no-omit-static-info
-
-   # Focus on specific nodes
-   uv --project kmir run kmir show proof_id --proof-dir ./proof_dir --nodes "1,2,3"
-
-   # Interactive view
-   uv --project kmir run kmir view proof_id --proof-dir ./proof_dir --verbose
-   ```
-
-4. **Analyze Rules**:
-   ```bash
-   uv --project kmir run kmir show proof_id --proof-dir ./proof_dir --rules "1:3"
-   ```
-
-### Advanced Show Usage Examples
-
-**Debugging workflow:**
-```bash
-# 1. Start with a quick overview
-uv --project kmir run kmir show my_proof --proof-dir ./proofs
+### Generate Stable MIR JSON manually
 
-# 2. Focus on problematic nodes (e.g., nodes 5, 6, 7)
-uv --project kmir run kmir show my_proof --proof-dir ./proofs --nodes "5,6,7"
+After `make stable-mir-json`:
 
-# 3. Examine transitions between specific nodes
-uv --project kmir run kmir show my_proof --proof-dir ./proofs --node-deltas "5:6,6:7"
-
-# 4. Get full details for deep debugging
-uv --project kmir run kmir show my_proof --proof-dir ./proofs --nodes "6" --full-printer --no-omit-static-info --no-omit-current-body
-```
-
-**Performance analysis:**
 ```bash
-# Hide verbose cells but show execution flow
-uv --project kmir run kmir show my_proof --proof-dir ./proofs --omit-cells "locals,heap" --verbose
+# Single file
+deps/.stable-mir-json/debug.sh -Zno-codegen your_file.rs
+
+# Cargo project
+RUSTC=deps/.stable-mir-json/debug.sh cargo build
 
-# Focus on function calls and type information
-uv --project kmir run kmir show my_proof --proof-dir ./proofs --no-omit-static-info --omit-cells "currentBody"
+# Convenience script (also supports png/pdf/dot visualization)
+./scripts/generate-smir-json.sh <rust-file> <output-dir> [png|pdf|dot]
 ```
 
-### Command Options
+## Troubleshooting
 
-Most commands support:
-- `--verbose, -v`: Detailed output
-- `--debug`: Debug information
-- `--proof-dir DIR`: Directory for proof results
-- `--max-depth DEPTH`: Maximum execution depth
-- `--max-iterations ITERATIONS`: Maximum iterations
+- **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`.
+- **`deps/stable-mir-json` is missing**: Run `git submodule update --init --recursive`.
+- **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.
 
-**`kmir show` specific options:**
-- `--nodes NODES`: Comma separated list of node IDs to show (e.g., "1,2,3")
-- `--node-deltas DELTAS`: Comma separated list of node deltas in format "source:target" (e.g., "1:2,3:4")
-- `--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".
-- `--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
-- `--omit-cells CELLS`: Comma separated list of cell names to omit from output
-- `--full-printer`: Display the full node in output (default is compact)
-- `--no-omit-static-info`: Display static information cells (functions, start-symbol, types, adt-to-ty)
-- `--no-omit-current-body`: Display the `<currentBody>` cell completely
-- `--smir-info SMIR_INFO`: Path to SMIR JSON file to improve debug messaging
+## Further Reading
 
-For complete options, use `--help` with each command.
+- [docs/semantics-of-mir.md](docs/semantics-of-mir.md)
+- [docs/example-mir-execution-flow.md](docs/example-mir-execution-flow.md)
+- [docs/dev/adding-intrinsics.md](docs/dev/adding-intrinsics.md)
+- [docs/feature-checklist.md](docs/feature-checklist.md)
+- [Stable-MIR-JSON repository](https://github.com/runtimeverification/stable-mir-json/)
 
-### Supporters
+## Supporters
 
-KMIR / mir-semantics is supported by funding from the following sources:
+KMIR / mir-semantics is supported by funding from:
 - [Polkadot Open Gov](https://polkadot.subsquare.io/referenda/749)
 - Solana