vstd/
seq.rs

1use core::marker;
2
3#[allow(unused_imports)]
4use super::pervasive::*;
5#[allow(unused_imports)]
6use super::prelude::*;
7
8use verus as verus_skip_verusfmt; // verusfmt doesn't handle s[..e] yet
9verus_skip_verusfmt! {
10
11#[verifier::ext_equal]
12#[verifier::accept_recursive_types(A)]
13tracked enum SeqInner<A> {
14    Nil,
15    Cons { head: Tracked<A>, tail: Tracked<SeqInner<A>> },
16}
17
18// This indirection is required to show the termination of `Seq::len`
19//
20// If we translated this to `Seq` we the decrease clauses wouldn't work,
21// because we would have had to re-internalize the tail into a `Seq`
22impl<A> SeqInner<A> {
23    spec fn len(self) -> nat
24        decreases self,
25    {
26        match self {
27            SeqInner::Nil => 0,
28            SeqInner::Cons { tail, .. } => { 1 + tail.len() },
29        }
30    }
31
32    spec fn index(self, i: int) -> A
33        recommends
34            0 <= i < self.len(),
35        decreases self.len(),
36    {
37        match self {
38            SeqInner::Nil => arbitrary(),
39            SeqInner::Cons { head, tail } => if i == 0 {
40                head@
41            } else {
42                tail.index(i - 1)
43            },
44        }
45    }
46
47    #[verifier::inline]
48    spec fn spec_index(self, i: int) -> A
49        recommends
50            0 <= i < self.len(),
51    {
52        self.index(i)
53    }
54
55    #[verifier::inline]
56    spec fn spec_index_range<I: Integer, J: Integer>(self, i: I, j: J) -> Self
57        recommends
58            0 <= i as int <= j as int <= self.len(),
59    {
60        self.subrange(i as int, j as int)
61    }
62
63    spec fn first(self) -> A
64        recommends
65            0 < self.len(),
66    {
67        self[0]
68    }
69
70    spec fn last(self) -> A
71        recommends
72            0 < self.len(),
73    {
74        self[self.len() as int - 1]
75    }
76
77    spec fn push(self, a: A) -> SeqInner<A>
78        decreases self.len(),
79    {
80        match self {
81            SeqInner::Nil => SeqInner::Cons { head: Tracked(a), tail: Tracked(SeqInner::Nil) },
82            SeqInner::Cons { head, tail } => {
83                let new_tail = tail.push(a);
84                SeqInner::Cons { head, tail: Tracked(new_tail) }
85            },
86        }
87    }
88
89    spec fn update(self, i: int, a: A) -> SeqInner<A>
90        recommends
91            0 <= i < self.len(),
92        decreases self.len(),
93    {
94        if !(0 <= i < self.len()) {  // this supports weakening some preconditions
95            self
96        } else {
97            match self {
98                SeqInner::Nil => arbitrary(),
99                SeqInner::Cons { head, tail } => if i == 0 {
100                    SeqInner::Cons { head: Tracked(a), tail }
101                } else {
102                    let new_tail = tail.update(i - 1, a);
103                    SeqInner::Cons { head, tail: Tracked(new_tail) }
104                },
105            }
106        }
107    }
108
109    spec fn subrange(self, start_inclusive: int, end_exclusive: int) -> SeqInner<A>
110        recommends
111            0 <= start_inclusive <= end_exclusive <= self.len(),
112        decreases start_inclusive, end_exclusive - start_inclusive,
113    {
114        match self {
115            SeqInner::Nil => SeqInner::Nil,
116            SeqInner::Cons {
117                head,
118                tail,
119            } =>
120            // skip elements until start_inclusive becomes 0
121            if start_inclusive > 0 {
122                tail.subrange(start_inclusive - 1, end_exclusive - 1)
123            } else {
124                if end_exclusive <= 0 {
125                    SeqInner::Nil
126                } else {
127                    let new_tail = tail.subrange(start_inclusive, end_exclusive - 1);
128                    SeqInner::Cons { head, tail: Tracked(new_tail) }
129                }
130            },
131        }
132    }
133
134    spec fn add(self, rhs: SeqInner<A>) -> SeqInner<A>
135        decreases self.len(),
136    {
137        match self {
138            SeqInner::Nil => rhs,
139            SeqInner::Cons { head, tail } => {
140                let new_tail = tail.add(rhs);
141                SeqInner::Cons { head, tail: Tracked(new_tail) }
142            },
143        }
144    }
145
146    spec fn insert(self, i: int, a: A) -> SeqInner<A>
147        recommends
148            0 <= i <= self.len(),
149    {
150        self.subrange(0, i).push(a).add(self.subrange(i, self.len() as int))
151    }
152
153    spec fn remove(self, i: int) -> SeqInner<A>
154        recommends
155            0 <= i < self.len(),
156    {
157        self.subrange(0, i).add(self.subrange(i + 1, self.len() as int))
158    }
159
160    // return the suffix
161    proof fn tracked_split_at(tracked &mut self, i: int) -> (tracked ret: Self)
162        requires
163            0 <= i <= old(self).len(),
164        ensures
165            *final(self) == old(self)[0..i],
166            ret == old(self)[i..old(self).len()],
167            final(self).len() == i,
168            ret.len() == old(self).len() - i,
169        decreases self.len(),
170    {
171        let tracked mut s = SeqInner::Nil;
172        super::modes::tracked_swap(&mut s, self);
173        let tracked ret = if i == 0 {
174            seq_inner::lemma_subrange_len(*old(self), 0, i);
175            seq_inner::lemma_empty(old(self)[0..i]);
176            seq_inner::lemma_full_subrange_idempotent(*old(self));
177
178            s
179        } else {
180            let ghost old_self = s;
181            match s {
182                SeqInner::Nil => {
183                    assert(false);
184                    proof_from_false()
185                },
186                SeqInner::Cons { head, tail } => {
187                    let tracked Tracked(mut tail) = tail;
188                    let ghost old_tail = tail;
189                    let tracked suff = tail.tracked_split_at(i - 1);
190
191                    let tracked mut new = SeqInner::Cons { head, tail: Tracked(tail) };
192
193                    super::modes::tracked_swap(&mut new, self);
194
195                    suff
196                },
197            }
198        };
199
200        assert(*final(self) == old(self)[0..i]);
201        assert(ret == old(self)[i..old(self).len()]);
202        seq_inner::lemma_subrange_len(*old(self), 0, i);
203        seq_inner::lemma_subrange_len(*old(self), i, old(self).len() as int);
204
205        ret
206    }
207
208    proof fn tracked_add(tracked &mut self, tracked mut b: Self)
209        ensures
210            *final(self) == old(self).add(b),
211            final(self).len() == old(self).len() + b.len(),
212        decreases self.len(),
213    {
214        let tracked mut s = SeqInner::Nil;
215        super::modes::tracked_swap(&mut s, self);
216        match s {
217            SeqInner::Nil => {
218                seq_inner::lemma_empty(*old(self));
219                super::modes::tracked_swap(&mut b, self);
220            },
221            SeqInner::Cons { head, tail } => {
222                let tracked Tracked(mut tail) = tail;
223                tail.tracked_add(b);
224                let tracked mut new = SeqInner::Cons { head, tail: Tracked(tail) };
225                super::modes::tracked_swap(&mut new, self);
226                seq_inner::lemma_add_len(s, b);
227            },
228        }
229    }
230
231    proof fn tracked_insert(tracked &mut self, i: int, tracked v: A)
232        requires
233            0 <= i <= old(self).len(),
234        ensures
235            final(self).len() == old(self).len() + 1,
236            *final(self) == old(self).insert(i, v),
237        decreases self.len(),
238    {
239        if i == self.len() {
240            seq_inner::lemma_subrange_len(*old(self), i, self.len() as int);
241            seq_inner::lemma_empty(old(self)[i..self.len()]);
242            seq_inner::lemma_full_subrange_idempotent(*old(self));
243            seq_inner::lemma_add_empty(self.push(v));
244            self.tracked_push(v);
245        } else {
246            let tracked suff = self.tracked_split_at(i);
247            self.tracked_push(v);
248            self.tracked_add(suff);
249        }
250    }
251
252    proof fn tracked_remove(tracked &mut self, i: int) -> (tracked ret: A)
253        requires
254            0 <= i < old(self).len(),
255        ensures
256            ret == old(self)[i],
257            final(self).len() == old(self).len() - 1,
258            *final(self) == old(self).remove(i),
259        decreases self.len(),
260    {
261        if i == 0 {
262            self.tracked_pop_front()
263        } else {
264            let tracked suff = self.tracked_split_at(i + 1);
265            assert(suff == old(self)[i + 1..old(self).len()]);
266
267            let tracked ret = self.tracked_pop();
268            seq_inner::lemma_subrange_index(*old(self), 0, i + 1, i);
269            assert(ret == old(self)[i]);
270            assert(*self == old(self)[0..i + 1][0..i]);
271            seq_inner::lemma_subrange_composition(*old(self), 0, i + 1, 0, i);
272
273            self.tracked_add(suff);
274            ret
275        }
276    }
277
278    proof fn tracked_borrow(tracked &self, i: int) -> (tracked ret: &A)
279        requires
280            0 <= i < self.len(),
281        ensures
282            *ret == self[i],
283        decreases self.len(),
284    {
285        if i == 0 {
286            match self {
287                SeqInner::Nil => {
288                    assert(false);
289                    proof_from_false()
290                },
291                SeqInner::Cons { head, .. } => { head.borrow() },
292            }
293        } else {
294            match self {
295                SeqInner::Nil => {
296                    assert(false);
297                    proof_from_false()
298                },
299                SeqInner::Cons { tail, .. } => { tail.tracked_borrow(i - 1) },
300            }
301        }
302    }
303
304    proof fn tracked_borrow_mut(tracked &mut self, i: int) -> (tracked ret: &mut A)
305        requires
306            0 <= i < old(self).len(),
307        ensures
308            *ret == old(self)[i],
309            *final(self) == old(self).update(i, *final(ret)),
310        decreases self.len(),
311    {
312        if i == 0 {
313            match self {
314                SeqInner::Nil => {
315                    assert(false);
316                    proof_from_false()
317                },
318                SeqInner::Cons { head, .. } => { head.borrow_mut() },
319            }
320        } else {
321            match self {
322                SeqInner::Nil => {
323                    assert(false);
324                    proof_from_false()
325                },
326                SeqInner::Cons { tail, .. } => { tail.tracked_borrow_mut(i - 1) },
327            }
328        }
329    }
330
331    proof fn tracked_push(tracked &mut self, tracked v: A)
332        ensures
333            *final(self) == old(self).push(v),
334            final(self).len() == old(self).len() + 1,
335        decreases self.len(),
336    {
337        let tracked mut s = SeqInner::Nil;
338        super::modes::tracked_swap(&mut s, self);
339        match s {
340            SeqInner::Nil => {
341                let tracked mut new = SeqInner::Cons {
342                    head: Tracked(v),
343                    tail: Tracked(SeqInner::Nil),
344                };
345                super::modes::tracked_swap(&mut new, self);
346            },
347            SeqInner::Cons { head, tail } => {
348                let tracked Tracked(mut tail) = tail;
349                tail.tracked_push(v);
350                let tracked mut new = SeqInner::Cons { head, tail: Tracked(tail) };
351                super::modes::tracked_swap(&mut new, self);
352            },
353        }
354        assert(*final(self) == old(self).push(v));
355        seq_inner::lemma_push_len(*old(self), v);
356    }
357
358    proof fn tracked_push_front(tracked &mut self, tracked v: A)
359        ensures
360            *final(self) == old(self).insert(0, v),
361            final(self).len() == old(self).len() + 1,
362        decreases self.len(),
363    {
364        self.tracked_insert(0, v);
365    }
366
367    proof fn tracked_pop(tracked &mut self) -> (tracked ret: A)
368        requires
369            old(self).len() > 0,
370        ensures
371            ret == old(self).last(),
372            final(self).len() == old(self).len() - 1,
373            *final(self) == old(self)[0..old(self).len() - 1],
374        decreases self.len(),
375    {
376        let tracked mut s = SeqInner::Nil;
377        super::modes::tracked_swap(&mut s, self);
378
379        let tracked ret = match s {
380            SeqInner::Nil => {
381                assert(false);
382                proof_from_false()
383            },
384            SeqInner::Cons { head, tail } => {
385                let tracked Tracked(mut tail) = tail;
386                let tracked Tracked(head) = head;
387
388                let tracked v = match tail {
389                    SeqInner::Nil => {
390                        let tracked mut new = SeqInner::Nil;
391                        super::modes::tracked_swap(&mut new, self);
392
393                        seq_inner::lemma_empty(tail);
394                        seq_inner::lemma_subrange_len(*old(self), 0, old(self).len() - 1);
395                        seq_inner::lemma_empty(old(self)[0..old(self).len() - 1]);
396
397                        head
398                    },
399                    SeqInner::Cons { head: thead, tail: ttail } => {
400                        let tracked mut tail = SeqInner::Cons { head: thead, tail: ttail };
401                        let tracked v = tail.tracked_pop();
402
403                        let tracked mut new = SeqInner::Cons {
404                            head: Tracked(head),
405                            tail: Tracked(tail),
406                        };
407                        super::modes::tracked_swap(&mut new, self);
408
409                        v
410                    },
411                };
412
413                v
414            },
415        };
416
417        assert(*final(self) == old(self)[0..old(self).len() - 1]);
418        seq_inner::lemma_subrange_len(*old(self), 0, old(self).len() - 1);
419
420        ret
421    }
422
423    proof fn tracked_pop_front(tracked &mut self) -> (tracked ret: A)
424        requires
425            old(self).len() > 0,
426        ensures
427            ret == old(self).first(),
428            final(self).len() == old(self).len() - 1,
429            *final(self) == old(self)[1..old(self).len()],
430    {
431        let tracked mut s = SeqInner::Nil;
432        super::modes::tracked_swap(&mut s, self);
433        let tracked ret = match s {
434            SeqInner::Nil => {
435                assert(false);
436                proof_from_false()
437            },
438            SeqInner::Cons { head, tail } => {
439                let tracked Tracked(mut tail) = tail;
440                let tracked Tracked(head) = head;
441                seq_inner::lemma_tail_subrange(head, tail);
442                assert(tail == old(self)[1..old(self).len()]);
443                super::modes::tracked_swap(&mut tail, self);
444                head
445            },
446        };
447
448        assert(*final(self) == old(self)[1..old(self).len()]);
449        seq_inner::lemma_subrange_len(*old(self), 1, old(self).len() as int);
450
451        ret
452    }
453}
454
455mod seq_inner {
456    use super::*;
457
458    // empty
459    pub(super) proof fn lemma_empty<A>(s: SeqInner<A>)
460        ensures
461            s.len() == 0 <==> s == SeqInner::Nil,
462    {
463        if s.len() == 0 {
464            assert(s == SeqInner::Nil)
465        }
466        if s == SeqInner::Nil {
467            assert(s.len() == 0);
468        }
469    }
470
471    // push lemmas
472    pub(super) proof fn lemma_push_len<A>(s: SeqInner<A>, a: A)
473        ensures
474            s.push(a).len() == s.len() + 1,
475        decreases s.len(),
476    {
477        match s {
478            SeqInner::Nil => {},
479            SeqInner::Cons { tail, .. } => {
480                lemma_push_len(tail@, a);
481            },
482        }
483    }
484
485    pub(super) proof fn lemma_push_index_different<A>(s: SeqInner<A>, a: A, i: int)
486        requires
487            i < s.len(),
488        ensures
489            #[trigger] s.push(a)[i] == s[i],
490        decreases s,
491    {
492        match s {
493            SeqInner::Nil => {
494                lemma_index_out_of_bounds(s.push(a), i);
495            },
496            SeqInner::Cons { tail, .. } => {
497                if i == 0 {
498                } else {
499                    lemma_push_index_different(tail@, a, i - 1);
500                }
501            },
502        }
503    }
504
505    pub(super) proof fn lemma_push_index_same<A>(s: SeqInner<A>, a: A, i: int)
506        requires
507            i == s.len(),
508        ensures
509            #[trigger] s.push(a)[i] == a,
510        decreases s,
511    {
512        match s {
513            SeqInner::Nil => {
514                assert(s.push(a) == SeqInner::Cons {
515                    head: Tracked(a),
516                    tail: Tracked(SeqInner::Nil),
517                });
518                assert(s.push(a)[0] == a);
519            },
520            SeqInner::Cons { tail, .. } => {
521                lemma_push_index_same(tail@, a, i - 1);
522            },
523        }
524    }
525
526    // update lemmas
527    pub(super) proof fn lemma_update_len<A>(s: SeqInner<A>, i: int, a: A)
528        ensures
529            s.update(i, a).len() == s.len(),
530        decreases i,
531    {
532        if !(0 <= i < s.len()) {
533            assert(s.update(i, a) == s);
534        } else {
535            let s_upd = s.update(i, a);
536            match s {
537                SeqInner::Nil => {},
538                SeqInner::Cons { head, tail } => {
539                    match s_upd {
540                        SeqInner::Nil => {},
541                        SeqInner::Cons { head: head_upd, tail: tail_upd } => {
542                            if i == 0 {
543                                assert(head_upd == a);
544                            } else {
545                                lemma_update_len(tail@, (i - 1), a);
546                            }
547                        },
548                    }
549                },
550            }
551        }
552    }
553
554    pub(super) proof fn lemma_update_index_same<A>(s: SeqInner<A>, i: int, a: A)
555        requires
556            0 <= i < s.len(),
557        ensures
558            #[trigger] s.update(i, a)[i] == a,
559        decreases s,
560    {
561        match s {
562            SeqInner::Nil => {},
563            SeqInner::Cons { tail, .. } => {
564                if i == 0 {
565                    assert(s.update(i, a)[i] == a)
566                } else {
567                    lemma_update_index_same(tail@, i - 1, a);
568                }
569            },
570        }
571    }
572
573    pub(super) proof fn lemma_update_index_different<A>(s: SeqInner<A>, i1: int, i2: int, a: A)
574        requires
575            i1 != i2,
576        ensures
577            #[trigger] s.update(i2, a)[i1] == s[i1],
578        decreases s,
579    {
580        if !(0 <= i2 < s.len()) {
581            assert(s.update(i2, a) == s);
582        } else {
583            match s {
584                SeqInner::Nil => {},
585                SeqInner::Cons { tail, .. } => {
586                    if i2 == 0 {
587                        assert(s.update(i2, a)[i1] == s[i1]);
588                    } else if i1 == 0 {
589                        assert(s.update(i2, a)[i1] == s[i1]);
590                    } else {
591                        lemma_update_index_different(tail@, i1 - 1, i2 - 1, a);
592                    }
593                },
594            }
595        }
596    }
597
598    // subrange lemmas
599    pub(super) proof fn lemma_subrange_len<A>(s: SeqInner<A>, j: int, k: int)
600        requires
601            0 <= j <= k <= s.len(),
602        ensures
603            s[j..k].len() == k - j,
604        decreases j, k,
605    {
606        match s {
607            SeqInner::Nil => {},
608            SeqInner::Cons { head, tail } => {
609                if j > 0 {
610                    assert(s[j..k] == tail[j - 1..k - 1]);
611                    lemma_subrange_len(tail@, j - 1, k - 1);
612                } else if k > 0 {
613                    let new_tail = tail@[j..k - 1];
614                    lemma_subrange_len(tail@, j, k - 1);
615                    assert(new_tail.len() == k - j - 1);
616                    let sub = SeqInner::Cons { head, tail: Tracked(new_tail) };
617                    assert(sub.len() == 1 + new_tail.len());
618                } else {
619                    assert(j == k == 0);
620                    assert(s[j..k].len() == 0);
621                }
622            },
623        }
624    }
625
626    pub(super) proof fn lemma_subrange_composition_aux2<A>(s: SeqInner<A>, j1: int, j2: int)
627        requires
628            0 <= j2 <= j1 <= s.len(),
629        ensures
630            s[0..j1][0..j2] == s[0..j2],
631        decreases s.len(),
632    {
633        if j1 == j2 {
634            lemma_subrange_len(s, 0, j1);
635            lemma_full_subrange_idempotent(s[0..j1]);
636        } else if j1 == 0 {
637            assert(false);
638        } else if j2 == 0 {
639            lemma_subrange_len(s[0..j1], 0, j2);
640            lemma_empty(s[0..j1][0..j2]);
641        } else {
642            match s {
643                SeqInner::Nil => {},
644                SeqInner::Cons { head, tail } => {
645                    lemma_subrange_composition_aux2(tail@, j1 - 1, j2 - 1);
646                },
647            }
648        }
649    }
650
651    pub(super) proof fn lemma_subrange_index_aux<A>(s: SeqInner<A>, k: int, i: int)
652        requires
653            0 <= k <= s.len(),
654            0 <= i < k,
655        ensures
656            s[0..k][i] == s[i],
657        decreases s,
658    {
659        lemma_subrange_len(s, 0, k);
660        // assert(s[0..k].len() == k);
661        // assert(0 <= i < s[0..k].len());
662        match s {
663            SeqInner::Nil => {
664                // assert(false);
665            },
666            SeqInner::Cons { head, tail } => {
667                if i == 0 {
668                    // assert(s[0] == head);
669                    assert(s[0..k][0] == head);
670                } else {
671                    lemma_subrange_index_aux(tail@, k - 1, i - 1);
672                }
673            },
674        }
675    }
676
677    pub(super) proof fn lemma_subrange_index<A>(s: SeqInner<A>, j: int, k: int, i: int)
678        requires
679            0 <= j <= k <= s.len(),
680            0 <= i < k - j,
681        ensures
682            s[j..k][i] == s[i + j],
683        decreases s,
684    {
685        lemma_subrange_len(s, j, k);
686        if j == 0 {
687            lemma_subrange_index_aux(s, k, i);
688        } else {
689            match s {
690                SeqInner::Nil => {
691                    assert(false);
692                },
693                SeqInner::Cons { head, tail } => {
694                    lemma_subrange_index(tail@, j - 1, k - 1, i);
695                },
696            }
697        }
698    }
699
700    pub(super) proof fn lemma_subrange_composition_aux1<A>(
701        s: SeqInner<A>,
702        j1: int,
703        i2: int,
704        j2: int,
705    )
706        requires
707            0 <= j1 <= s.len(),
708            0 <= i2 <= j2 <= j1,
709        ensures
710            s[0..j1][i2..j2] == s[i2..j2],
711        decreases s.len(),
712    {
713        if i2 == 0 {
714            lemma_subrange_composition_aux2(s, j1, j2);
715        } else {
716            match s {
717                SeqInner::Nil => {},
718                SeqInner::Cons { head, tail } => {
719                    lemma_subrange_composition_aux1(tail@, j1 - 1, i2 - 1, j2 - 1);
720                },
721            }
722        }
723    }
724
725    pub(super) proof fn lemma_subrange_composition<A>(
726        s: SeqInner<A>,
727        i1: int,
728        j1: int,
729        i2: int,
730        j2: int,
731    )
732        requires
733            0 <= i1 <= j1 <= s.len(),
734            0 <= i2 <= j2 <= j1 - i1,
735        ensures
736            s[i1..j1][i2..j2] == s[i1 + i2..i1 + j2],
737        decreases s.len(),
738    {
739        if i1 == 0 {
740            lemma_subrange_composition_aux1(s, j1, i2, j2);
741        } else {
742            match s {
743                SeqInner::Nil => {},
744                SeqInner::Cons { head, tail } => {
745                    lemma_subrange_composition(tail@, i1 - 1, j1 - 1, i2, j2);
746                },
747            }
748        }
749    }
750
751    pub(super) open spec fn cons_list<A>(head: A, tail: SeqInner<A>) -> SeqInner<A> {
752        SeqInner::Cons { head: Tracked(head), tail: Tracked(tail) }
753    }
754
755    pub(super) proof fn lemma_tail_subrange<A>(head: A, tail: SeqInner<A>)
756        ensures
757            cons_list(head, tail)[1..cons_list(head, tail).len()] == tail,
758    {
759        let s = SeqInner::Cons { head: Tracked(head), tail: Tracked(tail) };
760        match s {
761            SeqInner::Nil => {
762                assert(false);
763            },
764            SeqInner::Cons { head: h, tail: t } => { lemma_full_subrange_idempotent(tail) },
765        }
766    }
767
768    pub(super) proof fn lemma_full_subrange_idempotent<A>(s: SeqInner<A>)
769        ensures
770            s[0..s.len()] == s,
771        decreases s.len(),
772    {
773        match s {
774            SeqInner::Nil => {
775                assert(s[0..s.len()] == s);
776            },
777            SeqInner::Cons { head, tail } => {
778                lemma_subrange_index(s, 0, s.len() as int, 0);
779                lemma_full_subrange_idempotent(tail@);
780            },
781        }
782    }
783
784    // decrease to index
785    pub(super) proof fn lemma_index_decreases<A>(s: SeqInner<A>, i: int)
786        requires
787            0 <= i < s.len(),
788        ensures
789            (decreases_to!(s => s[i])),
790        decreases i,
791    {
792        match s {
793            SeqInner::Nil => {
794                assert(s.len() == 0);
795                assert(false);
796            },
797            SeqInner::Cons { head, tail } => {
798                if i == 0 {
799                    assert(decreases_to!(s => s[i]));
800                } else {
801                    assert(tail[i - 1] == s[i]);
802                    lemma_index_decreases(tail@, i - 1);
803                    assert(decreases_to!(s => tail@));
804                    assert(decreases_to!(tail@ => tail[i-1]));
805                }
806            },
807        }
808    }
809
810    // add lemmas
811    pub(super) proof fn lemma_add_empty<A>(s: SeqInner<A>)
812        ensures
813            s.add(SeqInner::Nil) == s,
814            SeqInner::Nil.add(s) == s,
815        decreases s.len(),
816    {
817        assert(SeqInner::Nil.add(s) == s);
818
819        let sum = s.add(SeqInner::Nil);
820        match s {
821            SeqInner::Nil => {
822                assert(sum == SeqInner::Nil);
823                assert(s == SeqInner::Nil);
824            },
825            SeqInner::Cons { head, tail } => {
826                assert(sum == SeqInner::Cons { head, tail: Tracked(tail@.add(SeqInner::Nil)) });
827                lemma_add_empty(tail@);
828            },
829        }
830    }
831
832    pub(super) proof fn lemma_add_len<A>(s1: SeqInner<A>, s2: SeqInner<A>)
833        ensures
834            s1.add(s2).len() == s1.len() + s2.len(),
835        decreases s1.add(s2).len(),
836    {
837        let sum = s1.add(s2);
838        match s1 {
839            SeqInner::Nil => {
840                assert(sum == s2);
841            },
842            SeqInner::Cons { head, tail } => {
843                let new_tail = tail@.add(s2);
844                lemma_add_len(tail@, s2);
845                assert(new_tail.len() == (s1.len() - 1) + s2.len());
846                assert(sum.len() == 1 + new_tail.len());
847            },
848        }
849    }
850
851    pub(super) proof fn lemma_add_index1<A>(s1: SeqInner<A>, s2: SeqInner<A>, i: int)
852        requires
853            i < s1.len(),
854        ensures
855            s1.add(s2)[i] == s1[i],
856        decreases s1,
857    {
858        if i < 0 {
859            lemma_index_out_of_bounds(s1, i);
860            lemma_index_out_of_bounds(s1.add(s2), i);
861        } else {
862            match s1 {
863                SeqInner::Nil => {},
864                SeqInner::Cons { head, tail } => {
865                    if i == 0 {
866                        assert(s1[i] == s1.add(s2)[i]);
867                    } else {
868                        lemma_add_index1(tail@, s2, i - 1);
869                    }
870                },
871            }
872        }
873    }
874
875    pub(super) proof fn lemma_add_index2<A>(s1: SeqInner<A>, s2: SeqInner<A>, i: int)
876        requires
877            s1.len() <= i < s1.len() + s2.len(),
878        ensures
879            s1.add(s2)[i] == s2[i - s1.len()],
880        decreases s1,
881    {
882        match s1 {
883            SeqInner::Nil => {
884                assert(s1.add(s2) == s2);
885                assert(s1.add(s2)[i] == s2[i - s1.len()]);
886            },
887            SeqInner::Cons { head, tail } => {
888                if i == 0 {
889                    assert(s1.add(s2)[i] == s2[i - s1.len()]);
890                } else {
891                    lemma_add_index2(tail@, s2, i - 1);
892                    assert(s1.add(s2)[i] == s2[i - s1.len()]);
893                }
894            },
895        }
896    }
897
898    // index lemma
899    pub(super) proof fn lemma_index_out_of_bounds<A>(s: SeqInner<A>, i: int)
900        requires
901            !(0 <= i < s.len()),
902        ensures
903            s[i] == arbitrary::<A>(),
904        decreases s,
905    {
906        match s {
907            SeqInner::Nil => {},
908            SeqInner::Cons { tail, .. } => {
909                lemma_index_out_of_bounds(tail@, i - 1);
910            },
911        }
912    }
913
914}
915
916/// `Seq<A>` is a sequence type for specifications.
917/// To use a "sequence" in compiled code, use an `exec` type like `vec::Vec`
918/// that has `Seq<A>` as its specification type.
919///
920/// An object `seq: Seq<A>` has a length, given by [`seq.len()`](Seq::len),
921/// and a value at each `i` for `0 <= i < seq.len()`, given by [`seq[i]`](Seq::index).
922///
923/// Sequences can be constructed in a few different ways:
924///  * [`Seq::empty`] construct an empty sequence (`len() == 0`)
925///  * [`Seq::new`] construct a sequence of a given length, initialized according
926///     to a given function mapping indices `i` to values `A`.
927///  * The [`seq!`] macro, to construct small sequences of a fixed size (analagous to the
928///     [`std::vec!`] macro).
929///  * By manipulating an existing sequence with [`Seq::push`], [`Seq::update`],
930///    or [`Seq::add`].
931///
932/// To prove that two sequences are equal, it is usually easiest to use the
933/// extensional equality operator `=~=`.
934#[verifier::ext_equal]
935#[verifier::accept_recursive_types(A)]
936pub tracked struct Seq<A> {
937    inner: SeqInner<A>,
938}
939
940impl<A> Seq<A> {
941    /// An empty sequence (i.e., a sequence of length 0).
942    #[rustc_diagnostic_item = "verus::vstd::seq::Seq::empty"]
943    pub closed spec fn empty() -> Seq<A> {
944        Seq { inner: SeqInner::Nil }
945    }
946
947    /// Construct a sequence `s` of length `len` where entry `s[i]` is given by `f(i)`.
948    #[rustc_diagnostic_item = "verus::vstd::seq::Seq::new"]
949    pub closed spec fn new(len: nat, f: spec_fn(int) -> A) -> Seq<A>
950        decreases len,
951    {
952        if len == 0 {
953            Seq { inner: SeqInner::Nil }
954        } else {
955            Self::new((len - 1) as nat, f).push(f(len - 1))
956        }
957    }
958
959    /// The length of a sequence.
960    #[rustc_diagnostic_item = "verus::vstd::seq::Seq::len"]
961    pub closed spec fn len(self) -> nat {
962        self.inner.len()
963    }
964
965    /// Gets the value at the given index `i`.
966    ///
967    /// If `i` is not in the range `[0, self.len())`, then the resulting value
968    /// is meaningless and arbitrary.
969    #[rustc_diagnostic_item = "verus::vstd::seq::Seq::index"]
970    pub closed spec fn index(self, i: int) -> A
971        recommends
972            0 <= i < self.len(),
973    {
974        self.inner.index(i)
975    }
976
977    /// `[]` operator, synonymous with `index`
978    #[verifier::inline]
979    pub open spec fn spec_index(self, i: int) -> A
980        recommends
981            0 <= i < self.len(),
982    {
983        self.index(i)
984    }
985
986    /// `[..]` operator, which returns the original Seq
987    #[verifier::inline]
988    pub open spec fn spec_index_range_full(self) -> Seq<A> {
989        self
990    }
991
992    /// `[i..]` operator, synonymous with `skip`
993    #[verifier::inline]
994    pub open spec fn spec_index_range_from<I: Integer>(self, i: I) -> Seq<A>
995        recommends
996            0 <= i as int <= self.len(),
997    {
998        self.skip(i as int)
999    }
1000
1001    /// `[..j]` operator, synonymous with `take`
1002    #[verifier::inline]
1003    pub open spec fn spec_index_range_to<J: Integer>(self, j: J) -> Seq<A>
1004        recommends
1005            0 <= j as int <= self.len(),
1006    {
1007        self.take(j as int)
1008    }
1009
1010    /// `[..=j]` operator, synonymous with `take` on j + 1
1011    #[verifier::inline]
1012    pub open spec fn spec_index_range_to_inclusive<J: Integer>(self, j: J) -> Seq<A>
1013        recommends
1014            0 <= (j as int) < self.len(),
1015    {
1016        self.take(j as int + 1)
1017    }
1018
1019    /// `[i..j]` operator, synonymous with `subrange`
1020    #[verifier::inline]
1021    pub open spec fn spec_index_range<I: Integer, J: Integer>(self, i: I, j: J) -> Seq<A>
1022        recommends
1023            0 <= i as int <= j as int <= self.len(),
1024    {
1025        self.subrange(i as int, j as int)
1026    }
1027
1028    /// `[i..=j]` operator, synonymous with `subrange` on j + 1
1029    #[verifier::inline]
1030    pub open spec fn spec_index_range_inclusive<I: Integer, J: Integer>(self, i: I, j: J) -> Seq<A>
1031        recommends
1032            0 <= i as int <= (j as int) < self.len(),
1033    {
1034        self.subrange(i as int, j as int + 1)
1035    }
1036
1037    /// Appends the value `a` to the end of the sequence.
1038    /// This always increases the length of the sequence by 1.
1039    /// This often requires annotating the type of the element literal in the sequence,
1040    /// e.g., `10int`.
1041    ///
1042    /// ## Example
1043    ///
1044    /// ```rust
1045    /// proof fn push_test() {
1046    ///     assert(seq![10int, 11, 12].push(13) =~= seq![10, 11, 12, 13]);
1047    /// }
1048    /// ```
1049    #[rustc_diagnostic_item = "verus::vstd::seq::Seq::push"]
1050    pub closed spec fn push(self, a: A) -> Seq<A> {
1051        Seq { inner: self.inner.push(a) }
1052    }
1053
1054    /// Updates the sequence at the given index, replacing the element with the given
1055    /// value, and leaves all other entries unchanged.
1056    ///
1057    /// ## Example
1058    ///
1059    /// ```rust
1060    /// proof fn update_test() {
1061    ///     let s = seq![10, 11, 12, 13, 14];
1062    ///     let t = s.update(2, -5);
1063    ///     assert(t =~= seq![10, 11, -5, 13, 14]);
1064    /// }
1065    /// ```
1066    #[rustc_diagnostic_item = "verus::vstd::seq::Seq::update"]
1067    pub closed spec fn update(self, i: int, a: A) -> Seq<A>
1068        recommends
1069            0 <= i < self.len(),
1070    {
1071        Seq { inner: self.inner.update(i, a) }
1072    }
1073
1074    /// Returns a sequence for the given subrange.
1075    ///
1076    /// ## Example
1077    ///
1078    /// ```rust
1079    /// proof fn subrange_test() {
1080    ///     let s = seq![10int, 11, 12, 13, 14];
1081    ///     //                      ^-------^
1082    ///     //           0      1   2   3   4   5
1083    ///     let sub = s[2..4];
1084    ///     assert(sub =~= seq![12, 13]);
1085    /// }
1086    /// ```
1087    #[rustc_diagnostic_item = "verus::vstd::seq::Seq::subrange"]
1088    pub closed spec fn subrange(self, start_inclusive: int, end_exclusive: int) -> Seq<A>
1089        recommends
1090            0 <= start_inclusive <= end_exclusive <= self.len(),
1091    {
1092        Seq { inner: self.inner.subrange(start_inclusive, end_exclusive) }
1093    }
1094
1095    /// Returns a sequence containing only the first n elements of the original sequence
1096    #[verifier::inline]
1097    pub open spec fn take(self, n: int) -> Seq<A> {
1098        self.subrange(0, n)
1099    }
1100
1101    /// Returns a sequence without the first n elements of the original sequence
1102    #[verifier::inline]
1103    pub open spec fn skip(self, n: int) -> Seq<A> {
1104        self.subrange(n, self.len() as int)
1105    }
1106
1107    /// Concatenates the sequences.
1108    ///
1109    /// ## Example
1110    ///
1111    /// ```rust
1112    /// proof fn add_test() {
1113    ///     assert(seq![10int, 11].add(seq![12, 13, 14])
1114    ///             =~= seq![10, 11, 12, 13, 14]);
1115    /// }
1116    /// ```
1117    #[rustc_diagnostic_item = "verus::vstd::seq::Seq::add"]
1118    pub closed spec fn add(self, rhs: Seq<A>) -> Seq<A> {
1119        Seq { inner: self.inner.add(rhs.inner) }
1120    }
1121
1122    /// `+` operator, synonymous with `add`
1123    #[verifier::inline]
1124    pub open spec fn spec_add(self, rhs: Seq<A>) -> Seq<A> {
1125        self.add(rhs)
1126    }
1127
1128    /// Returns the last element of the sequence.
1129    #[rustc_diagnostic_item = "verus::vstd::seq::Seq::last"]
1130    pub open spec fn last(self) -> A
1131        recommends
1132            0 < self.len(),
1133    {
1134        self[self.len() as int - 1]
1135    }
1136
1137    /// Returns the first element of the sequence.
1138    #[rustc_diagnostic_item = "vstd::seq::Seq::first"]
1139    pub open spec fn first(self) -> A
1140        recommends
1141            0 < self.len(),
1142    {
1143        self[0]
1144    }
1145
1146    /// Create an empty sequence
1147    pub proof fn tracked_empty() -> (tracked ret: Self)
1148        ensures
1149            ret == Seq::empty(),
1150    {
1151        Seq { inner: SeqInner::Nil }
1152    }
1153
1154    /// Insert a tracked element into a sequence
1155    ///
1156    /// ## Example
1157    ///
1158    /// ```rust
1159    /// proof fn insert_test(tracked &mut s: Seq<int>, tracked v: int)
1160    ///     requires
1161    ///         old(s)@ == seq![0, 1, 2]
1162    ///     ensures
1163    ///         final(s)@ == seq![0, 1, v, 2]
1164    /// {
1165    ///     s.tracked_insert(2, v)
1166    /// }
1167    /// ```
1168    pub proof fn tracked_insert(tracked &mut self, i: int, tracked v: A)
1169        requires
1170            0 <= i <= old(self).len(),
1171        ensures
1172            final(self).len() == old(self).len() + 1,
1173            *final(self) == old(self).insert(i, v),
1174    {
1175        self.inner.tracked_insert(i, v)
1176    }
1177
1178    /// Remove a tracked element from a sequence
1179    pub proof fn tracked_remove(tracked &mut self, i: int) -> (tracked ret: A)
1180        requires
1181            0 <= i < old(self).len(),
1182        ensures
1183            ret == old(self)[i],
1184            final(self).len() == old(self).len() - 1,
1185            *final(self) == old(self).remove(i),
1186    {
1187        self.inner.tracked_remove(i)
1188    }
1189
1190    /// Obtain a tracked borrow into an element of a sequence
1191    pub proof fn tracked_borrow(tracked &self, i: int) -> (tracked ret: &A)
1192        requires
1193            0 <= i < self.len(),
1194        ensures
1195            *ret == self[i],
1196    {
1197        self.inner.tracked_borrow(i)
1198    }
1199
1200    /// Obtain a tracked mutable borrow into an element of a sequence
1201    pub proof fn tracked_borrow_mut(tracked &mut self, i: int) -> (tracked ret: &mut A)
1202        requires
1203            0 <= i < old(self).len(),
1204        ensures
1205            *ret == old(self)[i],
1206            *final(self) == old(self).update(i, *final(ret)),
1207    {
1208        self.inner.tracked_borrow_mut(i)
1209    }
1210
1211    /// Push a tracked value into the end of a sequence
1212    pub proof fn tracked_push(tracked &mut self, tracked v: A)
1213        ensures
1214            *final(self) == old(self).push(v),
1215            final(self).len() == old(self).len() + 1,
1216    {
1217        self.inner.tracked_push(v)
1218    }
1219
1220    /// Push a tracked value into the beginning of a sequence
1221    pub proof fn tracked_push_front(tracked &mut self, tracked v: A)
1222        ensures
1223            *final(self) == old(self).insert(0, v),
1224            final(self).len() == old(self).len() + 1,
1225    {
1226        self.inner.tracked_push_front(v)
1227    }
1228
1229    /// Pop a tracked value from the end of a sequence
1230    pub proof fn tracked_pop(tracked &mut self) -> (tracked ret: A)
1231        requires
1232            old(self).len() > 0,
1233        ensures
1234            ret == old(self).last(),
1235            final(self).len() == old(self).len() - 1,
1236            *final(self) == old(self)[..old(self).len() - 1],
1237    {
1238        self.inner.tracked_pop()
1239    }
1240
1241    /// Pop a tracked value from the beginning of a sequence
1242    pub proof fn tracked_pop_front(tracked &mut self) -> (tracked ret: A)
1243        requires
1244            old(self).len() > 0,
1245        ensures
1246            ret == old(self).first(),
1247            final(self).len() == old(self).len() - 1,
1248            *final(self) == old(self).drop_first(),
1249    {
1250        self.inner.tracked_pop_front()
1251    }
1252
1253    /// Split a tracked sequence around an index
1254    pub proof fn tracked_split_at(tracked &mut self, i: int) -> (tracked ret: Self)
1255        requires
1256            0 <= i <= old(self).len(),
1257        ensures
1258            *final(self) == old(self)[0..i],
1259            ret == old(self)[i..old(self).len()],
1260            final(self).len() == i,
1261            ret.len() == old(self).len() - i,
1262    {
1263        Seq { inner: self.inner.tracked_split_at(i) }
1264    }
1265
1266    proof fn tracked_add(tracked &mut self, tracked b: Self)
1267        ensures
1268            *final(self) == old(self).add(b),
1269            final(self).len() == old(self).len() + b.len(),
1270    {
1271        self.inner.tracked_add(b.inner)
1272    }
1273}
1274
1275#[deprecated(note = "Seq axioms have been verified, and are now lemmas")]
1276pub broadcast proof fn axiom_seq_index_decreases<A>(s: Seq<A>, i: int)
1277    requires
1278        0 <= i < s.len(),
1279    ensures
1280        #[trigger] (decreases_to!(s => s[i])),
1281{
1282    lemma_seq_index_decreases(s, i)
1283}
1284
1285pub broadcast proof fn lemma_seq_index_decreases<A>(s: Seq<A>, i: int)
1286    requires
1287        0 <= i < s.len(),
1288    ensures
1289        #[trigger] (decreases_to!(s => s[i])),
1290{
1291    seq_inner::lemma_index_decreases(s.inner, i)
1292}
1293
1294// TODO: this should be provable
1295pub axiom fn axiom_seq_len_decreases<A>(s1: Seq<A>, s2: Seq<A>)
1296    requires
1297        s2.len() < s1.len(),
1298        forall|i2: int|
1299            0 <= i2 < s2.len() && #[trigger] trigger(s2[i2]) ==> exists|i1: int|
1300                0 <= i1 < s1.len() && s1[i1] == s2[i2],
1301    ensures
1302        decreases_to!(s1 => s2),
1303;
1304
1305#[deprecated(note = "Seq axioms have been verified, and are now lemmas")]
1306pub broadcast proof fn axiom_seq_subrange_decreases<A>(s: Seq<A>, i: int, j: int)
1307    requires
1308        0 <= i <= j <= s.len(),
1309        s[i..j].len() < s.len(),
1310    ensures
1311        #[trigger] (decreases_to!(s => s[i..j])),
1312{
1313    lemma_seq_subrange_decreases(s, i, j)
1314}
1315
1316pub broadcast proof fn lemma_seq_subrange_decreases<A>(s: Seq<A>, i: int, j: int)
1317    requires
1318        0 <= i <= j <= s.len(),
1319        s[i..j].len() < s.len(),
1320    ensures
1321        #[trigger] (decreases_to!(s => s[i..j])),
1322{
1323    broadcast use {lemma_seq_subrange_len, lemma_seq_subrange_index};
1324
1325    let s2 = s[i..j];
1326    assert forall|i2: int| 0 <= i2 < s2.len() && #[trigger] trigger(s2[i2]) implies exists|i1: int|
1327        0 <= i1 < s.len() && s[i1] == s2[i2] by {
1328        assert(s[i + i2] == s2[i2]);
1329    }
1330    axiom_seq_len_decreases(s, s2);
1331}
1332
1333#[deprecated(note = "Seq axioms have been verified, and are now lemmas")]
1334pub broadcast proof fn axiom_seq_empty<A>()
1335    ensures
1336        #[trigger] Seq::<A>::empty().len() == 0,
1337{
1338    broadcast use lemma_seq_empty;
1339
1340}
1341
1342pub broadcast proof fn lemma_seq_empty<A>()
1343    ensures
1344        #[trigger] Seq::<A>::empty().len() == 0,
1345{
1346    let s = Seq::<A>::empty();
1347    match s.inner {
1348        SeqInner::Nil => {
1349            assert(s == Seq { inner: SeqInner::Nil });
1350        },
1351        SeqInner::Cons { tail, .. } => {
1352            let seq_tail = Seq { inner: tail@ };
1353            assert(s.len() == 1 + seq_tail.len());
1354            assert(s.len() > 0);
1355        },
1356    }
1357}
1358
1359#[deprecated(note = "Seq axioms have been verified, and are now lemmas")]
1360pub broadcast proof fn axiom_seq_new_len<A>(len: nat, f: spec_fn(int) -> A)
1361    ensures
1362        #[trigger] Seq::new(len, f).len() == len,
1363{
1364    lemma_seq_new_len(len, f)
1365}
1366
1367pub broadcast proof fn lemma_seq_new_len<A>(len: nat, f: spec_fn(int) -> A)
1368    ensures
1369        #[trigger] Seq::new(len, f).len() == len,
1370    decreases len,
1371{
1372    let s = Seq::new(len, f);
1373    if len == 0 {
1374        assert(s.len() == 0);
1375    } else {
1376        broadcast use lemma_seq_push_len;
1377
1378        let pref = Seq::new((len - 1) as nat, f);
1379        lemma_seq_new_len((len - 1) as nat, f);
1380        assert(pref.len() == (len - 1) as nat);
1381
1382        let s2 = pref.push(f(len - 1));
1383        assert(s2.len() == pref.len() + 1);
1384
1385        assert(s == s2);
1386        assert(s.len() == len);
1387    }
1388}
1389
1390#[deprecated(note = "Seq axioms have been verified, and are now lemmas")]
1391pub broadcast proof fn axiom_seq_new_index<A>(len: nat, f: spec_fn(int) -> A, i: int)
1392    requires
1393        0 <= i < len,
1394    ensures
1395        #[trigger] Seq::new(len, f)[i] == f(i),
1396{
1397    lemma_seq_new_index(len, f, i)
1398}
1399
1400pub broadcast proof fn lemma_seq_new_index<A>(len: nat, f: spec_fn(int) -> A, i: int)
1401    requires
1402        0 <= i < len,
1403    ensures
1404        #[trigger] Seq::new(len, f)[i] == f(i),
1405    decreases len,
1406{
1407    broadcast use lemma_seq_new_len;
1408
1409    let s = Seq::new(len, f);
1410    assert(s.len() == len);
1411
1412    let pref = Seq::new((len - 1) as nat, f);
1413    assert(pref.len() == len - 1);
1414
1415    let a = f(len - 1);
1416    assert(s == pref.push(a));
1417
1418    if i == len - 1 {
1419        lemma_seq_push_index_same(pref, a, i);
1420        assert(s[i] == a);
1421    } else {
1422        assert(0 <= i < (len - 1));
1423        lemma_seq_new_index((len - 1) as nat, f, i);
1424        lemma_seq_push_index_different(pref, a, i);
1425    }
1426}
1427
1428#[deprecated(note = "Seq axioms have been verified, and are now lemmas")]
1429pub broadcast proof fn axiom_seq_push_len<A>(s: Seq<A>, a: A)
1430    ensures
1431        #[trigger] s.push(a).len() == s.len() + 1,
1432{
1433    lemma_seq_push_len(s, a)
1434}
1435
1436pub broadcast proof fn lemma_seq_push_len<A>(s: Seq<A>, a: A)
1437    ensures
1438        #[trigger] s.push(a).len() == s.len() + 1,
1439{
1440    seq_inner::lemma_push_len(s.inner, a)
1441}
1442
1443#[deprecated(note = "Seq axioms have been verified, and are now lemmas")]
1444pub broadcast proof fn axiom_seq_push_index_same<A>(s: Seq<A>, a: A, i: int)
1445    requires
1446        i == s.len(),
1447    ensures
1448        #[trigger] s.push(a)[i] == a,
1449{
1450    lemma_seq_push_index_same(s, a, i)
1451}
1452
1453pub broadcast proof fn lemma_seq_push_index_same<A>(s: Seq<A>, a: A, i: int)
1454    requires
1455        i == s.len(),
1456    ensures
1457        #[trigger] s.push(a)[i] == a,
1458{
1459    seq_inner::lemma_push_index_same(s.inner, a, i);
1460}
1461
1462#[deprecated(note = "Seq axioms have been verified, and are now lemmas")]
1463pub broadcast proof fn axiom_seq_push_index_different<A>(s: Seq<A>, a: A, i: int)
1464    requires
1465        i < s.len(),
1466    ensures
1467        #[trigger] s.push(a)[i] == s[i],
1468{
1469    lemma_seq_push_index_different(s, a, i)
1470}
1471
1472pub broadcast proof fn lemma_seq_push_index_different<A>(s: Seq<A>, a: A, i: int)
1473    requires
1474        i < s.len(),
1475    ensures
1476        #[trigger] s.push(a)[i] == s[i],
1477{
1478    seq_inner::lemma_push_index_different(s.inner, a, i);
1479}
1480
1481// Expensive lemma; not in the default broadcast group
1482pub broadcast proof fn lemma_seq_push_index_different_alt<A>(s: Seq<A>, a: A, i: int)
1483    requires
1484        i < s.len(),
1485    ensures
1486        (#[trigger] s.push(a))[i] == #[trigger] s[i],
1487{
1488    broadcast use lemma_seq_push_index_different;
1489
1490}
1491
1492#[deprecated(note = "Seq axioms have been verified, and are now lemmas")]
1493pub broadcast proof fn axiom_seq_update_len<A>(s: Seq<A>, i: int, a: A)
1494    ensures
1495        #[trigger] s.update(i, a).len() == s.len(),
1496{
1497    lemma_seq_update_len(s, i, a)
1498}
1499
1500pub broadcast proof fn lemma_seq_update_len<A>(s: Seq<A>, i: int, a: A)
1501    ensures
1502        #[trigger] s.update(i, a).len() == s.len(),
1503    decreases i,
1504{
1505    seq_inner::lemma_update_len(s.inner, i, a)
1506}
1507
1508#[deprecated(note = "Seq axioms have been verified, and are now lemmas")]
1509pub broadcast proof fn axiom_seq_update_same<A>(s: Seq<A>, i: int, a: A)
1510    requires
1511        0 <= i < s.len(),
1512    ensures
1513        #[trigger] s.update(i, a)[i] == a,
1514{
1515    lemma_seq_update_same(s, i, a)
1516}
1517
1518pub broadcast proof fn lemma_seq_update_same<A>(s: Seq<A>, i: int, a: A)
1519    requires
1520        0 <= i < s.len(),
1521    ensures
1522        #[trigger] s.update(i, a)[i] == a,
1523{
1524    seq_inner::lemma_update_index_same(s.inner, i, a);
1525}
1526
1527// Expensive lemma; not in the default broadcast group
1528pub broadcast proof fn lemma_seq_update_same_alt<A>(s: Seq<A>, i: int, a: A)
1529    requires
1530        0 <= i < s.len(),
1531    ensures
1532        #![trigger s.update(i, a), s[i]]
1533        s.update(i, a)[i] == a,
1534{
1535    broadcast use lemma_seq_update_same;
1536
1537}
1538
1539#[deprecated(note = "Seq axioms have been verified, and are now lemmas")]
1540pub broadcast proof fn axiom_seq_update_different<A>(s: Seq<A>, i1: int, i2: int, a: A)
1541    requires
1542        i1 != i2,
1543    ensures
1544        #[trigger] s.update(i2, a)[i1] == s[i1],
1545{
1546    lemma_seq_update_different(s, i1, i2, a)
1547}
1548
1549pub broadcast proof fn lemma_seq_update_different<A>(s: Seq<A>, i1: int, i2: int, a: A)
1550    requires
1551        i1 != i2,
1552    ensures
1553        #[trigger] s.update(i2, a)[i1] == s[i1],
1554{
1555    seq_inner::lemma_update_index_different(s.inner, i1, i2, a);
1556}
1557
1558// Expensive lemma; not in the default broadcast group
1559pub broadcast proof fn lemma_seq_update_different_alt<A>(s: Seq<A>, i1: int, i2: int, a: A)
1560    requires
1561        i1 != i2,
1562    ensures
1563        (#[trigger] s.update(i2, a))[i1] == #[trigger] s[i1],
1564{
1565    broadcast use lemma_seq_update_different;
1566
1567}
1568
1569#[deprecated(note = "Seq axioms have been verified, and are now lemmas")]
1570pub broadcast proof fn axiom_seq_ext_equal<A>(s1: Seq<A>, s2: Seq<A>)
1571    ensures
1572        #[trigger] (s1 =~= s2) <==> {
1573            &&& s1.len() == s2.len()
1574            &&& forall|i: int| 0 <= i < s1.len() ==> s1[i] == s2[i]
1575        },
1576{
1577    lemma_seq_ext_equal(s1, s2)
1578}
1579
1580pub broadcast proof fn lemma_seq_ext_equal<A>(s1: Seq<A>, s2: Seq<A>)
1581    ensures
1582        #[trigger] (s1 =~= s2) <==> {
1583            &&& s1.len() == s2.len()
1584            &&& forall|i: int| 0 <= i < s1.len() ==> s1[i] == s2[i]
1585        },
1586    decreases s1.len(),
1587{
1588    match s1.inner {
1589        SeqInner::Nil => {
1590            assert(s1.len() == s2.len() <==> s1 =~= s2);
1591        },
1592        SeqInner::Cons { head: head1, tail: tail1 } => {
1593            let seq_tail1 = Seq { inner: tail1@ };
1594
1595            match s2.inner {
1596                SeqInner::Nil => {
1597                    assert(s1.len() != s2.len());
1598                },
1599                SeqInner::Cons { head: head2, tail: tail2 } => {
1600                    if head1 != head2 {
1601                        assert(s1[0] != s2[0]);
1602                    } else {
1603                        let seq_tail2 = Seq { inner: tail2@ };
1604                        lemma_seq_ext_equal(seq_tail1, seq_tail2);
1605                        if seq_tail1 =~= seq_tail2 {
1606                            assert(s1.len() == seq_tail1.len() + 1 == seq_tail2.len() + 1
1607                                == s2.len());
1608                            assert forall|i: int| 0 <= i < s1.len() implies s1[i] == s2[i] by {
1609                                if i == 0 {
1610                                    assert(s1[0] == s2[0]);
1611                                } else {
1612                                    assert(s1[i] == s2[i]);
1613                                }
1614                            }
1615                        } else if seq_tail1.len() == seq_tail2.len() {
1616                            assert(exists|i: int|
1617                                0 <= i < seq_tail1.len() && seq_tail1[i] != seq_tail2[i]);
1618                            let i = choose|i: int|
1619                                0 <= i < seq_tail1.len() && seq_tail1[i] != seq_tail2[i];
1620                            assert(s1[i + 1] != s2[i + 1]);
1621                        } else {
1622                            assert(s1.len() != s2.len());
1623                        }
1624                    }
1625                },
1626            }
1627        },
1628    }
1629}
1630
1631#[deprecated(note = "Seq axioms have been verified, and are now lemmas")]
1632pub broadcast proof fn axiom_seq_ext_equal_deep<A>(s1: Seq<A>, s2: Seq<A>)
1633    ensures
1634        #[trigger] (s1 =~~= s2) <==> {
1635            &&& s1.len() == s2.len()
1636            &&& forall|i: int| 0 <= i < s1.len() ==> s1[i] =~~= s2[i]
1637        },
1638{
1639    lemma_seq_ext_equal_deep(s1, s2)
1640}
1641
1642pub broadcast proof fn lemma_seq_ext_equal_deep<A>(s1: Seq<A>, s2: Seq<A>)
1643    ensures
1644        #[trigger] (s1 =~~= s2) <==> {
1645            &&& s1.len() == s2.len()
1646            &&& forall|i: int| 0 <= i < s1.len() ==> s1[i] =~~= s2[i]
1647        },
1648{
1649    match s1.inner {
1650        SeqInner::Nil => {
1651            assert(s1.len() == s2.len() <==> s1 =~~= s2);
1652        },
1653        SeqInner::Cons { head: head1, tail: tail1 } => {
1654            let seq_tail1 = Seq { inner: tail1@ };
1655
1656            match s2.inner {
1657                SeqInner::Nil => {
1658                    assert(s1.len() != s2.len());
1659                },
1660                SeqInner::Cons { head: head2, tail: tail2 } => {
1661                    if head1 != head2 {
1662                        assert(s1[0] != s2[0]);
1663                    } else {
1664                        let seq_tail2 = Seq { inner: tail2@ };
1665                        lemma_seq_ext_equal(seq_tail1, seq_tail2);
1666                        if seq_tail1 =~~= seq_tail2 {
1667                            assert(s1.len() == seq_tail1.len() + 1 == seq_tail2.len() + 1
1668                                == s2.len());
1669                            assert forall|i: int| 0 <= i < s1.len() implies s1[i] == s2[i] by {
1670                                if i == 0 {
1671                                    assert(s1[0] == s2[0]);
1672                                } else {
1673                                    assert(s1[i] == s2[i]);
1674                                }
1675                            }
1676                        } else if seq_tail1.len() == seq_tail2.len() {
1677                            assert(exists|i: int|
1678                                0 <= i < seq_tail1.len() && seq_tail1[i] != seq_tail2[i]);
1679                            let i = choose|i: int|
1680                                0 <= i < seq_tail1.len() && seq_tail1[i] != seq_tail2[i];
1681                            assert(s1[i + 1] != s2[i + 1]);
1682                        } else {
1683                            assert(s1.len() != s2.len());
1684                        }
1685                    }
1686                },
1687            }
1688        },
1689    }
1690}
1691
1692#[deprecated(note = "Seq axioms have been verified, and are now lemmas")]
1693pub broadcast proof fn axiom_seq_subrange_len<A>(s: Seq<A>, j: int, k: int)
1694    requires
1695        0 <= j <= k <= s.len(),
1696    ensures
1697        #[trigger] s[j..k].len() == k - j,
1698{
1699    lemma_seq_subrange_len(s, j, k)
1700}
1701
1702pub broadcast proof fn lemma_seq_subrange_len<A>(s: Seq<A>, j: int, k: int)
1703    requires
1704        0 <= j <= k <= s.len(),
1705    ensures
1706        #[trigger] s[j..k].len() == k - j,
1707{
1708    seq_inner::lemma_subrange_len(s.inner, j, k)
1709}
1710
1711pub broadcast proof fn lemma_seq_subrange_composition<A>(
1712    s: Seq<A>,
1713    i1: int,
1714    j1: int,
1715    i2: int,
1716    j2: int,
1717)
1718    requires
1719        0 <= i1 <= j1 <= s.len(),
1720        0 <= i2 <= j2 <= j1 - i1,
1721    ensures
1722        #[trigger] s[i1..j1][i2..j2] == s[i1 + i2..i1 + j2],
1723{
1724    seq_inner::lemma_subrange_composition(s.inner, i1, j1, i2, j2)
1725}
1726
1727#[deprecated(note = "Seq axioms have been verified, and are now lemmas")]
1728pub broadcast proof fn axiom_seq_subrange_index<A>(s: Seq<A>, j: int, k: int, i: int)
1729    requires
1730        0 <= j <= k <= s.len(),
1731        0 <= i < k - j,
1732    ensures
1733        #[trigger] s[j..k][i] == s[i + j],
1734{
1735    lemma_seq_subrange_index(s, j, k, i)
1736}
1737
1738pub broadcast proof fn lemma_seq_subrange_index<A>(s: Seq<A>, j: int, k: int, i: int)
1739    requires
1740        0 <= j <= k <= s.len(),
1741        0 <= i < k - j,
1742    ensures
1743        #[trigger] s[j..k][i] == s[i + j],
1744{
1745    seq_inner::lemma_subrange_index(s.inner, j, k, i);
1746}
1747
1748// Expensive lemma; not in the default broadcast group
1749pub broadcast proof fn lemma_seq_subrange_index_alt<A>(s: Seq<A>, j: int, k: int, i: int)
1750    requires
1751        0 <= j <= k <= s.len(),
1752        0 <= i - j < k - j,
1753    ensures
1754        (#[trigger] s[j..k])[i - j] == #[trigger] s[i],
1755{
1756    broadcast use lemma_seq_subrange_index;
1757
1758}
1759
1760// Less expensive, more limited alternative to lemma_seq_subrange_index_alt
1761pub broadcast proof fn lemma_seq_two_subranges_index<A>(s: Seq<A>, j: int, k1: int, k2: int, i: int)
1762    requires
1763        0 <= j <= k1 <= s.len(),
1764        0 <= j <= k2 <= s.len(),
1765        0 <= i < k1 - j,
1766        0 <= i < k2 - j,
1767    ensures
1768        #[trigger] s[j..k1][i] == (#[trigger] s[j..k2])[i],
1769{
1770    broadcast use lemma_seq_subrange_index;
1771
1772}
1773
1774#[deprecated(note = "Seq axioms have been verified, and are now lemmas")]
1775pub broadcast proof fn axiom_seq_add_len<A>(s1: Seq<A>, s2: Seq<A>)
1776    ensures
1777        #[trigger] s1.add(s2).len() == s1.len() + s2.len(),
1778{
1779    lemma_seq_add_len(s1, s2)
1780}
1781
1782pub broadcast proof fn lemma_seq_add_len<A>(s1: Seq<A>, s2: Seq<A>)
1783    ensures
1784        #[trigger] s1.add(s2).len() == s1.len() + s2.len(),
1785{
1786    seq_inner::lemma_add_len(s1.inner, s2.inner);
1787}
1788
1789#[deprecated(note = "Seq axioms have been verified, and are now lemmas")]
1790pub broadcast proof fn axiom_seq_add_index1<A>(s1: Seq<A>, s2: Seq<A>, i: int)
1791    requires
1792        i < s1.len(),
1793    ensures
1794        #[trigger] s1.add(s2)[i] == s1[i],
1795{
1796    lemma_seq_add_index1(s1, s2, i)
1797}
1798
1799pub broadcast proof fn lemma_seq_add_index1<A>(s1: Seq<A>, s2: Seq<A>, i: int)
1800    requires
1801        i < s1.len(),
1802    ensures
1803        #[trigger] s1.add(s2)[i] == s1[i],
1804{
1805    seq_inner::lemma_add_index1(s1.inner, s2.inner, i)
1806}
1807
1808#[deprecated(note = "Seq axioms have been verified, and are now lemmas")]
1809pub broadcast proof fn axiom_seq_add_index2<A>(s1: Seq<A>, s2: Seq<A>, i: int)
1810    requires
1811        s1.len() <= i < s1.len() + s2.len(),
1812    ensures
1813        #[trigger] s1.add(s2)[i] == s2[i - s1.len()],
1814{
1815    lemma_seq_add_index2(s1, s2, i)
1816}
1817
1818pub broadcast proof fn lemma_seq_add_index2<A>(s1: Seq<A>, s2: Seq<A>, i: int)
1819    requires
1820        s1.len() <= i < s1.len() + s2.len(),
1821    ensures
1822        #[trigger] s1.add(s2)[i] == s2[i - s1.len()],
1823{
1824    seq_inner::lemma_add_index2(s1.inner, s2.inner, i);
1825}
1826
1827// Expensive lemma; not in the default broadcast group
1828pub broadcast proof fn lemma_seq_add_index1_alt<A>(s1: Seq<A>, s2: Seq<A>, i: int)
1829    requires
1830        0 <= i < s1.len(),
1831    ensures
1832        (#[trigger] s1.add(s2))[i] == #[trigger] s1[i],
1833{
1834    broadcast use lemma_seq_add_index1;
1835
1836}
1837
1838// Expensive lemma; not in the default broadcast group
1839pub broadcast proof fn lemma_seq_add_index2_alt<A>(s1: Seq<A>, s2: Seq<A>, i: int)
1840    requires
1841        0 <= i < s2.len(),
1842    ensures
1843        (#[trigger] s1.add(s2))[i + s1.len()] == #[trigger] s2[i],
1844{
1845    broadcast use lemma_seq_add_index2;
1846
1847}
1848
1849#[deprecated(note = "Use `group_seq_lemmas` instead")]
1850pub broadcast group group_seq_axioms {
1851    lemma_seq_index_decreases,
1852    lemma_seq_subrange_decreases,
1853    lemma_seq_empty,
1854    lemma_seq_new_len,
1855    lemma_seq_new_index,
1856    lemma_seq_push_len,
1857    lemma_seq_push_index_same,
1858    lemma_seq_push_index_different,
1859    lemma_seq_update_len,
1860    lemma_seq_update_same,
1861    lemma_seq_update_different,
1862    lemma_seq_ext_equal,
1863    lemma_seq_ext_equal_deep,
1864    lemma_seq_subrange_len,
1865    lemma_seq_subrange_index,
1866    lemma_seq_two_subranges_index,
1867    lemma_seq_add_len,
1868    lemma_seq_add_index1,
1869    lemma_seq_add_index2,
1870}
1871
1872pub broadcast group group_seq_lemmas {
1873    lemma_seq_index_decreases,
1874    lemma_seq_subrange_decreases,
1875    lemma_seq_empty,
1876    lemma_seq_new_len,
1877    lemma_seq_new_index,
1878    lemma_seq_push_len,
1879    lemma_seq_push_index_same,
1880    lemma_seq_push_index_different,
1881    lemma_seq_update_len,
1882    lemma_seq_update_same,
1883    lemma_seq_update_different,
1884    lemma_seq_ext_equal,
1885    lemma_seq_ext_equal_deep,
1886    lemma_seq_subrange_len,
1887    lemma_seq_subrange_index,
1888    lemma_seq_two_subranges_index,
1889    lemma_seq_add_len,
1890    lemma_seq_add_index1,
1891    lemma_seq_add_index2,
1892}
1893
1894// Expensive lemmas not in the default group (may slow down verification)
1895pub broadcast group group_seq_lemmas_expensive {
1896    lemma_seq_push_index_different_alt,
1897    lemma_seq_update_same_alt,
1898    lemma_seq_update_different_alt,
1899    lemma_seq_subrange_index_alt,
1900    lemma_seq_add_index1_alt,
1901    lemma_seq_add_index2_alt,
1902}
1903
1904// ------------- Macros ---------------- //
1905#[doc(hidden)]
1906#[macro_export]
1907macro_rules! seq_internal {
1908    [] => {
1909        $crate::vstd::seq::Seq::empty()
1910    };
1911    [$elem:expr] => {
1912        $crate::vstd::seq::Seq::empty()
1913            .push($elem)
1914    };
1915    [$elem:expr,] => {
1916        $crate::vstd::seq::Seq::empty()
1917            .push($elem)
1918    };
1919    [$($elem:expr),* $(,)?] => {
1920        <_ as $crate::vstd::view::View>::view(&[$($elem),*])
1921    };
1922    [$elem:expr; $n:expr] => {
1923        $crate::vstd::seq::Seq::new(
1924            $n,
1925            $crate::vstd::prelude::closure_to_fn_spec(
1926                |_x: _| $elem
1927            ),
1928        )
1929    };
1930}
1931
1932/// Creates a [`Seq`] containing the given elements.
1933///
1934/// ## Example
1935///
1936/// ```rust
1937/// let s = seq![11int, 12, 13];
1938///
1939/// assert(s.len() == 3);
1940/// assert(s[0] == 11);
1941/// assert(s[1] == 12);
1942/// assert(s[2] == 13);
1943/// ```
1944#[macro_export]
1945macro_rules! seq {
1946    [$($tail:tt)*] => {
1947        $crate::vstd::prelude::verus_proof_macro_exprs!($crate::vstd::seq::seq_internal!($($tail)*))
1948    };
1949}
1950
1951#[doc(hidden)]
1952pub use seq_internal;
1953pub use seq;
1954
1955} // verus!
vstd/seq.rs

vstd/
seq.rs
