Updates from master

.github/workflows/update-dependencies.yml

@@ -49,7 +49,8 @@ jobs:
           git fetch --all
           git checkout "${VERSION}"
           cd ../..
-          git add deps/stable-mir-json
+          sed -i 's!__smir_version__: Final = '"'[0-9a-f]*'"'!__smir_version__: Final = '"'${VERSION}'"'!' kmir/src/kmir/__init__.py
+          git add deps/stable-mir-json kmir/src/kmir/__init__.py
           git commit -m "deps/stable-mir-json: sync submodule ${VERSION}" || true
       - name: 'Update Nix flake inputs'
         run: |

deps/stable-mir-json_release

@@ -1 +1 @@
-626e8fed0470078c4d980b6b5b503a3aceb355ec
+a5b714d89d0c12c7f4b00602a95ad2d3a34530f0

deps/uv2nix

@@ -1 +1 @@
-4cca323a547a1aaa9b94929c4901bed5343eafe8
+9d357f0d2ce6f5f35ec7959d7e704452352eb4da

deps/uv_release

@@ -1 +1 @@
-0.9.14
+0.9.22

flake.nix

@@ -6,7 +6,7 @@
 
     flake-utils.url = "github:numtide/flake-utils";
 
-    stable-mir-json-flake.url = "github:runtimeverification/stable-mir-json/626e8fed0470078c4d980b6b5b503a3aceb355ec";
+    stable-mir-json-flake.url = "github:runtimeverification/stable-mir-json/a5b714d89d0c12c7f4b00602a95ad2d3a34530f0";
     stable-mir-json-flake = {
       inputs.nixpkgs.follows = "nixpkgs";
       inputs.flake-utils.follows = "flake-utils";
@@ -18,7 +18,7 @@
       inputs.nixpkgs.follows = "nixpkgs";
     };
 
-    uv2nix.url = "github:pyproject-nix/uv2nix/4cca323a547a1aaa9b94929c4901bed5343eafe8";
+    uv2nix.url = "github:pyproject-nix/uv2nix/9d357f0d2ce6f5f35ec7959d7e704452352eb4da";
     # uv2nix requires a newer version of nixpkgs
     # therefore, we pin uv2nix specifically to a newer version of nixpkgs
     # until we replaced our stale version of nixpkgs with an upstream one as well

kmir/src/kmir/__init__.py

@@ -1,3 +1,5 @@
+from importlib.metadata import version
 from typing import Final
 
-VERSION: Final = '0.3.181'
+__version__: Final = version('kmir')
+__smir_version__: Final = 'a5b714d89d0c12c7f4b00602a95ad2d3a34530f0'

kmir/src/kmir/__main__.py

@@ -10,11 +10,11 @@
 from pyk.cli.args import KCLIArgs
 from pyk.cterm.show import CTermShow
 from pyk.kast.pretty import PrettyPrinter
+from pyk.kdist import kdist
 from pyk.proof.reachability import APRProof
 from pyk.proof.show import APRProofShow
 from pyk.proof.tui import APRProofViewer
 
-from .build import HASKELL_DEF_DIR, LLVM_LIB_DIR
 from .cargo import CargoProject
 from .kmir import KMIR, KMIRAPRNodePrinter
 from .linker import link
@@ -54,7 +54,14 @@ def _kmir_run(opts: RunOpts) -> None:
         smir_info = cargo.smir_for_project(clean=False)
 
     def run(target_dir: Path):
-        kmir = KMIR.from_kompiled_kore(smir_info, symbolic=opts.haskell_backend, target_dir=target_dir)
+        kmir = KMIR.from_kompiled_kore(
+            smir_info,
+            target_dir=target_dir,
+            symbolic=opts.symbolic,
+            haskell_target=opts.haskell_target,
+            llvm_lib_target=opts.llvm_lib_target,
+            llvm_target=opts.llvm_target,
+        )
         result = kmir.run_smir(smir_info, start_symbol=opts.start_symbol, depth=opts.depth)
         print(kmir.kore_to_pretty(result))
 
