creusot_std/logic/
fset.rs

1//! A logical/ghost finite set.
2
3#[cfg(creusot)]
4use crate::resolve::structural_resolve;
5use crate::{logic::Mapping, prelude::*};
6use core::marker::PhantomData;
7
8/// A finite set type usable in pearlite and `ghost!` blocks.
9///
10/// If you need an infinite set, see [`Set`](super::Set).
11///
12/// # Ghost
13///
14/// Since [`std::collections::HashSet`] and
15/// [`std::collections::BTreeSet`] have finite
16/// capacity, this could cause some issues in ghost code:
17/// ```rust,creusot,compile_fail
18/// ghost! {
19///     let mut set = HashSet::new();
20///     for _ in 0..=usize::MAX as u128 + 1 {
21///         set.insert(0); // cannot fail, since we are in a ghost block
22///     }
23///     proof_assert!(set.len() <= usize::MAX@); // by definition
24///     proof_assert!(set.len() > usize::MAX@); // uh-oh
25/// }
26/// ```
27///
28/// This type is designed for this use-case, with no restriction on the capacity.
29#[opaque]
30#[builtin("set.Fset.fset")]
31pub struct FSet<T>(PhantomData<T>);
32
33impl<T> FSet<T> {
34    /// Returns the empty set.
35    #[logic]
36    #[builtin("set.Fset.empty", ascription)]
37    pub fn empty() -> Self {
38        dead
39    }
40
41    /// Returns `true` if `e` is in the set.
42    #[logic(open, inline)]
43    pub fn contains(self, e: T) -> bool {
44        Self::mem(e, self)
45    }
46
47    /// [`Self::contains`], but with the order of arguments flipped.
48    ///
49    /// This is how the function is defined in why3.
50    #[doc(hidden)]
51    #[logic]
52    #[builtin("set.Fset.mem")]
53    pub fn mem(_: T, _: Self) -> bool {
54        dead
55    }
56
57    /// Returns a new set, where `e` has been added if it was not present.
58    #[logic(open, inline)]
59    pub fn insert(self, e: T) -> Self {
60        Self::add(e, self)
61    }
62
63    /// [`Self::insert`], but with the order of arguments flipped.
64    ///
65    /// This is how the function is defined in why3.
66    #[doc(hidden)]
67    #[logic]
68    #[builtin("set.Fset.add")]
69    pub fn add(_: T, _: Self) -> Self {
70        dead
71    }
72
73    /// Returns `true` if the set contains no elements.
74    #[logic]
75    #[builtin("set.Fset.is_empty")]
76    pub fn is_empty(self) -> bool {
77        dead
78    }
79
80    /// Returns a new set, where `e` is no longer present.
81    #[logic(open, inline)]
82    pub fn remove(self, e: T) -> Self {
83        Self::rem(e, self)
84    }
85
86    /// [`Self::remove`], but with the order of arguments flipped.
87    ///
88    /// This is how the function is defined in why3.
89    #[doc(hidden)]
90    #[logic]
91    #[builtin("set.Fset.remove")]
92    pub fn rem(_: T, _: Self) -> Self {
93        dead
94    }
95
96    /// Returns a new set, which is the union of `self` and `other`.
97    ///
98    /// An element is in the result if it is in `self` _or_ if it is in `other`.
99    #[logic]
100    #[builtin("set.Fset.union")]
101    pub fn union(self, other: Self) -> Self {
102        let _ = other;
103        dead
104    }
105
106    /// Returns a new set, which is the union of `self` and `other`.
107    ///
108    /// An element is in the result if it is in `self` _or_ if it is in `other`.
109    #[logic]
110    #[builtin("set.Fset.inter")]
111    pub fn intersection(self, other: Self) -> Self {
112        let _ = other;
113        dead
114    }
115
116    /// Returns a new set, which is the difference of `self` with `other`.
117    ///
118    /// An element is in the result if and only if it is in `self` but not in `other`.
119    #[logic]
120    #[builtin("set.Fset.diff")]
121    pub fn difference(self, other: Self) -> Self {
122        let _ = other;
123        dead
124    }
125
126    /// Returns `true` if every element of `self` is in `other`.
127    #[logic]
128    #[builtin("set.Fset.subset")]
129    pub fn is_subset(self, other: Self) -> bool {
130        let _ = other;
131        dead
132    }
133
134    /// Returns `true` if every element of `other` is in `self`.
135    #[logic(open, inline)]
136    pub fn is_superset(self, other: Self) -> bool {
137        Self::is_subset(other, self)
138    }
139
140    /// Returns `true` if `self` and `other` are disjoint.
141    #[logic]
142    #[builtin("set.Fset.disjoint")]
143    pub fn disjoint(self, other: Self) -> bool {
144        let _ = other;
145        dead
146    }
147
148    /// Returns the number of elements in the set, also called its length.
149    #[logic]
150    #[builtin("set.Fset.cardinal")]
151    pub fn len(self) -> Int {
152        dead
153    }
154
155    /// Get an arbitrary element of the set.
156    ///
157    /// # Returns
158    ///
159    /// - If the set is nonempty, the result is guaranteed to be in the set
160    /// - If the set is empty, the result is unspecified
161    #[logic]
162    #[builtin("set.Fset.pick")]
163    pub fn peek(self) -> T {
164        dead
165    }
166
167    /// Extensional equality
168    ///
169    /// Returns `true` if `self` and `other` contain exactly the same elements.
170    ///
171    /// This is in fact equivalent with normal equality.
172    #[logic(open)]
173    #[ensures(#[trigger(self == other)] result == (self == other))]
174    pub fn ext_eq(self, other: Self) -> bool {
175        pearlite! {
176            forall <e: T> self.contains(e) == other.contains(e)
177        }
178    }
179
180    /// Returns the set containing only `x`.
181    #[logic(open)]
182    #[ensures(forall<y: T> result.contains(y) == (x == y))]
183    pub fn singleton(x: T) -> Self {
184        FSet::empty().insert(x)
185    }
186
187    /// Returns the union of sets `f(t)` over all `t: T`.
188    #[logic(open)]
189    #[ensures(forall<y: U> result.contains(y) == exists<x: T> self.contains(x) && f.get(x).contains(y))]
190    #[variant(self.len())]
191    pub fn unions<U>(self, f: Mapping<T, FSet<U>>) -> FSet<U> {
192        if self.len() == 0 {
193            FSet::empty()
194        } else {
195            let x = self.peek();
196            f.get(x).union(self.remove(x).unions(f))
197        }
198    }
199
200    /// Flipped `map`.
201    #[logic]
202    #[builtin("set.Fset.map")]
203    pub fn fmap<U>(_: Mapping<T, U>, _: Self) -> FSet<U> {
204        dead
205    }
206
207    /// Returns the image of a set by a function.
208    #[logic(open)]
209    pub fn map<U>(self, f: Mapping<T, U>) -> FSet<U> {
210        FSet::fmap(f, self)
211    }
212
213    /// Returns the subset of elements of `self` which satisfy the predicate `f`.
214    #[logic]
215    #[builtin("set.Fset.filter")]
216    pub fn filter(self, f: Mapping<T, bool>) -> Self {
217        let _ = f;
218        dead
219    }
220
221    /// Returns the set of sequences whose head is in `s` and whose tail is in `ss`.
222    #[logic(open)]
223    #[ensures(forall<xs: Seq<T>> result.contains(xs) == (0 < xs.len() && s.contains(xs[0]) && ss.contains(xs.tail())))]
224    pub fn cons(s: FSet<T>, ss: FSet<Seq<T>>) -> FSet<Seq<T>> {
225        proof_assert!(forall<x:T, xs: Seq<T>> xs.push_front(x).tail() == xs);
226        proof_assert!(forall<xs: Seq<T>> 0 < xs.len() ==> xs.tail().push_front(xs[0]) == xs);
227        s.unions(|x| ss.map(|xs: Seq<_>| xs.push_front(x)))
228    }
229
230    /// Returns the set of concatenations of a sequence in `s` and a sequence in `t`.
231    #[logic(open)]
232    #[ensures(forall<xs: Seq<T>> result.contains(xs) == (exists<ys: Seq<T>, zs: Seq<T>> s.contains(ys) && t.contains(zs) && xs == ys.concat(zs)))]
233    pub fn concat(s: FSet<Seq<T>>, t: FSet<Seq<T>>) -> FSet<Seq<T>> {
234        s.unions(|ys: Seq<_>| t.map(|zs| ys.concat(zs)))
235    }
236
237    /// Returns the set of sequences of length `n` whose elements are in `self`.
238    #[logic(open)]
239    #[requires(n >= 0)]
240    #[ensures(forall<xs: Seq<T>> result.contains(xs) == (xs.len() == n && forall<x: T> xs.contains(x) ==> self.contains(x)))]
241    #[variant(n)]
242    pub fn replicate(self, n: Int) -> FSet<Seq<T>> {
243        pearlite! {
244            if n == 0 {
245                proof_assert! { forall<xs: Seq<T>> xs.len() == 0 ==> xs == Seq::empty() };
246                FSet::singleton(Seq::empty())
247            } else {
248                proof_assert! { forall<xs: Seq<T>, i> 0 < i && i < xs.len() ==> xs[i] == xs.tail()[i-1] };
249                FSet::cons(self, self.replicate(n - 1))
250            }
251        }
252    }
253
254    /// Returns the set of sequences of length at most `n` whose elements are in `self`.
255    #[logic(open)]
256    #[requires(n >= 0)]
257    #[ensures(forall<xs: Seq<T>> result.contains(xs) == (xs.len() <= n && forall<x: T> xs.contains(x) ==> self.contains(x)))]
258    #[variant(n)]
259    pub fn replicate_up_to(self, n: Int) -> FSet<Seq<T>> {
260        pearlite! {
261            if n == 0 {
262                proof_assert! { forall<xs: Seq<T>> xs.len() == 0 ==> xs == Seq::empty() };
263                FSet::singleton(Seq::empty())
264            } else {
265                self.replicate_up_to(n - 1).union(self.replicate(n))
266            }
267        }
268    }
269
270    /// Distributivity of `unions` over `union`.
271    #[logic]
272    #[ensures(self.union(other).unions(f) == self.unions(f).union(other.unions(f)))]
273    #[ensures(self.unions(|x| f.get(x).union(g.get(x))) == self.unions(f).union(self.unions(g)))]
274    pub fn unions_union<U>(self, other: Self, f: Mapping<T, FSet<U>>, g: Mapping<T, FSet<U>>) {}
275
276    /// Distributivity of `map` over `union`.
277    #[logic]
278    #[ensures(self.union(other).map(f) == self.map(f).union(other.map(f)))]
279    pub fn map_union<U>(self, other: Self, f: Mapping<T, U>) {}
280
281    /// Distributivity of `concat` over `union`.
282    #[logic]
283    #[ensures(FSet::concat(s1.union(s2), t) == FSet::concat(s1, t).union(FSet::concat(s2, t)))]
284    #[ensures(FSet::concat(t, s1.union(s2)) == FSet::concat(t, s1).union(FSet::concat(t, s2)))]
285    pub fn concat_union(s1: FSet<Seq<T>>, s2: FSet<Seq<T>>, t: FSet<Seq<T>>) {}
286
287    /// Distributivity of `cons` over `union`.
288    #[logic]
289    #[ensures(FSet::concat(FSet::cons(self, t), u) == FSet::cons(self, FSet::concat(t, u)))]
290    pub fn cons_concat(self, t: FSet<Seq<T>>, u: FSet<Seq<T>>) {
291        proof_assert!(forall<x: T, xs: Seq<T>, ys: Seq<T>> xs.push_front(x).concat(ys) == xs.concat(ys).push_front(x));
292        proof_assert!(forall<x: T, ys: Seq<T>> ys.push_front(x).tail() == ys);
293        proof_assert!(forall<ys: Seq<T>> 0 < ys.len() ==> ys == ys.tail().push_front(ys[0]));
294        proof_assert!(forall<xs> FSet::concat(FSet::cons(self, t), u).contains(xs) ==
295                                 FSet::cons(self, FSet::concat(t, u)).contains(xs));
296    }
297
298    /// Distributivity of `replicate` over `union`.
299    #[logic]
300    #[requires(0 <= n && 0 <= m)]
301    #[ensures(self.replicate(n + m) == FSet::concat(self.replicate(n), self.replicate(m)))]
302    #[variant(n)]
303    pub fn concat_replicate(self, n: Int, m: Int) {
304        pearlite! {
305            if n == 0 {
306                Self::concat_empty(self.replicate(m));
307            } else {
308                self.cons_concat(self.replicate(n - 1), self.replicate(m));
309                self.concat_replicate(n - 1, m);
310            }
311        }
312    }
313
314    /// The neutral element of `FSet::concat` is `FSet::singleton(Seq::empty())`.
315    #[logic]
316    #[ensures(FSet::concat(FSet::singleton(Seq::empty()), s) == s)]
317    #[ensures(FSet::concat(s, FSet::singleton(Seq::empty())) == s)]
318    pub fn concat_empty(s: FSet<Seq<T>>) {
319        proof_assert!(forall<xs: Seq<T>> xs.concat(Seq::empty()) == xs);
320        proof_assert!(forall<xs: Seq<T>> Seq::empty().concat(xs) == xs);
321    }
322
323    /// An equation relating `s.replicate_up_to(m)` and `s.replicate_up_to(n)`.
324    #[logic]
325    #[requires(0 <= n && n < m)]
326    #[ensures(self.replicate_up_to(m) == self.replicate_up_to(n).union(
327        FSet::concat(self.replicate(n + 1), self.replicate_up_to(m - n - 1))))]
328    #[variant(m)]
329    pub fn concat_replicate_up_to(self, n: Int, m: Int) {
330        pearlite! {
331            if n + 1 == m {
332                Self::concat_empty(self.replicate(n + 1));
333            } else {
334                Self::concat_union(self.replicate(n), self.replicate(m - 1), self.replicate(m - n - 1));
335                self.concat_replicate(n, m - n - 1);
336                self.concat_replicate_up_to(n, m - 1);
337            }
338        }
339    }
340}
341
342impl FSet<Int> {
343    /// Return the interval of integers in `[i, j)`.
344    #[logic(open)]
345    #[builtin("set.FsetInt.interval")]
346    pub fn interval(i: Int, j: Int) -> FSet<Int> {
347        let _ = (i, j);
348        dead
349    }
350}
351
352/// Ghost definitions
353impl<T> FSet<T> {
354    /// Create a new, empty set on the ghost heap.
355    #[trusted]
356    #[check(ghost)]
357    #[ensures(result.is_empty())]
358    #[allow(unreachable_code)]
359    pub fn new() -> Ghost<Self> {
360        Ghost::conjure()
361    }
362
363    /// Returns the number of elements in the set.
364    ///
365    /// If you need to get the length in pearlite, consider using [`len`](Self::len).
366    ///
367    /// # Example
368    /// ```rust,creusot
369    /// use creusot_std::{logic::FSet, prelude::*};
370    ///
371    /// let mut set = FSet::new();
372    /// ghost! {
373    ///     let len1 = set.len_ghost();
374    ///     set.insert_ghost(1);
375    ///     set.insert_ghost(2);
376    ///     set.insert_ghost(1);
377    ///     let len2 = set.len_ghost();
378    ///     proof_assert!(len1 == 0);
379    ///     proof_assert!(len2 == 2);
380    /// };
381    /// ```
382    #[trusted]
383    #[check(ghost)]
384    #[ensures(result == self.len())]
385    pub fn len_ghost(&self) -> Int {
386        panic!()
387    }
388
389    /// Returns true if the set contains the specified value.
390    ///
391    /// # Example
392    /// ```rust,creusot
393    /// use creusot_std::{logic::FSet, prelude::*};
394    ///
395    /// let mut set = FSet::new();
396    /// ghost! {
397    ///     set.insert_ghost(1);
398    ///     let (b1, b2) = (set.contains_ghost(&1), set.contains_ghost(&2));
399    ///     proof_assert!(b1);
400    ///     proof_assert!(!b2);
401    /// };
402    /// ```
403    #[trusted]
404    #[check(ghost)]
405    #[ensures(result == self.contains(*value))]
406    pub fn contains_ghost(&self, value: &T) -> bool {
407        let _ = value;
408        panic!()
409    }
410
411    /// Adds a value to the set.
412    ///
413    /// Returns whether the value was newly inserted. That is:
414    /// - If the set did not previously contain this value, `true` is returned.
415    /// - If the set already contained this value, `false` is returned, and the set is
416    ///   not modified: original value is not replaced, and the value passed as argument
417    ///   is dropped.
418    ///
419    /// # Example
420    /// ```rust,creusot
421    /// use creusot_std::{logic::FSet, prelude::*};
422    ///
423    /// let mut set = FSet::new();
424    /// ghost! {
425    ///     let res1 = set.insert_ghost(42);
426    ///     proof_assert!(res1);
427    ///     proof_assert!(set.contains(42i32));
428    ///
429    ///     let res2 = set.insert_ghost(41);
430    ///     let res3 = set.insert_ghost(42);
431    ///     proof_assert!(res2);
432    ///     proof_assert!(!res3);
433    ///     proof_assert!(set.len() == 2);
434    /// };
435    /// ```
436    #[trusted]
437    #[check(ghost)]
438    #[ensures(^self == (*self).insert(value))]
439    #[ensures(result == !(*self).contains(value))]
440    pub fn insert_ghost(&mut self, value: T) -> bool {
441        let _ = value;
442        panic!()
443    }
444
445    /// Removes a value from the set. Returns whether the value was present in the set.
446    ///
447    /// # Example
448    /// ```rust,creusot
449    /// use creusot_std::{logic::FSet, prelude::*};
450    ///
451    /// let mut set = FSet::new();
452    /// let res = ghost! {
453    ///     set.insert_ghost(1);
454    ///     let res1 = set.remove_ghost(&1);
455    ///     let res2 = set.remove_ghost(&1);
456    ///     proof_assert!(res1 && !res2);
457    /// };
458    /// ```
459    #[trusted]
460    #[check(ghost)]
461    #[ensures(^self == (*self).remove(*value))]
462    #[ensures(result == (*self).contains(*value))]
463    pub fn remove_ghost(&mut self, value: &T) -> bool {
464        let _ = value;
465        panic!()
466    }
467
468    /// Clears the set, removing all values.
469    ///
470    /// # Example
471    /// ```rust,creusot
472    /// use creusot_std::{prelude::*, logic::FSet};
473    ///
474    /// let mut s = FSet::new();
475    /// ghost! {
476    ///     s.insert_ghost(1);
477    ///     s.insert_ghost(2);
478    ///     s.insert_ghost(3);
479    ///     s.clear_ghost();
480    ///     proof_assert!(s == FSet::empty());
481    /// };
482    /// ```
483    #[trusted]
484    #[check(ghost)]
485    #[ensures(^self == Self::empty())]
486    pub fn clear_ghost(&mut self) {}
487}
488
489impl<T: Clone + Copy> Clone for FSet<T> {
490    #[trusted]
491    #[check(ghost)]
492    #[ensures(result == *self)]
493    fn clone(&self) -> Self {
494        *self
495    }
496}
497
498// Having `Copy` guarantees that the operation is pure, even if we decide to change the definition of `Clone`.
499impl<T: Clone + Copy> Copy for FSet<T> {}
500
501impl<T> Invariant for FSet<T> {
502    #[logic(open, prophetic, inline)]
503    #[creusot::trusted_trivial_if_param_trivial]
504    fn invariant(self) -> bool {
505        pearlite! { forall<x: T> self.contains(x) ==> inv(x) }
506    }
507}
508impl<T> Resolve for FSet<T> {
509    #[logic(open, prophetic)]
510    #[creusot::trusted_trivial_if_param_trivial]
511    fn resolve(self) -> bool {
512        pearlite! { forall<x: T> self.contains(x) ==> resolve(x) }
513    }
514
515    #[trusted]
516    #[logic(open(self), prophetic)]
517    #[requires(structural_resolve(self))]
518    #[ensures(self.resolve())]
519    fn resolve_coherence(self) {}
520}
creusot_std/logic/fset.rs

creusot_std/logic/
fset.rs
