Proofs for Vec::swap_remove, Option::as_slice, and VecDeque::swap (#212)

Resolves: #76

### Changes
* Adds proofs for the following functions using raw pointer operations:
  * `Vec::swap_remove`
  * `Option::as_slice`
  * `VecDeque::swap`
* ideally the usages should have been verified by stubbing the contracts
for reaw pointer operations like `byte_add`, `add` and `offset`, but
stubbing cannot be done for these functions at this time due to
model-checking/kani#3732
* Marks Challenge 3 as Resolved and changes its end date.
* Adds contributors.

#### PoCs:
* `Vec::swap_remove`: @MayureshJoshi25
* `Option::as_slice`, `VecDeque::swap`: @stogaru 

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.

---------

Co-authored-by: Yifei Wang <[email protected]>
Co-authored-by: MayureshJoshi25 <[email protected]>
Co-authored-by: Yifei Wang <[email protected]>
Co-authored-by: Michael Tautschnig <[email protected]>
Co-authored-by: szlee118 <[email protected]>
Co-authored-by: szlee118 <[email protected]>
Co-authored-by: Felipe R. Monteiro <[email protected]>

Author: 6 people

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/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
+        }
+    }
+}