Implement View and DeepView in slice and array

source/rust_verify_test/tests/arrays.rs

@@ -5,6 +5,7 @@ use common::*;
 
 test_verify_one_file! {
     #[test] test1 verus_code! {
+        use vstd::prelude::*;
         use vstd::array::*;
 
         fn test(ar: [u8; 20])

source/rust_verify_test/tests/std.rs

@@ -337,5 +337,31 @@ test_verify_one_file! {
             assert(g2);
             assert(c2@ == v2@); // FAILS
         }
+
+        fn test_slice_deep_view(a1: &[Vec<u8>], a2: &[Vec<u8>])
+            requires
+                a1.len() == 1,
+                a2.len() == 1,
+                a1[0].len() == 1,
+                a2[0].len() == 1,
+                a1[0][0] == 10,
+                a2[0][0] == 10,
+            ensures
+                a1.deep_view() == a2.deep_view(),
+        {
+            assert(a1.deep_view() =~~= a2.deep_view()); // TODO: get rid of this?
+        }
+
+        fn test_array_deep_view(a1: &[Vec<u8>; 1], a2: &[Vec<u8>; 1])
+            requires
+                a1[0].len() == 1,
+                a2[0].len() == 1,
+                a1[0][0] == 10,
+                a2[0][0] == 10,
+            ensures
+                a1.deep_view() == a2.deep_view(),
+        {
+            assert(a1.deep_view() =~~= a2.deep_view()); // TODO: get rid of this?
+        }
     } => Err(err) => assert_fails(err, 2)
 }

source/vstd/array.rs

@@ -1,14 +1,28 @@
 #![allow(unused_imports)]
 use crate::seq::*;
 use crate::slice::SliceAdditionalSpecFns;
+use crate::view::*;
 use builtin::*;
 use builtin_macros::*;
 
 verus! {
 
-pub trait ArrayAdditionalSpecFns<T> {
+impl<T, const N: usize> View for [T; N] {
+    type V = Seq<T>;
+
     spec fn view(&self) -> Seq<T>;
+}
+
+impl<T: DeepView, const N: usize> DeepView for [T; N] {
+    type V = Seq<T::V>;
+
+    open spec fn deep_view(&self) -> Seq<T::V> {
+        let v = self.view();
+        Seq::new(v.len(), |i: int| v[i].deep_view())
+    }
+}
 
+pub trait ArrayAdditionalSpecFns<T>: View<V = Seq<T>> {
     spec fn spec_index(&self, i: int) -> T
         recommends
             0 <= i < self.view().len(),
@@ -21,8 +35,6 @@ pub trait ArrayAdditionalExecFns<T> {
 }
 
 impl<T, const N: usize> ArrayAdditionalSpecFns<T> for [T; N] {
-    spec fn view(&self) -> Seq<T>;
-
     #[verifier(inline)]
     open spec fn spec_index(&self, i: int) -> T {
         self.view().index(i)

source/vstd/slice.rs

@@ -10,18 +10,29 @@ pub use super::std_specs::vec::VecAdditionalSpecFns;
 
 verus! {
 
-pub trait SliceAdditionalSpecFns<T> {
+impl<T> View for [T] {
+    type V = Seq<T>;
+
     spec fn view(&self) -> Seq<T>;
+}
+
+impl<T: DeepView> DeepView for [T] {
+    type V = Seq<T::V>;
+
+    open spec fn deep_view(&self) -> Seq<T::V> {
+        let v = self.view();
+        Seq::new(v.len(), |i: int| v[i].deep_view())
+    }
+}
 
+pub trait SliceAdditionalSpecFns<T>: View<V = Seq<T>> {
     spec fn spec_index(&self, i: int) -> T
         recommends
             0 <= i < self.view().len(),
     ;
 }
 
 impl<T> SliceAdditionalSpecFns<T> for [T] {
-    spec fn view(&self) -> Seq<T>;
-
     #[verifier(inline)]
     open spec fn spec_index(&self, i: int) -> T {
         self.view().index(i)
@@ -39,6 +50,27 @@ pub exec fn slice_index_get<T>(slice: &[T], i: usize) -> (out: &T)
     &slice[i]
 }
 
+////// Len (with autospec)
+pub open spec fn spec_slice_len<T>(slice: &[T]) -> usize;
+
+// This axiom is slightly better than defining spec_slice_len to just be `[email protected]() as usize`
+// (the axiom also shows that [email protected]() is in-bounds for usize)
+#[verifier(external_body)]
+pub broadcast proof fn axiom_spec_len<T>(slice: &[T])
+    ensures
+        #[trigger] spec_slice_len(slice) == [email protected](),
+{
+}
+
+#[verifier::external_fn_specification]
+#[verifier::when_used_as_spec(spec_slice_len)]
+pub fn slice_len<T>(slice: &[T]) -> (len: usize)
+    ensures
+        len == spec_slice_len(slice),
+{
+    slice.len()
+}
+
 #[cfg(feature = "alloc")]
 #[verifier(external_body)]
 pub exec fn slice_to_vec<T: Copy>(slice: &[T]) -> (out: alloc::vec::Vec<T>)
@@ -58,13 +90,4 @@ pub exec fn slice_subrange<T, 'a>(slice: &'a [T], i: usize, j: usize) -> (out: &
     &slice[i..j]
 }
 
-#[verifier(external_fn_specification)]
-pub exec fn slice_len<T>(slice: &[T]) -> (length: usize)
-    ensures
-        length >= 0,
-        length == [email protected](),
-{
-    slice.len()
-}
-
 } // verus!

source/vstd/std_specs/vec.rs

@@ -19,16 +19,6 @@ pub struct ExVec<T, A: Allocator>(Vec<T, A>);
 #[verifier(external_body)]
 pub struct ExGlobal(alloc::alloc::Global);
 
-////// Declare 'view' function
-pub trait VecAdditionalSpecFns<T> {
-    spec fn spec_len(&self) -> nat;
-
-    spec fn spec_index(&self, i: int) -> T
-        recommends
-            0 <= i < self.spec_len(),
-    ;
-}
-
 impl<T, A: Allocator> View for Vec<T, A> {
     type V = Seq<T>;
 
@@ -39,16 +29,19 @@ impl<T: DeepView, A: Allocator> DeepView for Vec<T, A> {
     type V = Seq<T::V>;
 
     open spec fn deep_view(&self) -> Seq<T::V> {
-        Seq::new(self.view().len(), |i: int| self[i].deep_view())
+        let v = self.view();
+        Seq::new(v.len(), |i: int| v[i].deep_view())
     }
 }
 
-impl<T, A: Allocator> VecAdditionalSpecFns<T> for Vec<T, A> {
-    #[verifier(inline)]
-    open spec fn spec_len(&self) -> nat {
-        self.view().len()
-    }
+pub trait VecAdditionalSpecFns<T>: View<V = Seq<T>> {
+    spec fn spec_index(&self, i: int) -> T
+        recommends
+            0 <= i < self.view().len(),
+    ;
+}
 
+impl<T, A: Allocator> VecAdditionalSpecFns<T> for Vec<T, A> {
     #[verifier(inline)]
     open spec fn spec_index(&self, i: int) -> T {
         self.view().index(i)