paging: move address, sizes, and utility types to paging crate

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"

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

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

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<PageSize> 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;

kernel/src/utils/util.rs

@@ -5,72 +5,9 @@
 // Author: Joerg Roedel <jroedel@suse.de>
 
 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<T>(addr: T, align: T) -> T
-where
-    T: Add<Output = T> + Sub<Output = T> + BitAnd<Output = T> + Not<Output = T> + From<u8> + 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<T>(addr: T, align: T) -> T
-where
-    T: Sub<Output = T> + Not<Output = T> + BitAnd<Output = T> + From<u8> + 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<T>(addr: T, align: T) -> bool
-where
-    T: Sub<Output = T> + BitAnd<Output = T> + PartialEq + From<u8>,
-{
-    (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<T>(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];

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

kernel/src/address.rs → paging/src/address.rs

@@ -4,9 +4,8 @@
 //
 // Author: Carlos López <carlos.lopez@suse.com>
 
-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),
-        }
-    }
-}

paging/src/lib.rs

@@ -0,0 +1,9 @@
+// SPDX-License-Identifier: MIT OR Apache-2.0
+
+//! This crate provides page table–related functions and data structures.
+
+#![no_std]
+
+pub mod address;
+pub mod sizes;
+pub mod util;

kernel/src/utils/util.proof.verus.rs → paging/src/proofs/align.rs

@@ -4,7 +4,10 @@
 //
 // Author: Ziqiao Zhou <ziqiaozhou@microsoft.com>
 //
-// 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<T: IntegerAligned>(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,

kernel/src/types.verus.rs → paging/src/proofs/sizes.rs

@@ -3,6 +3,9 @@
 // Copyright (c) Microsoft Corporation
 //
 // Author: Ziqiao Zhou <ziqiaozhou@microsoft.com>
+use super::PAGE_SIZE;
+use verus_stub::*;
+
 verus! {
 
 pub broadcast group group_types_proof {

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 <jroedel@suse.de>
+
+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<PageSize> for usize {
+    fn from(psize: PageSize) -> Self {
+        match psize {
+            PageSize::Regular => PAGE_SIZE,
+            PageSize::Huge => PAGE_SIZE_2M,
+        }
+    }
+}