vstd/std_specs/
slice.rs

Help
1use super::super::prelude::*;
2use super::core::IndexSetTrustedSpec;
3use super::core::TrustedSpecSealed;
4
5use core::slice::Iter;
6
7use verus as verus_;
8
9verus_! {
10
11impl<T, const N: usize> TrustedSpecSealed for [T; N] {}
12
13impl<T, const N: usize> IndexSetTrustedSpec<usize> for [T; N] {
14    open spec fn spec_index_set_requires(&self, index: usize) -> bool {
15        0 <= index < N
16    }
17
18    open spec fn spec_index_set_ensures(&self, new_container: &Self, index: usize, val: T) -> bool {
19        new_container@ === self@.update(index as int, val)
20    }
21}
22
23impl<T> TrustedSpecSealed for [T] {}
24
25impl<T> IndexSetTrustedSpec<usize> for [T] {
26    open spec fn spec_index_set_requires(&self, index: usize) -> bool {
27        0 <= index < self@.len()
28    }
29
30    open spec fn spec_index_set_ensures(&self, new_container: &Self, index: usize, val: T) -> bool {
31        new_container@ == self@.update(index as int, val)
32    }
33}
34
35pub assume_specification[ core::hint::unreachable_unchecked ]() -> !
36    requires
37        false,
38;
39
40// The `iter` method of a `<T>` returns an iterator of type `Iter<'_, T>`,
41// so we specify that type here.
42#[verifier::external_type_specification]
43#[verifier::external_body]
44#[verifier::accept_recursive_types(T)]
45pub struct ExIter<'a, T: 'a>(Iter<'a, T>);
46
47impl<T> View for Iter<'_, T> {
48    type V = (int, Seq<T>);
49
50    uninterp spec fn view(&self) -> (int, Seq<T>);
51}
52
53impl<T: DeepView> DeepView for Iter<'_, T> {
54    type V = (int, Seq<T::V>);
55
56    open spec fn deep_view(&self) -> Self::V {
57        let (i, v) = self@;
58        (i, Seq::new(v.len(), |i: int| v[i].deep_view()))
59    }
60}
61
62pub assume_specification<'a, T>[ Iter::<'a, T>::next ](elements: &mut Iter<'a, T>) -> (r: Option<
63    &'a T,
64>)
65    ensures
66        ({
67            let (old_index, old_seq) = old(elements)@;
68            match r {
69                None => {
70                    &&& elements@ == old(elements)@
71                    &&& old_index >= old_seq.len()
72                },
73                Some(element) => {
74                    let (new_index, new_seq) = elements@;
75                    &&& 0 <= old_index < old_seq.len()
76                    &&& new_seq == old_seq
77                    &&& new_index == old_index + 1
78                    &&& element == old_seq[old_index]
79                },
80            }
81        }),
82;
83
84pub struct IterGhostIterator<'a, T> {
85    pub pos: int,
86    pub elements: Seq<T>,
87    pub phantom: Option<&'a T>,
88}
89
90impl<'a, T> super::super::pervasive::ForLoopGhostIteratorNew for Iter<'a, T> {
91    type GhostIter = IterGhostIterator<'a, T>;
92
93    open spec fn ghost_iter(&self) -> IterGhostIterator<'a, T> {
94        IterGhostIterator { pos: self@.0, elements: self@.1, phantom: None }
95    }
96}
97
98impl<'a, T: 'a> super::super::pervasive::ForLoopGhostIterator for IterGhostIterator<'a, T> {
99    type ExecIter = Iter<'a, T>;
100
101    type Item = T;
102
103    type Decrease = int;
104
105    open spec fn exec_invariant(&self, exec_iter: &Iter<'a, T>) -> bool {
106        &&& self.pos == exec_iter@.0
107        &&& self.elements == exec_iter@.1
108    }
109
110    open spec fn ghost_invariant(&self, init: Option<&Self>) -> bool {
111        init matches Some(init) ==> {
112            &&& init.pos == 0
113            &&& init.elements == self.elements
114            &&& 0 <= self.pos <= self.elements.len()
115        }
116    }
117
118    open spec fn ghost_ensures(&self) -> bool {
119        self.pos == self.elements.len()
120    }
121
122    open spec fn ghost_decrease(&self) -> Option<int> {
123        Some(self.elements.len() - self.pos)
124    }
125
126    open spec fn ghost_peek_next(&self) -> Option<T> {
127        if 0 <= self.pos < self.elements.len() {
128            Some(self.elements[self.pos])
129        } else {
130            None
131        }
132    }
133
134    open spec fn ghost_advance(&self, _exec_iter: &Iter<'a, T>) -> IterGhostIterator<'a, T> {
135        Self { pos: self.pos + 1, ..*self }
136    }
137}
138
139impl<'a, T> View for IterGhostIterator<'a, T> {
140    type V = Seq<T>;
141
142    open spec fn view(&self) -> Seq<T> {
143        self.elements.take(self.pos)
144    }
145}
146
147// To allow reasoning about the ghost iterator when the executable
148// function `iter()` is invoked in a `for` loop header (e.g., in
149// `for x in it: s.iter() { ... }`), we need to specify the behavior of
150// the iterator in spec mode. To do that, we add
151// `#[verifier::when_used_as_spec(spec_slice_iter)` to the specification for
152// the executable `into_iter` method and define that spec function here.
153pub uninterp spec fn spec_slice_iter<'a, T>(s: &'a [T]) -> (iter: Iter<'a, T>);
154
155pub broadcast proof fn axiom_spec_slice_iter<'a, T>(s: &'a [T])
156    ensures
157        (#[trigger] spec_slice_iter(s))@ == (0int, s@),
158{
159    admit();
160}
161
162#[verifier::when_used_as_spec(spec_slice_iter)]
163pub assume_specification<'a, T>[ <[T]>::iter ](s: &'a [T]) -> (iter: Iter<'a, T>)
164    ensures
165        ({
166            let (index, seq) = iter@;
167            &&& index == 0
168            &&& seq == s@
169        }),
170;
171
172pub broadcast group group_slice_axioms {
173    axiom_spec_slice_iter,
174}
175
176} // verus!
vstd/std_specs/slice.rs

vstd/std_specs/
slice.rs