@@ -73,7 +80,10 @@ def _kmir_prove_rs(opts: ProveRSOpts) -> None:
 
 
 def _kmir_view(opts: ViewOpts) -> None:
-    kmir = KMIR(HASKELL_DEF_DIR, LLVM_LIB_DIR)
+    kmir = KMIR(
+        definition_dir=kdist.which(opts.haskell_target or 'mir-semantics.haskell'),
+        llvm_library_dir=kdist.which(opts.llvm_lib_target or 'mir-semantics.llvm-library'),
+    )
     proof = APRProof.read_proof_data(opts.proof_dir, opts.id)
     printer = PrettyPrinter(kmir.definition)
     omit_labels = ('<currentBody>',) if opts.omit_current_body else ()
@@ -84,14 +94,53 @@ def _kmir_view(opts: ViewOpts) -> None:
     viewer.run()
 
 
+def _write_to_module(kmir: KMIR, proof: APRProof, to_module_path: Path) -> None:
+    """Write proof KCFG as a K module to the specified path."""
+    import json
+
+    from pyk.kast.manip import remove_generated_cells
+    from pyk.kast.outer import KRule
+
+    # Generate K module using KCFG.to_module with defunc_with for proper function inlining
+    module_name = proof.id.upper().replace('.', '-').replace('_', '-') + '-SUMMARY'
+    k_module = proof.kcfg.to_module(module_name=module_name, defunc_with=kmir.definition)
+
+    if to_module_path.suffix == '.json':
+        # JSON format for --add-module: keep <generatedTop> for Kore conversion
+        # Note: We don't use minimize_rule_like here because it creates partial configs
+        # with dots that cannot be converted back to Kore
+        to_module_path.write_text(json.dumps(k_module.to_dict(), indent=2))
+    else:
+        # K text format for human readability: remove <generatedTop> and <generatedCounter>
+        def _process_sentence(sent):  # type: ignore[no-untyped-def]
+            if isinstance(sent, KRule):
+                sent = sent.let(body=remove_generated_cells(sent.body))
+            return sent
+
+        k_module_readable = k_module.let(sentences=[_process_sentence(sent) for sent in k_module.sentences])
+        k_module_text = kmir.pretty_print(k_module_readable)
+        to_module_path.write_text(k_module_text)
+    _LOGGER.info(f'Module written to: {to_module_path}')
+
+
 def _kmir_show(opts: ShowOpts) -> None:
     from pyk.kast.pretty import PrettyPrinter
 
     from .kprint import KMIRPrettyPrinter
 
-    kmir = KMIR(HASKELL_DEF_DIR, LLVM_LIB_DIR)
+    kmir = KMIR(
+        definition_dir=kdist.which(opts.haskell_target or 'mir-semantics.haskell'),
+        llvm_library_dir=kdist.which(opts.llvm_lib_target or 'mir-semantics.llvm-library'),
+    )
     proof = APRProof.read_proof_data(opts.proof_dir, opts.id)
 
+    # Minimize proof KCFG if requested
+    if opts.minimize_proof:
+        _LOGGER.info('Minimizing proof KCFG...')
+        proof.minimize_kcfg()
+        proof.write_proof_data()
+        _LOGGER.info('Proof KCFG minimized and saved')
+
     # Use custom KMIR printer by default, switch to standard printer if requested
     if opts.use_default_printer:
         printer = PrettyPrinter(kmir.definition)
@@ -119,6 +168,7 @@ def _kmir_show(opts: ShowOpts) -> None:
         nodes=opts.nodes or (),
         node_deltas=effective_node_deltas,
         omit_cells=tuple(all_omit_cells),
+        to_module=opts.to_module is not None,
     )
     if opts.statistics:
         if lines and lines[-1] != '':
@@ -132,7 +182,12 @@ def _kmir_show(opts: ShowOpts) -> None:
             lines.append('')
         lines.extend(render_leaf_k_cells(proof, node_printer.cterm_show))
 
