MIR: Update Rust toolchain to 1.91 (nightly-2025-09-14)

.github/Dockerfile-crux-mir

@@ -1,6 +1,6 @@
 # If you update this, make sure to also update RUST_TOOLCHAIN in
 # .github/workflows/crux-mir-build.yml
-ARG RUST_TOOLCHAIN="nightly-2025-02-16"
+ARG RUST_TOOLCHAIN="nightly-2025-09-14"
 ARG CRUX_BUILD_DIR=/crux-mir/build
 
 # Note that we intentionally do not use ubuntu:24.04 or later pending a

.github/workflows/crux-mir-build.yml

@@ -29,7 +29,7 @@ env:
   CARGO_CACHE_VERSION: 1
   # If you update this, make sure to also update RUST_TOOLCHAIN in
   # .github/Dockerfile-crux-mir
-  RUST_TOOLCHAIN: "nightly-2025-02-16"
+  RUST_TOOLCHAIN: "nightly-2025-09-14"
 
 jobs:
   config:

crucible-mir/CHANGELOG.md

@@ -1,9 +1,10 @@
 # next
 
 This release supports [version
-5](https://github.com/GaloisInc/mir-json/blob/master/SCHEMA_CHANGELOG.md#5) of
+6](https://github.com/GaloisInc/mir-json/blob/master/SCHEMA_CHANGELOG.md#6) of
 `mir-json`'s schema.
 
+* Support simulating Rust code up to version 1.91.
 * Add an intrinsic for [`needs_drop`](https://doc.rust-lang.org/std/intrinsics/fn.needs_drop.html).
 * `TyConst` now has a `ConstVal` field to indicate the value of the constant
   used to instantiate a const generic parameter. This has no impact on the

crucible-mir/src/Mir/JSON.hs

@@ -266,7 +266,6 @@ instance FromJSON Fn where
 instance FromJSON Abi where
     parseJSON = withObject "Abi" $ \v -> case lookupKM "kind" v of
         Just (String "Rust") -> pure RustAbi
-        Just (String "RustIntrinsic") -> pure RustIntrinsic
         -- For `RustCall`, defaut to `RcNoBody`.  The spread_arg info will be
         -- added while parsing the `Fn`, if this `Abi` is part of a `Fn`'s
         -- signature.

crucible-mir/src/Mir/Mir.hs

@@ -157,7 +157,6 @@ data FnSig = FnSig {
 data Abi
     = RustAbi
     | RustCall RustCallBodyInfo
-    | RustIntrinsic
     | OtherAbi
     deriving (Show, Eq, Ord, Generic)
 

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 = 5
+supportedSchemaVersion = 6
 
 -- | 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

@@ -31,6 +31,7 @@ module Mir.Trans(transCollection,transStatics,RustModule(..)
                 , evalOperand
                 , vectorCopy, aggregateCopy_constLen
                 , ptrCopy, copyNonOverlapping
+                , isNonOverlapping
                 , evalRval
                 , callExp
                 , callHandle
@@ -3212,31 +3213,39 @@ copyNonOverlapping ::
     R.Expr MIR s UsizeType ->
     MirGenerator h s ret (MirExp s)
 copyNonOverlapping tpr src dest count = do
-    -- Assert that the two regions really are nonoverlapping.
-    maybeOffset <- mirRef_tryOffsetFrom dest src
-
     -- `count` must not exceed isize::MAX, else the overlap check
     -- will misbehave.
     let sizeBits = fromIntegral $ C.intValue (C.knownNat @SizeBits)
     let maxCount = R.App $ usizeLit (1 `shift` (sizeBits - 1))
     let countOk = R.App $ usizeLt count maxCount
     G.assertExpr countOk $ S.litExpr "count overflow in copy_nonoverlapping"
 
-    -- If `maybeOffset` is Nothing, then src and dest definitely
-    -- don't overlap, since they come from different allocations.
-    -- If it's Just, the value must be >= count or <= -count to put
-    -- the two regions far enough apart.
-    let count' = usizeToIsize R.App count
-    let destAbove = \offset -> R.App $ isizeLe count' offset
-    let destBelow = \offset -> R.App $ isizeLe offset (R.App $ isizeNeg count')
-    offsetOk <- G.caseMaybe maybeOffset C.BoolRepr $ G.MatchMaybe
-        (\offset -> return $ R.App $ E.Or (destAbove offset) (destBelow offset))
-        (return $ R.App $ E.BoolLit True)
-    G.assertExpr offsetOk $ S.litExpr "src and dest overlap in copy_nonoverlapping"
+    nonOverlapping <- isNonOverlapping src dest count
+    G.assertExpr nonOverlapping $ S.litExpr "src and dest overlap in copy_nonoverlapping"
 
     ptrCopy tpr src dest count
     return $ MirExp C.UnitRepr $ R.App E.EmptyApp
 
+-- | Check if two allocations of the given size are non-overlapping.
+-- Assumes @size <= isize::MAX@.
+isNonOverlapping ::
+    R.Expr MIR s MirReferenceType ->
+    R.Expr MIR s MirReferenceType ->
+    R.Expr MIR s UsizeType ->
+    MirGenerator h s ret (G.Expr MIR s C.BoolType)
+isNonOverlapping src dest size = do
+  maybeOffset <- mirRef_tryOffsetFrom dest src
+  -- If `maybeOffset` is Nothing, then src and dest definitely
+  -- don't overlap, since they come from different allocations.
+  -- If it's Just, the value must be >= size or <= -size to put
+  -- the two regions far enough apart.
+  let size' = usizeToIsize R.App size
+      destAbove offset = R.App $ isizeLe size' offset
+      destBelow offset = R.App $ isizeLe offset (R.App $ isizeNeg size')
+  G.caseMaybe maybeOffset C.BoolRepr $ G.MatchMaybe
+    (\offset -> return $ R.App $ E.Or (destAbove offset) (destBelow offset))
+    (return $ R.App $ E.BoolLit True)
+
 --  LocalWords:  params IndexMut FnOnce Fn IntoIterator iter impl
 --  LocalWords:  tovec fromelem tmethsubst MirExp initializer callExp
 --  LocalWords:  mkTraitObject mkCustomTraitObject TyClosure

crucible-mir/src/Mir/TransCustom.hs

@@ -179,6 +179,8 @@ customOpDefs = Map.fromList $ [
                          , intrinsics_copy
                          , intrinsics_copy_nonoverlapping
 
+                         , cell_swap_is_nonoverlapping
+
                          , exit
                          , abort
                          , panicking_begin_panic
@@ -761,6 +763,21 @@ intrinsics_copy_nonoverlapping = ( ["core", "intrinsics", "copy_nonoverlapping"]
             _ -> mirFail $ "bad arguments for intrinsics::copy_nonoverlapping: " ++ show ops
         _ -> Nothing)
 
+cell_swap_is_nonoverlapping :: (ExplodedDefId, CustomRHS)
+cell_swap_is_nonoverlapping =
+    ( ["core", "cell", "{impl}", "swap", "crucible_cell_swap_is_nonoverlapping_hook"]
+    , \case
+        Substs [ty] -> Just $ CustomOp $ \_ ops -> case ops of
+            [MirExp MirReferenceRepr src,
+             MirExp MirReferenceRepr dest] -> do
+                size <- getLayoutFieldAsExpr "crucible_cell_swap_is_nonoverlapping_hook" laySize ty
+                MirExp C.BoolRepr <$> isNonOverlapping src dest size
+            _ -> mirFail $
+                "bad arguments for Cell::swap::crucible_cell_swap_is_nonoverlapping_hook: "
+                ++ show ops
+        _ -> Nothing
+    )
+
 -----------------------------------------------------------------------------------------------------
 -- ** Custom: wrapping_mul
 

crux-mir/CHANGELOG.md

@@ -1,9 +1,11 @@
 # next
 
 This release supports [version
-5](https://github.com/GaloisInc/mir-json/blob/master/SCHEMA_CHANGELOG.md#5) of
+6](https://github.com/GaloisInc/mir-json/blob/master/SCHEMA_CHANGELOG.md#6) of
 `mir-json`'s schema.
 
+* Support simulating Rust code up to version 1.91.
+
 # 0.11 -- 2025-11-09
 
 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
-5](https://github.com/GaloisInc/mir-json/blob/master/SCHEMA_CHANGELOG.md#5) of
+6](https://github.com/GaloisInc/mir-json/blob/master/SCHEMA_CHANGELOG.md#6) 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/src/Mir/Generate.hs

@@ -16,6 +16,7 @@
 module Mir.Generate(generateMIR) where
 
 import Control.Monad (when)
+import Data.List (stripPrefix)
 
 import qualified Data.ByteString.Lazy as B
 import qualified Data.ByteString as BS
@@ -25,7 +26,7 @@ import System.FilePath
 import System.IO
 import qualified System.Process as Proc
 import           System.Exit (ExitCode(..))
-import           System.Directory (doesFileExist, removeFile, getModificationTime)
+import           System.Directory (doesFileExist, removeFile, getModificationTime, listDirectory)
 import           Data.Time.Clock (UTCTime)
 
 import GHC.Stack
@@ -69,6 +70,7 @@ compileMirJson cruxOpts keepRlib rustFile = do
     let outFile = rustFile -<.> "bin"
 
     rlibsDir <- getRlibsDir
+    rlibsFiles <- listDirectory rlibsDir
     -- rustc produces colorful error messages, so preserve the colors whenever
     -- possible when printing the error messages back out to the user.
     let colorOpts
@@ -81,10 +83,11 @@ compileMirJson cruxOpts keepRlib rustFile = do
           Proc.proc "mir-json" $
             [rustFile, "-L", rlibsDir, "--crate-type=rlib", "--edition=2021"] ++
             concat
-              [ [ "--extern"
-                , lib ++ "=" ++ rlibsDir </> "lib" ++ lib <.> "rlib"
-                ]
-              | lib <- libDependencies ] ++
+              [ ["--extern", libName ++ "=" ++ rlibsDir </> file]
+              | file <- rlibsFiles
+              , (baseName, ".rlib") <- [splitExtension file]
+              , Just libName <- [stripPrefix "lib" baseName]
+              ] ++
             colorOpts ++
             [ "--cfg", "crux", "--cfg", "crux_top_level"
             , "-Z", "ub-checks=false"
@@ -144,42 +147,6 @@ maybeLinkJson jsonFiles cacheFile = do
     else
         B.readFile cacheFile
 
-libDependencies :: [FilePath]
-libDependencies =
-    -- std and its dependencies
-    [ "addr2line"
-    , "adler2"
-    , "alloc"
-    , "cfg_if"
-    , "compiler_builtins"
-    , "core"
-    , "crucible"
-    , "getopts"
-    , "gimli"
-    , "hashbrown"
-    , "libc"
-    , "memchr"
-    , "miniz_oxide"
-    , "object"
-    , "panic_abort"
-    , "panic_unwind"
-    , "proc_macro"
-    , "rustc_demangle"
-    , "rustc_std_workspace_alloc"
-    , "rustc_std_workspace_core"
-    , "rustc_std_workspace_std"
-    , "std_detect"
-    , "std"
-    , "test"
-    , "unicode_width"
-    , "unwind"
-    -- additional libs
-    , "crucible"
-    , "int512"
-    , "byteorder"
-    , "bytes"
-    ]
-
 
 -- | Run mir-json on the input, generating lib file on disk
 -- NOTE: If the rust file has not been modified since the
@@ -197,7 +164,8 @@ generateMIR cruxOpts inputFile keepRlib
     let rustFile = inputFile
     maybeCompileMirJson cruxOpts keepRlib rustFile
     rlibsDir <- getRlibsDir
-    let libJsonPaths = [rlibsDir </> "lib" ++ lib <.> "mir" | lib <- libDependencies]
+    rlibsFiles <- listDirectory rlibsDir
+    let libJsonPaths = [rlibsDir </> file | file <- rlibsFiles, takeExtension file == ".mir"]
     b <- maybeLinkJson (mirJsonOutFile rustFile : libJsonPaths) (linkOutFile rustFile)
     parseMIR (linkOutFile rustFile) b
   | ext == ".json" = do

crux-mir/test/conc_eval/hash_map/extract_if.rs

@@ -0,0 +1,17 @@
+use std::collections::HashMap;
+use std::convert::TryInto;
+
+#[cfg_attr(crux, crux::test)]
+fn crux_test() -> ([i32; 4], [i32; 4]) {
+    let mut map: HashMap<i32, i32> = (0..8).map(|x| (x, x)).collect();
+    let extracted: HashMap<i32, i32> = map.extract_if(|k, _v| k % 2 == 0).collect();
+    let mut evens = extracted.keys().copied().collect::<Vec<_>>();
+    let mut odds = map.keys().copied().collect::<Vec<_>>();
+    evens.sort();
+    odds.sort();
+    (evens.try_into().unwrap(), odds.try_into().unwrap())
+}
+
+pub fn main() {
+    println!("{:?}", crux_test());
+}

crux-mir/test/conc_eval/num/cmp.rs

@@ -0,0 +1,8 @@
+use std::cmp::Ordering;
+
+#[cfg_attr(crux, crux::test)]
+pub fn crux_test() -> Ordering {
+    1.cmp(&2)
+}
+
+pub fn main() { println!("{:?}", crux_test()); }

crux-mir/test/conc_eval/rc/rc_basic.rs

@@ -1,4 +1,4 @@
-// FAIL: `Rc` uses `mem::size_of_val`
+// FAIL: `Rc` uses `mem::align_of_val`
 use std::rc::Rc;
 
 #[cfg_attr(crux, crux::test)]

crux-mir/test/conc_eval/vec/try_into_array.rs

@@ -0,0 +1,10 @@
+use std::convert::TryInto;
+
+#[cfg_attr(crux, crux::test)]
+fn test() -> Result<[i32; 4], Vec<i32>> {
+    vec![1, 2, 3, 4].try_into()
+}
+
+fn main() {
+    println!("{:?}", test());
+}

crux-mir/test/symb_eval/bytes/put_overflow.good

@@ -5,7 +5,7 @@ failures:
 
 ---- put_overflow/<DISAMB>::f[0] counterexamples ----
 [Crux] Found counterexample for verification goal
-[Crux]   ./libs/core/src/panic.rs:107:9: 107:73 !./libs/bytes.rs:201:9: 202:49: error: in bytes/<DISAMB>::{impl#4}[0]::put_slice[0]
+[Crux]   ./libs/core/src/panic.rs:62:9: 62:73 !./libs/bytes.rs:201:9: 202:49: error: in bytes/<DISAMB>::{impl#4}[0]::put_slice[0]
 [Crux]   panicking::panic_fmt, called from bytes/<DISAMB>::{impl#4}[0]::put_slice[0]
 
 [Crux-MIR] ---- FINAL RESULTS ----

crux-mir/test/symb_eval/crux/early_fail.good

@@ -7,7 +7,7 @@ failures:
 
 ---- early_fail/<DISAMB>::fail1[0] counterexamples ----
 [Crux] Found counterexample for verification goal
-[Crux]   ./libs/core/src/panic.rs:107:9: 107:73 !test/symb_eval/crux/early_fail.rs:11:5: 11:20: error: in early_fail/<DISAMB>::fail1[0]
+[Crux]   ./libs/core/src/panic.rs:62:9: 62:73 !test/symb_eval/crux/early_fail.rs:11:5: 11:20: error: in early_fail/<DISAMB>::fail1[0]
 [Crux]   panicking::panic_fmt, called from early_fail/<DISAMB>::fail1[0]
 
 ---- early_fail/<DISAMB>::fail2[0] counterexamples ----

crux-mir/test/symb_eval/crux/multi.good

@@ -18,7 +18,7 @@ failures:
 
 ---- multi/<DISAMB>::fail2[0] counterexamples ----
 [Crux] Found counterexample for verification goal
-[Crux]   ./libs/core/src/panic.rs:107:9: 107:73 !test/symb_eval/crux/multi.rs:15:9: 15:22: error: in multi/<DISAMB>::fail2[0]
+[Crux]   ./libs/core/src/panic.rs:62:9: 62:73 !test/symb_eval/crux/multi.rs:15:9: 15:22: error: in multi/<DISAMB>::fail2[0]
 [Crux]   panicking::panic_fmt, called from multi/<DISAMB>::fail2[0]
 
 ---- multi/<DISAMB>::fail3[0] counterexamples ----

crux-mir/test/symb_eval/num/unchecked_arith.good

@@ -13,27 +13,27 @@ failures:
 
 ---- unchecked_arith/<DISAMB>::add_test[0] counterexamples ----
 [Crux] Found counterexample for verification goal
-[Crux]   ./libs/core/src/num/uint_macros.rs:572:17: 572:53 !./libs/core/src/num/mod.rs:436:5: 454:6: error: in core/<DISAMB>::num[0]::{impl#6}[0]::unchecked_add[0]
+[Crux]   ./libs/core/src/num/uint_macros.rs:717:17: 717:53 !./libs/core/src/num/mod.rs:447:5: 468:6: error: in core/<DISAMB>::num[0]::{impl#6}[0]::unchecked_add[0]
 [Crux]   Binary operation (+) would overflow
 
 ---- unchecked_arith/<DISAMB>::mul_test[0] counterexamples ----
 [Crux] Found counterexample for verification goal
-[Crux]   ./libs/core/src/num/uint_macros.rs:945:17: 945:53 !./libs/core/src/num/mod.rs:436:5: 454:6: error: in core/<DISAMB>::num[0]::{impl#6}[0]::unchecked_mul[0]
+[Crux]   ./libs/core/src/num/uint_macros.rs:1105:17: 1105:53 !./libs/core/src/num/mod.rs:447:5: 468:6: error: in core/<DISAMB>::num[0]::{impl#6}[0]::unchecked_mul[0]
 [Crux]   Binary operation (*) would overflow
 
 ---- unchecked_arith/<DISAMB>::shl_test[0] counterexamples ----
 [Crux] Found counterexample for verification goal
-[Crux]   ./libs/core/src/num/uint_macros.rs:1558:17: 1558:53 !./libs/core/src/num/mod.rs:436:5: 454:6: error: in core/<DISAMB>::num[0]::{impl#6}[0]::unchecked_shl[0]
+[Crux]   ./libs/core/src/num/uint_macros.rs:1794:17: 1794:53 !./libs/core/src/num/mod.rs:447:5: 468:6: error: in core/<DISAMB>::num[0]::{impl#6}[0]::unchecked_shl[0]
 [Crux]   Binary operation (<<) would overflow
 
 ---- unchecked_arith/<DISAMB>::shr_test[0] counterexamples ----
 [Crux] Found counterexample for verification goal
-[Crux]   ./libs/core/src/num/uint_macros.rs:1679:17: 1679:53 !./libs/core/src/num/mod.rs:436:5: 454:6: error: in core/<DISAMB>::num[0]::{impl#6}[0]::unchecked_shr[0]
+[Crux]   ./libs/core/src/num/uint_macros.rs:1966:17: 1966:53 !./libs/core/src/num/mod.rs:447:5: 468:6: error: in core/<DISAMB>::num[0]::{impl#6}[0]::unchecked_shr[0]
 [Crux]   Binary operation (>>) would overflow
 
 ---- unchecked_arith/<DISAMB>::sub_test[0] counterexamples ----
 [Crux] Found counterexample for verification goal
-[Crux]   ./libs/core/src/num/uint_macros.rs:762:17: 762:53 !./libs/core/src/num/mod.rs:436:5: 454:6: error: in core/<DISAMB>::num[0]::{impl#6}[0]::unchecked_sub[0]
+[Crux]   ./libs/core/src/num/uint_macros.rs:896:17: 896:53 !./libs/core/src/num/mod.rs:447:5: 468:6: error: in core/<DISAMB>::num[0]::{impl#6}[0]::unchecked_sub[0]
 [Crux]   Binary operation (-) would overflow
 
 [Crux-MIR] ---- FINAL RESULTS ----

crux-mir/test/symb_eval/scalar/test1.good

@@ -3,8 +3,8 @@ ok
 
 [Crux-MIR] ---- FINAL RESULTS ----
 [Crux] Goal status:
-[Crux]   Total: 84
-[Crux]   Proved: 84
+[Crux]   Total: 77
+[Crux]   Proved: 77
 [Crux]   Disproved: 0
 [Crux]   Incomplete: 0
 [Crux]   Unknown: 0