creusot_std/logic/seq.rs
1#[cfg(creusot)]
2use crate::resolve::structural_resolve;
3use crate::{
4 ghost::Plain,
5 logic::{Mapping, ops::IndexLogic},
6 prelude::*,
7 std::ops::RangeInclusiveExt as _,
8};
9use core::{
10 marker::PhantomData,
11 ops::{Range, RangeFrom, RangeFull, RangeInclusive, RangeTo, RangeToInclusive},
12};
13
14/// A type of sequence usable in pearlite and `ghost!` blocks.
15///
16/// # Logic
17///
18/// This type is (in particular) the logical representation of a [`Vec`]. This can be
19/// accessed via its [view][crate::model::View] (The `@` operator).
20///
21/// ```rust,creusot
22/// # use creusot_std::prelude::*;
23/// #[logic]
24/// fn get_model<T>(v: Vec<T>) -> Seq<T> {
25/// pearlite!(v@)
26/// }
27/// ```
28///
29/// # Ghost
30///
31/// Since [`Vec`] have finite capacity, this could cause some issues in ghost code:
32/// ```rust,creusot,compile_fail
33/// ghost! {
34/// let mut v = Vec::new();
35/// for _ in 0..=usize::MAX as u128 + 1 {
36/// v.push(0); // cannot fail, since we are in a ghost block
37/// }
38/// proof_assert!(v@.len() <= usize::MAX@); // by definition
39/// proof_assert!(v@.len() > usize::MAX@); // uh-oh
40/// }
41/// ```
42///
43/// This type is designed for this use-case, with no restriction on the capacity.
44#[builtin("seq.Seq.seq")]
45pub struct Seq<T>(PhantomData<T>);
46
47/// Logical definitions
48impl<T> Seq<T> {
49 /// Returns the empty sequence.
50 #[logic]
51 #[builtin("seq.Seq.empty", ascription)]
52 pub fn empty() -> Self {
53 dead
54 }
55
56 /// Create a new sequence in pearlite.
57 ///
58 /// The new sequence will be of length `n`, and will contain `mapping[i]` at index `i`.
59 ///
60 /// # Example
61 ///
62 /// ```
63 /// # use creusot_std::prelude::*;
64 /// let s = snapshot!(Seq::create(5, |i| i + 1));
65 /// proof_assert!(s.len() == 5);
66 /// proof_assert!(forall<i> 0 <= i && i < 5 ==> s[i] == i + 1);
67 /// ```
68 #[logic]
69 #[builtin("seq.Seq.create")]
70 pub fn create(n: Int, mapping: Mapping<Int, T>) -> Self {
71 let _ = n;
72 let _ = mapping;
73 dead
74 }
75
76 /// Returns the value at index `ix`.
77 ///
78 /// If `ix` is out of bounds, return `None`.
79 #[logic(open)]
80 pub fn get(self, ix: Int) -> Option<T> {
81 if 0 <= ix && ix < self.len() { Some(self.index_logic(ix)) } else { None }
82 }
83
84 /// Returns the value at index `ix`.
85 ///
86 /// If `ix` is out of bounds, the returned value is meaningless.
87 ///
88 /// You should prefer using the indexing operator `s[ix]`.
89 ///
90 /// # Example
91 ///
92 /// ```
93 /// # use creusot_std::prelude::*;
94 /// let s = snapshot!(Seq::singleton(2));
95 /// proof_assert!(s.index_logic_unsized(0) == 2);
96 /// proof_assert!(s[0] == 2); // prefer this
97 /// ```
98 #[logic]
99 #[builtin("seq.Seq.get")]
100 pub fn index_logic_unsized<'a>(self, ix: Int) -> &'a T {
101 let _ = ix;
102 dead
103 }
104
105 /// Returns the subsequence between indices `start` and `end`.
106 ///
107 /// If either `start` or `end` are out of bounds, the result is meaningless.
108 ///
109 /// # Example
110 ///
111 /// ```
112 /// # use creusot_std::prelude::*;
113 /// let subs = snapshot! {
114 /// let s: Seq<Int> = Seq::create(10, |i| i);
115 /// s.subsequence(2, 5)
116 /// };
117 /// proof_assert!(subs.len() == 3);
118 /// proof_assert!(subs[0] == 2 && subs[1] == 3 && subs[2] == 4);
119 /// ```
120 #[logic]
121 #[builtin("seq.Seq.([..])")]
122 pub fn subsequence(self, start: Int, end: Int) -> Self {
123 let _ = start;
124 let _ = end;
125 dead
126 }
127
128 /// Create a sequence containing one element.
129 ///
130 /// # Example
131 ///
132 /// ```
133 /// # use creusot_std::prelude::*;
134 /// let s = snapshot!(Seq::singleton(42));
135 /// proof_assert!(s.len() == 1);
136 /// proof_assert!(s[0] == 42);
137 /// ```
138 #[logic]
139 #[builtin("seq.Seq.singleton")]
140 pub fn singleton(value: T) -> Self {
141 let _ = value;
142 dead
143 }
144
145 /// Returns the sequence without its first element.
146 ///
147 /// If the sequence is empty, the result is meaningless.
148 ///
149 /// # Example
150 ///
151 /// ```
152 /// # use creusot_std::prelude::*;
153 /// let s = snapshot!(seq![5, 10, 15]);
154 /// proof_assert!(s.tail() == seq![10, 15]);
155 /// proof_assert!(s.tail().tail() == Seq::singleton(15));
156 /// proof_assert!(s.tail().tail().tail() == Seq::empty());
157 /// ```
158 #[logic(open)]
159 pub fn tail(self) -> Self {
160 self.subsequence(1, self.len())
161 }
162
163 /// Alias for [`Self::tail`].
164 #[logic(open)]
165 pub fn pop_front(self) -> Self {
166 self.tail()
167 }
168
169 /// Returns the sequence without its last element.
170 ///
171 /// If the sequence is empty, the result is meaningless.
172 ///
173 /// # Example
174 ///
175 /// ```
176 /// # use creusot_std::prelude::*;
177 /// let s = snapshot!(seq![5, 10, 15]);
178 /// proof_assert!(s.pop_back() == seq![5, 10]);
179 /// proof_assert!(s.pop_back().pop_back() == Seq::singleton(5));
180 /// proof_assert!(s.pop_back().pop_back().pop_back() == Seq::empty());
181 /// ```
182 #[logic(open)]
183 pub fn pop_back(self) -> Self {
184 self.subsequence(0, self.len() - 1)
185 }
186
187 /// Returns the number of elements in the sequence, also referred to as its 'length'.
188 ///
189 /// # Example
190 ///
191 /// ```
192 /// # use creusot_std::prelude::*;
193 /// #[requires(v@.len() > 0)]
194 /// fn f<T>(v: Vec<T>) { /* ... */ }
195 /// ```
196 #[logic]
197 #[builtin("seq.Seq.length")]
198 pub fn len(self) -> Int {
199 dead
200 }
201
202 /// Returns a new sequence, where the element at index `ix` has been replaced by `x`.
203 ///
204 /// If `ix` is out of bounds, the result is meaningless.
205 ///
206 /// # Example
207 ///
208 /// ```
209 /// # use creusot_std::prelude::*;
210 /// let s = snapshot!(Seq::create(2, |_| 0));
211 /// let s2 = snapshot!(s.set(1, 3));
212 /// proof_assert!(s2[0] == 0);
213 /// proof_assert!(s2[1] == 3);
214 /// ```
215 #[logic]
216 #[builtin("seq.Seq.set")]
217 pub fn set(self, ix: Int, x: T) -> Self {
218 let _ = ix;
219 let _ = x;
220 dead
221 }
222
223 /// Extensional equality
224 ///
225 /// Returns `true` if `self` and `other` have the same length, and contain the same
226 /// elements at the same indices.
227 ///
228 /// This is in fact equivalent with normal equality.
229 #[logic]
230 #[builtin("seq.Seq.(==)")]
231 pub fn ext_eq(self, other: Self) -> bool {
232 let _ = other;
233 dead
234 }
235
236 // internal wrapper to match the order of arguments of Seq.cons
237 #[doc(hidden)]
238 #[logic]
239 #[builtin("seq.Seq.cons")]
240 pub fn cons(_: T, _: Self) -> Self {
241 dead
242 }
243
244 /// Returns a new sequence, where `x` has been prepended to `self`.
245 ///
246 /// # Example
247 ///
248 /// ```
249 /// let s = snapshot!(Seq::singleton(1));
250 /// let s2 = snapshot!(s.push_front(2));
251 /// proof_assert!(s2[0] == 2);
252 /// proof_assert!(s2[1] == 1);
253 /// ```
254 #[logic(open, inline)]
255 pub fn push_front(self, x: T) -> Self {
256 Self::cons(x, self)
257 }
258
259 /// Returns a new sequence, where `x` has been appended to `self`.
260 ///
261 /// # Example
262 ///
263 /// ```
264 /// let s = snapshot!(Seq::singleton(1));
265 /// let s2 = snapshot!(s.push_back(2));
266 /// proof_assert!(s2[0] == 1);
267 /// proof_assert!(s2[1] == 2);
268 /// ```
269 #[logic]
270 #[builtin("seq.Seq.snoc")]
271 pub fn push_back(self, x: T) -> Self {
272 let _ = x;
273 dead
274 }
275
276 /// Returns a new sequence, made of the concatenation of `self` and `other`.
277 ///
278 /// See also the program function [`Seq::extend`].
279 ///
280 /// # Example
281 ///
282 /// ```
283 /// # use creusot_std::prelude::*;
284 /// let s1 = snapshot!(Seq::singleton(1));
285 /// let s2 = snapshot!(Seq::create(2, |i| i));
286 /// let s = snapshot!(s1.concat(s2));
287 /// proof_assert!(s[0] == 1);
288 /// proof_assert!(s[1] == 0);
289 /// proof_assert!(s[2] == 1);
290 /// ```
291 #[logic]
292 #[builtin("seq.Seq.(++)")]
293 pub fn concat(self, other: Self) -> Self {
294 let _ = other;
295 dead
296 }
297
298 #[logic]
299 #[ensures(result.len() == self.len())]
300 #[ensures(forall<i> 0 <= i && i < self.len() ==> result[i] == m[self[i]])]
301 #[variant(self.len())]
302 pub fn map<U>(self, m: Mapping<T, U>) -> Seq<U> {
303 if self.len() == 0 {
304 Seq::empty()
305 } else {
306 self.tail().map(m).push_front(m.get(*self.index_logic_unsized(0)))
307 }
308 }
309
310 #[logic(open)]
311 #[variant(self.len())]
312 pub fn flat_map<U>(self, other: Mapping<T, Seq<U>>) -> Seq<U> {
313 if self.len() == 0 {
314 Seq::empty()
315 } else {
316 other.get(*self.index_logic_unsized(0)).concat(self.tail().flat_map(other))
317 }
318 }
319
320 /// Returns a new sequence, which is `self` in reverse order.
321 ///
322 /// # Example
323 ///
324 /// ```
325 /// # use creusot_std::prelude::*;
326 /// let s = snapshot!(Seq::create(3, |i| i));
327 /// let s2 = snapshot!(s.reverse());
328 /// proof_assert!(s2[0] == 2);
329 /// proof_assert!(s2[1] == 1);
330 /// proof_assert!(s2[2] == 0);
331 /// ```
332 #[logic]
333 #[builtin("seq.Reverse.reverse")]
334 pub fn reverse(self) -> Self {
335 dead
336 }
337
338 #[logic]
339 #[ensures(Self::empty().reverse() == Self::empty())]
340 pub fn reverse_empty() {}
341
342 /// Returns a new sequence, which is `self` with the element at the given `index` removed.
343 ///
344 /// See also the program function [`Seq::remove`].
345 ///
346 /// # Example
347 ///
348 /// ```rust,creusot
349 /// # use creusot_std::prelude::*;
350 /// let s = snapshot!(seq![7, 8, 9]);
351 /// proof_assert!(removed(*s, 1) == seq![7, 9]);
352 /// ```
353 #[logic(open)]
354 pub fn removed(self, index: Int) -> Self {
355 pearlite! { self[..index].concat(self[index+1..]) }
356 }
357
358 /// Returns `true` if `other` is a permutation of `self`.
359 #[logic(open)]
360 pub fn permutation_of(self, other: Self) -> bool {
361 self.permut(other, 0, self.len())
362 }
363
364 /// Returns `true` if:
365 /// - `self` and `other` have the same length
366 /// - `start` and `end` are in bounds (between `0` and `self.len()` included)
367 /// - Every element occurs as many times in `self[start..end]` as in `other[start..end]`.
368 #[logic]
369 #[builtin("seq.Permut.permut")]
370 pub fn permut(self, other: Self, start: Int, end: Int) -> bool {
371 let _ = other;
372 let _ = start;
373 let _ = end;
374 dead
375 }
376
377 /// Returns `true` if:
378 /// - `self` and `other` have the same length
379 /// - `i` and `j` are in bounds (between `0` and `self.len()` excluded)
380 /// - `other` is equal to `self` where the elements at `i` and `j` are swapped
381 #[logic]
382 #[builtin("seq.Permut.exchange")]
383 pub fn exchange(self, other: Self, i: Int, j: Int) -> bool {
384 let _ = other;
385 let _ = i;
386 let _ = j;
387 dead
388 }
389
390 /// Returns `true` if there is an index `i` such that `self[i] == x`.
391 #[logic(open)]
392 pub fn contains(self, x: T) -> bool {
393 pearlite! { exists<i> 0 <= i && i < self.len() && self[i] == x }
394 }
395
396 /// Returns `true` if `self` is sorted between `start` and `end`.
397 #[logic(open)]
398 pub fn sorted_range(self, start: Int, end: Int) -> bool
399 where
400 T: OrdLogic,
401 {
402 pearlite! {
403 forall<i, j> start <= i && i <= j && j < end ==> self[i] <= self[j]
404 }
405 }
406
407 /// Returns `true` if `self` is sorted.
408 #[logic(open)]
409 pub fn sorted(self) -> bool
410 where
411 T: OrdLogic,
412 {
413 self.sorted_range(0, self.len())
414 }
415
416 #[logic(open)]
417 #[ensures(forall<a: Seq<T>, b: Seq<T>, x>
418 a.concat(b).contains(x) == a.contains(x) || b.contains(x))]
419 pub fn concat_contains() {}
420
421 #[logic]
422 #[ensures(self.concat(other1).concat(other2) == self.concat(other1.concat(other2)))]
423 pub fn concat_assoc(self, other1: Self, other2: Self) {}
424
425 #[logic]
426 #[ensures(self.concat(Seq::empty()) == self)]
427 #[ensures(Seq::empty().concat(self) == self)]
428 pub fn concat_empty(self) {}
429
430 #[logic]
431 #[ensures(self.concat(other).reverse() == other.reverse().concat(self.reverse()))]
432 pub fn reverse_concat(self, other: Self) {}
433}
434
435impl<T> Seq<Seq<T>> {
436 #[logic(open)]
437 #[variant(self.len())]
438 pub fn flatten(self) -> Seq<T> {
439 if self.len() == 0 {
440 Seq::empty()
441 } else {
442 self.index_logic_unsized(0).concat(self.tail().flatten())
443 }
444 }
445}
446
447impl<T> Seq<&T> {
448 /// Convert `Seq<&T>` to `Seq<T>`.
449 ///
450 /// This is simply a utility method, because `&T` is equivalent to `T` in pearlite.
451 #[logic]
452 #[builtin("identity")]
453 pub fn to_owned_seq(self) -> Seq<T> {
454 dead
455 }
456}
457
458impl<T> IndexLogic<Int> for Seq<T> {
459 type Item = T;
460
461 #[logic]
462 #[builtin("seq.Seq.get")]
463 fn index_logic(self, _: Int) -> Self::Item {
464 dead
465 }
466}
467
468impl<T> IndexLogic<Range<Int>> for Seq<T> {
469 type Item = Seq<T>;
470
471 #[logic(open, inline)]
472 fn index_logic(self, range: Range<Int>) -> Self::Item {
473 self.subsequence(range.start, range.end)
474 }
475}
476
477impl<T> IndexLogic<RangeInclusive<Int>> for Seq<T> {
478 type Item = Seq<T>;
479
480 #[logic(open, inline)]
481 fn index_logic(self, range: RangeInclusive<Int>) -> Self::Item {
482 self.subsequence(range.start_log(), range.end_log() + 1)
483 }
484}
485
486impl<T> IndexLogic<RangeFull> for Seq<T> {
487 type Item = Seq<T>;
488
489 #[logic(open, inline)]
490 fn index_logic(self, _: RangeFull) -> Self::Item {
491 self
492 }
493}
494
495impl<T> IndexLogic<RangeFrom<Int>> for Seq<T> {
496 type Item = Seq<T>;
497
498 #[logic(open, inline)]
499 fn index_logic(self, range: RangeFrom<Int>) -> Self::Item {
500 self.subsequence(range.start, self.len())
501 }
502}
503
504impl<T> IndexLogic<RangeTo<Int>> for Seq<T> {
505 type Item = Seq<T>;
506
507 #[logic(open, inline)]
508 fn index_logic(self, range: RangeTo<Int>) -> Self::Item {
509 self.subsequence(0, range.end)
510 }
511}
512
513impl<T> IndexLogic<RangeToInclusive<Int>> for Seq<T> {
514 type Item = Seq<T>;
515
516 #[logic(open, inline)]
517 fn index_logic(self, range: RangeToInclusive<Int>) -> Self::Item {
518 self.subsequence(0, range.end + 1)
519 }
520}
521
522/// Ghost definitions
523impl<T> Seq<T> {
524 /// Constructs a new, empty `Seq<T>`.
525 ///
526 /// This can only be manipulated in the ghost world, and as such is wrapped in [`Ghost`].
527 ///
528 /// # Example
529 ///
530 /// ```rust,creusot
531 /// use creusot_std::prelude::*;
532 /// let ghost_seq = Seq::<i32>::new();
533 /// proof_assert!(seq == Seq::create());
534 /// ```
535 #[trusted]
536 #[check(ghost)]
537 #[ensures(*result == Self::empty())]
538 #[allow(unreachable_code)]
539 pub fn new() -> Ghost<Self> {
540 Ghost::conjure()
541 }
542
543 /// Returns the number of elements in the sequence, also referred to as its 'length'.
544 ///
545 /// If you need to get the length in pearlite, consider using [`len`](Self::len).
546 ///
547 /// # Example
548 /// ```rust,creusot
549 /// use creusot_std::prelude::*;
550 ///
551 /// let mut s = Seq::new();
552 /// ghost! {
553 /// s.push_back_ghost(1);
554 /// s.push_back_ghost(2);
555 /// s.push_back_ghost(3);
556 /// let len = s.len_ghost();
557 /// proof_assert!(len == 3);
558 /// };
559 /// ```
560 #[trusted]
561 #[check(ghost)]
562 #[ensures(result == self.len())]
563 pub fn len_ghost(&self) -> Int {
564 panic!()
565 }
566
567 /// Returns `true` if the sequence is empty.
568 ///
569 /// # Example
570 ///
571 /// ```rust,creusot
572 /// use creusot_std::prelude::*;
573 /// #[check(ghost)]
574 /// #[requires(s.len() == 0)]
575 /// pub fn foo(mut s: Seq<i32>) {
576 /// assert!(s.is_empty_ghost());
577 /// s.push_back_ghost(1i32);
578 /// assert!(!s.is_empty_ghost());
579 /// }
580 /// ghost! {
581 /// foo(Seq::new().into_inner())
582 /// };
583 /// ```
584 #[trusted]
585 #[check(ghost)]
586 #[ensures(result == (self.len() == 0))]
587 pub fn is_empty_ghost(&self) -> bool {
588 panic!()
589 }
590
591 /// Appends an element to the front of a collection.
592 ///
593 /// # Example
594 /// ```rust,creusot
595 /// use creusot_std::prelude::*;
596 ///
597 /// let mut s = Seq::new();
598 /// ghost! {
599 /// s.push_front_ghost(1);
600 /// s.push_front_ghost(2);
601 /// s.push_front_ghost(3);
602 /// proof_assert!(s[0] == 3i32 && s[1] == 2i32 && s[2] == 1i32);
603 /// };
604 /// ```
605 #[trusted]
606 #[check(ghost)]
607 #[ensures(^self == self.push_front(x))]
608 pub fn push_front_ghost(&mut self, x: T) {
609 let _ = x;
610 panic!()
611 }
612
613 /// Appends an element to the back of a collection.
614 ///
615 /// # Example
616 /// ```rust,creusot
617 /// use creusot_std::prelude::*;
618 ///
619 /// let mut s = Seq::new();
620 /// ghost! {
621 /// s.push_back_ghost(1);
622 /// s.push_back_ghost(2);
623 /// s.push_back_ghost(3);
624 /// proof_assert!(s[0] == 1i32 && s[1] == 2i32 && s[2] == 3i32);
625 /// };
626 /// ```
627 #[trusted]
628 #[check(ghost)]
629 #[ensures(^self == self.push_back(x))]
630 pub fn push_back_ghost(&mut self, x: T) {
631 let _ = x;
632 panic!()
633 }
634
635 /// Returns a reference to an element at `index` or `None` if `index` is out of bounds.
636 ///
637 /// # Example
638 /// ```rust,creusot
639 /// use creusot_std::prelude::*;
640 ///
641 /// let mut s = Seq::new();
642 /// ghost! {
643 /// s.push_back_ghost(10);
644 /// s.push_back_ghost(40);
645 /// s.push_back_ghost(30);
646 /// let get1 = s.get_ghost(1int);
647 /// let get2 = s.get_ghost(3int);
648 /// proof_assert!(get1 == Some(&40i32));
649 /// proof_assert!(get2 == None);
650 /// };
651 /// ```
652 #[check(ghost)]
653 #[ensures(match self.get(index) {
654 None => result == None,
655 Some(v) => result == Some(&v),
656 })]
657 pub fn get_ghost(&self, index: Int) -> Option<&T> {
658 // FIXME: we can't write 0 outside of a `ghost!` block
659 if index - index <= index && index < self.len_ghost() {
660 Some(self.as_refs().extract(index))
661 } else {
662 None
663 }
664 }
665
666 /// Returns a mutable reference to an element at `index` or `None` if `index` is out of bounds.
667 ///
668 /// # Example
669 /// ```rust,creusot
670 /// use creusot_std::prelude::*;
671 ///
672 /// let mut s = Seq::new();
673 ///
674 /// ghost! {
675 /// s.push_back_ghost(0);
676 /// s.push_back_ghost(1);
677 /// s.push_back_ghost(2);
678 /// if let Some(elem) = s.get_mut_ghost(1int) {
679 /// *elem = 42;
680 /// }
681 /// proof_assert!(s[0] == 0i32 && s[1] == 42i32 && s[2] == 2i32);
682 /// };
683 /// ```
684 #[check(ghost)]
685 #[ensures(match result {
686 None => self.get(index) == None && *self == ^self,
687 Some(r) => self.get(index) == Some(*r) && ^r == (^self)[index],
688 })]
689 #[ensures(forall<i> i != index ==> (*self).get(i) == (^self).get(i))]
690 #[ensures((*self).len() == (^self).len())]
691 pub fn get_mut_ghost(&mut self, index: Int) -> Option<&mut T> {
692 // FIXME: we can't write 0 outside of a `ghost!` block
693 if index - index <= index && index < self.len_ghost() {
694 Some(self.as_muts().extract(index))
695 } else {
696 None
697 }
698 }
699
700 /// Remove an element and discard the rest of the sequence.
701 ///
702 /// This is sometimes preferable to `remove` because this avoids reasoning about subsequences.
703 #[check(ghost)]
704 #[requires(0 <= index && index < self.len())]
705 #[ensures(result == self[index])]
706 #[ensures(forall<i> 0 <= i && i < self.len() && i != index ==> resolve(self[i]))]
707 pub fn extract(mut self, index: Int) -> T {
708 proof_assert! { forall<i> index < i && i < self.len() ==> self[i] == self[index + 1..][i - index - 1] }
709 self.split_off_ghost(index).pop_front_ghost().unwrap()
710 }
711
712 /// Remove an element from a sequence.
713 ///
714 /// See also the logic function [`Seq::removed`].
715 #[check(ghost)]
716 #[requires(0 <= index && index < self.len())]
717 #[ensures(result == self[index])]
718 #[ensures(^self == (*self).removed(index))]
719 pub fn remove(&mut self, index: Int) -> T {
720 let mut right = self.split_off_ghost(index);
721 let result = right.pop_front_ghost().unwrap();
722 self.extend(right);
723 result
724 }
725
726 /// Append a sequence to another.
727 ///
728 /// See also the logic function [`Seq::concat`].
729 ///
730 /// ## Remark
731 ///
732 /// The second argument is currently restricted to sequences.
733 /// Generalizing it to arbitrary `IntoIterator` requires some missing features
734 /// to specify that the iterator terminates and that its methods are
735 /// callable in ghost code.
736 #[check(ghost)]
737 #[ensures(^self == (*self).concat(rhs))]
738 pub fn extend(&mut self, mut rhs: Self) {
739 let _final = snapshot! { self.concat(rhs) };
740 #[variant(rhs.len())]
741 #[invariant(self.concat(rhs) == *_final)]
742 while let Some(x) = rhs.pop_front_ghost() {
743 self.push_back_ghost(x)
744 }
745 }
746
747 /// Removes the last element from a vector and returns it, or `None` if it is empty.
748 ///
749 /// # Example
750 /// ```rust,creusot
751 /// use creusot_std::prelude::*;
752 ///
753 /// let mut s = Seq::new();
754 /// ghost! {
755 /// s.push_back_ghost(1);
756 /// s.push_back_ghost(2);
757 /// s.push_back_ghost(3);
758 /// let popped = s.pop_back_ghost();
759 /// proof_assert!(popped == Some(3i32));
760 /// proof_assert!(s[0] == 1i32 && s[1] == 2i32);
761 /// };
762 /// ```
763 #[trusted]
764 #[check(ghost)]
765 #[ensures(match result {
766 None => *self == Seq::empty() && *self == ^self,
767 Some(r) => *self == (^self).push_back(r)
768 })]
769 pub fn pop_back_ghost(&mut self) -> Option<T> {
770 panic!()
771 }
772
773 /// Removes the first element from a vector and returns it, or `None` if it is empty.
774 ///
775 /// # Example
776 /// ```rust,creusot
777 /// use creusot_std::prelude::*;
778 ///
779 /// let mut s = Seq::new();
780 /// ghost! {
781 /// s.push_back_ghost(1);
782 /// s.push_back_ghost(2);
783 /// s.push_back_ghost(3);
784 /// let popped = s.pop_front_ghost();
785 /// proof_assert!(popped == Some(1i32));
786 /// proof_assert!(s[0] == 2i32 && s[1] == 3i32);
787 /// };
788 /// ```
789 #[trusted]
790 #[check(ghost)]
791 #[ensures(match result {
792 None => *self == Seq::empty() && *self == ^self,
793 Some(r) => (*self).len() > 0 && r == (*self)[0] && ^self == (*self).tail()
794 })]
795 pub fn pop_front_ghost(&mut self) -> Option<T> {
796 panic!()
797 }
798
799 /// Clears the sequence, removing all values.
800 ///
801 /// # Example
802 /// ```rust,creusot
803 /// use creusot_std::prelude::*;
804 ///
805 /// let mut s = Seq::new();
806 /// ghost! {
807 /// s.push_back_ghost(1);
808 /// s.push_back_ghost(2);
809 /// s.push_back_ghost(3);
810 /// s.clear_ghost();
811 /// proof_assert!(s == Seq::empty());
812 /// };
813 /// ```
814 #[trusted]
815 #[check(ghost)]
816 #[ensures(^self == Self::empty())]
817 pub fn clear_ghost(&mut self) {}
818
819 /// Split a sequence in two at the given index.
820 #[trusted]
821 #[check(ghost)]
822 #[requires(0 <= mid && mid <= self.len())]
823 #[ensures(^self == self[..mid])]
824 #[ensures(result == self[mid..])]
825 pub fn split_off_ghost(&mut self, mid: Int) -> Self {
826 let _ = mid;
827 panic!("ghost code")
828 }
829
830 /// Borrow every element of a borrowed sequence.
831 #[trusted]
832 #[check(ghost)]
833 #[ensures(*self == result.to_owned_seq())]
834 pub fn as_refs(&self) -> Seq<&T> {
835 panic!("ghost code")
836 }
837
838 /// Mutably borrow every element of a borrowed sequence.
839 #[trusted]
840 #[check(ghost)]
841 #[ensures(result.len() == self.len())]
842 #[ensures((^self).len() == self.len())]
843 #[ensures(forall<i> 0 <= i && i < self.len() ==> *result[i] == (*self)[i])]
844 #[ensures(forall<i> 0 <= i && i < self.len() ==> ^result[i] == (^self)[i])]
845 pub fn as_muts(&mut self) -> Seq<&mut T> {
846 panic!("ghost code")
847 }
848}
849
850impl<T> core::ops::Index<Int> for Seq<T> {
851 type Output = T;
852
853 #[check(ghost)]
854 #[requires(0 <= index && index < self.len())]
855 #[ensures(*result == self[index])]
856 fn index(&self, index: Int) -> &Self::Output {
857 self.get_ghost(index).unwrap()
858 }
859}
860impl<T> core::ops::IndexMut<Int> for Seq<T> {
861 #[check(ghost)]
862 #[requires(0 <= index && index < self.len())]
863 #[ensures((*self).len() == (^self).len())]
864 #[ensures(*result == (*self)[index] && ^result == (^self)[index])]
865 #[ensures(forall<i> i != index ==> (*self).get(i) == (^self).get(i))]
866 fn index_mut(&mut self, index: Int) -> &mut Self::Output {
867 self.get_mut_ghost(index).unwrap()
868 }
869}
870
871impl<T> core::ops::Index<(Int, Int)> for Seq<T> {
872 type Output = (T, T);
873
874 #[trusted]
875 #[check(ghost)]
876 #[requires(0 <= index.0 && index.0 < self.len() && 0 <= index.1 && index.1 < self.len())]
877 #[ensures(result.0 == self[index.0] && result.1 == self[index.1])]
878 #[allow(unused_variables)]
879 fn index(&self, index: (Int, Int)) -> &Self::Output {
880 panic!()
881 }
882}
883
884impl<T> core::ops::IndexMut<(Int, Int)> for Seq<T> {
885 #[trusted]
886 #[check(ghost)]
887 #[requires(0 <= index.0 && index.0 < self.len() && 0 <= index.1 && index.1 < self.len())]
888 #[requires(index.0 != index.1)]
889 #[ensures((*result).0 == (*self)[index.0] && (*result).1 == (*self)[index.1]
890 && (^result).0 == (^self)[index.0] && (^result).1 == (^self)[index.1])]
891 #[ensures(forall<i> i != index.0 && i != index.1 ==> (*self).get(i) == (^self).get(i))]
892 #[ensures((*self).len() == (^self).len())]
893 #[allow(unused_variables)]
894 fn index_mut(&mut self, index: (Int, Int)) -> &mut Self::Output {
895 panic!()
896 }
897}
898
899// Having `Copy` guarantees that the operation is pure, even if we decide to change the definition of `Clone`.
900impl<T: Clone + Copy> Clone for Seq<T> {
901 #[trusted]
902 #[check(ghost)]
903 #[ensures(result == *self)]
904 fn clone(&self) -> Self {
905 *self
906 }
907}
908
909impl<T: Copy> Copy for Seq<T> {}
910impl<T: Plain> Plain for Seq<T> {
911 #[ensures(*result == *snap)]
912 #[check(ghost)]
913 #[allow(unused_variables)]
914 fn into_ghost(snap: Snapshot<Self>) -> Ghost<Self> {
915 ghost! {
916 let mut res = Seq::new().into_inner();
917 let len: Snapshot<Int> = snapshot!(snap.len());
918 let len = len.into_ghost().into_inner();
919 let mut i = 0int;
920 #[variant(len - i)]
921 #[invariant(i <= len)]
922 #[invariant(res.len() == i)]
923 #[invariant(forall<j> 0 <= j && j < i ==> res[j] == snap[j])]
924 while i < len {
925 let elem: Snapshot<T> = snapshot!(snap[i]);
926 res.push_back_ghost(elem.into_ghost().into_inner());
927 i = i + 1int;
928 }
929 res
930 }
931 }
932}
933
934impl<T> Invariant for Seq<T> {
935 #[logic(open, prophetic, inline)]
936 #[creusot::trusted_trivial_if_param_trivial]
937 fn invariant(self) -> bool {
938 pearlite! { forall<i> 0 <= i && i < self.len() ==> inv(self.index_logic_unsized(i)) }
939 }
940}
941
942// =========
943// Iterators
944// =========
945
946/// Iterator for sequences.
947///
948/// This provides all three variants of `IntoIter` for `Seq`:
949/// `Iter<T>`, `Iter<&T>`, `Iter<&mut T>`.
950///
951/// This is a different type from `Seq` to enable `IntoIterator for &mut Seq<T>`
952/// (if `Seq` were an iterator, that would conflict with `IntoIterator for I where I: Iterator`).
953///
954/// # Ghost code and variants
955///
956/// This iterator is only obtainable in ghost code.
957///
958/// To use it in a `for` loop, a variant must be declared:
959/// ```rust,creusot
960/// # use creusot_std::prelude::*;
961/// # #[requires(true)]
962/// fn iter_on_seq<T>(s: Seq<T>) {
963/// let len = snapshot!(s.len());
964/// #[variant(len - produced.len())]
965/// for i in s {
966/// // ...
967/// }
968/// }
969/// ```
970pub struct Iter<T>(Seq<T>);
971
972impl<T> View for Iter<T> {
973 type ViewTy = Seq<T>;
974 #[logic]
975 fn view(self) -> Self::ViewTy {
976 self.0
977 }
978}
979
980impl<T> Iterator for Iter<T> {
981 type Item = T;
982
983 #[check(ghost)]
984 #[ensures(match result {
985 None => self.completed(),
986 Some(v) => (*self).produces(Seq::singleton(v), ^self)
987 })]
988 fn next(&mut self) -> Option<T> {
989 self.0.pop_front_ghost()
990 }
991}
992
993impl<T> IteratorSpec for Iter<T> {
994 #[logic(prophetic, open)]
995 fn produces(self, visited: Seq<T>, o: Self) -> bool {
996 pearlite! { self@ == visited.concat(o@) }
997 }
998
999 #[logic(prophetic, open)]
1000 fn completed(&mut self) -> bool {
1001 pearlite! { self@ == Seq::empty() }
1002 }
1003
1004 #[logic(law)]
1005 #[ensures(self.produces(Seq::empty(), self))]
1006 fn produces_refl(self) {}
1007
1008 #[logic(law)]
1009 #[requires(a.produces(ab, b))]
1010 #[requires(b.produces(bc, c))]
1011 #[ensures(a.produces(ab.concat(bc), c))]
1012 fn produces_trans(a: Self, ab: Seq<Self::Item>, b: Self, bc: Seq<Self::Item>, c: Self) {}
1013}
1014
1015impl<T> IntoIterator for Seq<T> {
1016 type Item = T;
1017 type IntoIter = Iter<T>;
1018
1019 #[check(ghost)]
1020 #[ensures(self == result@)]
1021 fn into_iter(self) -> Self::IntoIter {
1022 Iter(self)
1023 }
1024}
1025
1026impl<'a, T> IntoIterator for &'a Seq<T> {
1027 type Item = &'a T;
1028 type IntoIter = Iter<&'a T>;
1029
1030 #[check(ghost)]
1031 #[ensures(*self == result@.to_owned_seq())]
1032 fn into_iter(self) -> Self::IntoIter {
1033 Iter(self.as_refs())
1034 }
1035}
1036
1037impl<'a, T> IntoIterator for &'a mut Seq<T> {
1038 type Item = &'a mut T;
1039 type IntoIter = Iter<&'a mut T>;
1040
1041 #[check(ghost)]
1042 #[ensures(result@.len() == self.len())]
1043 #[ensures((^self).len() == self.len())]
1044 #[ensures(forall<i> 0 <= i && i < self.len() ==> *result@[i] == (*self)[i])]
1045 #[ensures(forall<i> 0 <= i && i < self.len() ==> ^result@[i] == (^self)[i])]
1046 fn into_iter(self) -> Self::IntoIter {
1047 Iter(self.as_muts())
1048 }
1049}
1050
1051impl<T> Resolve for Seq<T> {
1052 #[logic(open, prophetic)]
1053 #[creusot::trusted_trivial_if_param_trivial]
1054 fn resolve(self) -> bool {
1055 pearlite! { forall<i : Int> resolve(self.get(i)) }
1056 }
1057
1058 #[trusted]
1059 #[logic(prophetic)]
1060 #[requires(structural_resolve(self))]
1061 #[ensures(self.resolve())]
1062 fn resolve_coherence(self) {}
1063}
1064
1065impl<T> Resolve for Iter<T> {
1066 #[logic(open, prophetic, inline)]
1067 #[creusot::trusted_trivial_if_param_trivial]
1068 fn resolve(self) -> bool {
1069 pearlite! { resolve(self@) }
1070 }
1071
1072 #[logic(prophetic)]
1073 #[requires(structural_resolve(self))]
1074 #[ensures(self.resolve())]
1075 fn resolve_coherence(self) {}
1076}
1077
1078/// Properties
1079impl<T> Seq<T> {
1080 #[logic(open)]
1081 #[ensures(Seq::singleton(x).flat_map(f) == f.get(x))]
1082 pub fn flat_map_singleton<U>(x: T, f: Mapping<T, Seq<U>>) {}
1083
1084 #[logic(open)]
1085 #[ensures(self.push_back(x).flat_map(f) == self.flat_map(f).concat(f.get(x)))]
1086 #[variant(self.len())]
1087 pub fn flat_map_push_back<U>(self, x: T, f: Mapping<T, Seq<U>>) {
1088 if self.len() > 0 {
1089 Self::flat_map_push_back::<U>(self.tail(), x, f);
1090 proof_assert! { self.tail().push_back(x) == self.push_back(x).tail() }
1091 }
1092 }
1093}