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_logic(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, inline)]
159    pub fn tail(self) -> Self {
160        self[1..]
161    }
162
163    /// Returns the sequence without its last element.
164    ///
165    /// If the sequence is empty, the result is meaningless.
166    ///
167    /// # Example
168    ///
169    /// ```
170    /// # use creusot_std::prelude::*;
171    /// let s = snapshot!(seq![5, 10, 15]);
172    /// proof_assert!(s.init() == seq![5, 10]);
173    /// proof_assert!(s.init().init() == Seq::singleton(5));
174    /// proof_assert!(s.init().init().init() == Seq::empty());
175    /// ```
176    #[logic(open, inline)]
177    pub fn init(self) -> Self {
178        self[..self.len() - 1]
179    }
180
181    /// Returns the number of elements in the sequence, also referred to as its 'length'.
182    ///
183    /// # Example
184    ///
185    /// ```
186    /// # use creusot_std::prelude::*;
187    /// #[requires(v@.len() > 0)]
188    /// fn f<T>(v: Vec<T>) { /* ... */ }
189    /// ```
190    #[logic]
191    #[builtin("seq.Seq.length")]
192    pub fn len_logic(self) -> Int {
193        dead
194    }
195
196    /// Returns a new sequence, where the element at index `ix` has been replaced by `x`.
197    ///
198    /// If `ix` is out of bounds, the result is meaningless.
199    ///
200    /// # Example
201    ///
202    /// ```
203    /// # use creusot_std::prelude::*;
204    /// let s = snapshot!(Seq::create(2, |_| 0));
205    /// let s2 = snapshot!(s.set(1, 3));
206    /// proof_assert!(s2[0] == 0);
207    /// proof_assert!(s2[1] == 3);
208    /// ```
209    #[logic]
210    #[builtin("seq.Seq.set")]
211    pub fn set(self, ix: Int, x: T) -> Self {
212        let _ = ix;
213        let _ = x;
214        dead
215    }
216
217    /// Extensional equality
218    ///
219    /// Returns `true` if `self` and `other` have the same length, and contain the same
220    /// elements at the same indices.
221    ///
222    /// This is in fact equivalent with normal equality.
223    #[logic]
224    #[builtin("seq.Seq.(==)")]
225    pub fn ext_eq(self, other: Self) -> bool {
226        let _ = other;
227        dead
228    }
229
230    // internal wrapper to match the order of arguments of Seq.cons
231    #[doc(hidden)]
232    #[logic]
233    #[builtin("seq.Seq.cons")]
234    pub fn cons_(_: T, _: Self) -> Self {
235        dead
236    }
237
238    /// Returns a new sequence, where `x` has been prepended to `self`.
239    ///
240    /// # Example
241    ///
242    /// ```
243    /// let s = snapshot!(Seq::singleton(1));
244    /// let s2 = snapshot!(s.cons(2));
245    /// proof_assert!(s2[0] == 2);
246    /// proof_assert!(s2[1] == 1);
247    /// ```
248    #[logic(open, inline)]
249    pub fn cons(self, x: T) -> Self {
250        Self::cons_(x, self)
251    }
252
253    /// Returns a new sequence, where `x` has been appended to `self`.
254    ///
255    /// # Example
256    ///
257    /// ```
258    /// let s = snapshot!(Seq::singleton(1));
259    /// let s2 = snapshot!(s.snoc(2));
260    /// proof_assert!(s2[0] == 1);
261    /// proof_assert!(s2[1] == 2);
262    /// ```
263    #[logic]
264    #[builtin("seq.Seq.snoc")]
265    pub fn snoc(self, x: T) -> Self {
266        let _ = x;
267        dead
268    }
269
270    /// Returns a new sequence, made of the concatenation of `self` and `other`.
271    ///
272    /// See also the program function [`Seq::extend`].
273    ///
274    /// # Example
275    ///
276    /// ```
277    /// # use creusot_std::prelude::*;
278    /// let s1 = snapshot!(Seq::singleton(1));
279    /// let s2 = snapshot!(Seq::create(2, |i| i));
280    /// let s = snapshot!(s1.concat(s2));
281    /// proof_assert!(s[0] == 1);
282    /// proof_assert!(s[1] == 0);
283    /// proof_assert!(s[2] == 1);
284    /// ```
285    #[logic]
286    #[builtin("seq.Seq.(++)")]
287    pub fn concat(self, other: Self) -> Self {
288        let _ = other;
289        dead
290    }
291
292    #[logic]
293    #[ensures(result.len() == self.len())]
294    #[ensures(forall<i> 0 <= i && i < self.len() ==> result[i] == m[self[i]])]
295    #[variant(self.len())]
296    pub fn map<U>(self, m: Mapping<T, U>) -> Seq<U> {
297        if self.len() == 0 {
298            Seq::empty()
299        } else {
300            self.tail().map(m).cons(m.get(*self.index_logic_unsized(0)))
301        }
302    }
303
304    #[logic(open, inline)]
305    pub fn flat_map<U>(self, f: Mapping<T, Seq<U>>) -> Seq<U> {
306        self.map(f).flatten()
307    }
308
309    /// Returns a new sequence, which is `self` in reverse order.
310    ///
311    /// # Example
312    ///
313    /// ```
314    /// # use creusot_std::prelude::*;
315    /// let s = snapshot!(Seq::create(3, |i| i));
316    /// let s2 = snapshot!(s.reverse());
317    /// proof_assert!(s2[0] == 2);
318    /// proof_assert!(s2[1] == 1);
319    /// proof_assert!(s2[2] == 0);
320    /// ```
321    #[logic]
322    #[builtin("seq.Reverse.reverse")]
323    pub fn reverse(self) -> Self {
324        dead
325    }
326
327    #[logic]
328    #[ensures(Self::empty().reverse() == Self::empty())]
329    pub fn reverse_empty() {}
330
331    #[logic]
332    #[requires(0 <= position && position <= self.len())]
333    #[ensures(result.len() == self.len() + 1)]
334    #[ensures(forall<i> 0 <= i && i <= self.len() ==>
335        if i < position {
336            result[i] == self[i]
337        } else if i == position {
338            result[i] == value
339        } else {
340            result[i] == self[i - 1]
341        }
342    )]
343    #[variant(position)]
344    pub fn add_at(self, position: Int, value: T) -> Self {
345        if position == 0 {
346            self.cons(value)
347        } else {
348            self.tail().add_at(position - 1, value).cons(self[0])
349        }
350    }
351
352    /// Returns a new sequence, which is `self` with the element at the given `index` removed.
353    ///
354    /// See also the program function [`Seq::remove`].
355    ///
356    /// # Example
357    ///
358    /// ```rust,creusot
359    /// # use creusot_std::prelude::*;
360    /// let s = snapshot!(seq![7, 8, 9]);
361    /// proof_assert!(removed(*s, 1) == seq![7, 9]);
362    /// ```
363    #[logic(open)]
364    pub fn removed(self, index: Int) -> Self {
365        pearlite! { self[..index].concat(self[index+1..]) }
366    }
367
368    /// Returns `true` if `other` is a permutation of `self`.
369    #[logic(open)]
370    pub fn permutation_of(self, other: Self) -> bool {
371        self.permut(other, 0, self.len())
372    }
373
374    /// Returns `true` if:
375    /// - `self` and `other` have the same length
376    /// - `start` and `end` are in bounds (between `0` and `self.len()` included)
377    /// - Every element occurs as many times in `self[start..end]` as in `other[start..end]`.
378    #[logic]
379    #[builtin("seq.Permut.permut")]
380    pub fn permut(self, other: Self, start: Int, end: Int) -> bool {
381        let _ = other;
382        let _ = start;
383        let _ = end;
384        dead
385    }
386
387    /// Returns `true` if:
388    /// - `self` and `other` have the same length
389    /// - `i` and `j` are in bounds (between `0` and `self.len()` excluded)
390    /// - `other` is equal to `self` where the elements at `i` and `j` are swapped
391    #[logic]
392    #[builtin("seq.Permut.exchange")]
393    pub fn exchange(self, other: Self, i: Int, j: Int) -> bool {
394        let _ = other;
395        let _ = i;
396        let _ = j;
397        dead
398    }
399
400    /// Returns `true` if there is an index `i` such that `self[i] == x`.
401    #[logic(open)]
402    pub fn contains(self, x: T) -> bool {
403        pearlite! { exists<i> 0 <= i &&  i < self.len() && self[i] == x }
404    }
405
406    /// Returns `true` if `self` is sorted between `start` and `end`.
407    #[logic(open)]
408    pub fn sorted_range(self, start: Int, end: Int) -> bool
409    where
410        T: OrdLogic,
411    {
412        pearlite! {
413            forall<i, j> start <= i && i <= j && j < end ==> self[i] <= self[j]
414        }
415    }
416
417    /// Returns `true` if `self` is sorted.
418    #[logic(open)]
419    pub fn sorted(self) -> bool
420    where
421        T: OrdLogic,
422    {
423        self.sorted_range(0, self.len())
424    }
425
426    #[logic]
427    #[ensures(self.concat(other).contains(x) == self.contains(x) || other.contains(x))]
428    pub fn concat_contains(self, other: Self, x: T) {}
429
430    #[logic]
431    #[ensures(self.concat(other1).concat(other2) == self.concat(other1.concat(other2)))]
432    pub fn concat_assoc(self, other1: Self, other2: Self) {}
433
434    #[logic]
435    #[ensures(self.concat(Seq::empty()) == self)]
436    #[ensures(Seq::empty().concat(self) == self)]
437    pub fn concat_empty(self) {}
438
439    #[logic]
440    #[ensures(self.concat(other).reverse() == other.reverse().concat(self.reverse()))]
441    pub fn reverse_concat(self, other: Self) {}
442
443    #[logic]
444    #[ensures(Seq::singleton(x).map(f) == Seq::singleton(f.get(x)))]
445    pub fn singleton_map<U>(x: T, f: Mapping<T, U>) {
446        let _ = Self::ext_eq;
447    }
448
449    #[logic]
450    #[ensures(self.snoc(x).map(f) == self.map(f).snoc(f.get(x)))]
451    pub fn snoc_map<U>(self, x: T, f: Mapping<T, U>) {}
452
453    #[logic]
454    #[ensures(self.cons(x).map(f) == self.map(f).cons(f.get(x)))]
455    pub fn cons_map<U>(self, x: T, f: Mapping<T, U>) {}
456
457    #[logic]
458    #[ensures(self.concat(other).map(f) == self.map(f).concat(other.map(f)))]
459    pub fn concat_map<U>(self, other: Self, f: Mapping<T, U>) {}
460
461    #[logic]
462    #[ensures(Seq::singleton(x).flat_map(f) == f.get(x))]
463    pub fn singleton_flat_map<U>(x: T, f: Mapping<T, Seq<U>>) {}
464
465    #[logic]
466    #[ensures(self.snoc(x).flat_map(f) == self.flat_map(f).concat(f.get(x)))]
467    pub fn snoc_flat_map<U>(self, x: T, f: Mapping<T, Seq<U>>) {
468        let _ = Seq::<Seq<U>>::snoc_flatten;
469        let _ = Self::snoc_map::<Seq<U>>;
470    }
471
472    #[logic]
473    #[ensures(self.cons(x).flat_map(f) == f.get(x).concat(self.flat_map(f)))]
474    pub fn cons_flat_map<U>(self, x: T, f: Mapping<T, Seq<U>>) {
475        let _ = Seq::<Seq<U>>::cons_flatten;
476        let _ = Self::cons_map::<Seq<U>>;
477    }
478
479    #[logic]
480    #[ensures(self.concat(other).flat_map(f) == self.flat_map(f).concat(other.flat_map(f)))]
481    pub fn concat_flat_map<U>(self, other: Seq<T>, f: Mapping<T, Seq<U>>) {
482        let _ = Seq::<Seq<U>>::concat_flatten;
483        let _ = Self::concat_map::<Seq<U>>;
484    }
485}
486
487impl<T> Seq<Seq<T>> {
488    #[logic(open)]
489    #[variant(self.len())]
490    pub fn flatten(self) -> Seq<T> {
491        if self.len() == 0 {
492            Seq::empty()
493        } else {
494            self.index_logic_unsized(0).concat(self.tail().flatten())
495        }
496    }
497
498    #[logic]
499    #[ensures(Seq::singleton(x).flatten() == x)]
500    pub fn singleton_flatten(x: Seq<T>) {}
501
502    #[logic]
503    #[ensures(self.snoc(x).flatten() == self.flatten().concat(x))]
504    pub fn snoc_flatten(self, x: Seq<T>) {
505        proof_assert!(self.snoc(x) == self.concat(Seq::singleton(x)));
506        self.concat_flatten(Seq::singleton(x));
507        Self::singleton_flatten(x);
508    }
509
510    #[logic]
511    #[ensures(self.cons(x).flatten() == x.concat(self.flatten()))]
512    pub fn cons_flatten(self, x: Seq<T>) {}
513
514    #[logic]
515    #[ensures(self.concat(other).flatten() == self.flatten().concat(other.flatten()))]
516    #[variant(self.len())]
517    pub fn concat_flatten(self, other: Self) {
518        if self.len() > 0 {
519            self.tail().concat_flatten(other);
520        }
521    }
522
523    #[logic]
524    #[ensures(self.flatten() == self.flat_map(|s|s))]
525    pub fn flatten_flat_map(self) {}
526}
527
528impl<T> Seq<&T> {
529    /// Convert `Seq<&T>` to `Seq<T>`.
530    ///
531    /// This is simply a utility method, because `&T` is equivalent to `T` in pearlite.
532    #[logic]
533    #[builtin("identity")]
534    pub fn to_owned_seq(self) -> Seq<T> {
535        dead
536    }
537}
538
539impl<T> IndexLogic<Int> for Seq<T> {
540    type Item = T;
541
542    #[logic]
543    #[builtin("seq.Seq.get")]
544    fn index_logic(self, _: Int) -> Self::Item {
545        dead
546    }
547}
548
549impl<T> IndexLogic<Range<Int>> for Seq<T> {
550    type Item = Seq<T>;
551
552    #[logic(open, inline)]
553    fn index_logic(self, range: Range<Int>) -> Self::Item {
554        self.subsequence(range.start, range.end)
555    }
556}
557
558impl<T> IndexLogic<RangeInclusive<Int>> for Seq<T> {
559    type Item = Seq<T>;
560
561    #[logic(open, inline)]
562    fn index_logic(self, range: RangeInclusive<Int>) -> Self::Item {
563        self.subsequence(range.start_log(), range.end_log() + 1)
564    }
565}
566
567impl<T> IndexLogic<RangeFull> for Seq<T> {
568    type Item = Seq<T>;
569
570    #[logic(open, inline)]
571    fn index_logic(self, _: RangeFull) -> Self::Item {
572        self
573    }
574}
575
576impl<T> IndexLogic<RangeFrom<Int>> for Seq<T> {
577    type Item = Seq<T>;
578
579    #[logic(open, inline)]
580    fn index_logic(self, range: RangeFrom<Int>) -> Self::Item {
581        self.subsequence(range.start, self.len())
582    }
583}
584
585impl<T> IndexLogic<RangeTo<Int>> for Seq<T> {
586    type Item = Seq<T>;
587
588    #[logic(open, inline)]
589    fn index_logic(self, range: RangeTo<Int>) -> Self::Item {
590        self.subsequence(0, range.end)
591    }
592}
593
594impl<T> IndexLogic<RangeToInclusive<Int>> for Seq<T> {
595    type Item = Seq<T>;
596
597    #[logic(open, inline)]
598    fn index_logic(self, range: RangeToInclusive<Int>) -> Self::Item {
599        self.subsequence(0, range.end + 1)
600    }
601}
602
603impl<T: PartialOrdLogic> PartialOrdLogic for Seq<T> {
604    #[logic(open)]
605    fn lt_log(self, other: Self) -> bool {
606        pearlite! {
607            (exists<i: Int> 0 <= i && i < self.len() && i < other.len() &&
608                (forall<j: Int> 0 <= j && j < i ==> self[j] == other[j]) &&
609                self[i] < other[i])
610            ||
611            self.len() < other.len() &&
612            (forall<i: Int> 0 <= i && i < self.len() ==> self[i] == other[i])
613        }
614    }
615
616    #[logic(law)]
617    #[ensures(!(self < self))]
618    fn irreflexive(self) {}
619
620    #[logic(law)]
621    #[requires(x < y)]
622    #[requires(y < z)]
623    #[ensures(x < z)]
624    fn transitive(x: Self, y: Self, z: Self) {}
625
626    #[logic(law)]
627    #[ensures((self <= other) == (self < other || self == other))]
628    fn le_lt_log(self, other: Self) {}
629}
630
631impl<T: OrdLogic> Seq<T> {
632    #[logic]
633    #[requires(self.len() > 0 && other.len() > 0)]
634    #[requires(self[0] == other[0])]
635    #[ensures((self < other) == (self[1..] < other[1..]))]
636    fn lt_log_tail(self, other: Self) {
637        pearlite! {
638            let _ = |i| {
639                if 0 <= i && i < self.len() && i < other.len() &&
640                        (forall<j: Int> 0 <= j && j < i ==> self[j] == other[j]) &&
641                        self[i] < other[i] {
642                    proof_assert!(forall<j: Int> 0 <= j && j < i-1 ==> self[1..][j] == other[1..][j]);
643                    proof_assert!(self[1..][i-1] < other[1..][i-1]);
644                }
645            };
646        }
647    }
648}
649
650impl<T: OrdLogic> OrdLogic for Seq<T> {
651    #[logic(law)]
652    #[ensures(self < other || self == other || other < self)]
653    #[variant(self.len())]
654    fn lt_log_total(self, other: Self) {
655        if self.len() > 0 && other.len() > 0 {
656            if self[0] == other[0] {
657                self[1..].lt_log_total(other[1..]);
658                self.lt_log_tail(other);
659                other.lt_log_tail(self);
660                proof_assert!(forall<i> 0 < i && i < self.len() ==> self[i] == self[1..][i-1]);
661                proof_assert!(forall<i> 0 < i && i < other.len() ==> other[i] == other[1..][i-1]);
662            } else {
663                self[0].lt_log_total(other[0]);
664            }
665        }
666    }
667}
668
669/// Ghost definitions
670
671impl<T> Invariant for Seq<T> {
672    #[logic(open, prophetic, inline)]
673    #[creusot::trusted_trivial_if_param_trivial]
674    fn invariant(self) -> bool {
675        pearlite! { forall<i> 0 <= i && i < self.len() ==> inv(self.index_logic_unsized(i)) }
676    }
677}
678
679impl<T> Resolve for Seq<T> {
680    #[logic(open, prophetic)]
681    #[creusot::trusted_trivial_if_param_trivial]
682    fn resolve(self) -> bool {
683        pearlite! { forall<i : Int> 0 <= i && i < self.len() ==> resolve(self[i]) }
684    }
685
686    #[trusted]
687    #[logic(prophetic)]
688    #[requires(structural_resolve(self))]
689    #[ensures(self.resolve())]
690    fn resolve_coherence(self) {}
691}
692
693impl<T> Seq<T> {
694    /// Constructs a new, empty `Seq<T>`.
695    ///
696    /// This can only be manipulated in the ghost world, and as such is wrapped in [`Ghost`].
697    ///
698    /// # Example
699    ///
700    /// ```rust,creusot
701    /// use creusot_std::prelude::*;
702    /// let ghost_seq = Seq::<i32>::new();
703    /// proof_assert!(seq == Seq::create());
704    /// ```
705    #[trusted]
706    #[check(ghost)]
707    #[ensures(*result == Self::empty())]
708    #[allow(unreachable_code)]
709    pub fn new() -> Ghost<Self> {
710        Ghost::conjure()
711    }
712
713    /// Returns the number of elements in the sequence, also referred to as its 'length'.
714    ///
715    /// If you need to get the length in pearlite, consider using [`len`](Self::len).
716    ///
717    /// # Example
718    /// ```rust,creusot
719    /// use creusot_std::prelude::*;
720    ///
721    /// let mut s = Seq::new();
722    /// ghost! {
723    ///     s.push_back(1);
724    ///     s.push_back(2);
725    ///     s.push_back(3);
726    ///     let len = s.len();
727    ///     proof_assert!(len == 3);
728    /// };
729    /// ```
730    #[trusted]
731    #[check(ghost)]
732    #[logic_alias(self.len_logic())]
733    pub fn len(&self) -> Int {
734        panic!()
735    }
736
737    /// Returns `true` if the sequence is empty.
738    ///
739    /// # Example
740    ///
741    /// ```rust,creusot
742    /// use creusot_std::prelude::*;
743    /// #[check(ghost)]
744    /// #[requires(s.len() == 0)]
745    /// pub fn foo(mut s: Seq<i32>) {
746    ///     assert!(s.is_empty());
747    ///     s.push_back(1i32);
748    ///     assert!(!s.is_empty());
749    /// }
750    /// ghost! {
751    ///     foo(Seq::new().into_inner())
752    /// };
753    /// ```
754    #[trusted]
755    #[check(ghost)]
756    #[ensures(result == (self.len() == 0))]
757    pub fn is_empty(&self) -> bool {
758        panic!()
759    }
760
761    /// Appends an element to the front of a collection.
762    ///
763    /// # Example
764    /// ```rust,creusot
765    /// use creusot_std::prelude::*;
766    ///
767    /// let mut s = Seq::new();
768    /// ghost! {
769    ///     s.push_front(1);
770    ///     s.push_front(2);
771    ///     s.push_front(3);
772    ///     proof_assert!(s[0] == 3i32 && s[1] == 2i32 && s[2] == 1i32);
773    /// };
774    /// ```
775    #[trusted]
776    #[check(ghost)]
777    #[ensures(^self == self.cons(x))]
778    pub fn push_front(&mut self, x: T) {
779        let _ = x;
780        panic!()
781    }
782
783    /// Appends an element to the back of a collection.
784    ///
785    /// # Example
786    /// ```rust,creusot
787    /// use creusot_std::prelude::*;
788    ///
789    /// let mut s = Seq::new();
790    /// ghost! {
791    ///     s.push_back(1);
792    ///     s.push_back(2);
793    ///     s.push_back(3);
794    ///     proof_assert!(s[0] == 1i32 && s[1] == 2i32 && s[2] == 3i32);
795    /// };
796    /// ```
797    #[trusted]
798    #[check(ghost)]
799    #[ensures(^self == self.snoc(x))]
800    pub fn push_back(&mut self, x: T) {
801        let _ = x;
802        panic!()
803    }
804
805    /// Returns a reference to an element at `index` or `None` if `index` is out of bounds.
806    ///
807    /// # Example
808    /// ```rust,creusot
809    /// use creusot_std::prelude::*;
810    ///
811    /// let mut s = Seq::new();
812    /// ghost! {
813    ///     s.push_back(10);
814    ///     s.push_back(40);
815    ///     s.push_back(30);
816    ///     let get1 = s.get(1int);
817    ///     let get2 = s.get(3int);
818    ///     proof_assert!(get1 == Some(&40i32));
819    ///     proof_assert!(get2 == None);
820    /// };
821    /// ```
822    #[check(ghost)]
823    #[logic_alias(if 0 <= index && index < self.len() { Some(&self.index_logic(index)) } else { None })]
824    pub fn get(&self, index: Int) -> Option<&T> {
825        // FIXME: we can't write 0 outside of a `ghost!` block
826        if index - index <= index && index < self.len() {
827            Some(self.as_refs().extract(index))
828        } else {
829            None
830        }
831    }
832
833    /// Returns a mutable reference to an element at `index` or `None` if `index` is out of bounds.
834    ///
835    /// # Example
836    /// ```rust,creusot
837    /// use creusot_std::prelude::*;
838    ///
839    /// let mut s = Seq::new();
840    ///
841    /// ghost! {
842    ///     s.push_back(0);
843    ///     s.push_back(1);
844    ///     s.push_back(2);
845    ///     if let Some(elem) = s.get_mut(1int) {
846    ///         *elem = 42;
847    ///     }
848    ///     proof_assert!(s[0] == 0i32 && s[1] == 42i32 && s[2] == 2i32);
849    /// };
850    /// ```
851    #[check(ghost)]
852    #[ensures(match result {
853        None => self.get(index) == None && *self == ^self,
854        Some(r) => self.get(index) == Some(&*r) && ^r == (^self)[index],
855    })]
856    #[ensures(forall<i> i != index ==> (*self).get(i) == (^self).get(i))]
857    #[ensures((*self).len() == (^self).len())]
858    pub fn get_mut(&mut self, index: Int) -> Option<&mut T> {
859        // FIXME: we can't write 0 outside of a `ghost!` block
860        if index - index <= index && index < self.len() {
861            Some(self.as_muts().extract(index))
862        } else {
863            None
864        }
865    }
866
867    /// Insert an element in the middle of the sequence.
868    ///
869    /// The new element is located at index `position`.
870    ///
871    /// # Example
872    ///
873    /// ```rust,creusot
874    /// use creusot_std::prelude::*;
875    ///
876    /// let mut s = Seq::new();
877    /// ghost! {
878    ///     s.push_back(0);
879    ///     s.push_back(1);
880    ///     s.push_back(2);
881    ///     // s = [0, 1, 2]
882    ///
883    ///     s.insert(0int, 10);
884    ///     // s = [10, 0, 1, 2]
885    ///     s.insert(2int, 11);
886    ///     // s = [10, 0, 11, 1, 2]
887    ///     s.insert(5int, 12);
888    ///     // s = [10, 0, 11, 1, 2, 12]
889    /// };
890    /// ```
891    #[check(ghost)]
892    #[requires(0 <= position && position <= self.len())]
893    #[ensures((^self) == self.add_at(position, x))]
894    #[variant(position)]
895    pub fn insert(&mut self, position: Int, x: T) {
896        let after = self.split_off(position);
897        self.push_back(x);
898        self.extend(after);
899    }
900
901    /// Remove an element and discard the rest of the sequence.
902    ///
903    /// This is sometimes preferable to `remove` because this avoids reasoning about subsequences.
904    #[check(ghost)]
905    #[requires(0 <= index && index < self.len())]
906    #[ensures(result == self[index])]
907    #[ensures(forall<i> 0 <= i && i < self.len() && i != index ==> resolve(self[i]))]
908    pub fn extract(mut self, index: Int) -> T {
909        proof_assert! { forall<i> index < i && i < self.len() ==> self[i] == self[index + 1..][i - index - 1] }
910        self.split_off(index).pop_front().unwrap()
911    }
912
913    /// Remove an element from a sequence.
914    ///
915    /// See also the logic function [`Seq::removed`].
916    #[check(ghost)]
917    #[requires(0 <= index && index < self.len())]
918    #[ensures(result == self[index])]
919    #[ensures(^self == (*self).removed(index))]
920    pub fn remove(&mut self, index: Int) -> T {
921        let mut right = self.split_off(index);
922        let result = right.pop_front().unwrap();
923        self.extend(right);
924        result
925    }
926
927    /// Append a sequence to another.
928    ///
929    /// See also the logic function [`Seq::concat`].
930    ///
931    /// ## Remark
932    ///
933    /// The second argument is currently restricted to sequences.
934    /// Generalizing it to arbitrary `IntoIterator` requires some missing features
935    /// to specify that the iterator terminates and that its methods are
936    /// callable in ghost code.
937    #[check(ghost)]
938    #[ensures(^self == (*self).concat(rhs))]
939    pub fn extend(&mut self, mut rhs: Self) {
940        let _final = snapshot! { self.concat(rhs) };
941        #[variant(rhs.len())]
942        #[invariant(self.concat(rhs) == *_final)]
943        while let Some(x) = rhs.pop_front() {
944            self.push_back(x)
945        }
946    }
947
948    /// Removes the last element from a vector and returns it, or `None` if it is empty.
949    ///
950    /// # Example
951    /// ```rust,creusot
952    /// use creusot_std::prelude::*;
953    ///
954    /// let mut s = Seq::new();
955    /// ghost! {
956    ///     s.push_back(1);
957    ///     s.push_back(2);
958    ///     s.push_back(3);
959    ///     let popped = s.pop_back();
960    ///     proof_assert!(popped == Some(3i32));
961    ///     proof_assert!(s[0] == 1i32 && s[1] == 2i32);
962    /// };
963    /// ```
964    #[trusted]
965    #[check(ghost)]
966    #[ensures(match result {
967        None => *self == Seq::empty() && *self == ^self,
968        Some(r) => *self == (^self).snoc(r)
969    })]
970    pub fn pop_back(&mut self) -> Option<T> {
971        panic!()
972    }
973
974    /// Removes the first element from a vector and returns it, or `None` if it is empty.
975    ///
976    /// # Example
977    /// ```rust,creusot
978    /// use creusot_std::prelude::*;
979    ///
980    /// let mut s = Seq::new();
981    /// ghost! {
982    ///     s.push_back(1);
983    ///     s.push_back(2);
984    ///     s.push_back(3);
985    ///     let popped = s.pop_front();
986    ///     proof_assert!(popped == Some(1i32));
987    ///     proof_assert!(s[0] == 2i32 && s[1] == 3i32);
988    /// };
989    /// ```
990    #[trusted]
991    #[check(ghost)]
992    #[ensures(match result {
993        None => *self == Seq::empty() && *self == ^self,
994        Some(r) => (*self).len() > 0 && r == (*self)[0] && ^self == (*self).tail()
995    })]
996    pub fn pop_front(&mut self) -> Option<T> {
997        panic!()
998    }
999
1000    /// Clears the sequence, removing all values.
1001    ///
1002    /// # Example
1003    /// ```rust,creusot
1004    /// use creusot_std::prelude::*;
1005    ///
1006    /// let mut s = Seq::new();
1007    /// ghost! {
1008    ///     s.push_back(1);
1009    ///     s.push_back(2);
1010    ///     s.push_back(3);
1011    ///     s.clear();
1012    ///     proof_assert!(s == Seq::empty());
1013    /// };
1014    /// ```
1015    #[trusted]
1016    #[check(ghost)]
1017    #[ensures(^self == Self::empty())]
1018    pub fn clear(&mut self) {}
1019
1020    /// Split a sequence in two at the given index.
1021    #[trusted]
1022    #[check(ghost)]
1023    #[requires(0 <= mid && mid <= self.len())]
1024    #[ensures(^self == self[..mid])]
1025    #[ensures(result == self[mid..])]
1026    pub fn split_off(&mut self, mid: Int) -> Self {
1027        let _ = mid;
1028        panic!("ghost code")
1029    }
1030
1031    /// Borrow every element of a borrowed sequence.
1032    #[trusted]
1033    #[check(ghost)]
1034    #[ensures(*self == result.to_owned_seq())]
1035    pub fn as_refs(&self) -> Seq<&T> {
1036        panic!("ghost code")
1037    }
1038
1039    /// Mutably borrow every element of a borrowed sequence.
1040    #[trusted]
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    pub fn as_muts(&mut self) -> Seq<&mut T> {
1047        panic!("ghost code")
1048    }
1049}
1050
1051impl<T> core::ops::Index<Int> for Seq<T> {
1052    type Output = T;
1053
1054    #[check(ghost)]
1055    #[requires(0 <= index && index < self.len())]
1056    #[ensures(*result == self[index])]
1057    fn index(&self, index: Int) -> &Self::Output {
1058        self.get(index).unwrap()
1059    }
1060}
1061
1062impl<T> core::ops::IndexMut<Int> for Seq<T> {
1063    #[check(ghost)]
1064    #[requires(0 <= index && index < self.len())]
1065    #[ensures((*self).len() == (^self).len())]
1066    #[ensures(*result == (*self)[index] && ^result == (^self)[index])]
1067    #[ensures(forall<i> 0 <= i && i < self.len() && i != index ==> (*self)[i] == (^self)[i])]
1068    fn index_mut(&mut self, index: Int) -> &mut Self::Output {
1069        self.get_mut(index).unwrap()
1070    }
1071}
1072
1073impl<T> core::ops::Index<(Int, Int)> for Seq<T> {
1074    type Output = (T, T);
1075
1076    #[trusted]
1077    #[check(ghost)]
1078    #[requires(0 <= index.0 && index.0 < self.len() && 0 <= index.1 && index.1 < self.len())]
1079    #[ensures(result.0 == self[index.0] && result.1 == self[index.1])]
1080    #[allow(unused_variables)]
1081    fn index(&self, index: (Int, Int)) -> &Self::Output {
1082        panic!()
1083    }
1084}
1085
1086impl<T> core::ops::IndexMut<(Int, Int)> for Seq<T> {
1087    #[trusted]
1088    #[check(ghost)]
1089    #[requires(0 <= index.0 && index.0 < self.len() && 0 <= index.1 && index.1 < self.len())]
1090    #[requires(index.0 != index.1)]
1091    #[ensures((*result).0 == (*self)[index.0] && (*result).1 == (*self)[index.1]
1092           && (^result).0 == (^self)[index.0] && (^result).1 == (^self)[index.1])]
1093    #[ensures(forall<i> i != index.0 && i != index.1 ==> (*self).get(i) == (^self).get(i))]
1094    #[ensures((*self).len() == (^self).len())]
1095    #[allow(unused_variables)]
1096    fn index_mut(&mut self, index: (Int, Int)) -> &mut Self::Output {
1097        panic!()
1098    }
1099}
1100
1101// Having `Copy` guarantees that the operation is pure, even if we decide to change the definition of `Clone`.
1102impl<T: Clone + Copy> Clone for Seq<T> {
1103    #[trusted]
1104    #[check(ghost)]
1105    #[ensures(result == *self)]
1106    fn clone(&self) -> Self {
1107        *self
1108    }
1109}
1110
1111impl<T: Copy> Copy for Seq<T> {}
1112impl<T: Plain> Plain for Seq<T> {
1113    #[requires(inv(*snap))]
1114    #[ensures(*result == *snap)]
1115    #[check(ghost)]
1116    #[allow(unused_variables)]
1117    fn into_ghost(snap: Snapshot<Self>) -> Ghost<Self> {
1118        ghost! {
1119            let mut res = Seq::new().into_inner();
1120            let len: Snapshot<Int> = snapshot!(snap.len());
1121            let len = len.into_ghost().into_inner();
1122            let mut i = 0int;
1123            #[variant(len - i)]
1124            #[invariant(i <= len)]
1125            #[invariant(res.len() == i)]
1126            #[invariant(forall<j> 0 <= j && j < i ==> res[j] == snap[j])]
1127            while i < len {
1128                let elem: Snapshot<T> = snapshot!(snap[i]);
1129                res.push_back(elem.into_ghost().into_inner());
1130                i = i + 1int;
1131            }
1132            res
1133        }
1134    }
1135}
1136
1137// =========
1138// Iterators
1139// =========
1140
1141/// Iterator for sequences.
1142///
1143/// This provides all three variants of `IntoIter` for `Seq`:
1144/// `Iter<T>`, `Iter<&T>`, `Iter<&mut T>`.
1145///
1146/// This is a different type from `Seq` to enable `IntoIterator for &mut Seq<T>`
1147/// (if `Seq` were an iterator, that would conflict with `IntoIterator for I where I: Iterator`).
1148///
1149/// # Ghost code and variants
1150///
1151/// This iterator is only obtainable in ghost code.
1152///
1153/// To use it in a `for` loop, a variant must be declared:
1154/// ```rust,creusot
1155/// # use creusot_std::prelude::*;
1156/// # #[requires(true)]
1157/// fn iter_on_seq<T>(s: Seq<T>) {
1158///     let len = snapshot!(s.len());
1159///     #[variant(len - produced.len())]
1160///     for i in s {
1161///         // ...
1162///     }
1163/// }
1164/// ```
1165pub struct Iter<T>(Seq<T>);
1166
1167impl<T> View for Iter<T> {
1168    type ViewTy = Seq<T>;
1169    #[logic]
1170    fn view(self) -> Self::ViewTy {
1171        self.0
1172    }
1173}
1174
1175impl<T> Iterator for Iter<T> {
1176    type Item = T;
1177
1178    #[check(ghost)]
1179    #[ensures(match result {
1180        None => self.completed(),
1181        Some(v) => (*self).produces(Seq::singleton(v), ^self)
1182    })]
1183    fn next(&mut self) -> Option<T> {
1184        self.0.pop_front()
1185    }
1186}
1187
1188impl<T> IteratorSpec for Iter<T> {
1189    #[logic(prophetic, inline, open)]
1190    fn produces(self, visited: Seq<T>, o: Self) -> bool {
1191        pearlite! { self@ == visited.concat(o@) }
1192    }
1193
1194    #[logic(prophetic, inline, open)]
1195    fn completed(&mut self) -> bool {
1196        pearlite! { self@ == Seq::empty() }
1197    }
1198
1199    #[logic(law)]
1200    #[ensures(self.produces(Seq::empty(), self))]
1201    fn produces_refl(self) {}
1202
1203    #[logic(law)]
1204    #[requires(a.produces(ab, b))]
1205    #[requires(b.produces(bc, c))]
1206    #[ensures(a.produces(ab.concat(bc), c))]
1207    fn produces_trans(a: Self, ab: Seq<Self::Item>, b: Self, bc: Seq<Self::Item>, c: Self) {}
1208}
1209
1210impl<T> IntoIterator for Seq<T> {
1211    type Item = T;
1212    type IntoIter = Iter<T>;
1213
1214    #[check(ghost)]
1215    #[ensures(self == result@)]
1216    fn into_iter(self) -> Self::IntoIter {
1217        Iter(self)
1218    }
1219}
1220
1221impl<'a, T> IntoIterator for &'a Seq<T> {
1222    type Item = &'a T;
1223    type IntoIter = Iter<&'a T>;
1224
1225    #[check(ghost)]
1226    #[ensures(*self == result@.to_owned_seq())]
1227    fn into_iter(self) -> Self::IntoIter {
1228        Iter(self.as_refs())
1229    }
1230}
1231
1232impl<'a, T> IntoIterator for &'a mut Seq<T> {
1233    type Item = &'a mut T;
1234    type IntoIter = Iter<&'a mut T>;
1235
1236    #[check(ghost)]
1237    #[ensures(result@.len() == self.len())]
1238    #[ensures((^self).len() == self.len())]
1239    #[ensures(forall<i> 0 <= i && i < self.len() ==> *result@[i] == (*self)[i])]
1240    #[ensures(forall<i> 0 <= i && i < self.len() ==> ^result@[i] == (^self)[i])]
1241    fn into_iter(self) -> Self::IntoIter {
1242        Iter(self.as_muts())
1243    }
1244}
1245
1246impl<T> Resolve for Iter<T> {
1247    #[logic(open, prophetic, inline)]
1248    #[creusot::trusted_trivial_if_param_trivial]
1249    fn resolve(self) -> bool {
1250        pearlite! { resolve(self@) }
1251    }
1252
1253    #[logic(prophetic)]
1254    #[requires(structural_resolve(self))]
1255    #[ensures(self.resolve())]
1256    fn resolve_coherence(self) {}
1257}
creusot_std/logic/seq.rs

creusot_std/logic/
seq.rs
