From 08499b69901ba1e5ca1091f884878d1d70061234 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 b0b544b6..e2216321 100644 --- a/src/addr.rs +++ b/src/addr.rs @@ -717,6 +717,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) + }) + } +} + #[cfg(kani)] impl kani::Arbitrary for PhysAddr { fn any() -> Self { From 4801e48223eaa1af32ca96f0e28dc1de422489ea 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 | 43 ++++++++++++++++++++++++++++++++++ 1 file changed, 43 insertions(+) diff --git a/src/structures/paging/frame.rs b/src/structures/paging/frame.rs index 95015969..0768bee2 100644 --- a/src/structures/paging/frame.rs +++ b/src/structures/paging/frame.rs @@ -5,6 +5,8 @@ use crate::structures::paging::page::{PageSize, Size4KiB}; use crate::PhysAddr; 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}; @@ -133,6 +135,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 1ee19b9b0a428d9ddd633983dc86140dfaca09bf 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 | 270 ++++++++++++++++++++++++++-------------------------- 1 file changed, 137 insertions(+), 133 deletions(-) diff --git a/src/addr.rs b/src/addr.rs index e2216321..fcbef997 100644 --- a/src/addr.rs +++ b/src/addr.rs @@ -1018,139 +1018,143 @@ 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 = kani::any::(); - let start_raw = start.as_u64(); - - // 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 = kani::any::(); + let start_raw = start.as_u64(); + + // 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 = kani::any::(); + + 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 = kani::any::(); + 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 = kani::any::(); + 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 = kani::any::(); + 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 = kani::any::(); + let end = kani::any::(); + + // 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 = kani::any::(); - - 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 = kani::any::(); - 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 = kani::any::(); - 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 = kani::any::(); - 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 = kani::any::(); - let end = kani::any::(); - - // 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 4b229b8ccdfc6bdce7a6a6f20b743a75ef86b81e 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 fcbef997..8eca8625 100644 --- a/src/addr.rs +++ b/src/addr.rs @@ -1157,4 +1157,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 16815bb4842ddef4e470ee850fe500303a89144d 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 | 113 +++++++++++++++++++++++++++++++++ 1 file changed, 113 insertions(+) diff --git a/src/structures/paging/frame.rs b/src/structures/paging/frame.rs index 0768bee2..c93209ed 100644 --- a/src/structures/paging/frame.rs +++ b/src/structures/paging/frame.rs @@ -655,4 +655,117 @@ mod proofs { range.nth_back(m); assert_eq!(range.nth_back(n), range2.nth_back(sum)); } + + // 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); + } }