vstd/
seq.rs

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
320// Expensive lemma; not in the default broadcast group
321pub broadcast proof fn lemma_seq_push_index_different_alt<A>(s: Seq<A>, a: A, i: int)
322    requires
323        0 <= i < s.len(),
324    ensures
325        (#[trigger] s.push(a))[i] == #[trigger] s[i],
326{
327    broadcast use axiom_seq_push_index_different;
328
329}
330
331pub broadcast axiom fn axiom_seq_update_len<A>(s: Seq<A>, i: int, a: A)
332    requires
333        0 <= i < s.len(),
334    ensures
335        #[trigger] s.update(i, a).len() == s.len(),
336;
337
338pub broadcast axiom fn axiom_seq_update_same<A>(s: Seq<A>, i: int, a: A)
339    requires
340        0 <= i < s.len(),
341    ensures
342        #[trigger] s.update(i, a)[i] == a,
343;
344
345// Expensive lemma; not in the default broadcast group
346pub broadcast proof fn lemma_seq_update_same_alt<A>(s: Seq<A>, i: int, a: A)
347    requires
348        0 <= i < s.len(),
349    ensures
350        #![trigger s.update(i, a), s[i]]
351        s.update(i, a)[i] == a,
352{
353    broadcast use axiom_seq_update_same;
354
355}
356
357pub broadcast axiom fn axiom_seq_update_different<A>(s: Seq<A>, i1: int, i2: int, a: A)
358    requires
359        0 <= i1 < s.len(),
360        0 <= i2 < s.len(),
361        i1 != i2,
362    ensures
363        #[trigger] s.update(i2, a)[i1] == s[i1],
364;
365
366// Expensive lemma; not in the default broadcast group
367pub broadcast proof fn lemma_seq_update_different_alt<A>(s: Seq<A>, i1: int, i2: int, a: A)
368    requires
369        0 <= i1 < s.len(),
370        0 <= i2 < s.len(),
371        i1 != i2,
372    ensures
373        (#[trigger] s.update(i2, a))[i1] == #[trigger] s[i1],
374{
375    broadcast use axiom_seq_update_different;
376
377}
378
379pub broadcast axiom fn axiom_seq_ext_equal<A>(s1: Seq<A>, s2: Seq<A>)
380    ensures
381        #[trigger] (s1 =~= s2) <==> {
382            &&& s1.len() == s2.len()
383            &&& forall|i: int| 0 <= i < s1.len() ==> s1[i] == s2[i]
384        },
385;
386
387pub broadcast axiom fn axiom_seq_ext_equal_deep<A>(s1: Seq<A>, s2: Seq<A>)
388    ensures
389        #[trigger] (s1 =~~= s2) <==> {
390            &&& s1.len() == s2.len()
391            &&& forall|i: int| 0 <= i < s1.len() ==> s1[i] =~~= s2[i]
392        },
393;
394
395pub broadcast axiom fn axiom_seq_subrange_len<A>(s: Seq<A>, j: int, k: int)
396    requires
397        0 <= j <= k <= s.len(),
398    ensures
399        #[trigger] s.subrange(j, k).len() == k - j,
400;
401
402pub broadcast axiom fn axiom_seq_subrange_index<A>(s: Seq<A>, j: int, k: int, i: int)
403    requires
404        0 <= j <= k <= s.len(),
405        0 <= i < k - j,
406    ensures
407        #[trigger] s.subrange(j, k)[i] == s[i + j],
408;
409
410// Expensive lemma; not in the default broadcast group
411pub broadcast proof fn lemma_seq_subrange_index_alt<A>(s: Seq<A>, j: int, k: int, i: int)
412    requires
413        0 <= j <= k <= s.len(),
414        0 <= i - j < k - j,
415    ensures
416        (#[trigger] s.subrange(j, k))[i - j] == #[trigger] s[i],
417{
418    broadcast use axiom_seq_subrange_index;
419
420}
421
422// Less expensive, more limited alternative to lemma_seq_subrange_index_alt
423pub broadcast proof fn lemma_seq_two_subranges_index<A>(s: Seq<A>, j: int, k1: int, k2: int, i: int)
424    requires
425        0 <= j <= k1 <= s.len(),
426        0 <= j <= k2 <= s.len(),
427        0 <= i < k1 - j,
428        0 <= i < k2 - j,
429    ensures
430        #[trigger] s.subrange(j, k1)[i] == (#[trigger] s.subrange(j, k2))[i],
431{
432    broadcast use axiom_seq_subrange_index;
433
434}
435
436pub broadcast axiom fn axiom_seq_add_len<A>(s1: Seq<A>, s2: Seq<A>)
437    ensures
438        #[trigger] s1.add(s2).len() == s1.len() + s2.len(),
439;
440
441pub broadcast axiom fn axiom_seq_add_index1<A>(s1: Seq<A>, s2: Seq<A>, i: int)
442    requires
443        0 <= i < s1.len(),
444    ensures
445        #[trigger] s1.add(s2)[i] == s1[i],
446;
447
448pub broadcast axiom fn axiom_seq_add_index2<A>(s1: Seq<A>, s2: Seq<A>, i: int)
449    requires
450        s1.len() <= i < s1.len() + s2.len(),
451    ensures
452        #[trigger] s1.add(s2)[i] == s2[i - s1.len()],
453;
454
455// Expensive lemma; not in the default broadcast group
456pub broadcast proof fn lemma_seq_add_index1_alt<A>(s1: Seq<A>, s2: Seq<A>, i: int)
457    requires
458        0 <= i < s1.len(),
459    ensures
460        (#[trigger] s1.add(s2))[i] == #[trigger] s1[i],
461{
462    broadcast use axiom_seq_add_index1;
463
464}
465
466// Expensive lemma; not in the default broadcast group
467pub broadcast proof fn lemma_seq_add_index2_alt<A>(s1: Seq<A>, s2: Seq<A>, i: int)
468    requires
469        0 <= i < s2.len(),
470    ensures
471        (#[trigger] s1.add(s2))[i + s1.len()] == #[trigger] s2[i],
472{
473    broadcast use axiom_seq_add_index2;
474
475}
476
477pub broadcast group group_seq_axioms {
478    axiom_seq_index_decreases,
479    axiom_seq_subrange_decreases,
480    axiom_seq_empty,
481    axiom_seq_new_len,
482    axiom_seq_new_index,
483    axiom_seq_push_len,
484    axiom_seq_push_index_same,
485    axiom_seq_push_index_different,
486    axiom_seq_update_len,
487    axiom_seq_update_same,
488    axiom_seq_update_different,
489    axiom_seq_ext_equal,
490    axiom_seq_ext_equal_deep,
491    axiom_seq_subrange_len,
492    axiom_seq_subrange_index,
493    lemma_seq_two_subranges_index,
494    axiom_seq_add_len,
495    axiom_seq_add_index1,
496    axiom_seq_add_index2,
497}
498
499// Expensive lemmas not in the default group (may slow down verification)
500pub broadcast group group_seq_lemmas_expensive {
501    lemma_seq_push_index_different_alt,
502    lemma_seq_update_same_alt,
503    lemma_seq_update_different_alt,
504    lemma_seq_subrange_index_alt,
505    lemma_seq_add_index1_alt,
506    lemma_seq_add_index2_alt,
507}
508
509// ------------- Macros ---------------- //
510#[doc(hidden)]
511#[macro_export]
512macro_rules! seq_internal {
513    [] => {
514        $crate::vstd::seq::Seq::empty()
515    };
516    [$elem:expr] => {
517        $crate::vstd::seq::Seq::empty()
518            .push($elem)
519    };
520    [$($elem:expr),* $(,)?] => {
521        <_ as $crate::vstd::view::View>::view(&[$($elem),*])
522    };
523    [$elem:expr; $n:expr] => {
524        $crate::vstd::seq::Seq::new(
525            $n,
526            $crate::vstd::prelude::closure_to_fn_spec(
527                |_x: _| $elem
528            ),
529        )
530    };
531}
532
533/// Creates a [`Seq`] containing the given elements.
534///
535/// ## Example
536///
537/// ```rust
538/// let s = seq![11int, 12, 13];
539///
540/// assert(s.len() == 3);
541/// assert(s[0] == 11);
542/// assert(s[1] == 12);
543/// assert(s[2] == 13);
544/// ```
545#[macro_export]
546macro_rules! seq {
547    [$($tail:tt)*] => {
548        $crate::vstd::prelude::verus_proof_macro_exprs!($crate::vstd::seq::seq_internal!($($tail)*))
549    };
550}
551
552#[doc(hidden)]
553pub use seq_internal;
554pub use seq;
555
556} // verus!
vstd/seq.rs

vstd/
seq.rs
