feat: add spec for slice::contains

source/rust_verify_test/tests/slices.rs

@@ -1156,3 +1156,16 @@ test_verify_one_file! {
         }
     } => Ok(())
 }
+
+test_verify_one_file! {
+    #[test] test_slice_contains verus_code! {
+        use vstd::prelude::*;
+
+        fn test() {
+            let values: &[u8] = &[1, 2, 3];
+
+            assert(values.contains(&2));
+            assert(!values.contains(&4));
+        }
+    } => Ok(())
+}

source/vstd/std_specs/slice.rs

@@ -327,6 +327,20 @@ impl<T, U> super::cmp::PartialEqSpecImpl<[U]> for [T] where T: PartialEq<U> + su
     }
 }
 
+// contains
+pub open spec fn spec_slice_contains<T: PartialEq<T>>(slice: &[T], value: &T) -> bool {
+    exists |i: int| #![auto] 0 <= i < slice@.len()
+        && <T as super::cmp::PartialEqSpec<T>>::eq_spec(&slice[i], value)
+}
+
+#[verifier::when_used_as_spec(spec_slice_contains)]
+pub assume_specification<T>[ <[T]>::contains ] (slice: &[T], value: &T) -> (result: bool)
+    where
+        T: PartialEq<T>,
+        ensures
+            <T as super::cmp::PartialEqSpec<T>>::obeys_eq_spec() ==> result == spec_slice_contains(slice, value),
+;
+
 // The `iter` method of a `<T>` returns an iterator of type `Iter<'_, T>`,
 // so we specify that type here.
 #[verifier::external_type_specification]