Merge pull request coconut-svsm#1038 from ziqiaozhou/cargo-verus

[verification] Support Verus's verita test via cargo-verus.

Author: joergroedel

.cargo/config.toml

@@ -14,5 +14,5 @@ rustflags = [
 ]
 
 [alias]
-verify = "v build --features verus"
+verify = "verus focus --features verus"
 xbuild = "run --package xbuild --release --"

.github/workflows/manual-verify.yml

@@ -36,18 +36,10 @@ jobs:
         run: |
           verusfmt --check `find ./ -name *.verus.rs` --verus-only
 
-      # cargo-v doesn't propagate the `cargo build` exit code, so we need
-      # to check stderr for errors.
-      # When https://github.com/microsoft/verismo/issues/23 will be fixed
-      # we can remove it.
       - name: Verify svsm with verus
-        run: |
-          cargo verify 2>&1 | tee verify.log
-          ! grep -q 'cargo build failed' verify.log
+        run: cargo verify
         working-directory: kernel
 
       - name: Verify extra proof libs with verus
-        run: |
-          cargo verify 2>&1 | tee verify.log
-          ! grep -q 'cargo build failed' verify.log
+        run: cargo verify
         working-directory: verification/verify_proof

Cargo.lock

@@ -101,10 +101,10 @@ zerocopy = { version = "0.8.2", features = ["derive"] }
 embedded-io = { version = "0.6.1" }
 
 # Verus repos
-verus_builtin = { version = "=0.0.0-2025-12-07-0054", default-features = false }
-verus_builtin_macros = { version = "=0.0.0-2025-12-07-0054", features = ["vpanic"], default-features = false }
-verus_state_machines_macros = { version = "=0.0.0-2025-11-23-0053", default-features = false }
-vstd = { version = "0.0.0-2025-12-07-0054", features = ["alloc", "allow_panic"], default-features = false }
+verus_builtin = { version = "=0.0.0-2026-04-12-0118", default-features = false }
+verus_builtin_macros = { version = "=0.0.0-2026-04-12-0118", features = ["vpanic"], default-features = false }
+verus_state_machines_macros = { version = "=0.0.0-2026-04-05-0114", default-features = false }
+vstd = { version = "=0.0.0-2026-04-12-0118", features = ["alloc", "allow_panic"], default-features = false }
 
 # Verification libs
 verify_proof = { path = "verification/verify_proof", default-features = false  }

Cargo.toml

@@ -31,9 +31,18 @@ Run the following commands to install Verus tools.
 
 ```shell
 cd svsm
-./scripts/vinstall.sh
+./scripts/vinstall.sh --use-prebuilt
 ```
 
+The script skips installation if a matching version of Verus is already installed.
+To force reinstallation (e.g., some verus-related tools are missing), add the --force flag.
+To build both Verus and Z3 from source instead of using prebuilt binaries, omit the --use-prebuilt flag. Building from source is required for CI.
+
+> Can I use latest Verus toolchain?
+>> The `vinstall.sh` script and our Cargo dependencies are pinned to a specific
+ Verus version, but newer releases may work as well. Verus runs cross-project CI
+ to check whether new Verus changes remain compatible with Coconut SVSM.
+
 > Why am I using a different Rust toolchain?
 >> Verus requires a specific version of Rust (e.g., 1.88.0) because it depends
   on the compiler’s internal libraries for verification. Thanks to Rust’s strong
@@ -50,29 +59,28 @@ cd svsm/kernel
 cargo verify
 ```
 
-By default, it only verifies the current crate (`cargo verify` is an alias of `cargo v --features verus`), while using spec/proof from external crates. To verify all external crates, run `cargo v --features verusall`
-
-
+By default, `cargo verify` verifies only the current crate. It is an alias for
+`cargo verus focus --features verus` and uses specifications and proofs from
+dependency crates without re-verifying them. To verify dependency crates as
+well, run `cargo verus verify --features verus`.
 
 ### Pass verus arguments for verification
 
 For debugging purposes, it is helpful to pass additional Verus arguments.
-You can specify extra arguments using the environmental variable
-{crate}_{lib/bin}_VERUS_ARGS for a specific crate
-{crate} or VERUS_ARGS for all crates.
+You can specify extra arguments using `cargo verify -- $extra_verus_args`
 
 **Examples**
 
 * Compiles a crate without verifying svsm crate using verus compilation:
 
     ```shell
-    svsm_lib_VERUS_ARGS="--no-verify" cargo verify
+    cargo verify -- --no-verify
     ```
 
 * Compiles a crate while only verifying address module in svsm crate:
 
     ```shell
