toolchain: set x86 as verification target and use no_std accross the project

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"
@@ -49,4 +50,4 @@ codegen-units = 1
 
 [workspace.dependencies]
 # Verus
-vstd = { path = "tools/verus/source/vstd" }
+vstd = { path = "tools/verus/source/vstd", default-features = false, features = ["alloc"] }

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"
@@ -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"]
@@ -86,4 +87,4 @@ coverage = ["minicov"]
 workspace = true
 
 [package.metadata.verus]
-verify = true
+verify = true

ostd/specs/mm/page_table/owners.rs

@@ -1271,7 +1271,6 @@ impl<C: PageTableConfig> PageTableOwner<C> {
     /// `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<NR_ENTRIES>)
         requires
             self.pt_inv(),
@@ -1287,7 +1286,6 @@ impl<C: PageTableConfig> PageTableOwner<C> {
 
         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);
@@ -1306,7 +1304,6 @@ impl<C: PageTableConfig> PageTableOwner<C> {
             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::<C>(path);
             C::lemma_page_table_config_constant_properties();
             lemma_vaddr_strict_bound(path);
@@ -1351,9 +1348,8 @@ impl<C: PageTableConfig> PageTableOwner<C> {
             ;
             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));
             assert forall|m2: Mapping| #[trigger]
                 self.view_rec(path).contains(m2) implies m2.inv() by {
                 assert(self.view_rec(path).contains(m2) <==> m2 == m);

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<PageTableFrag<C>>) {
         // This proof touches several cursor snapshots. Keep their quantified invariants
         // opaque by default, then reveal only the concrete facts needed below. Leaving

rust-toolchain.toml

@@ -10,3 +10,4 @@ components = [
     "clippy",
     "rust-analyzer",
 ]
+targets = ["x86_64-unknown-none"]

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.
 //!

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 }

verified_libs/vstd_extra/src/array_ptr.rs

@@ -529,6 +529,7 @@ pub exec fn layout_for_array_is_valid<V: Sized, const N: usize>()
 }
 
 impl<V, const N: usize> ArrayPtr<V, N> {
+    #[cfg(feature = "std")]
     pub exec fn empty() -> ((res, perm): (ArrayPtr<V, N>, Tracked<PointsTo<V, N>>))
         requires
             layout::size_of::<[V; N]>() > 0,
@@ -582,6 +583,7 @@ impl<V, const N: usize> ArrayPtr<V, N> {
         ptr_mut_fill(ptr, Tracked(&mut perm.points_to), value);
     }
 
+    #[cfg(feature = "std")]
     pub exec fn new(dft: V) -> ((res, perm): (ArrayPtr<V, N>, Tracked<PointsTo<V, N>>)) where
         V: Copy,
 

verified_libs/vstd_extra/src/drop_tracking.rs

@@ -106,7 +106,7 @@ impl<T: TrackDrop> ManuallyDrop<T> {
             let tracked obligation = slot.tracked_obligation.get();
         }
         proof_with!(|= Tracked(obligation));
-        std::mem::ManuallyDrop::<T>::into_inner(slot.value)
+        core::mem::ManuallyDrop::<T>::into_inner(slot.value)
     }
 }
 

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<T>(b: Box<T>)
         #[trigger] *(b.deref_spec()) == *b,
 ;
 
-pub broadcast axiom fn rc_deref_spec<T>(r: std::rc::Rc<T>)
+pub broadcast axiom fn rc_deref_spec<T>(r: alloc::rc::Rc<T>)
     ensures
         #[trigger] *(r.deref_spec()) == *r,
 ;
 
-pub broadcast axiom fn arc_deref_spec<T>(a: std::sync::Arc<T>)
+pub broadcast axiom fn arc_deref_spec<T>(a: alloc::sync::Arc<T>)
     ensures
         #[trigger] *(a.deref_spec()) == *a,
 ;

verified_libs/vstd_extra/src/external/smart_ptr.rs

@@ -1,5 +1,6 @@
 use crate::ownership::*;
 use crate::raw_ptr_extra::*;
+use alloc::boxed::Box;
 use alloc::sync::Arc;
 use vstd::layout::valid_layout;
 use vstd::prelude::*;

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)]