chore: update master changes to feature/p-token

CLAUDE.md

@@ -13,7 +13,7 @@ MIR Semantics provides a K Framework-based formal semantics for Rust's Stable MI
 # Initial setup - install stable-mir-json tool for SMIR generation
 make stable-mir-json
 
-# Build K semantics definitions (required after any K file changes)
+# Build K semantics definitions (required after K file changes)
 make build
 
 # Full build and check

deps/stable-mir-json_release

@@ -1 +1 @@
-b54152a3099c4756c31fea1a126c20167ae42798
+cf0410fba16002276f6fcdc195b7003e145558e9

flake.nix

@@ -6,7 +6,7 @@
 
     flake-utils.url = "github:numtide/flake-utils";
 
-    stable-mir-json-flake.url = "github:runtimeverification/stable-mir-json/b54152a3099c4756c31fea1a126c20167ae42798";
+    stable-mir-json-flake.url = "github:runtimeverification/stable-mir-json/cf0410fba16002276f6fcdc195b7003e145558e9";
     stable-mir-json-flake = {
       inputs.nixpkgs.follows = "nixpkgs";
       inputs.flake-utils.follows = "flake-utils";
@@ -73,15 +73,22 @@
           final: prev:
           let
             rev = self.rev or null;
+            kmir-pyk-pyproject = final.callPackage ./nix/kmir-pyk-pyproject { inherit uv2nix; };
             kmir-pyk = final.callPackage ./nix/kmir-pyk {
-              inherit pyproject-nix pyproject-build-systems uv2nix;
+              inherit pyproject-nix pyproject-build-systems kmir-pyk-pyproject;
               python = final."python${pythonVer}";
+              pyproject-overlays = [ (k-framework.overlays.pyk-pyproject system) ];
             };
             kmir = final.callPackage ./nix/kmir { inherit kmir-pyk rev; };
             kmir-package-test = final.callPackage ./nix/test/package.nix { inherit rev; };
           in
           {
-            inherit kmir-pyk kmir kmir-package-test;
+            inherit
+              kmir-pyk
+              kmir
+              kmir-package-test
+              kmir-pyk-pyproject
+              ;
           };
         pkgs = import nixpkgs {
           inherit system;
@@ -137,5 +144,12 @@
     )
     // {
       overlays.default = final: prev: { inherit (self.packages.${final.system}) kmir; };
+      pyprojectOverlays = {
+        # this pyproject-nix overlay allows for overriding the python packages that are otherwise locked in `uv.lock`
+        # by using this overlay in dependant nix flakes, you ensure that nix overrides also override the python package     
+        pyk-pyproject = system: final: prev: {
+          inherit (self.packages.${system}.kmir-pyk-pyproject.lockFileOverlay final prev) kmir-pyk;
+        };
+      };
     };
 }

kmir/pyproject.toml

