From 8d352824bcd8fc5ad7c5c29829778aa7478c22c7 Mon Sep 17 00:00:00 2001 From: Tom Dohrmann Date: Sat, 15 Nov 2025 09:36:51 +0100 Subject: [PATCH 1/5] implement Step for PhysAddr --- src/addr.rs | 19 +++++++++++++++++++ 1 file changed, 19 insertions(+) diff --git a/src/addr.rs b/src/addr.rs index bd6692e5..fbbb702b 100644 --- a/src/addr.rs +++ b/src/addr.rs @@ -711,6 +711,25 @@ impl Sub for PhysAddr { } } +#[cfg(feature = "step_trait")] +impl Step for PhysAddr { + fn steps_between(start: &Self, end: &Self) -> (usize, Option) { + Step::steps_between(&start.as_u64(), &end.as_u64()) + } + + fn forward_checked(start: Self, count: usize) -> Option { + PhysAddr::try_new(Step::forward_checked(start.as_u64(), count)?).ok() + } + + fn backward_checked(start: Self, count: usize) -> Option { + let addr = Step::backward_checked(start.as_u64(), count)?; + Some(unsafe { + // SAFETY: There is no lower bound for valid addresses. + PhysAddr::new_unsafe(addr) + }) + } +} + /// Align address downwards. /// /// Returns the greatest `x` with alignment `align` so that `x <= addr`. From b5caae99d7b41bc96075600d0c976ff887bb35dc Mon Sep 17 00:00:00 2001 From: Tom Dohrmann Date: Sat, 15 Nov 2025 09:39:23 +0100 Subject: [PATCH 2/5] implement Step for PhysFrame --- src/structures/paging/frame.rs | 45 ++++++++++++++++++++++++++++++++++ 1 file changed, 45 insertions(+) diff --git a/src/structures/paging/frame.rs b/src/structures/paging/frame.rs index c4a8c97a..17e93e28 100644 --- a/src/structures/paging/frame.rs +++ b/src/structures/paging/frame.rs @@ -3,7 +3,11 @@ use super::page::AddressNotAligned; use crate::structures::paging::page::{PageSize, Size4KiB}; use crate::PhysAddr; +#[cfg(feature = "step_trait")] +use core::convert::TryFrom; use core::fmt; +#[cfg(feature = "step_trait")] +use core::iter::Step; use core::marker::PhantomData; use core::ops::{Add, AddAssign, Sub, SubAssign}; @@ -132,6 +136,47 @@ impl Sub> for PhysFrame { } } +#[cfg(feature = "step_trait")] +impl Step for PhysFrame +where + S: PageSize, +{ + fn steps_between(start: &Self, end: &Self) -> (usize, Option) { + let start = start.start_address().as_u64() / S::SIZE; + let end = end.start_address().as_u64() / S::SIZE; + Step::steps_between(&start, &end) + } + + fn forward_checked(start: Self, count: usize) -> Option { + let count = u64::try_from(count).ok()?; + let count = count.checked_mul(S::SIZE)?; + let addr = start.start_address.as_u64().checked_add(count)?; + let addr = PhysAddr::try_new(addr).ok()?; + Some(unsafe { + // SAFETY: `start` is a multiple of `S::SIZE` and we added + // multiples of `S::SIZE`, so `addr` is still a multiple of + // `S::SIZE`. + PhysFrame::from_start_address_unchecked(addr) + }) + } + + fn backward_checked(start: Self, count: usize) -> Option { + let count = u64::try_from(count).ok()?; + let count = count.checked_mul(S::SIZE)?; + let addr = start.start_address.as_u64().checked_sub(count)?; + let addr = unsafe { + // SAFETY: There is no lower bound for valid addresses. + PhysAddr::new_unsafe(addr) + }; + Some(unsafe { + // SAFETY: `start` is a multiple of `S::SIZE` and we subtracted + // multiples of `S::SIZE`, so `addr` is still a multiple of + // `S::SIZE`. + PhysFrame::from_start_address_unchecked(addr) + }) + } +} + /// An range of physical memory frames, exclusive the upper bound. #[derive(Clone, Copy, PartialEq, Eq, Hash)] #[repr(C)] From 347d459fced5d816fd6affec80ccb4fc12dda228 Mon Sep 17 00:00:00 2001 From: Tom Dohrmann Date: Sat, 15 Nov 2025 09:37:21 +0100 Subject: [PATCH 3/5] move existing kani harnessses for VirtAddr into module We'll have very similar harnesses for PhysAddr, so let's use a module to avoid name conflicts. --- src/addr.rs | 310 ++++++++++++++++++++++++++-------------------------- 1 file changed, 157 insertions(+), 153 deletions(-) diff --git a/src/addr.rs b/src/addr.rs index fbbb702b..18ea0473 100644 --- a/src/addr.rs +++ b/src/addr.rs @@ -1005,159 +1005,163 @@ mod tests { mod proofs { use super::*; - // The next two proof harnesses prove the correctness of the `forward` - // implementation of VirtAddr. - - // This harness proves that our implementation can correctly take 0 or 1 - // 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; - }; - - // Adding 0 to any address should always yield the same address. - let same = Step::forward(start, 0); - assert!(start == same); - - // Manually calculate the expected address after stepping once. - let expected = match start_raw { - // Adding 1 to addresses in this range don't require gap jumps, so - // we can just add 1. - 0x0000_0000_0000_0000..=0x0000_7fff_ffff_fffe => Some(start_raw + 1), - // Adding 1 to this address jumps the gap. - 0x0000_7fff_ffff_ffff => Some(0xffff_8000_0000_0000), - // The range of non-canonical addresses. - 0x0000_8000_0000_0000..=0xffff_7fff_ffff_ffff => unreachable!(), - // Adding 1 to addresses in this range don't require gap jumps, so - // we can just add 1. - 0xffff_8000_0000_0000..=0xffff_ffff_ffff_fffe => Some(start_raw + 1), - // Adding 1 to this address causes an overflow. - 0xffff_ffff_ffff_ffff => None, - }; - if let Some(expected) = expected { - // Verify that `expected` is a valid address. - assert!(VirtAddr::try_new(expected).is_ok()); + mod virt_addr { + use super::*; + + // The next two proof harnesses prove the correctness of the `forward` + // implementation of VirtAddr. + + // This harness proves that our implementation can correctly take 0 or 1 + // 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; + }; + + // Adding 0 to any address should always yield the same address. + let same = Step::forward(start, 0); + assert!(start == same); + + // Manually calculate the expected address after stepping once. + let expected = match start_raw { + // Adding 1 to addresses in this range don't require gap jumps, so + // we can just add 1. + 0x0000_0000_0000_0000..=0x0000_7fff_ffff_fffe => Some(start_raw + 1), + // Adding 1 to this address jumps the gap. + 0x0000_7fff_ffff_ffff => Some(0xffff_8000_0000_0000), + // The range of non-canonical addresses. + 0x0000_8000_0000_0000..=0xffff_7fff_ffff_ffff => unreachable!(), + // Adding 1 to addresses in this range don't require gap jumps, so + // we can just add 1. + 0xffff_8000_0000_0000..=0xffff_ffff_ffff_fffe => Some(start_raw + 1), + // Adding 1 to this address causes an overflow. + 0xffff_ffff_ffff_ffff => None, + }; + if let Some(expected) = expected { + // Verify that `expected` is a valid address. + assert!(VirtAddr::try_new(expected).is_ok()); + } + // Verify `forward_checked`. + let next = Step::forward_checked(start, 1); + assert!(next.map(VirtAddr::as_u64) == expected); + } + + // This harness proves that the result of taking two small steps is the + // 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 count1: usize = kani::any(); + let count2: usize = kani::any(); + // If we can take two small steps... + let Some(next1) = Step::forward_checked(start, count1) else { + return; + }; + let Some(next2) = Step::forward_checked(next1, count2) else { + return; + }; + + // ...then we can also take one combined large step. + let count_both = count1 + count2; + let next_both = Step::forward(start, count_both); + assert!(next2 == next_both); + } + + // The next two proof harnesses prove the correctness of the `backward` + // implementation of VirtAddr using the `forward` implementation which + // we've already proven to be correct. + // They do this by proving the symmetry between those two functions. + + // This harness proves the correctness of the implementation of `backward` + // 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 count: usize = kani::any(); + + // If `forward_checked` succeeds... + let Some(end) = Step::forward_checked(start, count) else { + return; + }; + + // ...then `backward` succeeds as well. + let start2 = Step::backward(end, count); + assert!(start == start2); + } + + // This harness proves that for all inputs for which `backward_checked` + // 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 count: usize = kani::any(); + + // If `backward_checked` succeeds... + let Some(start) = Step::backward_checked(end, count) else { + return; + }; + + // ...then `forward` succeeds as well. + let end2 = Step::forward(start, count); + assert!(end == end2); + } + + // The next two proof harnesses prove the correctness of the + // `steps_between` implementation of VirtAddr using the `forward` + // implementation which we've already proven to be correct. + // They do this by proving the symmetry between those two functions. + + // This harness proves the correctness of the implementation of + // `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 count: usize = kani::any(); + + // If `forward_checked` succeeds... + let Some(end) = Step::forward_checked(start, count) else { + return; + }; + + // ...then `steps_between` succeeds as well. + assert!(Step::steps_between(&start, &end) == (count, Some(count))); + } + + // This harness proves that for all inputs for which `steps_between` + // 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; + }; + + // If `steps_between` succeeds... + let Some(count) = Step::steps_between(&start, &end).1 else { + return; + }; + + // ...then `forward` succeeds as well. + assert!(Step::forward(start, count) == end); } - // Verify `forward_checked`. - let next = Step::forward_checked(start, 1); - assert!(next.map(VirtAddr::as_u64) == expected); - } - - // This harness proves that the result of taking two small steps is the - // 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 count1: usize = kani::any(); - let count2: usize = kani::any(); - // If we can take two small steps... - let Some(next1) = Step::forward_checked(start, count1) else { - return; - }; - let Some(next2) = Step::forward_checked(next1, count2) else { - return; - }; - - // ...then we can also take one combined large step. - let count_both = count1 + count2; - let next_both = Step::forward(start, count_both); - assert!(next2 == next_both); - } - - // The next two proof harnesses prove the correctness of the `backward` - // implementation of VirtAddr using the `forward` implementation which - // we've already proven to be correct. - // They do this by proving the symmetry between those two functions. - - // This harness proves the correctness of the implementation of `backward` - // 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 count: usize = kani::any(); - - // If `forward_checked` succeeds... - let Some(end) = Step::forward_checked(start, count) else { - return; - }; - - // ...then `backward` succeeds as well. - let start2 = Step::backward(end, count); - assert!(start == start2); - } - - // This harness proves that for all inputs for which `backward_checked` - // 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 count: usize = kani::any(); - - // If `backward_checked` succeeds... - let Some(start) = Step::backward_checked(end, count) else { - return; - }; - - // ...then `forward` succeeds as well. - let end2 = Step::forward(start, count); - assert!(end == end2); - } - - // The next two proof harnesses prove the correctness of the - // `steps_between` implementation of VirtAddr using the `forward` - // implementation which we've already proven to be correct. - // They do this by proving the symmetry between those two functions. - - // This harness proves the correctness of the implementation of - // `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 count: usize = kani::any(); - - // If `forward_checked` succeeds... - let Some(end) = Step::forward_checked(start, count) else { - return; - }; - - // ...then `steps_between` succeeds as well. - assert!(Step::steps_between(&start, &end) == (count, Some(count))); - } - - // This harness proves that for all inputs for which `steps_between` - // 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; - }; - - // If `steps_between` succeeds... - let Some(count) = Step::steps_between(&start, &end).1 else { - return; - }; - - // ...then `forward` succeeds as well. - assert!(Step::forward(start, count) == end); } } From e928d479020cfe7dd373d1478a75992d8d2bbee3 Mon Sep 17 00:00:00 2001 From: Tom Dohrmann Date: Sat, 15 Nov 2025 09:38:13 +0100 Subject: [PATCH 4/5] add kani harnesses for PhysAddr's Step implementation The Step implementation uses unsafe. The kani harnesses should give us some confidence that the unsafe code is correct. --- src/addr.rs | 155 ++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 155 insertions(+) diff --git a/src/addr.rs b/src/addr.rs index 18ea0473..f3581d36 100644 --- a/src/addr.rs +++ b/src/addr.rs @@ -1164,4 +1164,159 @@ mod proofs { assert!(Step::forward(start, count) == end); } } + + mod phys_addr { + use super::*; + + // The next two proof harnesses prove the correctness of the `forward` + // implementation of PhysAddr. + + // This harness proves that our implementation can correctly take 0 or 1 + // step starting from any address. + #[kani::proof] + fn forward_base_case() { + let start_raw: u64 = kani::any(); + let Ok(start) = PhysAddr::try_new(start_raw) else { + return; + }; + + // Adding 0 to any address should always yield the same address. + let same = Step::forward(start, 0); + assert!(start == same); + + // Manually calculate the expected address after stepping once. + let expected = match start_raw { + // Adding 1 to addresses in this range will result in a valid + // address. + 0x0000_0000_0000_0000..=0xf_ffff_ffff_fffe => Some(start_raw + 1), + // Adding 1 to this address causes an overflow. + 0xf_ffff_ffff_ffff => None, + // Bigger addresses do not exist. + _ => unreachable!(), + }; + if let Some(expected) = expected { + // Verify that `expected` is a valid address. + assert!(PhysAddr::try_new(expected).is_ok()); + } + // Verify `forward_checked`. + let next = Step::forward_checked(start, 1); + assert!(next.map(PhysAddr::as_u64) == expected); + } + + // This harness proves that the result of taking two small steps is the + // same as taking one combined large step. + #[kani::proof] + fn forward_induction_step() { + let start_raw: u64 = kani::any(); + let Ok(start) = PhysAddr::try_new(start_raw) else { + return; + }; + + let count1: usize = kani::any(); + let count2: usize = kani::any(); + // If we can take two small steps... + let Some(next1) = Step::forward_checked(start, count1) else { + return; + }; + let Some(next2) = Step::forward_checked(next1, count2) else { + return; + }; + + // ...then we can also take one combined large step. + let count_both = count1 + count2; + let next_both = Step::forward(start, count_both); + assert!(next2 == next_both); + } + + // The next two proof harnesses prove the correctness of the `backward` + // implementation of PhysAddr using the `forward` implementation which + // we've already proven to be correct. + // They do this by proving the symmetry between those two functions. + + // This harness proves the correctness of the implementation of `backward` + // for all inputs for which `forward_checked` succeeds. + #[kani::proof] + fn forward_implies_backward() { + let start_raw: u64 = kani::any(); + let Ok(start) = PhysAddr::try_new(start_raw) else { + return; + }; + let count: usize = kani::any(); + + // If `forward_checked` succeeds... + let Some(end) = Step::forward_checked(start, count) else { + return; + }; + + // ...then `backward` succeeds as well. + let start2 = Step::backward(end, count); + assert!(start == start2); + } + + // This harness proves that for all inputs for which `backward_checked` + // succeeds, `forward` succeeds as well. + #[kani::proof] + fn backward_implies_forward() { + let end_raw: u64 = kani::any(); + let Ok(end) = PhysAddr::try_new(end_raw) else { + return; + }; + let count: usize = kani::any(); + + // If `backward_checked` succeeds... + let Some(start) = Step::backward_checked(end, count) else { + return; + }; + + // ...then `forward` succeeds as well. + let end2 = Step::forward(start, count); + assert!(end == end2); + } + + // The next two proof harnesses prove the correctness of the + // `steps_between` implementation of PhysAddr using the `forward` + // implementation which we've already proven to be correct. + // They do this by proving the symmetry between those two functions. + + // This harness proves the correctness of the implementation of + // `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) = PhysAddr::try_new(start) else { + return; + }; + let count: usize = kani::any(); + + // If `forward_checked` succeeds... + let Some(end) = Step::forward_checked(start, count) else { + return; + }; + + // ...then `steps_between` succeeds as well. + assert!(Step::steps_between(&start, &end) == (count, Some(count))); + } + + // This harness proves that for all inputs for which `steps_between` + // succeeds, `forward` succeeds as well. + #[kani::proof] + fn steps_between_implies_forward() { + let start: u64 = kani::any(); + let Ok(start) = PhysAddr::try_new(start) else { + return; + }; + let end: u64 = kani::any(); + let Ok(end) = PhysAddr::try_new(end) else { + return; + }; + + // If `steps_between` succeeds... + let Some(count) = Step::steps_between(&start, &end).1 else { + return; + }; + + // ...then `forward` succeeds as well. + assert!(Step::forward(start, count) == end); + } + } } From 4c11e1e954e85d67ee7f1586c3a711d3f0dc692f Mon Sep 17 00:00:00 2001 From: Tom Dohrmann Date: Sat, 15 Nov 2025 09:40:24 +0100 Subject: [PATCH 5/5] add kani harnesses for PhysFrame's Step implementation These harnesses check that PhysFrame behaves like PhysAddr with the steps scaled by the page size. --- src/structures/paging/frame.rs | 118 +++++++++++++++++++++++++++++++++ 1 file changed, 118 insertions(+) diff --git a/src/structures/paging/frame.rs b/src/structures/paging/frame.rs index 17e93e28..6a07ab7c 100644 --- a/src/structures/paging/frame.rs +++ b/src/structures/paging/frame.rs @@ -309,3 +309,121 @@ mod tests { assert_eq!(range_inclusive.len(), 51); } } + +#[cfg(kani)] +mod proofs { + use super::*; + + // This harness proves that steps_between will return the same value + // returned by PhysAddr's Step implementation scaled by Size4KiB::Size. + #[kani::proof] + fn steps_between() { + let start_raw: u64 = kani::any(); + let Ok(start) = PhysAddr::try_new(start_raw) else { + return; + }; + let Ok(start_frame) = PhysFrame::::from_start_address(start) else { + return; + }; + + let start_end: u64 = kani::any(); + let Ok(end) = PhysAddr::try_new(start_end) else { + return; + }; + let Ok(end_frame) = PhysFrame::::from_start_address(end) else { + return; + }; + + let (addr_min, addr_max) = PhysAddr::steps_between(&start, &end); + let (frame_min, frame_max) = PhysFrame::steps_between(&start_frame, &end_frame); + assert_eq!(addr_min / (Size4KiB::SIZE as usize), frame_min); + assert_eq!( + addr_max.map(|max| max / (Size4KiB::SIZE as usize)), + frame_max + ); + } + + // This harness proves that forward_checked will return the same value + // returned by PhysAddr's forward_checked implementation if the count has + // scaled by Size4KiB::Size. + #[kani::proof] + fn forward() { + let start_raw: u64 = kani::any(); + let Ok(start) = PhysAddr::try_new(start_raw) else { + return; + }; + let Ok(start_frame) = PhysFrame::::from_start_address(start) else { + return; + }; + + let count: usize = kani::any(); + let Some(scaled_count) = count.checked_mul(Size4KiB::SIZE as usize) else { + return; + }; + + let end_addr = PhysAddr::forward_checked(start, scaled_count); + let end_frame = PhysFrame::forward_checked(start_frame, count); + assert_eq!(end_addr, end_frame.map(PhysFrame::start_address)); + } + + // This harness proves that forward_checked will always return `None` if + // the count cannot be scaled by Size4KiB::SIZE. + #[kani::proof] + fn forward_limit() { + let start_raw: u64 = kani::any(); + let Ok(start) = PhysAddr::try_new(start_raw) else { + return; + }; + let Ok(start_frame) = PhysFrame::::from_start_address(start) else { + return; + }; + + let count: usize = kani::any(); + kani::assume(count.checked_mul(Size4KiB::SIZE as usize).is_none()); + + let end_frame = PhysFrame::forward_checked(start_frame, count); + assert_eq!(end_frame, None); + } + + // This harness proves that backward_checked will return the same value + // returned by PhysAddr's backward_checked implementation if the count has + // scaled by Size4KiB::Size. + #[kani::proof] + fn backward() { + let start_raw: u64 = kani::any(); + let Ok(start) = PhysAddr::try_new(start_raw) else { + return; + }; + let Ok(start_frame) = PhysFrame::::from_start_address(start) else { + return; + }; + + let count: usize = kani::any(); + let Some(scaled_count) = count.checked_mul(Size4KiB::SIZE as usize) else { + return; + }; + + let end_addr = PhysAddr::backward_checked(start, scaled_count); + let end_frame = PhysFrame::backward_checked(start_frame, count); + assert_eq!(end_addr, end_frame.map(PhysFrame::start_address)); + } + + // This harness proves that backward_checked will always return `None` if + // the count cannot be scaled by Size4KiB::SIZE. + #[kani::proof] + fn backward_limit() { + let start_raw: u64 = kani::any(); + let Ok(start) = PhysAddr::try_new(start_raw) else { + return; + }; + let Ok(start_frame) = PhysFrame::::from_start_address(start) else { + return; + }; + + let count: usize = kani::any(); + kani::assume(count.checked_mul(Size4KiB::SIZE as usize).is_none()); + + let end_frame = PhysFrame::backward_checked(start_frame, count); + assert_eq!(end_frame, None); + } +}