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

vstd/
seq.rs
