From 2c23c5459cf1d217323775f809f2b2893ca9a40c Mon Sep 17 00:00:00 2001
From: Tianshu Huang <tianshu.huang.g@gmail.com>
Date: Mon, 9 Nov 2026 18:45:58 -0800
Subject: [PATCH] Add contracts for <*const T>::read and <*mut T>::write

---
 .github/workflows/kani.yml        |  2 ++
 library/core/src/ptr/const_ptr.rs | 16 ++++++++++++++++
 library/core/src/ptr/mut_ptr.rs   | 18 ++++++++++++++++++
 3 files changed, 36 insertions(+)

diff --git a/.github/workflows/kani.yml b/.github/workflows/kani.yml
index 9488a1592f0b4..9afcf89908a9e 100644
--- a/.github/workflows/kani.yml
+++ b/.github/workflows/kani.yml
@@ -224,6 +224,8 @@ jobs:
             --include-pattern ptr::alignment::Alignment::mask \
             --include-pattern ptr::alignment::Alignment::new \
             --include-pattern ptr::alignment::Alignment::new_unchecked \
+            --include-pattern "ptr::const_ptr::<impl[[:space:]]\*const[[:space:]](.+)>::read$" \
+            --include-pattern "ptr::mut_ptr::<impl[[:space:]]\*mut[[:space:]](.+)>::write$" \
             --include-pattern time::Duration::from_micros \
             --include-pattern time::Duration::from_millis \
             --include-pattern time::Duration::from_nanos \
diff --git a/library/core/src/ptr/const_ptr.rs b/library/core/src/ptr/const_ptr.rs
index 4207d48bdb70d..ff172b809e91a 100644
--- a/library/core/src/ptr/const_ptr.rs
+++ b/library/core/src/ptr/const_ptr.rs
@@ -1264,6 +1264,8 @@ impl<T: PointeeSized> *const T {
     #[rustc_const_stable(feature = "const_ptr_read", since = "1.71.0")]
     #[inline(always)]
     #[track_caller]
+    // Safety precondition from `ptr::read`: `self` must be valid for reads and properly aligned.
+    #[requires(core::ub_checks::can_dereference(self))]
     pub const unsafe fn read(self) -> T
     where
         T: Sized,
@@ -2771,4 +2773,18 @@ mod verify {
     //         ptr_caller.byte_offset_from(ptr_input);
     //     }
     // }
+
+    // An in-bounds pointer into the generator's buffer; the precondition (`can_dereference`)
+    // is assumed on it, which prunes the misaligned and uninitialized offsets.
+    #[kani::proof_for_contract(<*const i32>::read)]
+    pub fn check_const_read_i32() {
+        const BUF_SIZE: usize = 8;
+        let mut generator = kani::PointerGenerator::<BUF_SIZE>::new();
+        let test_ptr: *const i32 = generator.any_in_bounds().ptr;
+        unsafe {
+            let val = test_ptr.read();
+            // Read back the value and assert it's correct
+            assert_eq!(val, *test_ptr);
+        }
+    }
 }
diff --git a/library/core/src/ptr/mut_ptr.rs b/library/core/src/ptr/mut_ptr.rs
index 90a04a13dd78d..e1614e5797719 100644
--- a/library/core/src/ptr/mut_ptr.rs
+++ b/library/core/src/ptr/mut_ptr.rs
@@ -1522,6 +1522,9 @@ impl<T: PointeeSized> *mut T {
     #[rustc_const_stable(feature = "const_ptr_write", since = "1.83.0")]
     #[inline(always)]
     #[track_caller]
+    // Safety precondition from `ptr::write`: `self` must be valid for writes and properly aligned.
+    #[requires(core::ub_checks::can_write(self))]
+    #[cfg_attr(kani, kani::modifies(self))]
     pub const unsafe fn write(self, val: T)
     where
         T: Sized,
@@ -3155,4 +3158,19 @@ mod verify {
     //         ptr_caller.byte_offset_from(ptr_input);
     //     }
     // }
+
+    // An in-bounds pointer into the generator's buffer; the precondition (`can_write`)
+    // is assumed on it, which prunes the misaligned offsets.
+    #[kani::proof_for_contract(<*mut i32>::write)]
+    pub fn check_mut_write_i32() {
+        const BUF_SIZE: usize = 8;
+        let mut generator = kani::PointerGenerator::<BUF_SIZE>::new();
+        let test_ptr: *mut i32 = generator.any_in_bounds().ptr;
+        let val: i32 = kani::any();
+        unsafe {
+            test_ptr.write(val);
+            // Read back the value and assert it's correct
+            assert_eq!(*test_ptr, val);
+        }
+    }
 }