creusot_std/logic/
seq.rs

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

creusot_std/logic/
seq.rs
