Lean verification: prove 164 more functions and fix the kernel bugs the proofs found

src/arch/aarch64/security/bti.rs

@@ -17,7 +17,9 @@
 mod control;
 mod guard;
 mod landing;
+mod pad;
 
 pub use control::{bti_enabled, bti_supported, disable_bti, enable_bti, init_bti};
 pub use guard::BtiGuard;
 pub use landing::check_bti_landing_pad;
+pub use pad::is_bti_landing_pad;

src/arch/aarch64/security/bti/landing.rs

@@ -14,7 +14,9 @@
 // You should have received a copy of the GNU Affero General Public License
 // along with this program. If not, see <https://www.gnu.org/licenses/>.
 
+use super::pad::is_bti_landing_pad;
+
 pub fn check_bti_landing_pad(addr: u64) -> bool {
     let instruction = unsafe { *(addr as *const u32) };
-    matches!(instruction, 0xD503201F | 0xD503245F | 0xD503249F | 0xD50324DF)
+    is_bti_landing_pad(instruction)
 }

src/arch/aarch64/security/bti/pad.rs

@@ -0,0 +1,29 @@
+// NONOS Operating System
+// Copyright (C) 2026 NONOS Contributors
+//
+// This program is free software: you can redistribute it and/or modify
+// it under the terms of the GNU Affero General Public License as published by
+// the Free Software Foundation, either version 3 of the License, or
+// (at your option) any later version.
+//
+// This program is distributed in the hope that it will be useful,
+// but WITHOUT ANY WARRANTY; without even the implied warranty of
+// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+// GNU Affero General Public License for more details.
+//
+// You should have received a copy of the GNU Affero General Public License
+// along with this program. If not, see <https://www.gnu.org/licenses/>.
+
+pub const BTI_C: u32 = 0xD503245F;
+pub const BTI_J: u32 = 0xD503249F;
+pub const BTI_JC: u32 = 0xD50324DF;
+pub const PACIASP: u32 = 0xD503233F;
+pub const PACIBSP: u32 = 0xD503237F;
+
+/* Whether an indirect branch may land on this instruction in a guarded page.
+BTI c, j and jc are landing pads, and PACIASP and PACIBSP act as BTI c. A NOP
+or a bare BTI accepts no branch type, so on a core with FEAT_BTI a branch to
+either raises a Branch Target exception. */
+pub const fn is_bti_landing_pad(instruction: u32) -> bool {
+    matches!(instruction, BTI_C | BTI_J | BTI_JC | PACIASP | PACIBSP)
+}

src/arch/x86_64/acpi/data/ioapic.rs

@@ -22,7 +22,8 @@ pub struct IoApicInfo {
 }
 
 impl IoApicInfo {
+    /* gsi_base comes from the MADT unchecked; saturate rather than abort. */
     pub fn gsi_max(&self) -> u32 {
-        self.gsi_base + 23
+        self.gsi_base.saturating_add(23)
     }
 }

src/arch/x86_64/iommu/regs/mod.rs

@@ -16,3 +16,4 @@
 
 pub mod cap;
 pub mod offsets;
+pub mod window;

src/arch/x86_64/iommu/regs/window.rs

@@ -0,0 +1,27 @@
+// NONOS Operating System
+// Copyright (C) 2026 NONOS Contributors
+//
+// This program is free software: you can redistribute it and/or modify
+// it under the terms of the GNU Affero General Public License as published by
+// the Free Software Foundation, either version 3 of the License, or
+// (at your option) any later version.
+//
+// This program is distributed in the hope that it will be useful,
+// but WITHOUT ANY WARRANTY; without even the implied warranty of
+// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+// GNU Affero General Public License for more details.
+//
+// You should have received a copy of the GNU Affero General Public License
+// along with this program. If not, see <https://www.gnu.org/licenses/>.
+
+use super::cap::{fault_recording_count, fault_recording_offset};
+use super::offsets::iotlb_offset;
+
+/* Whether every register the kernel touches lies inside a mapped window of
+`window` bytes. The IOTLB register and the fault-recording registers sit
+where CAP and ECAP say, up to about 16 KiB into the unit, so a unit that
+places them past the window must be refused rather than accessed. */
+pub const fn registers_fit(cap: u64, ecap: u64, window: usize) -> bool {
+    let faults_end = fault_recording_offset(cap) + fault_recording_count(cap) as usize * 16;
+    iotlb_offset(ecap) + 8 <= window && faults_end <= window
+}

