crux-mir: Adjust documentation, CI, and test suite in light of standard library migration

Now that the `mir-json`-specific versions of the Rust standard libraries have
been moved to the `mir-json` repo (in
GaloisInc/mir-json#85), this patch adjusts the various
references to the standard libraries to ensure that `crux-mir`'s documentation,
CI, and test suite remain up to date.

Towards #1252

Author: RyanGlScott

.github/Dockerfile-crux-mir

@@ -39,7 +39,11 @@ ENV LANG=C.UTF-8 \
 WORKDIR ${CRUX_BUILD_DIR}/dependencies/mir-json
 RUN curl https://sh.rustup.rs -sSf | bash -s -- -y --profile minimal --default-toolchain ${RUST_TOOLCHAIN}
 RUN rustup component add --toolchain ${RUST_TOOLCHAIN} rustc-dev
-RUN cargo install --locked
+RUN cargo install --locked && \
+    ./translate_libs.sh
+# Define `CRUX_RUST_LIBRARY_PATH` this for the benefit of
+# `crux v2-test crux-mir` below.
+ENV CRUX_RUST_LIBRARY_PATH=$(pwd)/rlibs
 
 RUN mkdir -p /crux-mir/rootfs/usr/local/bin
 WORKDIR /crux-mir/rootfs/usr/local/bin
@@ -59,8 +63,6 @@ RUN mkdir -p /home/crux-mir/.ghcup && \
     ghcup install ghc 9.4.8 && \
     ghcup set ghc 9.4.8
 
-WORKDIR ${CRUX_BUILD_DIR}/crux-mir
-RUN ./translate_libs.sh
 WORKDIR ${CRUX_BUILD_DIR}
 RUN cabal v2-update && \
     cabal v2-build --only-dependencies crux-mir && \
@@ -82,7 +84,7 @@ RUN apt-get update && \
 COPY --from=build /home/crux-mir/.cargo/bin /home/crux-mir/.cargo/bin
 COPY --from=build /home/crux-mir/.rustup /home/crux-mir/.rustup
 COPY --from=build /crux-mir/rootfs /
-COPY --from=build ${CRUX_BUILD_DIR}/crux-mir/rlibs /crux-mir/rlibs
+COPY --from=build ${CRUX_BUILD_DIR}/dependencies/mir-json/rlibs /crux-mir/rlibs
 
 RUN useradd -m crux-mir && chown -R crux-mir:crux-mir /crux-mir /home/crux-mir
 USER crux-mir

.github/ci.sh

@@ -158,14 +158,6 @@ bundle_crux_mir_files() {
   setup_dist
   extract_exe crux-mir dist/bin
   cp crux-mir/README.md dist/doc
-  # rlibs is a symlink into rlibs_real; we can't just copy the symlink
-  # though because (currently at least) it's an absolute path that
-  # won't work in the output artefact.
-  #
-  # Use tar to copy (not cp -r, which isn't very safe) and descend
-  # into rlibs explicitly first as a cheap way to follow that symlink.
-  mkdir dist/rlibs
-  (cd crux-mir/rlibs && tar -cf - .) | (cd dist/rlibs && tar -xvf -)
   # It's less fragile to have users install mir-json themselves
   # (cd dependencies/mir-json && cargo install --locked --force --root ../../dist)
   VERSION=${VERSION:-$DATE}

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

@@ -129,8 +129,13 @@ jobs:
           BUILD_TARGET_OS: ${{ matrix.os }}
           BUILD_TARGET_ARCH: ${{ runner.arch }}
 
-      - shell: bash
-        run: cd dependencies/mir-json && cargo install --locked --force
+      - name: Install mir-json
+        shell: bash
+        working-directory: dependencies/mir-json
+        run: |
+          cargo install --locked --force
+          bash ./translate_libs.sh
+          echo "CRUX_RUST_LIBRARY_PATH=$(pwd)/rlibs" >> $GITHUB_ENV
 
       - shell: bash
         run: .github/ci.sh configure
@@ -147,9 +152,6 @@ jobs:
         # See Note [--disable-documentation] in `crucible-go-build.yml`.
         run: cabal v2-haddock --disable-documentation crucible-syntax crucible-concurrency crux-mir
 
-      - shell: bash
-        run: cd crux-mir && bash ./translate_libs.sh
-
       - shell: bash
         run: .github/ci.sh test crux-mir
 

crux-mir/CHANGELOG.md

@@ -1,6 +1,10 @@
 # next
 
-Nothing yet.
+* The modified copies of the Rust standard libraries that `mir-json` depends on
+  (and `crux-mir` therefore ingests) now live in the `mir-json` repo rather
+  than in the `crucible` repo. See the [`mir-json`
+  README](https://github.com/GaloisInc/mir-json/blob/master/README.md) for
+  details.
 
 # 0.10 -- 2025-03-21
 

crux-mir/README.md

@@ -15,9 +15,10 @@ functionality.
 
     $ git submodule update --init
 
-Next, navigate to the `crucible/dependencies/mir-json` directory and install
-`mir-json` according to the instructions in [the `mir-json`
-README][mir-json-readme].
+Next, navigate to the `crucible/dependencies/mir-json` directory. Install
+`mir-json`, translate its standard libraries, and define the
+`CRUX_RUST_LIBRARY_PATH` environment variable according to the instructions in
+[the `mir-json` README][mir-json-readme].
 
 Currently, `crux-mir` supports [version
 1](https://github.com/GaloisInc/mir-json/blob/master/SCHEMA_CHANGELOG.md#1) of
@@ -44,21 +45,6 @@ Use GHC 9.4, 9.6, or 9.8. From the `crux-mir` directory, run:
 
     $ cabal v2-install exe:crux-mir --overwrite-policy=always
 
-Then translate the Rust libraries in `lib/`:
-
-    $ ./translate_libs.sh
-
-If you want to cross-compile for a different target, you can optionally set the
-environment variable `TARGET` to a [target
-triple](https://doc.rust-lang.org/nightly/rustc/platform-support.html) when
-running `./translate_libs.sh`. This is experimental and we have only tested
-`wasm32-unknown-unknown` to work; you might get build errors for other targets.
-
-    $ TARGET=wasm32-unknown-unknown ./translate_libs.sh
-
-When upgrading from a previous version, first install the new `mir-json`
-version, then rerun the `cabal v2-install` and `./translate_libs.sh` commands.
-
 
 ## Usage
 
@@ -71,8 +57,8 @@ compiled by checking for the `crux` configuration predicate using
 `#[cfg_attr(crux, crux::test)]`.
 
 Test cases can create and manipulate symbolic values using the functions in the
-[`crucible`](lib/crucible) Rust crate.  See
-[`example/ffs/lib.rs`](example/ffs/lib.rs) or the files in
+[`crucible`](https://github.com/GaloisInc/mir-json/tree/master/libs/crucible)
+Rust crate.  See [`example/ffs/lib.rs`](example/ffs/lib.rs) or the files in
 [`test/symb_eval/`](test/symb_eval) for examples of creating symbolic values
 and asserting properties about them.
 
@@ -81,7 +67,7 @@ and asserting properties about them.
 Set the `CRUX_RUST_LIBRARY_PATH` environment variable to the path to the
 translated libraries:
 
-    $ export CRUX_RUST_LIBRARY_PATH=.../crux-mir/rlibs
+    $ export CRUX_RUST_LIBRARY_PATH=<mir-json checkout>/rlibs
 
 In the directory of a Cargo project (such as the [find-first-set
 example](example/ffs)), run the project's symbolic tests:
@@ -120,14 +106,10 @@ To run `crux-mir`'s test suite:
 
     $ cabal v2-test
 
-You need to have built and installed the mir-json tool such that it
-can be found on your $PATH.
-You also need translated libraries for the Rust target architecture
-you're testing on.
-Make sure that the `rlibs` symlink exists and points to the right
-architecture's libraries.
-If not, run the `translate_libs.sh` script as described above under
-Installation.
+You need to have built and installed the mir-json tool such that it can be
+found on your $PATH. You also need translated libraries for the Rust target
+architecture you're testing on. See the "Preliminaries" section above for more
+details.
 
 ### Expected Failures
 

crux-mir/test/symb_eval/concretize/assert.good

@@ -4,7 +4,7 @@ failures:
 
 ---- assert/<DISAMB>::crux_test[0] counterexamples ----
 [Crux] Found counterexample for verification goal
-[Crux]   ./lib/crucible/lib.rs:48:17: 48:82 !test/symb_eval/concretize/assert.rs:10:5: 10:81: error: in assert/<DISAMB>::crux_test[0]
+[Crux]   ./libs/crucible/lib.rs:48:17: 48:82 !test/symb_eval/concretize/assert.rs:10:5: 10:81: error: in assert/<DISAMB>::crux_test[0]
 [Crux]   MIR assertion at test/symb_eval/concretize/assert.rs:10:5:
 [Crux]   	100 + 157 == 1
 

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

@@ -10,7 +10,7 @@ failures:
 
 ---- early_fail/<DISAMB>::fail2[0] counterexamples ----
 [Crux] Found counterexample for verification goal
-[Crux]   ./lib/crucible/lib.rs:38:41: 38:58 !test/symb_eval/crux/early_fail.rs:17:5: 17:29: error: in early_fail/<DISAMB>::fail2[0]
+[Crux]   ./libs/crucible/lib.rs:38:41: 38:58 !test/symb_eval/crux/early_fail.rs:17:5: 17:29: error: in early_fail/<DISAMB>::fail2[0]
 [Crux]   MIR assertion at test/symb_eval/crux/early_fail.rs:17:5:
 [Crux]   	x == 0
 

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

@@ -8,7 +8,7 @@ failures:
 [Crux]   test/symb_eval/crux/fail_return.rs:8:22: 8:27: error: in fail_return/<DISAMB>::fail1[0]
 [Crux]   attempt to compute `move _4 + const 1_u8`, which would overflow
 [Crux] Found counterexample for verification goal
-[Crux]   ./lib/crucible/lib.rs:38:41: 38:58 !test/symb_eval/crux/fail_return.rs:8:5: 8:32: error: in fail_return/<DISAMB>::fail1[0]
+[Crux]   ./libs/crucible/lib.rs:38:41: 38:58 !test/symb_eval/crux/fail_return.rs:8:5: 8:32: error: in fail_return/<DISAMB>::fail1[0]
 [Crux]   MIR assertion at test/symb_eval/crux/fail_return.rs:8:5:
 [Crux]   	x + 1 > x
 
@@ -17,7 +17,7 @@ failures:
 [Crux]   test/symb_eval/crux/fail_return.rs:15:22: 15:27: error: in fail_return/<DISAMB>::fail2[0]
 [Crux]   attempt to compute `move _5 + const 1_u8`, which would overflow
 [Crux] Found counterexample for verification goal
-[Crux]   ./lib/crucible/lib.rs:38:41: 38:58 !test/symb_eval/crux/fail_return.rs:15:5: 15:32: error: in fail_return/<DISAMB>::fail2[0]
+[Crux]   ./libs/crucible/lib.rs:38:41: 38:58 !test/symb_eval/crux/fail_return.rs:15:5: 15:32: error: in fail_return/<DISAMB>::fail2[0]
 [Crux]   MIR assertion at test/symb_eval/crux/fail_return.rs:15:5:
 [Crux]   	x + 1 > x
 

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

@@ -10,7 +10,7 @@ failures:
 [Crux]   test/symb_eval/crux/mixed_fail.rs:8:22: 8:27: error: in mixed_fail/<DISAMB>::fail1[0]
 [Crux]   attempt to compute `move _5 + const 1_u8`, which would overflow
 [Crux] Found counterexample for verification goal
-[Crux]   ./lib/crucible/lib.rs:38:41: 38:58 !test/symb_eval/crux/mixed_fail.rs:8:5: 8:32: error: in mixed_fail/<DISAMB>::fail1[0]
+[Crux]   ./libs/crucible/lib.rs:38:41: 38:58 !test/symb_eval/crux/mixed_fail.rs:8:5: 8:32: error: in mixed_fail/<DISAMB>::fail1[0]
 [Crux]   MIR assertion at test/symb_eval/crux/mixed_fail.rs:8:5:
 [Crux]   	x + 1 > x
 
@@ -19,7 +19,7 @@ failures:
 [Crux]   test/symb_eval/crux/mixed_fail.rs:14:22: 14:27: error: in mixed_fail/<DISAMB>::fail2[0]
 [Crux]   attempt to compute `move _5 + const 2_u8`, which would overflow
 [Crux] Found counterexample for verification goal
-[Crux]   ./lib/crucible/lib.rs:38:41: 38:58 !test/symb_eval/crux/mixed_fail.rs:14:5: 14:32: error: in mixed_fail/<DISAMB>::fail2[0]
+[Crux]   ./libs/crucible/lib.rs:38:41: 38:58 !test/symb_eval/crux/mixed_fail.rs:14:5: 14:32: error: in mixed_fail/<DISAMB>::fail2[0]
 [Crux]   MIR assertion at test/symb_eval/crux/mixed_fail.rs:14:5:
 [Crux]   	x + 2 > x
 

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

@@ -9,7 +9,7 @@ failures:
 [Crux]   test/symb_eval/crux/multi.rs:8:22: 8:27: error: in multi/<DISAMB>::fail1[0]
 [Crux]   attempt to compute `move _5 + const 1_u8`, which would overflow
 [Crux] Found counterexample for verification goal
-[Crux]   ./lib/crucible/lib.rs:38:41: 38:58 !test/symb_eval/crux/multi.rs:8:5: 8:32: error: in multi/<DISAMB>::fail1[0]
+[Crux]   ./libs/crucible/lib.rs:38:41: 38:58 !test/symb_eval/crux/multi.rs:8:5: 8:32: error: in multi/<DISAMB>::fail1[0]
 [Crux]   MIR assertion at test/symb_eval/crux/multi.rs:8:5:
 [Crux]   	x + 1 > x
 
@@ -20,7 +20,7 @@ failures:
 
 ---- multi/<DISAMB>::fail3[0] counterexamples ----
 [Crux] Found counterexample for verification goal
-[Crux]   ./lib/crucible/lib.rs:38:41: 38:58 !test/symb_eval/crux/multi.rs:20:5: 20:29: error: in multi/<DISAMB>::assert_zero[0]
+[Crux]   ./libs/crucible/lib.rs:38:41: 38:58 !test/symb_eval/crux/multi.rs:20:5: 20:29: error: in multi/<DISAMB>::assert_zero[0]
 [Crux]   MIR assertion at test/symb_eval/crux/multi.rs:20:5:
 [Crux]   	x == 0