Implements any_vec::<LENGTH, T>() (rust-lang#1319)

Callout: tests under `tests/kani/Vector/any` are slow, but should terminate within 1 minute. 

* Added test case for any_vec feature.

* Implemented any_vec, arbitrary generator for vectors of T: Invariant

* Fixed push.

* Unified interface with any_slice.

* Loosened trait requirements with Arbitrary.

* Fixed typo: sice -> slice.

* Implemented variable and exact length vectors.

* Adjusted test case to fail. Detailed that failure in comments.

* Changed any_vec to use exact_vec for vector generation. Show diff.

* Reverted push test case. Separate `any/push_slow.rs` has been added.

Author: Yoshiki Takashima

library/kani/src/lib.rs

@@ -6,6 +6,7 @@
 pub mod arbitrary;
 pub mod invariant;
 pub mod slice;
+pub mod vec;
 
 pub use arbitrary::Arbitrary;
 pub use invariant::Invariant;

library/kani/src/vec.rs

@@ -0,0 +1,25 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+use crate::{any, assume, Invariant};
+
+/// Generates an arbitrary vector whose length is at most MAX_LENGTH.
+pub fn any_vec<T, const MAX_LENGTH: usize>() -> Vec<T>
+where
+    T: Invariant,
+{
+    let mut v = exact_vec::<T, MAX_LENGTH>();
+    let real_length: usize = any();
+    assume(real_length <= MAX_LENGTH);
+    unsafe { v.set_len(real_length) };
+
+    v
+}
+
+/// Generates an arbitrary vector that is exactly EXACT_LENGTH long.
+pub fn exact_vec<T, const EXACT_LENGTH: usize>() -> Vec<T>
+where
+    T: Invariant,
+{
+    let boxed_array: Box<[T; EXACT_LENGTH]> = Box::new(any());
+    <[T]>::into_vec(boxed_array)
+}

tests/kani/Vectors/any/fixme_append.rs

@@ -0,0 +1,28 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+/// Append 2 arbitrary vectors, lengths at most 1 and 2 respectively,
+/// and assert they have been appended.  This test case takes 53
+/// minutes with #[kani::unwind(75)], but takes less than a second
+/// with semantically equivalent exact_vec. This performance problem
+/// is the subject of issue #1322.
+#[kani::proof]
+#[kani::unwind(1)]
+fn main() {
+    let mut v1: Vec<u128> = kani::vec::any_vec::<_, 1>();
+    kani::assume(v1.len() == 1);
+    let mut v2: Vec<u128> = kani::vec::any_vec::<_, 2>();
+    kani::assume(v2.len() == 2);
+
+    let v1_initial = v1.clone();
+    let v2_initial = v2.clone();
+    let l1 = v1.len();
+    let l2 = v2.len();
+
+    v1.append(&mut v2);
+    assert!(v2.len() == 0);
+    assert!(v1.len() == (l1 + l2));
+
+    assert!(v1[0..l1] == v1_initial);
+    assert!(v1[l1..] == v2_initial);
+}

tests/kani/Vectors/any/push_slow.rs

@@ -0,0 +1,19 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! Variant of tests/kani/Vector/push.rs using any_vec. Slow due to
+//! performance issues involving any_vec. See #1329
+#[kani::proof]
+fn main() {
+    let mut v: Vec<isize> = kani::vec::any_vec::<_, 0>();
+    v.push(72);
+    v.push(2);
+    v.push(3);
+    v.push(4);
+    v.push(5);
+    assert!(v[0] == 72);
+    assert!(v[1] == 2);
+    assert!(v[2] == 3);
+    assert!(v[3] == 4);
+    assert!(v[4] == 5);
+}

tests/kani/Vectors/any/resize.rs

@@ -0,0 +1,24 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+/// Resizing arbitrary vector of Vec<i64> length at most 5, at least
+/// 2. Asserts that the modification occurs, and only on memory that
+/// should be changed.
+#[kani::proof]
+#[kani::unwind(50)]
+fn main() {
+    let mut v: Vec<i64> = kani::vec::exact_vec::<_, 5>();
+
+    let initial_length = v.len();
+    let initial_vector = v.clone();
+    let arbitrary_padding: i64 = kani::any();
+
+    v.resize(initial_length + 1, arbitrary_padding);
+    assert!(v.len() == initial_length + 1);
+    assert!(v[v.len() - 1] == arbitrary_padding);
+    assert!(v[0..initial_length] == initial_vector);
+
+    v.resize(initial_length - 1, arbitrary_padding);
+    assert!(v.len() == initial_length - 1);
+    assert_eq!(v[..], initial_vector[..initial_length - 1]);
+}

tests/kani/Vectors/any/sorting.rs

@@ -0,0 +1,15 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+/// Sort an arbitrary Vec<u32> of length 3. Assert that the sorting worked.
+#[kani::proof]
+#[kani::unwind(4)]
+fn main() {
+    let mut v: Vec<u32> = kani::vec::any_vec::<_, 2>();
+    kani::assume(v.len() == 2);
+
+    if v[0] > v[1] {
+        v.reverse();
+    }
+    assert!(v[0] <= v[1]);
+}