creusot_contracts/logic/
fset.rs

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

creusot_contracts/logic/
fset.rs
