crucible-mir: Support constant trait objects

This bumps the `mir-json` submodule to bring in the changes from
GaloisInc/mir-json#240. It also adds `crucible-mir`
support for parsing and translating constant trait object values. (See
GaloisInc/mir-json#237 for the motivation.)

Because these MIR JSON changes require bumping the schema version, we must also
do the same on the `crucible-mir` side.

Author: RyanGlScott

crucible-mir/CHANGELOG.md

@@ -1,5 +1,11 @@
 # next
 
+This release supports [version
+9](https://github.com/GaloisInc/mir-json/blob/master/SCHEMA_CHANGELOG.md#9) of
+`mir-json`'s schema.
+
+* Support translating constant trait object values.
+
 # 0.6 -- 2026-01-29
 
 This release supports [version

crucible-mir/src/Mir/JSON.hs

@@ -620,6 +620,12 @@ instance FromJSON ConstVal where
         Just (String "fn_ptr") ->
             ConstFnPtr <$> v .: "def_id"
 
+        Just (String "trait_object") ->
+            ConstTraitObject
+              <$> v .: "def_id"
+              <*> v .: "trait_id"
+              <*> v .: "vtable"
+
         o -> do
             fail $ "parseJSON - bad rendered constant kind: " ++ show o
 

crucible-mir/src/Mir/Mir.hs

@@ -641,6 +641,11 @@ data ConstVal =
   | ConstEnum Int [ConstVal]
   | ConstUnion
   | ConstFnPtr DefId
+  -- | A reference to a trait object (e.g., @&dyn Trait@). The 'DefId' is the
+  -- allocation backing the reference, the 'TraitName' is the name of the
+  -- trait object's principal trait, and the 'VtableName' is the name of the
+  -- trait object's vtable.
+  | ConstTraitObject DefId TraitName VtableName
   deriving (Show,Eq, Ord, Generic)
 
 data AggregateKind =

crucible-mir/src/Mir/PP.hs

@@ -394,6 +394,8 @@ instance Pretty ConstVal where
     pretty ConstUnion = pretty "union"
     pretty (ConstSliceRef a _len) = pretty "&" <> pr_id a
     pretty (ConstFnPtr i)   = pretty "fn_ptr" <> brackets (pretty i)
+    pretty (ConstTraitObject a trait vtable) =
+      pretty "&trait_object" <> list (map pr_id [a, trait, vtable])
 
 instance Pretty AggregateKind where
     pretty (AKArray t) = brackets (pretty t)

crucible-mir/src/Mir/ParseTranslate.hs

@@ -48,7 +48,7 @@ import Debug.Trace
 -- If you update the supported mir-json schema version below, make sure to also
 -- update the crux-mir README accordingly.
 supportedSchemaVersion :: Word64
-supportedSchemaVersion = 8
+supportedSchemaVersion = 9
 
 -- | Parse a MIR JSON file to a 'Collection'. If parsing fails, attempt to give
 -- a more informative error message if the MIR JSON schema version is

crucible-mir/src/Mir/Trans.hs

@@ -227,6 +227,10 @@ transConstVal ty _ ConstZST = initialValue ty >>= \case
     Just x -> return x
     Nothing -> mirFail $
         "failed to evaluate ZST constant of type " ++ show ty ++ " (initialValue failed)"
+transConstVal _ty (Some DynRefRepr) (ConstTraitObject defId traitId vtableId) = do
+  traitObjectPlace <- staticPlace defId
+  traitObjectAddr <- addrOfPlace traitObjectPlace
+  mkTraitObject traitId vtableId traitObjectAddr
 transConstVal _ty (Some MirReferenceRepr) (ConstRawPtr i) =
     MirExp MirReferenceRepr <$> integerToMirRef (R.App $ usizeLit i)
 transConstVal ty@(M.TyAdt aname _ _) tpr (ConstStruct fields) = do

crux-mir/CHANGELOG.md

@@ -1,5 +1,9 @@
 # next
 
+This release supports [version
+9](https://github.com/GaloisInc/mir-json/blob/master/SCHEMA_CHANGELOG.md#9) of
+`mir-json`'s schema.
+
 # 0.12 -- 2026-01-29
 
 This release supports [version

crux-mir/README.md

@@ -49,7 +49,7 @@ Next, navigate to the `crucible/dependencies/mir-json` directory. Install
 [the `mir-json` README][mir-json-readme].
 
 Currently, `crux-mir` supports [version
-8](https://github.com/GaloisInc/mir-json/blob/master/SCHEMA_CHANGELOG.md#8) of
+9](https://github.com/GaloisInc/mir-json/blob/master/SCHEMA_CHANGELOG.md#9) of
 `mir-json`'s schema. Note that the schema versions produced by `mir-json` can
 change over time as dictated by internal requirements and upstream changes. To
 help smooth this over:

crux-mir/test/conc_eval/traits/dynamic_const.rs

@@ -0,0 +1,18 @@
+pub trait Trait {
+    fn method(&self) -> u32;
+}
+
+impl Trait for u32 {
+    fn method(&self) -> u32 { *self }
+}
+
+const X: &dyn Trait = &0u32;
+
+#[cfg_attr(crux, crux::test)]
+pub fn crux_test() -> u32 {
+    X.method()
+}
+
+pub fn main() {
+    println!("{:?}", crux_test());
+}