Upgrade verus to latest version (Drop verification time to 3min)

.github/workflows/build.yml

@@ -5,6 +5,7 @@ on:
     branches: [ "main" ]
   pull_request:
     branches: [ "main" ]
+  workflow_dispatch:
 
 env:
   CARGO_TERM_COLOR: always
@@ -19,34 +20,12 @@ jobs:
         with:
           submodules: recursive
 
-      - name: Install specified rust toolchain
-        uses: actions-rs/toolchain@v1
-        with:
-          toolchain: nightly-2023-12-22
-          target: x86_64-unknown-none
-          profile: minimal
-
-      - name: fetch verus via metadata
-        working-directory: source
+      - name: Install verus via prebuilt
+        working-directory: tools
         run: |
-            source ../tools/v-ci-setup.sh
+            ./install_verus --use-prebuilt
             echo "VERUS_PATH=$(echo $VERUS_PATH)" >> $GITHUB_ENV
 
-      - uses: Swatinem/rust-cache@v2
-        with:
-          cache-directories: ${{ env.VERUS_PATH }}/source/target-verus
-          workspaces: |
-            ${{ github.workspace }}/source -> target
-            ${{ env.VERUS_PATH }}/source -> target
-            ${{ env.VERUS_PATH }}/tools/vargo -> target
-
-      - name: Install depdendencies
-        run: ./tools/activate.sh
-
-      - name: Build
-        working-directory: source/verismo
-        run: cargo v build
-
       - name: Fmt
         run: cargo fmt --check
         working-directory: tools/cargo-v
@@ -58,3 +37,6 @@ jobs:
       - name: Fmt verus code
         run: ./tools/fmt.sh --check
 
+      - name: Verify
+        working-directory: source
+        run: cargo verus focus --release -- --multiple-errors=20 --trace --time

.gitignore

