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_logic(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 add(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_logic(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().add(x)
185    }
186
187    /// Returns the union of sets `f(t)` over all `t: T`.
188    #[logic(opaque)]
189    #[ensures(forall<y: U> #[trigger(result.contains(&y))]
190        result.contains(&y) == exists<x: T> self.contains(&x) && f.get(x).contains(&y))]
191    #[variant(self.len())]
192    pub fn unions<U>(self, f: Mapping<T, FSet<U>>) -> FSet<U> {
193        if self.len() == 0 {
194            FSet::empty()
195        } else {
196            let x = self.peek();
197            f.get(x).union(self.remove(x).unions(f))
198        }
199    }
200
201    /// Flipped `map`.
202    #[logic]
203    #[builtin("set.Fset.map")]
204    pub fn fmap<U>(_: Mapping<T, U>, _: Self) -> FSet<U> {
205        dead
206    }
207
208    /// Returns the image of a set by a function.
209    #[logic(open)]
210    pub fn map<U>(self, f: Mapping<T, U>) -> FSet<U> {
211        FSet::fmap(f, self)
212    }
213
214    /// Returns the subset of elements of `self` which satisfy the predicate `f`.
215    #[logic]
216    #[builtin("set.Fset.filter")]
217    pub fn filter(self, f: Mapping<T, bool>) -> Self {
218        let _ = f;
219        dead
220    }
221
222    /// Returns the set of sequences whose head is in `s` and whose tail is in `ss`.
223    #[logic(open)]
224    #[ensures(forall<xs: Seq<T>> result.contains(&xs) == (0 < xs.len() && s.contains(&xs[0]) && ss.contains(&xs.tail())))]
225    pub fn cons(s: FSet<T>, ss: FSet<Seq<T>>) -> FSet<Seq<T>> {
226        proof_assert!(forall<x:T, xs: Seq<T>> xs.cons(x).tail() == xs);
227        proof_assert!(forall<xs: Seq<T>> 0 < xs.len() ==> xs.tail().cons(xs[0]) == xs);
228        s.unions(|x| ss.map(|xs: Seq<_>| xs.cons(x)))
229    }
230
231    /// Returns the set of concatenations of a sequence in `s` and a sequence in `t`.
232    #[logic(open)]
233    #[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)))]
234    pub fn concat(s: FSet<Seq<T>>, t: FSet<Seq<T>>) -> FSet<Seq<T>> {
235        s.unions(|ys: Seq<_>| t.map(|zs| ys.concat(zs)))
236    }
237
238    /// Returns the set of sequences of length `n` whose elements are in `self`.
239    #[logic(open)]
240    #[requires(n >= 0)]
241    #[ensures(forall<xs: Seq<T>> result.contains(&xs) == (xs.len() == n && forall<x: T> xs.contains(x) ==> self.contains(&x)))]
242    #[variant(n)]
243    pub fn replicate(self, n: Int) -> FSet<Seq<T>> {
244        pearlite! {
245            if n == 0 {
246                proof_assert! { forall<xs: Seq<T>> xs.len() == 0 ==> xs == Seq::empty() };
247                FSet::singleton(Seq::empty())
248            } else {
249                proof_assert! { forall<xs: Seq<T>, i> 0 < i && i < xs.len() ==> xs[i] == xs.tail()[i-1] };
250                FSet::cons(self, self.replicate(n - 1))
251            }
252        }
253    }
254
255    /// Returns the set of sequences of length at most `n` whose elements are in `self`.
256    #[logic(open)]
257    #[requires(n >= 0)]
258    #[ensures(forall<xs: Seq<T>> result.contains(&xs) == (xs.len() <= n && forall<x: T> xs.contains(x) ==> self.contains(&x)))]
259    #[variant(n)]
260    pub fn replicate_up_to(self, n: Int) -> FSet<Seq<T>> {
261        pearlite! {
262            if n == 0 {
263                proof_assert! { forall<xs: Seq<T>> xs.len() == 0 ==> xs == Seq::empty() };
264                FSet::singleton(Seq::empty())
265            } else {
266                self.replicate_up_to(n - 1).union(self.replicate(n))
267            }
268        }
269    }
270
271    /// Distributivity of `unions` over `union`.
272    #[logic]
273    #[ensures(self.union(other).unions(f) == self.unions(f).union(other.unions(f)))]
274    #[ensures(self.unions(|x| f.get(x).union(g.get(x))) == self.unions(f).union(self.unions(g)))]
275    pub fn unions_union<U>(self, other: Self, f: Mapping<T, FSet<U>>, g: Mapping<T, FSet<U>>) {}
276
277    /// Distributivity of `map` over `union`.
278    #[logic]
279    #[ensures(self.union(other).map(f) == self.map(f).union(other.map(f)))]
280    pub fn map_union<U>(self, other: Self, f: Mapping<T, U>) {}
281
282    /// Distributivity of `concat` over `union`.
283    #[logic]
284    #[ensures(FSet::concat(s1.union(s2), t) == FSet::concat(s1, t).union(FSet::concat(s2, t)))]
285    #[ensures(FSet::concat(t, s1.union(s2)) == FSet::concat(t, s1).union(FSet::concat(t, s2)))]
286    pub fn concat_union(s1: FSet<Seq<T>>, s2: FSet<Seq<T>>, t: FSet<Seq<T>>) {}
287
288    /// Distributivity of `cons` over `union`.
289    #[logic]
290    #[ensures(FSet::concat(FSet::cons(self, t), u) == FSet::cons(self, FSet::concat(t, u)))]
291    pub fn cons_concat(self, t: FSet<Seq<T>>, u: FSet<Seq<T>>) {
292        proof_assert!(forall<x: T, xs: Seq<T>, ys: Seq<T>> xs.cons(x).concat(ys) == xs.concat(ys).cons(x));
293        proof_assert!(forall<x: T, ys: Seq<T>> ys.cons(x).tail() == ys);
294        proof_assert!(forall<ys: Seq<T>> 0 < ys.len() ==> ys == ys.tail().cons(ys[0]));
295        proof_assert!(forall<xs> FSet::concat(FSet::cons(self, t), u).contains(xs) ==
296                                 FSet::cons(self, FSet::concat(t, u)).contains(xs));
297    }
298
299    /// Distributivity of `replicate` over `union`.
300    #[logic]
301    #[requires(0 <= n && 0 <= m)]
302    #[ensures(self.replicate(n + m) == FSet::concat(self.replicate(n), self.replicate(m)))]
303    #[variant(n)]
304    pub fn concat_replicate(self, n: Int, m: Int) {
305        pearlite! {
306            if n == 0 {
307                Self::concat_empty(self.replicate(m));
308            } else {
309                self.cons_concat(self.replicate(n - 1), self.replicate(m));
310                self.concat_replicate(n - 1, m);
311            }
312        }
313    }
314
315    /// The neutral element of `FSet::concat` is `FSet::singleton(Seq::empty())`.
316    #[logic]
317    #[ensures(FSet::concat(FSet::singleton(Seq::empty()), s) == s)]
318    #[ensures(FSet::concat(s, FSet::singleton(Seq::empty())) == s)]
319    pub fn concat_empty(s: FSet<Seq<T>>) {
320        proof_assert!(forall<xs: Seq<T>> xs.concat(Seq::empty()) == xs);
321        proof_assert!(forall<xs: Seq<T>> Seq::empty().concat(xs) == xs);
322    }
323
324    /// An equation relating `s.replicate_up_to(m)` and `s.replicate_up_to(n)`.
325    #[logic]
326    #[requires(0 <= n && n < m)]
327    #[ensures(self.replicate_up_to(m) == self.replicate_up_to(n).union(
328        FSet::concat(self.replicate(n + 1), self.replicate_up_to(m - n - 1))))]
329    #[variant(m)]
330    pub fn concat_replicate_up_to(self, n: Int, m: Int) {
331        pearlite! {
332            if n + 1 == m {
333                Self::concat_empty(self.replicate(n + 1));
334            } else {
335                Self::concat_union(self.replicate(n), self.replicate(m - 1), self.replicate(m - n - 1));
336                self.concat_replicate(n, m - n - 1);
337                self.concat_replicate_up_to(n, m - 1);
338            }
339        }
340    }
341}
342
343impl FSet<Int> {
344    /// Return the interval of integers in `[i, j)`.
345    #[logic(open)]
346    #[builtin("set.FsetInt.interval")]
347    pub fn interval(i: Int, j: Int) -> FSet<Int> {
348        let _ = (i, j);
349        dead
350    }
351}
352
353/// Ghost definitions
354impl<T> FSet<T> {
355    /// Create a new, empty set on the ghost heap.
356    #[trusted]
357    #[check(ghost)]
358    #[ensures(result.is_empty())]
359    #[allow(unreachable_code)]
360    pub fn new() -> Ghost<Self> {
361        Ghost::conjure()
362    }
363
364    /// Returns the number of elements in the set.
365    ///
366    /// If you need to get the length in pearlite, consider using [`len`](Self::len).
367    ///
368    /// # Example
369    /// ```rust,creusot
370    /// use creusot_std::{logic::FSet, prelude::*};
371    ///
372    /// let mut set = FSet::new();
373    /// ghost! {
374    ///     let len1 = set.len();
375    ///     set.insert(1);
376    ///     set.insert(2);
377    ///     set.insert(1);
378    ///     let len2 = set.len();
379    ///     proof_assert!(len1 == 0);
380    ///     proof_assert!(len2 == 2);
381    /// };
382    /// ```
383    #[trusted]
384    #[check(ghost)]
385    #[logic_alias(self.len_logic())]
386    pub fn len(&self) -> Int {
387        panic!()
388    }
389
390    /// Returns true if the set contains the specified value.
391    ///
392    /// # Example
393    /// ```rust,creusot
394    /// use creusot_std::{logic::FSet, prelude::*};
395    ///
396    /// let mut set = FSet::new();
397    /// ghost! {
398    ///     set.insert(1);
399    ///     let (b1, b2) = (set.contains(&1), set.contains(&2));
400    ///     proof_assert!(b1);
401    ///     proof_assert!(!b2);
402    /// };
403    /// ```
404    #[trusted]
405    #[check(ghost)]
406    //#[logic_alias(Self::contains(*self, *value))]
407    #[logic_alias(self.contains_logic(*value))]
408    pub fn contains(&self, value: &T) -> bool {
409        let _ = value;
410        panic!()
411    }
412
413    /// Adds a value to the set.
414    ///
415    /// Returns whether the value was newly inserted. That is:
416    /// - If the set did not previously contain this value, `true` is returned.
417    /// - If the set already contained this value, `false` is returned, and the set is
418    ///   not modified: original value is not replaced, and the value passed as argument
419    ///   is dropped.
420    ///
421    /// # Example
422    /// ```rust,creusot
423    /// use creusot_std::{logic::FSet, prelude::*};
424    ///
425    /// let mut set = FSet::new();
426    /// ghost! {
427    ///     let res1 = set.insert(42);
428    ///     proof_assert!(res1);
429    ///     proof_assert!(set.contains(42i32));
430    ///
431    ///     let res2 = set.insert(41);
432    ///     let res3 = set.insert(42);
433    ///     proof_assert!(res2);
434    ///     proof_assert!(!res3);
435    ///     proof_assert!(set.len() == 2);
436    /// };
437    /// ```
438    #[trusted]
439    #[check(ghost)]
440    #[ensures(^self == (*self).add(value))]
441    #[ensures(result == !(*self).contains(&value))]
442    pub fn insert(&mut self, value: T) -> bool {
443        let _ = value;
444        panic!()
445    }
446
447    /// Removes a value from the set. Returns whether the value was present in the set.
448    ///
449    /// # Example
450    /// ```rust,creusot
451    /// use creusot_std::{logic::FSet, prelude::*};
452    ///
453    /// let mut set = FSet::new();
454    /// let res = ghost! {
455    ///     set.insert(1);
456    ///     let res1 = set.delete(&1);
457    ///     let res2 = set.delete(&1);
458    ///     proof_assert!(res1 && !res2);
459    /// };
460    /// ```
461    #[trusted]
462    #[check(ghost)]
463    #[ensures(^self == (*self).remove(*value))]
464    #[ensures(result == (*self).contains(value))]
465    pub fn delete(&mut self, value: &T) -> bool {
466        let _ = value;
467        panic!()
468    }
469
470    /// Clears the set, removing all values.
471    ///
472    /// # Example
473    /// ```rust,creusot
474    /// use creusot_std::{prelude::*, logic::FSet};
475    ///
476    /// let mut s = FSet::new();
477    /// ghost! {
478    ///     s.insert(1);
479    ///     s.insert(2);
480    ///     s.insert(3);
481    ///     s.clear();
482    ///     proof_assert!(s == FSet::empty());
483    /// };
484    /// ```
485    #[trusted]
486    #[check(ghost)]
487    #[ensures(^self == Self::empty())]
488    pub fn clear(&mut self) {}
489}
490
491impl<T: Clone + Copy> Clone for FSet<T> {
492    #[trusted]
493    #[check(ghost)]
494    #[ensures(result == *self)]
495    fn clone(&self) -> Self {
496        *self
497    }
498}
499
500// Having `Copy` guarantees that the operation is pure, even if we decide to change the definition of `Clone`.
501impl<T: Clone + Copy> Copy for FSet<T> {}
502
503impl<T> Invariant for FSet<T> {
504    #[logic(open, prophetic, inline)]
505    #[creusot::trusted_trivial_if_param_trivial]
506    fn invariant(self) -> bool {
507        pearlite! { forall<x: T> self.contains(&x) ==> inv(x) }
508    }
509}
510impl<T> Resolve for FSet<T> {
511    #[logic(open, prophetic)]
512    #[creusot::trusted_trivial_if_param_trivial]
513    fn resolve(self) -> bool {
514        pearlite! { forall<x: T> self.contains(&x) ==> resolve(x) }
515    }
516
517    #[trusted]
518    #[logic(open(self), prophetic)]
519    #[requires(structural_resolve(self))]
520    #[ensures(self.resolve())]
521    fn resolve_coherence(self) {}
522}
creusot_std/logic/fset.rs

creusot_std/logic/
fset.rs