-    print('\n'.join(lines))
+    # Handle --to-module output
+    if opts.to_module:
+        _write_to_module(kmir, proof, opts.to_module)
+        print(f'Module written to: {opts.to_module}')
+    else:
+        print('\n'.join(lines))
 
 
 def _kmir_prune(opts: PruneOpts) -> None:
@@ -156,7 +211,14 @@ def _kmir_section_edge(opts: SectionEdgeOpts) -> None:
 
     smir_info = SMIRInfo.from_file(target_path / 'smir.json')
 
-    kmir = KMIR.from_kompiled_kore(smir_info, symbolic=True, bug_report=opts.bug_report, target_dir=target_path)
+    kmir = KMIR.from_kompiled_kore(
+        smir_info,
+        target_dir=target_path,
+        bug_report=opts.bug_report,
+        symbolic=True,
+        haskell_target=opts.haskell_target,
+        llvm_lib_target=opts.llvm_lib_target,
+    )
 
     source_id, target_id = opts.edge
     _LOGGER.info(f'Attempting to add {opts.sections} sections from node {source_id} to node {target_id}')
@@ -229,7 +291,10 @@ def _arg_parser() -> ArgumentParser:
     run_parser.add_argument(
         '--start-symbol', type=str, metavar='SYMBOL', default='main', help='Symbol name to begin execution from'
     )
-    run_parser.add_argument('--haskell-backend', action='store_true', help='Run with the haskell backend')
+    run_parser.add_argument('--symbolic', action='store_true', help='Run with the symbolic backend')
+    run_parser.add_argument('--haskell-target', metavar='TARGET', help='Haskell target to use')
+    run_parser.add_argument('--llvm-lib-target', metavar='TARGET', help='LLVM lib target to use')
+    run_parser.add_argument('--llvm-target', metavar='TARGET', help='LLVM target to use')
 
     info_parser = command_parser.add_parser(
         'info', help='Show information about a SMIR JSON file', parents=[kcli_args.logging_args]
@@ -239,6 +304,8 @@ def _arg_parser() -> ArgumentParser:
 
     prove_args = ArgumentParser(add_help=False)
     prove_args.add_argument('--proof-dir', metavar='DIR', help='Proof directory')
+    prove_args.add_argument('--haskell-target', metavar='TARGET', help='Haskell target to use')
+    prove_args.add_argument('--llvm-lib-target', metavar='TARGET', help='LLVM lib target to use')
     prove_args.add_argument('--bug-report', metavar='PATH', help='path to optional bug report')
     prove_args.add_argument('--max-depth', metavar='DEPTH', type=int, help='max steps to take between nodes in kcfg')
     prove_args.add_argument(
@@ -370,6 +437,8 @@ def _arg_parser() -> ArgumentParser:
         action='store_false',
         help='Display the <currentBody> cell completely.',
     )
+    display_args.add_argument('--haskell-target', metavar='TARGET', help='Haskell target to use')
+    display_args.add_argument('--llvm-lib-target', metavar='TARGET', help='LLVM lib target to use')
 
     show_parser = command_parser.add_parser(
         'show', help='Show proof information', parents=[kcli_args.logging_args, proof_args, display_args]
@@ -410,6 +479,17 @@ def _arg_parser() -> ArgumentParser:
     )
 
     show_parser.add_argument('--rules', metavar='EDGES', help='Comma separated list of edges in format "source:target"')
+    show_parser.add_argument(
+        '--to-module',
+        type=Path,
+        metavar='FILE',
+        help='Output path for K module file (.k for readable, .json for --add-module)',
+    )
+    show_parser.add_argument(
+        '--minimize-proof',
+        action='store_true',
+        help='Minimize the proof KCFG before exporting to module',
+    )
 
     command_parser.add_parser(
         'view', help='View proof information', parents=[kcli_args.logging_args, proof_args, display_args]
@@ -429,6 +509,8 @@ def _arg_parser() -> ArgumentParser:
     section_edge_parser.add_argument(
         '--sections', type=int, default=2, help='Number of sections to make from edge (>= 2, default: 2)'
     )
+    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]
@@ -443,6 +525,12 @@ def _arg_parser() -> ArgumentParser:
     prove_rs_parser.add_argument(
         '--start-symbol', type=str, metavar='SYMBOL', default='main', help='Symbol name to begin execution from'
     )
+    prove_rs_parser.add_argument(
+        '--add-module',
+        type=Path,
+        metavar='FILE',
+        help='K module file to include (.json format from --to-module)',
+    )
 
     link_parser = command_parser.add_parser(
         'link', help='Link together 2 or more SMIR JSON files', parents=[kcli_args.logging_args]
@@ -464,7 +552,7 @@ def _parse_args(ns: Namespace) -> KMirOpts:
                 target_dir=ns.target_dir,
                 depth=ns.depth,
                 start_symbol=ns.start_symbol,
-                haskell_backend=ns.haskell_backend,
+                symbolic=ns.symbolic,
             )
         case 'info':
             return InfoOpts(smir_file=Path(ns.smir_file), types=ns.types)
@@ -474,6 +562,8 @@ def _parse_args(ns: Namespace) -> KMirOpts:
                 id=ns.id,
                 full_printer=ns.full_printer,
                 smir_info=Path(ns.smir_info) if ns.smir_info else None,
+                haskell_target=ns.haskell_target,
+                llvm_lib_target=ns.llvm_lib_target,
                 omit_current_body=ns.omit_current_body,
                 nodes=ns.nodes,
                 node_deltas=ns.node_deltas,
@@ -492,6 +582,8 @@ def _parse_args(ns: Namespace) -> KMirOpts:
                 ns.id,
                 full_printer=ns.full_printer,
                 smir_info=ns.smir_info,
+                haskell_target=ns.haskell_target,
+                llvm_lib_target=ns.llvm_lib_target,
                 omit_current_body=ns.omit_current_body,
             )
         case 'prune':
