Add show-rule command & docs related to kmir (#642)

## Summary
Adds a new `show-rules` command to KMIR and improves documentation for
MIR semantics analysis.

## Changes

### New Features
- **`kmir show-rules`**: Display rules applied on edges between proof
nodes
- **`generate-smir-json.sh`**: Multi-format SMIR JSON generation
(JSON/DOT/PNG/PDF)
- **Enhanced README**: Comprehensive usage guide with examples and
workflow

### Documentation
- Add MIR execution steps documentation with rule references
- Update all documentation to English for internationalization
- Remove macOS-specific setup instructions

### Technical
- Fix code style issues (quotes, unused variables)
- Update stable-mir-json submodules
- Update .gitignore for new files

## Usage
```bash
# Show rules on edge
kmir show-rules proof_id 1 3 --proof-dir ./proof_dir

# Generate SMIR JSON
./scripts/generate-smir-json.sh your_file.rs . png
```

## Testing
- All code passes formatting checks (flake8, mypy, black)
- Scripts tested with various input formats

---------

Co-authored-by: Daniel Cumming <124537596+dkcumming@users.noreply.github.com>

Author: Stevengre

.gitignore

@@ -4,3 +4,4 @@ __pycache__/
 /deps/.stable-mir-json
 /.vscode/
 kmir/src/tests/integration/data/**/target
+.DS_Store

README.md

@@ -9,40 +9,144 @@ Also included is the `kmir` tool, a python script that acts as a front-end to th
 
 ### KMIR Setup
 
-Pre-requisites: `python >= 3.10`, `pip >= 20.0.2`, `poetry >= 1.3.2`, `gcc >= 11.4.0`, `cargo == nightly-2024-11-29`, `k >= v7.1.205`. To install K, follow the steps available in [K's Quick Start instructions](https://github.com/runtimeverification/k?tab=readme-ov-file#quick-start). 
+Pre-requisites: `python >= 3.10`, `pip >= 20.0.2`, `uv >= 0.7.11`, `gcc >= 11.4.0`, `cargo == nightly-2024-11-29`, `k >= v7.1.205`. To install K, follow the steps available in [K's Quick Start instructions](https://github.com/runtimeverification/k?tab=readme-ov-file#quick-start). 
 
 ```bash
 make build
 ```
 
 Use `make` to run common tasks (see the [Makefile](Makefile) for a complete list of available targets).
 
-For interactive use, spawn a shell with `poetry -C kmir/ shell` (after `poetry -C kmir/ install`), then run an interpreter. Or directly run from `mir-semantics` root with `poetry run -C kmir kmir <COMMAND>`
+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>`
 
 ### Stable-MIR-JSON Setup
 
-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:
+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.
 
-```Rust
+#### Quick Start
+```bash
 git submodule update --init --recursive
 make stable-mir-json
 ```
 
+#### Generating SMIR JSON Files
+
+After setting up stable-mir-json, you can generate SMIR JSON files from Rust source code:
+
+**Using the stable-mir-json tool directly:**
+```bash
+# For single files
+deps/.stable-mir-json/debug.sh -Zno-codegen your_file.rs
+
+# For cargo projects
+RUSTC=deps/.stable-mir-json/debug.sh cargo build
+```
+
+**Using the convenience script:**
+```bash
+# Generate JSON file
+./scripts/generate-smir-json.sh your_file.rs .
+
+# 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
+```
+
 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/).
 
 ## Usage
 
 Use `--help` with each command for more details.
 
-`parse` to parse a Stable MIR JSON file (`*.smir.json`) file to a K AST
+### Basic Commands
+
+**`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
+
+# Run with verbose output
+uv --project kmir run kmir run --file path/to/program.smir.json --verbose
+```
+
+**`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
+
+# Detailed proof with output
+uv --project kmir run kmir prove-rs path/to/program.rs --verbose --proof-dir ./proof_dir
+```
+
+**`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
+```
+
+**`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
+
+# Use default output filename (linker_output.smir.json)
+uv --project kmir run kmir link file1.smir.json file2.smir.json
+```
+
+### Analysis Commands
+
+**`kmir show`** - Display proof information
+```bash
+uv --project kmir run kmir show proof_id --proof-dir ./proof_dir
+```
+
+**`kmir view`** - Detailed view of proof results
+```bash
+uv --project kmir run kmir view proof_id --proof-dir ./proof_dir --verbose
+```
+
+**`kmir show-rules`** - Show rules applied between nodes
+```bash
+uv --project kmir run kmir show-rules proof_id source_node target_node --proof-dir ./proof_dir
+```
+
+### 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
+   uv --project kmir run kmir show proof_id --proof-dir ./proof_dir
+   uv --project kmir run kmir view proof_id --proof-dir ./proof_dir --verbose
+   ```
 
-`kmir run` to run a binary target in your cargo project (or a specific smir json provided with --file). The SMIR JSON will need to have been already built with `stable-mir-json`, or you will need the `RUSTC` environment variable set to your installation of `stable-mir-json`.
+4. **Analyze Rules**:
+   ```bash
+   uv --project kmir run kmir show-rules proof_id 1 3 --proof-dir ./proof_dir
+   ```
 
-`kmir gen-spec` to take a SMIR JSON and create a K specification module that ensures termination of the program.
+### Command Options
 
-`kmir prove run` to run the prover on a spec generated by `gen-spec`.
+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
 
-`kmir prove view` to run the KCFG visualizer and inspect the proof steps.
+For complete options, use `--help` with each command.
 
 ### Supporters
 

deps/stable-mir-json

@@ -1 +1 @@
-62a239d7102b4871a8d24eb921aab3630b7bd3a9
+89a011e5a590635892fffae9ffd16885106c14e3

deps/stable-mir-json_release

@@ -0,0 +1,40 @@
+# MIR Execution Steps
+
+**Last Updated: 2025-08-05**
+
+Execution steps based on `assert_eq.rs`, applying a total of 156 rules, transforming from node 1 to node 3.
+
+## Execution Steps List
+
+### 1. Function Call Initialization Phase
+- [Function Call Start](../kmir/src/kmir/kdist/mir-semantics/kmir.md#L461)
+- [Setup Callee Data](../kmir/src/kmir/kdist/mir-semantics/kmir.md#L494)
+- [Complete Argument Setup](../kmir/src/kmir/kdist/mir-semantics/kmir.md#L519)
+
+### 2. Basic Block Execution Phase
+- [Execute Basic Block](../kmir/src/kmir/kdist/mir-semantics/kmir.md#L256)
+- [Execute Statement Sequence](../kmir/src/kmir/kdist/mir-semantics/kmir.md#L264)
+
+### 3. Statement Execution Phase
+- [Handle Assignment Statement](../kmir/src/kmir/kdist/mir-semantics/kmir.md#L279)
+- [Set Local Variable Value (Hot Rule)](../kmir/src/kmir/kdist/mir-semantics/rt/data.md#L173)
+
+### 4. Operand Processing Phase
+- [Handle RValue Use](../kmir/src/kmir/kdist/mir-semantics/rt/data.md#L608)
+- [Handle Constant Operand](../kmir/src/kmir/kdist/mir-semantics/rt/data.md#L122)
+- [Decode Allocated Constant](../kmir/src/kmir/kdist/mir-semantics/rt/data.md#L1073)
+
+### 5. Arithmetic Operation Phase
+- [Binary Operation Processing](../kmir/src/kmir/kdist/mir-semantics/rt/data.md#L1109)
+- [Binary Operation Result](../kmir/src/kmir/kdist/mir-semantics/rt/data.md#L1174)
+
+### 6. Assertion Check Phase
+- [Assertion Check Start](../kmir/src/kmir/kdist/mir-semantics/kmir.md#L563)
+- [Expectation Check (Hot Rule)](../kmir/src/kmir/kdist/mir-semantics/kmir.md#L568)
+- [Move Operand Processing](../kmir/src/kmir/kdist/mir-semantics/rt/data.md#L154)
+- [Projection Traversal and Move Marking](../kmir/src/kmir/kdist/mir-semantics/rt/data.md#L357)
+- [Expectation Check (Cold Rule)](../kmir/src/kmir/kdist/mir-semantics/kmir.md#L568)
+
+### 7. Control Flow Processing Phase
+- [Assertion Success Processing](../kmir/src/kmir/kdist/mir-semantics/kmir.md#L570)
+- [Execute Target Basic Block](../kmir/src/kmir/kdist/mir-semantics/kmir.md#L245)

docs/example-mir-execution-flow.md

@@ -16,7 +16,7 @@ The _args_, _destination_, _unwind_, and (optional!) _target_ are
 supplied by either the `Terminator` kind `Call` (within a program), or
 unnecessary (when calling `main`).
 
-The execution of a body consists of
+The execution of a function call consists of
 * setting up a stack frame for this call
   - with reserved space for all _locals_: return value, arg.s, and local
     variables

docs/semantics-of-mir.md

@@ -18,7 +18,17 @@
 from .cargo import CargoProject
 from .kmir import KMIR, KMIRAPRNodePrinter
 from .linker import link
-from .options import GenSpecOpts, LinkOpts, ProveRawOpts, ProveRSOpts, PruneOpts, RunOpts, ShowOpts, ViewOpts
+from .options import (
+    GenSpecOpts,
+    LinkOpts,
+    ProveRawOpts,
+    ProveRSOpts,
+    PruneOpts,
+    RunOpts,
+    ShowOpts,
+    ShowRulesOpts,
+    ViewOpts,
+)
 from .parse.parser import parse_json
 from .smir import SMIRInfo
 
@@ -78,7 +88,7 @@ def _kmir_gen_spec(opts: GenSpecOpts) -> None:
     output_file = opts.output_file
     if output_file is None:
         suffixes = ''.join(opts.input_file.suffixes)
-        base = opts.input_file.name.removesuffix(suffixes)
+        base = opts.input_file.name.removesuffix(suffixes).replace('_', '-')
         output_file = Path(f'{base}-spec.k')
 
     module_name = output_file.stem.upper().replace('_', '-')
@@ -131,6 +141,22 @@ def _kmir_show(opts: ShowOpts) -> None:
     print('\n'.join(lines))
 
 
+def _kmir_show_rules(opts: ShowRulesOpts) -> None:
+    """Show rules applied on the edge from source to target node."""
+    proof = APRProof.read_proof_data(opts.proof_dir, opts.id)
+    edge = proof.kcfg.edge(opts.source, opts.target)
+    if edge is None:
+        print(f'Error: No edge found from node {opts.source} to node {opts.target}')
+        return
+    rules = edge.rules
+    print(f'Rules applied on edge {opts.source} -> {opts.target}:')
+    print(f'Total rules: {len(rules)}')
+    print('-' * 80)
+    for rule in rules:
+        print(rule)
+        print('-' * 80)
+
+
 def _kmir_prune(opts: PruneOpts) -> None:
     proof = APRProof.read_proof_data(opts.proof_dir, opts.id)
     pruned_nodes = proof.prune(opts.node_id)
@@ -158,6 +184,8 @@ def kmir(args: Sequence[str]) -> None:
             _kmir_view(opts)
         case ShowOpts():
             _kmir_show(opts)
+        case ShowRulesOpts():
+            _kmir_show_rules(opts)
         case PruneOpts():
             _kmir_prune(opts)
         case ProveRSOpts():
@@ -241,11 +269,17 @@ def _arg_parser() -> ArgumentParser:
     )
 
     command_parser.add_parser(
-        'show', help='Show a saved proof', parents=[kcli_args.logging_args, proof_args, display_args]
+        'show', help='Show proof information', parents=[kcli_args.logging_args, proof_args, display_args]
+    )
+
+    show_rules_parser = command_parser.add_parser(
+        'show-rules', help='Show rules applied on a specific edge', parents=[kcli_args.logging_args, proof_args]
     )
+    show_rules_parser.add_argument('source', type=int, metavar='SOURCE', help='Source node ID')
+    show_rules_parser.add_argument('target', type=int, metavar='TARGET', help='Target node ID')
 
     command_parser.add_parser(
-        'view', help='View a saved proof', parents=[kcli_args.logging_args, proof_args, display_args]
+        'view', help='View proof information', parents=[kcli_args.logging_args, proof_args, display_args]
     )
 
     prune_parser = command_parser.add_parser(
@@ -302,6 +336,21 @@ def _parse_args(ns: Namespace) -> KMirOpts:
                 reload=ns.reload,
                 max_iterations=ns.max_iterations,
             )
+        case 'show':
+            return ShowOpts(
+                proof_dir=Path(ns.proof_dir),
+                id=ns.id,
+                full_printer=ns.full_printer,
+                smir_info=Path(ns.smir_info) if ns.smir_info else None,
+                omit_current_body=ns.omit_current_body,
+            )
+        case 'show-rules':
+            return ShowRulesOpts(
+                proof_dir=Path(ns.proof_dir),
+                id=ns.id,
+                source=ns.source,
+                target=ns.target,
+            )
         case 'view':
             proof_dir = Path(ns.proof_dir)
             return ViewOpts(
@@ -314,15 +363,6 @@ def _parse_args(ns: Namespace) -> KMirOpts:
         case 'prune':
             proof_dir = Path(ns.proof_dir)
             return PruneOpts(proof_dir, ns.id, ns.node_id)
-        case 'show':
-            proof_dir = Path(ns.proof_dir)
-            return ShowOpts(
-                proof_dir,
-                ns.id,
-                full_printer=ns.full_printer,
-                smir_info=ns.smir_info,
-                omit_current_body=ns.omit_current_body,
-            )
         case 'prove-rs':
             return ProveRSOpts(
                 rs_file=Path(ns.rs_file),

kmir/src/kmir/__main__.py

@@ -157,6 +157,24 @@ class ShowOpts(DisplayOpts): ...
 class ViewOpts(DisplayOpts): ...
 
 
+@dataclass
+class ShowRulesOpts(ProofOpts):
+    source: int
+    target: int
+
+    def __init__(
+        self,
+        proof_dir: Path | str,
+        id: str,
+        source: int,
+        target: int,
+    ) -> None:
+        self.proof_dir = Path(proof_dir).resolve() if proof_dir is not None else None
+        self.id = id
+        self.source = source
+        self.target = target
+
+
 @dataclass
 class PruneOpts(ProofOpts):
     node_id: int