creusot_std/logic/
seq.rs

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

creusot_std/logic/
seq.rs
