vstd/contrib/exec_spec/
seq.rs

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