chore: sync feature/p-token with master

.github/workflows/test.yml

@@ -47,12 +47,37 @@ jobs:
         with:
           version: ${{ steps.uv_release.outputs.uv_version }}
       - name: 'Run unit tests'
-        run: make test-unit
+        run: make test-unit PARALLEL=12
 
   integration-tests:
     needs: code-quality-checks
-    name: 'Integration Tests'
+    name: 'Integration Tests ${{ matrix.name }}'
     runs-on: [self-hosted, linux, normal]
+    timeout-minutes: ${{ matrix.timeout }}
+    strategy:
+      fail-fast: true
+      matrix:
+        include:
+          - name: 'LLVM Concrete Tests'
+            test-args: '-k "llvm or test_run_smir_random"'
+            parallel: 12
+            timeout: 30
+          - name: 'Haskell Exec SMIR'
+            test-args: '-k "test_exec_smir and haskell"'
+            parallel: 6
+            timeout: 20
+          - name: 'Haskell Termination'
+            test-args: '-k test_prove_termination'
+            parallel: 6
+            timeout: 20
+          - name: 'Haskell Proofs'
+            test-args: '-k "test_prove and not test_prove_termination"'
+            parallel: 6
+            timeout: 120
+          - name: 'Remainder'
+            test-args: '-k "not llvm and not test_run_smir_random and not test_exec_smir and not test_prove_termination and not test_prove"'
+            parallel: 6
+            timeout: 20
     steps:
       - name: 'Check out code'
         uses: actions/checkout@v4
@@ -66,7 +91,9 @@ jobs:
       - name: 'Build stable-mir-json and kmir'
         run: docker exec --user github-user mir-semantics-ci-${GITHUB_SHA} make build
       - name: 'Run integration tests'
-        run: docker exec --user github-user mir-semantics-ci-${GITHUB_SHA} make test-integration
+        run: |
+          docker exec --user github-user mir-semantics-ci-${GITHUB_SHA} make test-integration \
+            TEST_ARGS='${{ matrix.test-args }}' PARALLEL=${{ matrix.parallel }}
       - name: 'Tear down Docker'
         if: always()
         run: docker stop --time 0 mir-semantics-ci-${GITHUB_SHA}

deps/stable-mir-json_release

@@ -1 +1 @@
-7da8e3bcd0aee1410be9c63cb92dd499f70e8fcc
+885ab4a9f6dd1b5416b57e914082fbb341c89f97

docs/add-module.md

@@ -0,0 +1,90 @@
+# Adding Extra Modules to Proofs
+
+## Overview
+
+The `--add-module` option for `kmir prove` allows including extra K rules in a proof without compiling them into the base K definition. This is useful for proof-specific lemmas, simplification rules, or summarized rules that are only needed for certain proofs.
+
+Rules from the added module are injected into the Haskell backend at prove time, alongside the SMIR-generated function equations.
+
+## Usage
+
+### K source files (`.k` or `.md`)
+
+To include rules from a K source file, use the `FILE:MODULE` format:
+
+```bash
+kmir prove test.rs --add-module lemmas.k:MY-LEMMAS
+kmir prove test.rs --add-module lemmas.md:MY-LEMMAS
+```
+
+The file is parsed against the compiled K definition using `kprove --dry-run`. The named module is extracted and its rules are converted to Kore axioms and added to the proof.
+
+If the file contains multiple modules, only the named module's rules are included. For example, given a file with modules `HELPERS` and `MY-LEMMAS`:
+
+```bash
+# Only rules from MY-LEMMAS are included
+kmir prove test.rs --add-module lemmas.k:MY-LEMMAS
+```
+
+### Pre-exported JSON files
+
+To include rules from a JSON module file (generated by `kmir show --to-module`):
+
+```bash
+kmir prove test.rs --add-module module.json
+```
+
+No module name is needed because JSON files are expected to contain exactly one serialized module (as produced by `--to-module`). Multi-module JSON inputs are not supported.
+
+## Module file requirements
+
+### K source files
+
+- The file must have a `.k` or `.md` extension.
+- The module can `imports` other modules that are already in the compiled definition. However, it must not `requires` files that would conflict with the compiled definition (i.e., do not re-require files already compiled in).
+
+For simple rules the dynamically loading pipeline should work reliably. However, there are some known limitations that restrict the kind of rules that can be expressed in a dynamically loaded module. We plan to address them in the future.
+
+### JSON files
+
+- The file must have a `.json` extension.
+- The file must contain a serialized `KFlatModule` (as produced by `kmir show --to-module output.json`).
+
+## Limitations
+
+The dynamic module loading pipeline has known limitations with complex rules. See the summary below, that includes a non-exhaustive list of the identified issues:
+
+| Limitation | Description | Workaround |
+|-----------|-------------|------------|
+| Limited syntax declarations | `kprove` rejects `syntax` productions in proof modules other than for tokens for existing sorts | Compile syntax into the base definition |
+| No `#as` patterns | pyk's `krule_to_kore` does not support `KAs` | Duplicate the matched pattern on the RHS |
+| Function rules may fail | The booster may reject dynamically-added function rules | Compile function rules into the base definition |
+| Sort injection issues | Complex rules with subsort relationships may crash the booster | Compile such rules into the base definition |
+
+## Examples
+
+### Simple simplification lemma
+
+```k
+// lemma.k
+module MY-SIMPLIFICATION
+    imports INT
+
+    rule [zero-add]: 0 +Int X => X [simplification]
+
+endmodule
+```
+
+```bash
+kmir prove test.rs --add-module lemma.k:MY-SIMPLIFICATION
+```
+
+### Proof summary from a previous run
+
+```bash
+# Export a proof node transition as a module
+kmir show proof-id --to-module summary.json --proof-dir ./proofs
+
+# Use it in a new proof
+kmir prove test.rs --add-module summary.json
+```

