Update P-Token branch with latest master

deps/k_release

@@ -1 +1 @@
-7.1.289
+7.1.299

deps/uv2nix

@@ -1 +1 @@
-be511633027f67beee87ab499f7b16d0a2f7eceb
+b6ed0901aec29583532abe65117b18d86a49b617

deps/uv_release

@@ -1 +1 @@
-0.8.15
+0.9.2

flake.nix

@@ -12,13 +12,13 @@
       inputs.flake-utils.follows = "flake-utils";
     };
 
-    k-framework.url = "github:runtimeverification/k/v7.1.289";
+    k-framework.url = "github:runtimeverification/k/v7.1.299";
     k-framework = {
       inputs.flake-utils.follows = "flake-utils";
       inputs.nixpkgs.follows = "nixpkgs";
     };
 
-    uv2nix.url = "github:pyproject-nix/uv2nix/64298e806f4a5f63a51c625edc100348138491aa";
+    uv2nix.url = "github:pyproject-nix/uv2nix/b6ed0901aec29583532abe65117b18d86a49b617";
     # 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
@@ -27,7 +27,7 @@
     nixpkgs-unstable.url = "github:NixOS/nixpkgs/nixos-unstable";
     uv2nix.inputs.nixpkgs.follows = "nixpkgs-unstable";
     # uv2nix.inputs.nixpkgs.follows = "nixpkgs";
-    pyproject-build-systems.url = "github:pyproject-nix/build-system-pkgs/7dba6dbc73120e15b558754c26024f6c93015dd7";
+    pyproject-build-systems.url = "github:pyproject-nix/build-system-pkgs/dbfc0483b5952c6b86e36f8b3afeb9dde30ea4b5";
     pyproject-build-systems = {
       inputs.nixpkgs.follows = "uv2nix/nixpkgs";
       inputs.uv2nix.follows = "uv2nix";

kmir/pyproject.toml

@@ -6,9 +6,9 @@ build-backend = "hatchling.build"
 name = "kmir"
 version = "0.3.181"
 description = ""
-requires-python = "~=3.10"
+requires-python = ">=3.10"
 dependencies = [
-    "kframework==v7.1.289",
+    "kframework==v7.1.299",
     "rust-demangler==1.0",
 ]
 

kmir/src/kmir/__main__.py

@@ -31,7 +31,7 @@
 )
 from .parse.parser import parse_json
 from .smir import SMIRInfo, Ty
-from .utils import render_rules
+from .utils import render_leaf_k_cells, render_rules, render_statistics
 
 if TYPE_CHECKING:
     from argparse import Namespace
@@ -166,9 +166,17 @@ def _kmir_show(opts: ShowOpts) -> None:
         node_deltas=effective_node_deltas,
         omit_cells=tuple(all_omit_cells),
     )
+    if opts.statistics:
+        if lines and lines[-1] != '':
+            lines.append('')
+        lines.extend(render_statistics(proof))
     if effective_rule_edges:
         lines.append('# Rules: ')
         lines.extend(render_rules(proof, effective_rule_edges))
+    if opts.leaves:
+        if lines and lines[-1] != '':
+            lines.append('')
+        lines.extend(render_leaf_k_cells(proof, node_printer.cterm_show))
 
     print('\n'.join(lines))
 
@@ -327,6 +335,16 @@ def _arg_parser() -> ArgumentParser:
         default=False,
         help='Use standard PrettyPrinter instead of custom KMIR printer',
     )
+    show_parser.add_argument(
+        '--statistics',
+        action='store_true',
+        help='Display aggregate statistics about the proof graph',
+    )
+    show_parser.add_argument(
+        '--leaves',
+        action='store_true',
+        help='Print the <k> cell for each leaf node in the proof graph',
+    )
 
     show_parser.add_argument('--rules', metavar='EDGES', help='Comma separated list of edges in format "source:target"')
 
@@ -404,6 +422,8 @@ def _parse_args(ns: Namespace) -> KMirOpts:
                 omit_cells=ns.omit_cells,
                 omit_static_info=ns.omit_static_info,
                 use_default_printer=ns.use_default_printer,
+                statistics=ns.statistics,
+                leaves=ns.leaves,
             )
         case 'view':
             proof_dir = Path(ns.proof_dir)

kmir/src/kmir/alloc.py

@@ -35,7 +35,7 @@ def from_dict(dct: dict[str, Any]) -> GlobalAlloc:
             case {'Memory': _}:
                 return Memory.from_dict(dct)
             case _:
-                raise ValueError('Unsupported or invalid GlobalAlloc data: {dct}')
+                raise ValueError(f'Unsupported or invalid GlobalAlloc data: {dct}')
 
 
 @dataclass