From 9ef84db815f665768d731dd974577df7effb645a Mon Sep 17 00:00:00 2001 From: Chris Hawblitzel Date: Mon, 22 Apr 2024 16:42:09 -0700 Subject: [PATCH 1/3] Implement View and DeepView in slice and array --- source/rust_verify_test/tests/arrays.rs | 1 + source/rust_verify_test/tests/std.rs | 26 ++++++++++++++ source/vstd/array.rs | 18 ++++++++-- source/vstd/slice.rs | 48 ++++++++++++++++++------- source/vstd/std_specs/vec.rs | 25 +++++-------- 5 files changed, 87 insertions(+), 31 deletions(-) diff --git a/source/rust_verify_test/tests/arrays.rs b/source/rust_verify_test/tests/arrays.rs index 079da75d76..50edd09c84 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 ed23646a12..0414dad5f3 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..d47bba76b6 100644 --- a/source/vstd/slice.rs +++ b/source/vstd/slice.rs @@ -10,9 +10,23 @@ 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()) + } +} +#[verusfmt::skip] // this doesn't help +pub trait SliceAdditionalSpecFns: View> { spec fn spec_index(&self, i: int) -> T recommends 0 <= i < self.view().len(), @@ -20,8 +34,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 +51,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) +#[verifier(external_body)] +pub broadcast proof fn axiom_spec_len(slice: &[T]) + ensures + #[trigger] spec_slice_len(slice) == slice@.len(), +{ +} + +#[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 +91,4 @@ 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() -} - } // verus! diff --git a/source/vstd/std_specs/vec.rs b/source/vstd/std_specs/vec.rs index 45221759f7..b0e278f451 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) From ecf0c53dd1a381fc17b8c2e59fe41219ee7a10e8 Mon Sep 17 00:00:00 2001 From: Chris Hawblitzel Date: Tue, 23 Apr 2024 09:17:55 -0700 Subject: [PATCH 2/3] Remove unnecessary verusfmt::skip --- source/vstd/slice.rs | 1 - 1 file changed, 1 deletion(-) diff --git a/source/vstd/slice.rs b/source/vstd/slice.rs index d47bba76b6..181771de34 100644 --- a/source/vstd/slice.rs +++ b/source/vstd/slice.rs @@ -25,7 +25,6 @@ impl DeepView for [T] { } } -#[verusfmt::skip] // this doesn't help pub trait SliceAdditionalSpecFns: View> { spec fn spec_index(&self, i: int) -> T recommends From 5e2bfbfc495f643453e844b9f7a8d953229ae3a4 Mon Sep 17 00:00:00 2001 From: Chris Hawblitzel Date: Tue, 7 May 2024 20:39:07 -0700 Subject: [PATCH 3/3] Add broadcast group for slice --- source/vstd/slice.rs | 7 ++++++- source/vstd/vstd.rs | 2 ++ 2 files changed, 8 insertions(+), 1 deletion(-) diff --git a/source/vstd/slice.rs b/source/vstd/slice.rs index 181771de34..1e8007465b 100644 --- a/source/vstd/slice.rs +++ b/source/vstd/slice.rs @@ -55,11 +55,11 @@ 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) -#[verifier(external_body)] pub broadcast proof fn axiom_spec_len(slice: &[T]) ensures #[trigger] spec_slice_len(slice) == slice@.len(), { + admit(); } #[verifier::external_fn_specification] @@ -90,4 +90,9 @@ pub exec fn slice_subrange(slice: &'a [T], i: usize, j: usize) -> (out: & &slice[i..j] } +#[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/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,