flake.nix

@@ -6,7 +6,7 @@
 
     flake-utils.url = "github:numtide/flake-utils";
 
-    stable-mir-json-flake.url = "github:runtimeverification/stable-mir-json/7da8e3bcd0aee1410be9c63cb92dd499f70e8fcc";
+    stable-mir-json-flake.url = "github:runtimeverification/stable-mir-json/885ab4a9f6dd1b5416b57e914082fbb341c89f97";
     stable-mir-json-flake = {
       inputs.nixpkgs.follows = "nixpkgs";
       inputs.flake-utils.follows = "flake-utils";

kmir/src/kmir/__init__.py

@@ -2,4 +2,4 @@
 from typing import Final
 
 __version__: Final = version('kmir')
-__smir_version__: Final = '7da8e3bcd0aee1410be9c63cb92dd499f70e8fcc'
+__smir_version__: Final = '885ab4a9f6dd1b5416b57e914082fbb341c89f97'

kmir/src/kmir/__main__.py

@@ -23,6 +23,7 @@
     LinkOpts,
     ProveOpts,
     PruneOpts,
+    ReduceOpts,
     RunOpts,
     SectionEdgeOpts,
     ShowOpts,
@@ -251,6 +252,17 @@ def _kmir_link(opts: LinkOpts) -> None:
     result.dump(opts.output_file)
 
 
+def _kmir_reduce(opts: ReduceOpts) -> None:
+    smir_info = SMIRInfo.from_file(opts.smir_file)
+    original = len(smir_info.items)
+    reduced = smir_info.reduce_to(opts.roots)
+    reduced.dump(opts.output_file)
+    _LOGGER.info(
+        f'Reduced {original} -> {len(reduced.items)} items'
+        f' ({original - len(reduced.items)} pruned), written to {opts.output_file}'
+    )
+
+
 def kmir(args: Sequence[str]) -> None:
     ns = _arg_parser().parse_args(args)
     opts = _parse_args(ns)
@@ -272,6 +284,8 @@ def kmir(args: Sequence[str]) -> None:
             _kmir_prove(opts)
         case LinkOpts():
             _kmir_link(opts)
+        case ReduceOpts():
+            _kmir_reduce(opts)
         case _:
             raise AssertionError()
 
@@ -555,9 +569,9 @@ def _arg_parser() -> ArgumentParser:
     )
     prove_parser.add_argument(
         '--add-module',
-        type=Path,
-        metavar='FILE',
-        help='K module file to include (.json format from --to-module)',
+        type=str,
+        metavar='MODULE',
+        help='K module to include. Formats: FILE.k:MODULE or FILE.md:MODULE (K source), FILE.json (from --to-module). See docs/add-module.md for details.',
     )
     prove_parser.add_argument(
         '--max-workers', metavar='N', type=int, help='Maximum number of workers for parallel exploration'
@@ -575,6 +589,27 @@ def _arg_parser() -> ArgumentParser:
         default='linker_output.smir.json',
     )
 
+    reduce_parser = command_parser.add_parser(
+        'reduce',
+        help='Reduce SMIR to functions reachable from given roots',
+        parents=[kcli_args.logging_args],
+    )
+    reduce_parser.add_argument('smir_file', metavar='SMIR_JSON', help='SMIR JSON file to reduce')
+    reduce_parser.add_argument(
+        '--roots',
+        '-r',
+        required=True,
+        metavar='ROOTS',
+        help='Comma-separated root function names, or @file for newline-separated file',
+    )
+    reduce_parser.add_argument(
+        '--output-file',
+        '-o',
+        metavar='FILE',
+        help='Output file (default: reduced.smir.json)',
+        default='reduced.smir.json',
+    )
+
     return parser
 
 
@@ -677,6 +712,12 @@ def _parse_args(ns: Namespace) -> KMirOpts:
                 smir_files=ns.smir_files,
                 output_file=ns.output_file,
             )
+        case 'reduce':
+            return ReduceOpts(
+                smir_file=ns.smir_file,
+                roots=ns.roots,
+                output_file=ns.output_file,
+            )
         case _:
             raise AssertionError()
 

kmir/src/kmir/_prove.py

@@ -82,7 +82,6 @@ def _prove(opts: ProveOpts, target_path: Path, label: str) -> APRProof:
             if 'MonoItemFn' in item['mono_item_kind'] and item['mono_item_kind']['MonoItemFn'].get('body') is None
         ]
         has_missing = len(missing_body_syms) > 0
-        _LOGGER.info(f'Reduced items table size {len(smir_info.items)}')
         if has_missing:
             _LOGGER.info(f'missing-bodies-present={has_missing} count={len(missing_body_syms)}')
             _LOGGER.debug(f'Missing-body function symbols (first 5): {missing_body_syms[:5]}')