Merging latest master into feature/p-token

CLAUDE.md

@@ -32,7 +32,7 @@ make test-unit
 make test-integration
 
 # Run a single test
-uv --directory kmir run pytest kmir/src/tests/integration/test_prove.py::test_prove_rs -k "test_name"
+uv --directory kmir run pytest kmir/src/tests/integration/test_prove.py::test_prove -k "test_name"
 
 # Generate and parse SMIR for test files
 make smir-parse-tests
@@ -61,7 +61,7 @@ source kmir/.venv/bin/activate
 uv --directory kmir run kmir <command>
 
 # Prove Rust code directly (recommended)
-uv --directory kmir run kmir prove-rs path/to/file.rs --verbose
+uv --directory kmir run kmir prove path/to/file.rs --verbose
 
 # Generate SMIR JSON from Rust
 ./scripts/generate-smir-json.sh file.rs output_dir
@@ -79,7 +79,7 @@ uv --directory kmir run kmir show proof_id --proof-dir ./proof_dir
     - `smir.py` - SMIR JSON parsing and info extraction
     - `kdist/mir-semantics/` - K semantics definitions
   - `src/tests/` - Test suites
-    - `integration/data/prove-rs/` - Rust test programs for prove-rs
+    - `integration/data/prove-rs/` - Rust test programs for prove
     - `integration/data/exec-smir/` - Rust programs for execution tests
 
 ### Key K Semantics Files
@@ -105,17 +105,17 @@ Intrinsic functions (like `black_box`, `raw_eq`) don't have regular function bod
 
 ## Testing Patterns
 
-### prove-rs Tests
+### prove Tests
 Tests in `kmir/src/tests/integration/data/prove-rs/` follow this pattern:
 - Simple Rust programs with assertions
 - File naming: `test-name.rs` (passes), `test-name-fail.rs` (expected to fail)
-- Tests run via `kmir prove-rs` command
+- Tests run via `kmir prove` command
 - Generate SMIR automatically during test execution
 
 ### Adding New Tests
 1. Add Rust file to `prove-rs/` directory
 2. Use assertions to verify behavior
-3. Run with: `uv --directory kmir run kmir prove-rs your-test.rs`
+3. Run with: `uv --directory kmir run kmir prove your-test.rs`
 
 ## Development Workflow
 

Makefile

@@ -56,6 +56,11 @@ test-integration: stable-mir-json build
 	$(UV_RUN) pytest $(TOP_DIR)/kmir/src/tests/integration --maxfail=1 --verbose \
 			--durations=0 --numprocesses=$(PARALLEL) --dist=worksteal $(TEST_ARGS)
 
+.PHONY: test-stable-mir-ui
+test-stable-mir-ui: stable-mir-json build
+	@test -n "$(RUST_DIR_ROOT)" || (echo "RUST_DIR_ROOT is required. Example: RUST_DIR_ROOT=/path/to/rust make test-stable-mir-ui"; exit 2)
+	$(UV_RUN) pytest $(TOP_DIR)/kmir/src/tests/external/test_stable_mir_ui_pass.py --maxfail=1 --verbose $(TEST_ARGS)
+
 # Checks and formatting
 
 format: autoflake isort black nix-fmt