Close Challenges 6 & 14; remove optional correctness work in Challenge 12

doc/src/challenges/0006-nonnull.md

@@ -1,11 +1,11 @@
 # Challenge 6: Safety of NonNull
 
-- **Status:** Open
+- **Status:** Resolved
 - **Tracking Issue:** [#53](https://github.com/model-checking/verify-rust-std/issues/53)
 - **Start date:** *2024/08/16*
 - **End date:** *2025/04/10*
 - **Reward:** *N/A*
-
+- **Contributors**: [Quinyuan Wu](https://github.com/QinyuanWu), [Daniel Tu](https://github.com/danielhumanmod), [Dhvani Kapadia](https://github.com/Dhvani-Kapadia) and [Jiun Chi Yang](https://github.com/Jimmycreative)
 -------------------
 
 

doc/src/challenges/0008-smallsort.md

@@ -11,8 +11,7 @@
 
 ## Goal
 
-The implementations of the traits `StableSmallSortTypeImpl`, `UnstableSmallSortTypeImpl`, and `UnstableSmallSortFreezeTypeImpl` in the `smallsort` [module](https://github.com/rust-lang/rust/blob/master/library/core/src/slice/sort/shared/smallsort.rs) of the Rust standard library are the sorting
-algorithms optimized for slices with small lengths.
+The implementations of the traits `StableSmallSortTypeImpl`, `UnstableSmallSortTypeImpl`, and `UnstableSmallSortFreezeTypeImpl` in the `smallsort` [module](https://github.com/rust-lang/rust/blob/master/library/core/src/slice/sort/shared/smallsort.rs) of the Rust standard library are the sorting algorithms with optimized implementations for slices with small lengths.
 In this challenge, the goal is to, first prove the memory safety of the public functions in the `smallsort` module, and, second, write contracts for them to
 show that the sorting algorithms actually sort the slices.
 

doc/src/challenges/0012-nonzero.md

@@ -73,7 +73,6 @@ Verify the safety of the following functions and methods (all located within `co
 |  `from_mut`   |
 |  `from_mut_unchecked` |
 
-You are not required to write correctness contracts for these methods (e.g., for `max`, ensuring that the `result` is indeed the maximum of the inputs), but it would be great to do so!
 
 ### List of UBs
 

doc/src/challenges/0014-convert-num.md

@@ -1,11 +1,11 @@
 # Challenge 14: Safety of Primitive Conversions
 
-- **Status:** Open
+- **Status:** Resolved
 - **Tracking Issue:** https://github.com/model-checking/verify-rust-std/issues/220
 - **Start date:** 2024/12/15
 - **End date:** 2025/2/28
 - **Prize:** *TBD*
-
+- **Contributors**: [Shoyu Vanilla](https://github.com/ShoyuVanilla)
 -------------------
 
 ## Goal

library/core/src/ptr/non_null.rs

@@ -1213,6 +1213,8 @@ impl<T: ?Sized> NonNull<T> {
     #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
     #[stable(feature = "non_null_convenience", since = "1.80.0")]
     #[rustc_const_stable(feature = "const_ptr_write", since = "1.83.0")]
+    #[cfg_attr(kani, kani::modifies(self.as_ptr()))]
+    #[requires(ub_checks::can_write(self.as_ptr()))]
     pub const unsafe fn write(self, val: T)
     where
         T: Sized,
@@ -1232,6 +1234,13 @@ impl<T: ?Sized> NonNull<T> {
     #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
     #[stable(feature = "non_null_convenience", since = "1.80.0")]
     #[rustc_const_stable(feature = "const_ptr_write", since = "1.83.0")]
+    #[cfg_attr(kani, kani::modifies(crate::ptr::slice_from_raw_parts(self.as_ptr(), count)))]
+    #[requires(
+        count.checked_mul(core::mem::size_of::<T>() as usize).is_some_and(|byte_count| byte_count.wrapping_add(self.as_ptr() as usize) <= isize::MAX as usize) &&
+        ub_checks::can_write(core::ptr::slice_from_raw_parts_mut(self.as_ptr(), count))
+    )]
+    #[ensures(|_|
+        ub_checks::can_dereference(crate::ptr::slice_from_raw_parts(self.as_ptr() as *const u8, count * size_of::<T>())))]
     pub const unsafe fn write_bytes(self, val: u8, count: usize)
     where
         T: Sized,
@@ -1275,6 +1284,8 @@ impl<T: ?Sized> NonNull<T> {
     #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
     #[stable(feature = "non_null_convenience", since = "1.80.0")]
     #[rustc_const_stable(feature = "const_ptr_write", since = "1.83.0")]
+    #[cfg_attr(kani, kani::modifies(self.as_ptr()))]
+    #[requires(ub_checks::can_write_unaligned(self.as_ptr()))]
     pub const unsafe fn write_unaligned(self, val: T)
     where
         T: Sized,
@@ -2535,12 +2546,143 @@ mod verify {
         }
     }
 
+    macro_rules! generate_write_harness {
+        ($type:ty, $harness_name:ident) => {
+            #[kani::proof_for_contract(NonNull::write)]
+            pub fn $harness_name() {
+                // Create a pointer generator for the given type with appropriate byte size
+                const ARR_SIZE: usize = mem::size_of::<$type>() * 100;
+                let mut generator = kani::PointerGenerator::<ARR_SIZE>::new();
+
+                // Get a raw pointer from the generator
+                let raw_ptr: *mut $type = generator.any_in_bounds().ptr;
+
+                // Create a non-null pointer from the raw pointer
+                let ptr = NonNull::new(raw_ptr).unwrap();
+
+                // Create a non-deterministic value to write
+                let new_value: $type = kani::any();
+
+                unsafe {
+                    // Perform the volatile write operation
+                    ptr.write(new_value);
+
+                    // Read back the value and assert it's correct
+                    assert_eq!(ptr.as_ptr().read(), new_value);
+                }
+            }
+        };
+    }
+
+    #[kani::proof_for_contract(NonNull::write)]
+    pub fn non_null_check_write_unit() {
+        // Create a pointer generator for the given type with appropriate byte size
+        let mut generator = kani::PointerGenerator::<1>::new();
+
+        // Get a raw pointer from the generator
+        let raw_ptr: *mut () = generator.any_in_bounds().ptr;
+
+        // Create a non-null pointer from the raw pointer
+        let ptr = NonNull::new(raw_ptr).unwrap();
+
+        // Create a non-deterministic value to write
+        let new_value: () = kani::any();
+
+        unsafe {
+            // Perform the volatile write operation
+            ptr.write(new_value);
+
+            // Read back the value and assert it's correct
+            assert_eq!(ptr.as_ptr().read(), new_value);
+        }
+    }
+
+    // Generate proof harnesses for multiple types with appropriate byte sizes
+    generate_write_harness!(i8, non_null_check_write_i8);
+    generate_write_harness!(i16, non_null_check_write_i16);
+    generate_write_harness!(i32, non_null_check_write_i32);
+    generate_write_harness!(i64, non_null_check_write_i64);
+    generate_write_harness!(i128, non_null_check_write_i128);
+    generate_write_harness!(isize, non_null_check_write_isize);
+    generate_write_harness!(u8, non_null_check_write_u8);
+    generate_write_harness!(u16, non_null_check_write_u16);
+    generate_write_harness!(u32, non_null_check_write_u32);
+    generate_write_harness!(u64, non_null_check_write_u64);
+    generate_write_harness!(u128, non_null_check_write_u128);
+    generate_write_harness!(usize, non_null_check_write_usize);
+
+    macro_rules! generate_write_unaligned_harness {
+        ($type:ty, $harness_name:ident) => {
+            #[kani::proof_for_contract(NonNull::write_unaligned)]
+            pub fn $harness_name() {
+                // Create a pointer generator for the given type with appropriate byte size
+                const ARR_SIZE: usize = mem::size_of::<$type>() * 100;
+                let mut generator = kani::PointerGenerator::<ARR_SIZE>::new();
+
+                // Get a raw pointer from the generator
+                let raw_ptr: *mut $type = generator.any_in_bounds().ptr;
+
+                // Create a non-null pointer from the raw pointer
+                let ptr = NonNull::new(raw_ptr).unwrap();
+
+                // Create a non-deterministic value to write
+                let new_value: $type = kani::any();
+
+                unsafe {
+                    // Perform the volatile write operation
+                    ptr.write_unaligned(new_value);
+
+                    // Read back the value and assert it's correct
+                    assert_eq!(ptr.as_ptr().read_unaligned(), new_value);
+                }
+            }
+        };
+    }
+
+    #[kani::proof_for_contract(NonNull::write_unaligned)]
+    pub fn non_null_check_write_unaligned_unit() {
+        // Create a pointer generator for the given type with appropriate byte size
+        let mut generator = kani::PointerGenerator::<1>::new();
+
+        // Get a raw pointer from the generator
+        let raw_ptr: *mut () = generator.any_in_bounds().ptr;
+
+        // Create a non-null pointer from the raw pointer
+        let ptr = NonNull::new(raw_ptr).unwrap();
+
+        // Create a non-deterministic value to write
+        let new_value: () = kani::any();
+
+        unsafe {
+            // Perform the volatile write operation
+            ptr.write_unaligned(new_value);
+
+            // Read back the value and assert it's correct
+            assert_eq!(ptr.as_ptr().read_unaligned(), new_value);
+        }
+    }
+
+    // Generate proof harnesses for multiple types with appropriate byte sizes
+    generate_write_unaligned_harness!(i8, non_null_check_write_unaligned_i8);
+    generate_write_unaligned_harness!(i16, non_null_check_write_unaligned_i16);
+    generate_write_unaligned_harness!(i32, non_null_check_write_unaligned_i32);
+    generate_write_unaligned_harness!(i64, non_null_check_write_unaligned_i64);
+    generate_write_unaligned_harness!(i128, non_null_check_write_unaligned_i128);
+    generate_write_unaligned_harness!(isize, non_null_check_write_unaligned_isize);
+    generate_write_unaligned_harness!(u8, non_null_check_write_unaligned_u8);
+    generate_write_unaligned_harness!(u16, non_null_check_write_unaligned_u16);
+    generate_write_unaligned_harness!(u32, non_null_check_write_unaligned_u32);
+    generate_write_unaligned_harness!(u64, non_null_check_write_unaligned_u64);
+    generate_write_unaligned_harness!(u128, non_null_check_write_unaligned_u128);
+    generate_write_unaligned_harness!(usize, non_null_check_write_unaligned_usize);
+
     macro_rules! generate_write_volatile_harness {
-        ($type:ty, $byte_size:expr, $harness_name:ident) => {
+        ($type:ty, $harness_name:ident) => {
             #[kani::proof_for_contract(NonNull::write_volatile)]
             pub fn $harness_name() {
                 // Create a pointer generator for the given type with appropriate byte size
-                let mut generator = kani::PointerGenerator::<$byte_size>::new();
+                const ARR_SIZE: usize = mem::size_of::<$type>() * 100;
+                let mut generator = kani::PointerGenerator::<ARR_SIZE>::new();
 
                 // Get a raw pointer from the generator
                 let raw_ptr: *mut $type = generator.any_in_bounds().ptr;
@@ -2562,28 +2704,114 @@ mod verify {
         };
     }
 
+    #[kani::proof_for_contract(NonNull::write_volatile)]
+    pub fn non_null_check_write_volatile_unit() {
+        // Create a pointer generator for the given type with appropriate byte size
+        let mut generator = kani::PointerGenerator::<1>::new();
+
+        // Get a raw pointer from the generator
+        let raw_ptr: *mut () = generator.any_in_bounds().ptr;
+
+        // Create a non-null pointer from the raw pointer
+        let ptr = NonNull::new(raw_ptr).unwrap();
+
+        // Create a non-deterministic value to write
+        let new_value: () = kani::any();
+
+        unsafe {
+            // Perform the volatile write operation
+            ptr.write_volatile(new_value);
+
+            // Read back the value and assert it's correct
+            assert_eq!(ptr.as_ptr().read_volatile(), new_value);
+        }
+    }
+
+    // Generate proof harnesses for multiple types with appropriate byte sizes
+    generate_write_volatile_harness!(i8, non_null_check_write_volatile_i8);
+    generate_write_volatile_harness!(i16, non_null_check_write_volatile_i16);
+    generate_write_volatile_harness!(i32, non_null_check_write_volatile_i32);
+    generate_write_volatile_harness!(i64, non_null_check_write_volatile_i64);
+    generate_write_volatile_harness!(i128, non_null_check_write_volatile_i128);
+    generate_write_volatile_harness!(isize, non_null_check_write_volatile_isize);
+    generate_write_volatile_harness!(u8, non_null_check_write_volatile_u8);
+    generate_write_volatile_harness!(u16, non_null_check_write_volatile_u16);
+    generate_write_volatile_harness!(u32, non_null_check_write_volatile_u32);
+    generate_write_volatile_harness!(u64, non_null_check_write_volatile_u64);
+    generate_write_volatile_harness!(u128, non_null_check_write_volatile_u128);
+    generate_write_volatile_harness!(usize, non_null_check_write_volatile_usize);
+
+    macro_rules! generate_write_bytes_harness {
+        ($type:ty, $harness_name:ident) => {
+            #[kani::proof_for_contract(NonNull::write_bytes)]
+            pub fn $harness_name() {
+                // Create a pointer generator for the given type with appropriate byte size
+                const ARR_SIZE: usize = mem::size_of::<$type>() * 10;
+                let mut generator = kani::PointerGenerator::<ARR_SIZE>::new();
+
+                // Get a raw pointer from the generator
+                let raw_ptr: *mut $type = generator.any_in_bounds().ptr;
+
+                // Create a non-null pointer from the raw pointer
+                let ptr = NonNull::new(raw_ptr).unwrap();
+
+                // Create a non-deterministic value to write
+                let val: u8 = kani::any();
+
+                // Create a non-deterministic count
+                let count: usize = kani::any();
+
+                unsafe {
+                    // Perform the volatile write operation
+                    ptr.write_bytes(val, count);
+
+                    // Create a non-deterministic count
+                    let i: usize = kani::any_where(|&x| x < count * mem::size_of::<$type>());
+                    let ptr_byte = ptr.as_ptr() as *const u8;
+
+                    // Read back the value and assert it's correct
+                    assert_eq!(*ptr_byte.add(i), val);
+                }
+            }
+        };
+    }
+
+    #[kani::proof_for_contract(NonNull::write_bytes)]
+    pub fn non_null_check_write_bytes_unit() {
+        // Create a pointer generator for the given type with appropriate byte size
+        let mut generator = kani::PointerGenerator::<1>::new();
+
+        // Get a raw pointer from the generator
+        let raw_ptr: *mut () = generator.any_in_bounds().ptr;
+
+        // Create a non-null pointer from the raw pointer
+        let ptr = NonNull::new(raw_ptr).unwrap();
+
+        // Create a non-deterministic value to write
+        let val: u8 = kani::any();
+
+        // Create a non-deterministic count
+        let count: usize = kani::any();
+
+        unsafe {
+            // Perform the volatile write operation
+            ptr.write_bytes(val, count);
+        }
+    }
+
     // Generate proof harnesses for multiple types with appropriate byte sizes
-    generate_write_volatile_harness!(i8, 1, non_null_check_write_volatile_i8);
-    generate_write_volatile_harness!(i16, 2, non_null_check_write_volatile_i16);
-    generate_write_volatile_harness!(i32, 4, non_null_check_write_volatile_i32);
-    generate_write_volatile_harness!(i64, 8, non_null_check_write_volatile_i64);
-    generate_write_volatile_harness!(i128, 16, non_null_check_write_volatile_i128);
-    generate_write_volatile_harness!(
-        isize,
-        { core::mem::size_of::<isize>() },
-        non_null_check_write_volatile_isize
-    );
-    generate_write_volatile_harness!(u8, 1, non_null_check_write_volatile_u8);
-    generate_write_volatile_harness!(u16, 2, non_null_check_write_volatile_u16);
-    generate_write_volatile_harness!(u32, 4, non_null_check_write_volatile_u32);
-    generate_write_volatile_harness!(u64, 8, non_null_check_write_volatile_u64);
-    generate_write_volatile_harness!(u128, 16, non_null_check_write_volatile_u128);
-    generate_write_volatile_harness!(
-        usize,
-        { core::mem::size_of::<usize>() },
-        non_null_check_write_volatile_usize
-    );
-    generate_write_volatile_harness!((), 1, non_null_check_write_volatile_unit);
+    generate_write_bytes_harness!(i8, non_null_check_write_bytes_i8);
+    generate_write_bytes_harness!(i16, non_null_check_write_bytes_i16);
+    generate_write_bytes_harness!(i32, non_null_check_write_bytes_i32);
+    generate_write_bytes_harness!(i64, non_null_check_write_bytes_i64);
+    generate_write_bytes_harness!(i128, non_null_check_write_bytes_i128);
+    generate_write_bytes_harness!(isize, non_null_check_write_bytes_isize);
+    generate_write_bytes_harness!(u8, non_null_check_write_bytes_u8);
+    generate_write_bytes_harness!(u16, non_null_check_write_bytes_u16);
+    generate_write_bytes_harness!(u32, non_null_check_write_bytes_u32);
+    generate_write_bytes_harness!(u64, non_null_check_write_bytes_u64);
+    generate_write_bytes_harness!(u128, non_null_check_write_bytes_u128);
+    generate_write_bytes_harness!(usize, non_null_check_write_bytes_usize);
 
     #[kani::proof_for_contract(NonNull::byte_add)]
     pub fn non_null_byte_add_proof() {