-    svsm_lib_VERUS_ARGS="--verify-module address --verify-function VirtAddr::new" cargo verify
+    cargo verify -- --verify-only-module address --verify-function VirtAddr::new
     ```
 
 ### Build without verification

Documentation/docs/developer/VERIFICATION.md

@@ -87,5 +87,8 @@ sha2 = { workspace = true, features = ["force-soft"] }
 [build-dependencies]
 rustc_version = "0.4"
 
+[package.metadata.verus]
+verify = true
+
 [lints]
 workspace = true

kernel/Cargo.toml

@@ -95,10 +95,7 @@ enum PageType {
 #[verus_verify]
 impl TryFrom<u64> for PageType {
     type Error = AllocError;
-    #[verus_spec(ret =>
-        ensures
-            PageType::ens_try_from(val, ret),
-    )]
+    #[verus_spec]
     fn try_from(val: u64) -> Result<Self, Self::Error> {
         match val {
             v if v == Self::Free as u64 => Ok(Self::Free),
@@ -1210,7 +1207,7 @@ impl HeapMemoryRegion {
             old(self).req_allocate_pfn(pfn, order)
         ensures
             ret.is_ok() ==> old(self).ens_allocate_pfn(self, pfn, order, *perm),
-            !ret.is_ok() ==> old(self) === self,
+            !ret.is_ok() ==> *old(self) === *self,
     )]
     #[verus_verify(spinoff_prover, rlimit(2))]
     fn allocate_pfn(&mut self, pfn: usize, order: usize) -> Result<(), AllocError> {
@@ -1242,7 +1239,7 @@ impl HeapMemoryRegion {
 
         #[cfg_attr(verus_keep_ghost, verus_spec(
             invariant
-                self === old(self),
+                *self === *old(self),
                 self.wf_next_pages(),
                 self.req_allocate_pfn(pfn, order),
                 self.req_allocate_pfn(old_pfn, order),

kernel/src/mm/alloc.rs

@@ -6,6 +6,7 @@
 //
 // Proves the encode/decode functions for PageInfo used in alloc.rs.
 use vstd::simple_pptr::MemContents;
+use vstd::std_specs::convert::TryFromSpec;
 verus! {
 
 // prove the size of PageStorageType
@@ -408,22 +409,21 @@ impl SpecDecoderProof<PageStorageType> for ReservedInfo {
     }
 }
 
-impl PageType {
-    spec fn spec_try_from(val: u64) -> Option<Self> {
-        match val {
-            v if v == Self::Free as u64 => Some(Self::Free),
-            v if v == Self::Allocated as u64 => Some(Self::Allocated),
-            v if v == Self::SlabPage as u64 => Some(Self::SlabPage),
-            v if v == Self::Compound as u64 => Some(Self::Compound),
-            v if v == Self::File as u64 => Some(Self::File),
-            v if v == Self::Reserved as u64 => Some(Self::Reserved),
-            _ => None,
-        }
+impl vstd::std_specs::convert::TryFromSpecImpl<u64> for PageType {
+    closed spec fn obeys_try_from_spec() -> bool {
+        true
     }
 
-    pub closed spec fn ens_try_from(val: u64, ret: Result<Self, AllocError>) -> bool {
-        &&& ret.is_ok() == PageType::spec_try_from(val).is_some()
-        &&& ret.is_ok() ==> ret.unwrap() == PageType::spec_try_from(val).unwrap()
+    closed spec fn try_from_spec(val: u64) -> Result<Self, Self::Error> {
+        match val {
+            v if v == Self::Free as u64 => Ok(Self::Free),
+            v if v == Self::Allocated as u64 => Ok(Self::Allocated),
+            v if v == Self::SlabPage as u64 => Ok(Self::SlabPage),
+            v if v == Self::Compound as u64 => Ok(Self::Compound),
+            v if v == Self::File as u64 => Ok(Self::File),
+            v if v == Self::Reserved as u64 => Ok(Self::Reserved),
+            _ => Err(AllocError::InvalidPageType),
+        }
     }
 }
 
@@ -434,7 +434,7 @@ impl SpecDecoderProof<PageStorageType> for PageType {
 
     spec fn spec_decode(mem: PageStorageType) -> Option<Self> {
         let val = mem.0 & PageStorageType::TYPE_MASK;
-        PageType::spec_try_from(val)
+        PageType::try_from_spec(val).ok()
     }
 
     proof fn lemma_encode_decode(&self) {