Spec for Vec::extend_from_slice (#1439)

source/rust_verify/example/std_test/vec_test.rs

@@ -0,0 +1,20 @@
+use std::vec::Vec;
+
+use vstd::pervasive::runtime_assert;
+use vstd::prelude::*;
+
+verus! {
+
+fn vec_extend_slice_test() {
+    let mut a: Vec<u32> = vec![1, 2];
+    let b: Vec<u32> = vec![3, 4];
+    a.extend_from_slice(b.as_slice());
+    runtime_assert(a.len() == 4);
+    runtime_assert(a[0] == 1);
+    runtime_assert(a[1] == 2);
+    runtime_assert(a[2] == 3);
+    runtime_assert(a[3] == 4);
+    runtime_assert(b.len() == 2);
+}
+
+} // verus!

source/vstd/std_specs/vec.rs

@@ -116,6 +116,21 @@ pub assume_specification<T, A: Allocator>[ Vec::<T, A>::append ](
         other@ == Seq::<T>::empty(),
 ;
 
+pub assume_specification<T: core::clone::Clone, A: Allocator>[ Vec::<T, A>::extend_from_slice ](
+    vec: &mut Vec<T, A>,
+    other: &[T],
+)
+    ensures
+        vec@.len() == old(vec)@.len() + other@.len(),
+        forall|i: int|
+            #![trigger vec@[i]]
+            0 <= i < vec@.len() ==> if i < old(vec)@.len() {
+                vec@[i] == old(vec)@[i]
+            } else {
+                cloned::<T>(other@[i - old(vec)@.len()], vec@[i])
+            },
+;
+
 /*
 // TODO find a way to support this
 // This is difficult because of the SliceIndex trait