Update dependency: deps/stable-mir-json_release (#947)

rv-jenkins · rv-auditor · github-actions[bot] · web-flow · commit 682df6b2dfec · 2026-03-03T16:39:23.000+10:00
- [stable-mir-json PR 122](https://github.com/runtimeverification/stable-mir-json/pull/122/changes#diff-f3fb88e143d9d90b06c9086e1c660a3e28674c1c1cebf1870de06d73156e3d54R413-R416) Added `Dyn` which needed corresponding K and python productions added to AST - [stable-mir-json PR 129](runtimeverification/stable-mir-json#129) or [131](runtimeverification/stable-mir-json#131) changes closures which do not have corresponding K updates in this PR, proofs `and_then_closure` and `closure_acces_struct` are regressed to failing for now with semantics for correct usage expected to come after merging --------- Co-authored-by: devops <devops@runtimeverification.com> Co-authored-by: github-actions[bot] <github-actions[bot]@users.noreply.github.com> Co-authored-by: Daniel Cumming <124537596+dkcumming@users.noreply.github.com> Co-authored-by: dkcumming <daniel.cumming@runtimeverification.com>
diff --git a/deps/stable-mir-json b/deps/stable-mir-json
@@ -1 +1 @@
-Subproject commit 9a7810914a338dfc2533b04bdb14b19c1943fdb8
+Subproject commit 047ca6ac01786e1b616e13a216d70268b9785e17
diff --git a/deps/stable-mir-json_release b/deps/stable-mir-json_release
@@ -1 +1 @@
-9a7810914a338dfc2533b04bdb14b19c1943fdb8
+047ca6ac01786e1b616e13a216d70268b9785e17
diff --git a/flake.lock b/flake.lock
diff --git a/flake.nix b/flake.nix
@@ -6,7 +6,7 @@
 
     flake-utils.url = "github:numtide/flake-utils";
 
-    stable-mir-json-flake.url = "github:runtimeverification/stable-mir-json/9a7810914a338dfc2533b04bdb14b19c1943fdb8";
+    stable-mir-json-flake.url = "github:runtimeverification/stable-mir-json/047ca6ac01786e1b616e13a216d70268b9785e17";
     stable-mir-json-flake = {
       inputs.nixpkgs.follows = "nixpkgs";
       inputs.flake-utils.follows = "flake-utils";
diff --git a/kmir/src/kmir/__init__.py b/kmir/src/kmir/__init__.py
@@ -2,4 +2,4 @@
 from typing import Final
 
 __version__: Final = version('kmir')
-__smir_version__: Final = '9a7810914a338dfc2533b04bdb14b19c1943fdb8'
+__smir_version__: Final = '047ca6ac01786e1b616e13a216d70268b9785e17'
diff --git a/kmir/src/kmir/kdist/mir-semantics/ty.md b/kmir/src/kmir/kdist/mir-semantics/ty.md
@@ -280,6 +280,8 @@ syntax ExistentialPredicateBinders ::= List {ExistentialPredicateBinder, ""}
                     | typeInfoRefType(Ty)                        [symbol(TypeInfo::RefType)      , group(mir-enum---pointee-type)]
                     | typeInfoTupleType(types: Tys, layout: MaybeLayoutShape)
                                                             [symbol(TypeInfo::TupleType)    , group(mir-enum---types--layout)]
+                    | TypeInfoDynType(name: MIRString, layout: MaybeLayoutShape)
+                                                            [symbol(TypeInfo::DynType)      , group(mir-enum---name--layout)]
                     | typeInfoFunType(MIRString)                 [symbol(TypeInfo::FunType)      , group(mir-enum)]
                     | "typeInfoVoidType"                         [symbol(TypeInfo::VoidType)     , group(mir-enum)]
 
diff --git a/kmir/src/kmir/ty.py b/kmir/src/kmir/ty.py
@@ -675,6 +675,28 @@ def nbytes(self, types: Mapping[Ty, TypeMetadata]) -> int:
                 return size.in_bytes
 
 
+@dataclass
+class DynT(TypeMetadata):
+    name: str
+    layout: LayoutShape | None
+
+    @staticmethod
+    def from_raw(data: Any) -> DynT:
+        match data:
+            case {
+                'DynType': {
+                    'name': name,
+                    'layout': layout,
+                }
+            }:
+                return DynT(
+                    name=name,
+                    layout=LayoutShape.from_raw(layout) if layout is not None else None,
+                )
+            case _:
+                raise _cannot_parse_as('DynT', data)
+
+
 @dataclass
 class FunT(TypeMetadata):
     type_str: str
diff --git a/kmir/src/tests/integration/data/crate-tests/two-crate-bin/crate2::main.expected b/kmir/src/tests/integration/data/crate-tests/two-crate-bin/crate2::main.expected
@@ -2,7 +2,7 @@
 ┌─ 1 (root, init)
 │   #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
 │
-│  (736 steps)
+│  (740 steps)
 ├─ 3 (terminal)
 │   #EndProgram ~> .K
 │
diff --git a/kmir/src/tests/integration/data/prove-rs/and_then_closure-fail.rs b/kmir/src/tests/integration/data/prove-rs/and_then_closure-fail.rs
diff --git a/kmir/src/tests/integration/data/prove-rs/closure_access_struct-fail.rs b/kmir/src/tests/integration/data/prove-rs/closure_access_struct-fail.rs
diff --git a/kmir/src/tests/integration/data/prove-rs/show/and_then_closure-fail.main.expected b/kmir/src/tests/integration/data/prove-rs/show/and_then_closure-fail.main.expected
@@ -0,0 +1,15 @@
+
+┌─ 1 (root, init)
+│   #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
+│   span: 0
+│
+│  (142 steps)
+└─ 3 (stuck, leaf)
+    #traverseProjection ( toLocal ( 2 ) , Aggregate ( variantIdx ( 0 ) , ListItem (
+    span: 157
+
+
+┌─ 2 (root, leaf, target, terminal)
+│   #EndProgram ~> .K
+
+
diff --git a/kmir/src/tests/integration/data/prove-rs/show/closure_access_struct-fail.main.expected b/kmir/src/tests/integration/data/prove-rs/show/closure_access_struct-fail.main.expected
@@ -0,0 +1,15 @@
+
+┌─ 1 (root, init)
+│   #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
+│   span: 0
+│
+│  (196 steps)
+└─ 3 (stuck, leaf)
+    #traverseProjection ( toLocal ( 2 ) , Aggregate ( variantIdx ( 0 ) , ListItem (
+    span: 125
+
+
+┌─ 2 (root, leaf, target, terminal)
+│   #EndProgram ~> .K
+
+
diff --git a/kmir/src/tests/integration/test_integration.py b/kmir/src/tests/integration/test_integration.py
@@ -63,6 +63,8 @@
     'test_offset_from-fail',
     'ref-ptr-cast-elem-fail',
     'ref-ptr-cast-elem-offset-fail',
+    'and_then_closure-fail',
+    'closure_access_struct-fail',
 ]
 
 
diff --git a/kmir/uv.lock b/kmir/uv.lock

Original file line number	Diff line number	Diff line change
`@@ -1 +1 @@`
`1`		`-9a7810914a338dfc2533b04bdb14b19c1943fdb8`
	`1`	`+047ca6ac01786e1b616e13a216d70268b9785e17`