diff --git a/source/rust_verify_test/tests/arrays.rs b/source/rust_verify_test/tests/arrays.rs index 97f2fc5847..b78ecb638e 100644 --- a/source/rust_verify_test/tests/arrays.rs +++ b/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]) diff --git a/source/rust_verify_test/tests/std.rs b/source/rust_verify_test/tests/std.rs index 3e7b3cded2..d618f4f117 100644 --- a/source/rust_verify_test/tests/std.rs +++ b/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], a2: &[Vec]) + 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; 1], a2: &[Vec; 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) } diff --git a/source/vstd/array.rs b/source/vstd/array.rs index b29969550c..46e2ddb9a4 100644 --- a/source/vstd/array.rs +++ b/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 { +impl View for [T; N] { + type V = Seq; + spec fn view(&self) -> Seq; +} + +impl DeepView for [T; N] { + type V = Seq; + + open spec fn deep_view(&self) -> Seq { + let v = self.view(); + Seq::new(v.len(), |i: int| v[i].deep_view()) + } +} +pub trait ArrayAdditionalSpecFns: View> { spec fn spec_index(&self, i: int) -> T recommends 0 <= i < self.view().len(), @@ -21,8 +35,6 @@ pub trait ArrayAdditionalExecFns { } impl ArrayAdditionalSpecFns for [T; N] { - spec fn view(&self) -> Seq; - #[verifier(inline)] open spec fn spec_index(&self, i: int) -> T { self.view().index(i) diff --git a/source/vstd/slice.rs b/source/vstd/slice.rs index 960c1b86ca..1e8007465b 100644 --- a/source/vstd/slice.rs +++ b/source/vstd/slice.rs @@ -10,9 +10,22 @@ pub use super::std_specs::vec::VecAdditionalSpecFns; verus! { -pub trait SliceAdditionalSpecFns { +impl View for [T] { + type V = Seq; + spec fn view(&self) -> Seq; +} + +impl DeepView for [T] { + type V = Seq; + + open spec fn deep_view(&self) -> Seq { + let v = self.view(); + Seq::new(v.len(), |i: int| v[i].deep_view()) + } +} +pub trait SliceAdditionalSpecFns: View> { spec fn spec_index(&self, i: int) -> T recommends 0 <= i < self.view().len(), @@ -20,8 +33,6 @@ pub trait SliceAdditionalSpecFns { } impl SliceAdditionalSpecFns for [T] { - spec fn view(&self) -> Seq; - #[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(slice: &[T], i: usize) -> (out: &T) &slice[i] } +////// Len (with autospec) +pub open spec fn spec_slice_len(slice: &[T]) -> usize; + +// This axiom is slightly better than defining spec_slice_len to just be `slice@.len() as usize` +// (the axiom also shows that slice@.len() is in-bounds for usize) +pub broadcast proof fn axiom_spec_len(slice: &[T]) + ensures + #[trigger] spec_slice_len(slice) == slice@.len(), +{ + admit(); +} + +#[verifier::external_fn_specification] +#[verifier::when_used_as_spec(spec_slice_len)] +pub fn slice_len(slice: &[T]) -> (len: usize) + ensures + len == spec_slice_len(slice), +{ + slice.len() +} + #[cfg(feature = "alloc")] #[verifier(external_body)] pub exec fn slice_to_vec(slice: &[T]) -> (out: alloc::vec::Vec) @@ -58,13 +90,9 @@ pub exec fn slice_subrange(slice: &'a [T], i: usize, j: usize) -> (out: & &slice[i..j] } -#[verifier(external_fn_specification)] -pub exec fn slice_len(slice: &[T]) -> (length: usize) - ensures - length >= 0, - length == slice@.len(), -{ - slice.len() +#[cfg_attr(verus_keep_ghost, verifier::prune_unless_this_module_is_used)] +pub broadcast group group_slice_axioms { + axiom_spec_len, } } // verus! diff --git a/source/vstd/std_specs/vec.rs b/source/vstd/std_specs/vec.rs index 1f2d28331e..d3c4fb4153 100644 --- a/source/vstd/std_specs/vec.rs +++ b/source/vstd/std_specs/vec.rs @@ -19,16 +19,6 @@ pub struct ExVec(Vec); #[verifier(external_body)] pub struct ExGlobal(alloc::alloc::Global); -////// Declare 'view' function -pub trait VecAdditionalSpecFns { - spec fn spec_len(&self) -> nat; - - spec fn spec_index(&self, i: int) -> T - recommends - 0 <= i < self.spec_len(), - ; -} - impl View for Vec { type V = Seq; @@ -39,16 +29,19 @@ impl DeepView for Vec { type V = Seq; open spec fn deep_view(&self) -> Seq { - 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 VecAdditionalSpecFns for Vec { - #[verifier(inline)] - open spec fn spec_len(&self) -> nat { - self.view().len() - } +pub trait VecAdditionalSpecFns: View> { + spec fn spec_index(&self, i: int) -> T + recommends + 0 <= i < self.view().len(), + ; +} +impl VecAdditionalSpecFns for Vec { #[verifier(inline)] open spec fn spec_index(&self, i: int) -> T { self.view().index(i) diff --git a/source/vstd/vstd.rs b/source/vstd/vstd.rs index 71c35b7e3b..4338c543d8 100644 --- a/source/vstd/vstd.rs +++ b/source/vstd/vstd.rs @@ -73,6 +73,7 @@ pub broadcast group group_vstd_default { std_specs::bits::group_bits_axioms, std_specs::control_flow::group_control_flow_axioms, std_specs::vec::group_vec_axioms, + slice::group_slice_axioms, array::group_array_axioms, multiset::group_multiset_axioms, string::group_string_axioms, @@ -91,6 +92,7 @@ pub broadcast group group_vstd_default { set_lib::group_set_lib_axioms, std_specs::bits::group_bits_axioms, std_specs::control_flow::group_control_flow_axioms, + slice::group_slice_axioms, array::group_array_axioms, multiset::group_multiset_axioms, string::group_string_axioms,