From eef353dbcb0115ad84f41f150dda8e2a46ac4310 Mon Sep 17 00:00:00 2001 From: Ziqiao Zhou Date: Sat, 9 May 2026 16:31:00 +0000 Subject: [PATCH 1/2] paging: move address, sizes, and utility types to paging crate Create the paging crate and move foundational types from the kernel: - address.rs (PhysAddr, VirtAddr, Address trait), remove unused VirtPhysPair which was introduced 2 years ago and is no longer used by svsm code. - sizes.rs (PAGE_SIZE, PAGE_SHIFT, size constants) - util.rs (align_up, align_down, page_align_up, overlap, bit_mask) - Associated verus spec/proof files for verification - paging: move Verus specs and proofs into dedicated dirs - gate proofs and spec with verus_only The kernel re-exports these types to maintain API compatibility. Unit tests for utility functions move to paging/src/util.rs. Signed-off-by: Ziqiao Zhou --- Cargo.lock | 13 +++ Cargo.toml | 3 + kernel/Cargo.toml | 4 +- kernel/src/lib.rs | 2 +- kernel/src/types.rs | 31 +---- kernel/src/utils/util.rs | 92 +-------------- paging/Cargo.toml | 23 ++++ {kernel => paging}/src/address.rs | 24 +--- paging/src/lib.rs | 9 ++ .../src/proofs/align.rs | 7 +- .../src/proofs/sizes.rs | 3 + paging/src/sizes.rs | 43 +++++++ .../src/specs/address.rs | 7 +- .../src/specs/address_inner.rs | 10 +- .../src/specs/align.rs | 9 +- paging/src/util.rs | 108 ++++++++++++++++++ 16 files changed, 236 insertions(+), 152 deletions(-) create mode 100644 paging/Cargo.toml rename {kernel => paging}/src/address.rs (97%) create mode 100644 paging/src/lib.rs rename kernel/src/utils/util.proof.verus.rs => paging/src/proofs/align.rs (98%) rename kernel/src/types.verus.rs => paging/src/proofs/sizes.rs (91%) create mode 100644 paging/src/sizes.rs rename kernel/src/address.verus.rs => paging/src/specs/address.rs (99%) rename kernel/src/address_inner.verus.rs => paging/src/specs/address_inner.rs (94%) rename kernel/src/utils/util.verus.rs => paging/src/specs/align.rs (95%) create mode 100644 paging/src/util.rs diff --git a/Cargo.lock b/Cargo.lock index e2c41d5593..2635303ba3 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -1469,6 +1469,18 @@ dependencies = [ "zerocopy", ] +[[package]] +name = "paging" +version = "0.1.0" +dependencies = [ + "bitflags", + "verify_external", + "verify_proof", + "verus_stub", + "vstd", + "zerocopy", +] + [[package]] name = "pastey" version = "0.2.1" @@ -1951,6 +1963,7 @@ dependencies = [ "libtcgtpm", "log", "packit", + "paging", "release", "rustc-demangle", "rustc_version", diff --git a/Cargo.toml b/Cargo.toml index 3f36440140..93ae8bdafd 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -9,6 +9,7 @@ members = [ "boot/bootimg", "boot/defs", "cpuarch", + "paging", # binary targets "stage1", "kernel", @@ -55,6 +56,7 @@ bldr = { path = "boot/bldr" } bootdefs = { path = "boot/defs" } bootimg = { path = "boot/bootimg" } cpuarch = { path = "cpuarch" } +paging = { path = "paging" } test = { path = "test" } svsm = { path = "kernel" } elf = { path = "elf" } @@ -127,6 +129,7 @@ missing_debug_implementations = { level = "deny", priority = 50 } single_use_lifetimes = { level = "warn", priority = 125 } trivial-numeric-casts = { level = "deny", priority = 10 } unsafe_op_in_unsafe_fn = { level = "deny", priority = 2 } +unexpected_cfgs = { level = "warn", check-cfg = ['cfg(verus_only)'] } [workspace.lints.clippy] await_holding_lock = "warn" diff --git a/kernel/Cargo.toml b/kernel/Cargo.toml index ec36f40595..e0e76a02b4 100644 --- a/kernel/Cargo.toml +++ b/kernel/Cargo.toml @@ -16,6 +16,8 @@ doctest = true bootdefs.workspace = true bootimg.workspace = true cpuarch.workspace = true +paging.workspace = true + libaproxy = { workspace = true, optional = true } elf.workspace = true syscall.workspace = true @@ -74,7 +76,7 @@ enable-gdb = ["dep:gdbstub", "dep:gdbstub_arch"] vtpm = ["dep:libtcgtpm"] nosmep = [] nosmap = [] -verus_all = ["verus_builtin", "verus_builtin_macros", "vstd", "verify_proof/verus", "verify_external/verus", "verus_stub/disable"] +verus_all = ["verus_builtin", "verus_builtin_macros", "vstd", "verify_proof/verus", "verify_external/verus", "verus_stub/disable", "paging/verus"] verus = ["verus_all", "verify_proof/noverify", "verify_external/noverify"] noverify = [] virtio-drivers = ["dep:virtio-drivers"] diff --git a/kernel/src/lib.rs b/kernel/src/lib.rs index fa29d11cf5..38fb0725f4 100644 --- a/kernel/src/lib.rs +++ b/kernel/src/lib.rs @@ -15,7 +15,7 @@ #![cfg_attr(verus_keep_ghost, feature(proc_macro_hygiene))] pub mod acpi; -pub mod address; +pub use paging::address; #[cfg(feature = "attest")] pub mod attest; #[cfg(feature = "block")] diff --git a/kernel/src/types.rs b/kernel/src/types.rs index cd369008e4..d19d8c7aa8 100644 --- a/kernel/src/types.rs +++ b/kernel/src/types.rs @@ -7,35 +7,8 @@ use crate::error::SvsmError; use crate::sev::vmsa::VMPL_MAX; -use verus_stub::*; -#[cfg(verus_keep_ghost)] -include!("types.verus.rs"); - -verus! { - -pub const PAGE_SHIFT: usize = 12; -pub const PAGE_SHIFT_2M: usize = 21; -pub const PAGE_SHIFT_1G: usize = 30; -pub const PAGE_SIZE: usize = 1 << PAGE_SHIFT; -pub const PAGE_SIZE_2M: usize = 1 << PAGE_SHIFT_2M; -pub const PAGE_SIZE_1G: usize = 1 << PAGE_SHIFT_1G; - -} - -#[derive(Clone, Copy, Debug, PartialEq, Eq)] -pub enum PageSize { - Regular, - Huge, -} - -impl From for usize { - fn from(psize: PageSize) -> Self { - match psize { - PageSize::Regular => PAGE_SIZE, - PageSize::Huge => PAGE_SIZE_2M, - } - } -} +// Re-export page types from paging crate +pub use paging::sizes::*; #[expect(clippy::identity_op)] pub const SVSM_CS: u16 = 1 * 8; diff --git a/kernel/src/utils/util.rs b/kernel/src/utils/util.rs index f1a38d2755..26844e0ecf 100644 --- a/kernel/src/utils/util.rs +++ b/kernel/src/utils/util.rs @@ -5,72 +5,9 @@ // Author: Joerg Roedel use crate::address::{Address, VirtAddr}; -use crate::types::PAGE_SIZE; -use core::ops::{Add, BitAnd, Not, Sub}; -use verus_stub::*; - -#[cfg(verus_keep_ghost)] -include!("util.verus.rs"); - -#[verus_spec(ret => - requires - align_up_requires((addr, align)), - ensures - align_up_ens((addr, align), ret), -)] -pub fn align_up(addr: T, align: T) -> T -where - T: Add + Sub + BitAnd + Not + From + Copy, -{ - let mask: T = align - T::from(1u8); - (addr + mask) & !mask -} - -#[verus_spec(ret => - requires - align_down_requires((addr, align)), - ensures - align_down_ens((addr, align), ret), -)] -pub fn align_down(addr: T, align: T) -> T -where - T: Sub + Not + BitAnd + From + Copy, -{ - addr & !(align - T::from(1u8)) -} - -#[verus_spec(ret => - requires - is_aligned_requires((addr, align)), - ensures - is_aligned_ens((addr, align), ret) -)] -pub fn is_aligned(addr: T, align: T) -> bool -where - T: Sub + BitAnd + PartialEq + From, -{ - (addr & (align - T::from(1u8))) == T::from(0u8) -} - -pub fn page_align_up(x: usize) -> usize { - align_up(x, PAGE_SIZE) -} - -pub fn round_to_pages(x: usize) -> usize { - page_align_up(x) / PAGE_SIZE -} - -pub fn page_offset(x: usize) -> usize { - x & (PAGE_SIZE - 1) -} - -pub fn overlap(x1: T, x2: T, y1: T, y2: T) -> bool -where - T: PartialOrd, -{ - x1 <= y2 && y1 <= x2 -} +// Re-export alignment utilities from paging crate +pub use paging::util::*; /// # Safety /// @@ -113,32 +50,9 @@ macro_rules! BIT_MASK { #[cfg(test)] mod tests { + use crate::address::VirtAddr; use crate::utils::util::*; - #[test] - fn test_mem_utils() { - // Align up - assert_eq!(align_up(7, 4), 8); - assert_eq!(align_up(15, 8), 16); - assert_eq!(align_up(10, 2), 10); - // Align down - assert_eq!(align_down(7, 4), 4); - assert_eq!(align_down(15, 8), 8); - assert_eq!(align_down(10, 2), 10); - // Page align up - assert_eq!(page_align_up(4096), 4096); - assert_eq!(page_align_up(4097), 8192); - assert_eq!(page_align_up(0), 0); - // Page offset - assert_eq!(page_offset(4096), 0); - assert_eq!(page_offset(4097), 1); - assert_eq!(page_offset(0), 0); - // Overlaps - assert!(overlap(1, 5, 3, 6)); - assert!(overlap(0, 10, 5, 15)); - assert!(!overlap(1, 5, 6, 8)); - } - #[test] fn test_zero_mem_region() { let mut data: [u8; 10] = [1; 10]; diff --git a/paging/Cargo.toml b/paging/Cargo.toml new file mode 100644 index 0000000000..2d3d98ef24 --- /dev/null +++ b/paging/Cargo.toml @@ -0,0 +1,23 @@ +[package] +name = "paging" +version = "0.1.0" +edition.workspace = true +description = "Generic page table structures for Rust OS projects" + +[dependencies] +bitflags.workspace = true +zerocopy.workspace = true +verus_stub.workspace = true +verify_proof = { workspace = true, optional = true } +verify_external = { workspace = true, optional = true } +vstd = { workspace = true, optional = true } + +[features] +default = [] +verus = ["verify_proof/verus", "verify_external/verus", "vstd", "verus_stub/disable"] + +[package.metadata.verus] +verify = true + +[lints] +workspace = true diff --git a/kernel/src/address.rs b/paging/src/address.rs similarity index 97% rename from kernel/src/address.rs rename to paging/src/address.rs index 83be81a861..58eda61f20 100644 --- a/kernel/src/address.rs +++ b/paging/src/address.rs @@ -4,9 +4,8 @@ // // Author: Carlos López -use crate::mm::virt_to_phys; -use crate::types::{PAGE_SHIFT, PAGE_SIZE}; -use crate::utils::{align_down, align_up, is_aligned}; +use crate::sizes::{PAGE_SHIFT, PAGE_SIZE}; +use crate::util::{align_down, align_up, is_aligned}; use core::fmt; use core::ops; @@ -17,8 +16,8 @@ use verus_stub::*; use zerocopy::FromBytes; -#[cfg(verus_keep_ghost)] -include!("address.verus.rs"); +#[cfg(verus_only)] +include!("specs/address.rs"); // The backing type to represent an address; type InnerAddr = usize; @@ -599,18 +598,3 @@ impl Address for VirtAddr { .map(|addr| sign_extend(addr).into()) } } - -#[derive(Clone, Copy, Debug)] -pub struct VirtPhysPair { - pub vaddr: VirtAddr, - pub paddr: PhysAddr, -} - -impl VirtPhysPair { - pub fn new(vaddr: VirtAddr) -> Self { - Self { - vaddr, - paddr: virt_to_phys(vaddr), - } - } -} diff --git a/paging/src/lib.rs b/paging/src/lib.rs new file mode 100644 index 0000000000..afff84e34e --- /dev/null +++ b/paging/src/lib.rs @@ -0,0 +1,9 @@ +// SPDX-License-Identifier: MIT + +//! This crate provides page table–related functions and data structures. + +#![no_std] + +pub mod address; +pub mod sizes; +pub mod util; diff --git a/kernel/src/utils/util.proof.verus.rs b/paging/src/proofs/align.rs similarity index 98% rename from kernel/src/utils/util.proof.verus.rs rename to paging/src/proofs/align.rs index 2e341c6506..eb623f6b39 100644 --- a/kernel/src/utils/util.proof.verus.rs +++ b/paging/src/proofs/align.rs @@ -4,7 +4,10 @@ // // Author: Ziqiao Zhou // -// Proofs related to util.rs +// Proofs related to alignment helpers. +use super::*; +use verus_stub::*; + verus! { /// A meaningful align_down should be verified to equal to align_up_integer_ens @@ -35,7 +38,7 @@ pub broadcast proof fn proof_align_up(val: T, align: T, ret: T::lemma_align_up(val, align, ret); } -broadcast group group_align_proofs { +pub broadcast group group_align_proofs { verify_proof::bits::lemma_bit_u64_not_is_sub, verify_proof::bits::lemma_bit_u64_shl_values, verify_proof::bits::lemma_bit_u64_and_mask, diff --git a/kernel/src/types.verus.rs b/paging/src/proofs/sizes.rs similarity index 91% rename from kernel/src/types.verus.rs rename to paging/src/proofs/sizes.rs index 62175f51dc..0ba2c125ea 100644 --- a/kernel/src/types.verus.rs +++ b/paging/src/proofs/sizes.rs @@ -3,6 +3,9 @@ // Copyright (c) Microsoft Corporation // // Author: Ziqiao Zhou +use super::PAGE_SIZE; +use verus_stub::*; + verus! { pub broadcast group group_types_proof { diff --git a/paging/src/sizes.rs b/paging/src/sizes.rs new file mode 100644 index 0000000000..1e5741c6b9 --- /dev/null +++ b/paging/src/sizes.rs @@ -0,0 +1,43 @@ +// SPDX-License-Identifier: MIT OR Apache-2.0 +// +// Copyright (c) 2022-2023 SUSE LLC +// +// Author: Joerg Roedel + +use verus_stub::*; + +#[cfg(verus_only)] +#[path = "proofs/sizes.rs"] +mod sizes_spec_defs; +#[cfg(verus_only)] +pub use sizes_spec_defs::*; +#[cfg(verus_only)] +verus! { + broadcast use sizes_spec_defs::group_types_proof; +} + +verus! { + +pub const PAGE_SHIFT: usize = 12; +pub const PAGE_SHIFT_2M: usize = 21; +pub const PAGE_SHIFT_1G: usize = 30; +pub const PAGE_SIZE: usize = 1 << PAGE_SHIFT; +pub const PAGE_SIZE_2M: usize = 1 << PAGE_SHIFT_2M; +pub const PAGE_SIZE_1G: usize = 1 << PAGE_SHIFT_1G; + +} + +#[derive(Clone, Copy, Debug, PartialEq, Eq)] +pub enum PageSize { + Regular, + Huge, +} + +impl From for usize { + fn from(psize: PageSize) -> Self { + match psize { + PageSize::Regular => PAGE_SIZE, + PageSize::Huge => PAGE_SIZE_2M, + } + } +} diff --git a/kernel/src/address.verus.rs b/paging/src/specs/address.rs similarity index 99% rename from kernel/src/address.verus.rs rename to paging/src/specs/address.rs index 9f4cefd106..3802759780 100644 --- a/kernel/src/address.verus.rs +++ b/paging/src/specs/address.rs @@ -4,7 +4,7 @@ // // Author: Ziqiao Zhou // -use crate::utils::util::{ +use crate::util::{ align_down_integer_ens, align_up_integer_ens, proof_align_down, proof_align_up, }; use verify_external::convert::{exists_into, forall_into}; @@ -26,7 +26,7 @@ pub broadcast group sign_extend_proof { } pub broadcast group address_align_proof { - crate::types::group_types_proof, + crate::sizes::group_types_proof, verify_proof::bits::lemma_bit_usize_and_mask_is_mod, proof_align_up, proof_align_down, @@ -52,7 +52,8 @@ broadcast use vaddr_impl_proof; /// Define a broadcast function and its related spec function calls in a inner /// module to avoid cyclic self-reference -mod address_spec { include!("address_inner.verus.rs"); } +#[path = "address_inner.rs"] +mod address_spec; pub use address_spec::*; diff --git a/kernel/src/address_inner.verus.rs b/paging/src/specs/address_inner.rs similarity index 94% rename from kernel/src/address_inner.verus.rs rename to paging/src/specs/address_inner.rs index 1ae02f6543..8d570af599 100644 --- a/kernel/src/address_inner.verus.rs +++ b/paging/src/specs/address_inner.rs @@ -123,7 +123,7 @@ pub broadcast proof fn reveal_pfn(addr: usize) #[verifier(inline)] pub open spec fn align_requires(align: InnerAddr) -> bool { - crate::utils::util::align_requires(align as u64) + crate::util::align_requires(align as u64) } pub open spec fn addr_align_up_requires(addr: A, align: InnerAddr) -> bool { @@ -141,7 +141,7 @@ pub broadcast proof fn lemma_align_up_requires( #[trigger] addr_align_up_requires(addr, align), A::into.ensures((addr,), iaddr), ensures - #[trigger] crate::utils::util::align_up_requires((iaddr, align)), + #[trigger] crate::util::align_up_requires((iaddr, align)), { assert forall|one: usize| call_ensures(usize::from, (1u8,), one) implies #[trigger] align.sub_req(one) by { @@ -157,7 +157,7 @@ pub open spec fn addr_align_up_impl(addr: A, align: InnerAddr, r &&& exists|iaddr: InnerAddr, iret: InnerAddr| { &&& A::into.ensures((addr,), iaddr) - &&& #[trigger] crate::utils::util::align_up_ens((iaddr, align), iret) + &&& #[trigger] crate::util::align_up_ens((iaddr, align), iret) &&& A::from.ensures((iret,), ret) } } @@ -200,10 +200,10 @@ pub broadcast proof fn lemma_align_up_ens(addr: A, align: InnerA let (iaddr, iret) = choose|iaddr: InnerAddr, iret: InnerAddr| { &&& A::into.ensures((addr,), iaddr) - &&& crate::utils::util::align_up_ens((iaddr, align), iret) + &&& crate::util::align_up_ens((iaddr, align), iret) &&& A::from.ensures((iret,), ret) }; - crate::utils::util::proof_align_up(iaddr, align, iret); + crate::util::proof_align_up(iaddr, align, iret); } } // verus! diff --git a/kernel/src/utils/util.verus.rs b/paging/src/specs/align.rs similarity index 95% rename from kernel/src/utils/util.verus.rs rename to paging/src/specs/align.rs index 81d63df600..a5bd03e228 100644 --- a/kernel/src/utils/util.verus.rs +++ b/paging/src/specs/align.rs @@ -4,7 +4,9 @@ // // Author: Ziqiao Zhou // -// Specifications related to util.rs that are used in proof_align_down and proof_align_up. +// Specifications related to alignment helpers that are used in proof_align_down and proof_align_up. +use core::ops::{Add, BitAnd, Not, Sub}; +use verus_stub::*; use vstd::std_specs::ops::{AddSpec, BitAndSpec, NotSpec, SubSpec}; #[verus_verify] @@ -154,4 +156,7 @@ pub open spec fn spec_is_aligned(val: T, align: T) -> bool where T: IsAligned } } // verus! -include!("util.proof.verus.rs"); +#[path = "../proofs/align.rs"] +mod align_proofs; + +pub use align_proofs::*; diff --git a/paging/src/util.rs b/paging/src/util.rs new file mode 100644 index 0000000000..2da6ac089b --- /dev/null +++ b/paging/src/util.rs @@ -0,0 +1,108 @@ +// SPDX-License-Identifier: MIT OR Apache-2.0 +// +// Copyright (c) 2022-2023 SUSE LLC +// +// Author: Joerg Roedel + +use crate::sizes::PAGE_SIZE; +use core::ops::{Add, BitAnd, Not, Sub}; + +use verus_stub::*; + +#[cfg(verus_only)] +#[path = "specs/align.rs"] +mod align_spec_defs; +#[cfg(verus_only)] +pub use align_spec_defs::*; +#[cfg(verus_only)] +verus! { + broadcast use align_spec_defs::group_align_proofs; +} + +#[verus_spec(ret => + requires + align_up_requires((addr, align)), + ensures + align_up_ens((addr, align), ret), +)] +pub fn align_up(addr: T, align: T) -> T +where + T: Add + Sub + BitAnd + Not + From + Copy, +{ + let mask: T = align - T::from(1u8); + (addr + mask) & !mask +} + +#[verus_spec(ret => + requires + align_down_requires((addr, align)), + ensures + align_down_ens((addr, align), ret), +)] +pub fn align_down(addr: T, align: T) -> T +where + T: Sub + Not + BitAnd + From + Copy, +{ + addr & !(align - T::from(1u8)) +} + +#[verus_spec(ret => + requires + is_aligned_requires((addr, align)), + ensures + is_aligned_ens((addr, align), ret) +)] +pub fn is_aligned(addr: T, align: T) -> bool +where + T: Sub + BitAnd + PartialEq + From, +{ + (addr & (align - T::from(1u8))) == T::from(0u8) +} + +pub fn page_align_up(x: usize) -> usize { + align_up(x, PAGE_SIZE) +} + +pub fn round_to_pages(x: usize) -> usize { + page_align_up(x) / PAGE_SIZE +} + +pub fn page_offset(x: usize) -> usize { + x & (PAGE_SIZE - 1) +} + +pub fn overlap(x1: T, x2: T, y1: T, y2: T) -> bool +where + T: PartialOrd, +{ + x1 <= y2 && y1 <= x2 +} + +#[cfg(test)] +mod tests { + use super::*; + + #[test] + fn test_mem_utils() { + // Align up + assert_eq!(align_up(7, 4), 8); + assert_eq!(align_up(15, 8), 16); + assert_eq!(align_up(10, 2), 10); + // Align down + assert_eq!(align_down(7, 4), 4); + assert_eq!(align_down(15, 8), 8); + assert_eq!(align_down(10, 2), 10); + // Page align up + assert_eq!(page_align_up(4096), 4096); + assert_eq!(page_align_up(4097), 8192); + assert_eq!(page_align_up(0), 0); + // Page offset + assert_eq!(page_offset(4096), 0); + assert_eq!(page_offset(4097), 1); + assert_eq!(page_offset(0), 0); + // Overlaps + assert!(overlap(1, 5, 3, 6)); + assert!(overlap(0, 10, 5, 15)); + assert!(!overlap(1, 5, 6, 8)); + } +} From 0645ad53cdc132185f5b05ad5ae044ff36cdd1d5 Mon Sep 17 00:00:00 2001 From: Ziqiao Zhou Date: Tue, 26 May 2026 17:56:04 +0000 Subject: [PATCH 2/2] paging/lib.rs: change MIT to MIT OR Apache-2.0 Match the license with other files. Signed-off-by: Ziqiao Zhou --- paging/src/lib.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/paging/src/lib.rs b/paging/src/lib.rs index afff84e34e..0943ebd251 100644 --- a/paging/src/lib.rs +++ b/paging/src/lib.rs @@ -1,4 +1,4 @@ -// SPDX-License-Identifier: MIT +// SPDX-License-Identifier: MIT OR Apache-2.0 //! This crate provides page table–related functions and data structures.