prove: arch::pci (x86) & io

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

ostd/Cargo.toml

@@ -18,14 +18,15 @@ 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"
 buddy_system_allocator = { version = "0.10", default-features = false, features = ["alloc"] }
 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"] }

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

ostd/src/arch/x86/device/io_port.rs

@@ -7,3 +7,62 @@ 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<T>(port: int) -> bool {
+    &&& valid_io_port_number(port)
+    &&& port + size_of::<T>() <= 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::<Self>(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::<Self>(port as int),
+    ;
+}
+
+} // verus!

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;*/

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: <https://bochs.sourceforge.io/techspec/PORTS.LST>.
+#[verus_verify]
 pub const MAX_IO_PORT: u16 = u16::MAX;

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 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;
-*/

ostd/src/arch/x86/pci.rs

@@ -1,30 +1,67 @@
 // 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::*};
 
-static PCI_ADDRESS_PORT: IoPort<u32, WriteOnlyAccess> = unsafe { IoPort::new(0x0CF8) };
-static PCI_DATA_PORT: IoPort<u32, ReadWriteAccess> = unsafe { IoPort::new(0x0CFC) };
+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<u32, WriteOnlyAccess>
+    ensures
+        PCI_ADDRESS_PORT.well_formed(),
+{
+    unsafe { IoPort::new(0x0CF8) }
+}
+
+exec static PCI_DATA_PORT: IoPort<u32, ReadWriteAccess>
+    ensures
+        PCI_DATA_PORT.well_formed(),
+{
+    unsafe { IoPort::new(0x0CFC) }
+}
 
+} // verus!
+#[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<u32> {
     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 +74,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)

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();
-}
+}*/

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

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);
     }
-}
+}*/