Update Veritas to Rust 1.88.0, use local containers

Author: hayley-leblanc

tools/veritas/README.md

@@ -5,9 +5,11 @@ Veritas is a rust crater-alike tool to run a version of verus on a number of pro
 generating a report of verification success/failures and verification performance data.
 
 Running veritas requires docker (or another container runtime). 
-You can start a run with `bash run.sh path_to_run_configuration.toml`.
-There is an example run configuration in this directory.
-Running that command will start an ephemeral container and will create four
-permanent docker volumes: `verus-veritas-cargo-cache`, `verus-veritas-repo-cache`,
-`verus-veritas-rustup`, `verus-veritas-z3-cache`. These volumes cache dowloaded repositories,
-binaries, and other files, to reduce unnecessary traffic when performing multiple runs.
+
+
+### Running Veritas
+
+1. Run `bash build_images.sh` to create the Docker images Veritas uses locally
+    - This only needs to be done when running Veritas for the first time or after an update to Verus that upgrades its Rust version. 
+2. Run `bash run.sh path_to_run_configuration.toml`. There is an example run configuration in this directory. 
+    - Running that command will start an ephemeral container and will create four permanent docker volumes: `verus-veritas-cargo-cache`, `verus-veritas-repo-cache`, `verus-veritas-rustup`, `verus-veritas-z3-cache`. These volumes cache dowloaded repositories, binaries, and other files, to reduce unnecessary traffic when performing multiple runs.

tools/veritas/build_images.sh

@@ -2,11 +2,13 @@
 set -e
 set -x
 
+RUST_VERSION=1.88.0
+
 if [ "$(dirname "$0")" != "." ]; then
     echo "Please run the script from its directory."
     exit 1
 fi
 
-docker build -f verus-lang_verus-deps.dockerfile -t ghcr.io/utaal/verus-lang/verus-deps .
-docker build -f verus-lang_verus-base-1.85.1.dockerfile -t ghcr.io/utaal/verus-lang/verus-base:rust-1.85.1 .
-docker build -f verus-lang_veritas-1.85.1.dockerfile -t ghcr.io/utaal/verus-lang/veritas:rust-1.85.1 .
+docker build -f verus-lang_verus-deps.dockerfile -t verus-deps .
+docker build -f verus-lang_verus-base-$RUST_VERSION.dockerfile -t verus-base:rust-$RUST_VERSION .
+docker build -f verus-lang_veritas-$RUST_VERSION.dockerfile -t veritas:rust-$RUST_VERSION .

tools/veritas/run.sh

@@ -1,5 +1,7 @@
 #! /bin/bash
 
+RUST_VERSION=1.88.0
+
 if [ "$(dirname "$0")" != "." ]; then
     echo "Please run the script from its directory."
     exit 1
@@ -9,9 +11,9 @@ docker run --platform=linux/amd64 \
     -v verus-veritas-repo-cache:/root/repos-cache \
     -v $(pwd):/root/veritas \
     -v /root/work \
-    -v verus-veritas-cargo-cache:/root/.cargo \
+    -v verus-veritas-cargo-$RUST_VERSION-cache:/root/.cargo \
     -v verus-veritas-z3-cache:/root/z3-cache \
-    -v verus-veritas-rustup:/root/.rustup \
+    -v verus-veritas-rustup-$RUST_VERSION:/root/.rustup \
     -v $(pwd)/output:/root/output \
     --rm \
-    ghcr.io/utaal/verus-lang/veritas:rust-1.85.1 $@
+    veritas:rust-$RUST_VERSION $@

…tas/verus-lang_veritas-1.85.1.dockerfile …tas/verus-lang_veritas-1.88.0.dockerfiletools/veritas/verus-lang_veritas-1.85.1.dockerfile renamed to tools/veritas/verus-lang_veritas-1.88.0.dockerfile tools/veritas/verus-lang_veritas-1.85.1.dockerfile renamed to tools/veritas/verus-lang_veritas-1.88.0.dockerfile

@@ -1,4 +1,4 @@
-FROM --platform=linux/amd64 ghcr.io/utaal/verus-lang/verus-base:rust-1.85.1
+FROM --platform=linux/amd64 verus-base:rust-1.88.0
 
 VOLUME /root/veritas
 

tools/veritas/verus-lang_verus-base-1.85.1.dockerfile

@@ -0,0 +1,3 @@
+FROM --platform=linux/amd64 verus-deps
+
+RUN /root/.cargo/bin/rustup install 1.88.0