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

vstd/
seq.rs
