Implement View and DeepView in slice and array #1078
Conversation
|
At the moment, verusfmt complains about the trait syntax |
| open spec fn deep_view(&self) -> Seq<T::V> { | ||
| let v = self.view(); | ||
| Seq::new(v.len(), |i: int| v[i].deep_view()) | ||
| } |
There was a problem hiding this comment.
Just making a quick note here that @y1ca1 had some concerns (during a separate discussion) about this adding more triggers than explicitly reimplementing deep_view on each of the vstd data structures individually.
Personally I think that implementing deep_view separately on each of (say) [u8], [u32], [u64] and so on is not really a good idea (because it doesn't scale and would prevent usage on user-defined types without them manually also implementing deepview on [Foo]), and that we should just go with the current approach.
However, @y1ca1, if I've misunderstood what you meant, please do comment here.
There was a problem hiding this comment.
Thanks for mentioning this. What I meant by "explicitly reimplementing" deep_view is to provide separate implementation on each of the methods for the generic slice type[T] whose specs are described in deep_view. This would arguably save a lot of triggers if one uses deep_view ubiquitously, but yeah, definitely less ergonomic and harder to maintain.
| // 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]) |
There was a problem hiding this comment.
This will now need to be added to the vstd_default broadcast group to be visible to users.
|
Hi! Is it possible to get this PR merged this week? Thanks |
This is related to #1070 .