Add support to min_specialization for arbitrary / invariant (rust-lan…

…g#1029)

* Add support to mim_specialization for arbitrary / invariant

We would like to enable users to provide custom implementations of
Invariant and Arbitrary. Use feature `min_specialization` to allow that.
Note that users will also need to enable that same feature in their
code.

library/kani/src/arbitrary.rs

@@ -14,7 +14,7 @@ impl<T> Arbitrary for T
 where
     T: Invariant,
 {
-    fn any() -> Self {
+    default fn any() -> Self {
         let value = unsafe { any_raw::<T>() };
         assume(value.is_valid());
         value

library/kani/src/lib.rs

@@ -1,6 +1,7 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 #![feature(rustc_attrs)] // Used for rustc_diagnostic_item.
+#![feature(min_specialization)] // Used for default implementation of Arbitrary.
 
 pub mod arbitrary;
 pub mod invariant;

tests/kani/Arbitrary/vector_wrapper.rs

@@ -0,0 +1,42 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//
+// Check that users can implement Invariant and Arbitrary to the same struct.
+#![cfg_attr(kani, feature(min_specialization))]
+
+extern crate kani;
+use kani::{Arbitrary, Invariant};
+
+// Dummy wrappar that keeps track of the vector size.
+struct VecWrapper {
+    has_data: bool,
+    data: Vec<u8>,
+}
+
+impl VecWrapper {
+    fn new() -> Self {
+        VecWrapper { has_data: false, data: Vec::new() }
+    }
+
+    fn from(buf: &[u8]) -> Self {
+        VecWrapper { has_data: true, data: Vec::from(buf) }
+    }
+}
+
+unsafe impl Invariant for VecWrapper {
+    fn is_valid(&self) -> bool {
+        self.has_data ^ self.data.is_empty()
+    }
+}
+
+impl Arbitrary for VecWrapper {
+    fn any() -> Self {
+        if kani::any() { VecWrapper::new() } else { VecWrapper::from(&[kani::any(), kani::any()]) }
+    }
+}
+
+#[kani::proof]
+fn check() {
+    let wrap: VecWrapper = kani::any();
+    assert!(wrap.is_valid());
+}