From d24ab2d483ee5e4a11e169ea39c0aaec1e23fd0f Mon Sep 17 00:00:00 2001 From: Marsman1996 Date: Wed, 12 Aug 2026 20:13:26 +0800 Subject: [PATCH 01/22] prove: arch::pci (x86) --- ostd/src/arch/x86/device/io_port.rs | 34 ++++++++++++++ ostd/src/arch/x86/device/mod.rs | 4 +- ostd/src/arch/x86/mod.rs | 12 ++--- ostd/src/arch/x86/pci.rs | 36 +++++++++++++++ ostd/src/bus/mod.rs | 4 +- ostd/src/bus/pci/device_info.rs | 7 ++- ostd/src/bus/pci/mod.rs | 9 ++-- ostd/src/io/io_mem/allocator.rs | 20 ++++++-- ostd/src/io/io_mem/mod.rs | 71 +++++++++++++++++++++++++---- ostd/src/io/io_port/mod.rs | 34 +++++++++++--- ostd/src/io/mod.rs | 3 +- ostd/src/lib.rs | 16 +++---- ostd/src/prelude.rs | 4 +- 13 files changed, 211 insertions(+), 43 deletions(-) diff --git a/ostd/src/arch/x86/device/io_port.rs b/ostd/src/arch/x86/device/io_port.rs index 74f7bbadf..c86716257 100644 --- a/ostd/src/arch/x86/device/io_port.rs +++ b/ostd/src/arch/x86/device/io_port.rs @@ -7,3 +7,37 @@ pub use x86_64::{ }, structures::port::{PortRead, PortWrite}, }; + +use vstd::prelude::*; + +verus! { + +/// Opaque specification boundary for the third-party read/write access marker. +#[verifier::external_type_specification] +#[verifier::external_body] +pub struct ExReadWriteAccess(ReadWriteAccess); + +/// Opaque specification boundary for the third-party write-only access marker. +#[verifier::external_type_specification] +#[verifier::external_body] +pub struct ExWriteOnlyAccess(WriteOnlyAccess); + +/// Trusted specification boundary for values that can be read from an x86 I/O port. +#[verifier::external_trait_specification] +pub trait ExPortRead { + type ExternalTraitSpecificationFor: PortRead; + + /// A port read can produce any value supplied by the device. + unsafe fn read_from_port(port: u16) -> Self where Self: Sized; +} + +/// Trusted specification boundary for values that can be written to an x86 I/O port. +#[verifier::external_trait_specification] +pub trait ExPortWrite { + type ExternalTraitSpecificationFor: PortWrite; + + /// A port write has no modeled logical effect on kernel memory. + unsafe fn write_to_port(port: u16, value: Self) where Self: Sized; +} + +} // verus! diff --git a/ostd/src/arch/x86/device/mod.rs b/ostd/src/arch/x86/device/mod.rs index 5d3b7fe3c..5e260d494 100644 --- a/ostd/src/arch/x86/device/mod.rs +++ b/ostd/src/arch/x86/device/mod.rs @@ -1,6 +1,6 @@ // SPDX-License-Identifier: MPL-2.0 //! Device-related APIs. //! This module mainly contains the APIs that should exposed to the device driver like PCI, RTC -pub mod cmos; +/*pub mod cmos;*/ pub mod io_port; -pub mod serial; +/*pub mod serial;*/ diff --git a/ostd/src/arch/x86/mod.rs b/ostd/src/arch/x86/mod.rs index df7a81de1..ec85da40d 100644 --- a/ostd/src/arch/x86/mod.rs +++ b/ostd/src/arch/x86/mod.rs @@ -1,16 +1,17 @@ // SPDX-License-Identifier: MPL-2.0 //! Platform-specific code for the x86 platform. /*pub mod boot; -pub(crate) mod cpu; +pub(crate) mod cpu;*/ pub mod device; -pub(crate) mod ex_table; + +/*pub(crate) mod ex_table; pub(crate) mod io; pub(crate) mod iommu;*/ pub(crate) mod irq; /* pub(crate) mod kernel; */ pub(crate) mod mm; -/*pub(crate) mod pci; -pub mod qemu; +pub(crate) mod pci; +/*pub mod qemu; pub(crate) mod serial; pub(crate) mod task; */ pub mod timer; @@ -212,7 +213,7 @@ pub(crate) fn enable_cpu_features() { *efer |= EferFlags::NO_EXECUTE_ENABLE; }); } -} +}*/ /// Inserts a TDX-specific code block. /// @@ -251,4 +252,3 @@ macro_rules! if_tdx_enabled { } pub use if_tdx_enabled; -*/ diff --git a/ostd/src/arch/x86/pci.rs b/ostd/src/arch/x86/pci.rs index e212be1f7..33832d995 100644 --- a/ostd/src/arch/x86/pci.rs +++ b/ostd/src/arch/x86/pci.rs @@ -1,30 +1,58 @@ // SPDX-License-Identifier: MPL-2.0 //! PCI bus access +use vstd::prelude::*; + use super::device::io_port::{ReadWriteAccess, WriteOnlyAccess}; use crate::{bus::pci::PciDeviceLocation, io::IoPort, prelude::*}; +verus! { + +/// x86 is little-endian, so converting a native-endian `u32` to little endian is the identity. +pub assume_specification[ u32::to_le ](value: u32) -> (result: u32) + ensures + result == value, +; + +} // verus! +#[verus_verify] static PCI_ADDRESS_PORT: IoPort = unsafe { IoPort::new(0x0CF8) }; +#[verus_verify] static PCI_DATA_PORT: IoPort = unsafe { IoPort::new(0x0CFC) }; +#[verus_verify] const BIT32_ALIGN_MASK: u32 = 0xFFFC; +#[verus_verify] +#[verus_spec(result => ensures result is Ok)] pub(crate) fn write32(location: &PciDeviceLocation, offset: u32, value: u32) -> Result<()> { PCI_ADDRESS_PORT.write(encode_as_port(location) | (offset & BIT32_ALIGN_MASK)); PCI_DATA_PORT.write(value.to_le()); Ok(()) } +#[verus_verify] +#[verus_spec(result => ensures result is Ok)] pub(crate) fn read32(location: &PciDeviceLocation, offset: u32) -> Result { PCI_ADDRESS_PORT.write(encode_as_port(location) | (offset & BIT32_ALIGN_MASK)); Ok(PCI_DATA_PORT.read().to_le()) } +#[verus_verify] +#[verus_spec(returns true)] pub(crate) fn has_pci_bus() -> bool { true } +#[verus_verify] pub(crate) const MSIX_DEFAULT_MSG_ADDR: u32 = 0xFEE0_0000; +#[verus_verify] +#[verus_spec(address => + ensures + address == MSIX_DEFAULT_MSG_ADDR | 0b1_1000 + | ((remapping_index & 0x7FFF) << 5) + | ((remapping_index & 0x8000) >> 13), +)] pub(crate) fn construct_remappable_msix_address(remapping_index: u32) -> u32 { // Use remappable format. The bits[4:3] should be always set to 1 according to the manual. let mut address = MSIX_DEFAULT_MSG_ADDR | 0b1_1000; @@ -37,6 +65,14 @@ pub(crate) fn construct_remappable_msix_address(remapping_index: u32) -> u32 { } /// Encodes the bus, device, and function into a port address for use with the PCI I/O port. +#[verus_verify] +#[verus_spec(port => + ensures + port == (1u32 << 31) + | ((location.bus as u32) << 16) + | (((location.device as u32) & 0b11111) << 11) + | (((location.function as u32) & 0b111) << 8), +)] fn encode_as_port(location: &PciDeviceLocation) -> u32 { // 1 << 31: Configuration enable (1 << 31) diff --git a/ostd/src/bus/mod.rs b/ostd/src/bus/mod.rs index 7b81924ce..b8898deb6 100644 --- a/ostd/src/bus/mod.rs +++ b/ostd/src/bus/mod.rs @@ -11,7 +11,7 @@ pub enum BusProbeError { ConfigurationSpaceError, } -/// Initializes the bus +/*/// Initializes the bus pub(crate) fn init() { pci::init(); -} +}*/ diff --git a/ostd/src/bus/pci/device_info.rs b/ostd/src/bus/pci/device_info.rs index 3d415c987..3bcc6c1a0 100644 --- a/ostd/src/bus/pci/device_info.rs +++ b/ostd/src/bus/pci/device_info.rs @@ -1,9 +1,12 @@ // SPDX-License-Identifier: MPL-2.0 //! PCI device Information +use vstd::prelude::*; + use core::iter; -use super::cfg_space::PciDeviceCommonCfgOffset; +/*use super::cfg_space::PciDeviceCommonCfgOffset;*/ +/* /// PCI device ID #[derive(Debug, Copy, Clone, PartialEq, Eq)] pub struct PciDeviceId { @@ -48,8 +51,10 @@ impl PciDeviceId { } } } +*/ /// PCI device Location +#[verus_verify] #[derive(Debug, Copy, Clone, PartialEq, Eq, PartialOrd, Ord)] pub struct PciDeviceLocation { /// Bus number diff --git a/ostd/src/bus/pci/mod.rs b/ostd/src/bus/pci/mod.rs index 0de48b517..261ab6202 100644 --- a/ostd/src/bus/pci/mod.rs +++ b/ostd/src/bus/pci/mod.rs @@ -48,14 +48,15 @@ //! PCI_BUS.lock().register_driver(driver_a); //! } //! ``` -pub mod bus; +/*pub mod bus; pub mod capability; pub mod cfg_space; -pub mod common_device; +pub mod common_device;*/ mod device_info; -pub use device_info::{PciDeviceId, PciDeviceLocation}; +pub use device_info::{/* PciDeviceId, */ PciDeviceLocation}; +/* use self::{bus::PciBus, common_device::PciCommonDevice}; use crate::{arch::pci::has_pci_bus, sync::Mutex}; @@ -74,4 +75,4 @@ pub(crate) fn init() { }; lock.register_common_device(device); } -} +}*/ diff --git a/ostd/src/io/io_mem/allocator.rs b/ostd/src/io/io_mem/allocator.rs index 0cd42a4e9..0e2ca94b1 100644 --- a/ostd/src/io/io_mem/allocator.rs +++ b/ostd/src/io/io_mem/allocator.rs @@ -1,5 +1,7 @@ // SPDX-License-Identifier: MPL-2.0 //! I/O Memory allocator. +use vstd::prelude::*; + use alloc::vec::Vec; use core::ops::Range; @@ -13,6 +15,7 @@ use crate::{ }; /// I/O memory allocator that allocates memory I/O access to device drivers. +#[verus_verify] pub struct IoMemAllocator { allocators: Vec, } @@ -29,7 +32,8 @@ impl IoMemAllocator { debug!("Acquiring MMIO range:{:x?}..{:x?}", range.start, range.end); // SAFETY: The created `IoMem` is guaranteed not to access physical memory or system device I/O. - unsafe { Some(IoMem::new(range, PageFlags::RW, CachePolicy::Uncacheable)) } + // Original Rust used the upstream bitflags-style associated constant `PageFlags::RW`. + unsafe { Some(IoMem::new(range, PageFlags::RW(), CachePolicy::Uncacheable)) } } /// Recycles an MMIO range. @@ -51,6 +55,7 @@ impl IoMemAllocator { /// # Safety /// /// User must ensure the range doesn't belong to physical memory or system device I/O. + #[verus_verify] unsafe fn new(allocators: Vec) -> Self { Self { allocators } } @@ -60,6 +65,7 @@ impl IoMemAllocator { /// /// The builder must contains the memory I/O regions that don't belong to the physical memory. Also, OSTD /// must exclude the memory I/O regions of the system device before building the `IoMemAllocator`. +#[verus_verify] pub(crate) struct IoMemAllocatorBuilder { allocators: Vec, } @@ -70,11 +76,12 @@ impl IoMemAllocatorBuilder { /// # Safety /// /// User must ensure the range doesn't belong to physical memory. + #[verus_verify] pub(crate) unsafe fn new(ranges: Vec>) -> Self { - info!( + /* info!( "Creating new I/O memory allocator builder, ranges: {:#x?}", ranges - ); + ); */ let mut allocators = Vec::with_capacity(ranges.len()); for range in ranges { allocators.push(RangeAllocator::new(range)); @@ -116,17 +123,24 @@ pub(crate) unsafe fn init(io_mem_builder: IoMemAllocatorBuilder) { IO_MEM_ALLOCATOR.call_once(|| unsafe { IoMemAllocator::new(io_mem_builder.allocators) }); } +#[verus_verify] fn find_allocator<'a>( allocators: &'a [RangeAllocator], range: &Range, ) -> Option<&'a RangeAllocator> { for allocator in allocators.iter() { let allocator_range = allocator.fullrange(); + // Verus does not yet support `continue` in `for` loops. Original Rust: + /* if allocator_range.start >= range.end || allocator_range.end <= range.start { continue; } return Some(allocator); + */ + if allocator_range.start < range.end && allocator_range.end > range.start { + return Some(allocator); + } } None } diff --git a/ostd/src/io/io_mem/mod.rs b/ostd/src/io/io_mem/mod.rs index 3afa2d077..3ad8b3087 100644 --- a/ostd/src/io/io_mem/mod.rs +++ b/ostd/src/io/io_mem/mod.rs @@ -1,5 +1,9 @@ // SPDX-License-Identifier: MPL-2.0 //! I/O memory and its allocator that allocates memory I/O (MMIO) to device drivers. +use crate::specs::arch::PAGE_SIZE; +use crate::specs::{mm::virt_mem::VirtPtr, task::AnyAtomicGuard}; +use vstd::prelude::*; + mod allocator; use core::ops::{Deref, Range}; @@ -11,8 +15,8 @@ pub(super) use self::allocator::init; use crate::{ Error, mm::{ - FallibleVmRead, FallibleVmWrite, HasPaddr, Infallible, PAGE_SIZE, Paddr, PodOnce, VmIo, - VmIoOnce, VmReader, VmWriter, + FallibleVmRead, FallibleVmWrite, HasPaddr, Infallible, /*PAGE_SIZE,*/ Paddr, PodOnce, + VmIo, VmIoOnce, VmReader, VmWriter, kspace::kvirt_area::KVirtArea, page_prop::{CachePolicy, PageFlags, PageProperty, PrivilegedPageFlags}, }, @@ -21,6 +25,7 @@ use crate::{ /// I/O memory. #[derive(Debug, Clone)] +#[verus_verify] pub struct IoMem { kvirt_area: Arc, // The actually used range for MMIO is `kvirt_area.start + offset..kvirt_area.start + offset + limit` @@ -29,7 +34,29 @@ pub struct IoMem { pa: Paddr, } +verus! { + +impl IoMem { + /// Logical physical-address projection used by verified callers. + pub closed spec fn paddr_spec(&self) -> Paddr { + self.pa + } + + /// Logical byte length used by verified callers. + pub closed spec fn length_spec(&self) -> usize { + self.limit + } + + /// Logical offset into the page-aligned mapping. + pub closed spec fn offset_spec(&self) -> usize { + self.offset + } +} + +} // verus! +#[verus_verify] impl HasPaddr for IoMem { + #[verus_spec(result => ensures result == self.paddr_spec())] fn paddr(&self) -> Paddr { self.pa } @@ -46,11 +73,15 @@ impl IoMem { } /// Returns the physical address of the I/O memory. + #[verus_verify] + #[verus_spec(result => ensures result == self.paddr_spec())] pub fn paddr(&self) -> Paddr { self.pa } /// Returns the length of the I/O memory region. + #[verus_verify] + #[verus_spec(result => ensures result == self.length_spec())] pub fn length(&self) -> usize { self.limit } @@ -60,15 +91,31 @@ impl IoMem { /// # Panics /// /// This method will panic if the range is empty or out of bounds. + #[verus_verify] + #[verus_spec(result => + requires + range.start < range.end, + range.end <= self.length_spec(), + self.offset_spec() + range.start <= usize::MAX, + self.paddr_spec() + range.start <= usize::MAX, + ensures + result.offset_spec() == self.offset_spec() + range.start, + result.length_spec() == range.end - range.start, + result.paddr_spec() == self.paddr_spec() + range.start, + )] pub fn slice(&self, range: Range) -> Self { // This ensures `range.start < range.end` and `range.end <= limit`. + /* assert!(!range.is_empty() && range.end <= self.limit); + */ + vstd_extra::assert!(range.start < range.end && range.end <= self.limit); // We've checked the range is in bounds, so we can construct the new `IoMem` safely. Self { kvirt_area: self.kvirt_area.clone(), offset: self.offset + range.start, - limit: range.len(), + /* limit: range.len(), */ + limit: range.end - range.start, pa: self.pa + range.start, } } @@ -123,7 +170,11 @@ impl IoMem { // SAFETY: The caller of `IoMem::new()` ensures that the given // physical address range is I/O memory, so it is safe to map. - let kva = unsafe { KVirtArea::map_untracked_frames(area_size, 0, frames_range, prop) }; + // Original Rust: + // let kva = unsafe { KVirtArea::map_untracked_frames(area_size, 0, frames_range, prop) }; + let kva = unsafe { + KVirtArea::map_untracked_frames::(area_size, 0, frames_range, prop) + }; Self { kvirt_area: Arc::new(kva), @@ -146,8 +197,10 @@ impl IoMem { // SAFETY: The constructor of the `IoMem` structure has already ensured the // safety of reading from the mapped physical address, and the mapping is valid. unsafe { + // `from_kernel_space` in ostd/src/mm/io.rs is changed + // (self.kvirt_area.deref().start() + self.offset) as *mut u8 VmReader::from_kernel_space( - (self.kvirt_area.deref().start() + self.offset) as *mut u8, + VirtPtr::from_vaddr(self.kvirt_area.deref().start() + self.offset, self.limit), self.limit, ) } @@ -157,15 +210,17 @@ impl IoMem { // SAFETY: The constructor of the `IoMem` structure has already ensured the // safety of writing to the mapped physical address, and the mapping is valid. unsafe { + // Original Rust passed the raw pointer + // `(self.kvirt_area.deref().start() + self.offset) as *mut u8`. VmWriter::from_kernel_space( - (self.kvirt_area.deref().start() + self.offset) as *mut u8, + VirtPtr::from_vaddr(self.kvirt_area.deref().start() + self.offset, self.limit), self.limit, ) } } } -impl VmIo for IoMem { +/*impl VmIo for IoMem { fn read(&self, offset: usize, writer: &mut VmWriter) -> Result<()> { let offset = offset + self.offset; if self @@ -213,7 +268,7 @@ impl VmIoOnce for IoMem { fn write_once(&self, offset: usize, new_val: &T) -> Result<()> { self.writer().skip(offset).write_once(new_val) } -} +}*/ impl Drop for IoMem { fn drop(&mut self) { diff --git a/ostd/src/io/io_port/mod.rs b/ostd/src/io/io_port/mod.rs index 731ed3571..c6ea35bd2 100644 --- a/ostd/src/io/io_port/mod.rs +++ b/ostd/src/io/io_port/mod.rs @@ -1,11 +1,13 @@ // SPDX-License-Identifier: MPL-2.0 //! I/O port and its allocator that allocates port I/O (PIO) to device drivers. +use vstd::prelude::*; + use crate::arch::device::io_port::{IoPortReadAccess, IoPortWriteAccess, PortRead, PortWrite}; -mod allocator; +/*mod allocator;*/ use core::{marker::PhantomData, mem::size_of}; -pub(super) use self::allocator::init; +/*pub(super) use self::allocator::init;*/ use crate::{Error, prelude::*}; /// An I/O port, representing a specific address in the I/O address of x86. @@ -20,23 +22,37 @@ use crate::{Error, prelude::*}; /// } /// ``` /// +#[verus_verify] pub struct IoPort { port: u16, value_marker: PhantomData, access_marker: PhantomData, } +verus! { + +impl View for IoPort { + type V = u16; + + closed spec fn view(&self) -> u16 { + self.port + } +} + +} // verus! +#[verus_verify] impl IoPort { /// Acquires an `IoPort` instance for the given range. - pub fn acquire(port: u16) -> Result> { + /*pub fn acquire(port: u16) -> Result> { allocator::IO_PORT_ALLOCATOR .get() .unwrap() .acquire(port) .ok_or(Error::AccessDenied) - } + }*/ /// Returns the port number. + #[verus_spec(returns self@)] pub const fn port(&self) -> u16 { self.port } @@ -52,6 +68,7 @@ impl IoPort { /// /// This function is marked unsafe as creating an I/O port is considered /// a privileged operation. + #[verus_spec(ret => ensures ret@ == port)] pub const unsafe fn new(port: u16) -> Self { Self { port, @@ -61,6 +78,8 @@ impl IoPort { } } +#[verus_verify] +#[verifier::allow(undeclared_external_trait)] impl IoPort { /// Reads from the I/O port #[inline] @@ -69,6 +88,8 @@ impl IoPort { } } +#[verus_verify] +#[verifier::allow(undeclared_external_trait)] impl IoPort { /// Writes to the I/O port #[inline] @@ -77,7 +98,7 @@ impl IoPort { } } -impl Drop for IoPort { +/*impl Drop for IoPort { fn drop(&mut self) { // SAFETY: The caller have ownership of the PIO region. unsafe { @@ -87,7 +108,7 @@ impl Drop for IoPort { .recycle(self.port..(self.port + size_of::() as u16)); } } -} +}*/ /// Reserves an I/O port range which may refer to the port I/O range used by the /// system device driver. @@ -162,6 +183,7 @@ pub(crate) use sensitive_io_port; #[doc(hidden)] #[derive(Debug, Clone, Copy)] #[repr(C)] +#[verus_verify] pub(crate) struct RawIoPortRange { pub(crate) begin: u16, pub(crate) end: u16, diff --git a/ostd/src/io/mod.rs b/ostd/src/io/mod.rs index a87940453..4de2932ff 100644 --- a/ostd/src/io/mod.rs +++ b/ostd/src/io/mod.rs @@ -20,6 +20,7 @@ cfg_if!( } ); +/* /// Initializes the static allocator based on builder. /// /// # Safety @@ -43,4 +44,4 @@ pub(crate) unsafe fn init(io_mem_builder: IoMemAllocatorBuilder) { unsafe { self::io_port::init() }; -} +}*/ diff --git a/ostd/src/lib.rs b/ostd/src/lib.rs index 8a90a3876..a4970bd77 100644 --- a/ostd/src/lib.rs +++ b/ostd/src/lib.rs @@ -38,16 +38,16 @@ pub mod arch; //#[path = "arch/riscv/mod.rs"] //pub mod arch; pub mod boot; -/*pub mod bus; -pub mod console; +pub mod bus; +/*pub mod console; pub mod cpu;*/ pub mod error; -/*pub mod io; -pub mod logger;*/ +pub mod io; +/*pub mod logger;*/ pub mod mm; -/*pub mod panic; +/*pub mod panic;*/ pub mod prelude; -pub mod smp;*/ +/*pub mod smp;*/ pub mod sync; pub mod task; pub mod timer; @@ -64,9 +64,9 @@ pub use ostd_macros::{ panic_handler, };*/ pub use ostd_pod::Pod; -/* -pub use self::{error::Error, prelude::Result}; +pub use self::{error::Error, prelude::Result}; +/* /// Initializes OSTD. /// /// This function represents the first phase booting up the system. It makes diff --git a/ostd/src/prelude.rs b/ostd/src/prelude.rs index f9ab829ef..bb1eeaf17 100644 --- a/ostd/src/prelude.rs +++ b/ostd/src/prelude.rs @@ -6,7 +6,7 @@ pub type Result = core::result::Result; pub(crate) use alloc::{boxed::Box, sync::Arc, vec::Vec}; - +/* #[cfg(ktest)] pub use ostd_macros::ktest; @@ -14,4 +14,4 @@ pub use crate::{ early_print as print, early_println as println, mm::{Paddr, UntypedMem, Vaddr}, panic::abort, -}; +}; */ From fffd33501958603bf78dbd932fd52413e7e789fb Mon Sep 17 00:00:00 2001 From: Marsman1996 Date: Thu, 13 Aug 2026 12:47:30 +0800 Subject: [PATCH 02/22] prove: io --- Cargo.lock | 8 ++ ostd/Cargo.toml | 2 +- ostd/libs/id-alloc/src/lib.rs | 1 - ostd/src/arch/x86/io.rs | 7 +- ostd/src/arch/x86/mod.rs | 4 +- ostd/src/io/io_mem/allocator.rs | 58 +++++++++---- ostd/src/io/io_mem/mod.rs | 142 +++++++++++++++++++++++++------ ostd/src/io/io_port/allocator.rs | 89 ++++++++++++++++++- ostd/src/io/io_port/mod.rs | 45 +++++++--- ostd/src/io/mod.rs | 6 +- 10 files changed, 297 insertions(+), 65 deletions(-) diff --git a/Cargo.lock b/Cargo.lock index 92c2f90e6..fe004aa9a 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -190,6 +190,13 @@ dependencies = [ "lazy_static", ] +[[package]] +name = "id-alloc" +version = "0.1.0" +dependencies = [ + "bitvec", +] + [[package]] name = "ident_case" version = "1.0.1" @@ -310,6 +317,7 @@ dependencies = [ "fdt", "gimli 0.28.1", "iced-x86", + "id-alloc", "inherit-methods-macro", "log", "loongArch64", diff --git a/ostd/Cargo.toml b/ostd/Cargo.toml index f1344922b..830b3a55d 100644 --- a/ostd/Cargo.toml +++ b/ostd/Cargo.toml @@ -25,7 +25,7 @@ buddy_system_allocator = { version = "0.10", default-features = false, features bitflags_upstream = { package = "bitflags", version = "1.3" } cfg-if = "1.0" gimli = { version = "0.28", default-features = false, features = ["read-core"] } -#id-alloc = { path = "libs/id-alloc", version = "0.1.0" } +id-alloc = { path = "libs/id-alloc", version = "0.1.0" } inherit-methods-macro = { git = "https://github.com/asterinas/inherit-methods-macro", rev = "98f7e3e", version = "0.1.0" } #int-to-c-enum = { path = "../kernel/libs/int-to-c-enum", version = "0.1.0" } # intrusive-collections = { version = "0.9.6", features = ["nightly"] } diff --git a/ostd/libs/id-alloc/src/lib.rs b/ostd/libs/id-alloc/src/lib.rs index 85fe26b25..4721d94e5 100644 --- a/ostd/libs/id-alloc/src/lib.rs +++ b/ostd/libs/id-alloc/src/lib.rs @@ -1,5 +1,4 @@ // SPDX-License-Identifier: MPL-2.0 - #![cfg_attr(not(test), no_std)] #![deny(unsafe_code)] diff --git a/ostd/src/arch/x86/io.rs b/ostd/src/arch/x86/io.rs index b78d04f26..35913c17f 100644 --- a/ostd/src/arch/x86/io.rs +++ b/ostd/src/arch/x86/io.rs @@ -1,5 +1,7 @@ // SPDX-License-Identifier: MPL-2.0 -use alloc::vec::Vec; +use vstd::prelude::*; + +/*use alloc::vec::Vec; use align_ext::AlignExt; @@ -55,6 +57,7 @@ pub(super) fn construct_io_mem_allocator_builder() -> IoMemAllocatorBuilder { // SAFETY: The range is guaranteed not to access physical memory. unsafe { IoMemAllocatorBuilder::new(ranges) } } - +*/ /// Port I/O definition reference: . +#[verus_verify] pub const MAX_IO_PORT: u16 = u16::MAX; diff --git a/ostd/src/arch/x86/mod.rs b/ostd/src/arch/x86/mod.rs index ec85da40d..302df01ae 100644 --- a/ostd/src/arch/x86/mod.rs +++ b/ostd/src/arch/x86/mod.rs @@ -4,9 +4,9 @@ pub(crate) mod cpu;*/ pub mod device; -/*pub(crate) mod ex_table; +/*pub(crate) mod ex_table;*/ pub(crate) mod io; -pub(crate) mod iommu;*/ +/*pub(crate) mod iommu;*/ pub(crate) mod irq; /* pub(crate) mod kernel; */ pub(crate) mod mm; diff --git a/ostd/src/io/io_mem/allocator.rs b/ostd/src/io/io_mem/allocator.rs index 0e2ca94b1..cfa98c8aa 100644 --- a/ostd/src/io/io_mem/allocator.rs +++ b/ostd/src/io/io_mem/allocator.rs @@ -1,12 +1,14 @@ // SPDX-License-Identifier: MPL-2.0 //! I/O Memory allocator. +use crate::specs::arch::PAGE_SIZE; +use crate::sync::{OnceImpl, TrivialPred}; use vstd::prelude::*; use alloc::vec::Vec; use core::ops::Range; use log::{debug, info}; -use spin::Once; +/*use spin::Once;*/ use crate::{ io::io_mem::IoMem, @@ -20,16 +22,27 @@ pub struct IoMemAllocator { allocators: Vec, } +#[verus_verify] impl IoMemAllocator { /// Acquires the I/O memory access for `range`. /// /// If the range is not available, then the return value will be `None`. + #[verus_spec(result => + requires + vstd::arithmetic::power2::is_pow2(PAGE_SIZE as int), + range.start < range.end, + range.end <= usize::MAX - (PAGE_SIZE - 1), + ensures + result is Some ==> result->Some_0.paddr_spec() == range.start, + result is Some ==> result->Some_0.length_spec() + == vstd_extra::external::range::range_usize_len_spec(&range), + )] pub fn acquire(&self, range: Range) -> Option { find_allocator(&self.allocators, &range)? .alloc_specific(&range) .ok()?; - debug!("Acquiring MMIO range:{:x?}..{:x?}", range.start, range.end); + /* debug!("Acquiring MMIO range:{:x?}..{:x?}", range.start, range.end); */ // SAFETY: The created `IoMem` is guaranteed not to access physical memory or system device I/O. // Original Rust used the upstream bitflags-style associated constant `PageFlags::RW`. @@ -42,10 +55,11 @@ impl IoMemAllocator { /// /// The caller must have ownership of the MMIO region through the `IoMemAllocator::get` interface. #[expect(dead_code)] + #[verifier::external_body] pub(in crate::io) unsafe fn recycle(&self, range: Range) { let allocator = find_allocator(&self.allocators, &range).unwrap(); - debug!("Recycling MMIO range:{:x}..{:x}", range.start, range.end); + /* debug!("Recycling MMIO range:{:x}..{:x}", range.start, range.end); */ allocator.free(range); } @@ -70,6 +84,7 @@ pub(crate) struct IoMemAllocatorBuilder { allocators: Vec, } +#[verus_verify] impl IoMemAllocatorBuilder { /// Initializes memory I/O region for devices. /// @@ -92,35 +107,42 @@ impl IoMemAllocatorBuilder { /// Removes access to a specific memory I/O range. /// /// All drivers in OSTD must use this method to prevent peripheral drivers from accessing illegal memory I/O range. + #[verus_spec( + requires + range.start < range.end, + vstd_extra::panic::may_panic(), + )] pub(crate) fn remove(&self, range: Range) { - let Some(allocator) = find_allocator(&self.allocators, &range) else { - panic!( - "Allocator for the system device's MMIO was not found. Range: {:x?}", - range - ); - }; - - if let Err(err) = allocator.alloc_specific(&range) { - panic!( - "An error occurred while trying to remove access to the system device's MMIO. Range: {:x?}. Error: {:?}", - range, err - ); - } + // Formatting machinery used by the original panic is not modeled by Verus. + // Original Rust used two formatted `panic!` branches here. + let allocator = find_allocator(&self.allocators, &range); + vstd_extra::assert!(allocator.is_some()); + let result = allocator.unwrap().alloc_specific(&range); + vstd_extra::assert!(result.is_ok()); } } /// The I/O Memory allocator of the system. -pub static IO_MEM_ALLOCATOR: Once = Once::new(); +verus! { +pub exec static IO_MEM_ALLOCATOR: OnceImpl + ensures + IO_MEM_ALLOCATOR.wf(), +{ + OnceImpl::new(Ghost(TrivialPred)) +} + +} // verus! /// Initializes the static `IO_MEM_ALLOCATOR` based on builder. /// /// # Safety /// /// User must ensure all the memory I/O regions that belong to the system device have been removed by calling the /// `remove` function. +#[verus_verify] pub(crate) unsafe fn init(io_mem_builder: IoMemAllocatorBuilder) { // SAFETY: The safety is upheld by the caller. - IO_MEM_ALLOCATOR.call_once(|| unsafe { IoMemAllocator::new(io_mem_builder.allocators) }); + IO_MEM_ALLOCATOR.init(unsafe { IoMemAllocator::new(io_mem_builder.allocators) }); } #[verus_verify] diff --git a/ostd/src/io/io_mem/mod.rs b/ostd/src/io/io_mem/mod.rs index 3ad8b3087..c92c2a947 100644 --- a/ostd/src/io/io_mem/mod.rs +++ b/ostd/src/io/io_mem/mod.rs @@ -1,7 +1,10 @@ // SPDX-License-Identifier: MPL-2.0 //! I/O memory and its allocator that allocates memory I/O (MMIO) to device drivers. use crate::specs::arch::PAGE_SIZE; -use crate::specs::{mm::virt_mem::VirtPtr, task::AnyAtomicGuard}; +use crate::specs::{ + mm::{io::VmIoOwner, virt_mem::VirtPtr}, + task::AnyAtomicGuard, +}; use vstd::prelude::*; mod allocator; @@ -36,6 +39,7 @@ pub struct IoMem { verus! { +#[verus_verify] impl IoMem { /// Logical physical-address projection used by verified callers. pub closed spec fn paddr_spec(&self) -> Paddr { @@ -62,12 +66,23 @@ impl HasPaddr for IoMem { } } +#[verus_verify] impl IoMem { /// Acquires an `IoMem` instance for the given range. + #[verus_spec(result => + requires + vstd::arithmetic::power2::is_pow2(PAGE_SIZE as int), + range.start < range.end, + range.end <= usize::MAX - (PAGE_SIZE - 1), + ensures + result is Ok ==> result->Ok_0.paddr_spec() == range.start, + result is Ok ==> result->Ok_0.length_spec() + == vstd_extra::external::range::range_usize_len_spec(&range), + )] pub fn acquire(range: Range) -> Result { allocator::IO_MEM_ALLOCATOR .get() - .unwrap() + .ok_or(Error::AccessDenied)? .acquire(range) .ok_or(Error::AccessDenied) } @@ -115,7 +130,7 @@ impl IoMem { kvirt_area: self.kvirt_area.clone(), offset: self.offset + range.start, /* limit: range.len(), */ - limit: range.end - range.start, + limit: vstd_extra::external::range::range_usize_len(&range), pa: self.pa + range.start, } } @@ -127,6 +142,17 @@ impl IoMem { /// - The given physical address range must be in the I/O memory region. /// - Reading from or writing to I/O memory regions may have side effects. Those side effects /// must not cause soundness problems (e.g., they must not corrupt the kernel memory). + #[verifier::external_body] + #[verus_spec(result => + requires + vstd::arithmetic::power2::is_pow2(PAGE_SIZE as int), + range.start <= range.end, + range.end <= usize::MAX - (PAGE_SIZE - 1), + ensures + result.paddr_spec() == range.start, + result.length_spec() + == vstd_extra::external::range::range_usize_len_spec(&range), + )] pub(crate) unsafe fn new(range: Range, flags: PageFlags, cache: CachePolicy) -> Self { let first_page_start = range.start.align_down(PAGE_SIZE); let last_page_end = range.end.align_up(PAGE_SIZE); @@ -220,40 +246,83 @@ impl IoMem { } } -/*impl VmIo for IoMem { - fn read(&self, offset: usize, writer: &mut VmWriter) -> Result<()> { +verus! { + +impl VmIo<()> for IoMem { + closed spec fn obeys_vmio_spec() -> bool { + false + } + + closed spec fn obeys_vmio_read_spec() -> bool { + false + } + + closed spec fn obeys_vmio_write_spec() -> bool { + false + } + + open spec fn read_spec( + self, + offset: usize, + old_writer: VmWriter<'_>, + new_writer: VmWriter<'_>, + old_writer_own: VmIoOwner, + new_writer_own: VmIoOwner, + old_owner: (), + new_owner: (), + r: Result<()>, + ) -> bool { + false + } + + open spec fn write_spec( + self, + offset: usize, + old_reader: VmReader<'_>, + new_reader: VmReader<'_>, + old_reader_own: VmIoOwner, + new_reader_own: VmIoOwner, + old_owner: (), + new_owner: (), + r: Result<()>, + ) -> bool { + false + } + + /// Device reads are a trusted hardware boundary; the range checks and cursor updates remain + /// identical to the original implementation. + #[verifier::external_body] + fn read( + &self, + offset: usize, + writer: &mut VmWriter, + Tracked(_writer_own): Tracked<&mut VmIoOwner>, + Tracked(_owner): Tracked<&mut ()>, + ) -> Result<()> { let offset = offset + self.offset; - if self - .limit - .checked_sub(offset) - .is_none_or(|remain| remain < writer.avail()) - { + if self.limit.checked_sub(offset).is_none_or(|remain| remain < writer.avail()) { return Err(Error::InvalidArgs); } - - self.reader() - .skip(offset) - .read_fallible(writer) - .map_err(|(e, _)| e)?; + self.reader().skip(offset).read_fallible(writer).map_err(|(e, _)| e)?; debug_assert!(!writer.has_avail()); Ok(()) } - fn write(&self, offset: usize, reader: &mut VmReader) -> Result<()> { + /// Device writes are a trusted hardware boundary for the same reason as [`Self::read`]. + #[verifier::external_body] + fn write( + &self, + offset: usize, + reader: &mut VmReader, + Tracked(_reader_own): Tracked<&mut VmIoOwner>, + Tracked(_owner): Tracked<&mut ()>, + ) -> Result<()> { let offset = offset + self.offset; - if self - .limit - .checked_sub(offset) - .is_none_or(|remain| remain < reader.remain()) - { + if self.limit.checked_sub(offset).is_none_or(|remain| remain < reader.remain()) { return Err(Error::InvalidArgs); } - - self.writer() - .skip(offset) - .write_fallible(reader) - .map_err(|(e, _)| e)?; + self.writer().skip(offset).write_fallible(reader).map_err(|(e, _)| e)?; debug_assert!(!reader.has_remain()); Ok(()) @@ -261,15 +330,34 @@ impl IoMem { } impl VmIoOnce for IoMem { + closed spec fn obeys_vmio_once_read_requires() -> bool { + false + } + + closed spec fn obeys_vmio_once_write_requires() -> bool { + false + } + + closed spec fn obeys_vmio_once_read_ensures() -> bool { + false + } + + closed spec fn obeys_vmio_once_write_ensures() -> bool { + false + } + + #[verifier::external_body] fn read_once(&self, offset: usize) -> Result { self.reader().skip(offset).read_once() } + #[verifier::external_body] fn write_once(&self, offset: usize, new_val: &T) -> Result<()> { self.writer().skip(offset).write_once(new_val) } -}*/ +} +} // verus! impl Drop for IoMem { fn drop(&mut self) { // TODO: Multiple `IoMem` instances should not overlap, we should refactor the driver code and diff --git a/ostd/src/io/io_port/allocator.rs b/ostd/src/io/io_port/allocator.rs index 0e5b85e9a..f4bff93f6 100644 --- a/ostd/src/io/io_port/allocator.rs +++ b/ostd/src/io/io_port/allocator.rs @@ -1,5 +1,7 @@ // SPDX-License-Identifier: MPL-2.0 //! I/O port allocator. +use vstd::prelude::*; + use core::ops::Range; use id_alloc::IdAlloc; @@ -12,7 +14,64 @@ use crate::{ sync::{LocalIrqDisabled, SpinLock}, }; +verus! { + +/// Verus model for the external bitmap-backed ID allocator. +#[verifier::external_type_specification] +#[verifier::external_body] +pub struct ExIdAlloc(IdAlloc); + +/// Opaque specification for the third-party one-time initialization primitive. +#[verifier::external_type_specification] +#[verifier::external_body] +#[verifier::reject_recursive_types(T)] +#[verifier::reject_recursive_types(R)] +pub struct ExOnce(spin::once::Once); + +/// IDs currently allocated by an external `IdAlloc`. +pub uninterp spec fn id_alloc_view(allocator: &IdAlloc) -> Set; + +/// Capacity configured for an external `IdAlloc`. +pub uninterp spec fn id_alloc_capacity(allocator: &IdAlloc) -> usize; + +pub assume_specification[ IdAlloc::with_capacity ](capacity: usize) -> (allocator: IdAlloc) + ensures + id_alloc_capacity(&allocator) == capacity, + id_alloc_view(&allocator) == Set::::empty(), +; + +pub assume_specification[ IdAlloc::is_allocated ](allocator: &IdAlloc, id: usize) -> (allocated: + bool) + ensures + id < id_alloc_capacity(allocator) ==> allocated == id_alloc_view(allocator).contains(id), +; + +pub assume_specification[ IdAlloc::alloc_specific ](allocator: &mut IdAlloc, id: usize) -> (result: + Option) + ensures + id_alloc_capacity(final(allocator)) == id_alloc_capacity(old(allocator)), + id < id_alloc_capacity(old(allocator)) && id_alloc_view(old(allocator)).contains(id) ==> { + &&& result is None + &&& id_alloc_view(final(allocator)) == id_alloc_view(old(allocator)) + }, + id < id_alloc_capacity(old(allocator)) && !id_alloc_view(old(allocator)).contains(id) ==> { + &&& result == Some(id) + &&& id_alloc_view(final(allocator)) == id_alloc_view(old(allocator)).insert(id) + }, +; + +pub assume_specification[ IdAlloc::free_consecutive ](allocator: &mut IdAlloc, range: Range) + ensures + id_alloc_capacity(final(allocator)) == id_alloc_capacity(old(allocator)), + range.end <= id_alloc_capacity(old(allocator)) ==> forall|id: usize| #[trigger] + id_alloc_view(final(allocator)).contains(id) <==> id_alloc_view( + old(allocator), + ).contains(id) && !(range.start <= id < range.end), +; + +} // verus! /// I/O port allocator that allocates port I/O access to device drivers. +#[verus_verify] pub struct IoPortAllocator { /// Each ID indicates whether a Port I/O (1B) is allocated. /// @@ -21,12 +80,28 @@ pub struct IoPortAllocator { allocator: SpinLock, } +#[verus_verify] impl IoPortAllocator { /// Acquires the `IoPort`. Return None if any region in `port` cannot be allocated. + #[verus_spec(result => + requires + size_of::() <= u16::MAX, + port as usize + size_of::() <= u16::MAX, + ensures + result is Some ==> result->Some_0@ == port, + )] pub fn acquire(&self, port: u16) -> Option> { let mut allocator = self.allocator.lock(); let mut range = port..(port + size_of::() as u16); - if range.any(|i| allocator.is_allocated(i as usize)) { + // `Iterator::any` with a capturing closure is not supported by Verus. Original Rust: + // if range.any(|i| allocator.is_allocated(i as usize)) { return None; } + let mut already_allocated = false; + for i in range.clone() { + if allocator.is_allocated(i as usize) { + already_allocated = true; + } + } + if already_allocated { return None; } @@ -44,7 +119,7 @@ impl IoPortAllocator { /// /// The caller must have ownership of the PIO region through the `IoPortAllocator::acquire` interface. pub(in crate::io) unsafe fn recycle(&self, range: Range) { - debug!("Recycling MMIO range: {:#x?}", range); + /* debug!("Recycling MMIO range: {:#x?}", range); */ self.allocator .lock() @@ -52,6 +127,15 @@ impl IoPortAllocator { } } +verus! { + +/// Trusted boot-state fact required before accessing the global PIO allocator. +/// +/// Verus cannot currently mention an `exec static` in a specification, so this predicate is the +/// explicit specification boundary for the architecture's guarantee that [`init`] ran first. +pub uninterp spec fn io_port_allocator_initialized() -> bool; + +} // verus! pub(super) static IO_PORT_ALLOCATOR: Once = Once::new(); /// Initializes the static `IO_PORT_ALLOCATOR` and removes the system device I/O port regions. @@ -65,6 +149,7 @@ pub(super) static IO_PORT_ALLOCATOR: Once = Once::new(); /// /// 2. `MAX_IO_PORT` defined in `crate::arch::io` is guaranteed not to exceed the maximum /// value specified by architecture. +#[verifier::external_body] pub(crate) unsafe fn init() { // SAFETY: `MAX_IO_PORT` is guaranteed not to exceed the maximum value specified by architecture. let mut allocator = IdAlloc::with_capacity(crate::arch::io::MAX_IO_PORT as usize); diff --git a/ostd/src/io/io_port/mod.rs b/ostd/src/io/io_port/mod.rs index c6ea35bd2..54ac0e99e 100644 --- a/ostd/src/io/io_port/mod.rs +++ b/ostd/src/io/io_port/mod.rs @@ -3,11 +3,11 @@ use vstd::prelude::*; use crate::arch::device::io_port::{IoPortReadAccess, IoPortWriteAccess, PortRead, PortWrite}; -/*mod allocator;*/ +mod allocator; use core::{marker::PhantomData, mem::size_of}; -/*pub(super) use self::allocator::init;*/ +pub(super) use self::allocator::init; use crate::{Error, prelude::*}; /// An I/O port, representing a specific address in the I/O address of x86. @@ -40,16 +40,35 @@ impl View for IoPort { } } // verus! +/// Returns the initialized global PIO allocator. +/// +/// The executable body intentionally preserves the original `get().unwrap()` behavior. This +/// helper is trusted only because Verus cannot connect an `exec static` to a spec-level boot-state +/// predicate. +#[verifier::external_body] +#[verus_spec( + requires allocator::io_port_allocator_initialized(), +)] +fn initialized_allocator() -> &'static allocator::IoPortAllocator { + allocator::IO_PORT_ALLOCATOR.get().unwrap() +} + #[verus_verify] impl IoPort { /// Acquires an `IoPort` instance for the given range. - /*pub fn acquire(port: u16) -> Result> { - allocator::IO_PORT_ALLOCATOR - .get() - .unwrap() + #[verus_spec(result => + requires + size_of::() <= u16::MAX, + port as usize + size_of::() <= u16::MAX, + allocator::io_port_allocator_initialized(), + ensures + result is Ok ==> result->Ok_0@ == port, + )] + pub fn acquire(port: u16) -> Result> { + initialized_allocator() .acquire(port) .ok_or(Error::AccessDenied) - }*/ + } /// Returns the port number. #[verus_spec(returns self@)] @@ -68,7 +87,13 @@ impl IoPort { /// /// This function is marked unsafe as creating an I/O port is considered /// a privileged operation. - #[verus_spec(ret => ensures ret@ == port)] + #[verus_spec(ret => + requires + size_of::() <= u16::MAX, + port as usize + size_of::() <= u16::MAX, + ensures + ret@ == port, + )] pub const unsafe fn new(port: u16) -> Self { Self { port, @@ -98,7 +123,7 @@ impl IoPort { } } -/*impl Drop for IoPort { +impl Drop for IoPort { fn drop(&mut self) { // SAFETY: The caller have ownership of the PIO region. unsafe { @@ -108,7 +133,7 @@ impl IoPort { .recycle(self.port..(self.port + size_of::() as u16)); } } -}*/ +} /// Reserves an I/O port range which may refer to the port I/O range used by the /// system device driver. diff --git a/ostd/src/io/mod.rs b/ostd/src/io/mod.rs index 4de2932ff..b27636383 100644 --- a/ostd/src/io/mod.rs +++ b/ostd/src/io/mod.rs @@ -5,6 +5,8 @@ //! through _allocators_. There are two types of device I/O: //! - `IoMem` for memory I/O (MMIO). //! - `IoPort` for port I/O (PIO). +use vstd::prelude::*; + mod io_mem; use cfg_if::cfg_if; @@ -20,7 +22,6 @@ cfg_if!( } ); -/* /// Initializes the static allocator based on builder. /// /// # Safety @@ -35,6 +36,7 @@ cfg_if!( /// /// 3. `MAX_IO_PORT` defined in `crate::arch::io` is guaranteed not to /// exceed the maximum value specified by architecture. +#[verus_verify] pub(crate) unsafe fn init(io_mem_builder: IoMemAllocatorBuilder) { // SAFETY: The safety is upheld by the caller. unsafe { self::io_mem::init(io_mem_builder) }; @@ -44,4 +46,4 @@ pub(crate) unsafe fn init(io_mem_builder: IoMemAllocatorBuilder) { unsafe { self::io_port::init() }; -}*/ +} From 18d72c57fdc75d0d27b109c30694a119730eaa58 Mon Sep 17 00:00:00 2001 From: Marsman1996 Date: Thu, 13 Aug 2026 17:40:16 +0800 Subject: [PATCH 03/22] prove: port allocation and access --- Cargo.lock | 1 + Cargo.toml | 1 + ostd/Cargo.toml | 1 + ostd/src/arch/x86/device/io_port.rs | 29 ++- ostd/src/arch/x86/pci.rs | 19 +- ostd/src/io/io_port/allocator.rs | 354 ++++++++++++++++++++++++++-- ostd/src/io/io_port/mod.rs | 99 +++++++- 7 files changed, 476 insertions(+), 28 deletions(-) diff --git a/Cargo.lock b/Cargo.lock index fe004aa9a..2ce4cdc68 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -331,6 +331,7 @@ dependencies = [ "spin", "tdx-guest", "unwinding", + "verus_state_machines_macros", "volatile 0.6.1", "vstd", "vstd_extra", diff --git a/Cargo.toml b/Cargo.toml index 0963ca334..2a3b5dca8 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -51,3 +51,4 @@ codegen-units = 1 [workspace.dependencies] # Verus vstd = { path = "tools/verus/source/vstd", default-features = false, features = ["alloc"] } +verus_state_machines_macros = { path = "tools/verus/source/state_machines_macros" } \ No newline at end of file diff --git a/ostd/Cargo.toml b/ostd/Cargo.toml index 830b3a55d..e1e1e8591 100644 --- a/ostd/Cargo.toml +++ b/ostd/Cargo.toml @@ -18,6 +18,7 @@ targets = ["x86_64-unknown-none"] [dependencies] vstd = { workspace = true } vstd_extra = { path = "../verified_libs/vstd_extra" } +verus_state_machines_macros = { workspace = true } bitflags = { path = "../verified_libs/bitflags" } align_ext = { path = "libs/align_ext", version = "0.1.0" } bit_field = "0.10.1" diff --git a/ostd/src/arch/x86/device/io_port.rs b/ostd/src/arch/x86/device/io_port.rs index c86716257..10bc5b58f 100644 --- a/ostd/src/arch/x86/device/io_port.rs +++ b/ostd/src/arch/x86/device/io_port.rs @@ -10,8 +10,27 @@ pub use x86_64::{ use vstd::prelude::*; +use core::mem::size_of; + verus! { +/// Whether `port` is representable in the 16-bit x86 I/O-port address space. +/// +/// This is only the ISA-level validity condition. It does not claim that a device decodes the +/// port, that the current CPU context may access it, or that the caller owns it. +pub open spec fn valid_io_port_number(port: int) -> bool { + 0 <= port <= u16::MAX as int +} + +/// Whether an access of type `T` is fully contained in the x86 I/O-port address space. +/// +/// OSTD allocates one port byte for every byte in `T`, so this is stronger than merely checking +/// that the starting port is representable. +pub open spec fn valid_io_port_access(port: int) -> bool { + &&& valid_io_port_number(port) + &&& port + size_of::() <= u16::MAX as int + 1 +} + /// Opaque specification boundary for the third-party read/write access marker. #[verifier::external_type_specification] #[verifier::external_body] @@ -28,7 +47,10 @@ pub trait ExPortRead { type ExternalTraitSpecificationFor: PortRead; /// A port read can produce any value supplied by the device. - unsafe fn read_from_port(port: u16) -> Self where Self: Sized; + unsafe fn read_from_port(port: u16) -> Self where Self: Sized + requires + valid_io_port_access::(port as int), + ; } /// Trusted specification boundary for values that can be written to an x86 I/O port. @@ -37,7 +59,10 @@ pub trait ExPortWrite { type ExternalTraitSpecificationFor: PortWrite; /// A port write has no modeled logical effect on kernel memory. - unsafe fn write_to_port(port: u16, value: Self) where Self: Sized; + unsafe fn write_to_port(port: u16, value: Self) where Self: Sized + requires + valid_io_port_access::(port as int), + ; } } // verus! diff --git a/ostd/src/arch/x86/pci.rs b/ostd/src/arch/x86/pci.rs index 33832d995..889bbb5ee 100644 --- a/ostd/src/arch/x86/pci.rs +++ b/ostd/src/arch/x86/pci.rs @@ -13,12 +13,21 @@ pub assume_specification[ u32::to_le ](value: u32) -> (result: u32) result == value, ; -} // verus! -#[verus_verify] -static PCI_ADDRESS_PORT: IoPort = unsafe { IoPort::new(0x0CF8) }; -#[verus_verify] -static PCI_DATA_PORT: IoPort = unsafe { IoPort::new(0x0CFC) }; +exec static PCI_ADDRESS_PORT: IoPort + ensures + PCI_ADDRESS_PORT.well_formed(), +{ + unsafe { IoPort::new(0x0CF8) } +} +exec static PCI_DATA_PORT: IoPort + ensures + PCI_DATA_PORT.well_formed(), +{ + unsafe { IoPort::new(0x0CFC) } +} + +} // verus! #[verus_verify] const BIT32_ALIGN_MASK: u32 = 0xFFFC; diff --git a/ostd/src/io/io_port/allocator.rs b/ostd/src/io/io_port/allocator.rs index f4bff93f6..ff4cad016 100644 --- a/ostd/src/io/io_port/allocator.rs +++ b/ostd/src/io/io_port/allocator.rs @@ -1,6 +1,8 @@ // SPDX-License-Identifier: MPL-2.0 //! I/O port allocator. +use verus_state_machines_macros::tokenized_state_machine; use vstd::prelude::*; +use vstd::tokens::{InstanceId, SetToken, ValueToken}; use core::ops::Range; @@ -8,7 +10,7 @@ use id_alloc::IdAlloc; use log::debug; use spin::Once; -use super::IoPort; +use super::{IoPort, lemma_port_id_set_contains, lemma_port_id_set_insert, port_id_set}; use crate::{ io::RawIoPortRange, sync::{LocalIrqDisabled, SpinLock}, @@ -34,6 +36,21 @@ pub uninterp spec fn id_alloc_view(allocator: &IdAlloc) -> Set; /// Capacity configured for an external `IdAlloc`. pub uninterp spec fn id_alloc_capacity(allocator: &IdAlloc) -> usize; +/// Identity assigned to the single global PIO allocator during trusted boot initialization. +pub uninterp spec fn io_port_allocator_instance_id() -> InstanceId; + +closed spec fn io_port_inner_inv_values( + instance_id: InstanceId, + allocated_instance_id: InstanceId, + allocated: Set, + allocator: &IdAlloc, +) -> bool { + &&& instance_id == io_port_allocator_instance_id() + &&& allocated_instance_id == io_port_allocator_instance_id() + &&& allocated.subset_of(id_alloc_view(allocator)) + &&& id_alloc_capacity(allocator) == crate::arch::io::MAX_IO_PORT as usize +} + pub assume_specification[ IdAlloc::with_capacity ](capacity: usize) -> (allocator: IdAlloc) ensures id_alloc_capacity(&allocator) == capacity, @@ -48,27 +65,154 @@ pub assume_specification[ IdAlloc::is_allocated ](allocator: &IdAlloc, id: usize pub assume_specification[ IdAlloc::alloc_specific ](allocator: &mut IdAlloc, id: usize) -> (result: Option) + requires + id < id_alloc_capacity(old(allocator)), ensures id_alloc_capacity(final(allocator)) == id_alloc_capacity(old(allocator)), - id < id_alloc_capacity(old(allocator)) && id_alloc_view(old(allocator)).contains(id) ==> { + id_alloc_view(final(allocator)) == id_alloc_view(old(allocator)).insert(id), + id_alloc_view(old(allocator)).subset_of(id_alloc_view(final(allocator))), + id_alloc_view(old(allocator)).contains(id) ==> { &&& result is None - &&& id_alloc_view(final(allocator)) == id_alloc_view(old(allocator)) }, - id < id_alloc_capacity(old(allocator)) && !id_alloc_view(old(allocator)).contains(id) ==> { + !id_alloc_view(old(allocator)).contains(id) ==> { &&& result == Some(id) - &&& id_alloc_view(final(allocator)) == id_alloc_view(old(allocator)).insert(id) }, + no_unwind ; pub assume_specification[ IdAlloc::free_consecutive ](allocator: &mut IdAlloc, range: Range) + requires + range.end <= id_alloc_capacity(old(allocator)), ensures id_alloc_capacity(final(allocator)) == id_alloc_capacity(old(allocator)), - range.end <= id_alloc_capacity(old(allocator)) ==> forall|id: usize| #[trigger] + forall|id: usize| #[trigger] id_alloc_view(final(allocator)).contains(id) <==> id_alloc_view( old(allocator), ).contains(id) && !(range.start <= id < range.end), + no_unwind ; +} // verus! +/// Transparent facade used only to pass ghost frame facts to the third-party mutation. +#[repr(transparent)] +#[verus_verify] +struct ModeledIdAlloc { + inner: IdAlloc, +} + +#[verus_verify] +impl ModeledIdAlloc { + #[verus_spec(result => + with + Ghost(instance_id): Ghost, + Ghost(allocated_instance_id): Ghost, + Ghost(preserved): Ghost>, + requires + id < id_alloc_capacity(&old(self).inner), + io_port_inner_inv_values( + instance_id, + allocated_instance_id, + preserved, + &old(self).inner, + ), + ensures + id_alloc_capacity(&final(self).inner) == id_alloc_capacity(&old(self).inner), + id_alloc_view(&final(self).inner) == id_alloc_view(&old(self).inner).insert(id), + id_alloc_view(&old(self).inner).subset_of(id_alloc_view(&final(self).inner)), + preserved.subset_of(id_alloc_view(&final(self).inner)), + io_port_inner_inv_values( + instance_id, + allocated_instance_id, + preserved, + &final(self).inner, + ), + id_alloc_view(&old(self).inner).contains(id) ==> result is None, + !id_alloc_view(&old(self).inner).contains(id) ==> result == Some(id), + no_unwind + )] + fn alloc_specific(&mut self, id: usize) -> Option { + self.inner.alloc_specific(id) + } +} + +verus! { + +tokenized_state_machine! { + IoPortAllocationState { + fields { + #[sharding(variable)] + pub allocated: Set, + #[sharding(set)] + pub claims: Set, + } + + #[invariant] + pub fn allocated_matches_claims(&self) -> bool { + self.allocated =~= self.claims + } + + init! { + initialize() { + init allocated = Set::empty(); + init claims = Set::empty(); + } + } + + transition! { + allocate(ids: Set) { + require pre.allocated.disjoint(ids); + update allocated = pre.allocated.union(ids); + add claims += (ids) by { + assert(pre.claims =~= pre.allocated); + }; + } + } + + transition! { + release(ids: Set) { + update allocated = pre.allocated.difference(ids); + remove claims -= (ids); + } + } + + #[inductive(initialize)] + fn initialize_inductive(post: Self) {} + + #[inductive(allocate)] + fn allocate_inductive(pre: Self, post: Self, ids: Set) {} + + #[inductive(release)] + fn release_inductive(pre: Self, post: Self, ids: Set) {} + } +} + +} // verus! +pub(super) type IoPortClaim = IoPortAllocationState::claims_set; + +/// Lock-protected executable bitmap and the state-machine token that models it. +#[verus_verify] +struct IoPortAllocatorInner { + allocator: ModeledIdAlloc, + #[cfg(verus_keep_ghost_body)] + tracked_instance: Tracked, + #[cfg(verus_keep_ghost_body)] + tracked_allocated: Tracked, +} + +verus! { + +impl IoPortAllocatorInner { + #[verifier::type_invariant] + pub closed spec fn type_inv(self) -> bool { + io_port_inner_inv_values( + self.tracked_instance@.id(), + self.tracked_allocated@.instance_id(), + self.tracked_allocated@.value(), + &self.allocator.inner, + ) + } +} + } // verus! /// I/O port allocator that allocates port I/O access to device drivers. #[verus_verify] @@ -77,40 +221,171 @@ pub struct IoPortAllocator { /// /// Instead of using `RangeAllocator` like `IoMemAllocator` does, it is more reasonable to use `IdAlloc`, /// as PIO space includes only a small region; for example, x86 module in OSTD allows just 65536 I/O ports. - allocator: SpinLock, + allocator: SpinLock, } #[verus_verify] impl IoPortAllocator { /// Acquires the `IoPort`. Return None if any region in `port` cannot be allocated. #[verus_spec(result => + with + -> claim: Tracked>, requires + vstd::layout::size_of::() <= u16::MAX, size_of::() <= u16::MAX, port as usize + size_of::() <= u16::MAX, ensures result is Some ==> result->Some_0@ == port, + result is Some ==> result->Some_0.well_formed(), + result is Some <==> claim@ is Some, + result is Some ==> claim@->Some_0.instance_id() == + io_port_allocator_instance_id(), + result is Some ==> result->Some_0.claim_matches_set(claim@->Some_0.set()), )] pub fn acquire(&self, port: u16) -> Option> { let mut allocator = self.allocator.lock(); + let allocator_inner = &mut *allocator; + proof! { + use_type_invariant(&*allocator_inner); + } let mut range = port..(port + size_of::() as u16); // `Iterator::any` with a capturing closure is not supported by Verus. Original Rust: // if range.any(|i| allocator.is_allocated(i as usize)) { return None; } let mut already_allocated = false; + #[verus_spec(scan_iter => + invariant + allocator_inner.type_inv(), + !already_allocated ==> forall|id: usize| + range.start as usize <= id < + (range.start as int + scan_iter.index()) as usize ==> + !id_alloc_view(&allocator_inner.allocator.inner).contains(id), + )] for i in range.clone() { - if allocator.is_allocated(i as usize) { + if allocator_inner.allocator.inner.is_allocated(i as usize) { already_allocated = true; } } + proof_decl! { + let tracked range_claim: IoPortClaim; + } if already_allocated { - return None; + allocator.drop(); + return { + proof_with!(|= Tracked(None)); + None + }; } + proof_decl! { + let ghost ids = port_id_set(range.start as usize, range.end as usize); + let ghost allocation_start_view = id_alloc_view(&allocator_inner.allocator.inner); + } + proof! { + assert(ids.disjoint(id_alloc_view(&allocator_inner.allocator.inner))) by { + assert forall|id: usize| #[trigger] ids.contains(id) implies + !id_alloc_view(&allocator_inner.allocator.inner).contains(id) by { + lemma_port_id_set_contains( + range.start as usize, + range.end as usize, + id, + ); + } + } + assert forall|id: usize| ids.contains(id) implies + id < id_alloc_capacity(&allocator_inner.allocator.inner) by { + lemma_port_id_set_contains( + range.start as usize, + range.end as usize, + id, + ); + } + assert forall|id: usize| + range.start as usize <= id < range.end as usize implies + !id_alloc_view(&allocator_inner.allocator.inner).contains(id) by { + lemma_port_id_set_contains( + range.start as usize, + range.end as usize, + id, + ); + } + } + #[verus_spec(allocation_iter => + invariant + range.end as usize <= id_alloc_capacity(&allocator_inner.allocator.inner), + allocator_inner.tracked_instance@.id() == io_port_allocator_instance_id(), + allocator_inner.tracked_allocated@.instance_id() == + io_port_allocator_instance_id(), + allocator_inner.tracked_allocated@.value().subset_of(allocation_start_view), + allocator_inner.tracked_allocated@.value().subset_of( + id_alloc_view(&allocator_inner.allocator.inner), + ), + id_alloc_capacity(&allocator_inner.allocator.inner) == + crate::arch::io::MAX_IO_PORT as usize, + id_alloc_view(&allocator_inner.allocator.inner) =~= + allocation_start_view.union( + port_id_set( + range.start as usize, + (range.start as int + allocation_iter.index()) as usize, + ), + ), + forall|id: usize| + (range.start as int + allocation_iter.index()) as usize <= id < + range.end as usize ==> + !id_alloc_view(&allocator_inner.allocator.inner).contains(id), + )] for i in range.clone() { - allocator.alloc_specific(i as usize); + proof_decl! { + let ghost old_view = id_alloc_view(&allocator_inner.allocator.inner); + } + proof! { + assert((i as usize) == + (range.start as int + allocation_iter.index()) as usize); + assert((i as usize) < id_alloc_capacity(&allocator_inner.allocator.inner)); + assert(!id_alloc_view(&allocator_inner.allocator.inner).contains(i as usize)); + assert(allocator_inner.tracked_allocated@.value().subset_of( + old_view.insert(i as usize), + )) by { + assert forall|id: usize| + allocator_inner.tracked_allocated@.value().contains(id) implies + old_view.insert(i as usize).contains(id) by { + } + } + assert(io_port_inner_inv_values( + allocator_inner.tracked_instance@.id(), + allocator_inner.tracked_allocated@.instance_id(), + allocator_inner.tracked_allocated@.value(), + &allocator_inner.allocator.inner, + )); + } + #[verus_spec(with + Ghost(allocator_inner.tracked_instance@.id()), + Ghost(allocator_inner.tracked_allocated@.instance_id()), + Ghost(allocator_inner.tracked_allocated@.value()), + )] + let _ = allocator_inner.allocator.alloc_specific(i as usize); + proof! { + lemma_port_id_set_insert(range.start as usize, i as usize); + assert(id_alloc_view(&allocator_inner.allocator.inner) =~= + old_view.insert(i as usize)); + } + } + proof! { + assert(ids.disjoint(allocator_inner.tracked_allocated@.value())) by { + assert forall|id: usize| #[trigger] ids.contains(id) implies + !allocator_inner.tracked_allocated@.value().contains(id) by { + } + } + range_claim = allocator_inner.tracked_instance.borrow().allocate( + ids, + allocator_inner.tracked_allocated.borrow_mut(), + ); } // SAFETY: The created IoPort is guaranteed not to access system device I/O - unsafe { Some(IoPort::new(port)) } + let result = unsafe { Some(IoPort::new(port)) }; + allocator.drop(); + proof_with!(|= Tracked(Some(range_claim))); + result } /// Recycles an PIO range. @@ -118,12 +393,47 @@ impl IoPortAllocator { /// # Safety /// /// The caller must have ownership of the PIO region through the `IoPortAllocator::acquire` interface. + #[verus_spec( + with + Tracked(claim): Tracked, + requires + claim.instance_id() == io_port_allocator_instance_id(), + claim.set() =~= port_id_set(range.start as usize, range.end as usize), + range.start <= range.end, + )] pub(in crate::io) unsafe fn recycle(&self, range: Range) { /* debug!("Recycling MMIO range: {:#x?}", range); */ - self.allocator - .lock() + let mut allocator = self.allocator.lock(); + let allocator_inner = &mut *allocator; + proof_decl! { + let ghost ids = port_id_set(range.start as usize, range.end as usize); + } + proof! { + use_type_invariant(&*allocator_inner); + assert(range.start as usize <= range.end as usize); + allocator_inner.tracked_instance.borrow().release( + ids, + allocator_inner.tracked_allocated.borrow_mut(), + claim, + ); + assert forall|id: usize| + #[trigger] allocator_inner.tracked_allocated@.value().contains(id) implies { + &&& id_alloc_view(&allocator_inner.allocator.inner).contains(id) + &&& !(range.start as usize <= id < range.end as usize) + } by { + lemma_port_id_set_contains( + range.start as usize, + range.end as usize, + id, + ); + } + } + allocator_inner + .allocator + .inner .free_consecutive(range.start as usize..range.end as usize); + allocator.drop(); } } @@ -177,7 +487,21 @@ pub(crate) unsafe fn init() { } } - IO_PORT_ALLOCATOR.call_once(|| IoPortAllocator { - allocator: SpinLock::new(allocator), + IO_PORT_ALLOCATOR.call_once(|| { + proof_decl! { + let tracked (Tracked(instance), Tracked(allocated), Tracked(_empty_claims)) = + IoPortAllocationState::Instance::initialize(); + } + let inner = IoPortAllocatorInner { + allocator: ModeledIdAlloc { inner: allocator }, + #[cfg(verus_keep_ghost_body)] + tracked_instance: Tracked::new(instance), + #[cfg(verus_keep_ghost_body)] + tracked_allocated: Tracked::new(allocated), + }; + // Original Rust: `IoPortAllocator { allocator: SpinLock::new(allocator) }`. + IoPortAllocator { + allocator: SpinLock::new(inner), + } }); } diff --git a/ostd/src/io/io_port/mod.rs b/ostd/src/io/io_port/mod.rs index 54ac0e99e..c541cb1b5 100644 --- a/ostd/src/io/io_port/mod.rs +++ b/ostd/src/io/io_port/mod.rs @@ -2,7 +2,9 @@ //! I/O port and its allocator that allocates port I/O (PIO) to device drivers. use vstd::prelude::*; -use crate::arch::device::io_port::{IoPortReadAccess, IoPortWriteAccess, PortRead, PortWrite}; +use crate::arch::device::io_port::{ + IoPortReadAccess, IoPortWriteAccess, PortRead, PortWrite, valid_io_port_access, +}; mod allocator; use core::{marker::PhantomData, mem::size_of}; @@ -39,6 +41,53 @@ impl View for IoPort { } } +impl IoPort { + /// The complete byte range occupied by this typed port lies in the x86 PIO address space. + #[verifier::type_invariant] + pub open spec fn well_formed(&self) -> bool { + valid_io_port_access::(self@ as int) + } + + /// Whether `claim` is the allocator-issued ownership token for this complete typed range. + pub open spec fn claim_matches_set(&self, claim: Set) -> bool { + claim =~= port_id_set(self@ as usize, (self@ as usize + size_of::()) as usize) + } +} + +/// Set of byte-sized PIO numbers in the half-open interval `[start, end)`. +pub open spec fn port_id_set(start: usize, end: usize) -> Set + decreases end - start, +{ + if start < end { + port_id_set(start, (end - 1) as usize).insert((end - 1) as usize) + } else { + Set::empty() + } +} + +/// Extending a PIO interval by one byte is equivalent to inserting its old endpoint. +pub proof fn lemma_port_id_set_insert(start: usize, end: usize) + requires + start <= end, + end < usize::MAX, + ensures + port_id_set(start, end).insert(end) == port_id_set(start, (end + 1) as usize), +{ +} + +/// Membership characterization for [`port_id_set`]. +pub proof fn lemma_port_id_set_contains(start: usize, end: usize, id: usize) + requires + start <= end, + ensures + port_id_set(start, end).contains(id) <==> start <= id < end, + decreases end - start, +{ + if start < end { + lemma_port_id_set_contains(start, (end - 1) as usize, id); + } +} + } // verus! /// Returns the initialized global PIO allocator. /// @@ -57,17 +106,30 @@ fn initialized_allocator() -> &'static allocator::IoPortAllocator { impl IoPort { /// Acquires an `IoPort` instance for the given range. #[verus_spec(result => + with + -> claim: Tracked>, requires + vstd::layout::size_of::() <= u16::MAX, size_of::() <= u16::MAX, port as usize + size_of::() <= u16::MAX, allocator::io_port_allocator_initialized(), ensures result is Ok ==> result->Ok_0@ == port, + result is Ok ==> result->Ok_0.well_formed(), + result is Ok <==> claim@ is Some, + result is Ok ==> claim@->Some_0.instance_id() == + allocator::io_port_allocator_instance_id(), + result is Ok ==> result->Ok_0.claim_matches_set(claim@->Some_0.set()), )] pub fn acquire(port: u16) -> Result> { - initialized_allocator() - .acquire(port) - .ok_or(Error::AccessDenied) + proof_decl! { + let tracked claim: Option; + } + #[verus_spec(with => Tracked(claim))] + let port = initialized_allocator().acquire(port); + let result = port.ok_or(Error::AccessDenied); + proof_with!(|= Tracked(claim)); + result } /// Returns the port number. @@ -89,10 +151,12 @@ impl IoPort { /// a privileged operation. #[verus_spec(ret => requires + vstd::layout::size_of::() <= u16::MAX, size_of::() <= u16::MAX, port as usize + size_of::() <= u16::MAX, ensures ret@ == port, + ret.well_formed(), )] pub const unsafe fn new(port: u16) -> Self { Self { @@ -101,6 +165,27 @@ impl IoPort { access_marker: PhantomData, } } + + /// Releases the allocator claim for this port. + /// + /// VERUS LIMITATION: this is called explicitly because Verus does not yet support proving the + /// standard `Drop` implementation below. + #[verus_spec( + with + Tracked(claim): Tracked, + requires + allocator::io_port_allocator_initialized(), + claim.instance_id() == allocator::io_port_allocator_instance_id(), + self.claim_matches_set(claim.set()), + self@ as usize + size_of::() <= u16::MAX, + )] + pub fn drop(self) { + let range = self.port..(self.port + size_of::() as u16); + unsafe { + #[verus_spec(with Tracked(claim))] + initialized_allocator().recycle(range); + } + } } #[verus_verify] @@ -108,6 +193,7 @@ impl IoPort { impl IoPort { /// Reads from the I/O port #[inline] + #[verus_spec(requires self.well_formed())] pub fn read(&self) -> T { unsafe { PortRead::read_from_port(self.port) } } @@ -118,12 +204,13 @@ impl IoPort { impl IoPort { /// Writes to the I/O port #[inline] + #[verus_spec(requires self.well_formed())] pub fn write(&self, value: T) { unsafe { PortWrite::write_to_port(self.port, value) } } } -impl Drop for IoPort { +/* impl Drop for IoPort { fn drop(&mut self) { // SAFETY: The caller have ownership of the PIO region. unsafe { @@ -133,7 +220,7 @@ impl Drop for IoPort { .recycle(self.port..(self.port + size_of::() as u16)); } } -} +} */ /// Reserves an I/O port range which may refer to the port I/O range used by the /// system device driver. From e4775af1b81849c282623e7efce18aaa4b6289ba Mon Sep 17 00:00:00 2001 From: Marsman1996 Date: Tue, 25 Aug 2026 10:45:53 +0800 Subject: [PATCH 04/22] refactor: move x86 I/O port specs to vstd_extra --- Cargo.lock | 1 + Cargo.toml | 2 +- ostd/src/arch/x86/device/io_port.rs | 60 +------------------ verified_libs/vstd_extra/Cargo.toml | 3 + .../vstd_extra/src/external/io_port.rs | 60 +++++++++++++++++++ verified_libs/vstd_extra/src/external/mod.rs | 4 ++ 6 files changed, 70 insertions(+), 60 deletions(-) create mode 100644 verified_libs/vstd_extra/src/external/io_port.rs diff --git a/Cargo.lock b/Cargo.lock index 2ce4cdc68..b49ac284f 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -672,6 +672,7 @@ name = "vstd_extra" version = "0.1.0" dependencies = [ "vstd", + "x86_64", ] [[package]] diff --git a/Cargo.toml b/Cargo.toml index 2a3b5dca8..b7836d68d 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -51,4 +51,4 @@ codegen-units = 1 [workspace.dependencies] # Verus vstd = { path = "tools/verus/source/vstd", default-features = false, features = ["alloc"] } -verus_state_machines_macros = { path = "tools/verus/source/state_machines_macros" } \ No newline at end of file +verus_state_machines_macros = { path = "tools/verus/source/state_machines_macros" } diff --git a/ostd/src/arch/x86/device/io_port.rs b/ostd/src/arch/x86/device/io_port.rs index 10bc5b58f..99c6fade2 100644 --- a/ostd/src/arch/x86/device/io_port.rs +++ b/ostd/src/arch/x86/device/io_port.rs @@ -1,5 +1,6 @@ // SPDX-License-Identifier: MPL-2.0 //! I/O port access. +pub use vstd_extra::external::{valid_io_port_access, valid_io_port_number}; pub use x86_64::{ instructions::port::{ PortReadAccess as IoPortReadAccess, PortWriteAccess as IoPortWriteAccess, ReadOnlyAccess, @@ -7,62 +8,3 @@ pub use x86_64::{ }, structures::port::{PortRead, PortWrite}, }; - -use vstd::prelude::*; - -use core::mem::size_of; - -verus! { - -/// Whether `port` is representable in the 16-bit x86 I/O-port address space. -/// -/// This is only the ISA-level validity condition. It does not claim that a device decodes the -/// port, that the current CPU context may access it, or that the caller owns it. -pub open spec fn valid_io_port_number(port: int) -> bool { - 0 <= port <= u16::MAX as int -} - -/// Whether an access of type `T` is fully contained in the x86 I/O-port address space. -/// -/// OSTD allocates one port byte for every byte in `T`, so this is stronger than merely checking -/// that the starting port is representable. -pub open spec fn valid_io_port_access(port: int) -> bool { - &&& valid_io_port_number(port) - &&& port + size_of::() <= u16::MAX as int + 1 -} - -/// Opaque specification boundary for the third-party read/write access marker. -#[verifier::external_type_specification] -#[verifier::external_body] -pub struct ExReadWriteAccess(ReadWriteAccess); - -/// Opaque specification boundary for the third-party write-only access marker. -#[verifier::external_type_specification] -#[verifier::external_body] -pub struct ExWriteOnlyAccess(WriteOnlyAccess); - -/// Trusted specification boundary for values that can be read from an x86 I/O port. -#[verifier::external_trait_specification] -pub trait ExPortRead { - type ExternalTraitSpecificationFor: PortRead; - - /// A port read can produce any value supplied by the device. - unsafe fn read_from_port(port: u16) -> Self where Self: Sized - requires - valid_io_port_access::(port as int), - ; -} - -/// Trusted specification boundary for values that can be written to an x86 I/O port. -#[verifier::external_trait_specification] -pub trait ExPortWrite { - type ExternalTraitSpecificationFor: PortWrite; - - /// A port write has no modeled logical effect on kernel memory. - unsafe fn write_to_port(port: u16, value: Self) where Self: Sized - requires - valid_io_port_access::(port as int), - ; -} - -} // verus! diff --git a/verified_libs/vstd_extra/Cargo.toml b/verified_libs/vstd_extra/Cargo.toml index 2f02cd467..1455796e1 100644 --- a/verified_libs/vstd_extra/Cargo.toml +++ b/verified_libs/vstd_extra/Cargo.toml @@ -15,3 +15,6 @@ std = ["vstd/std"] [dependencies] vstd = { workspace = true } + +[target.'cfg(target_arch = "x86_64")'.dependencies] +x86_64 = "0.14.13" diff --git a/verified_libs/vstd_extra/src/external/io_port.rs b/verified_libs/vstd_extra/src/external/io_port.rs new file mode 100644 index 000000000..96b810b22 --- /dev/null +++ b/verified_libs/vstd_extra/src/external/io_port.rs @@ -0,0 +1,60 @@ +//! Specifications for x86 I/O-port access types and traits. +use core::mem::size_of; + +use vstd::prelude::*; +use x86_64::{ + instructions::port::{ReadWriteAccess, WriteOnlyAccess}, + structures::port::{PortRead, PortWrite}, +}; + +verus! { + +/// Whether `port` is representable in the 16-bit x86 I/O-port address space. +/// +/// This is only the ISA-level validity condition. It does not claim that a device decodes the +/// port, that the current CPU context may access it, or that the caller owns it. +pub open spec fn valid_io_port_number(port: int) -> bool { + 0 <= port <= u16::MAX as int +} + +/// Whether an access of type `T` is fully contained in the x86 I/O-port address space. +pub open spec fn valid_io_port_access(port: int) -> bool { + &&& valid_io_port_number(port) + &&& port + size_of::() <= u16::MAX as int + 1 +} + +/// Opaque specification boundary for the third-party read/write access marker. +#[verifier::external_type_specification] +#[verifier::external_body] +pub struct ExReadWriteAccess(ReadWriteAccess); + +/// Opaque specification boundary for the third-party write-only access marker. +#[verifier::external_type_specification] +#[verifier::external_body] +pub struct ExWriteOnlyAccess(WriteOnlyAccess); + +/// Trusted specification boundary for values that can be read from an x86 I/O port. +#[verifier::external_trait_specification] +pub trait ExPortRead { + type ExternalTraitSpecificationFor: PortRead; + + /// A port read can produce any value supplied by the device. + unsafe fn read_from_port(port: u16) -> Self where Self: Sized + requires + valid_io_port_access::(port as int), + ; +} + +/// Trusted specification boundary for values that can be written to an x86 I/O port. +#[verifier::external_trait_specification] +pub trait ExPortWrite { + type ExternalTraitSpecificationFor: PortWrite; + + /// A port write has no modeled logical effect on kernel memory. + unsafe fn write_to_port(port: u16, value: Self) where Self: Sized + requires + valid_io_port_access::(port as int), + ; +} + +} // verus! diff --git a/verified_libs/vstd_extra/src/external/mod.rs b/verified_libs/vstd_extra/src/external/mod.rs index f4071583b..b399bf1e0 100644 --- a/verified_libs/vstd_extra/src/external/mod.rs +++ b/verified_libs/vstd_extra/src/external/mod.rs @@ -7,6 +7,8 @@ pub mod convert; pub mod deref; pub mod ilog2; pub mod int_specs; +#[cfg(target_arch = "x86_64")] +pub mod io_port; pub mod nonnull; pub mod ptr; pub mod range; @@ -17,6 +19,8 @@ pub mod time; pub use btree::*; pub use ilog2::*; pub use int_specs::*; +#[cfg(target_arch = "x86_64")] +pub use io_port::*; pub use nonnull::*; pub use ptr::*; pub use range::*; From 6750b28f84b2d529dc078c0e37ba054d2a840e29 Mon Sep 17 00:00:00 2001 From: Marsman1996 Date: Wed, 2 Sep 2026 15:31:01 +0800 Subject: [PATCH 05/22] refactor: replace state machine macros with ghost tokens --- Cargo.lock | 1 - Cargo.toml | 1 - ostd/Cargo.toml | 1 - ostd/src/io/io_mem/allocator.rs | 38 +++++++- ostd/src/io/io_mem/mod.rs | 1 + ostd/src/io/io_port/allocator.rs | 152 +++++++++++++++---------------- 6 files changed, 109 insertions(+), 85 deletions(-) diff --git a/Cargo.lock b/Cargo.lock index cdc0fc1ae..b2b577219 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -331,7 +331,6 @@ dependencies = [ "spin", "tdx-guest", "unwinding", - "verus_state_machines_macros", "volatile 0.6.1", "vstd", "vstd_extra", diff --git a/Cargo.toml b/Cargo.toml index b7836d68d..0963ca334 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -51,4 +51,3 @@ codegen-units = 1 [workspace.dependencies] # Verus vstd = { path = "tools/verus/source/vstd", default-features = false, features = ["alloc"] } -verus_state_machines_macros = { path = "tools/verus/source/state_machines_macros" } diff --git a/ostd/Cargo.toml b/ostd/Cargo.toml index e1e1e8591..830b3a55d 100644 --- a/ostd/Cargo.toml +++ b/ostd/Cargo.toml @@ -18,7 +18,6 @@ targets = ["x86_64-unknown-none"] [dependencies] vstd = { workspace = true } vstd_extra = { path = "../verified_libs/vstd_extra" } -verus_state_machines_macros = { workspace = true } bitflags = { path = "../verified_libs/bitflags" } align_ext = { path = "libs/align_ext", version = "0.1.0" } bit_field = "0.10.1" diff --git a/ostd/src/io/io_mem/allocator.rs b/ostd/src/io/io_mem/allocator.rs index cfa98c8aa..4e5cff9c2 100644 --- a/ostd/src/io/io_mem/allocator.rs +++ b/ostd/src/io/io_mem/allocator.rs @@ -3,6 +3,7 @@ use crate::specs::arch::PAGE_SIZE; use crate::sync::{OnceImpl, TrivialPred}; use vstd::prelude::*; +use vstd_extra::resource::flags::OneShotSet; use alloc::vec::Vec; use core::ops::Range; @@ -32,15 +33,26 @@ impl IoMemAllocator { vstd::arithmetic::power2::is_pow2(PAGE_SIZE as int), range.start < range.end, range.end <= usize::MAX - (PAGE_SIZE - 1), + io_mem_range_registered(range), ensures result is Some ==> result->Some_0.paddr_spec() == range.start, result is Some ==> result->Some_0.length_spec() == vstd_extra::external::range::range_usize_len_spec(&range), )] pub fn acquire(&self, range: Range) -> Option { - find_allocator(&self.allocators, &range)? - .alloc_specific(&range) - .ok()?; + let allocator = find_allocator(&self.allocators, &range)?; + proof! { + // Trusted boot fact (`io_mem_range_registered`): `range` was registered inside a + // single builder window, and `find_allocator` returns its first overlapping window, + // which is the containing window because the registered windows are disjoint. + assume(allocator@.start <= range.start && range.end <= allocator@.end); + } + proof_decl! { + let tracked initialized: OneShotSet; + } + let result = #[verus_spec(with => Tracked(initialized))] + allocator.alloc_specific(&range); + result.ok()?; /* debug!("Acquiring MMIO range:{:x?}..{:x?}", range.start, range.end); */ @@ -111,13 +123,23 @@ impl IoMemAllocatorBuilder { requires range.start < range.end, vstd_extra::panic::may_panic(), + io_mem_range_registered(range), )] pub(crate) fn remove(&self, range: Range) { // Formatting machinery used by the original panic is not modeled by Verus. // Original Rust used two formatted `panic!` branches here. let allocator = find_allocator(&self.allocators, &range); vstd_extra::assert!(allocator.is_some()); - let result = allocator.unwrap().alloc_specific(&range); + let allocator = allocator.unwrap(); + proof! { + // Trusted boot fact, same reasoning as in `acquire`. + assume(allocator@.start <= range.start && range.end <= allocator@.end); + } + proof_decl! { + let tracked initialized: OneShotSet; + } + let result = #[verus_spec(with => Tracked(initialized))] + allocator.alloc_specific(&range); vstd_extra::assert!(result.is_ok()); } } @@ -125,6 +147,14 @@ impl IoMemAllocatorBuilder { /// The I/O Memory allocator of the system. verus! { +/// Trusted boot-state fact required before allocating or removing a `range`. +/// +/// Verus cannot mention an exec static in a specification, so this predicate is the explicit +/// specification boundary for the boot-time guarantee that `range` was registered inside a +/// single MMIO window of the builder (and the windows are pairwise disjoint), which is what +/// `RangeAllocator::alloc_specific` requires. +pub uninterp spec fn io_mem_range_registered(range: Range) -> bool; + pub exec static IO_MEM_ALLOCATOR: OnceImpl ensures IO_MEM_ALLOCATOR.wf(), diff --git a/ostd/src/io/io_mem/mod.rs b/ostd/src/io/io_mem/mod.rs index c92c2a947..8c7d91153 100644 --- a/ostd/src/io/io_mem/mod.rs +++ b/ostd/src/io/io_mem/mod.rs @@ -74,6 +74,7 @@ impl IoMem { vstd::arithmetic::power2::is_pow2(PAGE_SIZE as int), range.start < range.end, range.end <= usize::MAX - (PAGE_SIZE - 1), + allocator::io_mem_range_registered(range), ensures result is Ok ==> result->Ok_0.paddr_spec() == range.start, result is Ok ==> result->Ok_0.length_spec() diff --git a/ostd/src/io/io_port/allocator.rs b/ostd/src/io/io_port/allocator.rs index ff4cad016..1917aa128 100644 --- a/ostd/src/io/io_port/allocator.rs +++ b/ostd/src/io/io_port/allocator.rs @@ -1,8 +1,8 @@ // SPDX-License-Identifier: MPL-2.0 //! I/O port allocator. -use verus_state_machines_macros::tokenized_state_machine; use vstd::prelude::*; -use vstd::tokens::{InstanceId, SetToken, ValueToken}; +use vstd::resource::set::{GhostSetAuth, GhostSubset}; +use vstd::tokens::InstanceId; use core::ops::Range; @@ -40,12 +40,10 @@ pub uninterp spec fn id_alloc_capacity(allocator: &IdAlloc) -> usize; pub uninterp spec fn io_port_allocator_instance_id() -> InstanceId; closed spec fn io_port_inner_inv_values( - instance_id: InstanceId, allocated_instance_id: InstanceId, allocated: Set, allocator: &IdAlloc, ) -> bool { - &&& instance_id == io_port_allocator_instance_id() &&& allocated_instance_id == io_port_allocator_instance_id() &&& allocated.subset_of(id_alloc_view(allocator)) &&& id_alloc_capacity(allocator) == crate::arch::io::MAX_IO_PORT as usize @@ -104,24 +102,17 @@ struct ModeledIdAlloc { impl ModeledIdAlloc { #[verus_spec(result => with - Ghost(instance_id): Ghost, Ghost(allocated_instance_id): Ghost, Ghost(preserved): Ghost>, requires id < id_alloc_capacity(&old(self).inner), - io_port_inner_inv_values( - instance_id, - allocated_instance_id, - preserved, - &old(self).inner, - ), + io_port_inner_inv_values(allocated_instance_id, preserved, &old(self).inner), ensures id_alloc_capacity(&final(self).inner) == id_alloc_capacity(&old(self).inner), id_alloc_view(&final(self).inner) == id_alloc_view(&old(self).inner).insert(id), id_alloc_view(&old(self).inner).subset_of(id_alloc_view(&final(self).inner)), preserved.subset_of(id_alloc_view(&final(self).inner)), io_port_inner_inv_values( - instance_id, allocated_instance_id, preserved, &final(self).inner, @@ -137,66 +128,87 @@ impl ModeledIdAlloc { verus! { -tokenized_state_machine! { - IoPortAllocationState { - fields { - #[sharding(variable)] - pub allocated: Set, - #[sharding(set)] - pub claims: Set, - } +/// Authority over the set of PIO ids currently allocated by the global allocator. +/// +/// The `Loc` of `auth` identifies the protocol instance and `auth@` is the set of allocated +/// ids. [`IoPortClaim`] fragments minted by [`IoPortAllocation::allocate`] transfer the +/// ownership of an acquired PIO range to the caller. +pub(super) tracked struct IoPortAllocation { + auth: GhostSetAuth, +} - #[invariant] - pub fn allocated_matches_claims(&self) -> bool { - self.allocated =~= self.claims - } +/// Fragment claiming ownership of a PIO id range handed out by [`IoPortAllocator::acquire`]. +/// +/// A claim asserts that its ids are allocated by the [`IoPortAllocation`] with the same +/// instance identity, and is consumed when the ids are released by +/// [`IoPortAllocator::recycle`]. +pub(super) tracked struct IoPortClaim { + subset: GhostSubset, +} - init! { - initialize() { - init allocated = Set::empty(); - init claims = Set::empty(); - } - } +impl IoPortAllocation { + /// Instance identity of the protocol. + pub closed spec fn instance_id(self) -> InstanceId { + self.auth.id() + } - transition! { - allocate(ids: Set) { - require pre.allocated.disjoint(ids); - update allocated = pre.allocated.union(ids); - add claims += (ids) by { - assert(pre.claims =~= pre.allocated); - }; - } - } + /// Ids currently allocated. + pub closed spec fn value(self) -> Set { + self.auth@ + } - transition! { - release(ids: Set) { - update allocated = pre.allocated.difference(ids); - remove claims -= (ids); - } - } + /// Creates a fresh protocol instance with an empty allocated set. + pub proof fn initialize() -> (tracked result: Self) { + let tracked (auth, _empty_claims) = GhostSetAuth::new(Set::empty()); + Self { auth } + } - #[inductive(initialize)] - fn initialize_inductive(post: Self) {} + /// Allocates `ids`, requiring them to be currently free, and mints the matching claim + /// fragment. + pub proof fn allocate(tracked &mut self, ids: Set) -> (tracked claim: IoPortClaim) + requires + old(self).value().disjoint(ids), + ensures + final(self).instance_id() == old(self).instance_id(), + final(self).value() == old(self).value().union(ids), + claim.instance_id() == final(self).instance_id(), + claim.set() == ids, + { + let tracked subset = self.auth.insert_set(ids); + IoPortClaim { subset } + } - #[inductive(allocate)] - fn allocate_inductive(pre: Self, post: Self, ids: Set) {} + /// Consumes `claim`, removing its ids from the allocated set. + pub proof fn release(tracked &mut self, tracked claim: IoPortClaim) + requires + claim.instance_id() == old(self).instance_id(), + ensures + final(self).instance_id() == old(self).instance_id(), + final(self).value() == old(self).value().difference(claim.set()), + { + self.auth.delete(claim.subset); + } +} - #[inductive(release)] - fn release_inductive(pre: Self, post: Self, ids: Set) {} +impl IoPortClaim { + /// Instance identity of the protocol that issued this claim. + pub closed spec fn instance_id(self) -> InstanceId { + self.subset.id() + } + + /// Ids claimed by this fragment. + pub closed spec fn set(self) -> Set { + self.subset@ } } } // verus! -pub(super) type IoPortClaim = IoPortAllocationState::claims_set; - -/// Lock-protected executable bitmap and the state-machine token that models it. +/// Lock-protected executable bitmap and the ghost allocation token. #[verus_verify] struct IoPortAllocatorInner { allocator: ModeledIdAlloc, #[cfg(verus_keep_ghost_body)] - tracked_instance: Tracked, - #[cfg(verus_keep_ghost_body)] - tracked_allocated: Tracked, + tracked_allocated: Tracked, } verus! { @@ -205,7 +217,6 @@ impl IoPortAllocatorInner { #[verifier::type_invariant] pub closed spec fn type_inv(self) -> bool { io_port_inner_inv_values( - self.tracked_instance@.id(), self.tracked_allocated@.instance_id(), self.tracked_allocated@.value(), &self.allocator.inner, @@ -312,7 +323,6 @@ impl IoPortAllocator { #[verus_spec(allocation_iter => invariant range.end as usize <= id_alloc_capacity(&allocator_inner.allocator.inner), - allocator_inner.tracked_instance@.id() == io_port_allocator_instance_id(), allocator_inner.tracked_allocated@.instance_id() == io_port_allocator_instance_id(), allocator_inner.tracked_allocated@.value().subset_of(allocation_start_view), @@ -351,14 +361,12 @@ impl IoPortAllocator { } } assert(io_port_inner_inv_values( - allocator_inner.tracked_instance@.id(), allocator_inner.tracked_allocated@.instance_id(), allocator_inner.tracked_allocated@.value(), &allocator_inner.allocator.inner, )); } #[verus_spec(with - Ghost(allocator_inner.tracked_instance@.id()), Ghost(allocator_inner.tracked_allocated@.instance_id()), Ghost(allocator_inner.tracked_allocated@.value()), )] @@ -375,10 +383,7 @@ impl IoPortAllocator { !allocator_inner.tracked_allocated@.value().contains(id) by { } } - range_claim = allocator_inner.tracked_instance.borrow().allocate( - ids, - allocator_inner.tracked_allocated.borrow_mut(), - ); + range_claim = allocator_inner.tracked_allocated.borrow_mut().allocate(ids); } // SAFETY: The created IoPort is guaranteed not to access system device I/O @@ -406,17 +411,11 @@ impl IoPortAllocator { let mut allocator = self.allocator.lock(); let allocator_inner = &mut *allocator; - proof_decl! { - let ghost ids = port_id_set(range.start as usize, range.end as usize); - } proof! { use_type_invariant(&*allocator_inner); assert(range.start as usize <= range.end as usize); - allocator_inner.tracked_instance.borrow().release( - ids, - allocator_inner.tracked_allocated.borrow_mut(), - claim, - ); + assert(claim.instance_id() == allocator_inner.tracked_allocated@.instance_id()); + allocator_inner.tracked_allocated.borrow_mut().release(claim); assert forall|id: usize| #[trigger] allocator_inner.tracked_allocated@.value().contains(id) implies { &&& id_alloc_view(&allocator_inner.allocator.inner).contains(id) @@ -489,19 +488,16 @@ pub(crate) unsafe fn init() { IO_PORT_ALLOCATOR.call_once(|| { proof_decl! { - let tracked (Tracked(instance), Tracked(allocated), Tracked(_empty_claims)) = - IoPortAllocationState::Instance::initialize(); + let tracked allocated = IoPortAllocation::initialize(); } let inner = IoPortAllocatorInner { allocator: ModeledIdAlloc { inner: allocator }, #[cfg(verus_keep_ghost_body)] - tracked_instance: Tracked::new(instance), - #[cfg(verus_keep_ghost_body)] tracked_allocated: Tracked::new(allocated), }; // Original Rust: `IoPortAllocator { allocator: SpinLock::new(allocator) }`. IoPortAllocator { - allocator: SpinLock::new(inner), + allocator: SpinLock::new(inner, Ghost::new(()), Tracked::new(())), } }); } From 0eb7a36a31adb42b31422692cddf704d8e6dcd81 Mon Sep 17 00:00:00 2001 From: Marsman1996 Date: Wed, 2 Sep 2026 16:59:22 +0800 Subject: [PATCH 06/22] prove: derive io_mem window ordering from the boot builder --- ostd/src/arch/x86/io.rs | 3 +- ostd/src/boot/memory_region.rs | 3 +- ostd/src/boot/mod.rs | 8 +- ostd/src/io/io_mem/allocator.rs | 146 ++++++++++++++++++++++++++++--- ostd/src/io/io_port/allocator.rs | 2 +- 5 files changed, 142 insertions(+), 20 deletions(-) diff --git a/ostd/src/arch/x86/io.rs b/ostd/src/arch/x86/io.rs index 35913c17f..36fe128a4 100644 --- a/ostd/src/arch/x86/io.rs +++ b/ostd/src/arch/x86/io.rs @@ -1,7 +1,7 @@ // SPDX-License-Identifier: MPL-2.0 use vstd::prelude::*; -/*use alloc::vec::Vec; +use alloc::vec::Vec; use align_ext::AlignExt; @@ -57,7 +57,6 @@ pub(super) fn construct_io_mem_allocator_builder() -> IoMemAllocatorBuilder { // SAFETY: The range is guaranteed not to access physical memory. unsafe { IoMemAllocatorBuilder::new(ranges) } } -*/ /// Port I/O definition reference: . #[verus_verify] pub const MAX_IO_PORT: u16 = u16::MAX; diff --git a/ostd/src/boot/memory_region.rs b/ostd/src/boot/memory_region.rs index 8b36d1a02..9806d5972 100644 --- a/ostd/src/boot/memory_region.rs +++ b/ostd/src/boot/memory_region.rs @@ -261,14 +261,13 @@ impl Default for MemoryRegionArray { Self::new() } } -/* impl Deref for MemoryRegionArray { type Target = [MemoryRegion]; fn deref(&self) -> &Self::Target { &self.regions[..self.count] } -}*/ +} #[verus_verify] impl MemoryRegionArray { /// Constructs an empty set. diff --git a/ostd/src/boot/mod.rs b/ostd/src/boot/mod.rs index bdcffdb7f..8eb8cc4ce 100644 --- a/ostd/src/boot/mod.rs +++ b/ostd/src/boot/mod.rs @@ -12,10 +12,10 @@ use alloc::{ string::{String, ToString}, vec::Vec, }; - -use memory_region::{MemoryRegion, MemoryRegionArray}; +*/ +use memory_region::{/* MemoryRegion, */ MemoryRegionArray}; use spin::Once; - +/* /// The boot information provided by the bootloader. pub struct BootInfo { /// The name of the bootloader. @@ -38,6 +38,7 @@ pub fn boot_info() -> &'static BootInfo { } static INFO: Once = Once::new(); +*/ /// ACPI information from the bootloader. /// @@ -91,6 +92,7 @@ pub(crate) struct EarlyBootInfo { /// The boot-time information. pub(crate) static EARLY_INFO: Once = Once::new(); +/* /// Initializes the boot information. /// /// This function copies the boot-time accessible information to the heap to diff --git a/ostd/src/io/io_mem/allocator.rs b/ostd/src/io/io_mem/allocator.rs index 4e5cff9c2..2d6a3bc9e 100644 --- a/ostd/src/io/io_mem/allocator.rs +++ b/ostd/src/io/io_mem/allocator.rs @@ -42,10 +42,8 @@ impl IoMemAllocator { pub fn acquire(&self, range: Range) -> Option { let allocator = find_allocator(&self.allocators, &range)?; proof! { - // Trusted boot fact (`io_mem_range_registered`): `range` was registered inside a - // single builder window, and `find_allocator` returns its first overlapping window, - // which is the containing window because the registered windows are disjoint. - assume(allocator@.start <= range.start && range.end <= allocator@.end); + use_type_invariant(self); + lemma_found_window_contains(&self.allocators, &range, allocator); } proof_decl! { let tracked initialized: OneShotSet; @@ -81,7 +79,10 @@ impl IoMemAllocator { /// # Safety /// /// User must ensure the range doesn't belong to physical memory or system device I/O. - #[verus_verify] + #[verus_spec(ret => + requires + windows_ordered(allocators@), + )] unsafe fn new(allocators: Vec) -> Self { Self { allocators } } @@ -103,15 +104,43 @@ impl IoMemAllocatorBuilder { /// # Safety /// /// User must ensure the range doesn't belong to physical memory. - #[verus_verify] + #[verus_spec(ret => + requires + usize_ranges_ordered(ranges@), + ensures + ret.type_inv(), + )] pub(crate) unsafe fn new(ranges: Vec>) -> Self { /* info!( "Creating new I/O memory allocator builder, ranges: {:#x?}", ranges ); */ - let mut allocators = Vec::with_capacity(ranges.len()); + let mut allocators: Vec = Vec::with_capacity(ranges.len()); + #[verus_spec(it => + invariant + allocators@.len() == it.index(), + forall|j: int| 0 <= j < it.index() ==> { + &&& allocators@[j]@.start == it.seq()[j].start + &&& allocators@[j]@.end == it.seq()[j].end + }, + usize_ranges_ordered(it.seq()), + windows_ordered(allocators@), + )] for range in ranges { + proof! { + assert(range == it.seq()[it.index()]); + } allocators.push(RangeAllocator::new(range)); + proof! { + assert(allocators@[allocators@.len() - 1]@.start == range.start); + assert forall|i: int| + 0 <= i < allocators@.len() - 1 + implies allocators@[i]@.end <= range.start by { + assert(allocators@[i]@.end == it.seq()[i].end); + assert(it.seq()[i].end <= it.seq()[i as int + 1].start); + } + assert(windows_ordered(allocators@)); + } } Self { allocators } } @@ -132,8 +161,8 @@ impl IoMemAllocatorBuilder { vstd_extra::assert!(allocator.is_some()); let allocator = allocator.unwrap(); proof! { - // Trusted boot fact, same reasoning as in `acquire`. - assume(allocator@.start <= range.start && range.end <= allocator@.end); + use_type_invariant(self); + lemma_found_window_contains(&self.allocators, &range, allocator); } proof_decl! { let tracked initialized: OneShotSet; @@ -147,12 +176,94 @@ impl IoMemAllocatorBuilder { /// The I/O Memory allocator of the system. verus! { +broadcast use vstd::std_specs::vec::group_vec_axioms; + +/// The registered MMIO windows are pairwise ordered: every window ends at or before the start +/// of the next one, so no window can partially cover a range that is contained in another one. +pub open spec fn windows_ordered(allocators: Seq) -> bool { + forall|i: int, j: int| + 0 <= i < j < allocators.len() ==> allocators[i]@.end <= allocators[j]@.start +} + +/// The format of the windows handed to [`IoMemAllocatorBuilder::new`]. +pub open spec fn usize_ranges_ordered(ranges: Seq>) -> bool { + forall|i: int, j: int| 0 <= i < j < ranges.len() ==> ranges[i].end <= ranges[j].start +} + +impl IoMemAllocatorBuilder { + /// The builder always holds the ordered windows handed to [`IoMemAllocatorBuilder::new`]. + #[verifier::type_invariant] + pub closed spec fn type_inv(self) -> bool { + windows_ordered(self.allocators@) + } +} + +impl IoMemAllocator { + /// The allocator inherits the ordered windows of the builder it was built from. + #[verifier::type_invariant] + pub closed spec fn type_inv(self) -> bool { + windows_ordered(self.allocators@) + } +} + +/// The trusted boot fact [`io_mem_range_registered`], made concrete: the index of the +/// registered window containing `range`. +pub proof fn lemma_registered_window(windows: &Vec, range: Range) -> (idx: + int) + requires + windows_ordered(windows@), + io_mem_range_registered(range), + ensures + 0 <= idx < windows@.len(), + windows@[idx]@.start <= range.start && range.end <= windows@[idx]@.end, +{ + assume(exists|m: int| + 0 <= m < windows@.len() && windows@[m]@.start <= range.start && range.end + <= windows@[m]@.end); + let idx = choose|m: int| + 0 <= m < windows@.len() && windows@[m]@.start <= range.start && range.end + <= windows@[m]@.end; + idx +} + +/// The window overlapping `range` found by [`find_allocator`] is exactly the registered +/// window containing it: ordered windows cannot partially cover a range contained in +/// another window. +pub proof fn lemma_found_window_contains( + windows: &Vec, + range: &Range, + found: &RangeAllocator, +) + requires + windows_ordered(windows@), + io_mem_range_registered(*range), + found@.start < range.end && found@.end > range.start, + exists|k: int| 0 <= k < windows@.len() && windows@[k]@ == found@, + ensures + found@.start <= range.start && range.end <= found@.end, +{ + let container_idx = lemma_registered_window(windows, *range); + let found_idx = choose|k: int| 0 <= k < windows@.len() && windows@[k]@ == found@; + if found_idx < container_idx { + assert(windows@[found_idx]@.end <= windows@[container_idx]@.start); + assert(windows@[container_idx]@.start <= range.start); + assert(false); + } else if found_idx == container_idx { + assert(windows@[found_idx]@.start <= range.start && range.end <= windows@[found_idx]@.end); + } else { + assert(range.end <= windows@[container_idx]@.end); + assert(windows@[container_idx]@.end <= windows@[found_idx]@.start); + assert(false); + } +} + /// Trusted boot-state fact required before allocating or removing a `range`. /// /// Verus cannot mention an exec static in a specification, so this predicate is the explicit -/// specification boundary for the boot-time guarantee that `range` was registered inside a -/// single MMIO window of the builder (and the windows are pairwise disjoint), which is what -/// `RangeAllocator::alloc_specific` requires. +/// specification boundary for the boot-time guarantee that `range` lies within a single window +/// registered by the boot builder. Combined with the ordered-window invariant +/// ([`IoMemAllocator::type_inv`]) it yields exactly what [`RangeAllocator::alloc_specific`] +/// requires; see [`IoMemAllocator::lemma_found_window_contains`]. pub uninterp spec fn io_mem_range_registered(range: Range) -> bool; pub exec static IO_MEM_ALLOCATOR: OnceImpl @@ -171,11 +282,22 @@ pub exec static IO_MEM_ALLOCATOR: OnceImpl /// `remove` function. #[verus_verify] pub(crate) unsafe fn init(io_mem_builder: IoMemAllocatorBuilder) { + proof! { + use_type_invariant(&io_mem_builder); + } // SAFETY: The safety is upheld by the caller. IO_MEM_ALLOCATOR.init(unsafe { IoMemAllocator::new(io_mem_builder.allocators) }); } #[verus_verify] +#[verus_spec(ret => + ensures + ret matches Some(res) ==> { + &&& res@.start < range.end + &&& res@.end > range.start + &&& exists|k: int| 0 <= k < allocators@.len() && allocators@[k]@ == res@ + } +)] fn find_allocator<'a>( allocators: &'a [RangeAllocator], range: &Range, diff --git a/ostd/src/io/io_port/allocator.rs b/ostd/src/io/io_port/allocator.rs index 1917aa128..3883c663d 100644 --- a/ostd/src/io/io_port/allocator.rs +++ b/ostd/src/io/io_port/allocator.rs @@ -203,7 +203,7 @@ impl IoPortClaim { } } // verus! -/// Lock-protected executable bitmap and the ghost allocation token. +/// Lock-protected executable bitmap and the state-machine token that models it. #[verus_verify] struct IoPortAllocatorInner { allocator: ModeledIdAlloc, From bc3bf00da70f2b828abf13ff347601d523393b00 Mon Sep 17 00:00:00 2001 From: Marsman1996 Date: Wed, 2 Sep 2026 19:40:07 +0800 Subject: [PATCH 07/22] refactor: add specifications for bitmap-backed ID allocator and update dependencies --- ostd/src/io/io_port/allocator.rs | 53 +--------------- verified_libs/vstd_extra/Cargo.toml | 1 + .../vstd_extra/src/external/id_alloc.rs | 61 +++++++++++++++++++ verified_libs/vstd_extra/src/external/mod.rs | 2 + 4 files changed, 65 insertions(+), 52 deletions(-) create mode 100644 verified_libs/vstd_extra/src/external/id_alloc.rs diff --git a/ostd/src/io/io_port/allocator.rs b/ostd/src/io/io_port/allocator.rs index 3883c663d..db36c8314 100644 --- a/ostd/src/io/io_port/allocator.rs +++ b/ostd/src/io/io_port/allocator.rs @@ -3,6 +3,7 @@ use vstd::prelude::*; use vstd::resource::set::{GhostSetAuth, GhostSubset}; use vstd::tokens::InstanceId; +use vstd_extra::external::{id_alloc_capacity, id_alloc_view}; use core::ops::Range; @@ -18,11 +19,6 @@ use crate::{ verus! { -/// Verus model for the external bitmap-backed ID allocator. -#[verifier::external_type_specification] -#[verifier::external_body] -pub struct ExIdAlloc(IdAlloc); - /// Opaque specification for the third-party one-time initialization primitive. #[verifier::external_type_specification] #[verifier::external_body] @@ -30,12 +26,6 @@ pub struct ExIdAlloc(IdAlloc); #[verifier::reject_recursive_types(R)] pub struct ExOnce(spin::once::Once); -/// IDs currently allocated by an external `IdAlloc`. -pub uninterp spec fn id_alloc_view(allocator: &IdAlloc) -> Set; - -/// Capacity configured for an external `IdAlloc`. -pub uninterp spec fn id_alloc_capacity(allocator: &IdAlloc) -> usize; - /// Identity assigned to the single global PIO allocator during trusted boot initialization. pub uninterp spec fn io_port_allocator_instance_id() -> InstanceId; @@ -49,47 +39,6 @@ closed spec fn io_port_inner_inv_values( &&& id_alloc_capacity(allocator) == crate::arch::io::MAX_IO_PORT as usize } -pub assume_specification[ IdAlloc::with_capacity ](capacity: usize) -> (allocator: IdAlloc) - ensures - id_alloc_capacity(&allocator) == capacity, - id_alloc_view(&allocator) == Set::::empty(), -; - -pub assume_specification[ IdAlloc::is_allocated ](allocator: &IdAlloc, id: usize) -> (allocated: - bool) - ensures - id < id_alloc_capacity(allocator) ==> allocated == id_alloc_view(allocator).contains(id), -; - -pub assume_specification[ IdAlloc::alloc_specific ](allocator: &mut IdAlloc, id: usize) -> (result: - Option) - requires - id < id_alloc_capacity(old(allocator)), - ensures - id_alloc_capacity(final(allocator)) == id_alloc_capacity(old(allocator)), - id_alloc_view(final(allocator)) == id_alloc_view(old(allocator)).insert(id), - id_alloc_view(old(allocator)).subset_of(id_alloc_view(final(allocator))), - id_alloc_view(old(allocator)).contains(id) ==> { - &&& result is None - }, - !id_alloc_view(old(allocator)).contains(id) ==> { - &&& result == Some(id) - }, - no_unwind -; - -pub assume_specification[ IdAlloc::free_consecutive ](allocator: &mut IdAlloc, range: Range) - requires - range.end <= id_alloc_capacity(old(allocator)), - ensures - id_alloc_capacity(final(allocator)) == id_alloc_capacity(old(allocator)), - forall|id: usize| #[trigger] - id_alloc_view(final(allocator)).contains(id) <==> id_alloc_view( - old(allocator), - ).contains(id) && !(range.start <= id < range.end), - no_unwind -; - } // verus! /// Transparent facade used only to pass ghost frame facts to the third-party mutation. #[repr(transparent)] diff --git a/verified_libs/vstd_extra/Cargo.toml b/verified_libs/vstd_extra/Cargo.toml index 1455796e1..6050c4ff1 100644 --- a/verified_libs/vstd_extra/Cargo.toml +++ b/verified_libs/vstd_extra/Cargo.toml @@ -15,6 +15,7 @@ std = ["vstd/std"] [dependencies] vstd = { workspace = true } +id-alloc = { path = "../../ostd/libs/id-alloc" } [target.'cfg(target_arch = "x86_64")'.dependencies] x86_64 = "0.14.13" diff --git a/verified_libs/vstd_extra/src/external/id_alloc.rs b/verified_libs/vstd_extra/src/external/id_alloc.rs new file mode 100644 index 000000000..8e9904339 --- /dev/null +++ b/verified_libs/vstd_extra/src/external/id_alloc.rs @@ -0,0 +1,61 @@ +//! Specifications for the bitmap-backed ID allocator. +use core::ops::Range; + +use id_alloc::IdAlloc; +use vstd::prelude::*; + +verus! { + +/// Verus model for the external bitmap-backed ID allocator. +#[verifier::external_type_specification] +#[verifier::external_body] +pub struct ExIdAlloc(IdAlloc); + +/// IDs currently allocated by an external `IdAlloc`. +pub uninterp spec fn id_alloc_view(allocator: &IdAlloc) -> Set; + +/// Capacity configured for an external `IdAlloc`. +pub uninterp spec fn id_alloc_capacity(allocator: &IdAlloc) -> usize; + +pub assume_specification[ IdAlloc::with_capacity ](capacity: usize) -> (allocator: IdAlloc) + ensures + id_alloc_capacity(&allocator) == capacity, + id_alloc_view(&allocator) == Set::::empty(), +; + +pub assume_specification[ IdAlloc::is_allocated ](allocator: &IdAlloc, id: usize) -> (allocated: + bool) + ensures + id < id_alloc_capacity(allocator) ==> allocated == id_alloc_view(allocator).contains(id), +; + +pub assume_specification[ IdAlloc::alloc_specific ](allocator: &mut IdAlloc, id: usize) -> (result: + Option) + requires + id < id_alloc_capacity(old(allocator)), + ensures + id_alloc_capacity(final(allocator)) == id_alloc_capacity(old(allocator)), + id_alloc_view(final(allocator)) == id_alloc_view(old(allocator)).insert(id), + id_alloc_view(old(allocator)).subset_of(id_alloc_view(final(allocator))), + id_alloc_view(old(allocator)).contains(id) ==> { + &&& result is None + }, + !id_alloc_view(old(allocator)).contains(id) ==> { + &&& result == Some(id) + }, + no_unwind +; + +pub assume_specification[ IdAlloc::free_consecutive ](allocator: &mut IdAlloc, range: Range) + requires + range.end <= id_alloc_capacity(old(allocator)), + ensures + id_alloc_capacity(final(allocator)) == id_alloc_capacity(old(allocator)), + forall|id: usize| #[trigger] + id_alloc_view(final(allocator)).contains(id) <==> id_alloc_view( + old(allocator), + ).contains(id) && !(range.start <= id < range.end), + no_unwind +; + +} // verus! diff --git a/verified_libs/vstd_extra/src/external/mod.rs b/verified_libs/vstd_extra/src/external/mod.rs index b399bf1e0..137517a9b 100644 --- a/verified_libs/vstd_extra/src/external/mod.rs +++ b/verified_libs/vstd_extra/src/external/mod.rs @@ -5,6 +5,7 @@ pub mod btree; pub mod convert; pub mod deref; +pub mod id_alloc; pub mod ilog2; pub mod int_specs; #[cfg(target_arch = "x86_64")] @@ -17,6 +18,7 @@ pub mod smart_ptr; pub mod time; pub use btree::*; +pub use id_alloc::*; pub use ilog2::*; pub use int_specs::*; #[cfg(target_arch = "x86_64")] From 2dc5398fede31cb6c5b41fc7654fbbeb9eea90a5 Mon Sep 17 00:00:00 2001 From: Marsman1996 Date: Wed, 2 Sep 2026 20:18:10 +0800 Subject: [PATCH 08/22] refine --- Cargo.lock | 1 + ostd/src/arch/x86/device/io_port.rs | 1 + ostd/src/arch/x86/pci.rs | 6 ------ verified_libs/vstd_extra/src/external/int_specs.rs | 9 +++++++++ 4 files changed, 11 insertions(+), 6 deletions(-) diff --git a/Cargo.lock b/Cargo.lock index b2b577219..91f60854b 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -670,6 +670,7 @@ dependencies = [ name = "vstd_extra" version = "0.1.0" dependencies = [ + "id-alloc", "vstd", "x86_64", ] diff --git a/ostd/src/arch/x86/device/io_port.rs b/ostd/src/arch/x86/device/io_port.rs index 99c6fade2..11b10c0a8 100644 --- a/ostd/src/arch/x86/device/io_port.rs +++ b/ostd/src/arch/x86/device/io_port.rs @@ -1,6 +1,7 @@ // SPDX-License-Identifier: MPL-2.0 //! I/O port access. pub use vstd_extra::external::{valid_io_port_access, valid_io_port_number}; + pub use x86_64::{ instructions::port::{ PortReadAccess as IoPortReadAccess, PortWriteAccess as IoPortWriteAccess, ReadOnlyAccess, diff --git a/ostd/src/arch/x86/pci.rs b/ostd/src/arch/x86/pci.rs index 889bbb5ee..ee4cdfcf5 100644 --- a/ostd/src/arch/x86/pci.rs +++ b/ostd/src/arch/x86/pci.rs @@ -7,12 +7,6 @@ use crate::{bus::pci::PciDeviceLocation, io::IoPort, prelude::*}; verus! { -/// x86 is little-endian, so converting a native-endian `u32` to little endian is the identity. -pub assume_specification[ u32::to_le ](value: u32) -> (result: u32) - ensures - result == value, -; - exec static PCI_ADDRESS_PORT: IoPort ensures PCI_ADDRESS_PORT.well_formed(), diff --git a/verified_libs/vstd_extra/src/external/int_specs.rs b/verified_libs/vstd_extra/src/external/int_specs.rs index 1998925a5..a840d2cb5 100644 --- a/verified_libs/vstd_extra/src/external/int_specs.rs +++ b/verified_libs/vstd_extra/src/external/int_specs.rs @@ -27,6 +27,15 @@ pub assume_specification[ u32::is_power_of_two ](self_: u32) -> (r: bool) no_unwind ; +/// On a little-endian target, converting a native-endian `u32` to little endian is the identity. +#[cfg(target_endian = "little")] +pub assume_specification[ u32::to_le ](value: u32) -> (result: u32) + returns + value, + opens_invariants none + no_unwind +; + pub assume_specification[ u64::is_power_of_two ](self_: u64) -> (r: bool) returns is_pow2(self_ as int), From 787495567e23e035ea2b9cf784933542614867d8 Mon Sep 17 00:00:00 2001 From: Marsman1996 Date: Wed, 2 Sep 2026 20:30:38 +0800 Subject: [PATCH 09/22] prove: assume --- ostd/src/io/io_mem/allocator.rs | 59 ++++++++++++++++++++++++--------- 1 file changed, 44 insertions(+), 15 deletions(-) diff --git a/ostd/src/io/io_mem/allocator.rs b/ostd/src/io/io_mem/allocator.rs index 2d6a3bc9e..a83b71e9e 100644 --- a/ostd/src/io/io_mem/allocator.rs +++ b/ostd/src/io/io_mem/allocator.rs @@ -82,6 +82,7 @@ impl IoMemAllocator { #[verus_spec(ret => requires windows_ordered(allocators@), + windows_match_registered(allocators@), )] unsafe fn new(allocators: Vec) -> Self { Self { allocators } @@ -107,6 +108,7 @@ impl IoMemAllocatorBuilder { #[verus_spec(ret => requires usize_ranges_ordered(ranges@), + usize_ranges_match_registered(ranges@), ensures ret.type_inv(), )] @@ -124,6 +126,9 @@ impl IoMemAllocatorBuilder { &&& allocators@[j]@.end == it.seq()[j].end }, usize_ranges_ordered(it.seq()), + usize_ranges_match_registered(it.seq()), + forall|j: int| 0 <= j < it.index() ==> + allocators@[j]@ == registered_io_mem_windows()[j], windows_ordered(allocators@), )] for range in ranges { @@ -133,6 +138,8 @@ impl IoMemAllocatorBuilder { allocators.push(RangeAllocator::new(range)); proof! { assert(allocators@[allocators@.len() - 1]@.start == range.start); + assert(range.start == registered_io_mem_windows()[it.index()].start); + assert(range.end == registered_io_mem_windows()[it.index()].end); assert forall|i: int| 0 <= i < allocators@.len() - 1 implies allocators@[i]@.end <= range.start by { @@ -142,6 +149,10 @@ impl IoMemAllocatorBuilder { assert(windows_ordered(allocators@)); } } + proof! { + assert(allocators@.len() == registered_io_mem_windows().len()); + assert(windows_match_registered(allocators@)); + } Self { allocators } } @@ -190,11 +201,31 @@ pub open spec fn usize_ranges_ordered(ranges: Seq>) -> bool { forall|i: int, j: int| 0 <= i < j < ranges.len() ==> ranges[i].end <= ranges[j].start } +/// The abstract MMIO windows registered by platform boot code. +pub uninterp spec fn registered_io_mem_windows() -> Seq>; + +/// The concrete range allocators represent the abstract boot-time windows exactly. +pub open spec fn windows_match_registered(allocators: Seq) -> bool { + &&& allocators.len() == registered_io_mem_windows().len() + &&& forall|i: int| + 0 <= i < allocators.len() ==> allocators[i]@ == registered_io_mem_windows()[i] +} + +/// The ranges passed across the unsafe builder boundary represent the abstract windows. +pub open spec fn usize_ranges_match_registered(ranges: Seq>) -> bool { + &&& ranges.len() == registered_io_mem_windows().len() + &&& forall|i: int| + 0 <= i < ranges.len() ==> { + &&& ranges[i].start == registered_io_mem_windows()[i].start + &&& ranges[i].end == registered_io_mem_windows()[i].end + } +} + impl IoMemAllocatorBuilder { /// The builder always holds the ordered windows handed to [`IoMemAllocatorBuilder::new`]. #[verifier::type_invariant] pub closed spec fn type_inv(self) -> bool { - windows_ordered(self.allocators@) + windows_ordered(self.allocators@) && windows_match_registered(self.allocators@) } } @@ -202,7 +233,7 @@ impl IoMemAllocator { /// The allocator inherits the ordered windows of the builder it was built from. #[verifier::type_invariant] pub closed spec fn type_inv(self) -> bool { - windows_ordered(self.allocators@) + windows_ordered(self.allocators@) && windows_match_registered(self.allocators@) } } @@ -212,17 +243,16 @@ pub proof fn lemma_registered_window(windows: &Vec, range: Range int) requires windows_ordered(windows@), + windows_match_registered(windows@), io_mem_range_registered(range), ensures 0 <= idx < windows@.len(), windows@[idx]@.start <= range.start && range.end <= windows@[idx]@.end, { - assume(exists|m: int| - 0 <= m < windows@.len() && windows@[m]@.start <= range.start && range.end - <= windows@[m]@.end); let idx = choose|m: int| - 0 <= m < windows@.len() && windows@[m]@.start <= range.start && range.end - <= windows@[m]@.end; + 0 <= m < registered_io_mem_windows().len() && registered_io_mem_windows()[m].start + <= range.start && range.end <= registered_io_mem_windows()[m].end; + assert(windows@[idx]@ == registered_io_mem_windows()[idx]); idx } @@ -236,6 +266,7 @@ pub proof fn lemma_found_window_contains( ) requires windows_ordered(windows@), + windows_match_registered(windows@), io_mem_range_registered(*range), found@.start < range.end && found@.end > range.start, exists|k: int| 0 <= k < windows@.len() && windows@[k]@ == found@, @@ -257,14 +288,12 @@ pub proof fn lemma_found_window_contains( } } -/// Trusted boot-state fact required before allocating or removing a `range`. -/// -/// Verus cannot mention an exec static in a specification, so this predicate is the explicit -/// specification boundary for the boot-time guarantee that `range` lies within a single window -/// registered by the boot builder. Combined with the ordered-window invariant -/// ([`IoMemAllocator::type_inv`]) it yields exactly what [`RangeAllocator::alloc_specific`] -/// requires; see [`IoMemAllocator::lemma_found_window_contains`]. -pub uninterp spec fn io_mem_range_registered(range: Range) -> bool; +/// A range is registered when one abstract boot-time MMIO window contains it. +pub open spec fn io_mem_range_registered(range: Range) -> bool { + exists|m: int| + 0 <= m < registered_io_mem_windows().len() && registered_io_mem_windows()[m].start + <= range.start && range.end <= registered_io_mem_windows()[m].end +} pub exec static IO_MEM_ALLOCATOR: OnceImpl ensures From d3b93b18abc6729086329100c2cb32c8d7a0de80 Mon Sep 17 00:00:00 2001 From: Marsman1996 Date: Wed, 2 Sep 2026 21:36:37 +0800 Subject: [PATCH 10/22] refine --- ostd/src/io/io_mem/allocator.rs | 24 +++++++++++++++++------- ostd/src/io/io_port/allocator.rs | 4 ++-- ostd/src/io/io_port/mod.rs | 2 +- 3 files changed, 20 insertions(+), 10 deletions(-) diff --git a/ostd/src/io/io_mem/allocator.rs b/ostd/src/io/io_mem/allocator.rs index a83b71e9e..f0c58bbff 100644 --- a/ostd/src/io/io_mem/allocator.rs +++ b/ostd/src/io/io_mem/allocator.rs @@ -121,13 +121,13 @@ impl IoMemAllocatorBuilder { #[verus_spec(it => invariant allocators@.len() == it.index(), - forall|j: int| 0 <= j < it.index() ==> { + forall|j: int| #![trigger it.seq()[j]] 0 <= j < it.index() ==> { &&& allocators@[j]@.start == it.seq()[j].start &&& allocators@[j]@.end == it.seq()[j].end }, usize_ranges_ordered(it.seq()), usize_ranges_match_registered(it.seq()), - forall|j: int| 0 <= j < it.index() ==> + forall|j: int| #![trigger registered_io_mem_windows()[j]] 0 <= j < it.index() ==> allocators@[j]@ == registered_io_mem_windows()[j], windows_ordered(allocators@), )] @@ -140,7 +140,7 @@ impl IoMemAllocatorBuilder { assert(allocators@[allocators@.len() - 1]@.start == range.start); assert(range.start == registered_io_mem_windows()[it.index()].start); assert(range.end == registered_io_mem_windows()[it.index()].end); - assert forall|i: int| + assert forall|i: int| #![trigger allocators@[i]] 0 <= i < allocators@.len() - 1 implies allocators@[i]@.end <= range.start by { assert(allocators@[i]@.end == it.seq()[i].end); @@ -193,12 +193,15 @@ broadcast use vstd::std_specs::vec::group_vec_axioms; /// of the next one, so no window can partially cover a range that is contained in another one. pub open spec fn windows_ordered(allocators: Seq) -> bool { forall|i: int, j: int| + #![trigger allocators[i], allocators[j]] 0 <= i < j < allocators.len() ==> allocators[i]@.end <= allocators[j]@.start } /// The format of the windows handed to [`IoMemAllocatorBuilder::new`]. pub open spec fn usize_ranges_ordered(ranges: Seq>) -> bool { - forall|i: int, j: int| 0 <= i < j < ranges.len() ==> ranges[i].end <= ranges[j].start + forall|i: int, j: int| + #![trigger ranges[i], ranges[j]] + 0 <= i < j < ranges.len() ==> ranges[i].end <= ranges[j].start } /// The abstract MMIO windows registered by platform boot code. @@ -208,6 +211,7 @@ pub uninterp spec fn registered_io_mem_windows() -> Seq>; pub open spec fn windows_match_registered(allocators: Seq) -> bool { &&& allocators.len() == registered_io_mem_windows().len() &&& forall|i: int| + #![trigger registered_io_mem_windows()[i]] 0 <= i < allocators.len() ==> allocators[i]@ == registered_io_mem_windows()[i] } @@ -215,6 +219,7 @@ pub open spec fn windows_match_registered(allocators: Seq) -> bo pub open spec fn usize_ranges_match_registered(ranges: Seq>) -> bool { &&& ranges.len() == registered_io_mem_windows().len() &&& forall|i: int| + #![trigger ranges[i]] 0 <= i < ranges.len() ==> { &&& ranges[i].start == registered_io_mem_windows()[i].start &&& ranges[i].end == registered_io_mem_windows()[i].end @@ -250,6 +255,7 @@ pub proof fn lemma_registered_window(windows: &Vec, range: Range windows@[idx]@.start <= range.start && range.end <= windows@[idx]@.end, { let idx = choose|m: int| + #![trigger registered_io_mem_windows()[m]] 0 <= m < registered_io_mem_windows().len() && registered_io_mem_windows()[m].start <= range.start && range.end <= registered_io_mem_windows()[m].end; assert(windows@[idx]@ == registered_io_mem_windows()[idx]); @@ -269,12 +275,14 @@ pub proof fn lemma_found_window_contains( windows_match_registered(windows@), io_mem_range_registered(*range), found@.start < range.end && found@.end > range.start, - exists|k: int| 0 <= k < windows@.len() && windows@[k]@ == found@, + exists|k: int| #![trigger windows@[k]] 0 <= k < windows@.len() && windows@[k]@ == found@, ensures found@.start <= range.start && range.end <= found@.end, { let container_idx = lemma_registered_window(windows, *range); - let found_idx = choose|k: int| 0 <= k < windows@.len() && windows@[k]@ == found@; + let found_idx = choose|k: int| + #![trigger windows@[k]] + 0 <= k < windows@.len() && windows@[k]@ == found@; if found_idx < container_idx { assert(windows@[found_idx]@.end <= windows@[container_idx]@.start); assert(windows@[container_idx]@.start <= range.start); @@ -291,6 +299,7 @@ pub proof fn lemma_found_window_contains( /// A range is registered when one abstract boot-time MMIO window contains it. pub open spec fn io_mem_range_registered(range: Range) -> bool { exists|m: int| + #![trigger registered_io_mem_windows()[m]] 0 <= m < registered_io_mem_windows().len() && registered_io_mem_windows()[m].start <= range.start && range.end <= registered_io_mem_windows()[m].end } @@ -324,7 +333,8 @@ pub(crate) unsafe fn init(io_mem_builder: IoMemAllocatorBuilder) { ret matches Some(res) ==> { &&& res@.start < range.end &&& res@.end > range.start - &&& exists|k: int| 0 <= k < allocators@.len() && allocators@[k]@ == res@ + &&& exists|k: int| #![trigger allocators@[k]] + 0 <= k < allocators@.len() && allocators@[k]@ == res@ } )] fn find_allocator<'a>( diff --git a/ostd/src/io/io_port/allocator.rs b/ostd/src/io/io_port/allocator.rs index db36c8314..36903e181 100644 --- a/ostd/src/io/io_port/allocator.rs +++ b/ostd/src/io/io_port/allocator.rs @@ -280,7 +280,7 @@ impl IoPortAllocator { ), id_alloc_capacity(&allocator_inner.allocator.inner) == crate::arch::io::MAX_IO_PORT as usize, - id_alloc_view(&allocator_inner.allocator.inner) =~= + id_alloc_view(&allocator_inner.allocator.inner) == allocation_start_view.union( port_id_set( range.start as usize, @@ -322,7 +322,7 @@ impl IoPortAllocator { let _ = allocator_inner.allocator.alloc_specific(i as usize); proof! { lemma_port_id_set_insert(range.start as usize, i as usize); - assert(id_alloc_view(&allocator_inner.allocator.inner) =~= + assert(id_alloc_view(&allocator_inner.allocator.inner) == old_view.insert(i as usize)); } } diff --git a/ostd/src/io/io_port/mod.rs b/ostd/src/io/io_port/mod.rs index c541cb1b5..46d5cbedc 100644 --- a/ostd/src/io/io_port/mod.rs +++ b/ostd/src/io/io_port/mod.rs @@ -50,7 +50,7 @@ impl IoPort { /// Whether `claim` is the allocator-issued ownership token for this complete typed range. pub open spec fn claim_matches_set(&self, claim: Set) -> bool { - claim =~= port_id_set(self@ as usize, (self@ as usize + size_of::()) as usize) + claim == port_id_set(self@ as usize, (self@ as usize + size_of::()) as usize) } } From 3cd89551983f9599139590956c0d3a8fe7e79eaf Mon Sep 17 00:00:00 2001 From: Marsman1996 Date: Wed, 2 Sep 2026 21:57:02 +0800 Subject: [PATCH 11/22] chore: add comments for modified exec code --- ostd/src/arch/x86/pci.rs | 2 ++ ostd/src/io/io_mem/allocator.rs | 31 ++++++++++++++++++++++++++----- ostd/src/io/io_mem/mod.rs | 12 ++++++++---- ostd/src/io/io_port/allocator.rs | 17 ++++++++++++++--- ostd/src/io/io_port/mod.rs | 1 + 5 files changed, 51 insertions(+), 12 deletions(-) diff --git a/ostd/src/arch/x86/pci.rs b/ostd/src/arch/x86/pci.rs index ee4cdfcf5..c1c142c04 100644 --- a/ostd/src/arch/x86/pci.rs +++ b/ostd/src/arch/x86/pci.rs @@ -7,6 +7,7 @@ use crate::{bus::pci::PciDeviceLocation, io::IoPort, prelude::*}; verus! { +// Original Rust: static PCI_ADDRESS_PORT: IoPort = unsafe { IoPort::new(0x0CF8) }; exec static PCI_ADDRESS_PORT: IoPort ensures PCI_ADDRESS_PORT.well_formed(), @@ -14,6 +15,7 @@ exec static PCI_ADDRESS_PORT: IoPort unsafe { IoPort::new(0x0CF8) } } +// Original Rust: static PCI_DATA_PORT: IoPort = unsafe { IoPort::new(0x0CFC) }; exec static PCI_DATA_PORT: IoPort ensures PCI_DATA_PORT.well_formed(), diff --git a/ostd/src/io/io_mem/allocator.rs b/ostd/src/io/io_mem/allocator.rs index f0c58bbff..ba4ef4850 100644 --- a/ostd/src/io/io_mem/allocator.rs +++ b/ostd/src/io/io_mem/allocator.rs @@ -40,6 +40,11 @@ impl IoMemAllocator { == vstd_extra::external::range::range_usize_len_spec(&range), )] pub fn acquire(&self, range: Range) -> Option { + /* Original Rust: + find_allocator(&self.allocators, &range)? + .alloc_specific(&range) + .ok()?; + */ let allocator = find_allocator(&self.allocators, &range)?; proof! { use_type_invariant(self); @@ -55,7 +60,7 @@ impl IoMemAllocator { /* debug!("Acquiring MMIO range:{:x?}..{:x?}", range.start, range.end); */ // SAFETY: The created `IoMem` is guaranteed not to access physical memory or system device I/O. - // Original Rust used the upstream bitflags-style associated constant `PageFlags::RW`. + /* Original Rust: PageFlags::RW */ unsafe { Some(IoMem::new(range, PageFlags::RW(), CachePolicy::Uncacheable)) } } @@ -166,8 +171,22 @@ impl IoMemAllocatorBuilder { io_mem_range_registered(range), )] pub(crate) fn remove(&self, range: Range) { - // Formatting machinery used by the original panic is not modeled by Verus. - // Original Rust used two formatted `panic!` branches here. + /* Formatting machinery used by the original panic is not modeled by Verus. + Original Rust: + let Some(allocator) = find_allocator(&self.allocators, &range) else { + panic!( + "Allocator for the system device's MMIO was not found. Range: {:x?}", + range + ); + }; + + if let Err(err) = allocator.alloc_specific(&range) { + panic!( + "An error occurred while trying to remove access to the system device's MMIO. Range: {:x?}. Error: {:?}", + range, err + ); + } + */ let allocator = find_allocator(&self.allocators, &range); vstd_extra::assert!(allocator.is_some()); let allocator = allocator.unwrap(); @@ -185,6 +204,7 @@ impl IoMemAllocatorBuilder { } /// The I/O Memory allocator of the system. +// Original Rust: pub static IO_MEM_ALLOCATOR: Once = Once::new(); verus! { broadcast use vstd::std_specs::vec::group_vec_axioms; @@ -324,6 +344,7 @@ pub(crate) unsafe fn init(io_mem_builder: IoMemAllocatorBuilder) { use_type_invariant(&io_mem_builder); } // SAFETY: The safety is upheld by the caller. + // Original Rust: IO_MEM_ALLOCATOR.call_once(|| unsafe { IoMemAllocator::new(io_mem_builder.allocators) }); IO_MEM_ALLOCATOR.init(unsafe { IoMemAllocator::new(io_mem_builder.allocators) }); } @@ -343,8 +364,8 @@ fn find_allocator<'a>( ) -> Option<&'a RangeAllocator> { for allocator in allocators.iter() { let allocator_range = allocator.fullrange(); - // Verus does not yet support `continue` in `for` loops. Original Rust: - /* + /* Verus does not yet support `continue` in `for` loops. + Original Rust: if allocator_range.start >= range.end || allocator_range.end <= range.start { continue; } diff --git a/ostd/src/io/io_mem/mod.rs b/ostd/src/io/io_mem/mod.rs index 8c7d91153..a0d6cd1e8 100644 --- a/ostd/src/io/io_mem/mod.rs +++ b/ostd/src/io/io_mem/mod.rs @@ -83,6 +83,7 @@ impl IoMem { pub fn acquire(range: Range) -> Result { allocator::IO_MEM_ALLOCATOR .get() + /* .unwrap() */ .ok_or(Error::AccessDenied)? .acquire(range) .ok_or(Error::AccessDenied) @@ -224,9 +225,9 @@ impl IoMem { // SAFETY: The constructor of the `IoMem` structure has already ensured the // safety of reading from the mapped physical address, and the mapping is valid. unsafe { - // `from_kernel_space` in ostd/src/mm/io.rs is changed - // (self.kvirt_area.deref().start() + self.offset) as *mut u8 VmReader::from_kernel_space( + /* Original Rust: + (self.kvirt_area.deref().start() + self.offset) as *mut u8, */ VirtPtr::from_vaddr(self.kvirt_area.deref().start() + self.offset, self.limit), self.limit, ) @@ -237,9 +238,9 @@ impl IoMem { // SAFETY: The constructor of the `IoMem` structure has already ensured the // safety of writing to the mapped physical address, and the mapping is valid. unsafe { - // Original Rust passed the raw pointer - // `(self.kvirt_area.deref().start() + self.offset) as *mut u8`. VmWriter::from_kernel_space( + /* Original Rust: + (self.kvirt_area.deref().start() + self.offset) as *mut u8, */ VirtPtr::from_vaddr(self.kvirt_area.deref().start() + self.offset, self.limit), self.limit, ) @@ -249,6 +250,7 @@ impl IoMem { verus! { +/* Original Rust: impl VmIo for IoMem { */ impl VmIo<()> for IoMem { closed spec fn obeys_vmio_spec() -> bool { false @@ -293,6 +295,7 @@ impl VmIo<()> for IoMem { /// Device reads are a trusted hardware boundary; the range checks and cursor updates remain /// identical to the original implementation. #[verifier::external_body] + /* Original Rust: fn read(&self, offset: usize, writer: &mut VmWriter) -> Result<()> { */ fn read( &self, offset: usize, @@ -312,6 +315,7 @@ impl VmIo<()> for IoMem { /// Device writes are a trusted hardware boundary for the same reason as [`Self::read`]. #[verifier::external_body] + /* Original Rust: fn write(&self, offset: usize, reader: &mut VmReader) -> Result<()> { */ fn write( &self, offset: usize, diff --git a/ostd/src/io/io_port/allocator.rs b/ostd/src/io/io_port/allocator.rs index 36903e181..c2ef4f11d 100644 --- a/ostd/src/io/io_port/allocator.rs +++ b/ostd/src/io/io_port/allocator.rs @@ -181,7 +181,7 @@ pub struct IoPortAllocator { /// /// Instead of using `RangeAllocator` like `IoMemAllocator` does, it is more reasonable to use `IdAlloc`, /// as PIO space includes only a small region; for example, x86 module in OSTD allows just 65536 I/O ports. - allocator: SpinLock, + allocator: SpinLock, } #[verus_verify] @@ -209,7 +209,8 @@ impl IoPortAllocator { use_type_invariant(&*allocator_inner); } let mut range = port..(port + size_of::() as u16); - // `Iterator::any` with a capturing closure is not supported by Verus. Original Rust: + // `Iterator::any` with a capturing closure is not supported by Verus. + // Original Rust: // if range.any(|i| allocator.is_allocated(i as usize)) { return None; } let mut already_allocated = false; #[verus_spec(scan_iter => @@ -319,6 +320,7 @@ impl IoPortAllocator { Ghost(allocator_inner.tracked_allocated@.instance_id()), Ghost(allocator_inner.tracked_allocated@.value()), )] + /* Original Rust: allocator.alloc_specific(i as usize); */ let _ = allocator_inner.allocator.alloc_specific(i as usize); proof! { lemma_port_id_set_insert(range.start as usize, i as usize); @@ -336,6 +338,7 @@ impl IoPortAllocator { } // SAFETY: The created IoPort is guaranteed not to access system device I/O + /* Original Rust: unsafe { Some(IoPort::new(port)) } */ let result = unsafe { Some(IoPort::new(port)) }; allocator.drop(); proof_with!(|= Tracked(Some(range_claim))); @@ -357,6 +360,11 @@ impl IoPortAllocator { )] pub(in crate::io) unsafe fn recycle(&self, range: Range) { /* debug!("Recycling MMIO range: {:#x?}", range); */ + /* Original Rust: + self.allocator + .lock() + .free_consecutive(range.start as usize..range.end as usize); + */ let mut allocator = self.allocator.lock(); let allocator_inner = &mut *allocator; @@ -435,6 +443,10 @@ pub(crate) unsafe fn init() { } } + /* Original Rust: + IO_PORT_ALLOCATOR.call_once(|| IoPortAllocator { + allocator: SpinLock::new(allocator), + }); */ IO_PORT_ALLOCATOR.call_once(|| { proof_decl! { let tracked allocated = IoPortAllocation::initialize(); @@ -444,7 +456,6 @@ pub(crate) unsafe fn init() { #[cfg(verus_keep_ghost_body)] tracked_allocated: Tracked::new(allocated), }; - // Original Rust: `IoPortAllocator { allocator: SpinLock::new(allocator) }`. IoPortAllocator { allocator: SpinLock::new(inner, Ghost::new(()), Tracked::new(())), } diff --git a/ostd/src/io/io_port/mod.rs b/ostd/src/io/io_port/mod.rs index 46d5cbedc..b89797e1b 100644 --- a/ostd/src/io/io_port/mod.rs +++ b/ostd/src/io/io_port/mod.rs @@ -126,6 +126,7 @@ impl IoPort { let tracked claim: Option; } #[verus_spec(with => Tracked(claim))] + /* Original Rust: allocator::IO_PORT_ALLOCATOR.get().unwrap() */ let port = initialized_allocator().acquire(port); let result = port.ok_or(Error::AccessDenied); proof_with!(|= Tracked(claim)); From 87875fed29a0d610bf8d1192dfda83ea5e7467d6 Mon Sep 17 00:00:00 2001 From: Marsman1996 Date: Thu, 3 Sep 2026 09:47:43 +0800 Subject: [PATCH 12/22] fmt --- ostd/src/arch/x86/mod.rs | 1 - 1 file changed, 1 deletion(-) diff --git a/ostd/src/arch/x86/mod.rs b/ostd/src/arch/x86/mod.rs index 302df01ae..db3d91a44 100644 --- a/ostd/src/arch/x86/mod.rs +++ b/ostd/src/arch/x86/mod.rs @@ -3,7 +3,6 @@ /*pub mod boot; pub(crate) mod cpu;*/ pub mod device; - /*pub(crate) mod ex_table;*/ pub(crate) mod io; /*pub(crate) mod iommu;*/ From b1201628c5a5862b0d4b2f6b8889f0d3eb0f81e6 Mon Sep 17 00:00:00 2001 From: Marsman1996 Date: Sat, 12 Sep 2026 10:50:41 +0800 Subject: [PATCH 13/22] prove: drop id-alloc assume_specifications, wire io_port to the proven IdAlloc --- ostd/src/io/io_mem/allocator.rs | 3 +- ostd/src/io/io_mem/mod.rs | 7 +- ostd/src/io/io_port/allocator.rs | 259 +++++++++++++++++- verified_libs/vstd_extra/Cargo.toml | 1 - .../vstd_extra/src/external/id_alloc.rs | 61 ----- verified_libs/vstd_extra/src/external/mod.rs | 6 +- 6 files changed, 257 insertions(+), 80 deletions(-) delete mode 100644 verified_libs/vstd_extra/src/external/id_alloc.rs diff --git a/ostd/src/io/io_mem/allocator.rs b/ostd/src/io/io_mem/allocator.rs index ba4ef4850..f74301f12 100644 --- a/ostd/src/io/io_mem/allocator.rs +++ b/ostd/src/io/io_mem/allocator.rs @@ -36,8 +36,7 @@ impl IoMemAllocator { io_mem_range_registered(range), ensures result is Some ==> result->Some_0.paddr_spec() == range.start, - result is Some ==> result->Some_0.length_spec() - == vstd_extra::external::range::range_usize_len_spec(&range), + result is Some ==> result->Some_0.length_spec() == range.end - range.start, )] pub fn acquire(&self, range: Range) -> Option { /* Original Rust: diff --git a/ostd/src/io/io_mem/mod.rs b/ostd/src/io/io_mem/mod.rs index a0d6cd1e8..8bd0e1da1 100644 --- a/ostd/src/io/io_mem/mod.rs +++ b/ostd/src/io/io_mem/mod.rs @@ -78,7 +78,7 @@ impl IoMem { ensures result is Ok ==> result->Ok_0.paddr_spec() == range.start, result is Ok ==> result->Ok_0.length_spec() - == vstd_extra::external::range::range_usize_len_spec(&range), + == range.end - range.start, )] pub fn acquire(range: Range) -> Result { allocator::IO_MEM_ALLOCATOR @@ -131,8 +131,7 @@ impl IoMem { Self { kvirt_area: self.kvirt_area.clone(), offset: self.offset + range.start, - /* limit: range.len(), */ - limit: vstd_extra::external::range::range_usize_len(&range), + limit: range.len(), pa: self.pa + range.start, } } @@ -153,7 +152,7 @@ impl IoMem { ensures result.paddr_spec() == range.start, result.length_spec() - == vstd_extra::external::range::range_usize_len_spec(&range), + == range.end - range.start, )] pub(crate) unsafe fn new(range: Range, flags: PageFlags, cache: CachePolicy) -> Self { let first_page_start = range.start.align_down(PAGE_SIZE); diff --git a/ostd/src/io/io_port/allocator.rs b/ostd/src/io/io_port/allocator.rs index c2ef4f11d..b818ebbb5 100644 --- a/ostd/src/io/io_port/allocator.rs +++ b/ostd/src/io/io_port/allocator.rs @@ -3,7 +3,7 @@ use vstd::prelude::*; use vstd::resource::set::{GhostSetAuth, GhostSubset}; use vstd::tokens::InstanceId; -use vstd_extra::external::{id_alloc_capacity, id_alloc_view}; +use vstd_extra::ownership::Inv; use core::ops::Range; @@ -29,12 +29,162 @@ pub struct ExOnce(spin::once::Once); /// Identity assigned to the single global PIO allocator during trusted boot initialization. pub uninterp spec fn io_port_allocator_instance_id() -> InstanceId; -closed spec fn io_port_inner_inv_values( +/// Allocated ids of a bitmap prefix `[0, end)`: `i` is in iff `s[i]`. +pub(crate) closed spec fn id_alloc_bits(s: Seq, end: int) -> Set + decreases end, +{ + if end <= 0 { + Set::empty() + } else { + let rest = id_alloc_bits(s, end - 1); + if s[end - 1] { + rest.insert((end - 1) as usize) + } else { + rest + } + } +} + +/// Set of ids currently allocated by `allocator`. +pub(crate) open spec fn id_alloc_view(allocator: &IdAlloc) -> Set { + id_alloc_bits(allocator@, allocator@.len() as int) +} + +/// Number of ids `allocator` can hold. +pub(crate) open spec fn id_alloc_capacity(allocator: &IdAlloc) -> usize { + allocator@.len() as usize +} + +/// Characterizes `id_alloc_bits`: `id_alloc_bits(s, end).contains(j)` holds exactly when +/// `0 <= j < end` and `s[j]` is `true`. +pub(crate) proof fn lemma_id_alloc_bits_char(s: Seq, end: int, j: usize) + requires + 0 <= end, + end <= usize::MAX as int, + s.len() >= end, + 0 <= (j as int), + ensures + id_alloc_bits(s, end).contains(j) == ((j as int) < end && s[j as int]), + decreases end, +{ + reveal(id_alloc_bits); + if end <= 0 { + assert(id_alloc_bits(s, end) =~= Set::empty()); + } else { + lemma_id_alloc_bits_char(s, end - 1, j); + if (j as int) == end - 1 { + assert(id_alloc_bits(s, end - 1).contains(j) == (((j as int) < end - 1) + && s[j as int])); + assert(id_alloc_bits(s, end).contains(j) == s[end - 1]); + assert(s[j as int] == s[end - 1]); + } else { + // j != end-1: the bit folded in at (end-1) is distinct from j. + assert(id_alloc_bits(s, end - 1).contains(j) == (((j as int) < end - 1) + && s[j as int])); + assert(((end - 1) as usize) as int == end - 1); + assert(j != (end - 1) as usize); + if s[end - 1] { + assert(id_alloc_bits(s, end - 1).insert((end - 1) as usize).contains(j) + == id_alloc_bits(s, end - 1).contains(j)); + } + assert(id_alloc_bits(s, end).contains(j) == id_alloc_bits(s, end - 1).contains(j)); + assert(((j as int) < end - 1 && s[j as int]) == ((j as int) < end && s[j as int])); + } + } +} + +/// For an in-bounds id, `id_alloc_view` membership coincides with the allocated bitmap bit. +pub(crate) proof fn lemma_id_alloc_view_contains(allocator: &IdAlloc, id: usize) + requires + allocator.inv(), + (id as int) < allocator@.len(), + allocator@.len() <= usize::MAX as int, + ensures + id_alloc_view(allocator).contains(id) == allocator@[id as int], +{ + lemma_id_alloc_bits_char(allocator@, allocator@.len() as int, id); +} + +/// Derives the set-level postcondition of `alloc_specific` from its bitmap postcondition. +pub(crate) proof fn lemma_alloc_specific_view( + old_a: &IdAlloc, + final_a: &IdAlloc, + id: usize, + res: Option, +) + requires + old_a.inv(), + final_a.inv(), + (id as int) < old_a@.len(), + old_a@.len() <= usize::MAX as int, + final_a@.len() == old_a@.len(), + res is None ==> old_a@[id as int] && final_a@ == old_a@, + res is Some ==> final_a@ == old_a@.update(id as int, true) && !old_a@[id as int], + res is Some ==> res == Some(id), + ensures + id_alloc_view(final_a) == id_alloc_view(old_a).insert(id), + id_alloc_view(old_a).subset_of(id_alloc_view(final_a)), + id_alloc_view(old_a).contains(id) ==> res is None, + !id_alloc_view(old_a).contains(id) ==> res == Some(id), +{ + let old_len: int = old_a@.len() as int; + assert forall|j: usize| + id_alloc_view(final_a).contains(j) == (id_alloc_view(old_a).insert(id)).contains(j) by { + lemma_id_alloc_bits_char(old_a@, old_len, j); + lemma_id_alloc_bits_char(final_a@, final_a@.len() as int, j); + if res is Some { + assert forall|jj: int| + #![trigger final_a@[jj]] + final_a@[jj] == (if jj == id as int { + true + } else { + old_a@[jj] + }) by { + assert(final_a@ == old_a@.update(id as int, true)); + } + } else { + assert(final_a@ == old_a@); + assert(old_a@[id as int]); + } + } + assert forall|j: usize| + #![trigger id_alloc_view(old_a).contains(j)] + id_alloc_view(old_a).contains(j) implies id_alloc_view(final_a).contains(j) by { + lemma_id_alloc_bits_char(old_a@, old_len, j); + lemma_id_alloc_bits_char(final_a@, final_a@.len() as int, j); + if res is Some { + assert forall|jj: int| + #![trigger final_a@[jj]] + final_a@[jj] == (if jj == id as int { + true + } else { + old_a@[jj] + }) by { + assert(final_a@ == old_a@.update(id as int, true)); + } + } else { + assert(final_a@ == old_a@); + } + } + lemma_id_alloc_bits_char(old_a@, old_len, id); + assert(id_alloc_view(old_a).contains(id) == old_a@[id as int]); + if res is Some { + assert(!old_a@[id as int]); + assert(res == Some(id)); + } else { + assert(old_a@[id as int]); + } +} + +/// Representation invariant of `IoPortAllocatorInner`. +pub(crate) open spec fn io_port_inner_inv_values( allocated_instance_id: InstanceId, allocated: Set, allocator: &IdAlloc, ) -> bool { &&& allocated_instance_id == io_port_allocator_instance_id() + &&& allocator.inv() + &&& allocator@.len() == crate::arch::io::MAX_IO_PORT as int &&& allocated.subset_of(id_alloc_view(allocator)) &&& id_alloc_capacity(allocator) == crate::arch::io::MAX_IO_PORT as usize } @@ -57,6 +207,8 @@ impl ModeledIdAlloc { id < id_alloc_capacity(&old(self).inner), io_port_inner_inv_values(allocated_instance_id, preserved, &old(self).inner), ensures + final(self).inner.inv(), + final(self).inner@.len() == crate::arch::io::MAX_IO_PORT as int, id_alloc_capacity(&final(self).inner) == id_alloc_capacity(&old(self).inner), id_alloc_view(&final(self).inner) == id_alloc_view(&old(self).inner).insert(id), id_alloc_view(&old(self).inner).subset_of(id_alloc_view(&final(self).inner)), @@ -68,10 +220,27 @@ impl ModeledIdAlloc { ), id_alloc_view(&old(self).inner).contains(id) ==> result is None, !id_alloc_view(&old(self).inner).contains(id) ==> result == Some(id), - no_unwind )] fn alloc_specific(&mut self, id: usize) -> Option { - self.inner.alloc_specific(id) + proof! { + assert(id < id_alloc_capacity(&old(self).inner)); + assert(id_alloc_capacity(&old(self).inner) + == crate::arch::io::MAX_IO_PORT as usize); + assert(old(self).inner@.len() == crate::arch::io::MAX_IO_PORT as int); + assert((id as int) < old(self).inner@.len()); + } + let res = self.inner.alloc_specific(id); + proof! { + assert(self.inner@.len() == old(self).inner@.len()); + assert(self.inner@.len() == crate::arch::io::MAX_IO_PORT as int); + assert(self.inner.inv()); + assert(old(self).inner@.len() <= usize::MAX as int); + lemma_alloc_specific_view(&old(self).inner, &self.inner, id, res); + assert(id_alloc_capacity(&self.inner) == id_alloc_capacity(&old(self).inner)); + assert(preserved.subset_of(id_alloc_view(&self.inner))); + assert(io_port_inner_inv_values(allocated_instance_id, preserved, &self.inner)); + } + res } } @@ -137,6 +306,16 @@ impl IoPortAllocation { { self.auth.delete(claim.subset); } + + /// Certifies `claim.set() <= self.value()` (the claim's ids are currently allocated). + pub proof fn claim_includes(tracked &self, tracked claim: &IoPortClaim) + requires + claim.instance_id() == self.instance_id(), + ensures + claim.set() <= self.value(), + { + claim.subset.agree(&self.auth); + } } impl IoPortClaim { @@ -163,7 +342,6 @@ struct IoPortAllocatorInner { verus! { impl IoPortAllocatorInner { - #[verifier::type_invariant] pub closed spec fn type_inv(self) -> bool { io_port_inner_inv_values( self.tracked_allocated@.instance_id(), @@ -194,6 +372,7 @@ impl IoPortAllocator { vstd::layout::size_of::() <= u16::MAX, size_of::() <= u16::MAX, port as usize + size_of::() <= u16::MAX, + io_port_allocator_initialized(), ensures result is Some ==> result->Some_0@ == port, result is Some ==> result->Some_0.well_formed(), @@ -206,7 +385,7 @@ impl IoPortAllocator { let mut allocator = self.allocator.lock(); let allocator_inner = &mut *allocator; proof! { - use_type_invariant(&*allocator_inner); + lemma_io_port_alloc_init(&*allocator_inner); } let mut range = port..(port + size_of::() as u16); // `Iterator::any` with a capturing closure is not supported by Verus. @@ -215,16 +394,30 @@ impl IoPortAllocator { let mut already_allocated = false; #[verus_spec(scan_iter => invariant - allocator_inner.type_inv(), + allocator_inner.allocator.inner.inv(), + allocator_inner.allocator.inner@.len() + == crate::arch::io::MAX_IO_PORT as int, !already_allocated ==> forall|id: usize| range.start as usize <= id < (range.start as int + scan_iter.index()) as usize ==> !id_alloc_view(&allocator_inner.allocator.inner).contains(id), )] for i in range.clone() { + proof! { + assert((i as usize) < allocator_inner.allocator.inner@.len()) by { + assert((i as usize) < range.end as usize); + assert((range.end as usize) <= u16::MAX as usize); + assert((u16::MAX as usize) <= crate::arch::io::MAX_IO_PORT as usize); + assert(allocator_inner.allocator.inner@.len() + == crate::arch::io::MAX_IO_PORT as int); + } + } if allocator_inner.allocator.inner.is_allocated(i as usize) { already_allocated = true; } + proof! { + lemma_id_alloc_view_contains(&allocator_inner.allocator.inner, i as usize); + } } proof_decl! { let tracked range_claim: IoPortClaim; @@ -272,6 +465,9 @@ impl IoPortAllocator { } #[verus_spec(allocation_iter => invariant + allocator_inner.allocator.inner.inv(), + allocator_inner.allocator.inner@.len() + == crate::arch::io::MAX_IO_PORT as int, range.end as usize <= id_alloc_capacity(&allocator_inner.allocator.inner), allocator_inner.tracked_allocated@.instance_id() == io_port_allocator_instance_id(), @@ -357,6 +553,7 @@ impl IoPortAllocator { claim.instance_id() == io_port_allocator_instance_id(), claim.set() =~= port_id_set(range.start as usize, range.end as usize), range.start <= range.end, + io_port_allocator_initialized(), )] pub(in crate::io) unsafe fn recycle(&self, range: Range) { /* debug!("Recycling MMIO range: {:#x?}", range); */ @@ -369,9 +566,20 @@ impl IoPortAllocator { let mut allocator = self.allocator.lock(); let allocator_inner = &mut *allocator; proof! { - use_type_invariant(&*allocator_inner); + lemma_io_port_alloc_init(&*allocator_inner); assert(range.start as usize <= range.end as usize); assert(claim.instance_id() == allocator_inner.tracked_allocated@.instance_id()); + allocator_inner.tracked_allocated.borrow().claim_includes(&claim); + assert(port_id_set(range.start as usize, range.end as usize) + <= allocator_inner.tracked_allocated@.value()); + assert(port_id_set(range.start as usize, range.end as usize) + <= id_alloc_view(&allocator_inner.allocator.inner)); + assert((range.end as usize) <= allocator_inner.allocator.inner@.len()) by { + assert((range.end as usize) <= u16::MAX as usize); + assert((u16::MAX as usize) <= crate::arch::io::MAX_IO_PORT as usize); + assert(allocator_inner.allocator.inner@.len() + == crate::arch::io::MAX_IO_PORT as int); + } allocator_inner.tracked_allocated.borrow_mut().release(claim); assert forall|id: usize| #[trigger] allocator_inner.tracked_allocated@.value().contains(id) implies { @@ -384,6 +592,27 @@ impl IoPortAllocator { id, ); } + assert forall|i: int| + range.start as usize <= i + && i < allocator_inner.allocator.inner@.len() + && i < range.end as usize implies + allocator_inner.allocator.inner@[i] + by { + assert(0 <= i); + assert(i < allocator_inner.allocator.inner@.len()); + assert(allocator_inner.allocator.inner@.len() <= usize::MAX as int); + assert(i <= usize::MAX as int); + assert((i as usize) as int == i); + lemma_port_id_set_contains( + range.start as usize, + range.end as usize, + i as usize, + ); + assert(port_id_set(range.start as usize, range.end as usize).contains(i as usize)); + assert(id_alloc_view(&allocator_inner.allocator.inner).contains(i as usize)); + lemma_id_alloc_view_contains(&allocator_inner.allocator.inner, i as usize); + assert(allocator_inner.allocator.inner@[i]); + } } allocator_inner .allocator @@ -401,6 +630,20 @@ verus! { /// explicit specification boundary for the architecture's guarantee that [`init`] ran first. pub uninterp spec fn io_port_allocator_initialized() -> bool; +/// Trusted: once `init` has run, the global allocator's inner satisfies its invariant. +#[verifier::external_body] +proof fn lemma_io_port_alloc_init(inner: &IoPortAllocatorInner) + requires + io_port_allocator_initialized(), + ensures + io_port_inner_inv_values( + inner.tracked_allocated@.instance_id(), + inner.tracked_allocated@.value(), + &inner.allocator.inner, + ), +{ +} + } // verus! pub(super) static IO_PORT_ALLOCATOR: Once = Once::new(); diff --git a/verified_libs/vstd_extra/Cargo.toml b/verified_libs/vstd_extra/Cargo.toml index 9c87a296d..b95c61f43 100644 --- a/verified_libs/vstd_extra/Cargo.toml +++ b/verified_libs/vstd_extra/Cargo.toml @@ -16,7 +16,6 @@ std = ["vstd/std"] [dependencies] vstd = { workspace = true } bitvec.workspace = true -id-alloc = { path = "../../ostd/libs/id-alloc" } [target.'cfg(target_arch = "x86_64")'.dependencies] x86_64 = "0.14.13" diff --git a/verified_libs/vstd_extra/src/external/id_alloc.rs b/verified_libs/vstd_extra/src/external/id_alloc.rs deleted file mode 100644 index 8e9904339..000000000 --- a/verified_libs/vstd_extra/src/external/id_alloc.rs +++ /dev/null @@ -1,61 +0,0 @@ -//! Specifications for the bitmap-backed ID allocator. -use core::ops::Range; - -use id_alloc::IdAlloc; -use vstd::prelude::*; - -verus! { - -/// Verus model for the external bitmap-backed ID allocator. -#[verifier::external_type_specification] -#[verifier::external_body] -pub struct ExIdAlloc(IdAlloc); - -/// IDs currently allocated by an external `IdAlloc`. -pub uninterp spec fn id_alloc_view(allocator: &IdAlloc) -> Set; - -/// Capacity configured for an external `IdAlloc`. -pub uninterp spec fn id_alloc_capacity(allocator: &IdAlloc) -> usize; - -pub assume_specification[ IdAlloc::with_capacity ](capacity: usize) -> (allocator: IdAlloc) - ensures - id_alloc_capacity(&allocator) == capacity, - id_alloc_view(&allocator) == Set::::empty(), -; - -pub assume_specification[ IdAlloc::is_allocated ](allocator: &IdAlloc, id: usize) -> (allocated: - bool) - ensures - id < id_alloc_capacity(allocator) ==> allocated == id_alloc_view(allocator).contains(id), -; - -pub assume_specification[ IdAlloc::alloc_specific ](allocator: &mut IdAlloc, id: usize) -> (result: - Option) - requires - id < id_alloc_capacity(old(allocator)), - ensures - id_alloc_capacity(final(allocator)) == id_alloc_capacity(old(allocator)), - id_alloc_view(final(allocator)) == id_alloc_view(old(allocator)).insert(id), - id_alloc_view(old(allocator)).subset_of(id_alloc_view(final(allocator))), - id_alloc_view(old(allocator)).contains(id) ==> { - &&& result is None - }, - !id_alloc_view(old(allocator)).contains(id) ==> { - &&& result == Some(id) - }, - no_unwind -; - -pub assume_specification[ IdAlloc::free_consecutive ](allocator: &mut IdAlloc, range: Range) - requires - range.end <= id_alloc_capacity(old(allocator)), - ensures - id_alloc_capacity(final(allocator)) == id_alloc_capacity(old(allocator)), - forall|id: usize| #[trigger] - id_alloc_view(final(allocator)).contains(id) <==> id_alloc_view( - old(allocator), - ).contains(id) && !(range.start <= id < range.end), - no_unwind -; - -} // verus! diff --git a/verified_libs/vstd_extra/src/external/mod.rs b/verified_libs/vstd_extra/src/external/mod.rs index d7aad6178..386b2e3b6 100644 --- a/verified_libs/vstd_extra/src/external/mod.rs +++ b/verified_libs/vstd_extra/src/external/mod.rs @@ -7,12 +7,11 @@ pub mod btree; pub mod cmp; pub mod convert; pub mod deref; -pub mod id_alloc; pub mod ilog2; pub mod int_specs; -pub mod iter; #[cfg(target_arch = "x86_64")] pub mod io_port; +pub mod iter; pub mod nonnull; pub mod ptr; pub mod range; @@ -23,12 +22,11 @@ pub mod time; pub use bitvec::*; pub use btree::*; pub use cmp::*; -pub use id_alloc::*; pub use ilog2::*; pub use int_specs::*; -pub use iter::*; #[cfg(target_arch = "x86_64")] pub use io_port::*; +pub use iter::*; pub use nonnull::*; pub use ptr::*; pub use range::*; From ea38da80c7ba74906513e9ea633030fe88cf262b Mon Sep 17 00:00:00 2001 From: Marsman1996 Date: Sat, 12 Sep 2026 19:56:24 +0800 Subject: [PATCH 14/22] refine: according to the review skill --- ostd/src/io/io_mem/allocator.rs | 10 +++-- ostd/src/io/io_mem/mod.rs | 25 ++++++------ ostd/src/io/io_port/allocator.rs | 39 ++++++------------- ostd/src/io/io_port/mod.rs | 11 +++--- .../vstd_extra/src/external/io_port.rs | 4 +- 5 files changed, 39 insertions(+), 50 deletions(-) diff --git a/ostd/src/io/io_mem/allocator.rs b/ostd/src/io/io_mem/allocator.rs index f74301f12..3767c31ca 100644 --- a/ostd/src/io/io_mem/allocator.rs +++ b/ostd/src/io/io_mem/allocator.rs @@ -2,7 +2,7 @@ //! I/O Memory allocator. use crate::specs::arch::PAGE_SIZE; use crate::sync::{OnceImpl, TrivialPred}; -use vstd::prelude::*; +use vstd::{arithmetic::power2::is_pow2, prelude::*}; use vstd_extra::resource::flags::OneShotSet; use alloc::vec::Vec; @@ -30,13 +30,15 @@ impl IoMemAllocator { /// If the range is not available, then the return value will be `None`. #[verus_spec(result => requires - vstd::arithmetic::power2::is_pow2(PAGE_SIZE as int), + is_pow2(PAGE_SIZE as int), range.start < range.end, range.end <= usize::MAX - (PAGE_SIZE - 1), io_mem_range_registered(range), ensures - result is Some ==> result->Some_0.paddr_spec() == range.start, - result is Some ==> result->Some_0.length_spec() == range.end - range.start, + result matches Some(io_mem) ==> { + &&& io_mem.paddr_spec() == range.start + &&& io_mem.length_spec() == range.end - range.start + }, )] pub fn acquire(&self, range: Range) -> Option { /* Original Rust: diff --git a/ostd/src/io/io_mem/mod.rs b/ostd/src/io/io_mem/mod.rs index 8bd0e1da1..fa64c5e96 100644 --- a/ostd/src/io/io_mem/mod.rs +++ b/ostd/src/io/io_mem/mod.rs @@ -1,11 +1,12 @@ // SPDX-License-Identifier: MPL-2.0 //! I/O memory and its allocator that allocates memory I/O (MMIO) to device drivers. -use crate::specs::arch::PAGE_SIZE; use crate::specs::{ + arch::PAGE_SIZE, mm::{io::VmIoOwner, virt_mem::VirtPtr}, task::AnyAtomicGuard, }; -use vstd::prelude::*; +use vstd::{arithmetic::power2::is_pow2, prelude::*}; +use vstd_extra::panic::UnwrapOrPanic; mod allocator; @@ -60,7 +61,7 @@ impl IoMem { } // verus! #[verus_verify] impl HasPaddr for IoMem { - #[verus_spec(result => ensures result == self.paddr_spec())] + #[verus_spec(returns self.paddr_spec())] fn paddr(&self) -> Paddr { self.pa } @@ -71,34 +72,36 @@ impl IoMem { /// Acquires an `IoMem` instance for the given range. #[verus_spec(result => requires - vstd::arithmetic::power2::is_pow2(PAGE_SIZE as int), + is_pow2(PAGE_SIZE as int), range.start < range.end, range.end <= usize::MAX - (PAGE_SIZE - 1), allocator::io_mem_range_registered(range), + vstd_extra::panic::may_panic(), ensures - result is Ok ==> result->Ok_0.paddr_spec() == range.start, - result is Ok ==> result->Ok_0.length_spec() - == range.end - range.start, + result matches Ok(io_mem) ==> { + &&& io_mem.paddr_spec() == range.start + &&& io_mem.length_spec() == range.end - range.start + }, )] pub fn acquire(range: Range) -> Result { allocator::IO_MEM_ALLOCATOR .get() /* .unwrap() */ - .ok_or(Error::AccessDenied)? + .unwrap_or_panic() .acquire(range) .ok_or(Error::AccessDenied) } /// Returns the physical address of the I/O memory. #[verus_verify] - #[verus_spec(result => ensures result == self.paddr_spec())] + #[verus_spec(returns self.paddr_spec())] pub fn paddr(&self) -> Paddr { self.pa } /// Returns the length of the I/O memory region. #[verus_verify] - #[verus_spec(result => ensures result == self.length_spec())] + #[verus_spec(returns self.length_spec())] pub fn length(&self) -> usize { self.limit } @@ -146,7 +149,7 @@ impl IoMem { #[verifier::external_body] #[verus_spec(result => requires - vstd::arithmetic::power2::is_pow2(PAGE_SIZE as int), + is_pow2(PAGE_SIZE as int), range.start <= range.end, range.end <= usize::MAX - (PAGE_SIZE - 1), ensures diff --git a/ostd/src/io/io_port/allocator.rs b/ostd/src/io/io_port/allocator.rs index b818ebbb5..0c9766054 100644 --- a/ostd/src/io/io_port/allocator.rs +++ b/ostd/src/io/io_port/allocator.rs @@ -1,8 +1,10 @@ // SPDX-License-Identifier: MPL-2.0 //! I/O port allocator. -use vstd::prelude::*; -use vstd::resource::set::{GhostSetAuth, GhostSubset}; -use vstd::tokens::InstanceId; +use vstd::{ + prelude::*, + resource::set::{GhostSetAuth, GhostSubset}, + tokens::InstanceId, +}; use vstd_extra::ownership::Inv; use core::ops::Range; @@ -19,13 +21,6 @@ use crate::{ verus! { -/// Opaque specification for the third-party one-time initialization primitive. -#[verifier::external_type_specification] -#[verifier::external_body] -#[verifier::reject_recursive_types(T)] -#[verifier::reject_recursive_types(R)] -pub struct ExOnce(spin::once::Once); - /// Identity assigned to the single global PIO allocator during trusted boot initialization. pub uninterp spec fn io_port_allocator_instance_id() -> InstanceId; @@ -339,19 +334,6 @@ struct IoPortAllocatorInner { tracked_allocated: Tracked, } -verus! { - -impl IoPortAllocatorInner { - pub closed spec fn type_inv(self) -> bool { - io_port_inner_inv_values( - self.tracked_allocated@.instance_id(), - self.tracked_allocated@.value(), - &self.allocator.inner, - ) - } -} - -} // verus! /// I/O port allocator that allocates port I/O access to device drivers. #[verus_verify] pub struct IoPortAllocator { @@ -374,12 +356,13 @@ impl IoPortAllocator { port as usize + size_of::() <= u16::MAX, io_port_allocator_initialized(), ensures - result is Some ==> result->Some_0@ == port, - result is Some ==> result->Some_0.well_formed(), result is Some <==> claim@ is Some, - result is Some ==> claim@->Some_0.instance_id() == - io_port_allocator_instance_id(), - result is Some ==> result->Some_0.claim_matches_set(claim@->Some_0.set()), + result matches Some(io_port) ==> { + &&& io_port@ == port + &&& io_port.well_formed() + &&& io_port.claim_matches_set(claim@->Some_0.set()) + &&& claim@->Some_0.instance_id() == io_port_allocator_instance_id() + }, )] pub fn acquire(&self, port: u16) -> Option> { let mut allocator = self.allocator.lock(); diff --git a/ostd/src/io/io_port/mod.rs b/ostd/src/io/io_port/mod.rs index b89797e1b..e844945f2 100644 --- a/ostd/src/io/io_port/mod.rs +++ b/ostd/src/io/io_port/mod.rs @@ -114,12 +114,13 @@ impl IoPort { port as usize + size_of::() <= u16::MAX, allocator::io_port_allocator_initialized(), ensures - result is Ok ==> result->Ok_0@ == port, - result is Ok ==> result->Ok_0.well_formed(), result is Ok <==> claim@ is Some, - result is Ok ==> claim@->Some_0.instance_id() == - allocator::io_port_allocator_instance_id(), - result is Ok ==> result->Ok_0.claim_matches_set(claim@->Some_0.set()), + result matches Ok(io_port) ==> { + &&& io_port@ == port + &&& io_port.well_formed() + &&& io_port.claim_matches_set(claim@->Some_0.set()) + &&& claim@->Some_0.instance_id() == allocator::io_port_allocator_instance_id() + }, )] pub fn acquire(port: u16) -> Result> { proof_decl! { diff --git a/verified_libs/vstd_extra/src/external/io_port.rs b/verified_libs/vstd_extra/src/external/io_port.rs index 96b810b22..1a0a6e41a 100644 --- a/verified_libs/vstd_extra/src/external/io_port.rs +++ b/verified_libs/vstd_extra/src/external/io_port.rs @@ -17,10 +17,10 @@ pub open spec fn valid_io_port_number(port: int) -> bool { 0 <= port <= u16::MAX as int } -/// Whether an access of type `T` is fully contained in the x86 I/O-port address space. +/// Whether an access of type `T` fits in the PIO byte range `0..u16::MAX`. pub open spec fn valid_io_port_access(port: int) -> bool { &&& valid_io_port_number(port) - &&& port + size_of::() <= u16::MAX as int + 1 + &&& port + size_of::() <= u16::MAX as int } /// Opaque specification boundary for the third-party read/write access marker. From 987e810cc30fc89eb4f1931694bf0baf4162b15a Mon Sep 17 00:00:00 2001 From: Marsman1996 Date: Tue, 15 Sep 2026 15:35:35 +0800 Subject: [PATCH 15/22] sync: ostd/src/io/io_port to 0.18.1 --- README.md | 2 +- ostd/src/arch/x86/device/io_port.rs | 2 +- ostd/src/arch/x86/pci.rs | 2 + ostd/src/io/io_port/allocator.rs | 68 ++++--- ostd/src/io/io_port/mod.rs | 168 ++++++++++++++---- ostd/src/io/mod.rs | 9 +- .../vstd_extra/src/external/io_port.rs | 54 ++++-- 7 files changed, 229 insertions(+), 76 deletions(-) diff --git a/README.md b/README.md index 52e1f12da..f45609b82 100644 --- a/README.md +++ b/README.md @@ -5,7 +5,7 @@ [![verify (verus-lang/verus)](https://img.shields.io/github/actions/workflow/status/asterinas/vostd/ci-upstream-verus.yml?branch=main&label=verify%20(verus-lang%2Fverus))](https://github.com/asterinas/vostd/actions/workflows/ci-upstream-verus.yml) > [!NOTE] -> This repository is currently in a transitional state: the components under `ostd/src/sync` and `ostd/libs/id-alloc` already track the upcoming Asterinas release [v0.18.1](https://github.com/asterinas/asterinas/releases/tag/v0.18.1), while every other OSTD component is still based on [v0.16.0](https://github.com/asterinas/asterinas/releases/tag/v0.16.0). +> This repository is currently in a transitional state: the components under `ostd/src/sync`, `ostd/libs/id-alloc` and `ostd/src/io/io_port` already track the upcoming Asterinas release [v0.18.1](https://github.com/asterinas/asterinas/releases/tag/v0.18.1), while every other OSTD component is still based on [v0.16.0](https://github.com/asterinas/asterinas/releases/tag/v0.16.0). ## Overview diff --git a/ostd/src/arch/x86/device/io_port.rs b/ostd/src/arch/x86/device/io_port.rs index 11b10c0a8..4ab813494 100644 --- a/ostd/src/arch/x86/device/io_port.rs +++ b/ostd/src/arch/x86/device/io_port.rs @@ -1,6 +1,6 @@ // SPDX-License-Identifier: MPL-2.0 //! I/O port access. -pub use vstd_extra::external::{valid_io_port_access, valid_io_port_number}; +pub use vstd_extra::external::{group_io_port_models, obeys_pio_model, valid_io_port_access}; pub use x86_64::{ instructions::port::{ diff --git a/ostd/src/arch/x86/pci.rs b/ostd/src/arch/x86/pci.rs index c1c142c04..d8292ac4e 100644 --- a/ostd/src/arch/x86/pci.rs +++ b/ostd/src/arch/x86/pci.rs @@ -7,7 +7,9 @@ use crate::{bus::pci::PciDeviceLocation, io::IoPort, prelude::*}; verus! { +broadcast use super::device::io_port::group_io_port_models; // Original Rust: static PCI_ADDRESS_PORT: IoPort = unsafe { IoPort::new(0x0CF8) }; + exec static PCI_ADDRESS_PORT: IoPort ensures PCI_ADDRESS_PORT.well_formed(), diff --git a/ostd/src/io/io_port/allocator.rs b/ostd/src/io/io_port/allocator.rs index 0c9766054..bf1aa787b 100644 --- a/ostd/src/io/io_port/allocator.rs +++ b/ostd/src/io/io_port/allocator.rs @@ -14,6 +14,7 @@ use log::debug; use spin::Once; use super::{IoPort, lemma_port_id_set_contains, lemma_port_id_set_insert, port_id_set}; +use crate::arch::device::io_port::obeys_pio_model; use crate::{ io::RawIoPortRange, sync::{LocalIrqDisabled, SpinLock}, @@ -124,6 +125,7 @@ pub(crate) proof fn lemma_alloc_specific_view( { let old_len: int = old_a@.len() as int; assert forall|j: usize| + #![trigger id_alloc_view(final_a).contains(j)] id_alloc_view(final_a).contains(j) == (id_alloc_view(old_a).insert(id)).contains(j) by { lemma_id_alloc_bits_char(old_a@, old_len, j); lemma_id_alloc_bits_char(final_a@, final_a@.len() as int, j); @@ -336,7 +338,7 @@ struct IoPortAllocatorInner { /// I/O port allocator that allocates port I/O access to device drivers. #[verus_verify] -pub struct IoPortAllocator { +pub(super) struct IoPortAllocator { /// Each ID indicates whether a Port I/O (1B) is allocated. /// /// Instead of using `RangeAllocator` like `IoMemAllocator` does, it is more reasonable to use `IdAlloc`, @@ -346,31 +348,42 @@ pub struct IoPortAllocator { #[verus_verify] impl IoPortAllocator { - /// Acquires the `IoPort`. Return None if any region in `port` cannot be allocated. + /// Acquires an `IoPort`. Returns `None` if the PIO range is unavailable. + /// + /// `is_overlapping` indicates whether another `IoPort` can have a PIO range that overlaps with + /// this one. If it is true, only the first port in the PIO range will be marked as occupied; + /// otherwise, all ports in the PIO range will be marked as occupied. #[verus_spec(result => with - -> claim: Tracked>, + Tracked(claim_out): Tracked<&mut Tracked>>, requires - vstd::layout::size_of::() <= u16::MAX, size_of::() <= u16::MAX, - port as usize + size_of::() <= u16::MAX, + is_overlapping ==> port as usize + size_of::() <= u16::MAX, + obeys_pio_model::(), io_port_allocator_initialized(), + (*old(claim_out))@ is None, ensures - result is Some <==> claim@ is Some, + result is Some <==> (*final(claim_out))@ is Some, result matches Some(io_port) ==> { &&& io_port@ == port + &&& io_port.is_overlapping() == is_overlapping &&& io_port.well_formed() - &&& io_port.claim_matches_set(claim@->Some_0.set()) - &&& claim@->Some_0.instance_id() == io_port_allocator_instance_id() + &&& io_port.claim_matches_set((*final(claim_out))@->Some_0.set()) + &&& (*final(claim_out))@->Some_0.instance_id() == io_port_allocator_instance_id() }, )] - pub fn acquire(&self, port: u16) -> Option> { + pub(super) fn acquire(&self, port: u16, is_overlapping: bool) -> Option> { + let range = if !is_overlapping { + port..port.checked_add(size_of::().try_into().ok()?)? + } else { + port..port.checked_add(1)? + }; + /* debug!("Try to acquire PIO range: {:#x?}", range); */ let mut allocator = self.allocator.lock(); let allocator_inner = &mut *allocator; proof! { lemma_io_port_alloc_init(&*allocator_inner); } - let mut range = port..(port + size_of::() as u16); // `Iterator::any` with a capturing closure is not supported by Verus. // Original Rust: // if range.any(|i| allocator.is_allocated(i as usize)) { return None; } @@ -407,10 +420,10 @@ impl IoPortAllocator { } if already_allocated { allocator.drop(); - return { - proof_with!(|= Tracked(None)); - None - }; + proof! { + *claim_out = Tracked(None); + } + return None; } proof_decl! { @@ -516,11 +529,13 @@ impl IoPortAllocator { range_claim = allocator_inner.tracked_allocated.borrow_mut().allocate(ids); } - // SAFETY: The created IoPort is guaranteed not to access system device I/O - /* Original Rust: unsafe { Some(IoPort::new(port)) } */ - let result = unsafe { Some(IoPort::new(port)) }; + // SAFETY: The created `IoPort` is guaranteed not to access system device I/O. + /* Original Rust: unsafe { Some(IoPort::new_overlapping(port, is_overlapping)) } */ + let result = unsafe { Some(IoPort::new_overlapping(port, is_overlapping)) }; allocator.drop(); - proof_with!(|= Tracked(Some(range_claim))); + proof! { + *claim_out = Tracked(Some(range_claim)); + } result } @@ -538,8 +553,8 @@ impl IoPortAllocator { range.start <= range.end, io_port_allocator_initialized(), )] - pub(in crate::io) unsafe fn recycle(&self, range: Range) { - /* debug!("Recycling MMIO range: {:#x?}", range); */ + pub(super) unsafe fn recycle(&self, range: Range) { + /* debug!("Recycling PIO range: {:#x?}", range); */ /* Original Rust: self.allocator .lock() @@ -642,22 +657,23 @@ pub(super) static IO_PORT_ALLOCATOR: Once = Once::new(); /// 2. `MAX_IO_PORT` defined in `crate::arch::io` is guaranteed not to exceed the maximum /// value specified by architecture. #[verifier::external_body] -pub(crate) unsafe fn init() { +pub(in crate::io) unsafe fn init() { // SAFETY: `MAX_IO_PORT` is guaranteed not to exceed the maximum value specified by architecture. let mut allocator = IdAlloc::with_capacity(crate::arch::io::MAX_IO_PORT as usize); - extern "C" { + unsafe extern "C" { fn __sensitive_io_ports_start(); fn __sensitive_io_ports_end(); } - let start = __sensitive_io_ports_start as usize; - let end = __sensitive_io_ports_end as usize; - assert!((end - start) % size_of::() == 0); + let start = __sensitive_io_ports_start as *const () as usize; + let end = __sensitive_io_ports_end as *const () as usize; + assert!((end - start).is_multiple_of(size_of::())); // Iterate through the sensitive I/O port ranges and remove them from the allocator. let io_port_range_count = (end - start) / size_of::(); for i in 0..io_port_range_count { - let range_base_addr = __sensitive_io_ports_start as usize + i * size_of::(); + let range_base_addr = + __sensitive_io_ports_start as *const () as usize + i * size_of::(); // SAFETY: The range is guaranteed to be valid as it is defined in the `.sensitive_io_ports` section. let port_range = unsafe { *(range_base_addr as *const RawIoPortRange) }; diff --git a/ostd/src/io/io_port/mod.rs b/ostd/src/io/io_port/mod.rs index e844945f2..fddbed460 100644 --- a/ostd/src/io/io_port/mod.rs +++ b/ostd/src/io/io_port/mod.rs @@ -3,7 +3,7 @@ use vstd::prelude::*; use crate::arch::device::io_port::{ - IoPortReadAccess, IoPortWriteAccess, PortRead, PortWrite, valid_io_port_access, + IoPortReadAccess, IoPortWriteAccess, PortRead, PortWrite, obeys_pio_model, valid_io_port_access, }; mod allocator; @@ -12,6 +12,11 @@ use core::{marker::PhantomData, mem::size_of}; pub(super) use self::allocator::init; use crate::{Error, prelude::*}; +verus! { + +broadcast use crate::arch::device::io_port::group_io_port_models; + +} // verus! /// An I/O port, representing a specific address in the I/O address of x86. /// /// The following code shows and example to read and write u32 value to an I/O port: @@ -24,9 +29,11 @@ use crate::{Error, prelude::*}; /// } /// ``` /// +#[derive(Debug)] #[verus_verify] pub struct IoPort { port: u16, + is_overlapping: bool, value_marker: PhantomData, access_marker: PhantomData, } @@ -48,9 +55,26 @@ impl IoPort { valid_io_port_access::(self@ as int) } - /// Whether `claim` is the allocator-issued ownership token for this complete typed range. + /// Whether the port was acquired as overlapping: it occupies only its first port. + /// + /// Marks the occupied range of [`Self::claim_matches_set`] and the released range of + /// [`Self::drop`]. + pub closed spec fn is_overlapping(&self) -> bool { + self.is_overlapping + } + + /// Whether `claim` is the allocator-issued ownership token for this port's occupied range: + /// the complete typed range, or only the first port if the port was acquired as + /// overlapping. pub open spec fn claim_matches_set(&self, claim: Set) -> bool { - claim == port_id_set(self@ as usize, (self@ as usize + size_of::()) as usize) + claim == port_id_set( + self@ as usize, + if self.is_overlapping() { + (self@ as usize + 1) as usize + } else { + (self@ as usize + size_of::()) as usize + }, + ) } } @@ -105,18 +129,21 @@ fn initialized_allocator() -> &'static allocator::IoPortAllocator { #[verus_verify] impl IoPort { /// Acquires an `IoPort` instance for the given range. + /// + /// This method will mark all ports in the PIO range as occupied. #[verus_spec(result => with -> claim: Tracked>, requires - vstd::layout::size_of::() <= u16::MAX, size_of::() <= u16::MAX, port as usize + size_of::() <= u16::MAX, + obeys_pio_model::(), allocator::io_port_allocator_initialized(), ensures - result is Ok <==> claim@ is Some, + result is Ok <== claim@ is Some, result matches Ok(io_port) ==> { &&& io_port@ == port + &&& !io_port.is_overlapping() &&& io_port.well_formed() &&& io_port.claim_matches_set(claim@->Some_0.set()) &&& claim@->Some_0.instance_id() == allocator::io_port_allocator_instance_id() @@ -124,13 +151,56 @@ impl IoPort { )] pub fn acquire(port: u16) -> Result> { proof_decl! { - let tracked claim: Option; + let tracked mut claim: Tracked> = Tracked(None); + } + let port = { + /* Original Rust: allocator::IO_PORT_ALLOCATOR.get().unwrap() */ + #[verus_spec(with Tracked(&mut claim))] + initialized_allocator().acquire(port, false) + }; + let result = port.ok_or(Error::AccessDenied); + proof_decl! { + let tracked claim_val: Option = claim.get(); + } + proof_with!(|= Tracked(claim_val)); + result + } + + /// Acquires an `IoPort` instance that may overlap with other `IoPort`s. + /// + /// This method will only mark the first port in the PIO range as occupied. + #[verus_spec(result => + with + -> claim: Tracked>, + requires + size_of::() <= u16::MAX, + port as usize + size_of::() <= u16::MAX, + obeys_pio_model::(), + allocator::io_port_allocator_initialized(), + ensures + result is Ok <== claim@ is Some, + result matches Ok(io_port) ==> { + &&& io_port@ == port + &&& io_port.is_overlapping() + &&& io_port.well_formed() + &&& io_port.claim_matches_set(claim@->Some_0.set()) + &&& claim@->Some_0.instance_id() == allocator::io_port_allocator_instance_id() + }, + )] + pub fn acquire_overlapping(port: u16) -> Result> { + proof_decl! { + let tracked mut claim: Tracked> = Tracked(None); } - #[verus_spec(with => Tracked(claim))] - /* Original Rust: allocator::IO_PORT_ALLOCATOR.get().unwrap() */ - let port = initialized_allocator().acquire(port); + let port = { + /* Original Rust: allocator::IO_PORT_ALLOCATOR.get().unwrap() */ + #[verus_spec(with Tracked(&mut claim))] + initialized_allocator().acquire(port, true) + }; let result = port.ok_or(Error::AccessDenied); - proof_with!(|= Tracked(claim)); + proof_decl! { + let tracked claim_val: Option = claim.get(); + } + proof_with!(|= Tracked(claim_val)); result } @@ -145,24 +215,50 @@ impl IoPort { size_of::() as u16 } - /// Create an I/O port. + /// Creates an I/O port. + /// + /// # Safety + /// + /// Reading from or writing to the I/O port may have side effects. Those side effects must + /// not cause soundness problems (e.g., they must not corrupt the kernel memory). + #[verus_spec(ret => + requires + size_of::() <= u16::MAX, + port as usize + size_of::() <= u16::MAX, + obeys_pio_model::(), + ensures + ret@ == port, + !ret.is_overlapping(), + ret.well_formed(), + )] + pub(crate) const unsafe fn new(port: u16) -> Self { + // SAFETY: The safety is upheld by the caller. + unsafe { Self::new_overlapping(port, false) } + } + + /// Creates an I/O port. + /// + /// See [`allocator::IoPortAllocator::acquire`] for an explanation of the `is_overlapping` + /// argument. /// /// # Safety /// - /// This function is marked unsafe as creating an I/O port is considered - /// a privileged operation. + /// Reading from or writing to the I/O port may have side effects. Those side effects must + /// not cause soundness problems (e.g., they must not corrupt the kernel memory). #[verus_spec(ret => requires - vstd::layout::size_of::() <= u16::MAX, size_of::() <= u16::MAX, port as usize + size_of::() <= u16::MAX, + obeys_pio_model::(), ensures ret@ == port, + ret.is_overlapping() == is_overlapping, ret.well_formed(), )] - pub const unsafe fn new(port: u16) -> Self { + const unsafe fn new_overlapping(port: u16, is_overlapping: bool) -> Self { Self { port, + is_overlapping, value_marker: PhantomData, access_marker: PhantomData, } @@ -170,8 +266,8 @@ impl IoPort { /// Releases the allocator claim for this port. /// - /// VERUS LIMITATION: this is called explicitly because Verus does not yet support proving the - /// standard `Drop` implementation below. + /// VERUS LIMITATION: this is called explicitly because Verus does not yet support proving + /// the standard `Drop` implementation below. #[verus_spec( with Tracked(claim): Tracked, @@ -179,10 +275,15 @@ impl IoPort { allocator::io_port_allocator_initialized(), claim.instance_id() == allocator::io_port_allocator_instance_id(), self.claim_matches_set(claim.set()), - self@ as usize + size_of::() <= u16::MAX, + self@ as usize + + (if self.is_overlapping() { 1 } else { size_of::() }) <= u16::MAX, )] pub fn drop(self) { - let range = self.port..(self.port + size_of::() as u16); + let range = if self.is_overlapping { + self.port..(self.port + 1) + } else { + self.port..(self.port + size_of::() as u16) + }; unsafe { #[verus_spec(with Tracked(claim))] initialized_allocator().recycle(range); @@ -194,7 +295,6 @@ impl IoPort { #[verifier::allow(undeclared_external_trait)] impl IoPort { /// Reads from the I/O port - #[inline] #[verus_spec(requires self.well_formed())] pub fn read(&self) -> T { unsafe { PortRead::read_from_port(self.port) } @@ -205,7 +305,6 @@ impl IoPort { #[verifier::allow(undeclared_external_trait)] impl IoPort { /// Writes to the I/O port - #[inline] #[verus_spec(requires self.well_formed())] pub fn write(&self, value: T) { unsafe { PortWrite::write_to_port(self.port, value) } @@ -214,13 +313,14 @@ impl IoPort { /* impl Drop for IoPort { fn drop(&mut self) { - // SAFETY: The caller have ownership of the PIO region. - unsafe { - allocator::IO_PORT_ALLOCATOR - .get() - .unwrap() - .recycle(self.port..(self.port + size_of::() as u16)); - } + let range = if !self.is_overlapping { + self.port..(self.port + size_of::() as u16) + } else { + self.port..(self.port + 1) + }; + + // SAFETY: We have ownership of the PIO region. + unsafe { allocator::IO_PORT_ALLOCATOR.get().unwrap().recycle(range) }; } } */ @@ -240,7 +340,8 @@ macro_rules! reserve_io_port_range { const _: () = { #[used] - #[link_section = ".sensitive_io_ports"] + // SAFETY: This is properly handled in the linker script. + #[unsafe(link_section = ".sensitive_io_ports")] static _RANGE: crate::io::RawIoPortRange = crate::io::RawIoPortRange { begin: $range.start, end: $range.end, @@ -277,15 +378,14 @@ macro_rules! sensitive_io_port { $(#[$meta])* $vis static $name: IoPort<$size, $access> = { #[used] - #[link_section = ".sensitive_io_ports"] + // SAFETY: This is properly handled in the linker script. + #[unsafe(link_section = ".sensitive_io_ports")] static _RESERVED_IO_PORT_RANGE: crate::io::RawIoPortRange = crate::io::RawIoPortRange { begin: $name.port(), end: $name.port() + $name.size(), }; - unsafe { - IoPort::new($port) - } + unsafe { IoPort::new($port) } }; )* }; @@ -295,8 +395,8 @@ pub(crate) use reserve_io_port_range; pub(crate) use sensitive_io_port; #[doc(hidden)] -#[derive(Debug, Clone, Copy)] #[repr(C)] +#[derive(Clone, Copy, Debug)] #[verus_verify] pub(crate) struct RawIoPortRange { pub(crate) begin: u16, diff --git a/ostd/src/io/mod.rs b/ostd/src/io/mod.rs index b27636383..e868aa4b3 100644 --- a/ostd/src/io/mod.rs +++ b/ostd/src/io/mod.rs @@ -7,7 +7,7 @@ //! - `IoPort` for port I/O (PIO). use vstd::prelude::*; -mod io_mem; +pub(crate) mod io_mem; use cfg_if::cfg_if; @@ -17,7 +17,8 @@ pub(crate) use self::io_mem::IoMemAllocatorBuilder; cfg_if!( if #[cfg(target_arch = "x86_64")] { mod io_port; - pub use io_port::IoPort; + + pub use self::io_port::IoPort; pub(crate) use self::io_port::{reserve_io_port_range, sensitive_io_port, RawIoPortRange}; } ); @@ -39,11 +40,11 @@ cfg_if!( #[verus_verify] pub(crate) unsafe fn init(io_mem_builder: IoMemAllocatorBuilder) { // SAFETY: The safety is upheld by the caller. - unsafe { self::io_mem::init(io_mem_builder) }; + unsafe { io_mem::init(io_mem_builder) }; // SAFETY: The safety is upheld by the caller. #[cfg(target_arch = "x86_64")] unsafe { - self::io_port::init() + io_port::init() }; } diff --git a/verified_libs/vstd_extra/src/external/io_port.rs b/verified_libs/vstd_extra/src/external/io_port.rs index 1a0a6e41a..4180a4d31 100644 --- a/verified_libs/vstd_extra/src/external/io_port.rs +++ b/verified_libs/vstd_extra/src/external/io_port.rs @@ -9,18 +9,52 @@ use x86_64::{ verus! { -/// Whether `port` is representable in the 16-bit x86 I/O-port address space. +/// Whether a `T`-typed access at `port` fits in the PIO byte range `0..=u16::MAX`. /// -/// This is only the ISA-level validity condition. It does not claim that a device decodes the -/// port, that the current CPU context may access it, or that the caller owns it. -pub open spec fn valid_io_port_number(port: int) -> bool { - 0 <= port <= u16::MAX as int -} +/// Uninterpreted: `PortRead`/`PortWrite` are user-implementable, so meaning comes only from +/// the trusted widths in [`group_io_port_models`]. ISA-level fact only — no claim about +/// device decoding, access permission, or ownership. +pub uninterp spec fn valid_io_port_access(port: int) -> bool; + +/// Whether `T` is one of the trusted port widths; uninterpreted, admitted only by the axioms +/// below. +pub uninterp spec fn obeys_pio_model() -> bool; + +/// Trusted: `u8` ports are written and read via `outb`/`inb`. +pub broadcast axiom fn axiom_u8_pio_model() + ensures + #[trigger] obeys_pio_model::(), +; + +/// Trusted: `u16` ports are written and read via `outw`/`inw`. +pub broadcast axiom fn axiom_u16_pio_model() + ensures + #[trigger] obeys_pio_model::(), +; + +/// Trusted: `u32` ports are written and read via `outl`/`inl`. +pub broadcast axiom fn axiom_u32_pio_model() + ensures + #[trigger] obeys_pio_model::(), +; + +/// Under the model, a `T`-access is ISA-valid iff its `size_of::()` bytes fit in +/// `0..(u16::MAX + 1)`. +pub broadcast axiom fn axiom_pio_model_access() + requires + obeys_pio_model::(), + ensures + forall|port: int| #[trigger] + valid_io_port_access::(port) <==> (0 <= port && port + size_of::() <= u16::MAX + + 1), +; -/// Whether an access of type `T` fits in the PIO byte range `0..u16::MAX`. -pub open spec fn valid_io_port_access(port: int) -> bool { - &&& valid_io_port_number(port) - &&& port + size_of::() <= u16::MAX as int +/// The trusted instances of the PIO model. +pub broadcast group group_io_port_models { + axiom_u8_pio_model, + axiom_u16_pio_model, + axiom_u32_pio_model, + axiom_pio_model_access, } /// Opaque specification boundary for the third-party read/write access marker. From 16058e2563f0937d77878a1dff8af450009a2081 Mon Sep 17 00:00:00 2001 From: Marsman1996 Date: Tue, 15 Sep 2026 16:53:29 +0800 Subject: [PATCH 16/22] refine: replace `obeys_pio_model` with `valid_io_port_access` in I/O port handling --- ostd/src/arch/x86/device/io_port.rs | 2 +- ostd/src/io/io_port/allocator.rs | 4 +-- ostd/src/io/io_port/mod.rs | 12 +++---- .../vstd_extra/src/external/io_port.rs | 34 +++++-------------- 4 files changed, 18 insertions(+), 34 deletions(-) diff --git a/ostd/src/arch/x86/device/io_port.rs b/ostd/src/arch/x86/device/io_port.rs index 4ab813494..c2d0399b6 100644 --- a/ostd/src/arch/x86/device/io_port.rs +++ b/ostd/src/arch/x86/device/io_port.rs @@ -1,6 +1,6 @@ // SPDX-License-Identifier: MPL-2.0 //! I/O port access. -pub use vstd_extra::external::{group_io_port_models, obeys_pio_model, valid_io_port_access}; +pub use vstd_extra::external::{group_io_port_models, valid_io_port_access}; pub use x86_64::{ instructions::port::{ diff --git a/ostd/src/io/io_port/allocator.rs b/ostd/src/io/io_port/allocator.rs index bf1aa787b..e7f859c67 100644 --- a/ostd/src/io/io_port/allocator.rs +++ b/ostd/src/io/io_port/allocator.rs @@ -1,5 +1,6 @@ // SPDX-License-Identifier: MPL-2.0 //! I/O port allocator. +use crate::arch::device::io_port::valid_io_port_access; use vstd::{ prelude::*, resource::set::{GhostSetAuth, GhostSubset}, @@ -14,7 +15,6 @@ use log::debug; use spin::Once; use super::{IoPort, lemma_port_id_set_contains, lemma_port_id_set_insert, port_id_set}; -use crate::arch::device::io_port::obeys_pio_model; use crate::{ io::RawIoPortRange, sync::{LocalIrqDisabled, SpinLock}, @@ -359,7 +359,7 @@ impl IoPortAllocator { requires size_of::() <= u16::MAX, is_overlapping ==> port as usize + size_of::() <= u16::MAX, - obeys_pio_model::(), + valid_io_port_access::(port), io_port_allocator_initialized(), (*old(claim_out))@ is None, ensures diff --git a/ostd/src/io/io_port/mod.rs b/ostd/src/io/io_port/mod.rs index fddbed460..71f753c97 100644 --- a/ostd/src/io/io_port/mod.rs +++ b/ostd/src/io/io_port/mod.rs @@ -3,7 +3,7 @@ use vstd::prelude::*; use crate::arch::device::io_port::{ - IoPortReadAccess, IoPortWriteAccess, PortRead, PortWrite, obeys_pio_model, valid_io_port_access, + IoPortReadAccess, IoPortWriteAccess, PortRead, PortWrite, valid_io_port_access, }; mod allocator; @@ -52,7 +52,7 @@ impl IoPort { /// The complete byte range occupied by this typed port lies in the x86 PIO address space. #[verifier::type_invariant] pub open spec fn well_formed(&self) -> bool { - valid_io_port_access::(self@ as int) + valid_io_port_access::(self@) } /// Whether the port was acquired as overlapping: it occupies only its first port. @@ -137,7 +137,7 @@ impl IoPort { requires size_of::() <= u16::MAX, port as usize + size_of::() <= u16::MAX, - obeys_pio_model::(), + valid_io_port_access::(port), allocator::io_port_allocator_initialized(), ensures result is Ok <== claim@ is Some, @@ -175,7 +175,7 @@ impl IoPort { requires size_of::() <= u16::MAX, port as usize + size_of::() <= u16::MAX, - obeys_pio_model::(), + valid_io_port_access::(port), allocator::io_port_allocator_initialized(), ensures result is Ok <== claim@ is Some, @@ -225,7 +225,7 @@ impl IoPort { requires size_of::() <= u16::MAX, port as usize + size_of::() <= u16::MAX, - obeys_pio_model::(), + valid_io_port_access::(port), ensures ret@ == port, !ret.is_overlapping(), @@ -249,7 +249,7 @@ impl IoPort { requires size_of::() <= u16::MAX, port as usize + size_of::() <= u16::MAX, - obeys_pio_model::(), + valid_io_port_access::(port), ensures ret@ == port, ret.is_overlapping() == is_overlapping, diff --git a/verified_libs/vstd_extra/src/external/io_port.rs b/verified_libs/vstd_extra/src/external/io_port.rs index 4180a4d31..d4ce66be8 100644 --- a/verified_libs/vstd_extra/src/external/io_port.rs +++ b/verified_libs/vstd_extra/src/external/io_port.rs @@ -14,39 +14,24 @@ verus! { /// Uninterpreted: `PortRead`/`PortWrite` are user-implementable, so meaning comes only from /// the trusted widths in [`group_io_port_models`]. ISA-level fact only — no claim about /// device decoding, access permission, or ownership. -pub uninterp spec fn valid_io_port_access(port: int) -> bool; - -/// Whether `T` is one of the trusted port widths; uninterpreted, admitted only by the axioms -/// below. -pub uninterp spec fn obeys_pio_model() -> bool; +pub uninterp spec fn valid_io_port_access(port: u16) -> bool; /// Trusted: `u8` ports are written and read via `outb`/`inb`. -pub broadcast axiom fn axiom_u8_pio_model() +pub broadcast axiom fn axiom_u8_pio_model(port: u16) ensures - #[trigger] obeys_pio_model::(), + #[trigger] valid_io_port_access::(port) <==> port + size_of::() <= u16::MAX + 1, ; /// Trusted: `u16` ports are written and read via `outw`/`inw`. -pub broadcast axiom fn axiom_u16_pio_model() +pub broadcast axiom fn axiom_u16_pio_model(port: u16) ensures - #[trigger] obeys_pio_model::(), + #[trigger] valid_io_port_access::(port) <==> port + size_of::() <= u16::MAX + 1, ; /// Trusted: `u32` ports are written and read via `outl`/`inl`. -pub broadcast axiom fn axiom_u32_pio_model() - ensures - #[trigger] obeys_pio_model::(), -; - -/// Under the model, a `T`-access is ISA-valid iff its `size_of::()` bytes fit in -/// `0..(u16::MAX + 1)`. -pub broadcast axiom fn axiom_pio_model_access() - requires - obeys_pio_model::(), +pub broadcast axiom fn axiom_u32_pio_model(port: u16) ensures - forall|port: int| #[trigger] - valid_io_port_access::(port) <==> (0 <= port && port + size_of::() <= u16::MAX - + 1), + #[trigger] valid_io_port_access::(port) <==> port + size_of::() <= u16::MAX + 1, ; /// The trusted instances of the PIO model. @@ -54,7 +39,6 @@ pub broadcast group group_io_port_models { axiom_u8_pio_model, axiom_u16_pio_model, axiom_u32_pio_model, - axiom_pio_model_access, } /// Opaque specification boundary for the third-party read/write access marker. @@ -75,7 +59,7 @@ pub trait ExPortRead { /// A port read can produce any value supplied by the device. unsafe fn read_from_port(port: u16) -> Self where Self: Sized requires - valid_io_port_access::(port as int), + valid_io_port_access::(port), ; } @@ -87,7 +71,7 @@ pub trait ExPortWrite { /// A port write has no modeled logical effect on kernel memory. unsafe fn write_to_port(port: u16, value: Self) where Self: Sized requires - valid_io_port_access::(port as int), + valid_io_port_access::(port), ; } From 662ee6f9e48fe1b46d535606a7e565739ed75637 Mon Sep 17 00:00:00 2001 From: Marsman1996 Date: Wed, 16 Sep 2026 13:01:19 +0800 Subject: [PATCH 17/22] chore: update with `OnceImpl` update --- ostd/src/io/io_mem/allocator.rs | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/ostd/src/io/io_mem/allocator.rs b/ostd/src/io/io_mem/allocator.rs index 3767c31ca..49222a054 100644 --- a/ostd/src/io/io_mem/allocator.rs +++ b/ostd/src/io/io_mem/allocator.rs @@ -1,9 +1,10 @@ // SPDX-License-Identifier: MPL-2.0 //! I/O Memory allocator. use crate::specs::arch::PAGE_SIZE; -use crate::sync::{OnceImpl, TrivialPred}; use vstd::{arithmetic::power2::is_pow2, prelude::*}; -use vstd_extra::resource::flags::OneShotSet; +use vstd_extra::{ + once::OnceImpl, resource::flags::OneShotSet, resource_invariant::TrivialResourceInvariant, +}; use alloc::vec::Vec; use core::ops::Range; @@ -325,11 +326,11 @@ pub open spec fn io_mem_range_registered(range: Range) -> bool { <= range.start && range.end <= registered_io_mem_windows()[m].end } -pub exec static IO_MEM_ALLOCATOR: OnceImpl +pub exec static IO_MEM_ALLOCATOR: OnceImpl ensures IO_MEM_ALLOCATOR.wf(), { - OnceImpl::new(Ghost(TrivialPred)) + OnceImpl::new(Ghost(TrivialResourceInvariant)) } } // verus! From 038fe48760666df618f467b90917c1fe7b5fc87a Mon Sep 17 00:00:00 2001 From: Marsman1996 Date: Wed, 16 Sep 2026 16:54:26 +0800 Subject: [PATCH 18/22] refine: carry PIO allocator's ghost token via the lock's ResourceInvariant --- ostd/src/io/io_port/allocator.rs | 273 +++++++++++++++++++------------ 1 file changed, 169 insertions(+), 104 deletions(-) diff --git a/ostd/src/io/io_port/allocator.rs b/ostd/src/io/io_port/allocator.rs index e7f859c67..3455d44a4 100644 --- a/ostd/src/io/io_port/allocator.rs +++ b/ostd/src/io/io_port/allocator.rs @@ -7,6 +7,7 @@ use vstd::{ tokens::InstanceId, }; use vstd_extra::ownership::Inv; +use vstd_extra::resource_invariant::ResourceInvariant; use core::ops::Range; @@ -173,7 +174,10 @@ pub(crate) proof fn lemma_alloc_specific_view( } } -/// Representation invariant of `IoPortAllocatorInner`. +/// Relation tying the ghost allocation authority (`IoPortAllocation`) to the executable bitmap. +/// +/// Used as the `ResourceInvariant` of the allocator's lock, so the lock maintains it across +/// lock/unlock instead of a separate bundling struct. pub(crate) open spec fn io_port_inner_inv_values( allocated_instance_id: InstanceId, allocated: Set, @@ -328,14 +332,21 @@ impl IoPortClaim { } } // verus! -/// Lock-protected executable bitmap and the state-machine token that models it. -#[verus_verify] -struct IoPortAllocatorInner { - allocator: ModeledIdAlloc, - #[cfg(verus_keep_ghost_body)] - tracked_allocated: Tracked, +verus! { + +ghost struct IoPortAllocInvariant; + +impl ResourceInvariant for IoPortAllocInvariant { + type Constant = (); + + type Resource = IoPortAllocation; + + closed spec fn inv(_constant: (), alloc: ModeledIdAlloc, r: IoPortAllocation) -> bool { + io_port_inner_inv_values(r.instance_id(), r.value(), &alloc.inner) + } } +} // verus! /// I/O port allocator that allocates port I/O access to device drivers. #[verus_verify] pub(super) struct IoPortAllocator { @@ -343,7 +354,11 @@ pub(super) struct IoPortAllocator { /// /// Instead of using `RangeAllocator` like `IoMemAllocator` does, it is more reasonable to use `IdAlloc`, /// as PIO space includes only a small region; for example, x86 module in OSTD allows just 65536 I/O ports. - allocator: SpinLock, + allocator: SpinLock< + /* Original Rust: IdAlloc */ ModeledIdAlloc, + LocalIrqDisabled, + IoPortAllocInvariant, + >, } #[verus_verify] @@ -380,39 +395,43 @@ impl IoPortAllocator { }; /* debug!("Try to acquire PIO range: {:#x?}", range); */ let mut allocator = self.allocator.lock(); - let allocator_inner = &mut *allocator; + proof_decl! { + let ghost instance_id = allocator.resource().instance_id(); + let ghost preserved = allocator.resource().value(); + } proof! { - lemma_io_port_alloc_init(&*allocator_inner); + assert(io_port_inner_inv_values(instance_id, preserved, &allocator.value().inner)); } + let allocator_inner = &mut *allocator; // `Iterator::any` with a capturing closure is not supported by Verus. // Original Rust: // if range.any(|i| allocator.is_allocated(i as usize)) { return None; } let mut already_allocated = false; #[verus_spec(scan_iter => invariant - allocator_inner.allocator.inner.inv(), - allocator_inner.allocator.inner@.len() + allocator_inner.inner.inv(), + allocator_inner.inner@.len() == crate::arch::io::MAX_IO_PORT as int, !already_allocated ==> forall|id: usize| range.start as usize <= id < (range.start as int + scan_iter.index()) as usize ==> - !id_alloc_view(&allocator_inner.allocator.inner).contains(id), + !id_alloc_view(&allocator_inner.inner).contains(id), )] for i in range.clone() { proof! { - assert((i as usize) < allocator_inner.allocator.inner@.len()) by { + assert((i as usize) < allocator_inner.inner@.len()) by { assert((i as usize) < range.end as usize); assert((range.end as usize) <= u16::MAX as usize); assert((u16::MAX as usize) <= crate::arch::io::MAX_IO_PORT as usize); - assert(allocator_inner.allocator.inner@.len() + assert(allocator_inner.inner@.len() == crate::arch::io::MAX_IO_PORT as int); } } - if allocator_inner.allocator.inner.is_allocated(i as usize) { + if allocator_inner.inner.is_allocated(i as usize) { already_allocated = true; } proof! { - lemma_id_alloc_view_contains(&allocator_inner.allocator.inner, i as usize); + lemma_id_alloc_view_contains(&allocator_inner.inner, i as usize); } } proof_decl! { @@ -428,12 +447,12 @@ impl IoPortAllocator { proof_decl! { let ghost ids = port_id_set(range.start as usize, range.end as usize); - let ghost allocation_start_view = id_alloc_view(&allocator_inner.allocator.inner); + let ghost allocation_start_view = id_alloc_view(&allocator_inner.inner); } proof! { - assert(ids.disjoint(id_alloc_view(&allocator_inner.allocator.inner))) by { + assert(ids.disjoint(id_alloc_view(&allocator_inner.inner))) by { assert forall|id: usize| #[trigger] ids.contains(id) implies - !id_alloc_view(&allocator_inner.allocator.inner).contains(id) by { + !id_alloc_view(&allocator_inner.inner).contains(id) by { lemma_port_id_set_contains( range.start as usize, range.end as usize, @@ -442,7 +461,7 @@ impl IoPortAllocator { } } assert forall|id: usize| ids.contains(id) implies - id < id_alloc_capacity(&allocator_inner.allocator.inner) by { + id < id_alloc_capacity(&allocator_inner.inner) by { lemma_port_id_set_contains( range.start as usize, range.end as usize, @@ -451,7 +470,7 @@ impl IoPortAllocator { } assert forall|id: usize| range.start as usize <= id < range.end as usize implies - !id_alloc_view(&allocator_inner.allocator.inner).contains(id) by { + !id_alloc_view(&allocator_inner.inner).contains(id) by { lemma_port_id_set_contains( range.start as usize, range.end as usize, @@ -461,19 +480,16 @@ impl IoPortAllocator { } #[verus_spec(allocation_iter => invariant - allocator_inner.allocator.inner.inv(), - allocator_inner.allocator.inner@.len() + allocator_inner.inner.inv(), + allocator_inner.inner@.len() == crate::arch::io::MAX_IO_PORT as int, - range.end as usize <= id_alloc_capacity(&allocator_inner.allocator.inner), - allocator_inner.tracked_allocated@.instance_id() == - io_port_allocator_instance_id(), - allocator_inner.tracked_allocated@.value().subset_of(allocation_start_view), - allocator_inner.tracked_allocated@.value().subset_of( - id_alloc_view(&allocator_inner.allocator.inner), - ), - id_alloc_capacity(&allocator_inner.allocator.inner) == + range.end as usize <= id_alloc_capacity(&allocator_inner.inner), + instance_id == io_port_allocator_instance_id(), + preserved.subset_of(allocation_start_view), + preserved.subset_of(id_alloc_view(&allocator_inner.inner)), + id_alloc_capacity(&allocator_inner.inner) == crate::arch::io::MAX_IO_PORT as usize, - id_alloc_view(&allocator_inner.allocator.inner) == + id_alloc_view(&allocator_inner.inner) == allocation_start_view.union( port_id_set( range.start as usize, @@ -483,55 +499,60 @@ impl IoPortAllocator { forall|id: usize| (range.start as int + allocation_iter.index()) as usize <= id < range.end as usize ==> - !id_alloc_view(&allocator_inner.allocator.inner).contains(id), + !id_alloc_view(&allocator_inner.inner).contains(id), )] for i in range.clone() { proof_decl! { - let ghost old_view = id_alloc_view(&allocator_inner.allocator.inner); + let ghost old_view = id_alloc_view(&allocator_inner.inner); } proof! { assert((i as usize) == (range.start as int + allocation_iter.index()) as usize); - assert((i as usize) < id_alloc_capacity(&allocator_inner.allocator.inner)); - assert(!id_alloc_view(&allocator_inner.allocator.inner).contains(i as usize)); - assert(allocator_inner.tracked_allocated@.value().subset_of( - old_view.insert(i as usize), - )) by { + assert((i as usize) < id_alloc_capacity(&allocator_inner.inner)); + assert(!id_alloc_view(&allocator_inner.inner).contains(i as usize)); + assert(preserved.subset_of(old_view.insert(i as usize))) by { assert forall|id: usize| - allocator_inner.tracked_allocated@.value().contains(id) implies + preserved.contains(id) implies old_view.insert(i as usize).contains(id) by { } } - assert(io_port_inner_inv_values( - allocator_inner.tracked_allocated@.instance_id(), - allocator_inner.tracked_allocated@.value(), - &allocator_inner.allocator.inner, - )); + assert(io_port_inner_inv_values(instance_id, preserved, &allocator_inner.inner)); } #[verus_spec(with - Ghost(allocator_inner.tracked_allocated@.instance_id()), - Ghost(allocator_inner.tracked_allocated@.value()), + Ghost(instance_id), + Ghost(preserved), )] /* Original Rust: allocator.alloc_specific(i as usize); */ - let _ = allocator_inner.allocator.alloc_specific(i as usize); + let _ = allocator_inner.alloc_specific(i as usize); proof! { lemma_port_id_set_insert(range.start as usize, i as usize); - assert(id_alloc_view(&allocator_inner.allocator.inner) == + assert(id_alloc_view(&allocator_inner.inner) == old_view.insert(i as usize)); } } proof! { - assert(ids.disjoint(allocator_inner.tracked_allocated@.value())) by { + assert(ids.disjoint(preserved)) by { assert forall|id: usize| #[trigger] ids.contains(id) implies - !allocator_inner.tracked_allocated@.value().contains(id) by { + !preserved.contains(id) by { } } - range_claim = allocator_inner.tracked_allocated.borrow_mut().allocate(ids); + assert(preserved.disjoint(ids)); + range_claim = allocator.tracked_borrow_mut_resource().allocate(ids); } // SAFETY: The created `IoPort` is guaranteed not to access system device I/O. /* Original Rust: unsafe { Some(IoPort::new_overlapping(port, is_overlapping)) } */ let result = unsafe { Some(IoPort::new_overlapping(port, is_overlapping)) }; + proof! { + assert(id_alloc_view(&allocator.value().inner) == allocation_start_view.union(ids)); + assert(preserved.subset_of(allocation_start_view)); + assert(allocator.resource().value() == preserved.union(ids)); + assert(io_port_inner_inv_values( + allocator.resource().instance_id(), + allocator.resource().value(), + &allocator.value().inner, + )); + } allocator.drop(); proof! { *claim_out = Tracked(Some(range_claim)); @@ -562,26 +583,49 @@ impl IoPortAllocator { */ let mut allocator = self.allocator.lock(); - let allocator_inner = &mut *allocator; + proof_decl! { + let ghost instance_id: InstanceId; + let ghost preserved: Set; + let ghost bitmap_view: Set; + let ghost token_released: Set; + let ghost pre_seq: Seq; + let ghost pre_len: int; + } proof! { - lemma_io_port_alloc_init(&*allocator_inner); assert(range.start as usize <= range.end as usize); - assert(claim.instance_id() == allocator_inner.tracked_allocated@.instance_id()); - allocator_inner.tracked_allocated.borrow().claim_includes(&claim); - assert(port_id_set(range.start as usize, range.end as usize) - <= allocator_inner.tracked_allocated@.value()); - assert(port_id_set(range.start as usize, range.end as usize) - <= id_alloc_view(&allocator_inner.allocator.inner)); - assert((range.end as usize) <= allocator_inner.allocator.inner@.len()) by { + instance_id = allocator.resource().instance_id(); + preserved = allocator.resource().value(); + pre_seq = allocator.value().inner@; + pre_len = allocator.value().inner@.len() as int; + bitmap_view = id_alloc_view(&allocator.value().inner); + assert(io_port_inner_inv_values(instance_id, preserved, &allocator.value().inner)); + assert(preserved.subset_of(bitmap_view)); + assert(bitmap_view == id_alloc_bits(pre_seq, pre_len)); + assert(pre_len == crate::arch::io::MAX_IO_PORT as int); + assert(crate::arch::io::MAX_IO_PORT as int <= usize::MAX as int); + assert(pre_len <= usize::MAX as int); + assert(claim.instance_id() == instance_id); + assert((range.end as usize) <= allocator.value().inner@.len()) by { assert((range.end as usize) <= u16::MAX as usize); assert((u16::MAX as usize) <= crate::arch::io::MAX_IO_PORT as usize); - assert(allocator_inner.allocator.inner@.len() + assert(allocator.value().inner@.len() == crate::arch::io::MAX_IO_PORT as int); } - allocator_inner.tracked_allocated.borrow_mut().release(claim); + } + proof! { + let tracked r = allocator.tracked_borrow_mut_resource(); + r.claim_includes(&claim); + assert(port_id_set(range.start as usize, range.end as usize) <= r.value()); + assert(r.value() == preserved); + assert(port_id_set(range.start as usize, range.end as usize) <= preserved); + r.release(claim); + token_released = r.value(); + assert(token_released + == preserved.difference(port_id_set(range.start as usize, range.end as usize))); assert forall|id: usize| - #[trigger] allocator_inner.tracked_allocated@.value().contains(id) implies { - &&& id_alloc_view(&allocator_inner.allocator.inner).contains(id) + #![trigger token_released.contains(id)] + token_released.contains(id) implies { + &&& bitmap_view.contains(id) &&& !(range.start as usize <= id < range.end as usize) } by { lemma_port_id_set_contains( @@ -590,32 +634,73 @@ impl IoPortAllocator { id, ); } + } + let allocator_inner = &mut *allocator; + /* Original Rust: + self.allocator + .lock() + .free_consecutive(range.start as usize..range.end as usize); + */ + proof! { + assert(allocator_inner.inner@.len() == crate::arch::io::MAX_IO_PORT as int); + assert(id_alloc_capacity(&allocator_inner.inner) + == crate::arch::io::MAX_IO_PORT as usize); + assert(allocator_inner.inner@ == pre_seq); + assert((range.end as usize) <= id_alloc_capacity(&allocator_inner.inner)); + assert(io_port_inner_inv_values(instance_id, preserved, &allocator_inner.inner)); + assert(id_alloc_view(&allocator_inner.inner) == bitmap_view); assert forall|i: int| range.start as usize <= i - && i < allocator_inner.allocator.inner@.len() + && i < allocator_inner.inner@.len() && i < range.end as usize implies - allocator_inner.allocator.inner@[i] + allocator_inner.inner@[i] by { - assert(0 <= i); - assert(i < allocator_inner.allocator.inner@.len()); - assert(allocator_inner.allocator.inner@.len() <= usize::MAX as int); - assert(i <= usize::MAX as int); - assert((i as usize) as int == i); + assert(port_id_set(range.start as usize, range.end as usize) <= preserved); + assert(preserved.subset_of(bitmap_view)); + assert(bitmap_view == id_alloc_view(&allocator_inner.inner)); lemma_port_id_set_contains( range.start as usize, range.end as usize, i as usize, ); - assert(port_id_set(range.start as usize, range.end as usize).contains(i as usize)); - assert(id_alloc_view(&allocator_inner.allocator.inner).contains(i as usize)); - lemma_id_alloc_view_contains(&allocator_inner.allocator.inner, i as usize); - assert(allocator_inner.allocator.inner@[i]); + lemma_id_alloc_view_contains(&allocator_inner.inner, i as usize); } } allocator_inner - .allocator .inner .free_consecutive(range.start as usize..range.end as usize); + proof! { + assert(allocator.value().inner == allocator_inner.inner); + let final_llen: int = allocator_inner.inner@.len() as int; + assert(final_llen == pre_len); + assert(final_llen <= usize::MAX as int); + assert forall|id: usize| + #![trigger allocator.resource().value().contains(id)] + allocator.resource().value().contains(id) implies + id_alloc_view(&allocator_inner.inner).contains(id) by { + lemma_port_id_set_contains(range.start as usize, range.end as usize, id); + lemma_id_alloc_bits_char(pre_seq, pre_len, id); + lemma_id_alloc_bits_char(allocator_inner.inner@, final_llen, id); + assert(allocator.resource().value().contains(id) + == (preserved.contains(id) + && !port_id_set(range.start as usize, range.end as usize).contains(id))); + assert(port_id_set(range.start as usize, range.end as usize) <= preserved); + assert(preserved.subset_of(bitmap_view)); + assert(bitmap_view == id_alloc_bits(pre_seq, pre_len)); + assert(id_alloc_view(&allocator_inner.inner) + == id_alloc_bits(allocator_inner.inner@, final_llen)); + } + assert(allocator_inner.inner.inv()); + assert(allocator_inner.inner@.len() == crate::arch::io::MAX_IO_PORT as int); + assert(id_alloc_capacity(&allocator_inner.inner) + == crate::arch::io::MAX_IO_PORT as usize); + assert(allocator.resource().instance_id() == instance_id); + assert(io_port_inner_inv_values( + allocator.resource().instance_id(), + allocator.resource().value(), + &allocator_inner.inner, + )); + } allocator.drop(); } } @@ -628,20 +713,6 @@ verus! { /// explicit specification boundary for the architecture's guarantee that [`init`] ran first. pub uninterp spec fn io_port_allocator_initialized() -> bool; -/// Trusted: once `init` has run, the global allocator's inner satisfies its invariant. -#[verifier::external_body] -proof fn lemma_io_port_alloc_init(inner: &IoPortAllocatorInner) - requires - io_port_allocator_initialized(), - ensures - io_port_inner_inv_values( - inner.tracked_allocated@.instance_id(), - inner.tracked_allocated@.value(), - &inner.allocator.inner, - ), -{ -} - } // verus! pub(super) static IO_PORT_ALLOCATOR: Once = Once::new(); @@ -689,17 +760,11 @@ pub(in crate::io) unsafe fn init() { IO_PORT_ALLOCATOR.call_once(|| IoPortAllocator { allocator: SpinLock::new(allocator), }); */ - IO_PORT_ALLOCATOR.call_once(|| { - proof_decl! { - let tracked allocated = IoPortAllocation::initialize(); - } - let inner = IoPortAllocatorInner { - allocator: ModeledIdAlloc { inner: allocator }, - #[cfg(verus_keep_ghost_body)] - tracked_allocated: Tracked::new(allocated), - }; - IoPortAllocator { - allocator: SpinLock::new(inner, Ghost::new(()), Tracked::new(())), - } + IO_PORT_ALLOCATOR.call_once(|| IoPortAllocator { + allocator: SpinLock::new( + ModeledIdAlloc { inner: allocator }, + Ghost::new(()), + Tracked::new(IoPortAllocation::initialize()), + ), }); } From afdbf4462206f4eba236a88eaf947ca612298b82 Mon Sep 17 00:00:00 2001 From: Marsman1996 Date: Wed, 16 Sep 2026 17:55:55 +0800 Subject: [PATCH 19/22] refine: remove modeled id alloc wrapper --- ostd/src/io/io_port/allocator.rs | 287 +++++++++---------------------- 1 file changed, 85 insertions(+), 202 deletions(-) diff --git a/ostd/src/io/io_port/allocator.rs b/ostd/src/io/io_port/allocator.rs index 3455d44a4..c73d67ace 100644 --- a/ostd/src/io/io_port/allocator.rs +++ b/ostd/src/io/io_port/allocator.rs @@ -102,82 +102,6 @@ pub(crate) proof fn lemma_id_alloc_view_contains(allocator: &IdAlloc, id: usize) lemma_id_alloc_bits_char(allocator@, allocator@.len() as int, id); } -/// Derives the set-level postcondition of `alloc_specific` from its bitmap postcondition. -pub(crate) proof fn lemma_alloc_specific_view( - old_a: &IdAlloc, - final_a: &IdAlloc, - id: usize, - res: Option, -) - requires - old_a.inv(), - final_a.inv(), - (id as int) < old_a@.len(), - old_a@.len() <= usize::MAX as int, - final_a@.len() == old_a@.len(), - res is None ==> old_a@[id as int] && final_a@ == old_a@, - res is Some ==> final_a@ == old_a@.update(id as int, true) && !old_a@[id as int], - res is Some ==> res == Some(id), - ensures - id_alloc_view(final_a) == id_alloc_view(old_a).insert(id), - id_alloc_view(old_a).subset_of(id_alloc_view(final_a)), - id_alloc_view(old_a).contains(id) ==> res is None, - !id_alloc_view(old_a).contains(id) ==> res == Some(id), -{ - let old_len: int = old_a@.len() as int; - assert forall|j: usize| - #![trigger id_alloc_view(final_a).contains(j)] - id_alloc_view(final_a).contains(j) == (id_alloc_view(old_a).insert(id)).contains(j) by { - lemma_id_alloc_bits_char(old_a@, old_len, j); - lemma_id_alloc_bits_char(final_a@, final_a@.len() as int, j); - if res is Some { - assert forall|jj: int| - #![trigger final_a@[jj]] - final_a@[jj] == (if jj == id as int { - true - } else { - old_a@[jj] - }) by { - assert(final_a@ == old_a@.update(id as int, true)); - } - } else { - assert(final_a@ == old_a@); - assert(old_a@[id as int]); - } - } - assert forall|j: usize| - #![trigger id_alloc_view(old_a).contains(j)] - id_alloc_view(old_a).contains(j) implies id_alloc_view(final_a).contains(j) by { - lemma_id_alloc_bits_char(old_a@, old_len, j); - lemma_id_alloc_bits_char(final_a@, final_a@.len() as int, j); - if res is Some { - assert forall|jj: int| - #![trigger final_a@[jj]] - final_a@[jj] == (if jj == id as int { - true - } else { - old_a@[jj] - }) by { - assert(final_a@ == old_a@.update(id as int, true)); - } - } else { - assert(final_a@ == old_a@); - } - } - lemma_id_alloc_bits_char(old_a@, old_len, id); - assert(id_alloc_view(old_a).contains(id) == old_a@[id as int]); - if res is Some { - assert(!old_a@[id as int]); - assert(res == Some(id)); - } else { - assert(old_a@[id as int]); - } -} - -/// Relation tying the ghost allocation authority (`IoPortAllocation`) to the executable bitmap. -/// -/// Used as the `ResourceInvariant` of the allocator's lock, so the lock maintains it across -/// lock/unlock instead of a separate bundling struct. pub(crate) open spec fn io_port_inner_inv_values( allocated_instance_id: InstanceId, allocated: Set, @@ -191,60 +115,6 @@ pub(crate) open spec fn io_port_inner_inv_values( } } // verus! -/// Transparent facade used only to pass ghost frame facts to the third-party mutation. -#[repr(transparent)] -#[verus_verify] -struct ModeledIdAlloc { - inner: IdAlloc, -} - -#[verus_verify] -impl ModeledIdAlloc { - #[verus_spec(result => - with - Ghost(allocated_instance_id): Ghost, - Ghost(preserved): Ghost>, - requires - id < id_alloc_capacity(&old(self).inner), - io_port_inner_inv_values(allocated_instance_id, preserved, &old(self).inner), - ensures - final(self).inner.inv(), - final(self).inner@.len() == crate::arch::io::MAX_IO_PORT as int, - id_alloc_capacity(&final(self).inner) == id_alloc_capacity(&old(self).inner), - id_alloc_view(&final(self).inner) == id_alloc_view(&old(self).inner).insert(id), - id_alloc_view(&old(self).inner).subset_of(id_alloc_view(&final(self).inner)), - preserved.subset_of(id_alloc_view(&final(self).inner)), - io_port_inner_inv_values( - allocated_instance_id, - preserved, - &final(self).inner, - ), - id_alloc_view(&old(self).inner).contains(id) ==> result is None, - !id_alloc_view(&old(self).inner).contains(id) ==> result == Some(id), - )] - fn alloc_specific(&mut self, id: usize) -> Option { - proof! { - assert(id < id_alloc_capacity(&old(self).inner)); - assert(id_alloc_capacity(&old(self).inner) - == crate::arch::io::MAX_IO_PORT as usize); - assert(old(self).inner@.len() == crate::arch::io::MAX_IO_PORT as int); - assert((id as int) < old(self).inner@.len()); - } - let res = self.inner.alloc_specific(id); - proof! { - assert(self.inner@.len() == old(self).inner@.len()); - assert(self.inner@.len() == crate::arch::io::MAX_IO_PORT as int); - assert(self.inner.inv()); - assert(old(self).inner@.len() <= usize::MAX as int); - lemma_alloc_specific_view(&old(self).inner, &self.inner, id, res); - assert(id_alloc_capacity(&self.inner) == id_alloc_capacity(&old(self).inner)); - assert(preserved.subset_of(id_alloc_view(&self.inner))); - assert(io_port_inner_inv_values(allocated_instance_id, preserved, &self.inner)); - } - res - } -} - verus! { /// Authority over the set of PIO ids currently allocated by the global allocator. @@ -336,13 +206,13 @@ verus! { ghost struct IoPortAllocInvariant; -impl ResourceInvariant for IoPortAllocInvariant { +impl ResourceInvariant for IoPortAllocInvariant { type Constant = (); type Resource = IoPortAllocation; - closed spec fn inv(_constant: (), alloc: ModeledIdAlloc, r: IoPortAllocation) -> bool { - io_port_inner_inv_values(r.instance_id(), r.value(), &alloc.inner) + closed spec fn inv(_constant: (), alloc: IdAlloc, r: IoPortAllocation) -> bool { + io_port_inner_inv_values(r.instance_id(), r.value(), &alloc) } } @@ -354,11 +224,7 @@ pub(super) struct IoPortAllocator { /// /// Instead of using `RangeAllocator` like `IoMemAllocator` does, it is more reasonable to use `IdAlloc`, /// as PIO space includes only a small region; for example, x86 module in OSTD allows just 65536 I/O ports. - allocator: SpinLock< - /* Original Rust: IdAlloc */ ModeledIdAlloc, - LocalIrqDisabled, - IoPortAllocInvariant, - >, + allocator: SpinLock, } #[verus_verify] @@ -400,7 +266,7 @@ impl IoPortAllocator { let ghost preserved = allocator.resource().value(); } proof! { - assert(io_port_inner_inv_values(instance_id, preserved, &allocator.value().inner)); + assert(io_port_inner_inv_values(instance_id, preserved, &allocator.value())); } let allocator_inner = &mut *allocator; // `Iterator::any` with a capturing closure is not supported by Verus. @@ -409,29 +275,29 @@ impl IoPortAllocator { let mut already_allocated = false; #[verus_spec(scan_iter => invariant - allocator_inner.inner.inv(), - allocator_inner.inner@.len() + allocator_inner.inv(), + allocator_inner@.len() == crate::arch::io::MAX_IO_PORT as int, !already_allocated ==> forall|id: usize| range.start as usize <= id < (range.start as int + scan_iter.index()) as usize ==> - !id_alloc_view(&allocator_inner.inner).contains(id), + !id_alloc_view(&allocator_inner).contains(id), )] for i in range.clone() { proof! { - assert((i as usize) < allocator_inner.inner@.len()) by { + assert((i as usize) < allocator_inner@.len()) by { assert((i as usize) < range.end as usize); assert((range.end as usize) <= u16::MAX as usize); assert((u16::MAX as usize) <= crate::arch::io::MAX_IO_PORT as usize); - assert(allocator_inner.inner@.len() + assert(allocator_inner@.len() == crate::arch::io::MAX_IO_PORT as int); } } - if allocator_inner.inner.is_allocated(i as usize) { + if allocator_inner.is_allocated(i as usize) { already_allocated = true; } proof! { - lemma_id_alloc_view_contains(&allocator_inner.inner, i as usize); + lemma_id_alloc_view_contains(&allocator_inner, i as usize); } } proof_decl! { @@ -447,12 +313,12 @@ impl IoPortAllocator { proof_decl! { let ghost ids = port_id_set(range.start as usize, range.end as usize); - let ghost allocation_start_view = id_alloc_view(&allocator_inner.inner); + let ghost allocation_start_view = id_alloc_view(&allocator_inner); } proof! { - assert(ids.disjoint(id_alloc_view(&allocator_inner.inner))) by { + assert(ids.disjoint(id_alloc_view(&allocator_inner))) by { assert forall|id: usize| #[trigger] ids.contains(id) implies - !id_alloc_view(&allocator_inner.inner).contains(id) by { + !id_alloc_view(&allocator_inner).contains(id) by { lemma_port_id_set_contains( range.start as usize, range.end as usize, @@ -461,7 +327,7 @@ impl IoPortAllocator { } } assert forall|id: usize| ids.contains(id) implies - id < id_alloc_capacity(&allocator_inner.inner) by { + id < id_alloc_capacity(&allocator_inner) by { lemma_port_id_set_contains( range.start as usize, range.end as usize, @@ -470,7 +336,7 @@ impl IoPortAllocator { } assert forall|id: usize| range.start as usize <= id < range.end as usize implies - !id_alloc_view(&allocator_inner.inner).contains(id) by { + !id_alloc_view(&allocator_inner).contains(id) by { lemma_port_id_set_contains( range.start as usize, range.end as usize, @@ -480,16 +346,16 @@ impl IoPortAllocator { } #[verus_spec(allocation_iter => invariant - allocator_inner.inner.inv(), - allocator_inner.inner@.len() + allocator_inner.inv(), + allocator_inner@.len() == crate::arch::io::MAX_IO_PORT as int, - range.end as usize <= id_alloc_capacity(&allocator_inner.inner), + range.end as usize <= id_alloc_capacity(&allocator_inner), instance_id == io_port_allocator_instance_id(), preserved.subset_of(allocation_start_view), - preserved.subset_of(id_alloc_view(&allocator_inner.inner)), - id_alloc_capacity(&allocator_inner.inner) == + preserved.subset_of(id_alloc_view(&allocator_inner)), + id_alloc_capacity(&allocator_inner) == crate::arch::io::MAX_IO_PORT as usize, - id_alloc_view(&allocator_inner.inner) == + id_alloc_view(&allocator_inner) == allocation_start_view.union( port_id_set( range.start as usize, @@ -499,35 +365,54 @@ impl IoPortAllocator { forall|id: usize| (range.start as int + allocation_iter.index()) as usize <= id < range.end as usize ==> - !id_alloc_view(&allocator_inner.inner).contains(id), + !id_alloc_view(&allocator_inner).contains(id), )] for i in range.clone() { proof_decl! { - let ghost old_view = id_alloc_view(&allocator_inner.inner); + let ghost old_view = id_alloc_view(&allocator_inner); + let ghost old_seq = allocator_inner@; + let ghost old_len = (allocator_inner@.len()) as int; } proof! { assert((i as usize) == (range.start as int + allocation_iter.index()) as usize); - assert((i as usize) < id_alloc_capacity(&allocator_inner.inner)); - assert(!id_alloc_view(&allocator_inner.inner).contains(i as usize)); + assert((i as usize) < id_alloc_capacity(&allocator_inner)); + assert(allocator_inner.inv()); + assert(!id_alloc_view(&allocator_inner).contains(i as usize)); assert(preserved.subset_of(old_view.insert(i as usize))) by { assert forall|id: usize| preserved.contains(id) implies old_view.insert(i as usize).contains(id) by { } } - assert(io_port_inner_inv_values(instance_id, preserved, &allocator_inner.inner)); } - #[verus_spec(with - Ghost(instance_id), - Ghost(preserved), - )] /* Original Rust: allocator.alloc_specific(i as usize); */ - let _ = allocator_inner.alloc_specific(i as usize); + let _res = allocator_inner.alloc_specific(i as usize); proof! { - lemma_port_id_set_insert(range.start as usize, i as usize); - assert(id_alloc_view(&allocator_inner.inner) == - old_view.insert(i as usize)); + assert((allocator_inner@.len()) as int == old_len); + assert(id_alloc_view(&allocator_inner) == old_view.insert(i as usize)) by { + lemma_port_id_set_insert(range.start as usize, i as usize); + assert forall|j: usize| + #![trigger id_alloc_view(&allocator_inner).contains(j)] + id_alloc_view(&allocator_inner).contains(j) + == old_view.insert(i as usize).contains(j) by { + lemma_id_alloc_bits_char(old_seq, old_len, j); + lemma_id_alloc_bits_char(allocator_inner@, old_len, j); + if _res is Some { + assert(allocator_inner@ == old_seq.update(i as int, true)); + assert(allocator_inner@[j as int] == (if (j as int) == (i as int) { + true + } else { + old_seq[j as int] + })); + } else { + assert(old_seq[i as int]); + assert(allocator_inner@ == old_seq); + } + } + } + assert(preserved.subset_of(id_alloc_view(&allocator_inner))); + assert(io_port_inner_inv_values(instance_id, preserved, &allocator_inner)); } } proof! { @@ -544,13 +429,13 @@ impl IoPortAllocator { /* Original Rust: unsafe { Some(IoPort::new_overlapping(port, is_overlapping)) } */ let result = unsafe { Some(IoPort::new_overlapping(port, is_overlapping)) }; proof! { - assert(id_alloc_view(&allocator.value().inner) == allocation_start_view.union(ids)); + assert(id_alloc_view(&allocator.value()) == allocation_start_view.union(ids)); assert(preserved.subset_of(allocation_start_view)); assert(allocator.resource().value() == preserved.union(ids)); assert(io_port_inner_inv_values( allocator.resource().instance_id(), allocator.resource().value(), - &allocator.value().inner, + &allocator.value(), )); } allocator.drop(); @@ -595,20 +480,20 @@ impl IoPortAllocator { assert(range.start as usize <= range.end as usize); instance_id = allocator.resource().instance_id(); preserved = allocator.resource().value(); - pre_seq = allocator.value().inner@; - pre_len = allocator.value().inner@.len() as int; - bitmap_view = id_alloc_view(&allocator.value().inner); - assert(io_port_inner_inv_values(instance_id, preserved, &allocator.value().inner)); + pre_seq = allocator.value()@; + pre_len = allocator.value()@.len() as int; + bitmap_view = id_alloc_view(&allocator.value()); + assert(io_port_inner_inv_values(instance_id, preserved, &allocator.value())); assert(preserved.subset_of(bitmap_view)); assert(bitmap_view == id_alloc_bits(pre_seq, pre_len)); assert(pre_len == crate::arch::io::MAX_IO_PORT as int); assert(crate::arch::io::MAX_IO_PORT as int <= usize::MAX as int); assert(pre_len <= usize::MAX as int); assert(claim.instance_id() == instance_id); - assert((range.end as usize) <= allocator.value().inner@.len()) by { + assert((range.end as usize) <= allocator.value()@.len()) by { assert((range.end as usize) <= u16::MAX as usize); assert((u16::MAX as usize) <= crate::arch::io::MAX_IO_PORT as usize); - assert(allocator.value().inner@.len() + assert(allocator.value()@.len() == crate::arch::io::MAX_IO_PORT as int); } } @@ -642,63 +527,61 @@ impl IoPortAllocator { .free_consecutive(range.start as usize..range.end as usize); */ proof! { - assert(allocator_inner.inner@.len() == crate::arch::io::MAX_IO_PORT as int); - assert(id_alloc_capacity(&allocator_inner.inner) + assert(allocator_inner@.len() == crate::arch::io::MAX_IO_PORT as int); + assert(id_alloc_capacity(&allocator_inner) == crate::arch::io::MAX_IO_PORT as usize); - assert(allocator_inner.inner@ == pre_seq); - assert((range.end as usize) <= id_alloc_capacity(&allocator_inner.inner)); - assert(io_port_inner_inv_values(instance_id, preserved, &allocator_inner.inner)); - assert(id_alloc_view(&allocator_inner.inner) == bitmap_view); + assert(allocator_inner@ == pre_seq); + assert((range.end as usize) <= id_alloc_capacity(&allocator_inner)); + assert(io_port_inner_inv_values(instance_id, preserved, &allocator_inner)); + assert(id_alloc_view(&allocator_inner) == bitmap_view); assert forall|i: int| range.start as usize <= i - && i < allocator_inner.inner@.len() + && i < allocator_inner@.len() && i < range.end as usize implies - allocator_inner.inner@[i] + allocator_inner@[i] by { assert(port_id_set(range.start as usize, range.end as usize) <= preserved); assert(preserved.subset_of(bitmap_view)); - assert(bitmap_view == id_alloc_view(&allocator_inner.inner)); + assert(bitmap_view == id_alloc_view(&allocator_inner)); lemma_port_id_set_contains( range.start as usize, range.end as usize, i as usize, ); - lemma_id_alloc_view_contains(&allocator_inner.inner, i as usize); + lemma_id_alloc_view_contains(&allocator_inner, i as usize); } } - allocator_inner - .inner - .free_consecutive(range.start as usize..range.end as usize); + allocator_inner.free_consecutive(range.start as usize..range.end as usize); proof! { - assert(allocator.value().inner == allocator_inner.inner); - let final_llen: int = allocator_inner.inner@.len() as int; + assert(allocator.value() == *allocator_inner); + let final_llen: int = allocator_inner@.len() as int; assert(final_llen == pre_len); assert(final_llen <= usize::MAX as int); assert forall|id: usize| #![trigger allocator.resource().value().contains(id)] allocator.resource().value().contains(id) implies - id_alloc_view(&allocator_inner.inner).contains(id) by { + id_alloc_view(&allocator_inner).contains(id) by { lemma_port_id_set_contains(range.start as usize, range.end as usize, id); lemma_id_alloc_bits_char(pre_seq, pre_len, id); - lemma_id_alloc_bits_char(allocator_inner.inner@, final_llen, id); + lemma_id_alloc_bits_char(allocator_inner@, final_llen, id); assert(allocator.resource().value().contains(id) == (preserved.contains(id) && !port_id_set(range.start as usize, range.end as usize).contains(id))); assert(port_id_set(range.start as usize, range.end as usize) <= preserved); assert(preserved.subset_of(bitmap_view)); assert(bitmap_view == id_alloc_bits(pre_seq, pre_len)); - assert(id_alloc_view(&allocator_inner.inner) - == id_alloc_bits(allocator_inner.inner@, final_llen)); + assert(id_alloc_view(&allocator_inner) + == id_alloc_bits(allocator_inner@, final_llen)); } - assert(allocator_inner.inner.inv()); - assert(allocator_inner.inner@.len() == crate::arch::io::MAX_IO_PORT as int); - assert(id_alloc_capacity(&allocator_inner.inner) + assert(allocator_inner.inv()); + assert(allocator_inner@.len() == crate::arch::io::MAX_IO_PORT as int); + assert(id_alloc_capacity(&allocator_inner) == crate::arch::io::MAX_IO_PORT as usize); assert(allocator.resource().instance_id() == instance_id); assert(io_port_inner_inv_values( allocator.resource().instance_id(), allocator.resource().value(), - &allocator_inner.inner, + &allocator_inner, )); } allocator.drop(); @@ -762,7 +645,7 @@ pub(in crate::io) unsafe fn init() { }); */ IO_PORT_ALLOCATOR.call_once(|| IoPortAllocator { allocator: SpinLock::new( - ModeledIdAlloc { inner: allocator }, + allocator, Ghost::new(()), Tracked::new(IoPortAllocation::initialize()), ), From 4f8df107b80f2bad608c9be03c50ed539ccfa8c4 Mon Sep 17 00:00:00 2001 From: Marsman1996 Date: Wed, 16 Sep 2026 22:04:49 +0800 Subject: [PATCH 20/22] refine --- verified_libs/vstd_extra/src/external/int_specs.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/verified_libs/vstd_extra/src/external/int_specs.rs b/verified_libs/vstd_extra/src/external/int_specs.rs index a840d2cb5..239a7919a 100644 --- a/verified_libs/vstd_extra/src/external/int_specs.rs +++ b/verified_libs/vstd_extra/src/external/int_specs.rs @@ -29,7 +29,7 @@ pub assume_specification[ u32::is_power_of_two ](self_: u32) -> (r: bool) /// On a little-endian target, converting a native-endian `u32` to little endian is the identity. #[cfg(target_endian = "little")] -pub assume_specification[ u32::to_le ](value: u32) -> (result: u32) +pub assume_specification[ u32::to_le ](value: u32) -> u32 returns value, opens_invariants none From c032fc63ae0ba279acf75340cc1aa14b3b0b14b9 Mon Sep 17 00:00:00 2001 From: Marsman1996 Date: Thu, 17 Sep 2026 10:25:30 +0800 Subject: [PATCH 21/22] refine: according to the review skill --- ostd/src/arch/x86/pci.rs | 20 +++++++++----------- ostd/src/io/io_mem/mod.rs | 3 +-- ostd/src/io/io_port/allocator.rs | 9 +-------- ostd/src/io/io_port/mod.rs | 4 ++-- 4 files changed, 13 insertions(+), 23 deletions(-) diff --git a/ostd/src/arch/x86/pci.rs b/ostd/src/arch/x86/pci.rs index d8292ac4e..1a01d7f8e 100644 --- a/ostd/src/arch/x86/pci.rs +++ b/ostd/src/arch/x86/pci.rs @@ -54,11 +54,10 @@ pub(crate) fn has_pci_bus() -> bool { pub(crate) const MSIX_DEFAULT_MSG_ADDR: u32 = 0xFEE0_0000; #[verus_verify] -#[verus_spec(address => - ensures - address == MSIX_DEFAULT_MSG_ADDR | 0b1_1000 - | ((remapping_index & 0x7FFF) << 5) - | ((remapping_index & 0x8000) >> 13), +#[verus_spec(returns + MSIX_DEFAULT_MSG_ADDR | 0b1_1000 + | ((remapping_index & 0x7FFF) << 5) + | ((remapping_index & 0x8000) >> 13), )] pub(crate) fn construct_remappable_msix_address(remapping_index: u32) -> u32 { // Use remappable format. The bits[4:3] should be always set to 1 according to the manual. @@ -73,12 +72,11 @@ pub(crate) fn construct_remappable_msix_address(remapping_index: u32) -> u32 { /// Encodes the bus, device, and function into a port address for use with the PCI I/O port. #[verus_verify] -#[verus_spec(port => - ensures - port == (1u32 << 31) - | ((location.bus as u32) << 16) - | (((location.device as u32) & 0b11111) << 11) - | (((location.function as u32) & 0b111) << 8), +#[verus_spec(returns + (1u32 << 31) + | ((location.bus as u32) << 16) + | (((location.device as u32) & 0b11111) << 11) + | (((location.function as u32) & 0b111) << 8), )] fn encode_as_port(location: &PciDeviceLocation) -> u32 { // 1 << 31: Configuration enable diff --git a/ostd/src/io/io_mem/mod.rs b/ostd/src/io/io_mem/mod.rs index fa64c5e96..306fc0e8d 100644 --- a/ostd/src/io/io_mem/mod.rs +++ b/ostd/src/io/io_mem/mod.rs @@ -114,8 +114,7 @@ impl IoMem { #[verus_verify] #[verus_spec(result => requires - range.start < range.end, - range.end <= self.length_spec(), + range.start < range.end <= self.length_spec(), self.offset_spec() + range.start <= usize::MAX, self.paddr_spec() + range.start <= usize::MAX, ensures diff --git a/ostd/src/io/io_port/allocator.rs b/ostd/src/io/io_port/allocator.rs index c73d67ace..f33c54ac2 100644 --- a/ostd/src/io/io_port/allocator.rs +++ b/ostd/src/io/io_port/allocator.rs @@ -6,8 +6,7 @@ use vstd::{ resource::set::{GhostSetAuth, GhostSubset}, tokens::InstanceId, }; -use vstd_extra::ownership::Inv; -use vstd_extra::resource_invariant::ResourceInvariant; +use vstd_extra::{ownership::Inv, resource_invariant::ResourceInvariant}; use core::ops::Range; @@ -114,9 +113,6 @@ pub(crate) open spec fn io_port_inner_inv_values( &&& id_alloc_capacity(allocator) == crate::arch::io::MAX_IO_PORT as usize } -} // verus! -verus! { - /// Authority over the set of PIO ids currently allocated by the global allocator. /// /// The `Loc` of `auth` identifies the protocol instance and `auth@` is the set of allocated @@ -201,9 +197,6 @@ impl IoPortClaim { } } -} // verus! -verus! { - ghost struct IoPortAllocInvariant; impl ResourceInvariant for IoPortAllocInvariant { diff --git a/ostd/src/io/io_port/mod.rs b/ostd/src/io/io_port/mod.rs index 71f753c97..6f4c5671a 100644 --- a/ostd/src/io/io_port/mod.rs +++ b/ostd/src/io/io_port/mod.rs @@ -140,7 +140,7 @@ impl IoPort { valid_io_port_access::(port), allocator::io_port_allocator_initialized(), ensures - result is Ok <== claim@ is Some, + result is Ok <==> claim@ is Some, result matches Ok(io_port) ==> { &&& io_port@ == port &&& !io_port.is_overlapping() @@ -178,7 +178,7 @@ impl IoPort { valid_io_port_access::(port), allocator::io_port_allocator_initialized(), ensures - result is Ok <== claim@ is Some, + result is Ok <==> claim@ is Some, result matches Ok(io_port) ==> { &&& io_port@ == port &&& io_port.is_overlapping() From e13a92b87986440218fe26770898f15ca2af2305 Mon Sep 17 00:00:00 2001 From: Marsman1996 Date: Thu, 17 Sep 2026 11:18:22 +0800 Subject: [PATCH 22/22] refine: xinyi --- ostd/src/io/io_mem/allocator.rs | 4 ++-- ostd/src/io/io_mem/mod.rs | 34 +++++++++++---------------------- 2 files changed, 13 insertions(+), 25 deletions(-) diff --git a/ostd/src/io/io_mem/allocator.rs b/ostd/src/io/io_mem/allocator.rs index 49222a054..9e60f79c6 100644 --- a/ostd/src/io/io_mem/allocator.rs +++ b/ostd/src/io/io_mem/allocator.rs @@ -37,8 +37,8 @@ impl IoMemAllocator { io_mem_range_registered(range), ensures result matches Some(io_mem) ==> { - &&& io_mem.paddr_spec() == range.start - &&& io_mem.length_spec() == range.end - range.start + &&& io_mem.paddr() == range.start + &&& io_mem.length() == range.end - range.start }, )] pub fn acquire(&self, range: Range) -> Option { diff --git a/ostd/src/io/io_mem/mod.rs b/ostd/src/io/io_mem/mod.rs index 306fc0e8d..b546c7483 100644 --- a/ostd/src/io/io_mem/mod.rs +++ b/ostd/src/io/io_mem/mod.rs @@ -42,16 +42,6 @@ verus! { #[verus_verify] impl IoMem { - /// Logical physical-address projection used by verified callers. - pub closed spec fn paddr_spec(&self) -> Paddr { - self.pa - } - - /// Logical byte length used by verified callers. - pub closed spec fn length_spec(&self) -> usize { - self.limit - } - /// Logical offset into the page-aligned mapping. pub closed spec fn offset_spec(&self) -> usize { self.offset @@ -61,7 +51,7 @@ impl IoMem { } // verus! #[verus_verify] impl HasPaddr for IoMem { - #[verus_spec(returns self.paddr_spec())] + #[verus_spec(returns IoMem::paddr(self))] fn paddr(&self) -> Paddr { self.pa } @@ -79,8 +69,8 @@ impl IoMem { vstd_extra::panic::may_panic(), ensures result matches Ok(io_mem) ==> { - &&& io_mem.paddr_spec() == range.start - &&& io_mem.length_spec() == range.end - range.start + &&& io_mem.paddr() == range.start + &&& io_mem.length() == range.end - range.start }, )] pub fn acquire(range: Range) -> Result { @@ -93,15 +83,13 @@ impl IoMem { } /// Returns the physical address of the I/O memory. - #[verus_verify] - #[verus_spec(returns self.paddr_spec())] + #[verus_verify(dual_spec)] pub fn paddr(&self) -> Paddr { self.pa } /// Returns the length of the I/O memory region. - #[verus_verify] - #[verus_spec(returns self.length_spec())] + #[verus_verify(dual_spec)] pub fn length(&self) -> usize { self.limit } @@ -114,13 +102,13 @@ impl IoMem { #[verus_verify] #[verus_spec(result => requires - range.start < range.end <= self.length_spec(), + range.start < range.end <= self.length(), self.offset_spec() + range.start <= usize::MAX, - self.paddr_spec() + range.start <= usize::MAX, + self.paddr() + range.start <= usize::MAX, ensures result.offset_spec() == self.offset_spec() + range.start, - result.length_spec() == range.end - range.start, - result.paddr_spec() == self.paddr_spec() + range.start, + result.length() == range.end - range.start, + result.paddr() == self.paddr() + range.start, )] pub fn slice(&self, range: Range) -> Self { // This ensures `range.start < range.end` and `range.end <= limit`. @@ -152,8 +140,8 @@ impl IoMem { range.start <= range.end, range.end <= usize::MAX - (PAGE_SIZE - 1), ensures - result.paddr_spec() == range.start, - result.length_spec() + result.paddr() == range.start, + result.length() == range.end - range.start, )] pub(crate) unsafe fn new(range: Range, flags: PageFlags, cache: CachePolicy) -> Self {