vstd/
seq.rs

Help
1use core::marker;
2
3#[allow(unused_imports)]
4use super::pervasive::*;
5#[allow(unused_imports)]
6use super::prelude::*;
7
8verus! {
9
10/// `Seq<A>` is a sequence type for specifications.
11/// To use a "sequence" in compiled code, use an `exec` type like `vec::Vec`
12/// that has `Seq<A>` as its specification type.
13///
14/// An object `seq: Seq<A>` has a length, given by [`seq.len()`](Seq::len),
15/// and a value at each `i` for `0 <= i < seq.len()`, given by [`seq[i]`](Seq::index).
16///
17/// Sequences can be constructed in a few different ways:
18///  * [`Seq::empty`] construct an empty sequence (`len() == 0`)
19///  * [`Seq::new`] construct a sequence of a given length, initialized according
20///     to a given function mapping indices `i` to values `A`.
21///  * The [`seq!`] macro, to construct small sequences of a fixed size (analagous to the
22///     [`std::vec!`] macro).
23///  * By manipulating an existing sequence with [`Seq::push`], [`Seq::update`],
24///    or [`Seq::add`].
25///
26/// To prove that two sequences are equal, it is usually easiest to use the
27/// extensional equality operator `=~=`.
28#[verifier::external_body]
29#[verifier::ext_equal]
30#[verifier::accept_recursive_types(A)]
31pub struct Seq<A> {
32    dummy: marker::PhantomData<A>,
33}
34
35impl<A> Seq<A> {
36    /// An empty sequence (i.e., a sequence of length 0).
37    #[rustc_diagnostic_item = "verus::vstd::seq::Seq::empty"]
38    pub uninterp spec fn empty() -> Seq<A>;
39
40    /// Construct a sequence `s` of length `len` where entry `s[i]` is given by `f(i)`.
41    #[rustc_diagnostic_item = "verus::vstd::seq::Seq::new"]
42    pub uninterp spec fn new(len: nat, f: impl Fn(int) -> A) -> Seq<A>;
43
44    /// The length of a sequence.
45    #[rustc_diagnostic_item = "verus::vstd::seq::Seq::len"]
46    pub uninterp spec fn len(self) -> nat;
47
48    /// Gets the value at the given index `i`.
49    ///
50    /// If `i` is not in the range `[0, self.len())`, then the resulting value
51    /// is meaningless and arbitrary.
52    #[rustc_diagnostic_item = "verus::vstd::seq::Seq::index"]
53    pub uninterp spec fn index(self, i: int) -> A
54        recommends
55            0 <= i < self.len(),
56    ;
57
58    /// `[]` operator, synonymous with `index`
59    #[verifier::inline]
60    pub open spec fn spec_index(self, i: int) -> A
61        recommends
62            0 <= i < self.len(),
63    {
64        self.index(i)
65    }
66
67    /// Appends the value `a` to the end of the sequence.
68    /// This always increases the length of the sequence by 1.
69    /// This often requires annotating the type of the element literal in the sequence,
70    /// e.g., `10int`.
71    ///
72    /// ## Example
73    ///
74    /// ```rust
75    /// proof fn push_test() {
76    ///     assert(seq![10int, 11, 12].push(13) =~= seq![10, 11, 12, 13]);
77    /// }
78    /// ```
79    #[rustc_diagnostic_item = "verus::vstd::seq::Seq::push"]
80    pub uninterp spec fn push(self, a: A) -> Seq<A>;
81
82    /// Updates the sequence at the given index, replacing the element with the given
83    /// value, and leaves all other entries unchanged.
84    ///
85    /// ## Example
86    ///
87    /// ```rust
88    /// proof fn update_test() {
89    ///     let s = seq![10, 11, 12, 13, 14];
90    ///     let t = s.update(2, -5);
91    ///     assert(t =~= seq![10, 11, -5, 13, 14]);
92    /// }
93    /// ```
94    #[rustc_diagnostic_item = "verus::vstd::seq::Seq::update"]
95    pub uninterp spec fn update(self, i: int, a: A) -> Seq<A>
96        recommends
97            0 <= i < self.len(),
98    ;
99
100    /// Returns a sequence for the given subrange.
101    ///
102    /// ## Example
103    ///
104    /// ```rust
105    /// proof fn subrange_test() {
106    ///     let s = seq![10int, 11, 12, 13, 14];
107    ///     //                      ^-------^
108    ///     //           0      1   2   3   4   5
109    ///     let sub = s.subrange(2, 4);
110    ///     assert(sub =~= seq![12, 13]);
111    /// }
112    /// ```
113    #[rustc_diagnostic_item = "verus::vstd::seq::Seq::subrange"]
114    pub uninterp spec fn subrange(self, start_inclusive: int, end_exclusive: int) -> Seq<A>
115        recommends
116            0 <= start_inclusive <= end_exclusive <= self.len(),
117    ;
118
119    /// Returns a sequence containing only the first n elements of the original sequence
120    #[verifier::inline]
121    pub open spec fn take(self, n: int) -> Seq<A> {
122        self.subrange(0, n)
123    }
124
125    /// Returns a sequence without the first n elements of the original sequence
126    #[verifier::inline]
127    pub open spec fn skip(self, n: int) -> Seq<A> {
128        self.subrange(n, self.len() as int)
129    }
130
131    /// Concatenates the sequences.
132    ///
133    /// ## Example
134    ///
135    /// ```rust
136    /// proof fn add_test() {
137    ///     assert(seq![10int, 11].add(seq![12, 13, 14])
138    ///             =~= seq![10, 11, 12, 13, 14]);
139    /// }
140    /// ```
141    #[rustc_diagnostic_item = "verus::vstd::seq::Seq::add"]
142    pub uninterp spec fn add(self, rhs: Seq<A>) -> Seq<A>;
143
144    /// `+` operator, synonymous with `add`
145    #[verifier::inline]
146    pub open spec fn spec_add(self, rhs: Seq<A>) -> Seq<A> {
147        self.add(rhs)
148    }
149
150    /// Returns the last element of the sequence.
151    #[rustc_diagnostic_item = "verus::vstd::seq::Seq::last"]
152    pub open spec fn last(self) -> A
153        recommends
154            0 < self.len(),
155    {
156        self[self.len() as int - 1]
157    }
158
159    /// Returns the first element of the sequence.
160    #[rustc_diagnostic_item = "vstd::seq::Seq::first"]
161    pub open spec fn first(self) -> A
162        recommends
163            0 < self.len(),
164    {
165        self[0]
166    }
167
168    #[verifier(external_body)]
169    pub proof fn tracked_empty() -> (tracked ret: Self)
170        ensures
171            ret === Seq::empty(),
172    {
173        unimplemented!()
174    }
175
176    #[verifier(external_body)]
177    pub proof fn tracked_remove(tracked &mut self, i: int) -> (tracked ret: A)
178        requires
179            0 <= i < old(self).len(),
180        ensures
181            ret === old(self)[i],
182            self.len() == old(self).len() - 1,
183            self == old(self).remove(i),
184    {
185        unimplemented!()
186    }
187
188    #[verifier(external_body)]
189    pub proof fn tracked_insert(tracked &mut self, i: int, tracked v: A)
190        requires
191            0 <= i <= old(self).len(),
192        ensures
193            self.len() == old(self).len() + 1,
194            self == old(self).insert(i, v),
195    {
196        unimplemented!()
197    }
198
199    #[verifier(external_body)]
200    pub proof fn tracked_borrow(tracked &self, i: int) -> (tracked ret: &A)
201        requires
202            0 <= i < self.len(),
203        ensures
204            *ret === self[i],
205    {
206        unimplemented!()
207    }
208
209    pub proof fn tracked_push(tracked &mut self, tracked v: A)
210        ensures
211            *self == old(self).push(v),
212            self.len() == old(self).len() + 1,
213    {
214        broadcast use group_seq_axioms;
215
216        assert(self.insert(self.len() as int, v) =~= self.push(v));
217        self.tracked_insert(self.len() as int, v);
218    }
219
220    pub proof fn tracked_pop(tracked &mut self) -> (tracked ret: A)
221        requires
222            old(self).len() > 0,
223        ensures
224            ret === old(self).last(),
225            self.len() == old(self).len() - 1,
226            *self == old(self).take(old(self).len() - 1),
227    {
228        broadcast use group_seq_axioms;
229
230        assert(self.remove(self.len() - 1) =~= self.take(self.len() - 1));
231        self.tracked_remove(self.len() - 1)
232    }
233
234    pub proof fn tracked_pop_front(tracked &mut self) -> (tracked ret: A)
235        requires
236            old(self).len() > 0,
237        ensures
238            ret === old(self).first(),
239            self.len() == old(self).len() - 1,
240            *self == old(self).drop_first(),
241    {
242        broadcast use group_seq_axioms;
243
244        assert(self.remove(0) =~= self.drop_first());
245        self.tracked_remove(0)
246    }
247}
248
249// Trusted axioms
250pub broadcast axiom fn axiom_seq_index_decreases<A>(s: Seq<A>, i: int)
251    requires
252        0 <= i < s.len(),
253    ensures
254        #[trigger] (decreases_to!(s => s[i])),
255;
256
257pub axiom fn axiom_seq_len_decreases<A>(s1: Seq<A>, s2: Seq<A>)
258    requires
259        s2.len() < s1.len(),
260        forall|i2: int|
261            0 <= i2 < s2.len() && #[trigger] trigger(s2[i2]) ==> exists|i1: int|
262                0 <= i1 < s1.len() && s1[i1] == s2[i2],
263    ensures
264        decreases_to!(s1 => s2),
265;
266
267pub broadcast proof fn axiom_seq_subrange_decreases<A>(s: Seq<A>, i: int, j: int)
268    requires
269        0 <= i <= j <= s.len(),
270        s.subrange(i, j).len() < s.len(),
271    ensures
272        #[trigger] (decreases_to!(s => s.subrange(i, j))),
273{
274    broadcast use {axiom_seq_subrange_len, axiom_seq_subrange_index};
275
276    let s2 = s.subrange(i, j);
277    assert forall|i2: int| 0 <= i2 < s2.len() && #[trigger] trigger(s2[i2]) implies exists|i1: int|
278        0 <= i1 < s.len() && s[i1] == s2[i2] by {
279        assert(s[i + i2] == s2[i2]);
280    }
281    axiom_seq_len_decreases(s, s2);
282}
283
284pub broadcast axiom fn axiom_seq_empty<A>()
285    ensures
286        #[trigger] Seq::<A>::empty().len() == 0,
287;
288
289pub broadcast axiom fn axiom_seq_new_len<A>(len: nat, f: spec_fn(int) -> A)
290    ensures
291        #[trigger] Seq::new(len, f).len() == len,
292;
293
294pub broadcast axiom fn axiom_seq_new_index<A>(len: nat, f: spec_fn(int) -> A, i: int)
295    requires
296        0 <= i < len,
297    ensures
298        #[trigger] Seq::new(len, f)[i] == f(i),
299;
300
301pub broadcast axiom fn axiom_seq_push_len<A>(s: Seq<A>, a: A)
302    ensures
303        #[trigger] s.push(a).len() == s.len() + 1,
304;
305
306pub broadcast axiom fn axiom_seq_push_index_same<A>(s: Seq<A>, a: A, i: int)
307    requires
308        i == s.len(),
309    ensures
310        #[trigger] s.push(a)[i] == a,
311;
312
313pub broadcast axiom fn axiom_seq_push_index_different<A>(s: Seq<A>, a: A, i: int)
314    requires
315        0 <= i < s.len(),
316    ensures
317        #[trigger] s.push(a)[i] == s[i],
318;
319
320pub broadcast axiom fn axiom_seq_update_len<A>(s: Seq<A>, i: int, a: A)
321    requires
322        0 <= i < s.len(),
323    ensures
324        #[trigger] s.update(i, a).len() == s.len(),
325;
326
327pub broadcast axiom fn axiom_seq_update_same<A>(s: Seq<A>, i: int, a: A)
328    requires
329        0 <= i < s.len(),
330    ensures
331        #[trigger] s.update(i, a)[i] == a,
332;
333
334pub broadcast axiom fn axiom_seq_update_different<A>(s: Seq<A>, i1: int, i2: int, a: A)
335    requires
336        0 <= i1 < s.len(),
337        0 <= i2 < s.len(),
338        i1 != i2,
339    ensures
340        #[trigger] s.update(i2, a)[i1] == s[i1],
341;
342
343pub broadcast axiom fn axiom_seq_ext_equal<A>(s1: Seq<A>, s2: Seq<A>)
344    ensures
345        #[trigger] (s1 =~= s2) <==> {
346            &&& s1.len() == s2.len()
347            &&& forall|i: int| 0 <= i < s1.len() ==> s1[i] == s2[i]
348        },
349;
350
351pub broadcast axiom fn axiom_seq_ext_equal_deep<A>(s1: Seq<A>, s2: Seq<A>)
352    ensures
353        #[trigger] (s1 =~~= s2) <==> {
354            &&& s1.len() == s2.len()
355            &&& forall|i: int| 0 <= i < s1.len() ==> s1[i] =~~= s2[i]
356        },
357;
358
359pub broadcast axiom fn axiom_seq_subrange_len<A>(s: Seq<A>, j: int, k: int)
360    requires
361        0 <= j <= k <= s.len(),
362    ensures
363        #[trigger] s.subrange(j, k).len() == k - j,
364;
365
366pub broadcast axiom fn axiom_seq_subrange_index<A>(s: Seq<A>, j: int, k: int, i: int)
367    requires
368        0 <= j <= k <= s.len(),
369        0 <= i < k - j,
370    ensures
371        #[trigger] s.subrange(j, k)[i] == s[i + j],
372;
373
374pub broadcast axiom fn axiom_seq_add_len<A>(s1: Seq<A>, s2: Seq<A>)
375    ensures
376        #[trigger] s1.add(s2).len() == s1.len() + s2.len(),
377;
378
379pub broadcast axiom fn axiom_seq_add_index1<A>(s1: Seq<A>, s2: Seq<A>, i: int)
380    requires
381        0 <= i < s1.len(),
382    ensures
383        #[trigger] s1.add(s2)[i] == s1[i],
384;
385
386pub broadcast axiom fn axiom_seq_add_index2<A>(s1: Seq<A>, s2: Seq<A>, i: int)
387    requires
388        s1.len() <= i < s1.len() + s2.len(),
389    ensures
390        #[trigger] s1.add(s2)[i] == s2[i - s1.len()],
391;
392
393pub broadcast group group_seq_axioms {
394    axiom_seq_index_decreases,
395    axiom_seq_subrange_decreases,
396    axiom_seq_empty,
397    axiom_seq_new_len,
398    axiom_seq_new_index,
399    axiom_seq_push_len,
400    axiom_seq_push_index_same,
401    axiom_seq_push_index_different,
402    axiom_seq_update_len,
403    axiom_seq_update_same,
404    axiom_seq_update_different,
405    axiom_seq_ext_equal,
406    axiom_seq_ext_equal_deep,
407    axiom_seq_subrange_len,
408    axiom_seq_subrange_index,
409    axiom_seq_add_len,
410    axiom_seq_add_index1,
411    axiom_seq_add_index2,
412}
413
414// ------------- Macros ---------------- //
415#[doc(hidden)]
416#[macro_export]
417macro_rules! seq_internal {
418    [] => {
419        $crate::vstd::seq::Seq::empty()
420    };
421    [$elem:expr] => {
422        $crate::vstd::seq::Seq::empty()
423            .push($elem)
424    };
425    [$($elem:expr),* $(,)?] => {
426        <_ as $crate::vstd::view::View>::view(&[$($elem),*])
427    };
428    [$elem:expr; $n:expr] => {
429        $crate::vstd::seq::Seq::new(
430            $n,
431            $crate::vstd::prelude::closure_to_fn_spec(
432                |_x: _| $elem
433            ),
434        )
435    };
436}
437
438/// Creates a [`Seq`] containing the given elements.
439///
440/// ## Example
441///
442/// ```rust
443/// let s = seq![11int, 12, 13];
444///
445/// assert(s.len() == 3);
446/// assert(s[0] == 11);
447/// assert(s[1] == 12);
448/// assert(s[2] == 13);
449/// ```
450#[macro_export]
451macro_rules! seq {
452    [$($tail:tt)*] => {
453        ::builtin_macros::verus_proof_macro_exprs!($crate::vstd::seq::seq_internal!($($tail)*))
454    };
455}
456
457#[doc(hidden)]
458pub use seq_internal;
459pub use seq;
460
461} // verus!
vstd/seq.rs

vstd/
seq.rs
