Proofs for Vec::swap_remove, Option::as_slice, and VecDeque::swap

doc/src/challenges/0003-pointer-arithmentic.md

@@ -1,10 +1,11 @@
 # Challenge 3: Verifying Raw Pointer Arithmetic Operations
 
-- **Status:** Open
+- **Status:** Resolved
 - **Tracking Issue:** [#76](https://github.com/model-checking/verify-rust-std/issues/76)
 - **Start date:** *2024/06/24*
-- **End date:** *2025/04/10*
+- **End date:** *2024/12/11*
 - **Reward:** *N/A*
+- **Contributors:** [Surya Togaru](https://github.com/stogaru), [Yifei Wang](https://github.com/xsxszab), [Szu-Yu Lee](https://github.com/szlee118), [Mayuresh Joshi](https://github.com/MayureshJoshi25)
 
 -------------------
 

library/alloc/src/collections/vec_deque/mod.rs

@@ -58,6 +58,9 @@ mod spec_from_iter;
 #[cfg(test)]
 mod tests;
 
+#[cfg(kani)]
+use core::kani;
+
 /// A double-ended queue implemented with a growable ring buffer.
 ///
 /// The "default" usage of this type as a queue is to use [`push_back`] to add to
@@ -3079,3 +3082,43 @@ impl<T, const N: usize> From<[T; N]> for VecDeque<T> {
         deq
     }
 }
+
+#[cfg(kani)]
+#[unstable(feature = "kani", issue = "none")]
+mod verify {
+    use core::kani;
+    use crate::collections::VecDeque;
+
+    #[kani::proof]
+    fn check_vecdeque_swap() {
+        // The array's length is set to an arbitrary value, which defines its size.
+        // In this case, implementing a dynamic array is not possible using any_array
+        // The more elements in the array the longer the veification time.
+        const ARRAY_LEN: usize = 40;
+        let mut arr: [u32; ARRAY_LEN] = kani::Arbitrary::any_array();
+        let mut deque: VecDeque<u32> = VecDeque::from(arr);
+        let len = deque.len();
+
+        // Generate valid indices within bounds
+        let i = kani::any_where(|&x: &usize| x < len);
+        let j = kani::any_where(|&x: &usize| x < len);
+
+        // Capture the elements at i and j before the swap
+        let elem_i_before = deque[i];
+        let elem_j_before = deque[j];
+
+        // Perform the swap
+        deque.swap(i, j);
+
+        // Postcondition: Verify elements have swapped places
+        assert_eq!(deque[i], elem_j_before);
+        assert_eq!(deque[j], elem_i_before);
+
+        // Ensure other elements remain unchanged
+        let k = kani::any_where(|&x: &usize| x < len);
+        if k != i && k != j {
+            assert!(deque[k] == arr[k]);
+        }
+    }
+
+}

library/alloc/src/string.rs

@@ -3217,3 +3217,56 @@ impl From<char> for String {
         c.to_string()
     }
 }
+
+
+
+#[cfg(kani)]
+#[unstable(feature = "kani", issue = "none")]
+mod verify {
+    use core::kani;
+    use crate::string::String;
+
+    #[kani::proof]
+    #[kani::unwind(9)]  // Unwind up to 9 times
+    /// This proof harness verifies the safety of the `String::remove`
+    /// 
+    /// The harness checks:
+    /// 1. The string length decreases by one after the `remove` operation.
+    /// 2. The removed character is valid ASCII.
+    /// 3. The removed character matches the character at the specified index in the original string.
+    /// 
+    /// This ensures the `remove` function behaves as expected for constrained inputs.
+    fn check_remove() {
+        // array size is chosen because it is small enough to be feasible to check exhaustively
+        const ARRAY_SIZE: usize = 8;
+        let arr: [u8; ARRAY_SIZE] = kani::Arbitrary::any_array();
+        for &byte in &arr {
+            kani::assume(byte.is_ascii()); // Constrain to ASCII characters
+        }
+
+        // Convert byte array to a String directly (safe since all are ASCII)
+        let mut s = unsafe { String::from_utf8_unchecked(arr.to_vec()) };
+
+        // Ensure the string is not empty
+        kani::assume(!s.is_empty());
+
+        // Generate a valid index within the bounds of the string
+        let idx: usize = kani::any_where(|&x| x < s.len());
+
+        // Store the character at the index `idx` before calling `remove`
+        let original_char = s.chars().nth(idx).expect("Index out of bounds");
+
+        // Call the `remove` function
+        let removed_char = s.remove(idx);
+
+        // Verify the string length decreases correctly
+        assert_eq!(s.len(), arr.len() - 1);
+
+        // Verify the removed character is a valid ASCII character
+        assert!(removed_char.is_ascii());
+
+        // Assert that the removed character matches the original character at `idx`
+        assert_eq!(removed_char, original_char);
+    }
+}
+

