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#[verifier::ext_equal]
11#[verifier::accept_recursive_types(A)]
12tracked enum SeqInner<A> {
13    Nil,
14    Cons { head: A, tail: Ghost<SeqInner<A>> },
15}
16
17// This indirection is required to show the termination of `Seq::len`
18//
19// If we translated this to `Seq` we the decrease clauses wouldn't work,
20// because we would have had to re-internalize the tail into a `Seq`
21impl<A> SeqInner<A> {
22    spec fn len(self) -> nat
23        decreases self,
24    {
25        match self {
26            SeqInner::Nil => 0,
27            SeqInner::Cons { tail, .. } => { 1 + tail.len() },
28        }
29    }
30
31    spec fn index(self, i: int) -> A
32        recommends
33            0 <= i < self.len(),
34        decreases self.len(),
35    {
36        match self {
37            SeqInner::Nil => arbitrary(),
38            SeqInner::Cons { head, tail } => if i == 0 {
39                head
40            } else {
41                tail.index(i - 1)
42            },
43        }
44    }
45
46    #[verifier::inline]
47    spec fn spec_index(self, i: int) -> A
48        recommends
49            0 <= i < self.len(),
50    {
51        self.index(i)
52    }
53
54    spec fn push(self, a: A) -> SeqInner<A>
55        decreases self.len(),
56    {
57        match self {
58            SeqInner::Nil => SeqInner::Cons { head: a, tail: Ghost(SeqInner::Nil) },
59            SeqInner::Cons { head, tail } => {
60                let new_tail = tail.push(a);
61                SeqInner::Cons { head, tail: Ghost(new_tail) }
62            },
63        }
64    }
65
66    spec fn update(self, i: int, a: A) -> SeqInner<A>
67        recommends
68            0 <= i < self.len(),
69        decreases self.len(),
70    {
71        if !(0 <= i < self.len()) {  // this supports weakening some preconditions
72            self
73        } else {
74            match self {
75                SeqInner::Nil => arbitrary(),
76                SeqInner::Cons { head, tail } => if i == 0 {
77                    SeqInner::Cons { head: a, tail }
78                } else {
79                    let new_tail = tail.update(i - 1, a);
80                    SeqInner::Cons { head, tail: Ghost(new_tail) }
81                },
82            }
83        }
84    }
85
86    spec fn subrange(self, start_inclusive: int, end_exclusive: int) -> SeqInner<A>
87        recommends
88            0 <= start_inclusive <= end_exclusive <= self.len(),
89        decreases start_inclusive, end_exclusive - start_inclusive,
90    {
91        match self {
92            SeqInner::Nil => SeqInner::Nil,
93            SeqInner::Cons {
94                head,
95                tail,
96            } =>
97            // skip elements until start_inclusive becomes 0
98            if start_inclusive > 0 {
99                tail.subrange(start_inclusive - 1, end_exclusive - 1)
100            } else {
101                if end_exclusive <= 0 {
102                    SeqInner::Nil
103                } else {
104                    let new_tail = tail.subrange(start_inclusive, end_exclusive - 1);
105                    SeqInner::Cons { head, tail: Ghost(new_tail) }
106                }
107            },
108        }
109    }
110
111    spec fn add(self, rhs: SeqInner<A>) -> SeqInner<A>
112        decreases self.len(),
113    {
114        match self {
115            SeqInner::Nil => rhs,
116            SeqInner::Cons { head, tail } => {
117                let new_tail = tail.add(rhs);
118                SeqInner::Cons { head, tail: Ghost(new_tail) }
119            },
120        }
121    }
122}
123
124/// `Seq<A>` is a sequence type for specifications.
125/// To use a "sequence" in compiled code, use an `exec` type like `vec::Vec`
126/// that has `Seq<A>` as its specification type.
127///
128/// An object `seq: Seq<A>` has a length, given by [`seq.len()`](Seq::len),
129/// and a value at each `i` for `0 <= i < seq.len()`, given by [`seq[i]`](Seq::index).
130///
131/// Sequences can be constructed in a few different ways:
132///  * [`Seq::empty`] construct an empty sequence (`len() == 0`)
133///  * [`Seq::new`] construct a sequence of a given length, initialized according
134///     to a given function mapping indices `i` to values `A`.
135///  * The [`seq!`] macro, to construct small sequences of a fixed size (analagous to the
136///     [`std::vec!`] macro).
137///  * By manipulating an existing sequence with [`Seq::push`], [`Seq::update`],
138///    or [`Seq::add`].
139///
140/// To prove that two sequences are equal, it is usually easiest to use the
141/// extensional equality operator `=~=`.
142#[verifier::ext_equal]
143#[verifier::accept_recursive_types(A)]
144pub tracked struct Seq<A> {
145    inner: SeqInner<A>,
146}
147
148impl<A> Seq<A> {
149    /// An empty sequence (i.e., a sequence of length 0).
150    #[rustc_diagnostic_item = "verus::vstd::seq::Seq::empty"]
151    pub closed spec fn empty() -> Seq<A> {
152        Seq { inner: SeqInner::Nil }
153    }
154
155    /// Construct a sequence `s` of length `len` where entry `s[i]` is given by `f(i)`.
156    #[rustc_diagnostic_item = "verus::vstd::seq::Seq::new"]
157    pub closed spec fn new(len: nat, f: spec_fn(int) -> A) -> Seq<A>
158        decreases len,
159    {
160        if len == 0 {
161            Seq { inner: SeqInner::Nil }
162        } else {
163            Self::new((len - 1) as nat, f).push(f(len - 1))
164        }
165    }
166
167    /// The length of a sequence.
168    #[rustc_diagnostic_item = "verus::vstd::seq::Seq::len"]
169    pub closed spec fn len(self) -> nat {
170        self.inner.len()
171    }
172
173    /// Gets the value at the given index `i`.
174    ///
175    /// If `i` is not in the range `[0, self.len())`, then the resulting value
176    /// is meaningless and arbitrary.
177    #[rustc_diagnostic_item = "verus::vstd::seq::Seq::index"]
178    pub closed spec fn index(self, i: int) -> A
179        recommends
180            0 <= i < self.len(),
181    {
182        self.inner.index(i)
183    }
184
185    /// `[]` operator, synonymous with `index`
186    #[verifier::inline]
187    pub open spec fn spec_index(self, i: int) -> A
188        recommends
189            0 <= i < self.len(),
190    {
191        self.index(i)
192    }
193
194    /// Appends the value `a` to the end of the sequence.
195    /// This always increases the length of the sequence by 1.
196    /// This often requires annotating the type of the element literal in the sequence,
197    /// e.g., `10int`.
198    ///
199    /// ## Example
200    ///
201    /// ```rust
202    /// proof fn push_test() {
203    ///     assert(seq![10int, 11, 12].push(13) =~= seq![10, 11, 12, 13]);
204    /// }
205    /// ```
206    #[rustc_diagnostic_item = "verus::vstd::seq::Seq::push"]
207    pub closed spec fn push(self, a: A) -> Seq<A> {
208        Seq { inner: self.inner.push(a) }
209    }
210
211    /// Updates the sequence at the given index, replacing the element with the given
212    /// value, and leaves all other entries unchanged.
213    ///
214    /// ## Example
215    ///
216    /// ```rust
217    /// proof fn update_test() {
218    ///     let s = seq![10, 11, 12, 13, 14];
219    ///     let t = s.update(2, -5);
220    ///     assert(t =~= seq![10, 11, -5, 13, 14]);
221    /// }
222    /// ```
223    #[rustc_diagnostic_item = "verus::vstd::seq::Seq::update"]
224    pub closed spec fn update(self, i: int, a: A) -> Seq<A>
225        recommends
226            0 <= i < self.len(),
227    {
228        Seq { inner: self.inner.update(i, a) }
229    }
230
231    /// Returns a sequence for the given subrange.
232    ///
233    /// ## Example
234    ///
235    /// ```rust
236    /// proof fn subrange_test() {
237    ///     let s = seq![10int, 11, 12, 13, 14];
238    ///     //                      ^-------^
239    ///     //           0      1   2   3   4   5
240    ///     let sub = s.subrange(2, 4);
241    ///     assert(sub =~= seq![12, 13]);
242    /// }
243    /// ```
244    #[rustc_diagnostic_item = "verus::vstd::seq::Seq::subrange"]
245    pub closed spec fn subrange(self, start_inclusive: int, end_exclusive: int) -> Seq<A>
246        recommends
247            0 <= start_inclusive <= end_exclusive <= self.len(),
248    {
249        Seq { inner: self.inner.subrange(start_inclusive, end_exclusive) }
250    }
251
252    /// Returns a sequence containing only the first n elements of the original sequence
253    #[verifier::inline]
254    pub open spec fn take(self, n: int) -> Seq<A> {
255        self.subrange(0, n)
256    }
257
258    /// Returns a sequence without the first n elements of the original sequence
259    #[verifier::inline]
260    pub open spec fn skip(self, n: int) -> Seq<A> {
261        self.subrange(n, self.len() as int)
262    }
263
264    /// Concatenates the sequences.
265    ///
266    /// ## Example
267    ///
268    /// ```rust
269    /// proof fn add_test() {
270    ///     assert(seq![10int, 11].add(seq![12, 13, 14])
271    ///             =~= seq![10, 11, 12, 13, 14]);
272    /// }
273    /// ```
274    #[rustc_diagnostic_item = "verus::vstd::seq::Seq::add"]
275    pub closed spec fn add(self, rhs: Seq<A>) -> Seq<A> {
276        Seq { inner: self.inner.add(rhs.inner) }
277    }
278
279    /// `+` operator, synonymous with `add`
280    #[verifier::inline]
281    pub open spec fn spec_add(self, rhs: Seq<A>) -> Seq<A> {
282        self.add(rhs)
283    }
284
285    /// Returns the last element of the sequence.
286    #[rustc_diagnostic_item = "verus::vstd::seq::Seq::last"]
287    pub open spec fn last(self) -> A
288        recommends
289            0 < self.len(),
290    {
291        self[self.len() as int - 1]
292    }
293
294    /// Returns the first element of the sequence.
295    #[rustc_diagnostic_item = "vstd::seq::Seq::first"]
296    pub open spec fn first(self) -> A
297        recommends
298            0 < self.len(),
299    {
300        self[0]
301    }
302
303    #[verifier(external_body)]
304    pub proof fn tracked_empty() -> (tracked ret: Self)
305        ensures
306            ret == Seq::empty(),
307    {
308        unimplemented!()
309    }
310
311    #[verifier(external_body)]
312    pub proof fn tracked_remove(tracked &mut self, i: int) -> (tracked ret: A)
313        requires
314            0 <= i < old(self).len(),
315        ensures
316            ret == old(self)[i],
317            final(self).len() == old(self).len() - 1,
318            *final(self) == old(self).remove(i),
319    {
320        unimplemented!()
321    }
322
323    #[verifier(external_body)]
324    pub proof fn tracked_insert(tracked &mut self, i: int, tracked v: A)
325        requires
326            0 <= i <= old(self).len(),
327        ensures
328            final(self).len() == old(self).len() + 1,
329            *final(self) == old(self).insert(i, v),
330    {
331        unimplemented!()
332    }
333
334    #[verifier(external_body)]
335    pub proof fn tracked_borrow(tracked &self, i: int) -> (tracked ret: &A)
336        requires
337            0 <= i < self.len(),
338        ensures
339            *ret == self[i],
340    {
341        unimplemented!()
342    }
343
344    pub proof fn tracked_push(tracked &mut self, tracked v: A)
345        ensures
346            *final(self) == old(self).push(v),
347            final(self).len() == old(self).len() + 1,
348    {
349        broadcast use group_seq_axioms;
350
351        assert(self.insert(self.len() as int, v) =~= self.push(v));
352        self.tracked_insert(self.len() as int, v);
353    }
354
355    pub proof fn tracked_pop(tracked &mut self) -> (tracked ret: A)
356        requires
357            old(self).len() > 0,
358        ensures
359            ret == old(self).last(),
360            final(self).len() == old(self).len() - 1,
361            *final(self) == old(self).take(old(self).len() - 1),
362    {
363        broadcast use group_seq_axioms;
364
365        assert(self.remove(self.len() - 1) =~= self.take(self.len() - 1));
366        self.tracked_remove(self.len() - 1)
367    }
368
369    pub proof fn tracked_pop_front(tracked &mut self) -> (tracked ret: A)
370        requires
371            old(self).len() > 0,
372        ensures
373            ret == old(self).first(),
374            final(self).len() == old(self).len() - 1,
375            *final(self) == old(self).drop_first(),
376    {
377        broadcast use group_seq_axioms;
378
379        assert(self.remove(0) =~= self.drop_first());
380        self.tracked_remove(0)
381    }
382}
383
384proof fn lemma_seq_inner_index_decreases<A>(s: SeqInner<A>, i: int)
385    requires
386        0 <= i < s.len(),
387    ensures
388        (decreases_to!(s => s[i])),
389    decreases i,
390{
391    match s {
392        SeqInner::Nil => {
393            assert(s.len() == 0);
394            assert(false);
395        },
396        SeqInner::Cons { head, tail } => {
397            if i == 0 {
398                assert(decreases_to!(s => s[i]));
399            } else {
400                assert(tail[i - 1] == s[i]);
401                lemma_seq_inner_index_decreases(tail@, i - 1);
402                assert(decreases_to!(s => tail@));
403                assert(decreases_to!(tail@ => tail[i-1]));
404            }
405        },
406    }
407}
408
409pub broadcast proof fn axiom_seq_index_decreases<A>(s: Seq<A>, i: int)
410    requires
411        0 <= i < s.len(),
412    ensures
413        #[trigger] (decreases_to!(s => s[i])),
414{
415    lemma_seq_inner_index_decreases(s.inner, i)
416}
417
418// TODO: this should be provable
419pub axiom fn axiom_seq_len_decreases<A>(s1: Seq<A>, s2: Seq<A>)
420    requires
421        s2.len() < s1.len(),
422        forall|i2: int|
423            0 <= i2 < s2.len() && #[trigger] trigger(s2[i2]) ==> exists|i1: int|
424                0 <= i1 < s1.len() && s1[i1] == s2[i2],
425    ensures
426        decreases_to!(s1 => s2),
427;
428
429pub broadcast proof fn axiom_seq_subrange_decreases<A>(s: Seq<A>, i: int, j: int)
430    requires
431        0 <= i <= j <= s.len(),
432        s.subrange(i, j).len() < s.len(),
433    ensures
434        #[trigger] (decreases_to!(s => s.subrange(i, j))),
435{
436    broadcast use {axiom_seq_subrange_len, axiom_seq_subrange_index};
437
438    let s2 = s.subrange(i, j);
439    assert forall|i2: int| 0 <= i2 < s2.len() && #[trigger] trigger(s2[i2]) implies exists|i1: int|
440        0 <= i1 < s.len() && s[i1] == s2[i2] by {
441        assert(s[i + i2] == s2[i2]);
442    }
443    axiom_seq_len_decreases(s, s2);
444}
445
446pub broadcast proof fn axiom_seq_empty<A>()
447    ensures
448        #[trigger] Seq::<A>::empty().len() == 0,
449{
450    let s = Seq::<A>::empty();
451    match s.inner {
452        SeqInner::Nil => {
453            assert(s == Seq { inner: SeqInner::Nil });
454        },
455        SeqInner::Cons { tail, .. } => {
456            let seq_tail = Seq { inner: tail@ };
457            assert(s.len() == 1 + seq_tail.len());
458            assert(s.len() > 0);
459        },
460    }
461}
462
463pub broadcast proof fn axiom_seq_new_len<A>(len: nat, f: spec_fn(int) -> A)
464    ensures
465        #[trigger] Seq::new(len, f).len() == len,
466    decreases len,
467{
468    let s = Seq::new(len, f);
469    if len == 0 {
470        assert(s.len() == 0);
471    } else {
472        broadcast use axiom_seq_push_len;
473
474        let pref = Seq::new((len - 1) as nat, f);
475        axiom_seq_new_len((len - 1) as nat, f);
476        assert(pref.len() == (len - 1) as nat);
477
478        let s2 = pref.push(f(len - 1));
479        assert(s2.len() == pref.len() + 1);
480
481        assert(s == s2);
482        assert(s.len() == len);
483    }
484}
485
486pub broadcast proof fn axiom_seq_new_index<A>(len: nat, f: spec_fn(int) -> A, i: int)
487    requires
488        0 <= i < len,
489    ensures
490        #[trigger] Seq::new(len, f)[i] == f(i),
491    decreases len,
492{
493    broadcast use axiom_seq_new_len;
494
495    let s = Seq::new(len, f);
496    assert(s.len() == len);
497
498    let pref = Seq::new((len - 1) as nat, f);
499    assert(pref.len() == len - 1);
500
501    let a = f(len - 1);
502    assert(s == pref.push(a));
503
504    if i == len - 1 {
505        axiom_seq_push_index_same(pref, a, i);
506        assert(s[i] == a);
507    } else {
508        assert(0 <= i < (len - 1));
509        axiom_seq_new_index((len - 1) as nat, f, i);
510        axiom_seq_push_index_different(pref, a, i);
511    }
512}
513
514proof fn lemma_seq_inner_push_len<A>(s: SeqInner<A>, a: A)
515    ensures
516        s.push(a).len() == s.len() + 1,
517    decreases s.len(),
518{
519    match s {
520        SeqInner::Nil => {},
521        SeqInner::Cons { tail, .. } => {
522            lemma_seq_inner_push_len(tail@, a);
523        },
524    }
525}
526
527pub broadcast proof fn axiom_seq_push_len<A>(s: Seq<A>, a: A)
528    ensures
529        #[trigger] s.push(a).len() == s.len() + 1,
530{
531    lemma_seq_inner_push_len(s.inner, a)
532}
533
534proof fn lemma_seq_inner_push_index_same<A>(s: SeqInner<A>, a: A, i: int)
535    requires
536        i == s.len(),
537    ensures
538        #[trigger] s.push(a)[i] == a,
539    decreases s,
540{
541    match s {
542        SeqInner::Nil => {
543            assert(s.push(a) == SeqInner::Cons { head: a, tail: Ghost(SeqInner::Nil) });
544            assert(s.push(a)[0] == a);
545        },
546        SeqInner::Cons { tail, .. } => {
547            lemma_seq_inner_push_index_same(tail@, a, i - 1);
548        },
549    }
550}
551
552pub broadcast proof fn axiom_seq_push_index_same<A>(s: Seq<A>, a: A, i: int)
553    requires
554        i == s.len(),
555    ensures
556        #[trigger] s.push(a)[i] == a,
557{
558    lemma_seq_inner_push_index_same(s.inner, a, i);
559}
560
561proof fn lemma_seq_inner_index_out_of_bounds<A>(s: SeqInner<A>, i: int)
562    requires
563        !(0 <= i < s.len()),
564    ensures
565        s[i] == arbitrary::<A>(),
566    decreases s,
567{
568    match s {
569        SeqInner::Nil => {},
570        SeqInner::Cons { tail, .. } => {
571            lemma_seq_inner_index_out_of_bounds(tail@, i - 1);
572        },
573    }
574}
575
576proof fn lemma_seq_inner_push_index_different<A>(s: SeqInner<A>, a: A, i: int)
577    requires
578        i < s.len(),
579    ensures
580        #[trigger] s.push(a)[i] == s[i],
581    decreases s,
582{
583    match s {
584        SeqInner::Nil => {
585            lemma_seq_inner_index_out_of_bounds(s.push(a), i);
586        },
587        SeqInner::Cons { tail, .. } => {
588            if i == 0 {
589            } else {
590                lemma_seq_inner_push_index_different(tail@, a, i - 1);
591            }
592        },
593    }
594}
595
596pub broadcast proof fn axiom_seq_push_index_different<A>(s: Seq<A>, a: A, i: int)
597    requires
598        i < s.len(),
599    ensures
600        #[trigger] s.push(a)[i] == s[i],
601{
602    lemma_seq_inner_push_index_different(s.inner, a, i);
603}
604
605// Expensive lemma; not in the default broadcast group
606pub broadcast proof fn lemma_seq_push_index_different_alt<A>(s: Seq<A>, a: A, i: int)
607    requires
608        i < s.len(),
609    ensures
610        (#[trigger] s.push(a))[i] == #[trigger] s[i],
611{
612    broadcast use axiom_seq_push_index_different;
613
614}
615
616proof fn lemma_seq_inner_update_len<A>(s: SeqInner<A>, i: int, a: A)
617    ensures
618        s.update(i, a).len() == s.len(),
619    decreases i,
620{
621    if !(0 <= i < s.len()) {
622        assert(s.update(i, a) == s);
623    } else {
624        let s_upd = s.update(i, a);
625        match s {
626            SeqInner::Nil => {},
627            SeqInner::Cons { head, tail } => {
628                match s_upd {
629                    SeqInner::Nil => {},
630                    SeqInner::Cons { head: head_upd, tail: tail_upd } => {
631                        if i == 0 {
632                            assert(head_upd == a);
633                        } else {
634                            lemma_seq_inner_update_len(tail@, (i - 1), a);
635                        }
636                    },
637                }
638            },
639        }
640    }
641}
642
643pub broadcast proof fn axiom_seq_update_len<A>(s: Seq<A>, i: int, a: A)
644    ensures
645        #[trigger] s.update(i, a).len() == s.len(),
646    decreases i,
647{
648    lemma_seq_inner_update_len(s.inner, i, a)
649}
650
651proof fn lemma_seq_inner_update_index_same<A>(s: SeqInner<A>, i: int, a: A)
652    requires
653        0 <= i < s.len(),
654    ensures
655        #[trigger] s.update(i, a)[i] == a,
656    decreases s,
657{
658    match s {
659        SeqInner::Nil => {},
660        SeqInner::Cons { tail, .. } => {
661            if i == 0 {
662                assert(s.update(i, a)[i] == a)
663            } else {
664                lemma_seq_inner_update_index_same(tail@, i - 1, a);
665            }
666        },
667    }
668}
669
670pub broadcast proof fn axiom_seq_update_same<A>(s: Seq<A>, i: int, a: A)
671    requires
672        0 <= i < s.len(),
673    ensures
674        #[trigger] s.update(i, a)[i] == a,
675{
676    lemma_seq_inner_update_index_same(s.inner, i, a);
677}
678
679// Expensive lemma; not in the default broadcast group
680pub broadcast proof fn lemma_seq_update_same_alt<A>(s: Seq<A>, i: int, a: A)
681    requires
682        0 <= i < s.len(),
683    ensures
684        #![trigger s.update(i, a), s[i]]
685        s.update(i, a)[i] == a,
686{
687    broadcast use axiom_seq_update_same;
688
689}
690
691proof fn lemma_seq_inner_update_index_different<A>(s: SeqInner<A>, i1: int, i2: int, a: A)
692    requires
693        i1 != i2,
694    ensures
695        #[trigger] s.update(i2, a)[i1] == s[i1],
696    decreases s,
697{
698    if !(0 <= i2 < s.len()) {
699        assert(s.update(i2, a) == s);
700    } else {
701        match s {
702            SeqInner::Nil => {},
703            SeqInner::Cons { tail, .. } => {
704                if i2 == 0 {
705                    assert(s.update(i2, a)[i1] == s[i1]);
706                } else if i1 == 0 {
707                    assert(s.update(i2, a)[i1] == s[i1]);
708                } else {
709                    lemma_seq_inner_update_index_different(tail@, i1 - 1, i2 - 1, a);
710                }
711            },
712        }
713    }
714}
715
716pub broadcast proof fn axiom_seq_update_different<A>(s: Seq<A>, i1: int, i2: int, a: A)
717    requires
718        i1 != i2,
719    ensures
720        #[trigger] s.update(i2, a)[i1] == s[i1],
721{
722    lemma_seq_inner_update_index_different(s.inner, i1, i2, a);
723}
724
725// Expensive lemma; not in the default broadcast group
726pub broadcast proof fn lemma_seq_update_different_alt<A>(s: Seq<A>, i1: int, i2: int, a: A)
727    requires
728        i1 != i2,
729    ensures
730        (#[trigger] s.update(i2, a))[i1] == #[trigger] s[i1],
731{
732    broadcast use axiom_seq_update_different;
733
734}
735
736pub broadcast proof fn axiom_seq_ext_equal<A>(s1: Seq<A>, s2: Seq<A>)
737    ensures
738        #[trigger] (s1 =~= s2) <==> {
739            &&& s1.len() == s2.len()
740            &&& forall|i: int| 0 <= i < s1.len() ==> s1[i] == s2[i]
741        },
742    decreases s1.len(),
743{
744    match s1.inner {
745        SeqInner::Nil => {
746            assert(s1.len() == s2.len() <==> s1 =~= s2);
747        },
748        SeqInner::Cons { head: head1, tail: tail1 } => {
749            let seq_tail1 = Seq { inner: tail1@ };
750
751            match s2.inner {
752                SeqInner::Nil => {
753                    assert(s1.len() != s2.len());
754                },
755                SeqInner::Cons { head: head2, tail: tail2 } => {
756                    if head1 != head2 {
757                        assert(s1[0] != s2[0]);
758                    } else {
759                        let seq_tail2 = Seq { inner: tail2@ };
760                        axiom_seq_ext_equal(seq_tail1, seq_tail2);
761                        if seq_tail1 =~= seq_tail2 {
762                            assert(s1.len() == seq_tail1.len() + 1 == seq_tail2.len() + 1
763                                == s2.len());
764                            assert forall|i: int| 0 <= i < s1.len() implies s1[i] == s2[i] by {
765                                if i == 0 {
766                                    assert(s1[0] == s2[0]);
767                                } else {
768                                    assert(s1[i] == s2[i]);
769                                }
770                            }
771                        } else if seq_tail1.len() == seq_tail2.len() {
772                            assert(exists|i: int|
773                                0 <= i < seq_tail1.len() && seq_tail1[i] != seq_tail2[i]);
774                            let i = choose|i: int|
775                                0 <= i < seq_tail1.len() && seq_tail1[i] != seq_tail2[i];
776                            assert(s1[i + 1] != s2[i + 1]);
777                        } else {
778                            assert(s1.len() != s2.len());
779                        }
780                    }
781                },
782            }
783        },
784    }
785}
786
787pub broadcast proof fn axiom_seq_ext_equal_deep<A>(s1: Seq<A>, s2: Seq<A>)
788    ensures
789        #[trigger] (s1 =~~= s2) <==> {
790            &&& s1.len() == s2.len()
791            &&& forall|i: int| 0 <= i < s1.len() ==> s1[i] =~~= s2[i]
792        },
793{
794    match s1.inner {
795        SeqInner::Nil => {
796            assert(s1.len() == s2.len() <==> s1 =~~= s2);
797        },
798        SeqInner::Cons { head: head1, tail: tail1 } => {
799            let seq_tail1 = Seq { inner: tail1@ };
800
801            match s2.inner {
802                SeqInner::Nil => {
803                    assert(s1.len() != s2.len());
804                },
805                SeqInner::Cons { head: head2, tail: tail2 } => {
806                    if head1 != head2 {
807                        assert(s1[0] != s2[0]);
808                    } else {
809                        let seq_tail2 = Seq { inner: tail2@ };
810                        axiom_seq_ext_equal(seq_tail1, seq_tail2);
811                        if seq_tail1 =~~= seq_tail2 {
812                            assert(s1.len() == seq_tail1.len() + 1 == seq_tail2.len() + 1
813                                == s2.len());
814                            assert forall|i: int| 0 <= i < s1.len() implies s1[i] == s2[i] by {
815                                if i == 0 {
816                                    assert(s1[0] == s2[0]);
817                                } else {
818                                    assert(s1[i] == s2[i]);
819                                }
820                            }
821                        } else if seq_tail1.len() == seq_tail2.len() {
822                            assert(exists|i: int|
823                                0 <= i < seq_tail1.len() && seq_tail1[i] != seq_tail2[i]);
824                            let i = choose|i: int|
825                                0 <= i < seq_tail1.len() && seq_tail1[i] != seq_tail2[i];
826                            assert(s1[i + 1] != s2[i + 1]);
827                        } else {
828                            assert(s1.len() != s2.len());
829                        }
830                    }
831                },
832            }
833        },
834    }
835}
836
837proof fn lemma_seq_inner_subrange_len<A>(s: SeqInner<A>, j: int, k: int)
838    requires
839        0 <= j <= k <= s.len(),
840    ensures
841        s.subrange(j, k).len() == k - j,
842    decreases j, k,
843{
844    match s {
845        SeqInner::Nil => {},
846        SeqInner::Cons { head, tail } => {
847            if j > 0 {
848                assert(s.subrange(j, k) == tail.subrange(j - 1, k - 1));
849                lemma_seq_inner_subrange_len(tail@, j - 1, k - 1);
850            } else if k > 0 {
851                let new_tail = tail@.subrange(j, k - 1);
852                lemma_seq_inner_subrange_len(tail@, j, k - 1);
853                assert(new_tail.len() == k - j - 1);
854                let sub = SeqInner::Cons { head, tail: Ghost(new_tail) };
855                assert(sub.len() == 1 + new_tail.len());
856            } else {
857                assert(j == k == 0);
858                assert(s.subrange(j, k).len() == 0);
859            }
860        },
861    }
862}
863
864pub broadcast proof fn axiom_seq_subrange_len<A>(s: Seq<A>, j: int, k: int)
865    requires
866        0 <= j <= k <= s.len(),
867    ensures
868        #[trigger] s.subrange(j, k).len() == k - j,
869{
870    lemma_seq_inner_subrange_len(s.inner, j, k)
871}
872
873proof fn lemma_seq_inner_subrange_index_aux<A>(s: SeqInner<A>, k: int, i: int)
874    requires
875        0 <= k <= s.len(),
876        0 <= i < k,
877    ensures
878        s.subrange(0, k)[i] == s[i],
879    decreases s,
880{
881    lemma_seq_inner_subrange_len(s, 0, k);
882    // assert(s.subrange(0, k).len() == k);
883    // assert(0 <= i < s.subrange(0, k).len());
884    match s {
885        SeqInner::Nil => {
886            // assert(false);
887        },
888        SeqInner::Cons { head, tail } => {
889            if i == 0 {
890                // assert(s[0] == head);
891                assert(s.subrange(0, k)[0] == head);
892            } else {
893                lemma_seq_inner_subrange_index_aux(tail@, k - 1, i - 1);
894            }
895        },
896    }
897}
898
899proof fn lemma_seq_inner_subrange_index<A>(s: SeqInner<A>, j: int, k: int, i: int)
900    requires
901        0 <= j <= k <= s.len(),
902        0 <= i < k - j,
903    ensures
904        s.subrange(j, k)[i] == s[i + j],
905    decreases s,
906{
907    lemma_seq_inner_subrange_len(s, j, k);
908    if j == 0 {
909        lemma_seq_inner_subrange_index_aux(s, k, i);
910    } else {
911        match s {
912            SeqInner::Nil => {
913                assert(false);
914            },
915            SeqInner::Cons { head, tail } => {
916                lemma_seq_inner_subrange_index(tail@, j - 1, k - 1, i);
917            },
918        }
919    }
920}
921
922pub broadcast proof fn axiom_seq_subrange_index<A>(s: Seq<A>, j: int, k: int, i: int)
923    requires
924        0 <= j <= k <= s.len(),
925        0 <= i < k - j,
926    ensures
927        #[trigger] s.subrange(j, k)[i] == s[i + j],
928{
929    lemma_seq_inner_subrange_index(s.inner, j, k, i);
930}
931
932// Expensive lemma; not in the default broadcast group
933pub broadcast proof fn lemma_seq_subrange_index_alt<A>(s: Seq<A>, j: int, k: int, i: int)
934    requires
935        0 <= j <= k <= s.len(),
936        0 <= i - j < k - j,
937    ensures
938        (#[trigger] s.subrange(j, k))[i - j] == #[trigger] s[i],
939{
940    broadcast use axiom_seq_subrange_index;
941
942}
943
944// Less expensive, more limited alternative to lemma_seq_subrange_index_alt
945pub broadcast proof fn lemma_seq_two_subranges_index<A>(s: Seq<A>, j: int, k1: int, k2: int, i: int)
946    requires
947        0 <= j <= k1 <= s.len(),
948        0 <= j <= k2 <= s.len(),
949        0 <= i < k1 - j,
950        0 <= i < k2 - j,
951    ensures
952        #[trigger] s.subrange(j, k1)[i] == (#[trigger] s.subrange(j, k2))[i],
953{
954    broadcast use axiom_seq_subrange_index;
955
956}
957
958proof fn lemma_seq_inner_add_len<A>(s1: SeqInner<A>, s2: SeqInner<A>)
959    ensures
960        s1.add(s2).len() == s1.len() + s2.len(),
961    decreases s1.add(s2).len(),
962{
963    let sum = s1.add(s2);
964    match s1 {
965        SeqInner::Nil => {
966            assert(sum == s2);
967        },
968        SeqInner::Cons { head, tail } => {
969            let new_tail = tail@.add(s2);
970            lemma_seq_inner_add_len(tail@, s2);
971            assert(new_tail.len() == (s1.len() - 1) + s2.len());
972            assert(sum.len() == 1 + new_tail.len());
973        },
974    }
975}
976
977pub broadcast proof fn axiom_seq_add_len<A>(s1: Seq<A>, s2: Seq<A>)
978    ensures
979        #[trigger] s1.add(s2).len() == s1.len() + s2.len(),
980{
981    lemma_seq_inner_add_len(s1.inner, s2.inner);
982}
983
984proof fn lemma_seq_inner_add_index1<A>(s1: SeqInner<A>, s2: SeqInner<A>, i: int)
985    requires
986        i < s1.len(),
987    ensures
988        s1.add(s2)[i] == s1[i],
989    decreases s1,
990{
991    if i < 0 {
992        lemma_seq_inner_index_out_of_bounds(s1, i);
993        lemma_seq_inner_index_out_of_bounds(s1.add(s2), i);
994    } else {
995        match s1 {
996            SeqInner::Nil => {},
997            SeqInner::Cons { head, tail } => {
998                if i == 0 {
999                    assert(s1[i] == s1.add(s2)[i]);
1000                } else {
1001                    lemma_seq_inner_add_index1(tail@, s2, i - 1);
1002                }
1003            },
1004        }
1005    }
1006}
1007
1008pub broadcast proof fn axiom_seq_add_index1<A>(s1: Seq<A>, s2: Seq<A>, i: int)
1009    requires
1010        i < s1.len(),
1011    ensures
1012        #[trigger] s1.add(s2)[i] == s1[i],
1013{
1014    lemma_seq_inner_add_index1(s1.inner, s2.inner, i)
1015}
1016
1017proof fn lemma_seq_inner_add_index2<A>(s1: SeqInner<A>, s2: SeqInner<A>, i: int)
1018    requires
1019        s1.len() <= i < s1.len() + s2.len(),
1020    ensures
1021        s1.add(s2)[i] == s2[i - s1.len()],
1022    decreases s1,
1023{
1024    match s1 {
1025        SeqInner::Nil => {
1026            assert(s1.add(s2) == s2);
1027            assert(s1.add(s2)[i] == s2[i - s1.len()]);
1028        },
1029        SeqInner::Cons { head, tail } => {
1030            if i == 0 {
1031                assert(s1.add(s2)[i] == s2[i - s1.len()]);
1032            } else {
1033                lemma_seq_inner_add_index2(tail@, s2, i - 1);
1034                assert(s1.add(s2)[i] == s2[i - s1.len()]);
1035            }
1036        },
1037    }
1038}
1039
1040pub broadcast proof fn axiom_seq_add_index2<A>(s1: Seq<A>, s2: Seq<A>, i: int)
1041    requires
1042        s1.len() <= i < s1.len() + s2.len(),
1043    ensures
1044        #[trigger] s1.add(s2)[i] == s2[i - s1.len()],
1045{
1046    lemma_seq_inner_add_index2(s1.inner, s2.inner, i);
1047}
1048
1049// Expensive lemma; not in the default broadcast group
1050pub broadcast proof fn lemma_seq_add_index1_alt<A>(s1: Seq<A>, s2: Seq<A>, i: int)
1051    requires
1052        0 <= i < s1.len(),
1053    ensures
1054        (#[trigger] s1.add(s2))[i] == #[trigger] s1[i],
1055{
1056    broadcast use axiom_seq_add_index1;
1057
1058}
1059
1060// Expensive lemma; not in the default broadcast group
1061pub broadcast proof fn lemma_seq_add_index2_alt<A>(s1: Seq<A>, s2: Seq<A>, i: int)
1062    requires
1063        0 <= i < s2.len(),
1064    ensures
1065        (#[trigger] s1.add(s2))[i + s1.len()] == #[trigger] s2[i],
1066{
1067    broadcast use axiom_seq_add_index2;
1068
1069}
1070
1071pub broadcast group group_seq_axioms {
1072    axiom_seq_index_decreases,
1073    axiom_seq_subrange_decreases,
1074    axiom_seq_empty,
1075    axiom_seq_new_len,
1076    axiom_seq_new_index,
1077    axiom_seq_push_len,
1078    axiom_seq_push_index_same,
1079    axiom_seq_push_index_different,
1080    axiom_seq_update_len,
1081    axiom_seq_update_same,
1082    axiom_seq_update_different,
1083    axiom_seq_ext_equal,
1084    axiom_seq_ext_equal_deep,
1085    axiom_seq_subrange_len,
1086    axiom_seq_subrange_index,
1087    lemma_seq_two_subranges_index,
1088    axiom_seq_add_len,
1089    axiom_seq_add_index1,
1090    axiom_seq_add_index2,
1091}
1092
1093// Expensive lemmas not in the default group (may slow down verification)
1094pub broadcast group group_seq_lemmas_expensive {
1095    lemma_seq_push_index_different_alt,
1096    lemma_seq_update_same_alt,
1097    lemma_seq_update_different_alt,
1098    lemma_seq_subrange_index_alt,
1099    lemma_seq_add_index1_alt,
1100    lemma_seq_add_index2_alt,
1101}
1102
1103// ------------- Macros ---------------- //
1104#[doc(hidden)]
1105#[macro_export]
1106macro_rules! seq_internal {
1107    [] => {
1108        $crate::vstd::seq::Seq::empty()
1109    };
1110    [$elem:expr] => {
1111        $crate::vstd::seq::Seq::empty()
1112            .push($elem)
1113    };
1114    [$elem:expr,] => {
1115        $crate::vstd::seq::Seq::empty()
1116            .push($elem)
1117    };
1118    [$($elem:expr),* $(,)?] => {
1119        <_ as $crate::vstd::view::View>::view(&[$($elem),*])
1120    };
1121    [$elem:expr; $n:expr] => {
1122        $crate::vstd::seq::Seq::new(
1123            $n,
1124            $crate::vstd::prelude::closure_to_fn_spec(
1125                |_x: _| $elem
1126            ),
1127        )
1128    };
1129}
1130
1131/// Creates a [`Seq`] containing the given elements.
1132///
1133/// ## Example
1134///
1135/// ```rust
1136/// let s = seq![11int, 12, 13];
1137///
1138/// assert(s.len() == 3);
1139/// assert(s[0] == 11);
1140/// assert(s[1] == 12);
1141/// assert(s[2] == 13);
1142/// ```
1143#[macro_export]
1144macro_rules! seq {
1145    [$($tail:tt)*] => {
1146        $crate::vstd::prelude::verus_proof_macro_exprs!($crate::vstd::seq::seq_internal!($($tail)*))
1147    };
1148}
1149
1150#[doc(hidden)]
1151pub use seq_internal;
1152pub use seq;
1153
1154} // verus!
vstd/seq.rs

vstd/
seq.rs