@@ -18,3 +18,7 @@ richos/module/*.dwo
 **.rust_verify
 **.bin
 **.log
+
+# Worktrees for parallel agent verification (ignored)
+.worktrees/
+.verus-log/

Makefile

@@ -19,7 +19,7 @@ verify: verifyonly fs
 
 verifyonly:
 	cd source/verismo_main &&\
-	(cargo verify --release 1> verus-stderr.log)
+	(cargo verus build --release 1> verus-stderr.log)
 
 
 ${CURDIR}/source/target/target/release/verismo_main:
@@ -28,7 +28,7 @@ ${CURDIR}/source/target/target/release/verismo_main:
 ${CURDIR}/source/target/target/${DEBUG}/verismo_main: buildonly
 
 buildonly:
-	cd source/verismo_main && cargo verify --release --feature noverify
+	cd source/verismo_main && cargo verus build --release
 
 
 $(LINUX_OUT):

README.md

@@ -28,13 +28,21 @@ First, Install rust toolchain;
 tools/install.sh
 ```
 
-## 1. Install tools 🧰
-Then, build verus, verus-rustc (replacing rustc) and igvm tools and dependencies.
+## 1. Install Verus 🧰
+Install the Verus toolchain (verus, rust_verify, z3, cargo-verus, verusfmt) into `~/.cargo/bin`.
+By default this downloads the pinned prebuilt release:
+```
+tools/install_verus
+```
+Pass `--verus-dir PATH` (optionally with `--verus-rev REV`) to build Verus from a source checkout instead, or `--force` to reinstall when the expected version is already present. Run `tools/install_verus --help` for full usage.
+
+## 2. Install build tools 🧰
+Then, build verus-rustc (replacing rustc) and igvm tools and dependencies.
 ```
 tools/activate.sh
 ```
 
-## 2. Verify and Build ✔️ 🛠️
+## 3. Verify and Build ✔️ 🛠️
 
 Now, run verification checks and build the binary. 
 
@@ -77,14 +85,14 @@ or
 cd source/verismo_main; cargo build --feature noverify --release;
 ```
 
-## 3. Create VM image (skip if you run `make` or `make verify`)
+## 4. Create VM image (skip if you run `make` or `make verify`)
 
 1. Download linux submodule: `git submodule update --init richos/snplinux`
 2. Build guest OS and drivers: `make fs -f Makefile.default`
 1. Run `sh source/target/target/release/verismo/igvm.sh` to generate the verismo in IGVM format for Hyper-V: `source/target/target/release/verismo/verismo-rust.bin`
 2. Run `make fs` to generate a vhdx file  as filesystem for the VM: `richos/test-fs/verismo.vhdx`
 
-## 4. Deploy and run
+## 5. Deploy and run
 
 ### Requirements
 

source/.cargo/config.toml

@@ -1,12 +1,12 @@
-[unstable]
-build-std-features = ["compiler-builtins-mem"]
-build-std = ["core","alloc", "compiler_builtins"]
-unstable-options = true
-
 [build]
-target = "target.json"
+target = "x86_64-unknown-none"
 incremental = true
 
+[env]
+RUSTC_BOOTSTRAP = { value = "1", force = true }
+CARGO_UNSTABLE_JSON_TARGET_SPEC = { value = "true", force = true }
+CARGO_UNSTABLE_UNSTABLE_OPTIONS = { value = "true", force = true }
+
 [profile.dev]
 incremental = true
 debug-assertions = true

source/Cargo.toml

@@ -1,17 +1,29 @@
 [workspace]
+resolver = "2"
 members = [
     "verismo_main",
     "verismo",
-    "verismo_macro"
+    "verismo_macro",
+    "verismo_tspec"
 ]
 
 [workspace.dependencies]
-# Verus repos
-builtin = { git = "https://github.com/ziqiaozhou/verus", rev ="7c4a5274a4d74522f3965eb038bb7e22fa5eebef" }
-vstd = { git = "https://github.com/ziqiaozhou/verus", rev ="7c4a5274a4d74522f3965eb038bb7e22fa5eebef", features = ["alloc"], default-features = false }
-builtin_macros = { git = "https://github.com/ziqiaozhou/verus", rev ="7c4a5274a4d74522f3965eb038bb7e22fa5eebef" }
-syn_verus = { git = "https://github.com/ziqiaozhou/verus", rev ="7c4a5274a4d74522f3965eb038bb7e22fa5eebef", features = ["full", "visit-mut", "extra-traits"] }
-prettyplease_verus = { git = "https://github.com/ziqiaozhou/verus", rev ="7c4a5274a4d74522f3965eb038bb7e22fa5eebef" }
+# Verus crates from crates.io.
+# `builtin` and `builtin_macros` are kept as the local crate names (via the
+# `package = ...` rename) so we don't have to touch the `use builtin::*;` /
+# `use builtin_macros::*;` statements scattered through the codebase.
+builtin = { package = "verus_builtin", version = "=0.0.0-2026-05-17-0151", default-features = false }
+builtin_macros = { package = "verus_builtin_macros", version = "=0.0.0-2026-05-24-0157", features = ["vpanic"], default-features = false }
+verus_state_machines_macros = { version = "=0.0.0-2026-05-24-0157", default-features = false }
+vstd = { version = "=0.0.0-2026-05-24-0157", features = ["alloc", "allow_panic"], default-features = false }
+
+# `syn_verus` and `prettyplease_verus` are used only by the project's own
+# proc-macro crates (`verismo_macro` and `verismo_verus`). They are pinned to
+# the old syn-1.x-based fork because the rest of those macros are written
+# against the syn-1.x API (e.g. `token::Colon2`, `NestedMeta`, etc.); the
+# current upstream `verus_syn` is a syn-2.0 fork with a different API.
+syn_verus = { git = "https://github.com/verus-lang/verus", rev ="7c4a5274a4d74522f3965eb038bb7e22fa5eebef", features = ["full", "visit-mut", "extra-traits"] }
+prettyplease_verus = { git = "https://github.com/verus-lang/verus", rev ="7c4a5274a4d74522f3965eb038bb7e22fa5eebef" }
 
 # the profile used for `cargo build`
 [profile.dev]

source/rust-toolchain.toml

@@ -1,3 +1,3 @@
 [toolchain]
-channel = "nightly-2023-12-22"
+channel = "1.95.0"
 components = [ "rust-src", "rustc", "cargo", "rustfmt", "rustc-dev", "llvm-tools-preview" ] # TODO llvm-tools-preview may be unnecessary

source/verismo/Cargo.toml

@@ -1,6 +1,7 @@
 [package]
 name = "verismo"
 version = "0.1.0"
+edition = "2021"
 
 # See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
 
@@ -14,10 +15,11 @@ vstd = { workspace = true, features = ["alloc"], default-features = false }
 #builtin_macros = { path = "../../tools/verus/source/builtin_macros"}
 #vstd = {path = "../../tools/verus/source/vstd", features = ["alloc"], default-features = false }
 # Trusted
-hacl-sys = {git = "https://github.com/ziqiaozhou/hacl-packages", rev = "e12108dc04f79edb19c10f9ea4fa12bb49ca9da2"}
+hacl-sys = {git = "https://github.com/ziqiaozhou/hacl-packages", rev = "e02b4182d7afe346ebd04da6f96a54dc29488892"}
 # Useful macros
 verismo_macro = {path = "../verismo_macro"}
 verismo_verus = {path = "../verismo_verus"}
+verismo_tspec = {path = "../verismo_tspec"}
 paste = "1.0"
 seq-macro = "0.3"
 vops = {path = "../vops"}
@@ -32,4 +34,7 @@ noverify = []
 alloc = []
 
 [package.metadata.rust-analyzer]
-rustc_private=true
+rustc_private=true
+
+[package.metadata.verus]
+verify = true

source/verismo/src/addr_e/exe.rs

@@ -38,7 +38,6 @@ verismo_simple! {
             bit64_shl_values_auto();
         }
         let v: u64 = value.into();
-        assert(v.wf());
-        (align_down_by(v, PAGE_SIZE as u64) as usize)
+        align_down_by(v, PAGE_SIZE as u64) as usize
     }
 }