library/alloc/src/vec/mod.rs

@@ -4032,3 +4032,49 @@ impl<T, A: Allocator, const N: usize> TryFrom<Vec<T, A>> for [T; N] {
         Ok(array)
     }
 }
+
+#[cfg(kani)]
+#[unstable(feature = "kani", issue = "none")]
+mod verify {
+    use core::kani;
+    use crate::vec::Vec;
+
+    // Size chosen for testing the empty vector (0), middle element removal (1) 
+    // and last element removal (2) cases while keeping verification tractable 
+    const ARRAY_LEN: usize = 3;
+
+    #[kani::proof]
+    pub fn verify_swap_remove() {
+
+        // Creating a vector directly from a fixed length arbitrary array
+        let mut arr: [i32; ARRAY_LEN] = kani::Arbitrary::any_array();
+        let mut vect = Vec::from(&arr);
+
+        // Recording the original length and a copy of the vector for validation
+        let original_len = vect.len();
+        let original_vec = vect.clone();
+
+        // Generating a nondeterministic index which is guaranteed to be within bounds
+        let index: usize = kani::any_where(|x| *x < original_len);
+
+        let removed = vect.swap_remove(index);
+
+        // Verifying that the length of the vector decreases by one after the operation is performed
+        assert!(vect.len() == original_len - 1, "Length should decrease by 1");
+
+        // Verifying that the removed element matches the original element at the index
+        assert!(removed == original_vec[index], "Removed element should match original");
+
+        // Verifying that the removed index now contains the element originally at the vector's last index if applicable
+        if index < original_len - 1 {
+            assert!(vect[index] == original_vec[original_len - 1], "Index should contain last element");
+        }
+
+        // Check that all other unaffected elements remain unchanged
+        let k = kani::any_where(|&x: &usize| x < original_len - 1);
+        if k != index {
+            assert!(vect[k] == arr[k]);
+        }
+
+    }
+}

library/core/src/option.rs

@@ -2572,3 +2572,30 @@ impl<T, const N: usize> [Option<T>; N] {
         self.try_map(core::convert::identity)
     }
 }
+
+#[cfg(kani)]
+#[unstable(feature = "kani", issue = "none")]
+mod verify {
+    use crate::kani;
+    use crate::option::Option;
+
+    #[kani::proof]
+    fn verify_as_slice() {
+        if kani::any() {
+            // Case 1: Option is Some
+            let value: u32 = kani::any();
+            let some_option: Option<u32> = Some(value);
+
+            let slice = some_option.as_slice();
+            assert_eq!(slice.len(), 1); // The slice should have exactly one element
+            assert_eq!(slice[0], value); // The value in the slice should match
+        } else {
+            // Case 2: Option is None
+            let none_option: Option<u32> = None;
+
+            let empty_slice = none_option.as_slice();
+            assert_eq!(empty_slice.len(), 0); // The slice should be empty
+            assert!(empty_slice.is_empty()); // Explicit check for emptiness
+        }
+    }
+}