From adaea8b9b6fcfb93b96c91a28af60eb8674fce2c Mon Sep 17 00:00:00 2001
From: Tom Dohrmann <erbse.13@gmx.de>
Date: Sun, 10 May 2026 18:28:19 +0200
Subject: [PATCH 01/10] implement kani::Arbitrary for VirtAddr and Page

---
 src/addr.rs                   | 43 ++++++++++++-----------------------
 src/structures/paging/page.rs |  7 ++++++
 2 files changed, 22 insertions(+), 28 deletions(-)

diff --git a/src/addr.rs b/src/addr.rs
index 232e96a1..1a271120 100644
--- a/src/addr.rs
+++ b/src/addr.rs
@@ -488,6 +488,13 @@ impl Step for VirtAddr {
     }
 }
 
+#[cfg(kani)]
+impl kani::Arbitrary for VirtAddr {
+    fn any() -> Self {
+        Self::new_truncate(kani::any())
+    }
+}
+
 /// A passed `u64` was not a valid physical address.
 ///
 /// This means that bits 52 to 64 were not all null.
@@ -993,10 +1000,8 @@ mod proofs {
     // step starting from any address.
     #[kani::proof]
     fn forward_base_case() {
-        let start_raw: u64 = kani::any();
-        let Ok(start) = VirtAddr::try_new(start_raw) else {
-            return;
-        };
+        let start = kani::any::<VirtAddr>();
+        let start_raw = start.as_u64();
 
         // Adding 0 to any address should always yield the same address.
         let same = Step::forward(start, 0);
@@ -1030,10 +1035,7 @@ mod proofs {
     // same as taking one combined large step.
     #[kani::proof]
     fn forward_induction_step() {
-        let start_raw: u64 = kani::any();
-        let Ok(start) = VirtAddr::try_new(start_raw) else {
-            return;
-        };
+        let start = kani::any::<VirtAddr>();
 
         let count1: usize = kani::any();
         let count2: usize = kani::any();
@@ -1060,10 +1062,7 @@ mod proofs {
     // for all inputs for which `forward_checked` succeeds.
     #[kani::proof]
     fn forward_implies_backward() {
-        let start_raw: u64 = kani::any();
-        let Ok(start) = VirtAddr::try_new(start_raw) else {
-            return;
-        };
+        let start = kani::any::<VirtAddr>();
         let count: usize = kani::any();
 
         // If `forward_checked` succeeds...
@@ -1080,10 +1079,7 @@ mod proofs {
     // succeeds, `forward` succeeds as well.
     #[kani::proof]
     fn backward_implies_forward() {
-        let end_raw: u64 = kani::any();
-        let Ok(end) = VirtAddr::try_new(end_raw) else {
-            return;
-        };
+        let end = kani::any::<VirtAddr>();
         let count: usize = kani::any();
 
         // If `backward_checked` succeeds...
@@ -1105,10 +1101,7 @@ mod proofs {
     // `steps_between` for all inputs for which `forward_checked` succeeds.
     #[kani::proof]
     fn forward_implies_steps_between() {
-        let start: u64 = kani::any();
-        let Ok(start) = VirtAddr::try_new(start) else {
-            return;
-        };
+        let start = kani::any::<VirtAddr>();
         let count: usize = kani::any();
 
         // If `forward_checked` succeeds...
@@ -1124,14 +1117,8 @@ mod proofs {
     // succeeds, `forward` succeeds as well.
     #[kani::proof]
     fn steps_between_implies_forward() {
-        let start: u64 = kani::any();
-        let Ok(start) = VirtAddr::try_new(start) else {
-            return;
-        };
-        let end: u64 = kani::any();
-        let Ok(end) = VirtAddr::try_new(end) else {
-            return;
-        };
+        let start = kani::any::<VirtAddr>();
+        let end = kani::any::<VirtAddr>();
 
         // If `steps_between` succeeds...
         let Some(count) = Step::steps_between(&start, &end).1 else {
diff --git a/src/structures/paging/page.rs b/src/structures/paging/page.rs
index 9bfe22cf..b8ed8bb0 100644
--- a/src/structures/paging/page.rs
+++ b/src/structures/paging/page.rs
@@ -460,6 +460,13 @@ impl<S: PageSize> fmt::Debug for PageRangeInclusive<S> {
     }
 }
 
+#[cfg(kani)]
+impl<S: PageSize> kani::Arbitrary for Page<S> {
+    fn any() -> Self {
+        Self::containing_address(kani::any())
+    }
+}
+
 /// The given address was not sufficiently aligned.
 #[derive(Debug)]
 pub struct AddressNotAligned;

From 70add4af9fdb54025f185ea5411ef18e337f2179 Mon Sep 17 00:00:00 2001
From: Tom Dohrmann <erbse.13@gmx.de>
Date: Sun, 10 May 2026 16:31:28 +0200
Subject: [PATCH 02/10] test that jumping the address range gap panics

PageRange::next and PageRangeInclusive::next should panic when the user
tries to jump the address range gap.
---
 src/structures/paging/page.rs | 38 +++++++++++++++++++++++++++++++++++
 1 file changed, 38 insertions(+)

diff --git a/src/structures/paging/page.rs b/src/structures/paging/page.rs
index b8ed8bb0..6e7b1aad 100644
--- a/src/structures/paging/page.rs
+++ b/src/structures/paging/page.rs
@@ -537,6 +537,44 @@ mod tests {
         assert_eq!(range_inclusive.next(), None);
     }
 
+    #[test]
+    #[should_panic = "attempt to add resulted in non-canonical virtual address: VirtAddrNotValid(0x800000000000)"]
+    fn test_page_range_next_jumping_gap_panics() {
+        let start = 0x7fff_ffff_f000;
+        let end = 0xffff_8000_0000_0000;
+        let start = VirtAddr::new(start);
+        let end = VirtAddr::new(end);
+        let start = Page::<Size4KiB>::from_start_address(start).unwrap();
+        let end = Page::from_start_address(end).unwrap();
+        Page::range(start, end).next();
+    }
+
+    // TODO: This probably shouldn't panic, but we can't fix this without a breaking change.
+    #[test]
+    #[should_panic = "attempt to add resulted in non-canonical virtual address: VirtAddrNotValid(0x800000000000)"]
+    fn test_page_range_inclusive_next_not_jumping_gap_panics() {
+        let start = 0x7fff_ffff_f000;
+        let end = 0x7fff_ffff_f000;
+        let start = VirtAddr::new(start);
+        let end = VirtAddr::new(end);
+        let start = Page::<Size4KiB>::from_start_address(start).unwrap();
+        let end = Page::from_start_address(end).unwrap();
+        Page::range_inclusive(start, end).next();
+    }
+
+    #[test]
+    #[should_panic = "attempt to add resulted in non-canonical virtual address: VirtAddrNotValid(0x800000000000)"]
+    fn test_page_range_inclusive_next_jumping_gap_panics() {
+        let start = 0x7fff_ffff_f000;
+        let end = 0x7fff_ffff_f000;
+        let start = VirtAddr::new(start);
+        let end = VirtAddr::new(end);
+        let start = Page::<Size4KiB>::from_start_address(start).unwrap();
+        let end = Page::from_start_address(end).unwrap();
+        Page::range_inclusive(start, end).next();
+        Page::range_inclusive(start, end).next();
+    }
+
     #[test]
     pub fn test_page_range_len() {
         let start_addr = VirtAddr::new(0xdead_beaf);

From 28d2377adc198919119c8278edc616cf773da3c2 Mon Sep 17 00:00:00 2001
From: Tom Dohrmann <erbse.13@gmx.de>
Date: Sun, 10 May 2026 16:33:11 +0200
Subject: [PATCH 03/10] implement DoubleEndedIterator for
 PageRange/PageRangeInclusive

---
 src/structures/paging/page.rs | 71 +++++++++++++++++++++++++++++++++++
 1 file changed, 71 insertions(+)

diff --git a/src/structures/paging/page.rs b/src/structures/paging/page.rs
index 6e7b1aad..7c449dc1 100644
--- a/src/structures/paging/page.rs
+++ b/src/structures/paging/page.rs
@@ -373,6 +373,18 @@ impl<S: PageSize> Iterator for PageRange<S> {
     }
 }
 
+impl<S: PageSize> DoubleEndedIterator for PageRange<S> {
+    #[inline]
+    fn next_back(&mut self) -> Option<Self::Item> {
+        if self.start < self.end {
+            self.end -= 1;
+            Some(self.end)
+        } else {
+            None
+        }
+    }
+}
+
 impl PageRange<Size2MiB> {
     /// Converts the range of 2MiB pages to a range of 4KiB pages.
     #[inline]
@@ -451,6 +463,27 @@ impl<S: PageSize> Iterator for PageRangeInclusive<S> {
     }
 }
 
+impl<S: PageSize> DoubleEndedIterator for PageRangeInclusive<S> {
+    #[inline]
+    fn next_back(&mut self) -> Option<Self::Item> {
+        if self.start <= self.end {
+            let page = self.end;
+
+            // If the start of the inclusive range is 0, decrementing end until
+            // it is smaller than the start will cause an integer underflow.
+            // So instead, in that case we increment start rather than decrementing end.
+            if self.end.start_address().as_u64() != 0 {
+                self.end -= 1;
+            } else {
+                self.start += 1;
+            }
+            Some(page)
+        } else {
+            None
+        }
+    }
+}
+
 impl<S: PageSize> fmt::Debug for PageRangeInclusive<S> {
     fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
         f.debug_struct("PageRangeInclusive")
@@ -550,6 +583,18 @@ mod tests {
     }
 
     // TODO: This probably shouldn't panic, but we can't fix this without a breaking change.
+    #[test]
+    #[should_panic = "attempt to subtract resulted in non-canonical virtual address: VirtAddrNotValid(0xffff7ffffffff000)"]
+    fn test_page_range_next_back_jumping_gap_panics() {
+        let start = 0x7fff_ffff_f000;
+        let end = 0xffff_8000_0000_0000;
+        let start = VirtAddr::new(start);
+        let end = VirtAddr::new(end);
+        let start = Page::<Size4KiB>::from_start_address(start).unwrap();
+        let end = Page::from_start_address(end).unwrap();
+        Page::range(start, end).next_back();
+    }
+
     #[test]
     #[should_panic = "attempt to add resulted in non-canonical virtual address: VirtAddrNotValid(0x800000000000)"]
     fn test_page_range_inclusive_next_not_jumping_gap_panics() {
@@ -562,6 +607,19 @@ mod tests {
         Page::range_inclusive(start, end).next();
     }
 
+    #[test]
+    #[should_panic = "attempt to subtract resulted in non-canonical virtual address: VirtAddrNotValid(0xffff7ffffffff000)"]
+    fn test_page_range_inclusive_next_back_not_jumping_gap_panics() {
+        let start = 0x7fff_ffff_f000;
+        let end = 0xffff_8000_0000_0000;
+        let start = VirtAddr::new(start);
+        let end = VirtAddr::new(end);
+        let start = Page::<Size4KiB>::from_start_address(start).unwrap();
+        let end = Page::from_start_address(end).unwrap();
+        Page::range_inclusive(start, end).next_back();
+    }
+
+    // TODO: This probably shouldn't panic, but we can't fix this without a breaking change.
     #[test]
     #[should_panic = "attempt to add resulted in non-canonical virtual address: VirtAddrNotValid(0x800000000000)"]
     fn test_page_range_inclusive_next_jumping_gap_panics() {
@@ -575,6 +633,19 @@ mod tests {
         Page::range_inclusive(start, end).next();
     }
 
+    #[test]
+    #[should_panic = "attempt to subtract resulted in non-canonical virtual address: VirtAddrNotValid(0xffff7ffffffff000)"]
+    fn test_page_range_inclusive_next_back_jumping_gap_panics() {
+        let start = 0xffff_8000_0000_0000;
+        let end = 0xffff_8000_0000_0000;
+        let start = VirtAddr::new(start);
+        let end = VirtAddr::new(end);
+        let start = Page::<Size4KiB>::from_start_address(start).unwrap();
+        let end = Page::from_start_address(end).unwrap();
+        Page::range_inclusive(start, end).next_back();
+        Page::range_inclusive(start, end).next_back();
+    }
+
     #[test]
     pub fn test_page_range_len() {
         let start_addr = VirtAddr::new(0xdead_beaf);

From 797102e4e10df26f3d468dd4b789084053d950ae Mon Sep 17 00:00:00 2001
From: Tom Dohrmann <erbse.13@gmx.de>
Date: Sun, 10 May 2026 16:34:33 +0200
Subject: [PATCH 04/10] prove that PageRange/PageRangeInclusive behave like
 Range

... except when jumping the address space gap.
---
 src/structures/paging/page.rs | 157 ++++++++++++++++++++++++++++++++++
 1 file changed, 157 insertions(+)

diff --git a/src/structures/paging/page.rs b/src/structures/paging/page.rs
index 7c449dc1..7af2e465 100644
--- a/src/structures/paging/page.rs
+++ b/src/structures/paging/page.rs
@@ -765,3 +765,160 @@ mod tests {
         }
     }
 }
+
+#[cfg(kani)]
+mod proofs {
+    use super::*;
+
+    fn page_range_next_harness(should_panic_mode: bool) {
+        let start = kani::any::<Page<Size4KiB>>();
+        let end = kani::any::<Page<Size4KiB>>();
+
+        // If the code is expected to panic, only run it in `#[should_panic]`
+        // mode.
+        let should_panic = start.start_address().as_u64() != 0x7fff_ffff_e000
+            || start.start_address().as_u64() != 0x7fff_ffff_f000;
+        kani::assume(should_panic == should_panic_mode);
+
+        if should_panic {
+            // Calling `next` should panic.
+            let mut our_range = Page::range(start, end);
+            our_range.next();
+            our_range.next();
+            return;
+        }
+
+        // Otherwise the results should match what `Range` returns.
+        let mut our_range = Page::range(start, end);
+        let mut native_range = start..end;
+        // The first assert checks that we're returning the correct value.
+        assert_eq!(our_range.next(), native_range.next());
+        // The second assert checks that we're updating the range state correctly.
+        assert_eq!(our_range.next(), native_range.next());
+    }
+
+    #[kani::proof]
+    fn page_range_next() {
+        page_range_next_harness(false);
+    }
+
+    #[kani::proof]
+    #[kani::should_panic]
+    fn page_range_next_panic() {
+        page_range_next_harness(true);
+    }
+
+    fn page_range_next_back_harness(should_panic_mode: bool) {
+        let start = kani::any::<Page<Size4KiB>>();
+        let end = kani::any::<Page<Size4KiB>>();
+
+        // If the code is expected to panic, only run it in `#[should_panic]`
+        // mode.
+        let should_panic = start.start_address().as_u64() != 0xffff_8000_0000_0000
+            || start.start_address().as_u64() != 0xffff_8000_0000_1000;
+        kani::assume(should_panic == should_panic_mode);
+
+        if should_panic {
+            // Calling `next_back` should panic.
+            let mut our_range = Page::range(start, end);
+            our_range.next_back();
+            our_range.next_back();
+            return;
+        }
+
+        // Otherwise the results should match what `Range` returns.
+        let mut our_range = Page::range(start, end);
+        let mut native_range = start..end;
+        // The first assert checks that we're returning the correct value.
+        assert_eq!(our_range.next_back(), native_range.next_back());
+        // The second assert checks that we're updating the range state correctly.
+        assert_eq!(our_range.next_back(), native_range.next_back());
+    }
+
+    #[kani::proof]
+    fn page_range_next_back() {
+        page_range_next_back_harness(false);
+    }
+
+    #[kani::proof]
+    #[kani::should_panic]
+    fn page_range_next_back_panic() {
+        page_range_next_back_harness(true);
+    }
+
+    fn page_range_inclusive_next_harness(should_panic_mode: bool) {
+        let start = kani::any::<Page<Size4KiB>>();
+        let end = kani::any::<Page<Size4KiB>>();
+
+        // If the code is expected to panic, only run it in `#[should_panic]`
+        // mode.
+        let should_panic = start.start_address().as_u64() != 0x7fff_ffff_e000
+            || start.start_address().as_u64() != 0x7fff_ffff_f000;
+        kani::assume(should_panic == should_panic_mode);
+
+        if should_panic {
+            // Calling `next` should panic.
+            let mut our_range = Page::range_inclusive(start, end);
+            our_range.next();
+            our_range.next();
+            return;
+        }
+
+        // Otherwise the results should match what `Range` returns.
+        let mut our_range = Page::range_inclusive(start, end);
+        let mut native_range = start..=end;
+        // The first assert checks that we're returning the correct value.
+        assert_eq!(our_range.next(), native_range.next());
+        // The second assert checks that we're updating the range state correctly.
+        assert_eq!(our_range.next(), native_range.next());
+    }
+
+    #[kani::proof]
+    fn page_range_inclusive_next() {
+        page_range_inclusive_next_harness(false);
+    }
+
+    #[kani::proof]
+    #[kani::should_panic]
+    fn page_range_inclusive_next_panic() {
+        page_range_inclusive_next_harness(true);
+    }
+
+    fn page_range_inclusive_next_back_harness(should_panic_mode: bool) {
+        let start = kani::any::<Page<Size4KiB>>();
+        let end = kani::any::<Page<Size4KiB>>();
+
+        // If the code is expected to panic, only run it in `#[should_panic]`
+        // mode.
+        let should_panic = start.start_address().as_u64() != 0xffff_8000_0000_0000
+            || start.start_address().as_u64() != 0xffff_8000_0000_1000;
+        kani::assume(should_panic == should_panic_mode);
+
+        if should_panic {
+            // Calling `next_back` should panic.
+            let mut our_range = Page::range_inclusive(start, end);
+            our_range.next_back();
+            our_range.next_back();
+            return;
+        }
+
+        // Otherwise the results should match what `Range` returns.
+        let mut our_range = Page::range_inclusive(start, end);
+        let mut native_range = start..=end;
+        // The first assert checks that we're returning the correct value.
+        assert_eq!(our_range.next_back(), native_range.next_back());
+        // The second assert checks that we're updating the range state correctly.
+        assert_eq!(our_range.next_back(), native_range.next_back());
+    }
+
+    #[kani::proof]
+    fn page_range_inclusive_next_back() {
+        page_range_inclusive_next_back_harness(false);
+    }
+
+    #[kani::proof]
+    #[kani::should_panic]
+    fn page_range_inclusive_next_back_panic() {
+        page_range_inclusive_next_back_harness(true);
+    }
+}

From fe0cb22582ccbd47d897566b74bfb88e28e63642 Mon Sep 17 00:00:00 2001
From: Tom Dohrmann <erbse.13@gmx.de>
Date: Sun, 10 May 2026 16:37:08 +0200
Subject: [PATCH 05/10] implement DoubleEndedIterator for
 PhysFrameRange/PhysFrameRangeInclusive

---
 src/structures/paging/frame.rs | 24 ++++++++++++++++++++++++
 1 file changed, 24 insertions(+)

diff --git a/src/structures/paging/frame.rs b/src/structures/paging/frame.rs
index c4a8c97a..ecf5b837 100644
--- a/src/structures/paging/frame.rs
+++ b/src/structures/paging/frame.rs
@@ -181,6 +181,18 @@ impl<S: PageSize> Iterator for PhysFrameRange<S> {
     }
 }
 
+impl<S: PageSize> DoubleEndedIterator for PhysFrameRange<S> {
+    #[inline]
+    fn next_back(&mut self) -> Option<Self::Item> {
+        if self.start < self.end {
+            self.end -= 1;
+            Some(self.end)
+        } else {
+            None
+        }
+    }
+}
+
 impl<S: PageSize> fmt::Debug for PhysFrameRange<S> {
     fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
         f.debug_struct("PhysFrameRange")
@@ -239,6 +251,18 @@ impl<S: PageSize> Iterator for PhysFrameRangeInclusive<S> {
     }
 }
 
+impl<S: PageSize> DoubleEndedIterator for PhysFrameRangeInclusive<S> {
+    #[inline]
+    fn next_back(&mut self) -> Option<Self::Item> {
+        if self.start <= self.end {
+            self.end -= 1;
+            Some(self.end)
+        } else {
+            None
+        }
+    }
+}
+
 impl<S: PageSize> fmt::Debug for PhysFrameRangeInclusive<S> {
     fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
         f.debug_struct("PhysFrameRangeInclusive")

From b316d9dc5e6893a1f9e4cb4fbf5edd6f195541c4 Mon Sep 17 00:00:00 2001
From: Tom Dohrmann <erbse.13@gmx.de>
Date: Sun, 10 May 2026 17:29:38 +0200
Subject: [PATCH 06/10] implement size_hint for iterator

---
 src/structures/paging/frame.rs | 15 +++++++++++++++
 src/structures/paging/page.rs  | 19 +++++++++++++++----
 2 files changed, 30 insertions(+), 4 deletions(-)

diff --git a/src/structures/paging/frame.rs b/src/structures/paging/frame.rs
index ecf5b837..bfbfa574 100644
--- a/src/structures/paging/frame.rs
+++ b/src/structures/paging/frame.rs
@@ -3,6 +3,7 @@
 use super::page::AddressNotAligned;
 use crate::structures::paging::page::{PageSize, Size4KiB};
 use crate::PhysAddr;
+use core::convert::TryFrom;
 use core::fmt;
 use core::marker::PhantomData;
 use core::ops::{Add, AddAssign, Sub, SubAssign};
@@ -179,6 +180,13 @@ impl<S: PageSize> Iterator for PhysFrameRange<S> {
             None
         }
     }
+
+    fn size_hint(&self) -> (usize, Option<usize>) {
+        let len = self.len();
+        usize::try_from(len)
+            .map(|len| (len, Some(len)))
+            .unwrap_or((usize::MAX, None))
+    }
 }
 
 impl<S: PageSize> DoubleEndedIterator for PhysFrameRange<S> {
@@ -249,6 +257,13 @@ impl<S: PageSize> Iterator for PhysFrameRangeInclusive<S> {
             None
         }
     }
+
+    fn size_hint(&self) -> (usize, Option<usize>) {
+        let len = self.len();
+        usize::try_from(len)
+            .map(|len| (len, Some(len)))
+            .unwrap_or((usize::MAX, None))
+    }
 }
 
 impl<S: PageSize> DoubleEndedIterator for PhysFrameRangeInclusive<S> {
diff --git a/src/structures/paging/page.rs b/src/structures/paging/page.rs
index 7af2e465..19948a86 100644
--- a/src/structures/paging/page.rs
+++ b/src/structures/paging/page.rs
@@ -4,6 +4,7 @@ use crate::sealed::Sealed;
 use crate::structures::paging::page_table::PageTableLevel;
 use crate::structures::paging::PageTableIndex;
 use crate::VirtAddr;
+use core::convert::TryFrom;
 use core::fmt;
 #[cfg(feature = "step_trait")]
 use core::iter::Step;
@@ -161,8 +162,6 @@ impl<S: PageSize> Page<S> {
     // FIXME: Move this into the `Step` impl, once `Step` is stabilized.
     #[cfg(any(feature = "instructions", feature = "step_trait"))]
     pub(crate) fn steps_between_impl(start: &Self, end: &Self) -> (usize, Option<usize>) {
-        use core::convert::TryFrom;
-
         if let Some(steps) =
             VirtAddr::steps_between_u64(&start.start_address(), &end.start_address())
         {
@@ -177,8 +176,6 @@ impl<S: PageSize> Page<S> {
     // FIXME: Move this into the `Step` impl, once `Step` is stabilized.
     #[cfg(any(feature = "instructions", feature = "step_trait"))]
     pub(crate) fn forward_checked_impl(start: Self, count: usize) -> Option<Self> {
-        use core::convert::TryFrom;
-
         let count = u64::try_from(count).ok()?.checked_mul(S::SIZE)?;
         let start_address = VirtAddr::forward_checked_u64(start.start_address, count)?;
         Some(Self {
@@ -371,6 +368,13 @@ impl<S: PageSize> Iterator for PageRange<S> {
             None
         }
     }
+
+    fn size_hint(&self) -> (usize, Option<usize>) {
+        let len = self.len();
+        usize::try_from(len)
+            .map(|len| (len, Some(len)))
+            .unwrap_or((usize::MAX, None))
+    }
 }
 
 impl<S: PageSize> DoubleEndedIterator for PageRange<S> {
@@ -461,6 +465,13 @@ impl<S: PageSize> Iterator for PageRangeInclusive<S> {
             None
         }
     }
+
+    fn size_hint(&self) -> (usize, Option<usize>) {
+        let len = self.len();
+        usize::try_from(len)
+            .map(|len| (len, Some(len)))
+            .unwrap_or((usize::MAX, None))
+    }
 }
 
 impl<S: PageSize> DoubleEndedIterator for PageRangeInclusive<S> {

From 42edcae64551f4c03a6a9ccc632453c2b06bbb08 Mon Sep 17 00:00:00 2001
From: Tom Dohrmann <erbse.13@gmx.de>
Date: Sun, 10 May 2026 19:35:56 +0200
Subject: [PATCH 07/10] implement nth for PageRange/PageRangeInclusive

---
 src/addr.rs                   |   1 -
 src/structures/paging/page.rs | 173 +++++++++++++++++++++++++++++++++-
 2 files changed, 169 insertions(+), 5 deletions(-)

diff --git a/src/addr.rs b/src/addr.rs
index 1a271120..ff29219e 100644
--- a/src/addr.rs
+++ b/src/addr.rs
@@ -259,7 +259,6 @@ impl VirtAddr {
     /// An implementation of steps_between that returns u64. Note that this
     /// function always returns the exact bound, so it doesn't need to return a
     /// lower and upper bound like steps_between does.
-    #[cfg(any(feature = "instructions", feature = "step_trait"))]
     pub(crate) fn steps_between_u64(start: &Self, end: &Self) -> Option<u64> {
         let mut steps = end.0.checked_sub(start.0)?;
 
diff --git a/src/structures/paging/page.rs b/src/structures/paging/page.rs
index 19948a86..6e278c46 100644
--- a/src/structures/paging/page.rs
+++ b/src/structures/paging/page.rs
@@ -159,13 +159,16 @@ impl<S: PageSize> Page<S> {
         PageRangeInclusive { start, end }
     }
 
+    // FIXME: Move this into the `Step` impl, once `Step` is stabilized.
+    pub(crate) fn steps_between_u64(start: &Self, end: &Self) -> Option<u64> {
+        VirtAddr::steps_between_u64(&start.start_address(), &end.start_address())
+            .map(|steps| steps / S::SIZE)
+    }
+
     // FIXME: Move this into the `Step` impl, once `Step` is stabilized.
     #[cfg(any(feature = "instructions", feature = "step_trait"))]
     pub(crate) fn steps_between_impl(start: &Self, end: &Self) -> (usize, Option<usize>) {
-        if let Some(steps) =
-            VirtAddr::steps_between_u64(&start.start_address(), &end.start_address())
-        {
-            let steps = steps / S::SIZE;
+        if let Some(steps) = Self::steps_between_u64(start, end) {
             let steps = usize::try_from(steps).ok();
             (steps.unwrap_or(usize::MAX), steps)
         } else {
@@ -369,6 +372,40 @@ impl<S: PageSize> Iterator for PageRange<S> {
         }
     }
 
+    fn nth(&mut self, n: usize) -> Option<Self::Item> {
+        if self.is_empty() {
+            return None;
+        }
+
+        // Convert to `u64`. If the value doesn't fit just use `u64::MAX`.
+        // `self.len()` is guaranteed to be smaller than the real value and
+        // `u64::MAX` anyway, so it doesn't make a difference.
+        let n = u64::try_from(n).unwrap_or(u64::MAX);
+
+        // Handling `n >= self.len()` is a bit more complicated because we
+        // can't just add `n` to `self.start`. Handle this by doing two steps,
+        // `self.len()-1` and `1`. This should return `None` (or panic).
+        if n >= self.len() {
+            self.nth(self.len() as usize - 1)?;
+            return self.next();
+        }
+
+        // Figure out how many steps there are until the address range gap.
+        let second_half_start = Page::<S>::containing_address(VirtAddr::new(0xffff_8000_0000_0000));
+        let steps_until_gap = Page::steps_between_u64(&self.start, &second_half_start)
+            .filter(|steps| *steps <= n && *steps > 0);
+        if let Some(steps_until_gap) = steps_until_gap {
+            // Jump just *before* the address range gap.
+            self.start += steps_until_gap - 1;
+            // Advancing one more time should panic.
+            self.next()?;
+            unreachable!("the previous call to `next` should have panicked")
+        }
+
+        self.start += n;
+        self.next()
+    }
+
     fn size_hint(&self) -> (usize, Option<usize>) {
         let len = self.len();
         usize::try_from(len)
@@ -466,6 +503,40 @@ impl<S: PageSize> Iterator for PageRangeInclusive<S> {
         }
     }
 
+    fn nth(&mut self, n: usize) -> Option<Self::Item> {
+        if self.is_empty() {
+            return None;
+        }
+
+        // Convert to `u64`. If the value doesn't fit just use `u64::MAX`.
+        // `self.len()` is guaranteed to be smaller than the real value and
+        // `u64::MAX` anyway, so it doesn't make a difference.
+        let n = u64::try_from(n).unwrap_or(u64::MAX);
+
+        // Handling `n >= self.len()` is a bit more complicated because we
+        // can't just add `n` to `self.start`. Handle this by doing two steps,
+        // `self.len()-1` and `1`. This should return `None` (or panic).
+        if n >= self.len() {
+            self.nth(self.len() as usize - 1)?;
+            return self.next();
+        }
+
+        // Figure out how many steps there are until the address range gap.
+        let second_half_start = Page::<S>::containing_address(VirtAddr::new(0xffff_8000_0000_0000));
+        let steps_until_gap = Page::steps_between_u64(&self.start, &second_half_start)
+            .filter(|steps| *steps <= n && *steps > 0);
+        if let Some(steps_until_gap) = steps_until_gap {
+            // Jump just *before* the address range gap.
+            self.start += steps_until_gap - 1;
+            // Advancing one more time should panic.
+            self.next()?;
+            unreachable!("the previous call to `next` should have panicked")
+        }
+
+        self.start += n;
+        self.next()
+    }
+
     fn size_hint(&self) -> (usize, Option<usize>) {
         let len = self.len();
         usize::try_from(len)
@@ -932,4 +1003,98 @@ mod proofs {
     fn page_range_inclusive_next_back_panic() {
         page_range_inclusive_next_back_harness(true);
     }
+
+    fn page_range_nth_harness(should_panic_mode: bool) {
+        let start = kani::any::<Page>();
+        let end = kani::any::<Page>();
+        let m = kani::any::<u64>();
+        let n = kani::any::<u64>();
+
+        // If the code is expected to panic, only run it in `#[should_panic]`
+        // mode.
+        let offset = m
+            .checked_add(n)
+            .and_then(|sum| sum.checked_add(2))
+            .and_then(|sum| sum.checked_mul(Size4KiB::SIZE));
+        let expected_end =
+            offset.and_then(|offset| start.start_address().as_u64().checked_add(offset));
+        let should_panic = expected_end.is_some_and(|expected_end| {
+            start.start_address().as_u64() <= 0x7fff_ffff_f000 && expected_end > 0x7fff_ffff_f000
+        }) || expected_end.is_none();
+        kani::assume(should_panic == should_panic_mode);
+
+        if should_panic {
+            // Calling `nth` should panic.
+            let mut our_range = Page::range(start, end);
+            our_range.nth(n as usize);
+            our_range.nth(m as usize);
+            return;
+        }
+
+        // Otherwise the results should match what `Range` returns.
+        let mut our_range = Page::range(start, end);
+        let mut native_range = start..end;
+        assert_eq!(our_range.nth(m as usize), native_range.nth(m as usize));
+        assert_eq!(our_range.nth(n as usize), native_range.nth(n as usize));
+    }
+
+    #[kani::proof]
+    #[kani::unwind(1)]
+    fn page_range_nth() {
+        page_range_nth_harness(false);
+    }
+
+    #[kani::proof]
+    #[kani::unwind(1)]
+    #[kani::should_panic]
+    fn page_range_nth_panic() {
+        page_range_nth_harness(true);
+    }
+
+    fn page_range_inclusive_nth_harness(should_panic_mode: bool) {
+        let start = kani::any::<Page>();
+        let end = kani::any::<Page>();
+        let m = kani::any::<u64>();
+        let n = kani::any::<u64>();
+
+        // If the code is expected to panic, only run it in `#[should_panic]`
+        // mode.
+        let offset = m
+            .checked_add(n)
+            .and_then(|sum| sum.checked_add(2))
+            .and_then(|sum| sum.checked_mul(Size4KiB::SIZE));
+        let expected_end =
+            offset.and_then(|offset| start.start_address().as_u64().checked_add(offset));
+        let should_panic = expected_end.is_some_and(|expected_end| {
+            start.start_address().as_u64() <= 0x7fff_ffff_f000 && expected_end > 0x7fff_ffff_f000
+        }) || expected_end.is_none();
+        kani::assume(should_panic == should_panic_mode);
+
+        if should_panic {
+            // Calling `nth` should panic.
+            let mut our_range = Page::range_inclusive(start, end);
+            our_range.nth(n as usize);
+            our_range.nth(m as usize);
+            return;
+        }
+
+        // Otherwise the results should match what `Range` returns.
+        let mut our_range = Page::range_inclusive(start, end);
+        let mut native_range = start..=end;
+        assert_eq!(our_range.nth(m as usize), native_range.nth(m as usize));
+        assert_eq!(our_range.nth(n as usize), native_range.nth(n as usize));
+    }
+
+    #[kani::proof]
+    #[kani::unwind(1)]
+    fn page_range_inclusive_nth() {
+        page_range_inclusive_nth_harness(false);
+    }
+
+    #[kani::proof]
+    #[kani::unwind(1)]
+    #[kani::should_panic]
+    fn page_range_inclusive_nth_panic() {
+        page_range_inclusive_nth_harness(true);
+    }
 }

From 3280ca222301a09fa56f27a4c2c1398d053e0ea6 Mon Sep 17 00:00:00 2001
From: Tom Dohrmann <erbse.13@gmx.de>
Date: Sun, 10 May 2026 21:07:39 +0200
Subject: [PATCH 08/10] implement nth_back for PageRange/PageRangeInclusive

---
 src/structures/paging/page.rs | 176 ++++++++++++++++++++++++++++++++++
 1 file changed, 176 insertions(+)

diff --git a/src/structures/paging/page.rs b/src/structures/paging/page.rs
index 6e278c46..42e0fa94 100644
--- a/src/structures/paging/page.rs
+++ b/src/structures/paging/page.rs
@@ -424,6 +424,40 @@ impl<S: PageSize> DoubleEndedIterator for PageRange<S> {
             None
         }
     }
+
+    fn nth_back(&mut self, n: usize) -> Option<Self::Item> {
+        if self.is_empty() {
+            return None;
+        }
+
+        // Convert to `u64`. If the value doesn't fit just use `u64::MAX`.
+        // `self.len()` is guaranteed to be smaller than the real value and
+        // `u64::MAX` anyway, so it doesn't make a difference.
+        let n = u64::try_from(n).unwrap_or(u64::MAX);
+
+        // Handling `n >= self.len()` is a bit more complicated because we
+        // can't just subtract `n` from `self.end`. Handle this by doing two
+        // steps, `self.len()-1` and `1`. This should return `None` (or panic).
+        if n >= self.len() {
+            self.nth_back(self.len() as usize - 1);
+            return self.next_back();
+        }
+
+        // Figure out how many steps there are until the address range gap.
+        let first_half_end = Page::<S>::containing_address(VirtAddr::new(0x7fff_ffff_f000));
+        let steps_until_gap = Page::steps_between_u64(&first_half_end, &self.end)
+            .filter(|steps| *steps <= n && *steps > 0);
+        if let Some(steps_until_gap) = steps_until_gap {
+            // Jump just *before* the address range gap.
+            self.end -= steps_until_gap - 1;
+            // Advancing one more time should panic.
+            self.next_back()?;
+            unreachable!("the previous call to `next_back` should have panicked")
+        }
+
+        self.end -= n;
+        self.next_back()
+    }
 }
 
 impl PageRange<Size2MiB> {
@@ -564,6 +598,40 @@ impl<S: PageSize> DoubleEndedIterator for PageRangeInclusive<S> {
             None
         }
     }
+
+    fn nth_back(&mut self, n: usize) -> Option<Self::Item> {
+        if self.is_empty() {
+            return None;
+        }
+
+        // Convert to `u64`. If the value doesn't fit just use `u64::MAX`.
+        // `self.len()` is guaranteed to be smaller than the real value and
+        // `u64::MAX` anyway, so it doesn't make a difference.
+        let n = u64::try_from(n).unwrap_or(u64::MAX);
+
+        // Handling `n >= self.len()` is a bit more complicated because we
+        // can't just subtract `n` from `self.end`. Handle this by doing two
+        // steps, `self.len()-1` and `1`. This should return `None` (or panic).
+        if n >= self.len() {
+            self.nth_back(self.len() as usize - 1);
+            return self.next_back();
+        }
+
+        // Figure out how many steps there are until the address range gap.
+        let first_half_end = Page::<S>::containing_address(VirtAddr::new(0x7fff_ffff_f000));
+        let steps_until_gap = Page::steps_between_u64(&first_half_end, &self.end)
+            .filter(|steps| *steps <= n && *steps > 0);
+        if let Some(steps_until_gap) = steps_until_gap {
+            // Jump just *before* the address range gap.
+            self.end -= steps_until_gap - 1;
+            // Advancing one more time should panic.
+            self.next_back()?;
+            unreachable!("the previous call to `next_back` should have panicked")
+        }
+
+        self.end -= n;
+        self.next_back()
+    }
 }
 
 impl<S: PageSize> fmt::Debug for PageRangeInclusive<S> {
@@ -1051,6 +1119,60 @@ mod proofs {
         page_range_nth_harness(true);
     }
 
+    fn page_range_nth_back_harness(should_panic_mode: bool) {
+        let start = kani::any::<Page>();
+        let end = kani::any::<Page>();
+        let m = kani::any::<u64>();
+        let n = kani::any::<u64>();
+
+        // If the code is expected to panic, only run it in `#[should_panic]`
+        // mode.
+        let offset = m
+            .checked_add(n)
+            .and_then(|sum| sum.checked_add(2))
+            .and_then(|sum| sum.checked_mul(Size4KiB::SIZE));
+        let expected_start =
+            offset.and_then(|offset| end.start_address().as_u64().checked_sub(offset));
+        let should_panic = expected_start.is_some_and(|expected_start| {
+            expected_start <= 0xffff_7fff_ffff_f000
+                && end.start_address().as_u64() > 0xffff_7fff_ffff_f000
+        }) || expected_start.is_none();
+        kani::assume(should_panic == should_panic_mode);
+
+        if should_panic {
+            // Calling `nth_back` should panic.
+            let mut our_range = Page::range(start, end);
+            our_range.nth_back(n as usize);
+            our_range.nth_back(m as usize);
+            return;
+        }
+
+        // Otherwise the results should match what `Range` returns.
+        let mut our_range = Page::range(start, end);
+        let mut native_range = start..end;
+        assert_eq!(
+            our_range.nth_back(m as usize),
+            native_range.nth_back(m as usize)
+        );
+        assert_eq!(
+            our_range.nth_back(n as usize),
+            native_range.nth_back(n as usize)
+        );
+    }
+
+    #[kani::proof]
+    #[kani::unwind(1)]
+    fn page_range_nth_back() {
+        page_range_nth_back_harness(false);
+    }
+
+    #[kani::proof]
+    #[kani::unwind(1)]
+    #[kani::should_panic]
+    fn page_range_nth_back_panic() {
+        page_range_nth_back_harness(true);
+    }
+
     fn page_range_inclusive_nth_harness(should_panic_mode: bool) {
         let start = kani::any::<Page>();
         let end = kani::any::<Page>();
@@ -1097,4 +1219,58 @@ mod proofs {
     fn page_range_inclusive_nth_panic() {
         page_range_inclusive_nth_harness(true);
     }
+
+    fn page_range_inclusive_nth_back_harness(should_panic_mode: bool) {
+        let start = kani::any::<Page>();
+        let end = kani::any::<Page>();
+        let m = kani::any::<u64>();
+        let n = kani::any::<u64>();
+
+        // If the code is expected to panic, only run it in `#[should_panic]`
+        // mode.
+        let offset = m
+            .checked_add(n)
+            .and_then(|sum| sum.checked_add(2))
+            .and_then(|sum| sum.checked_mul(Size4KiB::SIZE));
+        let expected_start =
+            offset.and_then(|offset| end.start_address().as_u64().checked_sub(offset));
+        let should_panic = expected_start.is_some_and(|expected_start| {
+            expected_start <= 0xffff_7fff_ffff_f000
+                && end.start_address().as_u64() > 0xffff_7fff_ffff_f000
+        }) || expected_start.is_none();
+        kani::assume(should_panic == should_panic_mode);
+
+        if should_panic {
+            // Calling `nth_back` should panic.
+            let mut our_range = Page::range_inclusive(start, end);
+            our_range.nth_back(n as usize);
+            our_range.nth_back(m as usize);
+            return;
+        }
+
+        // Otherwise the results should match what `Range` returns.
+        let mut our_range = Page::range_inclusive(start, end);
+        let mut native_range = start..=end;
+        assert_eq!(
+            our_range.nth_back(m as usize),
+            native_range.nth_back(m as usize)
+        );
+        assert_eq!(
+            our_range.nth_back(n as usize),
+            native_range.nth_back(n as usize)
+        );
+    }
+
+    #[kani::proof]
+    #[kani::unwind(1)]
+    fn page_range_inclusive_nth_back() {
+        page_range_inclusive_nth_back_harness(false);
+    }
+
+    #[kani::proof]
+    #[kani::unwind(1)]
+    #[kani::should_panic]
+    fn page_range_inclusive_nth_back_panic() {
+        page_range_inclusive_nth_back_harness(true);
+    }
 }

From 4518e3f8f6660cd8c8cb0dcad314fead192edc01 Mon Sep 17 00:00:00 2001
From: Tom Dohrmann <erbse.13@gmx.de>
Date: Sun, 17 May 2026 15:02:50 +0200
Subject: [PATCH 09/10] implement nth for
 PhysFrameRange/PhysFrameRangeInclusive

---
 src/structures/paging/frame.rs | 46 ++++++++++++++++++++++++++++++++++
 1 file changed, 46 insertions(+)

diff --git a/src/structures/paging/frame.rs b/src/structures/paging/frame.rs
index bfbfa574..1b21de6f 100644
--- a/src/structures/paging/frame.rs
+++ b/src/structures/paging/frame.rs
@@ -181,6 +181,29 @@ impl<S: PageSize> Iterator for PhysFrameRange<S> {
         }
     }
 
+    fn nth(&mut self, n: usize) -> Option<Self::Item> {
+        if self.is_empty() {
+            return None;
+        }
+
+        // Convert to `u64`. If the value doesn't fit just use `u64::MAX`.
+        // `self.len()` is guaranteed to be smaller than the real value and
+        // `u64::MAX` anyway, so it doesn't make a difference.
+        let n = u64::try_from(n).unwrap_or(u64::MAX);
+
+        // Handling `n >= self.len()` is a bit more complicated because we
+        // can't just add `n` to `self.start` (it might overflow). Handle this
+        // by doing two steps, `self.len()-1` and `1`. This should return
+        // `None`.
+        if n >= self.len() {
+            self.nth(self.len() as usize - 1)?;
+            return self.next();
+        }
+
+        self.start += n;
+        self.next()
+    }
+
     fn size_hint(&self) -> (usize, Option<usize>) {
         let len = self.len();
         usize::try_from(len)
@@ -258,6 +281,29 @@ impl<S: PageSize> Iterator for PhysFrameRangeInclusive<S> {
         }
     }
 
+    fn nth(&mut self, n: usize) -> Option<Self::Item> {
+        if self.is_empty() {
+            return None;
+        }
+
+        // Convert to `u64`. If the value doesn't fit just use `u64::MAX`.
+        // `self.len()` is guaranteed to be smaller than the real value and
+        // `u64::MAX` anyway, so it doesn't make a difference.
+        let n = u64::try_from(n).unwrap_or(u64::MAX);
+
+        // Handling `n >= self.len()` is a bit more complicated because we
+        // can't just add `n` to `self.start` (it might overflow). Handle this
+        // by doing two steps, `self.len()-1` and `1`. This should return
+        // `None`.
+        if n >= self.len() {
+            self.nth(self.len() as usize - 1)?;
+            return self.next();
+        }
+
+        self.start += n;
+        self.next()
+    }
+
     fn size_hint(&self) -> (usize, Option<usize>) {
         let len = self.len();
         usize::try_from(len)

From 2700117ff81dabd2a284ced217839c112d463e3c Mon Sep 17 00:00:00 2001
From: Tom Dohrmann <erbse.13@gmx.de>
Date: Sun, 17 May 2026 15:03:23 +0200
Subject: [PATCH 10/10] implement nth_back for
 PhysFrameRange/PhysFrameRangeInclusive

---
 src/structures/paging/frame.rs | 46 ++++++++++++++++++++++++++++++++++
 1 file changed, 46 insertions(+)

diff --git a/src/structures/paging/frame.rs b/src/structures/paging/frame.rs
index 1b21de6f..4633eb52 100644
--- a/src/structures/paging/frame.rs
+++ b/src/structures/paging/frame.rs
@@ -222,6 +222,29 @@ impl<S: PageSize> DoubleEndedIterator for PhysFrameRange<S> {
             None
         }
     }
+
+    fn nth_back(&mut self, n: usize) -> Option<Self::Item> {
+        if self.is_empty() {
+            return None;
+        }
+
+        // Convert to `u64`. If the value doesn't fit just use `u64::MAX`.
+        // `self.len()` is guaranteed to be smaller than the real value and
+        // `u64::MAX` anyway, so it doesn't make a difference.
+        let n = u64::try_from(n).unwrap_or(u64::MAX);
+
+        // Handling `n >= self.len()` is a bit more complicated because we
+        // can't just subtract `n` to `self.end` (it might overflow). Handle
+        // this by doing two steps, `self.len()-1` and `1`. This should return
+        // `None`.
+        if n >= self.len() {
+            self.nth_back(self.len() as usize - 1)?;
+            return self.next_back();
+        }
+
+        self.end -= n;
+        self.next_back()
+    }
 }
 
 impl<S: PageSize> fmt::Debug for PhysFrameRange<S> {
@@ -322,6 +345,29 @@ impl<S: PageSize> DoubleEndedIterator for PhysFrameRangeInclusive<S> {
             None
         }
     }
+
+    fn nth_back(&mut self, n: usize) -> Option<Self::Item> {
+        if self.is_empty() {
+            return None;
+        }
+
+        // Convert to `u64`. If the value doesn't fit just use `u64::MAX`.
+        // `self.len()` is guaranteed to be smaller than the real value and
+        // `u64::MAX` anyway, so it doesn't make a difference.
+        let n = u64::try_from(n).unwrap_or(u64::MAX);
+
+        // Handling `n >= self.len()` is a bit more complicated because we
+        // can't just subtract `n` to `self.end` (it might overflow). Handle
+        // this by doing two steps, `self.len()-1` and `1`. This should return
+        // `None`.
+        if n >= self.len() {
+            self.nth_back(self.len() as usize - 1)?;
+            return self.next_back();
+        }
+
+        self.end -= n;
+        self.next_back()
+    }
 }
 
 impl<S: PageSize> fmt::Debug for PhysFrameRangeInclusive<S> {