@@ -38,7 +38,7 @@ dev = [
     "flake8-type-checking",
     "isort",
     "mypy",
-    "pep8",
+    "pep8-naming",
     "pytest",
     "pytest-cov",
     "pytest-mock",

kmir/src/kmir/decoding.py

@@ -6,7 +6,7 @@
 from pyk.kast.inner import KApply
 from pyk.kast.prelude.string import stringToken
 
-from .alloc import Allocation, AllocInfo, Memory, ProvenanceEntry, ProvenanceMap
+from .alloc import Allocation, AllocInfo, Function, Memory, ProvenanceEntry, ProvenanceMap, Static, VTable
 from .ty import (
     ArbitraryFields,
     ArrayT,
@@ -21,6 +21,7 @@
     RefT,
     Single,
     StrT,
+    StructT,
     UintT,
 )
 from .value import (
@@ -71,6 +72,28 @@ def decode_alloc_or_unable(alloc_info: AllocInfo, types: Mapping[Ty, TypeMetadat
         ):
             data = bytes(n or 0 for n in bytez)
             return _decode_memory_alloc_or_unable(data=data, ptrs=ptrs, ty=ty, types=types)
+        case AllocInfo(
+            ty=_,
+            # `Static` currently only carries `def_id`; we ignore it here.
+            global_alloc=Static(),
+        ):
+            # Static global alloc does not carry raw bytes here; leave as unable-to-decode placeholder
+            return UnableToDecodeValue('Static global allocation not decoded')
+        case AllocInfo(
+            ty=_,
+            global_alloc=Function(
+                instance=_,
+            ),
+        ):
+            # Function alloc currently not decoded to a runtime value
+            return UnableToDecodeValue('Function global allocation not decoded')
+        case AllocInfo(
+            ty=_,
+            # `VTable` carries `ty` and optional `binder`; we ignore both here.
+            global_alloc=VTable(),
+        ):
+            # VTable alloc currently not decoded to a runtime value
+            return UnableToDecodeValue('VTable global allocation not decoded')
         case _:
             raise AssertionError('Unhandled case')
 
@@ -149,6 +172,8 @@ def decode_value(data: bytes, type_info: TypeMetadata, types: Mapping[Ty, TypeMe
             return _decode_int(data, int_ty)
         case ArrayT(elem_ty, length):
             return _decode_array(data, elem_ty, length, types)
+        case StructT(fields=fields, layout=layout):
+            return _decode_struct(data=data, fields=fields, layout=layout, types=types)
         case EnumT(
             discriminants=discriminants,
             fields=fields,
@@ -219,6 +244,28 @@ def _decode_array(
     return RangeValue(elems)
 
 
+def _decode_struct(
+    *,
+    data: bytes,
+    fields: list[Ty],
+    layout: LayoutShape | None,
+    types: Mapping[Ty, TypeMetadata],
+) -> Value:
+    if not layout:
+        raise ValueError('Struct layout not provided')
+
+    offsets = _extract_offsets(layout.fields)
+
+    match layout.variants:
+        case Single(index=0):
+            pass
+        case _:
+            raise ValueError(f'Unexpected layout variants in struct: {layout.variants}')
+
+    field_values = _decode_fields(data=data, tys=fields, offsets=offsets, types=types)
+    return AggregateValue(0, field_values)
+
+
 def _decode_enum(
     *,
     data: bytes,

kmir/src/kmir/kmir.py

@@ -87,45 +87,61 @@ def kcfg_explore(self, label: str | None = None) -> Iterator[KCFGExplore]:
         ) as cts:
             yield KCFGExplore(cts, kcfg_semantics=KMIRSemantics())
 
-    def make_call_config(
+    def _make_concrete_call_config(self, smir_info: SMIRInfo, *, start_symbol: str = 'main') -> KInner:
+        def init_subst() -> dict[str, KInner]:
+            init_config = self.definition.init_config(KSort('GeneratedTopCell'))
+            _, res = split_config_from(init_config)
+            return res
+
+        if not start_symbol in smir_info.function_tys:
+            raise KeyError(f'{start_symbol} not found in program')
+
+        args_info = smir_info.function_arguments[start_symbol]
+        if args_info:
+            raise ValueError(
+                f'Cannot create concrete call configuration for {start_symbol}: function has parameters: {args_info}'
+            )
+
+        # The configuration is the default initial configuration, with the K cell updated with the call terminator
+        # TODO: see if this can be expressed in more simple terms
+        subst = Subst(
+            {
+                **init_subst(),
+                **{
+                    'K_CELL': mk_call_terminator(smir_info.function_tys[start_symbol], len(args_info)),
+                },
+            }
+        )
+        empty_config = self.definition.empty_config(KSort('GeneratedTopCell'))
+        config = subst(empty_config)
+        assert not free_vars(config), f'Config by construction should not have any free variables: {config}'
+        return config
+
+    def _make_symbolic_call_config(
         self,
         smir_info: SMIRInfo,
         *,
         start_symbol: str = 'main',
-        sort: str = 'GeneratedTopCell',
-        init: bool = False,
     ) -> tuple[KInner, list[KInner]]:
         if not start_symbol in smir_info.function_tys:
             raise KeyError(f'{start_symbol} not found in program')
 
         args_info = smir_info.function_arguments[start_symbol]
         locals, constraints = symbolic_locals(smir_info, args_info)
-
-        _subst = {
-            'K_CELL': mk_call_terminator(smir_info.function_tys[start_symbol], len(args_info)),
-            'STACK_CELL': list_empty(),  # FIXME see #560, problems matching a symbolic stack
-            'LOCALS_CELL': list_of(locals),
-        }
-
-        _init_subst: dict[str, KInner] = {}
-        if init:
-            _subst['LOCALS_CELL'] = list_empty()
-            init_config = self.definition.init_config(KSort(sort))
-            _, _init_subst = split_config_from(init_config)
-
-        for key in _init_subst:
-            if key not in _subst:
-                _subst[key] = _init_subst[key]
-
-        subst = Subst(_subst)
-        config = self.definition.empty_config(KSort(sort))
-        return (subst.apply(config), constraints)
+        subst = Subst(
+            {
+                'K_CELL': mk_call_terminator(smir_info.function_tys[start_symbol], len(args_info)),
+                'STACK_CELL': list_empty(),  # FIXME see #560, problems matching a symbolic stack
+                'LOCALS_CELL': list_of(locals),
+            },
+        )
+        empty_config = self.definition.empty_config(KSort('GeneratedTopCell'))
+        config = subst(empty_config)
+        return config, constraints
 
     def run_smir(self, smir_info: SMIRInfo, start_symbol: str = 'main', depth: int | None = None) -> Pattern:
         smir_info = smir_info.reduce_to(start_symbol)
-        init_config, init_constraints = self.make_call_config(smir_info, start_symbol=start_symbol, init=True)
-        if len(free_vars(init_config)) > 0 or len(init_constraints) > 0:
-            raise ValueError(f'Cannot run function with variables: {start_symbol} - {free_vars(init_config)}')
+        init_config = self._make_concrete_call_config(smir_info, start_symbol=start_symbol)
         init_kore = self.kast_to_kore(init_config, KSort('GeneratedTopCell'))
         result = self.run_pattern(init_kore, depth=depth)
         return result
@@ -135,10 +151,9 @@ def apr_proof_from_smir(
         id: str,
         smir_info: SMIRInfo,
         start_symbol: str = 'main',
-        sort: str = 'GeneratedTopCell',
         proof_dir: Path | None = None,
     ) -> APRProof:
-        lhs_config, constraints = self.make_call_config(smir_info, start_symbol=start_symbol, sort=sort)
+        lhs_config, constraints = self._make_symbolic_call_config(smir_info, start_symbol=start_symbol)
         lhs = CTerm(lhs_config, constraints)
 
         var_config, var_subst = split_config_from(lhs_config)
@@ -181,7 +196,18 @@ def prove_rs(opts: ProveRSOpts) -> APRProof:
                     smir_info = SMIRInfo(cargo_get_smir_json(opts.rs_file, save_smir=opts.save_smir))
 
                 smir_info = smir_info.reduce_to(opts.start_symbol)
+                # Report whether the reduced call graph includes any functions without MIR bodies
+                missing_body_syms = [
+                    sym
+                    for sym, item in smir_info.items.items()
+                    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]}')
 
                 kmir = KMIR.from_kompiled_kore(
                     smir_info, symbolic=True, bug_report=opts.bug_report, target_dir=str(target_path)

kmir/src/kmir/linker.py

@@ -197,7 +197,7 @@ def apply_offset(info: SMIRInfo, offset: int) -> None:
 
     info._smir['functions'] = [(ty + offset, sym) for ty, sym in info._smir['functions']]
     info._smir['types'] = [
-        (ty + offset, apply_offset_typeInfo(typeInfo, offset)) for ty, typeInfo in info._smir['types']
+        (ty + offset, apply_offset_type_info(type_info, offset)) for ty, type_info in info._smir['types']
     ]
     info._smir['spans'] = [(i + offset, span) for i, span in info._smir['spans']]
 
@@ -208,6 +208,14 @@ def apply_offset(info: SMIRInfo, offset: int) -> None:
         match global_alloc:
             case {'Memory': allocation}:  # global_alloc: Memory, allocation: Allocation
                 apply_offset_provenance(allocation['provenance'], offset)
+            case {'Static': alloc_id}:  # global_alloc: Static
+                alloc['global_alloc']['Static'] = alloc_id + offset
+            case {'Function': _}:  # global_alloc: Function
+                # Quick-compat: leave function instance as-is; not used for offset computations
+                pass
+            case {'VTable': _}:  # global_alloc: VTable
+                # Quick-compat: keep as-is (if present). We do not offset embedded types here.
+                pass
             case _:
                 raise ValueError('Unsupported or invalid GlobalAlloc data: {global_alloc}')
 
@@ -216,7 +224,7 @@ def apply_offset(info: SMIRInfo, offset: int) -> None:
         apply_offset_item(item['mono_item_kind'], offset)
 
 
-def apply_offset_typeInfo(typeinfo: dict, offset: int) -> dict:
+def apply_offset_type_info(typeinfo: dict, offset: int) -> dict:
     # traverses type information, updating all `Ty`-valued fields and `adt_def` fields within
     # returns the updated (i.e., mutated) `typeinfo`` dictionary
     # 'PrimitiveType' in typeinfo:
@@ -249,17 +257,20 @@ def apply_offset_item(item: dict, offset: int) -> None:
     # * traverses function locals and debug information to add `offset` to all `span` fields
     if 'MonoItemFn' in item and 'body' in item['MonoItemFn']:
         body = item['MonoItemFn']['body']
-        for local in body['locals']:
+        if body is None:
+            _LOGGER.warning(f"MonoItemFn {item['MonoItemFn'].get('name', '<unknown>')!r} has no body; skipping offsets")
+            return
+        for local in body.get('locals', []):
             local['ty'] += offset
             local['span'] += offset
-        for block in body['blocks']:
+        for block in body.get('blocks', []):
             for stmt in block['statements']:
                 apply_offset_stmt(stmt['kind'], offset)
                 stmt['span'] += offset
             apply_offset_terminator(block['terminator']['kind'], offset)
             block['terminator']['span'] += offset
         # adjust span in var_debug_info, each item's source_info.span
-        for thing in body['var_debug_info']:
+        for thing in body.get('var_debug_info', []):
             thing['source_info']['span'] += offset
             if 'Constant' in thing['value']:
                 apply_offset_operand({'Constant': thing['value']}, offset)

kmir/src/kmir/parse/parser.py

@@ -449,7 +449,7 @@ def _parse_mir_bytes_json(self, json: JSON, prod: KProduction) -> ParseResult:
             import string
 
             # Characters that need special escaping (using hex encoding)
-            ESCAPE_CHARS = {'\n': '\\x0a', '@': '\\x40', '"': '\\x34'}
+            escape_chars = {'\n': '\\x0a', '@': '\\x40', '"': '\\x34'}
 
             # TODO: Handle uninitialized bytes instead of defaulting to 0
             if all((chr(int(i)) if i is not None else chr(0)) in string.printable for i in json):
@@ -458,8 +458,8 @@ def format_printable_byte(byte_val):
                     if byte_val is None:
                         return '\\x00'
                     char = chr(byte_val)
-                    if char in ESCAPE_CHARS:
-                        return ESCAPE_CHARS[char]
+                    if char in escape_chars:
+                        return escape_chars[char]
                     else:
                         return char