@@ -501,7 +593,14 @@ def _parse_args(ns: Namespace) -> KMirOpts:
             if ns.proof_dir is None:
                 raise ValueError('Must pass --proof-dir to section-edge command')
             proof_dir = Path(ns.proof_dir)
-            return SectionEdgeOpts(proof_dir, ns.id, ns.edge, ns.sections)
+            return SectionEdgeOpts(
+                proof_dir,
+                ns.id,
+                ns.edge,
+                sections=ns.sections,
+                haskell_target=ns.haskell_target,
+                llvm_lib_target=ns.llvm_lib_target,
+            )
         case 'prove-rs':
             return ProveRSOpts(
                 rs_file=Path(ns.rs_file),
@@ -530,6 +629,7 @@ def _parse_args(ns: Namespace) -> KMirOpts:
                 break_every_terminator=ns.break_every_terminator,
                 break_every_step=ns.break_every_step,
                 terminate_on_thunk=ns.terminate_on_thunk,
+                add_module=ns.add_module,
             )
         case 'link':
             return LinkOpts(

kmir/src/kmir/kdist/mir-semantics/lemmas/kmir-lemmas.md

@@ -79,6 +79,17 @@ Definedness of the list and list elements is also guaranteed.
 For symbolic enum values, the variant index remains unevaluated but the original (symbolic) discriminant can be restored:
 
 ```k
+  syntax Int ::= size(Discriminants) [function, total]
+  rule size(.Discriminants) => 0
+  rule size(discriminant(_) REST) => 1 +Int size(REST)
+
+  rule #Ceil(#lookupDiscrAux(DISCRS:Discriminants, I:Int))
+    => #Ceil(DISCRS)
+     #And #Ceil(I)
+     #And {true #Equals 0 <=Int I}
+     #And {true #Equals I <Int size(DISCRS)}
+    [simplification]
+
   rule #lookupDiscriminant(typeInfoEnumType(_, _, _, _, _), #findVariantIdxAux(DISCR, DISCRS, _IDX)) => DISCR
     requires isOneOf(DISCR, DISCRS)
     [simplification, preserves-definedness, symbolic(DISCR)]