vstd/contrib/exec_spec/
seq.rs

1//! This module contains [`Seq`]-specific method implementations.
2use crate::contrib::exec_spec::*;
3use crate::prelude::*;
4
5use verus as verus_skip_verusfmt; // verusfmt doesn't handle s[..e] yet
6verus_skip_verusfmt! {
7
8// Note: the exec translations which use iterators are unverified.
9broadcast use crate::group_vstd_default;
10
11/// Impls for shared traits
12/// NOTE: can't implement [`ExecSpecType`] for [`Seq<T>`]
13/// since it conflicts with [`SpecString`] (i.e., [`Seq<char>`]).
14impl<'a, T: DeepView> ToRef<&'a [T]> for &'a Vec<T> {
15    #[inline(always)]
16    fn get_ref(self) -> &'a [T] {
17        self.as_slice()
18    }
19}
20
21impl<'a, T: DeepView + DeepViewClone> ToOwned<Vec<T>> for &'a [T] {
22    /// TODO: verify this
23    #[verifier::external_body]
24    #[inline(always)]
25    fn get_owned(self) -> Vec<T> {
26        self.iter().map(|x| x.deep_clone()).collect()
27    }
28}
29
30impl<T: DeepViewClone> DeepViewClone for Vec<T> {
31    /// TODO: verify this
32    #[verifier::external_body]
33    #[inline(always)]
34    fn deep_clone(&self) -> Self {
35        self.iter().map(|x| x.deep_clone()).collect()
36    }
37}
38
39impl<'a, T: DeepView> ExecSpecEq<'a> for &'a [T] where &'a T: ExecSpecEq<'a, Other = &'a T> {
40    type Other = &'a [T];
41
42    #[verifier::external_body]
43    #[inline(always)]
44    fn exec_eq(this: Self, other: Self::Other) -> bool {
45        this.len() == other.len() && this.iter().zip(other.iter()).all(
46            |(a, b)| <&'a T>::exec_eq(a, b),
47        )
48    }
49}
50
51impl<'a, T: DeepView> ExecSpecEq<'a> for &'a Vec<T> where &'a T: ExecSpecEq<'a, Other = &'a T> {
52    type Other = &'a Vec<T>;
53
54    #[verifier::external_body]
55    #[inline(always)]
56    fn exec_eq(this: Self, other: Self::Other) -> bool {
57        this.len() == other.len() && this.iter().zip(other.iter()).all(
58            |(a, b)| <&'a T>::exec_eq(a, b),
59        )
60    }
61}
62
63impl<'a, T: DeepView> ExecSpecLen for &'a [T] {
64    #[inline(always)]
65    fn exec_len(self) -> (res: usize)
66        ensures
67            res == self.deep_view().len(),
68    {
69        self.len()
70    }
71}
72
73impl<'a, T: DeepView> ExecSpecIndex<'a> for &'a [T] {
74    type Elem = &'a T;
75
76    #[inline(always)]
77    fn exec_index(self, index: usize) -> (res: Self::Elem)
78        ensures
79            res.deep_view() == self.deep_view()[index as int],
80    {
81        self.get(index).unwrap()
82    }
83}
84
85//
86// Trait definitions for methods
87//
88/// Spec for executable version of [`Seq::add`].
89pub trait ExecSpecSeqAdd<'a, Out: Sized + DeepView>: Sized + DeepView + ToOwned<Out> {
90    fn exec_add(self, rhs: Self) -> Out;
91}
92
93/// Spec for executable version of [`Seq::push`].
94pub trait ExecSpecSeqPush<'a, Out: Sized + DeepView>: Sized + DeepView + ToOwned<Out> {
95    type Elem: DeepView + DeepViewClone;
96
97    fn exec_push(self, a: Self::Elem) -> Out;
98}
99
100/// Spec for executable version of [`Seq::update`].
101pub trait ExecSpecSeqUpdate<'a, Out: Sized + DeepView>: Sized + DeepView + ToOwned<Out> {
102    type Elem: DeepView + DeepViewClone;
103
104    fn exec_update(self, i: usize, a: Self::Elem) -> Out;
105}
106
107/// Spec for executable version of [`Seq::subrange`].
108pub trait ExecSpecSeqSubrange<'a>: Sized + DeepView<V = Seq<<Self::Elem as DeepView>::V>> {
109    type Elem: DeepView;
110
111    fn exec_subrange(self, start_inclusive: usize, end_exclusive: usize) -> Self
112        requires
113            0 <= start_inclusive <= end_exclusive <= self.deep_view().len(),
114    ;
115}
116
117/// Spec for executable version of [`Seq::empty`].
118pub trait ExecSpecSeqEmpty: Sized {
119    fn exec_empty() -> Self;
120}
121
122/// Spec for executable version of [`Seq::to_multiset`].
123pub trait ExecSpecSeqToMultiset<'a>: Sized {
124    type Elem: DeepView + DeepViewClone + std::hash::Hash + std::cmp::Eq;
125
126    fn exec_to_multiset(self) -> ExecMultiset<Self::Elem>;
127}
128
129// The implementations here for interp Seq methods (e.g. take) could be streamlined.
130// Currently, the spec fn definition is copied and translated to the exec version by hand.
131// A more concise approach would be to apply the exec_spec macro directly to the spec fns on Seq.
132/// Spec for executable version of [`Seq::drop_first`].
133pub trait ExecSpecSeqDropFirst<'a>: Sized + DeepView<V = Seq<<Self::Elem as DeepView>::V>> {
134    type Elem: DeepView;
135
136    fn exec_drop_first(self) -> Self
137        requires
138            self.deep_view().len() >= 1,
139    ;
140}
141
142/// Spec for executable version of [`Seq::drop_last`].
143pub trait ExecSpecSeqDropLast<'a>: Sized + DeepView<V = Seq<<Self::Elem as DeepView>::V>> {
144    type Elem: DeepView;
145
146    fn exec_drop_last(self) -> Self
147        requires
148            self.deep_view().len() >= 1,
149    ;
150}
151
152/// Spec for executable version of [`Seq::take`].
153pub trait ExecSpecSeqTake<'a>: Sized + DeepView<V = Seq<<Self::Elem as DeepView>::V>> {
154    type Elem: DeepView;
155
156    fn exec_take(self, n: usize) -> Self
157        requires
158            0 <= n <= self.deep_view().len(),
159    ;
160}
161
162/// Spec for executable version of [`Seq::skip`].
163pub trait ExecSpecSeqSkip<'a>: Sized + DeepView<V = Seq<<Self::Elem as DeepView>::V>> {
164    type Elem: DeepView;
165
166    fn exec_skip(self, n: usize) -> Self
167        requires
168            0 <= n <= self.deep_view().len(),
169    ;
170}
171
172/// Spec for executable version of [`Seq::last`].
173pub trait ExecSpecSeqLast<'a>: Sized + DeepView<V = Seq<<Self::Elem as DeepView>::V>> {
174    type Elem: DeepView;
175
176    fn exec_last(self) -> Self::Elem
177        requires
178            0 < self.deep_view().len(),
179    ;
180}
181
182/// Spec for executable version of [`Seq::first`].
183pub trait ExecSpecSeqFirst<'a>: Sized + DeepView<V = Seq<<Self::Elem as DeepView>::V>> {
184    type Elem: DeepView;
185
186    fn exec_first(self) -> Self::Elem
187        requires
188            0 < self.deep_view().len(),
189    ;
190}
191
192/// Spec for executable version of [`Seq::is_prefix_of`].
193pub trait ExecSpecSeqIsPrefixOf<'a>: DeepView + Sized {
194    type Other: DeepView<V = Self::V>;
195
196    fn exec_is_prefix_of(self, other: Self::Other) -> (res: bool);
197}
198
199/// Spec for executable version of [`Seq::is_suffix_of`].
200pub trait ExecSpecSeqIsSuffixOf<'a>: DeepView + Sized {
201    type Other: DeepView<V = Self::V>;
202
203    fn exec_is_suffix_of(self, other: Self::Other) -> (res: bool);
204}
205
206/// Spec for executable version of [`Seq::contains`].
207pub trait ExecSpecSeqContains<'a>: Sized + DeepView {
208    type Elem: DeepView;
209
210    fn exec_contains(self, needle: Self::Elem) -> bool;
211}
212
213/// Spec for executable version of [`Seq::index_of`].
214pub trait ExecSpecSeqIndexOf<'a>: Sized + DeepView {
215    type Elem: DeepView;
216
217    fn exec_index_of(self, needle: Self::Elem) -> usize;
218}
219
220/// Spec for executable version of [`Seq::index_of_first`].
221pub trait ExecSpecSeqIndexOfFirst<'a>: Sized + DeepView {
222    type Elem: DeepView;
223
224    fn exec_index_of_first(self, needle: Self::Elem) -> Option<usize>;
225}
226
227/// Spec for executable version of [`Seq::index_of_last`].
228pub trait ExecSpecSeqIndexOfLast<'a>: Sized + DeepView {
229    type Elem: DeepView;
230
231    fn exec_index_of_last(self, needle: Self::Elem) -> Option<usize>;
232}
233
234//
235// Implementations for Vec and slices
236//
237impl<'a, T: DeepView + DeepViewClone> ExecSpecSeqAdd<'a, Vec<T>> for &'a [T] {
238    #[verifier::external_body]
239    #[inline(always)]
240    fn exec_add(self, rhs: Self) -> (res: Vec<T>)
241        ensures
242            res.deep_view() =~= self.deep_view().add(rhs.deep_view()),
243    {
244        self.get_owned().into_iter().chain(rhs.get_owned()).collect()
245    }
246}
247
248impl<'a, T: DeepView + DeepViewClone> ExecSpecSeqPush<'a, Vec<T>> for &'a [T] {
249    type Elem = T;
250
251    #[verifier::external_body]
252    #[inline(always)]
253    fn exec_push(self, a: Self::Elem) -> (res: Vec<T>)
254        ensures
255            res.deep_view() =~= self.deep_view().push(a.deep_view()),
256    {
257        let v = vec![a];
258        self.get_owned().into_iter().chain(v).collect()
259    }
260}
261
262impl<'a, T: DeepView + DeepViewClone> ExecSpecSeqUpdate<'a, Vec<T>> for &'a [T] {
263    type Elem = T;
264
265    #[verifier::external_body]
266    #[inline(always)]
267    fn exec_update(self, i: usize, a: Self::Elem) -> (res: Vec<T>)
268        ensures
269            res.deep_view() =~= self.deep_view().update(i as int, a.deep_view()),
270    {
271        let mut v: Vec<T> = self.get_owned();
272        v[i] = a.deep_clone();
273        v
274    }
275}
276
277impl<'a, T: DeepView> ExecSpecSeqSubrange<'a> for &'a [T] {
278    type Elem = &'a T;
279
280    #[verifier::external_body]
281    #[inline(always)]
282    fn exec_subrange(self, start_inclusive: usize, end_exclusive: usize) -> (res: Self)
283        ensures
284            res.deep_view() =~= self.deep_view()[start_inclusive..end_exclusive],
285    {
286        &self[start_inclusive..end_exclusive]
287    }
288}
289
290impl<T: DeepView> ExecSpecSeqEmpty for Vec<T> {
291    #[inline(always)]
292    fn exec_empty() -> (res: Self)
293        ensures
294            res.deep_view() =~= Seq::empty(),
295    {
296        Vec::new()
297    }
298}
299
300impl<'a, T: DeepView + DeepViewClone + std::hash::Hash + std::cmp::Eq> ExecSpecSeqToMultiset<
301    'a,
302> for &'a [T] {
303    type Elem = T;
304
305    #[verifier::external_body]
306    #[inline(always)]
307    fn exec_to_multiset(self) -> (res: ExecMultiset<Self::Elem>)
308        ensures
309            res.deep_view() =~= self.deep_view().to_multiset(),
310    {
311        let mut mset = ExecMultiset { m: HashMap::new() };
312        for e in self.iter() {
313            match mset.m.remove_entry(e) {
314                Some((k, c)) => {
315                    mset.m.insert(k, c + 1);
316                },
317                None => {
318                    mset.m.insert(e.deep_clone(), 1);
319                },
320            }
321        }
322        mset
323    }
324}
325
326impl<'a, T: DeepView> ExecSpecSeqDropFirst<'a> for &'a [T] {
327    type Elem = &'a T;
328
329    #[inline(always)]
330    fn exec_drop_first(self) -> (res: Self)
331        ensures
332            res.deep_view() =~= self.deep_view().drop_first(),
333    {
334        self.exec_subrange(1, self.exec_len())
335    }
336}
337
338impl<'a, T: DeepView> ExecSpecSeqDropLast<'a> for &'a [T] {
339    type Elem = &'a T;
340
341    #[inline(always)]
342    fn exec_drop_last(self) -> (res: Self)
343        ensures
344            res.deep_view() =~= self.deep_view().drop_last(),
345    {
346        self.exec_subrange(0, self.exec_len() - 1)
347    }
348}
349
350impl<'a, T: DeepView> ExecSpecSeqTake<'a> for &'a [T] {
351    type Elem = &'a T;
352
353    #[inline(always)]
354    fn exec_take(self, n: usize) -> (res: Self)
355        ensures
356            res.deep_view() =~= self.deep_view()[..n],
357    {
358        self.exec_subrange(0, n)
359    }
360}
361
362impl<'a, T: DeepView> ExecSpecSeqSkip<'a> for &'a [T] {
363    type Elem = &'a T;
364
365    #[inline(always)]
366    fn exec_skip(self, n: usize) -> (res: Self)
367        ensures
368            res.deep_view() =~= self.deep_view()[n..],
369    {
370        self.exec_subrange(n, self.exec_len())
371    }
372}
373
374impl<'a, T: DeepView> ExecSpecSeqLast<'a> for &'a [T] {
375    type Elem = &'a T;
376
377    #[inline(always)]
378    fn exec_last(self) -> (res: Self::Elem)
379        ensures
380            res.deep_view() == self.deep_view().last(),
381    {
382        &self.exec_index(self.len() - 1)
383    }
384}
385
386impl<'a, T: DeepView> ExecSpecSeqFirst<'a> for &'a [T] {
387    type Elem = &'a T;
388
389    #[inline(always)]
390    fn exec_first(self) -> (res: Self::Elem)
391        ensures
392            res.deep_view() == self.deep_view().first(),
393    {
394        &self.exec_index(0)
395    }
396}
397
398impl<'a, T: DeepView> ExecSpecSeqIsPrefixOf<'a> for &'a [T] where
399    &'a T: ExecSpecEq<'a, Other = &'a T>,
400    &'a [T]: DeepView<V = Seq<<&'a T as DeepView>::V>>,
401 {
402    type Other = &'a [T];
403
404    #[inline(always)]
405    fn exec_is_prefix_of(self, other: Self::Other) -> (res: bool)
406        ensures
407            res == self.deep_view().is_prefix_of(other.deep_view()),
408    {
409        self.exec_len() <= other.exec_len() && (<&[T]>::exec_eq(
410            self,
411            other.exec_subrange(0, self.exec_len()),
412        ))
413    }
414}
415
416impl<'a, T: DeepView> ExecSpecSeqIsSuffixOf<'a> for &'a [T] where
417    &'a T: ExecSpecEq<'a, Other = &'a T>,
418    &'a [T]: DeepView<V = Seq<<&'a T as DeepView>::V>>,
419 {
420    type Other = &'a [T];
421
422    #[inline(always)]
423    fn exec_is_suffix_of(self, other: Self::Other) -> (res: bool)
424        ensures
425            res == self.deep_view().is_suffix_of(other.deep_view()),
426    {
427        self.exec_len() <= other.exec_len() && (<&[T]>::exec_eq(
428            self,
429            other.exec_subrange(other.exec_len() - self.exec_len(), other.exec_len()),
430        ))
431    }
432}
433
434impl<'a, T: DeepView + PartialEq> ExecSpecSeqContains<'a> for &'a [T] where
435    &'a T: ExecSpecEq<'a, Other = &'a T>,
436 {
437    type Elem = T;
438
439    #[verifier::external_body]
440    #[inline(always)]
441    fn exec_contains(self, needle: Self::Elem) -> (res: bool)
442        ensures
443            res == self.deep_view().contains(needle.deep_view()),
444    {
445        self.contains(&needle)
446    }
447}
448
449impl<'a, T: DeepView + PartialEq> ExecSpecSeqIndexOf<'a> for &'a [T] where
450    &'a T: ExecSpecEq<'a, Other = &'a T>,
451 {
452    type Elem = T;
453
454    // hard to verify - index_of contains a choose operator
455    #[verifier::external_body]
456    #[inline(always)]
457    fn exec_index_of(self, needle: Self::Elem) -> (res: usize)
458        ensures
459            res == self.deep_view().index_of(needle.deep_view()),
460    {
461        for i in 0..self.exec_len() {
462            if self[i] == needle {
463                return i;
464            }
465        }
466        self.exec_len()
467    }
468}
469
470impl<'a, T: DeepView + PartialEq> ExecSpecSeqIndexOfFirst<'a> for &'a [T] where
471    &'a T: ExecSpecEq<'a, Other = &'a T>,
472 {
473    type Elem = T;
474
475    #[verifier::external_body]
476    fn exec_index_of_first(self, needle: Self::Elem) -> (res: Option<usize>)
477        ensures
478            match res {
479                Some(i) => self.deep_view().index_of_first(needle.deep_view()).is_some() && i as int
480                    == self.deep_view().index_of_first(needle.deep_view())->0,
481                None => self.deep_view().index_of_first(needle.deep_view()) == None::<int>,
482            },
483    {
484        for i in 0..self.exec_len() {
485            if self[i] == needle {
486                return Some(i);
487            }
488        }
489        None
490    }
491}
492
493impl<'a, T: DeepView + PartialEq> ExecSpecSeqIndexOfLast<'a> for &'a [T] where
494    &'a T: ExecSpecEq<'a, Other = &'a T>,
495 {
496    type Elem = T;
497
498    #[verifier::external_body]
499    #[inline(always)]
500    fn exec_index_of_last(self, needle: Self::Elem) -> (res: Option<usize>)
501        ensures
502            match res {
503                Some(i) => self.deep_view().index_of_last(needle.deep_view()).is_some() && i as int
504                    == self.deep_view().index_of_last(needle.deep_view())->0,
505                None => self.deep_view().index_of_last(needle.deep_view()) == None::<int>,
506            },
507    {
508        for i in (0..self.exec_len()).rev() {
509            if self[i] == needle {
510                return Some(i);
511            }
512        }
513        None
514    }
515}
516
517} // verus!
vstd/contrib/exec_spec/seq.rs

vstd/contrib/exec_spec/
seq.rs
