vstd/contrib/exec_spec/
seq.rs

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

vstd/contrib/exec_spec/
seq.rs
