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()[start_inclusive..end_exclusive],
284    {
285        &self[start_inclusive..end_exclusive]
286    }
287}
288
289impl<T: DeepView> ExecSpecSeqEmpty for Vec<T> {
290    #[inline(always)]
291    fn exec_empty() -> (res: Self)
292        ensures
293            res.deep_view() =~= Seq::empty(),
294    {
295        Vec::new()
296    }
297}
298
299impl<'a, T: DeepView + DeepViewClone + std::hash::Hash + std::cmp::Eq> ExecSpecSeqToMultiset<
300    'a,
301> for &'a [T] {
302    type Elem = T;
303
304    #[verifier::external_body]
305    #[inline(always)]
306    fn exec_to_multiset(self) -> (res: ExecMultiset<Self::Elem>)
307        ensures
308            res.deep_view() =~= self.deep_view().to_multiset(),
309    {
310        let mut mset = ExecMultiset { m: HashMap::new() };
311        for e in self.iter() {
312            match mset.m.remove_entry(e) {
313                Some((k, c)) => {
314                    mset.m.insert(k, c + 1);
315                },
316                None => {
317                    mset.m.insert(e.deep_clone(), 1);
318                },
319            }
320        }
321        mset
322    }
323}
324
325impl<'a, T: DeepView> ExecSpecSeqDropFirst<'a> for &'a [T] {
326    type Elem = &'a T;
327
328    #[inline(always)]
329    fn exec_drop_first(self) -> (res: Self)
330        ensures
331            res.deep_view() =~= self.deep_view().drop_first(),
332    {
333        self.exec_subrange(1, self.exec_len())
334    }
335}
336
337impl<'a, T: DeepView> ExecSpecSeqDropLast<'a> for &'a [T] {
338    type Elem = &'a T;
339
340    #[inline(always)]
341    fn exec_drop_last(self) -> (res: Self)
342        ensures
343            res.deep_view() =~= self.deep_view().drop_last(),
344    {
345        self.exec_subrange(0, self.exec_len() - 1)
346    }
347}
348
349impl<'a, T: DeepView> ExecSpecSeqTake<'a> for &'a [T] {
350    type Elem = &'a T;
351
352    #[inline(always)]
353    fn exec_take(self, n: usize) -> (res: Self)
354        ensures
355            res.deep_view() =~= self.deep_view()[..n],
356    {
357        self.exec_subrange(0, n)
358    }
359}
360
361impl<'a, T: DeepView> ExecSpecSeqSkip<'a> for &'a [T] {
362    type Elem = &'a T;
363
364    #[inline(always)]
365    fn exec_skip(self, n: usize) -> (res: Self)
366        ensures
367            res.deep_view() =~= self.deep_view()[n..],
368    {
369        self.exec_subrange(n, self.exec_len())
370    }
371}
372
373impl<'a, T: DeepView> ExecSpecSeqLast<'a> for &'a [T] {
374    type Elem = &'a T;
375
376    #[inline(always)]
377    fn exec_last(self) -> (res: Self::Elem)
378        ensures
379            res.deep_view() == self.deep_view().last(),
380    {
381        &self.exec_index(self.len() - 1)
382    }
383}
384
385impl<'a, T: DeepView> ExecSpecSeqFirst<'a> for &'a [T] {
386    type Elem = &'a T;
387
388    #[inline(always)]
389    fn exec_first(self) -> (res: Self::Elem)
390        ensures
391            res.deep_view() == self.deep_view().first(),
392    {
393        &self.exec_index(0)
394    }
395}
396
397impl<'a, T: DeepView> ExecSpecSeqIsPrefixOf<'a> for &'a [T] where
398    &'a T: ExecSpecEq<'a, Other = &'a T>,
399    &'a [T]: DeepView<V = Seq<<&'a T as DeepView>::V>>,
400 {
401    type Other = &'a [T];
402
403    #[inline(always)]
404    fn exec_is_prefix_of(self, other: Self::Other) -> (res: bool)
405        ensures
406            res == self.deep_view().is_prefix_of(other.deep_view()),
407    {
408        self.exec_len() <= other.exec_len() && (<&[T]>::exec_eq(
409            self,
410            other.exec_subrange(0, self.exec_len()),
411        ))
412    }
413}
414
415impl<'a, T: DeepView> ExecSpecSeqIsSuffixOf<'a> for &'a [T] where
416    &'a T: ExecSpecEq<'a, Other = &'a T>,
417    &'a [T]: DeepView<V = Seq<<&'a T as DeepView>::V>>,
418 {
419    type Other = &'a [T];
420
421    #[inline(always)]
422    fn exec_is_suffix_of(self, other: Self::Other) -> (res: bool)
423        ensures
424            res == self.deep_view().is_suffix_of(other.deep_view()),
425    {
426        self.exec_len() <= other.exec_len() && (<&[T]>::exec_eq(
427            self,
428            other.exec_subrange(other.exec_len() - self.exec_len(), other.exec_len()),
429        ))
430    }
431}
432
433impl<'a, T: DeepView + PartialEq> ExecSpecSeqContains<'a> for &'a [T] where
434    &'a T: ExecSpecEq<'a, Other = &'a T>,
435 {
436    type Elem = T;
437
438    #[verifier::external_body]
439    #[inline(always)]
440    fn exec_contains(self, needle: Self::Elem) -> (res: bool)
441        ensures
442            res == self.deep_view().contains(needle.deep_view()),
443    {
444        self.contains(&needle)
445    }
446}
447
448impl<'a, T: DeepView + PartialEq> ExecSpecSeqIndexOf<'a> for &'a [T] where
449    &'a T: ExecSpecEq<'a, Other = &'a T>,
450 {
451    type Elem = T;
452
453    // hard to verify - index_of contains a choose operator
454    #[verifier::external_body]
455    #[inline(always)]
456    fn exec_index_of(self, needle: Self::Elem) -> (res: usize)
457        ensures
458            res == self.deep_view().index_of(needle.deep_view()),
459    {
460        for i in 0..self.exec_len() {
461            if self[i] == needle {
462                return i;
463            }
464        }
465        self.exec_len()
466    }
467}
468
469impl<'a, T: DeepView + PartialEq> ExecSpecSeqIndexOfFirst<'a> for &'a [T] where
470    &'a T: ExecSpecEq<'a, Other = &'a T>,
471 {
472    type Elem = T;
473
474    #[verifier::external_body]
475    fn exec_index_of_first(self, needle: Self::Elem) -> (res: Option<usize>)
476        ensures
477            match res {
478                Some(i) => self.deep_view().index_of_first(needle.deep_view()).is_some() && i as int
479                    == self.deep_view().index_of_first(needle.deep_view())->0,
480                None => self.deep_view().index_of_first(needle.deep_view()) == None::<int>,
481            },
482    {
483        for i in 0..self.exec_len() {
484            if self[i] == needle {
485                return Some(i);
486            }
487        }
488        None
489    }
490}
491
492impl<'a, T: DeepView + PartialEq> ExecSpecSeqIndexOfLast<'a> for &'a [T] where
493    &'a T: ExecSpecEq<'a, Other = &'a T>,
494 {
495    type Elem = T;
496
497    #[verifier::external_body]
498    #[inline(always)]
499    fn exec_index_of_last(self, needle: Self::Elem) -> (res: Option<usize>)
500        ensures
501            match res {
502                Some(i) => self.deep_view().index_of_last(needle.deep_view()).is_some() && i as int
503                    == self.deep_view().index_of_last(needle.deep_view())->0,
504                None => self.deep_view().index_of_last(needle.deep_view()) == None::<int>,
505            },
506    {
507        for i in (0..self.exec_len()).rev() {
508            if self[i] == needle {
509                return Some(i);
510            }
511        }
512        None
513    }
514}
515
516} // verus!
vstd/contrib/exec_spec/seq.rs

vstd/contrib/exec_spec/
seq.rs
