update veritas to rust 1.82.0, update run configurations

tools/veritas/build_images.sh

@@ -7,6 +7,6 @@ if [ "$(dirname "$0")" != "." ]; then
     exit 1
 fi
 
-docker build -f verus-lang_verus-base.dockerfile -t ghcr.io/utaal/verus-lang/verus-base .
-docker build -f verus-lang_verus-base-1.79.0.dockerfile -t ghcr.io/utaal/verus-lang/verus-base:rust-1.79.0 .
-docker build -f verus-lang_veritas-1.79.0.dockerfile -t ghcr.io/utaal/verus-lang/veritas:rust-1.79.0 .
+docker build -f verus-lang_verus-deps.dockerfile -t ghcr.io/utaal/verus-lang/verus-deps .
+docker build -f verus-lang_verus-base-1.82.0.dockerfile -t ghcr.io/utaal/verus-lang/verus-base:rust-1.82.0 .
+docker build -f verus-lang_veritas-1.82.0.dockerfile -t ghcr.io/utaal/verus-lang/veritas:rust-1.82.0 .

tools/veritas/build_verus.sh

@@ -4,9 +4,10 @@ set -x
 unset RUSTUP_TOOLCHAIN
 cd source
 
-pushd tools/line_count
-cargo build --release
-popd
+# TODO restore once line_count is fixed
+# pushd tools/line_count
+# cargo build --release
+# popd
 
 . ../tools/activate
 # ./tools/get-z3.sh

tools/veritas/push_images.sh

@@ -0,0 +1,12 @@
+
+set -e
+set -x
+
+if [ "$(dirname "$0")" != "." ]; then
+    echo "Please run the script from its directory."
+    exit 1
+fi
+
+docker push ghcr.io/utaal/verus-lang/verus-deps
+docker push ghcr.io/utaal/verus-lang/verus-base:rust-1.82.0
+docker push ghcr.io/utaal/verus-lang/veritas:rust-1.82.0

tools/veritas/run.sh

@@ -13,5 +13,4 @@ docker run --platform=linux/amd64 \
     -v verus-veritas-z3-cache:/root/z3-cache \
     -v verus-veritas-rustup:/root/.rustup \
     -v $(pwd)/output:/root/output \
-    ghcr.io/utaal/verus-lang/veritas:rust-1.79.0 $@
-    # --rm ghcr.io/utaal/verus-lang/veritas:rust-1.79.0 $@
+    ghcr.io/utaal/verus-lang/veritas:rust-1.82.0 $@

tools/veritas/run_configuration_all.toml

@@ -1,6 +1,7 @@
 verus_git_url = "https://github.com/verus-lang/verus.git"
 verus_revspec = "main"
 verus_features = ["singular"]
+verus_verify_vstd = false
 
 [[project]]
 name = "memory-allocator"
@@ -14,7 +15,7 @@ extra_args = [
 prepare_script = """
 pushd test_libc
 cargo clean
-cargo +1.79.0 build --release
+cargo +1.82.0 build --release
 popd
 LIBC_RLIB_NAME=$(find ./test_libc/target/release/deps/ -name 'liblibc-*.rlib')
 mkdir -p build
@@ -24,9 +25,9 @@ cp $LIBC_RLIB_NAME build/liblibc.rlib
 [[project]]
 name = "page-table"
 git_url = "https://github.com/utaal/verified-nrkernel.git"
-revspec = "page-table"
-crate_root = "page-table/main.rs"
-extra_args = ["--rlimit", "60"]
+revspec = "main"
+crate_root = "page-table/src/lib.rs"
+extra_args = ["--crate-type=lib", "--rlimit", "60"]
 
 [[project]]
 name = "verified-storage"
@@ -52,7 +53,7 @@ cargo build
 
 [[project]]
 name = "node-replication"
-git_url = "https://github.com/achreto/verified-node-replication.git"
+git_url = "https://github.com/verus-lang/verified-node-replication.git"
 revspec = "main"
 crate_root = "verified-node-replication/src/lib.rs"
 extra_args = ["--crate-type=dylib"]

tools/veritas/run_configuration_small.toml → tools/veritas/run_configuration_page_table.toml

@@ -1,11 +1,12 @@
 verus_git_url = "https://github.com/verus-lang/verus.git"
 verus_revspec = "main"
 verus_features = ["singular"]
+verus_verify_vstd = false
 
 [[project]]
 name = "page-table"
 git_url = "https://github.com/utaal/verified-nrkernel.git"
-revspec = "page-table"
-crate_root = "page-table/main.rs"
-extra_args = ["--rlimit", "60"]
+revspec = "main"
+crate_root = "page-table/src/lib.rs"
+extra_args = ["--crate-type=lib", "--rlimit", "60"]
 

tools/veritas/run_configuration_vstd.toml

@@ -0,0 +1,4 @@
+verus_git_url = "https://github.com/verus-lang/verus.git"
+verus_revspec = "main"
+verus_features = ["singular"]
+

tools/veritas/src/main.rs

@@ -391,10 +391,10 @@ fn run(run_configuration_path: &str) -> Result<(), VeritasError> {
                     revspec: run_configuration.verus_revspec.clone(),
                     crate_root: "source/vstd/vstd.rs".to_owned(),
                     extra_args: Some(vec![
-                        "--no-vstd".to_owned(),
+                        "--is-vstd".to_owned(),
                         "--crate-type=lib".to_owned(),
-                        "-V".to_owned(),
-                        "use-crate-name".to_owned(),
+                        // "-V".to_owned(),
+                        // "use-crate-name".to_owned(),
                     ]),
                     prepare_script: None,
                 },
@@ -466,8 +466,8 @@ fn run(run_configuration_path: &str) -> Result<(), VeritasError> {
 
     info("verus ready");
     let verus_binary_path = verus_workdir.join("source/target-verus/release/verus");
-    // TODO perform line counting?
-    let _verus_line_count_path = verus_workdir.join("source/target/release/line_count");
+    // TODO perform line counting? (once line_count is fixed)
+    // let _verus_line_count_path = verus_workdir.join("source/target/release/line_count");
 
     let output_path = env_var_dir_or_err(OUTPUT_PATH_VAR)?;
     let date = chrono::Utc::now()

tools/veritas/verus-lang_veritas-1.79.0.dockerfile → tools/veritas/verus-lang_veritas-1.82.0.dockerfile

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

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

@@ -0,0 +1,3 @@
+FROM --platform=linux/amd64 ghcr.io/utaal/verus-lang/verus-deps
+
+RUN /root/.cargo/bin/rustup install 1.82.0