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.

Author: Freax13

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