Collapse prove-rs into prove (#986)

dkcumming · web-flow · commit a322781b8eb9 · 2026-03-14T15:29:03.000Z
Collapse `prove-rs` into `prove`: - ProveRSOpts merged into ProveOpts - `kmir prove` is the primary command (`prove-rs` kept as alias for backwards compatibility) - adds `parsed_smir` option for programmatic use (useful for tests with many start symbols like #985)
diff --git a/CLAUDE.md b/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
 
diff --git a/README.md b/README.md
@@ -70,7 +70,7 @@ 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 prove` | 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 |
@@ -82,7 +82,7 @@ Every subcommand supports `--help` for the full option list.
 
 ```bash
 # 1. Run a proof
-uv --project kmir run kmir prove-rs program.rs --proof-dir ./proofs --verbose
+uv --project kmir run kmir prove 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
@@ -104,27 +104,27 @@ When a proof does not close, the typical cycle is **inspect → refine → re-pr
 
 ```bash
 # Narrow down where things go wrong — break on every function call
-uv --project kmir run kmir prove-rs program.rs --proof-dir ./proofs \
+uv --project kmir run kmir prove 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 \
+uv --project kmir run kmir prove 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
+uv --project kmir run kmir prove 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.json
+uv --project kmir run kmir prove program.rs --proof-dir ./proofs --add-module lemma.json
 ```
 
-Other useful `prove-rs` break flags: `--break-every-step`, `--break-every-terminator`, `--break-on-thunk`, `--terminate-on-thunk`.
+Other useful `prove` break flags: `--break-every-step`, `--break-every-terminator`, `--break-on-thunk`, `--terminate-on-thunk`.
 
 ### Generate Stable MIR JSON manually
 
diff --git a/kmir/src/kmir/__main__.py b/kmir/src/kmir/__main__.py
@@ -21,7 +21,7 @@
 from .options import (
     InfoOpts,
     LinkOpts,
-    ProveRSOpts,
+    ProveOpts,
     PruneOpts,
     RunOpts,
     SectionEdgeOpts,
@@ -72,8 +72,8 @@ def run(target_dir: Path):
             run(target_dir=Path(target_dir))
 
 
-def _kmir_prove_rs(opts: ProveRSOpts) -> None:
-    proof = KMIR.prove_rs(opts)
+def _kmir_prove(opts: ProveOpts) -> None:
+    proof = KMIR.prove_program(opts)
     print(str(proof.summary))
     if not proof.passed:
         sys.exit(1)
@@ -268,8 +268,8 @@ def kmir(args: Sequence[str]) -> None:
             _kmir_prune(opts)
         case SectionEdgeOpts():
             _kmir_section_edge(opts)
-        case ProveRSOpts():
-            _kmir_prove_rs(opts)
+        case ProveOpts():
+            _kmir_prove(opts)
         case LinkOpts():
             _kmir_link(opts)
         case _:
@@ -542,26 +542,24 @@ def _arg_parser() -> ArgumentParser:
     section_edge_parser.add_argument('--haskell-target', metavar='TARGET', help='Haskell target to use')
     section_edge_parser.add_argument('--llvm-lib-target', metavar='TARGET', help='LLVM lib target to use')
 
-    prove_rs_parser = command_parser.add_parser(
-        'prove-rs', help='Prove a rust program', parents=[kcli_args.logging_args, prove_args]
+    prove_parser = command_parser.add_parser(
+        'prove', help='Prove a Rust program', aliases=['prove-rs'], parents=[kcli_args.logging_args, prove_args]
     )
-    prove_rs_parser.add_argument(
-        'rs_file', type=Path, metavar='FILE', help='Rust file with the spec function (e.g. main)'
-    )
-    prove_rs_parser.add_argument(
+    prove_parser.add_argument('rs_file', type=Path, metavar='FILE', help='Rust file with the spec function (e.g. main)')
+    prove_parser.add_argument(
         '--save-smir', action='store_true', help='Do not delete the intermediate generated SMIR JSON file.'
     )
-    prove_rs_parser.add_argument('--smir', action='store_true', help='Treat the input file as a smir json.')
-    prove_rs_parser.add_argument(
+    prove_parser.add_argument('--smir', action='store_true', help='Treat the input file as a smir json.')
+    prove_parser.add_argument(
         '--start-symbol', type=str, metavar='SYMBOL', default='main', help='Symbol name to begin execution from'
     )
-    prove_rs_parser.add_argument(
+    prove_parser.add_argument(
         '--add-module',
         type=Path,
         metavar='FILE',
         help='K module file to include (.json format from --to-module)',
     )
-    prove_rs_parser.add_argument(
+    prove_parser.add_argument(
         '--max-workers', metavar='N', type=int, help='Maximum number of workers for parallel exploration'
     )
 
@@ -640,8 +638,8 @@ def _parse_args(ns: Namespace) -> KMirOpts:
                 haskell_target=ns.haskell_target,
                 llvm_lib_target=ns.llvm_lib_target,
             )
-        case 'prove-rs':
-            return ProveRSOpts(
+        case 'prove' | 'prove-rs':
+            return ProveOpts(
                 rs_file=Path(ns.rs_file),
                 proof_dir=ns.proof_dir,
                 haskell_target=ns.haskell_target,
diff --git a/kmir/src/kmir/_prove.py b/kmir/src/kmir/_prove.py
@@ -25,13 +25,13 @@
 
     from pyk.kast.inner import KInner
 
-    from .options import ProveRSOpts
+    from .options import ProveOpts
 
 
 _LOGGER: Final = logging.getLogger(__name__)
 
 
-def prove_rs(opts: ProveRSOpts) -> APRProof:
+def prove(opts: ProveOpts) -> APRProof:
     if not opts.rs_file.is_file():
         raise ValueError(f'Input file does not exist: {opts.rs_file}')
 
@@ -42,14 +42,14 @@ def prove_rs(opts: ProveRSOpts) -> APRProof:
 
     if opts.proof_dir is not None:
         target_path = opts.proof_dir / label
-        return _prove_rs(opts, target_path, label)
+        return _prove(opts, target_path, label)
 
     with tempfile.TemporaryDirectory() as tmp_dir:
         target_path = Path(tmp_dir)
-        return _prove_rs(opts, target_path, label)
+        return _prove(opts, target_path, label)
 
 
-def _prove_rs(opts: ProveRSOpts, target_path: Path, label: str) -> APRProof:
+def _prove(opts: ProveOpts, target_path: Path, label: str) -> APRProof:
     if not opts.reload and opts.proof_dir is not None and APRProof.proof_data_exists(label, opts.proof_dir):
         _LOGGER.info(f'Reading proof from disc: {opts.proof_dir}, {label}')
         proof = APRProof.read_proof_data(opts.proof_dir, label)
@@ -67,7 +67,9 @@ def _prove_rs(opts: ProveRSOpts, target_path: Path, label: str) -> APRProof:
         )
     else:
         _LOGGER.info(f'Constructing initial proof: {label}')
-        if opts.smir:
+        if opts.parsed_smir is not None:
+            smir_info = SMIRInfo(opts.parsed_smir)
+        elif opts.smir:
             smir_info = SMIRInfo.from_file(opts.rs_file)
         else:
             smir_info = SMIRInfo(cargo_get_smir_json(opts.rs_file, save_smir=opts.save_smir))
@@ -138,7 +140,7 @@ def _prove_parallel(
     kmir: KMIR,
     proof: APRProof,
     *,
-    opts: ProveRSOpts,
+    opts: ProveOpts,
     label: str,
     cut_point_rules: list[str],
 ) -> None:
@@ -192,7 +194,7 @@ def _prove_sequential(
     kmir: KMIR,
     proof: APRProof,
     *,
-    opts: ProveRSOpts,
+    opts: ProveOpts,
     label: str,
     cut_point_rules: list[str],
 ) -> None:
diff --git a/kmir/src/kmir/kmir.py b/kmir/src/kmir/kmir.py
@@ -33,7 +33,7 @@
     from pyk.proof.reachability import APRProof
     from pyk.utils import BugReport
 
-    from .options import DisplayOpts, ProveRSOpts
+    from .options import DisplayOpts, ProveOpts
 
 
 _LOGGER: Final = logging.getLogger(__name__)
@@ -121,10 +121,10 @@ def run_smir(
         return result
 
     @staticmethod
-    def prove_rs(opts: ProveRSOpts) -> APRProof:
-        from ._prove import prove_rs
+    def prove_program(opts: ProveOpts) -> APRProof:
+        from ._prove import prove
 
-        return prove_rs(opts)
+        return prove(opts)
 
 
 class KMIRSemantics(DefaultSemantics):
diff --git a/kmir/src/kmir/options.py b/kmir/src/kmir/options.py
@@ -61,15 +61,22 @@ class ProofOpts(KMirOpts):
 
 @dataclass
 class ProveOpts(KMirOpts):
+    rs_file: Path
     proof_dir: Path | None
     haskell_target: str | None
     llvm_lib_target: str | None
     bug_report: Path | None
     max_depth: int | None
     max_iterations: int | None
+    max_workers: int | None
     reload: bool
     fail_fast: bool
     maintenance_rate: int
+    save_smir: bool
+    smir: bool
+    parsed_smir: dict | None
+    start_symbol: str
+    add_module: Path | None
     break_on_calls: bool
     break_on_function_calls: bool
     break_on_intrinsic_calls: bool
@@ -87,71 +94,6 @@ class ProveOpts(KMirOpts):
     terminate_on_thunk: bool
     break_on_function: list[str]
 
-    def __init__(
-        self,
-        *,
-        proof_dir: Path | str | None = None,
-        haskell_target: str | None = None,
-        llvm_lib_target: str | None = None,
-        bug_report: Path | None = None,
-        max_depth: int | None = None,
-        max_iterations: int | None = None,
-        reload: bool = False,
-        fail_fast: bool = False,
-        maintenance_rate: int = 1,
-        break_on_calls: bool = False,
-        break_on_function_calls: bool = False,
-        break_on_intrinsic_calls: bool = False,
-        break_on_thunk: bool = False,
-        break_every_statement: bool = False,
-        break_on_terminator_goto: bool = False,
-        break_on_terminator_switch_int: bool = False,
-        break_on_terminator_return: bool = False,
-        break_on_terminator_call: bool = False,
-        break_on_terminator_assert: bool = False,
-        break_on_terminator_drop: bool = False,
-        break_on_terminator_unreachable: bool = False,
-        break_every_terminator: bool = False,
-        break_every_step: bool = False,
-        terminate_on_thunk: bool = False,
-        break_on_function: list[str] | None = None,
-    ) -> None:
-        self.proof_dir = Path(proof_dir).resolve() if proof_dir is not None else None
-        self.haskell_target = haskell_target
-        self.llvm_lib_target = llvm_lib_target
-        self.bug_report = bug_report
-        self.max_depth = max_depth
-        self.max_iterations = max_iterations
-        self.reload = reload
-        self.fail_fast = fail_fast
-        self.maintenance_rate = maintenance_rate
-        self.break_on_calls = break_on_calls
-        self.break_on_function_calls = break_on_function_calls
-        self.break_on_intrinsic_calls = break_on_intrinsic_calls
-        self.break_on_thunk = break_on_thunk
-        self.break_every_statement = break_every_statement
-        self.break_on_terminator_goto = break_on_terminator_goto
-        self.break_on_terminator_switch_int = break_on_terminator_switch_int
-        self.break_on_terminator_return = break_on_terminator_return
-        self.break_on_terminator_call = break_on_terminator_call
-        self.break_on_terminator_assert = break_on_terminator_assert
-        self.break_on_terminator_drop = break_on_terminator_drop
-        self.break_on_terminator_unreachable = break_on_terminator_unreachable
-        self.break_every_terminator = break_every_terminator
-        self.break_every_step = break_every_step
-        self.terminate_on_thunk = terminate_on_thunk
-        self.break_on_function = break_on_function if break_on_function is not None else []
-
-
-@dataclass
-class ProveRSOpts(ProveOpts):
-    rs_file: Path
-    save_smir: bool
-    smir: bool
-    start_symbol: str
-    add_module: Path | None
-    max_workers: int | None
-
     def __init__(
         self,
         rs_file: Path,
@@ -168,6 +110,7 @@ def __init__(
         maintenance_rate: int = 1,
         save_smir: bool = False,
         smir: bool = False,
+        parsed_smir: dict | None = None,
         start_symbol: str = 'main',
         break_on_calls: bool = False,
         break_on_function_calls: bool = False,
@@ -200,6 +143,7 @@ def __init__(
         self.maintenance_rate = maintenance_rate
         self.save_smir = save_smir
         self.smir = smir
+        self.parsed_smir = parsed_smir
         self.start_symbol = start_symbol
         self.break_on_calls = break_on_calls
         self.break_on_function_calls = break_on_function_calls
diff --git a/kmir/src/tests/integration/test_cli.py b/kmir/src/tests/integration/test_cli.py
diff --git a/kmir/src/tests/integration/test_integration.py b/kmir/src/tests/integration/test_integration.py
diff --git a/package/test-package.sh b/package/test-package.sh
