From 8050584773cbf98be323bd12747c12f5dd02f575 Mon Sep 17 00:00:00 2001 From: rikosellic <64517311+rikosellic@users.noreply.github.com> Date: Mon, 3 Aug 2026 23:56:51 +0800 Subject: [PATCH 1/8] toolchain: set x86 as verification target and disable `std` in `vstd_extra` --- Cargo.lock | 4 ++-- Cargo.toml | 2 +- dv | 2 +- ostd/Cargo.toml | 6 +++--- rust-toolchain.toml | 1 + verified_libs/bitflags/src/lib.rs | 1 + verified_libs/vstd_extra/Cargo.toml | 4 ++++ verified_libs/vstd_extra/src/drop_tracking.rs | 2 +- verified_libs/vstd_extra/src/external/deref.rs | 5 +++-- verified_libs/vstd_extra/src/external/smart_ptr.rs | 3 ++- verified_libs/vstd_extra/src/lib.rs | 1 + 11 files changed, 20 insertions(+), 11 deletions(-) diff --git a/Cargo.lock b/Cargo.lock index 33630a226..f1945994d 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -586,9 +586,9 @@ checksum = "5a5f39404a5da50712a4c1eecf25e90dd62b613502b7e925fd4e4d19b5c96512" [[package]] name = "unwinding" -version = "0.2.5" +version = "0.2.6" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "51f06a05848f650946acef3bf525fe96612226b61f74ae23ffa4e98bfbb8ab3c" +checksum = "8393f2782b6060a807337ff353780c1ca15206f9ba2424df18cb6e733bd7b345" dependencies = [ "gimli 0.31.1", ] diff --git a/Cargo.toml b/Cargo.toml index d53e3d290..e1de5efbf 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -49,4 +49,4 @@ codegen-units = 1 [workspace.dependencies] # Verus -vstd = { path = "tools/verus/source/vstd" } +vstd = { path = "tools/verus/source/vstd", default-features = false, features = ["alloc"] } diff --git a/dv b/dv index 00d9bc7b5..dac47aff7 160000 --- a/dv +++ b/dv @@ -1 +1 @@ -Subproject commit 00d9bc7b52ec3bdb14fe9ca95bbbad901c99cc3b +Subproject commit dac47aff7102440aea661847f153cf17b8a3dedc diff --git a/ostd/Cargo.toml b/ostd/Cargo.toml index 1a09823b8..94a96e196 100644 --- a/ostd/Cargo.toml +++ b/ostd/Cargo.toml @@ -63,13 +63,13 @@ iced-x86 = { version = "1.21.0", default-features = false, features = [ "gas", ], optional = true } tdx-guest = { version = "0.2.1", optional = true } -unwinding = { version = "=0.2.5", default-features = false, features = ["fde-gnu-eh-frame-hdr", "hide-trace", "panic", "personality", "unwinder"] } +unwinding = { version = "=0.2.6", default-features = false, features = ["fde-gnu-eh-frame-hdr", "hide-trace", "panic", "personality", "unwinder"] } [target.riscv64imac-unknown-none-elf.dependencies] riscv = { version = "0.11.1", features = ["s-mode"] } sbi-rt = "0.0.3" fdt = { version = "0.1.5", features = ["pretty-printing"] } -unwinding = { version = "=0.2.5", default-features = false, features = ["fde-gnu-eh-frame-hdr", "hide-trace", "panic", "personality", "unwinder"] } +unwinding = { version = "=0.2.6", default-features = false, features = ["fde-gnu-eh-frame-hdr", "hide-trace", "panic", "personality", "unwinder"] } [target.loongarch64-unknown-none-softfloat.dependencies] loongArch64 = "0.2.5" @@ -86,4 +86,4 @@ coverage = ["minicov"] workspace = true [package.metadata.verus] -verify = true \ No newline at end of file +verify = true diff --git a/rust-toolchain.toml b/rust-toolchain.toml index adb122250..c1f2c875e 100644 --- a/rust-toolchain.toml +++ b/rust-toolchain.toml @@ -10,3 +10,4 @@ components = [ "clippy", "rust-analyzer", ] +targets = ["x86_64-unknown-none"] diff --git a/verified_libs/bitflags/src/lib.rs b/verified_libs/bitflags/src/lib.rs index 2d3a07f89..ad096f4bd 100644 --- a/verified_libs/bitflags/src/lib.rs +++ b/verified_libs/bitflags/src/lib.rs @@ -1,3 +1,4 @@ +#![no_std] #![allow(non_snake_case)] //! A verified version of the [`bitflags`](https://docs.rs/bitflags/latest/bitflags/) crate. //! diff --git a/verified_libs/vstd_extra/Cargo.toml b/verified_libs/vstd_extra/Cargo.toml index bb8cee3ba..2bb81040e 100644 --- a/verified_libs/vstd_extra/Cargo.toml +++ b/verified_libs/vstd_extra/Cargo.toml @@ -6,5 +6,9 @@ edition = "2021" [package.metadata.verus] verify = true +[features] +default = [] +std = ["vstd/std"] + [dependencies] vstd = { workspace = true } diff --git a/verified_libs/vstd_extra/src/drop_tracking.rs b/verified_libs/vstd_extra/src/drop_tracking.rs index 4fed0edec..c3ffae4a6 100644 --- a/verified_libs/vstd_extra/src/drop_tracking.rs +++ b/verified_libs/vstd_extra/src/drop_tracking.rs @@ -106,7 +106,7 @@ impl ManuallyDrop { let tracked obligation = slot.tracked_obligation.get(); } proof_with!(|= Tracked(obligation)); - std::mem::ManuallyDrop::::into_inner(slot.value) + core::mem::ManuallyDrop::::into_inner(slot.value) } } diff --git a/verified_libs/vstd_extra/src/external/deref.rs b/verified_libs/vstd_extra/src/external/deref.rs index 7d5bebe2d..0479156d3 100644 --- a/verified_libs/vstd_extra/src/external/deref.rs +++ b/verified_libs/vstd_extra/src/external/deref.rs @@ -2,6 +2,7 @@ note = "If you can, do not use this module as it adds assumptions about the core of Rust's deref semantics." )] +use alloc::boxed::Box; use core::hint::spin_loop; use core::mem::ManuallyDrop; use core::ops::Deref; @@ -40,12 +41,12 @@ pub broadcast axiom fn box_deref_spec(b: Box) #[trigger] *(b.deref_spec()) == *b, ; -pub broadcast axiom fn rc_deref_spec(r: std::rc::Rc) +pub broadcast axiom fn rc_deref_spec(r: alloc::rc::Rc) ensures #[trigger] *(r.deref_spec()) == *r, ; -pub broadcast axiom fn arc_deref_spec(a: std::sync::Arc) +pub broadcast axiom fn arc_deref_spec(a: alloc::sync::Arc) ensures #[trigger] *(a.deref_spec()) == *a, ; diff --git a/verified_libs/vstd_extra/src/external/smart_ptr.rs b/verified_libs/vstd_extra/src/external/smart_ptr.rs index e205c935a..a71a4fba9 100644 --- a/verified_libs/vstd_extra/src/external/smart_ptr.rs +++ b/verified_libs/vstd_extra/src/external/smart_ptr.rs @@ -1,6 +1,7 @@ +use alloc::boxed::Box; +use alloc::sync::Arc; use crate::ownership::*; use crate::raw_ptr_extra::*; -use alloc::sync::Arc; use vstd::layout::valid_layout; use vstd::prelude::*; use vstd::raw_ptr::*; diff --git a/verified_libs/vstd_extra/src/lib.rs b/verified_libs/vstd_extra/src/lib.rs index fa427fe3b..68cf8e5ae 100644 --- a/verified_libs/vstd_extra/src/lib.rs +++ b/verified_libs/vstd_extra/src/lib.rs @@ -1,6 +1,7 @@ //! The "extra standard library" for [Verus](https://github.com/verus-lang/verus). //! Contains various utilities and general datatypes for proofs useful in Asterinas verification, //! as well as extending [Verus standard library(vstd)](https://verus-lang.github.io/verus/verusdoc/vstd) with additional functionality. +#![no_std] #![feature(nonzero_internals)] #![feature(sized_hierarchy)] #![feature(proc_macro_hygiene)] From f2c0eafeeab0c2924473fc986d0d17338b44c37b Mon Sep 17 00:00:00 2001 From: rikosellic <64517311+rikosellic@users.noreply.github.com> Date: Tue, 4 Aug 2026 00:06:49 +0800 Subject: [PATCH 2/8] fix --- verified_libs/vstd_extra/src/array_ptr.rs | 2 ++ 1 file changed, 2 insertions(+) diff --git a/verified_libs/vstd_extra/src/array_ptr.rs b/verified_libs/vstd_extra/src/array_ptr.rs index fd0bfe24b..4dd68101a 100644 --- a/verified_libs/vstd_extra/src/array_ptr.rs +++ b/verified_libs/vstd_extra/src/array_ptr.rs @@ -529,6 +529,7 @@ pub exec fn layout_for_array_is_valid() } impl ArrayPtr { + #[cfg(feature = "std")] pub exec fn empty() -> ((res, perm): (ArrayPtr, Tracked>)) requires layout::size_of::<[V; N]>() > 0, @@ -582,6 +583,7 @@ impl ArrayPtr { ptr_mut_fill(ptr, Tracked(&mut perm.points_to), value); } + #[cfg(feature = "std")] pub exec fn new(dft: V) -> ((res, perm): (ArrayPtr, Tracked>)) where V: Copy, From 34b9c876bb55fb9857072af1913145b2c4ff4136 Mon Sep 17 00:00:00 2001 From: rikosellic <64517311+rikosellic@users.noreply.github.com> Date: Tue, 4 Aug 2026 08:09:54 +0800 Subject: [PATCH 3/8] fix --- ostd/specs/mm/page_table/owners.rs | 5 +---- verified_libs/vstd_extra/src/external/smart_ptr.rs | 4 ++-- 2 files changed, 3 insertions(+), 6 deletions(-) diff --git a/ostd/specs/mm/page_table/owners.rs b/ostd/specs/mm/page_table/owners.rs index 6ac48625d..35eb7ca97 100644 --- a/ostd/specs/mm/page_table/owners.rs +++ b/ostd/specs/mm/page_table/owners.rs @@ -1305,8 +1305,6 @@ impl PageTableOwner { assert(self.view_rec(path) == set![m]); let ps = page_size(pt_level) as int; vstd_extra::arithmetic::lemma_mod_0_add(frame.mapped_pa as int, ps, ps); - // Bridge `vaddr_of(path) == vaddr(path) + LB * 2^48`. - lemma_vaddr_of_eq_int::(path); C::lemma_page_table_config_constant_properties(); lemma_vaddr_strict_bound(path); let lb = C::LEADING_BITS_spec() as int; @@ -1350,9 +1348,8 @@ impl PageTableOwner { ; vstd::arithmetic::mul::lemma_mul_inequality(1, q, ps); vstd::arithmetic::mul::lemma_mul_inequality(lb, 0xffffint, 0x1_0000_0000_0000int); - assert(0x1_0000_0000_0000int + 0xffffint * 0x1_0000_0000_0000int - == 0x1_0000_0000_0000_0000int) by (compute_only); vstd_extra::arithmetic::lemma_mod_0_add(m.va_range.start, ps, ps); + assert(set![4096, 2097152, 1073741824].contains(m.page_size)); } else if self.0.value().is_node() && path.len() < INC_LEVELS - 1 { assert forall|m: Mapping| #[trigger] self.view_rec(path).contains(m) implies m.inv() by { diff --git a/verified_libs/vstd_extra/src/external/smart_ptr.rs b/verified_libs/vstd_extra/src/external/smart_ptr.rs index a71a4fba9..711c90527 100644 --- a/verified_libs/vstd_extra/src/external/smart_ptr.rs +++ b/verified_libs/vstd_extra/src/external/smart_ptr.rs @@ -1,7 +1,7 @@ -use alloc::boxed::Box; -use alloc::sync::Arc; use crate::ownership::*; use crate::raw_ptr_extra::*; +use alloc::boxed::Box; +use alloc::sync::Arc; use vstd::layout::valid_layout; use vstd::prelude::*; use vstd::raw_ptr::*; From 241fad930f660c35d3a3ea407e5a51fe778977a1 Mon Sep 17 00:00:00 2001 From: rikosellic <64517311+rikosellic@users.noreply.github.com> Date: Tue, 4 Aug 2026 11:15:16 +0800 Subject: [PATCH 4/8] Minor --- Cargo.toml | 1 + ostd/specs/mm/page_table/owners.rs | 1 - 2 files changed, 1 insertion(+), 1 deletion(-) diff --git a/Cargo.toml b/Cargo.toml index e1de5efbf..0963ca334 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -19,6 +19,7 @@ exclude = [ [workspace.lints.rust] unsafe_op_in_unsafe_fn = "warn" +unexpected_cfgs = { level = "warn", check-cfg = ["cfg(ktest)"] } [workspace.lints.clippy] allow_attributes = "warn" diff --git a/ostd/specs/mm/page_table/owners.rs b/ostd/specs/mm/page_table/owners.rs index 35eb7ca97..8d34f217a 100644 --- a/ostd/specs/mm/page_table/owners.rs +++ b/ostd/specs/mm/page_table/owners.rs @@ -1286,7 +1286,6 @@ impl PageTableOwner { if self.0.value().is_frame() { lemma_page_size_spec_values(); - ; let frame = self.0.value().frame(); let pt_level = (INC_LEVELS - path.len()) as PagingLevel; Self::lemma_vaddr_path_alignment_and_bound(path); From 396f391fc9510b8fcd4c5f87feceee78f8471b49 Mon Sep 17 00:00:00 2001 From: rikosellic <64517311+rikosellic@users.noreply.github.com> Date: Tue, 4 Aug 2026 11:23:53 +0800 Subject: [PATCH 5/8] suppress another warning --- ostd/Cargo.toml | 1 + 1 file changed, 1 insertion(+) diff --git a/ostd/Cargo.toml b/ostd/Cargo.toml index 94a96e196..f1344922b 100644 --- a/ostd/Cargo.toml +++ b/ostd/Cargo.toml @@ -78,6 +78,7 @@ fdt = { version = "0.1.5", features = ["pretty-printing"] } [features] # default = ["cvm_guest"] default = [] +allow_panic = [] # The guest OS support for Confidential VMs (CVMs), e.g., Intel TDX cvm_guest = ["dep:tdx-guest", "dep:iced-x86"] coverage = ["minicov"] From 3902130caee903ae965de6504c64d4bc25ba2e28 Mon Sep 17 00:00:00 2001 From: rikosellic <64517311+rikosellic@users.noreply.github.com> Date: Tue, 4 Aug 2026 12:12:40 +0800 Subject: [PATCH 6/8] fix an error --- ostd/specs/mm/page_table/owners.rs | 1 + 1 file changed, 1 insertion(+) diff --git a/ostd/specs/mm/page_table/owners.rs b/ostd/specs/mm/page_table/owners.rs index 0cb397f01..dba7e8a83 100644 --- a/ostd/specs/mm/page_table/owners.rs +++ b/ostd/specs/mm/page_table/owners.rs @@ -1305,6 +1305,7 @@ impl PageTableOwner { assert(self.view_rec(path) == set![m]); let ps = page_size(pt_level) as int; vstd_extra::arithmetic::lemma_mod_0_add(frame.mapped_pa as int, ps, ps); + lemma_vaddr_of_eq_int::(path); C::lemma_page_table_config_constant_properties(); lemma_vaddr_strict_bound(path); let lb = C::LEADING_BITS_spec() as int; From 662905e5adfb1539876bd4eb9a9f7819effc8441 Mon Sep 17 00:00:00 2001 From: Marsman1996 Date: Tue, 4 Aug 2026 13:05:12 +0800 Subject: [PATCH 7/8] chore: restore the rlimit --- ostd/specs/mm/page_table/owners.rs | 1 - ostd/src/mm/page_table/cursor/mod.rs | 2 +- 2 files changed, 1 insertion(+), 2 deletions(-) diff --git a/ostd/specs/mm/page_table/owners.rs b/ostd/specs/mm/page_table/owners.rs index dba7e8a83..4c335f6c1 100644 --- a/ostd/specs/mm/page_table/owners.rs +++ b/ostd/specs/mm/page_table/owners.rs @@ -1271,7 +1271,6 @@ impl PageTableOwner { /// `parent_level < NR_LEVELS` constraint plus the arithmetic identity /// `page_size(k) ∈ {4K, 2M, 1G}` for `k ∈ {1, 2, 3}`, and VA alignment /// + no-overflow via `lemma_vaddr_path_alignment_and_bound`. - #[verifier::rlimit(200)] pub proof fn view_rec_mapping_inv(self, path: TreePath) requires self.pt_inv(), diff --git a/ostd/src/mm/page_table/cursor/mod.rs b/ostd/src/mm/page_table/cursor/mod.rs index 408650daf..1e8c9e8ed 100644 --- a/ostd/src/mm/page_table/cursor/mod.rs +++ b/ostd/src/mm/page_table/cursor/mod.rs @@ -3532,7 +3532,7 @@ impl<'rcu, C: PageTableConfig, A: InAtomicMode> CursorMut<'rcu, C, A> { }, )] #[verifier::spinoff_prover] - #[verifier::rlimit(600)] + #[verifier::rlimit(50)] pub unsafe fn take_next(&mut self, len: usize) -> (r: Option>) { // This proof touches several cursor snapshots. Keep their quantified invariants // opaque by default, then reveal only the concrete facts needed below. Leaving From 57c396bcabc6281320f2dcdbaa6a00a21987d1d7 Mon Sep 17 00:00:00 2001 From: rikosellic <64517311+rikosellic@users.noreply.github.com> Date: Tue, 4 Aug 2026 14:09:54 +0800 Subject: [PATCH 8/8] Update dv --- dv | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/dv b/dv index dac47aff7..9205a9e0b 160000 --- a/dv +++ b/dv @@ -1 +1 @@ -Subproject commit dac47aff7102440aea661847f153cf17b8a3dedc +Subproject commit 9205a9e0b04730749bf65724a7df5ea98f768dbe