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    /// # Example
279    ///
280    /// ```
281    /// # use creusot_std::prelude::*;
282    /// let s1 = snapshot!(Seq::singleton(1));
283    /// let s2 = snapshot!(Seq::create(2, |i| i));
284    /// let s = snapshot!(s1.concat(s2));
285    /// proof_assert!(s[0] == 1);
286    /// proof_assert!(s[1] == 0);
287    /// proof_assert!(s[2] == 1);
288    /// ```
289    #[logic]
290    #[builtin("seq.Seq.(++)")]
291    pub fn concat(self, other: Self) -> Self {
292        let _ = other;
293        dead
294    }
295
296    #[logic]
297    #[ensures(result.len() == self.len())]
298    #[ensures(forall<i> 0 <= i && i < self.len() ==> result[i] == m[self[i]])]
299    #[variant(self.len())]
300    pub fn map<U>(self, m: Mapping<T, U>) -> Seq<U> {
301        if self.len() == 0 {
302            Seq::empty()
303        } else {
304            self.tail().map(m).push_front(m.get(*self.index_logic_unsized(0)))
305        }
306    }
307
308    #[logic(open)]
309    #[variant(self.len())]
310    pub fn flat_map<U>(self, other: Mapping<T, Seq<U>>) -> Seq<U> {
311        if self.len() == 0 {
312            Seq::empty()
313        } else {
314            other.get(*self.index_logic_unsized(0)).concat(self.tail().flat_map(other))
315        }
316    }
317
318    /// Returns a new sequence, which is `self` in reverse order.
319    ///
320    /// # Example
321    ///
322    /// ```
323    /// # use creusot_std::prelude::*;
324    /// let s = snapshot!(Seq::create(3, |i| i));
325    /// let s2 = snapshot!(s.reverse());
326    /// proof_assert!(s2[0] == 2);
327    /// proof_assert!(s2[1] == 1);
328    /// proof_assert!(s2[2] == 0);
329    /// ```
330    #[logic]
331    #[builtin("seq.Reverse.reverse")]
332    pub fn reverse(self) -> Self {
333        dead
334    }
335
336    /// Returns `true` if `other` is a permutation of `self`.
337    #[logic(open)]
338    pub fn permutation_of(self, other: Self) -> bool {
339        self.permut(other, 0, self.len())
340    }
341
342    /// Returns `true` if:
343    /// - `self` and `other` have the same length
344    /// - `start` and `end` are in bounds (between `0` and `self.len()` included)
345    /// - Every element occurs as many times in `self[start..end]` as in `other[start..end]`.
346    #[logic]
347    #[builtin("seq.Permut.permut")]
348    pub fn permut(self, other: Self, start: Int, end: Int) -> bool {
349        let _ = other;
350        let _ = start;
351        let _ = end;
352        dead
353    }
354
355    /// Returns `true` if:
356    /// - `self` and `other` have the same length
357    /// - `i` and `j` are in bounds (between `0` and `self.len()` excluded)
358    /// - `other` is equal to `self` where the elements at `i` and `j` are swapped
359    #[logic]
360    #[builtin("seq.Permut.exchange")]
361    pub fn exchange(self, other: Self, i: Int, j: Int) -> bool {
362        let _ = other;
363        let _ = i;
364        let _ = j;
365        dead
366    }
367
368    /// Returns `true` if there is an index `i` such that `self[i] == x`.
369    #[logic(open)]
370    pub fn contains(self, x: T) -> bool {
371        pearlite! { exists<i> 0 <= i &&  i < self.len() && self[i] == x }
372    }
373
374    /// Returns `true` if `self` is sorted between `start` and `end`.
375    #[logic(open)]
376    pub fn sorted_range(self, start: Int, end: Int) -> bool
377    where
378        T: OrdLogic,
379    {
380        pearlite! {
381            forall<i, j> start <= i && i <= j && j < end ==> self[i] <= self[j]
382        }
383    }
384
385    /// Returns `true` if `self` is sorted.
386    #[logic(open)]
387    pub fn sorted(self) -> bool
388    where
389        T: OrdLogic,
390    {
391        self.sorted_range(0, self.len())
392    }
393
394    #[logic(open)]
395    #[ensures(forall<a: Seq<T>, b: Seq<T>, x>
396        a.concat(b).contains(x) == a.contains(x) || b.contains(x))]
397    pub fn concat_contains() {}
398}
399
400impl<T> Seq<Seq<T>> {
401    #[logic(open)]
402    #[variant(self.len())]
403    pub fn flatten(self) -> Seq<T> {
404        if self.len() == 0 {
405            Seq::empty()
406        } else {
407            self.index_logic_unsized(0).concat(self.tail().flatten())
408        }
409    }
410}
411
412impl<T> Seq<&T> {
413    /// Convert `Seq<&T>` to `Seq<T>`.
414    ///
415    /// This is simply a utility method, because `&T` is equivalent to `T` in pearlite.
416    #[logic]
417    #[builtin("identity")]
418    pub fn to_owned_seq(self) -> Seq<T> {
419        dead
420    }
421}
422
423impl<T> IndexLogic<Int> for Seq<T> {
424    type Item = T;
425
426    #[logic]
427    #[builtin("seq.Seq.get")]
428    fn index_logic(self, _: Int) -> Self::Item {
429        dead
430    }
431}
432
433impl<T> IndexLogic<Range<Int>> for Seq<T> {
434    type Item = Seq<T>;
435
436    #[logic(open, inline)]
437    fn index_logic(self, range: Range<Int>) -> Self::Item {
438        self.subsequence(range.start, range.end)
439    }
440}
441
442impl<T> IndexLogic<RangeInclusive<Int>> for Seq<T> {
443    type Item = Seq<T>;
444
445    #[logic(open, inline)]
446    fn index_logic(self, range: RangeInclusive<Int>) -> Self::Item {
447        self.subsequence(range.start_log(), range.end_log() + 1)
448    }
449}
450
451impl<T> IndexLogic<RangeFull> for Seq<T> {
452    type Item = Seq<T>;
453
454    #[logic(open, inline)]
455    fn index_logic(self, _: RangeFull) -> Self::Item {
456        self
457    }
458}
459
460impl<T> IndexLogic<RangeFrom<Int>> for Seq<T> {
461    type Item = Seq<T>;
462
463    #[logic(open, inline)]
464    fn index_logic(self, range: RangeFrom<Int>) -> Self::Item {
465        self.subsequence(range.start, self.len())
466    }
467}
468
469impl<T> IndexLogic<RangeTo<Int>> for Seq<T> {
470    type Item = Seq<T>;
471
472    #[logic(open, inline)]
473    fn index_logic(self, range: RangeTo<Int>) -> Self::Item {
474        self.subsequence(0, range.end)
475    }
476}
477
478impl<T> IndexLogic<RangeToInclusive<Int>> for Seq<T> {
479    type Item = Seq<T>;
480
481    #[logic(open, inline)]
482    fn index_logic(self, range: RangeToInclusive<Int>) -> Self::Item {
483        self.subsequence(0, range.end + 1)
484    }
485}
486
487/// Ghost definitions
488impl<T> Seq<T> {
489    /// Constructs a new, empty `Seq<T>`.
490    ///
491    /// This can only be manipulated in the ghost world, and as such is wrapped in [`Ghost`].
492    ///
493    /// # Example
494    ///
495    /// ```rust,creusot
496    /// use creusot_std::prelude::*;
497    /// let ghost_seq = Seq::<i32>::new();
498    /// proof_assert!(seq == Seq::create());
499    /// ```
500    #[trusted]
501    #[check(ghost)]
502    #[ensures(*result == Self::empty())]
503    #[allow(unreachable_code)]
504    pub fn new() -> Ghost<Self> {
505        Ghost::conjure()
506    }
507
508    /// Returns the number of elements in the sequence, also referred to as its 'length'.
509    ///
510    /// If you need to get the length in pearlite, consider using [`len`](Self::len).
511    ///
512    /// # Example
513    /// ```rust,creusot
514    /// use creusot_std::prelude::*;
515    ///
516    /// let mut s = Seq::new();
517    /// ghost! {
518    ///     s.push_back_ghost(1);
519    ///     s.push_back_ghost(2);
520    ///     s.push_back_ghost(3);
521    ///     let len = s.len_ghost();
522    ///     proof_assert!(len == 3);
523    /// };
524    /// ```
525    #[trusted]
526    #[check(ghost)]
527    #[ensures(result == self.len())]
528    pub fn len_ghost(&self) -> Int {
529        panic!()
530    }
531
532    /// Returns `true` if the sequence is empty.
533    ///
534    /// # Example
535    ///
536    /// ```rust,creusot
537    /// use creusot_std::prelude::*;
538    /// #[check(ghost)]
539    /// #[requires(s.len() == 0)]
540    /// pub fn foo(mut s: Seq<i32>) {
541    ///     assert!(s.is_empty_ghost());
542    ///     s.push_back_ghost(1i32);
543    ///     assert!(!s.is_empty_ghost());
544    /// }
545    /// ghost! {
546    ///     foo(Seq::new().into_inner())
547    /// };
548    /// ```
549    #[trusted]
550    #[check(ghost)]
551    #[ensures(result == (self.len() == 0))]
552    pub fn is_empty_ghost(&self) -> bool {
553        panic!()
554    }
555
556    /// Appends an element to the front of a collection.
557    ///
558    /// # Example
559    /// ```rust,creusot
560    /// use creusot_std::prelude::*;
561    ///
562    /// let mut s = Seq::new();
563    /// ghost! {
564    ///     s.push_front_ghost(1);
565    ///     s.push_front_ghost(2);
566    ///     s.push_front_ghost(3);
567    ///     proof_assert!(s[0] == 3i32 && s[1] == 2i32 && s[2] == 1i32);
568    /// };
569    /// ```
570    #[trusted]
571    #[check(ghost)]
572    #[ensures(^self == self.push_front(x))]
573    pub fn push_front_ghost(&mut self, x: T) {
574        let _ = x;
575        panic!()
576    }
577
578    /// Appends an element to the back of a collection.
579    ///
580    /// # Example
581    /// ```rust,creusot
582    /// use creusot_std::prelude::*;
583    ///
584    /// let mut s = Seq::new();
585    /// ghost! {
586    ///     s.push_back_ghost(1);
587    ///     s.push_back_ghost(2);
588    ///     s.push_back_ghost(3);
589    ///     proof_assert!(s[0] == 1i32 && s[1] == 2i32 && s[2] == 3i32);
590    /// };
591    /// ```
592    #[trusted]
593    #[check(ghost)]
594    #[ensures(^self == self.push_back(x))]
595    pub fn push_back_ghost(&mut self, x: T) {
596        let _ = x;
597        panic!()
598    }
599
600    /// Returns a reference to an element at `index` or `None` if `index` is out of bounds.
601    ///
602    /// # Example
603    /// ```rust,creusot
604    /// use creusot_std::prelude::*;
605    ///
606    /// let mut s = Seq::new();
607    /// ghost! {
608    ///     s.push_back_ghost(10);
609    ///     s.push_back_ghost(40);
610    ///     s.push_back_ghost(30);
611    ///     let get1 = s.get_ghost(1int);
612    ///     let get2 = s.get_ghost(3int);
613    ///     proof_assert!(get1 == Some(&40i32));
614    ///     proof_assert!(get2 == None);
615    /// };
616    /// ```
617    #[trusted]
618    #[check(ghost)]
619    #[ensures(match self.get(index) {
620        None => result == None,
621        Some(v) => result == Some(&v),
622    })]
623    pub fn get_ghost(&self, index: Int) -> Option<&T> {
624        let _ = index;
625        panic!()
626    }
627
628    /// Returns a mutable reference to an element at `index` or `None` if `index` is out of bounds.
629    ///
630    /// # Example
631    /// ```rust,creusot
632    /// use creusot_std::prelude::*;
633    ///
634    /// let mut s = Seq::new();
635    ///
636    /// ghost! {
637    ///     s.push_back_ghost(0);
638    ///     s.push_back_ghost(1);
639    ///     s.push_back_ghost(2);
640    ///     if let Some(elem) = s.get_mut_ghost(1int) {
641    ///         *elem = 42;
642    ///     }
643    ///     proof_assert!(s[0] == 0i32 && s[1] == 42i32 && s[2] == 2i32);
644    /// };
645    /// ```
646    #[trusted]
647    #[check(ghost)]
648    #[ensures(match result {
649        None => self.get(index) == None && *self == ^self,
650        Some(r) => self.get(index) == Some(*r) && ^r == (^self)[index],
651    })]
652    #[ensures(forall<i> i != index ==> (*self).get(i) == (^self).get(i))]
653    #[ensures((*self).len() == (^self).len())]
654    pub fn get_mut_ghost(&mut self, index: Int) -> Option<&mut T> {
655        let _ = index;
656        panic!()
657    }
658
659    /// Removes the last element from a vector and returns it, or `None` if it is empty.
660    ///
661    /// # Example
662    /// ```rust,creusot
663    /// use creusot_std::prelude::*;
664    ///
665    /// let mut s = Seq::new();
666    /// ghost! {
667    ///     s.push_back_ghost(1);
668    ///     s.push_back_ghost(2);
669    ///     s.push_back_ghost(3);
670    ///     let popped = s.pop_back_ghost();
671    ///     proof_assert!(popped == Some(3i32));
672    ///     proof_assert!(s[0] == 1i32 && s[1] == 2i32);
673    /// };
674    /// ```
675    #[trusted]
676    #[check(ghost)]
677    #[ensures(match result {
678        None => *self == Seq::empty() && *self == ^self,
679        Some(r) => *self == (^self).push_back(r)
680    })]
681    pub fn pop_back_ghost(&mut self) -> Option<T> {
682        panic!()
683    }
684
685    /// Removes the first element from a vector and returns it, or `None` if it is empty.
686    ///
687    /// # Example
688    /// ```rust,creusot
689    /// use creusot_std::prelude::*;
690    ///
691    /// let mut s = Seq::new();
692    /// ghost! {
693    ///     s.push_back_ghost(1);
694    ///     s.push_back_ghost(2);
695    ///     s.push_back_ghost(3);
696    ///     let popped = s.pop_front_ghost();
697    ///     proof_assert!(popped == Some(1i32));
698    ///     proof_assert!(s[0] == 2i32 && s[1] == 3i32);
699    /// };
700    /// ```
701    #[trusted]
702    #[check(ghost)]
703    #[ensures(match result {
704        None => *self == Seq::empty() && *self == ^self,
705        Some(r) => (*self).len() > 0 && r == (*self)[0] && ^self == (*self).tail()
706    })]
707    pub fn pop_front_ghost(&mut self) -> Option<T> {
708        panic!()
709    }
710
711    /// Clears the sequence, removing all values.
712    ///
713    /// # Example
714    /// ```rust,creusot
715    /// use creusot_std::prelude::*;
716    ///
717    /// let mut s = Seq::new();
718    /// ghost! {
719    ///     s.push_back_ghost(1);
720    ///     s.push_back_ghost(2);
721    ///     s.push_back_ghost(3);
722    ///     s.clear_ghost();
723    ///     proof_assert!(s == Seq::empty());
724    /// };
725    /// ```
726    #[trusted]
727    #[check(ghost)]
728    #[ensures(^self == Self::empty())]
729    pub fn clear_ghost(&mut self) {}
730
731    /// Split a sequence in two at the given index.
732    #[trusted]
733    #[check(ghost)]
734    #[requires(0 <= mid && mid <= self.len())]
735    #[ensures((^self).len() == mid)]
736    #[ensures((^self).concat(result) == *self)]
737    pub fn split_off_ghost(&mut self, mid: Int) -> Self {
738        let _ = mid;
739        panic!("ghost code")
740    }
741}
742
743impl<T> core::ops::Index<Int> for Seq<T> {
744    type Output = T;
745
746    #[check(ghost)]
747    #[requires(0 <= index && index < self.len())]
748    #[ensures(*result == self[index])]
749    fn index(&self, index: Int) -> &Self::Output {
750        self.get_ghost(index).unwrap()
751    }
752}
753impl<T> core::ops::IndexMut<Int> for Seq<T> {
754    #[check(ghost)]
755    #[requires(0 <= index && index < self.len())]
756    #[ensures((*self).len() == (^self).len())]
757    #[ensures(*result == (*self)[index] && ^result == (^self)[index])]
758    #[ensures(forall<i> i != index ==> (*self).get(i) == (^self).get(i))]
759    fn index_mut(&mut self, index: Int) -> &mut Self::Output {
760        self.get_mut_ghost(index).unwrap()
761    }
762}
763
764impl<T> core::ops::Index<(Int, Int)> for Seq<T> {
765    type Output = (T, T);
766
767    #[trusted]
768    #[check(ghost)]
769    #[requires(0 <= index.0 && index.0 < self.len() && 0 <= index.1 && index.1 < self.len())]
770    #[ensures(result.0 == self[index.0] && result.1 == self[index.1])]
771    #[allow(unused_variables)]
772    fn index(&self, index: (Int, Int)) -> &Self::Output {
773        panic!()
774    }
775}
776
777impl<T> core::ops::IndexMut<(Int, Int)> for Seq<T> {
778    #[trusted]
779    #[check(ghost)]
780    #[requires(0 <= index.0 && index.0 < self.len() && 0 <= index.1 && index.1 < self.len())]
781    #[requires(index.0 != index.1)]
782    #[ensures((*result).0 == (*self)[index.0] && (*result).1 == (*self)[index.1]
783           && (^result).0 == (^self)[index.0] && (^result).1 == (^self)[index.1])]
784    #[ensures(forall<i> i != index.0 && i != index.1 ==> (*self).get(i) == (^self).get(i))]
785    #[ensures((*self).len() == (^self).len())]
786    #[allow(unused_variables)]
787    fn index_mut(&mut self, index: (Int, Int)) -> &mut Self::Output {
788        panic!()
789    }
790}
791
792// Having `Copy` guarantees that the operation is pure, even if we decide to change the definition of `Clone`.
793impl<T: Clone + Copy> Clone for Seq<T> {
794    #[trusted]
795    #[check(ghost)]
796    #[ensures(result == *self)]
797    fn clone(&self) -> Self {
798        *self
799    }
800}
801
802impl<T: Copy> Copy for Seq<T> {}
803#[trusted]
804impl<T: Plain> Plain for Seq<T> {}
805
806impl<T> Invariant for Seq<T> {
807    #[logic(open, prophetic, inline)]
808    #[creusot::trusted_trivial_if_param_trivial]
809    fn invariant(self) -> bool {
810        pearlite! { forall<i> 0 <= i && i < self.len() ==> inv(self.index_logic_unsized(i)) }
811    }
812}
813
814// =========
815// Iterators
816// =========
817
818impl<T> IntoIterator for Seq<T> {
819    type Item = T;
820    type IntoIter = SeqIter<T>;
821
822    #[check(ghost)]
823    #[ensures(result@ == self)]
824    fn into_iter(self) -> SeqIter<T> {
825        SeqIter { inner: self }
826    }
827}
828
829/// An owning iterator for [`Seq`].
830///
831/// # Ghost code and variants
832///
833/// This iterator is only obtainable in ghost code.
834///
835/// To use it in a `for` loop, a variant must be declared:
836/// ```rust,creusot
837/// # use creusot_std::prelude::*;
838/// # #[requires(true)]
839/// fn iter_on_seq<T>(s: Seq<T>) {
840///     let len = snapshot!(s.len());
841///     #[variant(len - produced.len())]
842///     for i in s {
843///         // ...
844///     }
845/// }
846/// ```
847pub struct SeqIter<T> {
848    inner: Seq<T>,
849}
850
851impl<T> View for SeqIter<T> {
852    type ViewTy = Seq<T>;
853    #[logic]
854    fn view(self) -> Seq<T> {
855        self.inner
856    }
857}
858
859impl<T> Iterator for SeqIter<T> {
860    type Item = T;
861
862    #[check(ghost)]
863    #[ensures(match result {
864        None => self.completed(),
865        Some(v) => (*self).produces(Seq::singleton(v), ^self)
866    })]
867    fn next(&mut self) -> Option<T> {
868        self.inner.pop_front_ghost()
869    }
870}
871
872impl<T> IteratorSpec for SeqIter<T> {
873    #[logic(prophetic, open)]
874    fn produces(self, visited: Seq<T>, o: Self) -> bool {
875        pearlite! { self@ == visited.concat(o@) }
876    }
877
878    #[logic(prophetic, open)]
879    fn completed(&mut self) -> bool {
880        pearlite! { self@ == Seq::empty() }
881    }
882
883    #[logic(law)]
884    #[ensures(self.produces(Seq::empty(), self))]
885    fn produces_refl(self) {}
886
887    #[logic(law)]
888    #[requires(a.produces(ab, b))]
889    #[requires(b.produces(bc, c))]
890    #[ensures(a.produces(ab.concat(bc), c))]
891    fn produces_trans(a: Self, ab: Seq<Self::Item>, b: Self, bc: Seq<Self::Item>, c: Self) {}
892}
893
894impl<'a, T> IntoIterator for &'a Seq<T> {
895    type Item = &'a T;
896    type IntoIter = SeqIterRef<'a, T>;
897
898    #[check(ghost)]
899    #[ensures(result@ == *self)]
900    fn into_iter(self) -> Self::IntoIter {
901        SeqIterRef { inner: self, index: self.len_ghost() - self.len_ghost() }
902    }
903}
904
905/// An iterator over references in a [`Seq`].
906pub struct SeqIterRef<'a, T> {
907    inner: &'a Seq<T>,
908    index: Int,
909}
910impl<T> Invariant for SeqIterRef<'_, T> {
911    #[logic]
912    fn invariant(self) -> bool {
913        0 <= self.index && self.index <= self.inner.len()
914    }
915}
916
917impl<T> View for SeqIterRef<'_, T> {
918    type ViewTy = Seq<T>;
919    #[logic]
920    fn view(self) -> Seq<T> {
921        self.inner.subsequence(self.index, self.inner.len())
922    }
923}
924
925impl<'a, T> Iterator for SeqIterRef<'a, T> {
926    type Item = &'a T;
927
928    #[check(ghost)]
929    #[ensures(match result {
930        None => self.completed(),
931        Some(v) => (*self).produces(Seq::singleton(v), ^self)
932    })]
933    fn next(&mut self) -> Option<&'a T> {
934        let _before = snapshot!((*self)@);
935        if let Some(res) = self.inner.get_ghost(self.index) {
936            self.index.incr_ghost();
937            proof_assert!((*self)@ == _before.tail());
938            Some(res)
939        } else {
940            proof_assert!(self.index == self.inner.len());
941            proof_assert!(self@ == Seq::empty());
942            None
943        }
944    }
945}
946impl<'a, T> IteratorSpec for SeqIterRef<'a, T> {
947    #[logic(prophetic, open)]
948    fn produces(self, visited: Seq<&'a T>, o: Self) -> bool {
949        let visited: Seq<T> = visited.to_owned_seq();
950        pearlite! { self@ == visited.concat(o@) }
951    }
952
953    #[logic(prophetic, open)]
954    fn completed(&mut self) -> bool {
955        pearlite! { self@ == Seq::empty() }
956    }
957
958    #[logic(law)]
959    #[ensures(self.produces(Seq::empty(), self))]
960    fn produces_refl(self) {}
961
962    #[logic(law)]
963    #[requires(a.produces(ab, b))]
964    #[requires(b.produces(bc, c))]
965    #[ensures(a.produces(ab.concat(bc), c))]
966    fn produces_trans(a: Self, ab: Seq<Self::Item>, b: Self, bc: Seq<Self::Item>, c: Self) {}
967}
968
969impl<T> Resolve for Seq<T> {
970    #[logic(open, prophetic)]
971    #[creusot::trusted_trivial_if_param_trivial]
972    fn resolve(self) -> bool {
973        pearlite! { forall<i : Int> resolve(self.get(i)) }
974    }
975
976    #[trusted]
977    #[logic(open(self), prophetic)]
978    #[requires(structural_resolve(self))]
979    #[ensures(self.resolve())]
980    fn resolve_coherence(self) {}
981}
982
983impl<T> Resolve for SeqIter<T> {
984    #[logic(open, prophetic, inline)]
985    #[creusot::trusted_trivial_if_param_trivial]
986    fn resolve(self) -> bool {
987        pearlite! { resolve(self@) }
988    }
989
990    #[logic(open, prophetic)]
991    #[requires(structural_resolve(self))]
992    #[ensures(self.resolve())]
993    fn resolve_coherence(self) {}
994}
995
996// Some properties
997// TODO : use parameters instead of quantification, and mode to impl block
998
999#[logic(open)]
1000#[ensures(forall<x: A, f: Mapping<A, Seq<B>>> Seq::singleton(x).flat_map(f) == f.get(x))]
1001pub fn flat_map_singleton<A, B>() {}
1002
1003#[logic(open)]
1004#[ensures(forall<x: A, f: Mapping<A, Seq<B>>> xs.push_back(x).flat_map(f) == xs.flat_map(f).concat(f.get(x)))]
1005#[variant(xs.len())]
1006pub fn flat_map_push_back<A, B>(xs: Seq<A>) {
1007    if xs.len() > 0 {
1008        flat_map_push_back::<A, B>(xs.tail());
1009        proof_assert! { forall<x: A> xs.tail().push_back(x) == xs.push_back(x).tail() }
1010    }
1011}
creusot_std/logic/seq.rs

creusot_std/logic/
seq.rs