src/arch/x86_64/iommu/unit/access.rs

@@ -27,6 +27,9 @@ pub struct RemapUnit {
 /// Register window of a unit, per the spec.
 pub const UNIT_WINDOW: usize = 4096;
 
+/* Each accessor bounds the offset by subtracting from the window rather than
+adding to the offset, so no offset, however large, can wrap past the check. */
+
 impl RemapUnit {
     /// # Safety
     /// `base_va` must be a live mapping of `UNIT_WINDOW` uncached bytes over
@@ -40,14 +43,14 @@ impl RemapUnit {
     }
 
     pub fn read32(&self, offset: usize) -> u32 {
-        debug_assert!(offset + 4 <= UNIT_WINDOW);
+        assert!(offset <= UNIT_WINDOW - 4);
         // SAFETY: offset is inside the mapped register window this value
         // promises, and the registers are uncached device memory.
         unsafe { core::ptr::read_volatile((self.base_va as usize + offset) as *const u32) }
     }
 
     pub fn read64(&self, offset: usize) -> u64 {
-        debug_assert!(offset + 8 <= UNIT_WINDOW);
+        assert!(offset <= UNIT_WINDOW - 8);
         // SAFETY: as read32.
         unsafe { core::ptr::read_volatile((self.base_va as usize + offset) as *const u64) }
     }
@@ -56,15 +59,15 @@ impl RemapUnit {
     /// Writing a remapping register changes how devices reach memory. The
     /// caller owns the sequencing the spec requires around the register.
     pub unsafe fn write32(&self, offset: usize, value: u32) {
-        debug_assert!(offset + 4 <= UNIT_WINDOW);
+        assert!(offset <= UNIT_WINDOW - 4);
         // SAFETY: offset is inside the mapped window; the caller owns meaning.
         unsafe { core::ptr::write_volatile((self.base_va as usize + offset) as *mut u32, value) }
     }
 
     /// # Safety
     /// As `write32`.
     pub unsafe fn write64(&self, offset: usize, value: u64) {
-        debug_assert!(offset + 8 <= UNIT_WINDOW);
+        assert!(offset <= UNIT_WINDOW - 8);
         // SAFETY: offset is inside the mapped window; the caller owns meaning.
         unsafe { core::ptr::write_volatile((self.base_va as usize + offset) as *mut u64, value) }
     }

src/arch/x86_64/iommu/unit/probe.rs

@@ -19,7 +19,7 @@
 
 use super::access::{RemapUnit, UNIT_WINDOW};
 use crate::arch::x86_64::acpi::parser::other::remap_unit_bases;
-use crate::arch::x86_64::iommu::regs::{cap, offsets};
+use crate::arch::x86_64::iommu::regs::{cap, offsets, window};
 use crate::memory::addr::PhysAddr;
 
 /// What one unit supports, as read from its Capability register.
@@ -44,6 +44,8 @@ pub enum ProbeError {
     MapFailed,
     /// The unit reports no supported paging depth, so it cannot translate.
     NoUsableAgaw,
+    /// CAP or ECAP places a register the kernel uses beyond the mapped window.
+    RegistersOutsideWindow,
 }
 
 /// Map the first unit DMAR reported and read its capabilities.
@@ -77,6 +79,9 @@ pub fn probe_at(base_pa: u64) -> Result<UnitInfo, ProbeError> {
     let status = unit.read32(offsets::GSTS);
 
     let levels = cap::preferred_levels(capability).ok_or(ProbeError::NoUsableAgaw)?;
+    if !window::registers_fit(capability, ecap, UNIT_WINDOW) {
+        return Err(ProbeError::RegistersOutsideWindow);
+    }
 
     Ok(UnitInfo {
         unit,

src/arch/x86_64/iommu/unit/report/failure.rs

@@ -23,5 +23,6 @@ pub(super) fn reason(e: ProbeError) -> &'static [u8] {
         ProbeError::NoUnits => b"no units",
         ProbeError::MapFailed => b"register window not mappable",
         ProbeError::NoUsableAgaw => b"no supported paging depth",
+        ProbeError::RegistersOutsideWindow => b"registers beyond the mapped window",
     }
 }

src/arch/x86_64/multiboot/modules_acpi.rs

@@ -24,6 +24,7 @@ pub struct AcpiRsdp {
     pub length: Option<u32>,
     pub xsdt_address: Option<u64>,
     pub extended_checksum: Option<u8>,
+    pub reserved: Option<[u8; 3]>,
 }
 
 impl AcpiRsdp {
@@ -60,10 +61,23 @@ impl AcpiRsdp {
         sum == 0
     }
 
+    /* An ACPI 2.0 RSDP passes only with all its extended fields present, a
+    length of exactly 36, and those 36 bytes summing to zero, reserved bytes
+    included. The extended checksum covers the length the table declares, and
+    only 36 bytes are kept, so a longer declaration could hide unchecked bytes.
+    Below revision 2 there is no extended checksum to check. */
     pub fn verify_extended_checksum(&self) -> bool {
         if !self.is_acpi2() {
             return true;
         }
+        let (Some(len), Some(xsdt), Some(ext), Some(reserved)) =
+            (self.length, self.xsdt_address, self.extended_checksum, self.reserved)
+        else {
+            return false;
+        };
+        if len != 36 {
+            return false;
+        }
         let mut sum: u8 = 0;
         for &b in &self.signature {
             sum = sum.wrapping_add(b);
@@ -76,18 +90,15 @@ impl AcpiRsdp {
         for &b in &self.rsdt_address.to_le_bytes() {
             sum = sum.wrapping_add(b);
         }
-        if let Some(len) = self.length {
-            for &b in &len.to_le_bytes() {
-                sum = sum.wrapping_add(b);
-            }
+        for &b in &len.to_le_bytes() {
+            sum = sum.wrapping_add(b);
         }
-        if let Some(xsdt) = self.xsdt_address {
-            for &b in &xsdt.to_le_bytes() {
-                sum = sum.wrapping_add(b);
-            }
+        for &b in &xsdt.to_le_bytes() {
+            sum = sum.wrapping_add(b);
         }
-        if let Some(ext) = self.extended_checksum {
-            sum = sum.wrapping_add(ext);
+        sum = sum.wrapping_add(ext);
+        for &b in &reserved {
+            sum = sum.wrapping_add(b);
         }
         sum == 0
     }

src/arch/x86_64/multiboot/state/parse/firmware.rs

@@ -87,13 +87,15 @@ impl MultibootManager {
             let revision = *rsdp_ptr.add(15);
             let rsdt_address = core::ptr::read_unaligned(rsdp_ptr.add(16) as *const u32);
 
-            let (length, xsdt_address, extended_checksum) = if is_new && rsdp_size >= 36 {
+            let (length, xsdt_address, extended_checksum, reserved) = if is_new && rsdp_size >= 36 {
                 let length = core::ptr::read_unaligned(rsdp_ptr.add(20) as *const u32);
                 let xsdt_address = core::ptr::read_unaligned(rsdp_ptr.add(24) as *const u64);
                 let extended_checksum = *rsdp_ptr.add(32);
-                (Some(length), Some(xsdt_address), Some(extended_checksum))
+                let mut reserved = [0u8; 3];
+                reserved.copy_from_slice(slice::from_raw_parts(rsdp_ptr.add(33), 3));
+                (Some(length), Some(xsdt_address), Some(extended_checksum), Some(reserved))
             } else {
-                (None, None, None)
+                (None, None, None, None)
             };
 
             Ok(AcpiRsdp {
@@ -105,6 +107,7 @@ impl MultibootManager {
                 length,
                 xsdt_address,
                 extended_checksum,
+                reserved,
             })
         }
     }

src/arch/x86_64/port/stats_snapshot.rs

@@ -26,10 +26,14 @@ pub struct PortStatsSnapshot {
 }
 
 impl PortStatsSnapshot {
+    /* The counters wrap on their own; their sums saturate rather than abort. */
     pub const fn total_ops(&self) -> u64 {
-        self.read_ops + self.write_ops + self.string_read_ops + self.string_write_ops
+        self.read_ops
+            .saturating_add(self.write_ops)
+            .saturating_add(self.string_read_ops)
+            .saturating_add(self.string_write_ops)
     }
     pub const fn total_bytes(&self) -> u64 {
-        self.bytes_read + self.bytes_written
+        self.bytes_read.saturating_add(self.bytes_written)
     }
 }

src/arch/x86_64/port/stats_types.rs

@@ -63,10 +63,7 @@ impl PortStats {
     }
 
     pub fn total_ops(&self) -> u64 {
-        self.read_ops.load(Ordering::Relaxed)
-            + self.write_ops.load(Ordering::Relaxed)
-            + self.string_read_ops.load(Ordering::Relaxed)
-            + self.string_write_ops.load(Ordering::Relaxed)
+        self.snapshot().total_ops()
     }
 }
 

src/arch/x86_64/uefi/constants/revisions.rs

@@ -14,27 +14,34 @@
 // You should have received a copy of the GNU Affero General Public License
 // along with this program. If not, see <https://www.gnu.org/licenses/>.
 
-pub const UEFI_REVISION_2_0: u32 = 0x00020000;
+/* The UEFI specification packs a revision as the major version in the upper
+sixteen bits and, in the lower sixteen, the minor version times ten plus the
+patch digit: 2.3.1 is (2 << 16) | 31 and 2.10 is (2 << 16) | 100. */
+pub const fn uefi_revision(major: u16, minor: u16, patch: u16) -> u32 {
+    ((major as u32) << 16) | (minor as u32 * 10 + patch as u32)
+}
 
-pub const UEFI_REVISION_2_1: u32 = 0x00020100;
+pub const UEFI_REVISION_2_0: u32 = uefi_revision(2, 0, 0);
 
-pub const UEFI_REVISION_2_3: u32 = 0x00020300;
+pub const UEFI_REVISION_2_1: u32 = uefi_revision(2, 1, 0);
 
-pub const UEFI_REVISION_2_3_1: u32 = 0x0002001F;
+pub const UEFI_REVISION_2_3: u32 = uefi_revision(2, 3, 0);
 
-pub const UEFI_REVISION_2_4: u32 = 0x00020400;
+pub const UEFI_REVISION_2_3_1: u32 = uefi_revision(2, 3, 1);
 
-pub const UEFI_REVISION_2_5: u32 = 0x00020500;
+pub const UEFI_REVISION_2_4: u32 = uefi_revision(2, 4, 0);
 
-pub const UEFI_REVISION_2_6: u32 = 0x00020600;
+pub const UEFI_REVISION_2_5: u32 = uefi_revision(2, 5, 0);
 
-pub const UEFI_REVISION_2_7: u32 = 0x00020700;
+pub const UEFI_REVISION_2_6: u32 = uefi_revision(2, 6, 0);
 
-pub const UEFI_REVISION_2_8: u32 = 0x00020800;
+pub const UEFI_REVISION_2_7: u32 = uefi_revision(2, 7, 0);
 
-pub const UEFI_REVISION_2_9: u32 = 0x00020900;
+pub const UEFI_REVISION_2_8: u32 = uefi_revision(2, 8, 0);
 
-pub const UEFI_REVISION_2_10: u32 = 0x00020A00;
+pub const UEFI_REVISION_2_9: u32 = uefi_revision(2, 9, 0);
+
+pub const UEFI_REVISION_2_10: u32 = uefi_revision(2, 10, 0);
 
 pub const RESET_TYPE_COLD: u32 = 0;
 

src/arch/x86_64/uefi/manager/init.rs

@@ -21,6 +21,7 @@ use core::sync::atomic::Ordering;
 
 use super::core::UefiManager;
 use super::state::INITIALIZED;
+use crate::arch::x86_64::uefi::constants::UEFI_REVISION_2_8;
 use crate::arch::x86_64::uefi::error::UefiError;
 use crate::arch::x86_64::uefi::tables::RuntimeServices;
 use crate::arch::x86_64::uefi::types::Guid;
@@ -70,7 +71,7 @@ impl UefiManager {
 
         info.vendor = String::from("NONOS UEFI");
         info.version = String::from("2.8");
-        info.revision = 0x00020008;
+        info.revision = UEFI_REVISION_2_8;
         info.firmware_revision = 0x00010000;
 
         *self.firmware_info.write() = info;

src/arch/x86_64/uefi/tables/memory_desc.rs

@@ -40,11 +40,16 @@ impl MemoryDescriptor {
     pub const EFI_MEMORY_CPU_CRYPTO: u64 = 0x0000000000080000;
     pub const EFI_MEMORY_RUNTIME: u64 = 0x8000000000000000;
 
+    /* Saturating: the page count and start come from firmware, and an
+    overflowing descriptor must not abort the kernel. */
     pub fn size_bytes(&self) -> u64 {
+        if self.number_of_pages > u64::MAX / 4096 {
+            return u64::MAX;
+        }
         self.number_of_pages * 4096
     }
     pub fn end_address(&self) -> u64 {
-        self.physical_start + self.size_bytes()
+        self.physical_start.saturating_add(self.size_bytes())
     }
     pub fn is_runtime(&self) -> bool {
         self.attribute & Self::EFI_MEMORY_RUNTIME != 0