creusot_std/logic/
fmap.rs

1//! A logical/ghost finite map.
2
3#[cfg(creusot)]
4use crate::resolve::structural_resolve;
5use crate::{
6    logic::{FSet, Mapping, ops::IndexLogic},
7    prelude::*,
8};
9use core::marker::PhantomData;
10
11/// A finite map type usable in pearlite and `ghost!` blocks.
12///
13/// If you need an infinite map, see [`Mapping`].
14///
15/// # Ghost
16///
17/// Since [`std::collections::HashMap`] and [`std::collections::BTreeMap`] have
18/// finite capacity, this could cause some issues in ghost code:
19/// ```rust,creusot,compile_fail
20/// ghost! {
21///     let mut map = HashMap::new();
22///     for _ in 0..=usize::MAX as u128 + 1 {
23///         map.insert(0, 0); // cannot fail, since we are in a ghost block
24///     }
25///     proof_assert!(map.len() <= usize::MAX@); // by definition
26///     proof_assert!(map.len() > usize::MAX@); // uh-oh
27/// }
28/// ```
29///
30/// This type is designed for this use-case, with no restriction on the capacity.
31#[opaque]
32pub struct FMap<K, V>(PhantomData<K>, PhantomData<V>);
33
34/// Logical definitions
35impl<K, V> FMap<K, V> {
36    /// The actual content of the map: other methods are specified relative to this.
37    #[logic(opaque)]
38    pub fn to_mapping(self) -> Mapping<K, Option<V>> {
39        dead
40    }
41
42    /// Returns the empty map.
43    #[trusted]
44    #[logic(opaque)]
45    #[ensures(result.len() == 0)]
46    #[ensures(result.to_mapping() == Mapping::cst(None))]
47    pub fn empty() -> Self {
48        dead
49    }
50
51    /// The number of elements in the map, also called its length.
52    #[trusted]
53    #[logic(opaque)]
54    #[ensures(result >= 0)]
55    pub fn len(self) -> Int {
56        dead
57    }
58
59    /// Returns a new map, where the key-value pair `(k, v)` has been inserted.
60    #[trusted]
61    #[logic(opaque)]
62    #[ensures(result.to_mapping() == self.to_mapping().set(k, Some(v)))]
63    #[ensures(result.len() == if self.contains(k) { self.len() } else { self.len() + 1 })]
64    pub fn insert(self, k: K, v: V) -> Self {
65        dead
66    }
67
68    /// Returns the map where containing the only key-value pair `(k, v)`.
69    #[logic(open)]
70    pub fn singleton(k: K, v: V) -> Self {
71        Self::empty().insert(k, v)
72    }
73
74    /// Returns a new map, where the key `k` is no longer present.
75    #[trusted]
76    #[logic(opaque)]
77    #[ensures(result.to_mapping() == self.to_mapping().set(k, None))]
78    #[ensures(result.len() == if self.contains(k) {self.len() - 1} else {self.len()})]
79    pub fn remove(self, k: K) -> Self {
80        dead
81    }
82
83    /// Get the value associated with key `k` in the map.
84    ///
85    /// If no value is present, returns [`None`].
86    #[logic(open, inline)]
87    pub fn get(self, k: K) -> Option<V> {
88        self.to_mapping().get(k)
89    }
90
91    /// Get the value associated with key `k` in the map.
92    ///
93    /// If no value is present, the returned value is meaningless.
94    #[logic(open, inline)]
95    pub fn lookup(self, k: K) -> V {
96        self.get(k).unwrap_logic()
97    }
98
99    /// Returns `true` if the map contains a value for the specified key.
100    #[logic(open, inline)]
101    pub fn contains(self, k: K) -> bool {
102        self.get(k) != None
103    }
104
105    /// Returns `true` if the map contains no elements.
106    #[logic(open)]
107    pub fn is_empty(self) -> bool {
108        self.ext_eq(FMap::empty())
109    }
110
111    /// Returns `true` if the two maps have no key in common.
112    #[logic(open)]
113    pub fn disjoint(self, other: Self) -> bool {
114        pearlite! {forall<k: K> !self.contains(k) || !other.contains(k)}
115    }
116
117    /// Returns `true` if all key-value pairs in `self` are also in `other`.
118    #[logic(open)]
119    pub fn subset(self, other: Self) -> bool {
120        pearlite! {
121            forall<k: K> self.contains(k) ==> other.get(k) == self.get(k)
122        }
123    }
124
125    /// Returns a new map, which is the union of `self` and `other`.
126    ///
127    /// If `self` and `other` are not [`disjoint`](Self::disjoint), the result is unspecified.
128    #[trusted]
129    #[logic(opaque)]
130    #[requires(self.disjoint(other))]
131    #[ensures(forall<k: K> #[trigger(result.get(k))] !self.contains(k) ==> result.get(k) == other.get(k))]
132    #[ensures(forall<k: K> #[trigger(result.get(k))] !other.contains(k) ==> result.get(k) == self.get(k))]
133    #[ensures(result.len() == self.len() + other.len())]
134    pub fn union(self, other: Self) -> Self {
135        dead
136    }
137
138    /// Returns a new map, that contains all the key-value pairs of `self` such that the
139    /// key is not in `other`.
140    #[trusted]
141    #[logic(opaque)]
142    #[ensures(result.disjoint(other))]
143    #[ensures(other.subset(self) ==> other.union(result) == self)]
144    #[ensures(forall<k: K> #[trigger(result.get(k))] result.get(k) ==
145        if other.contains(k) {
146            None
147        } else {
148            self.get(k)
149        }
150    )]
151    pub fn subtract(self, other: Self) -> Self {
152        dead
153    }
154
155    /// Injectivity of [`to_mapping`]. Private axiom used by ext_eq
156    #[logic]
157    #[trusted]
158    #[requires(self.to_mapping() == other.to_mapping())]
159    #[ensures(self == other)]
160    fn to_mapping_inj(self, other: Self) {}
161
162    /// Extensional equality.
163    ///
164    /// Returns `true` if `self` and `other` contain exactly the same key-value pairs.
165    ///
166    /// This is in fact equivalent with normal equality.
167    #[logic(open)]
168    #[ensures(result == (self == other))]
169    pub fn ext_eq(self, other: Self) -> bool {
170        pearlite! {
171            let _ = Self::to_mapping_inj;
172            forall<k: K> self.get(k) == other.get(k)
173        }
174    }
175
176    /// Merge the two maps together
177    ///
178    /// If both map contain the same key, the entry for the result is determined by `f`.
179    #[trusted]
180    #[logic(opaque)]
181    #[ensures(
182        forall<k: K> #[trigger(result.get(k))]
183            match (self.get(k), m.get(k)) {
184                (None, y) => result.get(k) == y,
185                (x, None) => result.get(k) == x,
186                (Some(x), Some(y)) => result.get(k) == Some(f[(x, y)]),
187            }
188    )]
189    pub fn merge(self, m: FMap<K, V>, f: Mapping<(V, V), V>) -> FMap<K, V> {
190        dead
191    }
192
193    /// Map every value in `self` according to `f`. Keys are unchanged.
194    #[logic]
195    #[trusted] // The ensures clause that says the lenght do not change is rather difficult
196    #[ensures(forall<k: K> #[trigger(result.get(k))] result.get(k) == match self.get(k) {
197        None => None,
198        Some(v) => Some(f[(k, v)]),
199    })]
200    #[ensures(result.len() == self.len())]
201    pub fn map<V2>(self, f: Mapping<(K, V), V2>) -> FMap<K, V2> {
202        self.filter_map(|(k, v)| Some(f[(k, v)]))
203    }
204
205    /// Filter key-values in `self` according to `p`.
206    ///
207    /// A key-value pair will be in the result map if and only if it is in `self` and
208    /// `p` returns `true` on this pair.
209    #[logic]
210    #[ensures(forall<k: K> #[trigger(result.get(k))] result.get(k) == match self.get(k) {
211        None => None,
212        Some(v) => if p[(k, v)] { Some(v) } else { None },
213    })]
214    pub fn filter(self, p: Mapping<(K, V), bool>) -> Self {
215        self.filter_map(|(k, v)| if p[(k, v)] { Some(v) } else { None })
216    }
217
218    /// Map every value in `self` according to `f`. Keys are unchanged.
219    /// If `f` returns `false`, remove the key-value from the map.
220    #[trusted]
221    #[logic(opaque)]
222    #[ensures(forall<k: K> #[trigger(result.get(k))] result.get(k) == match self.get(k) {
223        None => None,
224        Some(v) => f[(k, v)],
225    })]
226    pub fn filter_map<V2>(self, f: Mapping<(K, V), Option<V2>>) -> FMap<K, V2> {
227        dead
228    }
229
230    /// Returns the set of keys in the map.
231    #[trusted]
232    #[logic(opaque)]
233    #[ensures(forall<k: K> result.contains(k) == self.contains(k))]
234    #[ensures(result.len() == self.len())]
235    pub fn keys(self) -> FSet<K> {
236        dead
237    }
238}
239
240impl<K, V> IndexLogic<K> for FMap<K, V> {
241    type Item = V;
242
243    #[logic(open, inline)]
244    fn index_logic(self, key: K) -> Self::Item {
245        self.lookup(key)
246    }
247}
248
249/// Ghost definitions
250impl<K, V> FMap<K, V> {
251    /// Create a new, empty map on the ghost heap.
252    #[trusted]
253    #[check(ghost)]
254    #[ensures(result.is_empty())]
255    #[allow(unreachable_code)]
256    pub fn new() -> Ghost<Self> {
257        Ghost::conjure()
258    }
259
260    /// Returns the number of elements in the map.
261    ///
262    /// If you need to get the length in pearlite, consider using [`len`](Self::len).
263    ///
264    /// # Example
265    /// ```rust,creusot
266    /// use creusot_std::{logic::FMap, prelude::*};
267    ///
268    /// let mut map = FMap::new();
269    /// ghost! {
270    ///     let len1 = map.len_ghost();
271    ///     map.insert_ghost(1, 21);
272    ///     map.insert_ghost(1, 42);
273    ///     map.insert_ghost(2, 50);
274    ///     let len2 = map.len_ghost();
275    ///     proof_assert!(len1 == 0);
276    ///     proof_assert!(len2 == 2);
277    /// };
278    /// ```
279    #[trusted]
280    #[check(ghost)]
281    #[ensures(result == self.len())]
282    pub fn len_ghost(&self) -> Int {
283        panic!()
284    }
285
286    #[trusted]
287    #[check(ghost)]
288    #[ensures(result == (self.len() == 0 && forall<k> !self.contains(k)))]
289    pub fn is_empty_ghost(&self) -> bool {
290        panic!()
291    }
292
293    /// Returns true if the map contains a value for the specified key.
294    ///
295    /// # Example
296    /// ```rust,creusot
297    /// use creusot_std::{logic::FMap, prelude::*};
298    ///
299    /// let mut map = FMap::new();
300    /// ghost! {
301    ///     map.insert_ghost(1, 42);
302    ///     let (b1, b2) = (map.contains_ghost(&1), map.contains_ghost(&2));
303    ///     proof_assert!(b1);
304    ///     proof_assert!(!b2);
305    /// };
306    /// ```
307    #[check(ghost)]
308    #[ensures(result == self.contains(*key))]
309    pub fn contains_ghost(&self, key: &K) -> bool {
310        self.get_ghost(key).is_some()
311    }
312
313    /// Returns a reference to the value corresponding to the key.
314    ///
315    /// # Example
316    /// ```rust,creusot
317    /// use creusot_std::{logic::FMap, prelude::*};
318    ///
319    /// let mut map = FMap::new();
320    /// ghost! {
321    ///     map.insert_ghost(1, 2);
322    ///     let x1 = map.get_ghost(&1);
323    ///     let x2 = map.get_ghost(&2);
324    ///     proof_assert!(x1 == Some(&2));
325    ///     proof_assert!(x2 == None);
326    /// };
327    /// ```
328    #[trusted]
329    #[check(ghost)]
330    #[ensures(result == self.get(*key).map_logic(|v|&v))]
331    pub fn get_ghost(&self, key: &K) -> Option<&V> {
332        let _ = key;
333        panic!()
334    }
335
336    /// Returns a mutable reference to the value corresponding to the key.
337    ///
338    /// # Example
339    /// ```rust,creusot
340    /// use creusot_std::{logic::FMap, prelude::*};
341    ///
342    /// let mut map = FMap::new();
343    /// ghost! {
344    ///     map.insert_ghost(1, 21);
345    ///     if let Some(x) = map.get_mut_ghost(&1) {
346    ///         *x = 42;
347    ///     }
348    ///     proof_assert!(map[1i32] == 42i32);
349    /// };
350    /// ```
351    #[trusted]
352    #[check(ghost)]
353    #[ensures(if self.contains(*key) {
354            match result {
355                None => false,
356                Some(r) =>
357                    (^self).contains(*key) && self[*key] == *r && (^self)[*key] == ^r,
358            }
359        } else {
360            result == None && *self == ^self
361        })]
362    #[ensures(forall<k: K> k != *key ==> (*self).get(k) == (^self).get(k))]
363    #[ensures((*self).len() == (^self).len())]
364    pub fn get_mut_ghost(&mut self, key: &K) -> Option<&mut V> {
365        let _ = key;
366        panic!()
367    }
368
369    /// Returns a mutable reference to the value corresponding to a key, while still allowing
370    /// modification on the other keys.
371    ///
372    /// # Example
373    /// ```rust,creusot
374    /// use creusot_std::{logic::FMap, prelude::*};
375    ///
376    /// let mut map = FMap::new();
377    /// ghost! {
378    ///     map.insert_ghost(1, 21);
379    ///     map.insert_ghost(2, 42);
380    ///     let (x, map2) = map.split_mut_ghost(&1);
381    ///     *x = 22;
382    ///     map2.insert_ghost(3, 30);
383    ///     map2.insert_ghost(1, 56); // This modification will be ignored on `map`
384    ///     proof_assert!(map[1i32] == 22i32);
385    ///     proof_assert!(map[2i32] == 42i32);
386    ///     proof_assert!(map[3i32] == 30i32);
387    /// };
388    /// ```
389    #[trusted]
390    #[check(ghost)]
391    #[requires(self.contains(*key))]
392    #[ensures(*result.1 == (*self).remove(*key))]
393    #[ensures(self[*key] == *result.0 && ^self == (^result.1).insert(*key, ^result.0))]
394    pub fn split_mut_ghost(&mut self, key: &K) -> (&mut V, &mut Self) {
395        let _ = key;
396        panic!()
397    }
398
399    /// Inserts a key-value pair into the map.
400    ///
401    /// If the map did not have this key present, `None` is returned.
402    ///
403    /// # Example
404    /// ```rust,creusot
405    /// use creusot_std::{logic::FMap, prelude::*};
406    ///
407    /// let mut map = FMap::new();
408    /// ghost! {
409    ///     let res1 = map.insert_ghost(37, 41);
410    ///     proof_assert!(res1 == None);
411    ///     proof_assert!(map.is_empty() == false);
412    ///
413    ///     let res2 = map.insert_ghost(37, 42);
414    ///     proof_assert!(res2 == Some(41));
415    ///     proof_assert!(map[37i32] == 42i32);
416    /// };
417    /// ```
418    #[trusted]
419    #[check(ghost)]
420    #[ensures(^self == (*self).insert(key, value))]
421    #[ensures(result == (*self).get(key))]
422    pub fn insert_ghost(&mut self, key: K, value: V) -> Option<V> {
423        let _ = key;
424        let _ = value;
425        panic!()
426    }
427
428    /// Removes a key from the map, returning the value at the key if the key was previously in the map.
429    ///
430    /// # Example
431    /// ```rust,creusot
432    /// use creusot_std::{logic::FMap, prelude::*};
433    ///
434    /// let mut map = FMap::new();
435    /// let res = ghost! {
436    ///     map.insert_ghost(1, 42);
437    ///     let res1 = map.remove_ghost(&1);
438    ///     let res2 = map.remove_ghost(&1);
439    ///     proof_assert!(res1 == Some(42i32));
440    ///     proof_assert!(res2 == None);
441    /// };
442    /// ```
443    #[trusted]
444    #[check(ghost)]
445    #[ensures(^self == (*self).remove(*key))]
446    #[ensures(result == (*self).get(*key))]
447    pub fn remove_ghost(&mut self, key: &K) -> Option<V> {
448        let _ = key;
449        panic!()
450    }
451
452    /// Clears the map, removing all values.
453    ///
454    /// # Example
455    /// ```rust,creusot
456    /// use creusot_std::{logic::FMap, prelude::*};
457    ///
458    /// let mut s = FMap::new();
459    /// ghost! {
460    ///     s.insert_ghost(1, 2);
461    ///     s.insert_ghost(2, 3);
462    ///     s.insert_ghost(3, 42);
463    ///     s.clear_ghost();
464    ///     proof_assert!(s == FMap::empty());
465    /// };
466    /// ```
467    #[trusted]
468    #[check(ghost)]
469    #[ensures(^self == Self::empty())]
470    pub fn clear_ghost(&mut self) {}
471
472    #[trusted]
473    #[check(ghost)]
474    #[ensures(match result {
475        None => *self == ^self && self.is_empty(),
476        Some((k, v)) => *self == (^self).insert(k, v) && !(^self).contains(k),
477    })]
478    pub fn remove_one_ghost(&mut self) -> Option<(K, V)> {
479        panic!()
480    }
481
482    #[trusted]
483    #[check(ghost)]
484    #[ensures(result.len() == self.len())]
485    #[ensures(forall<k, v> (self.get(k) == Some(v)) == (exists<i> result.get(i) == Some((k, v))))]
486    pub fn to_seq(self) -> Seq<(K, V)> {
487        panic!()
488    }
489
490    #[trusted]
491    #[check(ghost)]
492    #[ensures(result.len() == self.len())]
493    #[ensures(forall<k, v> (self.get(k) == Some(v)) == (result.get(&k) == Some(&v)))]
494    pub fn as_ref_ghost(&self) -> FMap<&K, &V> {
495        panic!()
496    }
497
498    #[trusted]
499    #[check(ghost)]
500    #[ensures(result.len() == self.len())]
501    #[ensures(forall<k> match result.get(&k) {
502        None => !(*self).contains(k) && !(^self).contains(k),
503        Some(v) => (*self).get(k) == Some(*v) && (^self).get(k) == Some(^v),
504    })]
505    pub fn as_mut_ghost(&mut self) -> FMap<&K, &mut V> {
506        panic!()
507    }
508}
509
510impl<'a, K, V> core::ops::Index<&'a K> for FMap<K, V> {
511    type Output = V;
512
513    #[check(ghost)]
514    #[requires(self.contains(*key))]
515    #[ensures(Some(*result) == self.get(*key))]
516    fn index(&self, key: &'a K) -> &Self::Output {
517        self.get_ghost(key).unwrap()
518    }
519}
520
521impl<K: Clone + Copy, V: Clone + Copy> Clone for FMap<K, V> {
522    #[trusted]
523    #[check(ghost)]
524    #[ensures(result == *self)]
525    fn clone(&self) -> Self {
526        *self
527    }
528}
529
530// Having `Copy` guarantees that the operation is pure, even if we decide to change the definition of `Clone`.
531impl<K: Clone + Copy, V: Clone + Copy> Copy for FMap<K, V> {}
532
533impl<K, V> Invariant for FMap<K, V> {
534    #[logic(open, prophetic, inline)]
535    #[creusot::trusted_trivial_if_param_trivial]
536    fn invariant(self) -> bool {
537        pearlite! { forall<k: K> self.contains(k) ==> inv(k) && inv(self[k]) }
538    }
539}
540
541impl<K, V> Iterator for FMap<K, V> {
542    type Item = (K, V);
543
544    #[check(ghost)]
545    #[ensures(match result {
546        None => self.completed(),
547        Some((k, v)) => (*self).produces(Seq::singleton((k, v)), ^self) && (*self) == (^self).insert(k, v),
548    })]
549    fn next(&mut self) -> Option<(K, V)> {
550        self.remove_one_ghost()
551    }
552}
553
554impl<K, V> IteratorSpec for FMap<K, V> {
555    #[logic(prophetic, open)]
556    fn produces(self, visited: Seq<(K, V)>, o: Self) -> bool {
557        pearlite! {
558            // We cannot visit the same key twice
559            (forall<i, j> 0 <= i && i < j && j < visited.len() ==> visited[i].0 != visited[j].0) &&
560            // If a key-value is visited, it was in `self` but not in `o`
561            (forall<k, v, i> visited.get(i) == Some((k, v)) ==> !o.contains(k) && self.get(k) == Some(v)) &&
562            // Helper for the length
563            self.len() == visited.len() + o.len() &&
564            // else, the key-value is the same in `self` and `o`
565            (forall<k> (forall<i> 0 <= i && i < visited.len() ==> visited[i].0 != k) ==> o.get(k) == self.get(k))
566        }
567    }
568
569    #[logic(prophetic, open)]
570    fn completed(&mut self) -> bool {
571        pearlite! { self.is_empty() }
572    }
573
574    #[logic(law)]
575    #[ensures(self.produces(Seq::empty(), self))]
576    fn produces_refl(self) {}
577
578    #[logic(law)]
579    #[requires(a.produces(ab, b))]
580    #[requires(b.produces(bc, c))]
581    #[ensures(a.produces(ab.concat(bc), c))]
582    fn produces_trans(a: Self, ab: Seq<Self::Item>, b: Self, bc: Seq<Self::Item>, c: Self) {
583        let ac = ab.concat(bc);
584        proof_assert!(forall<x> ab.contains(x) ==> ac.contains(x));
585        proof_assert!(forall<i> 0 <= i && i < bc.len() ==> ac[i + ab.len()] == bc[i]);
586        proof_assert!(forall<k> (forall<i> 0 <= i && i < ac.len() ==> ac[i].0 != k) ==> {
587            (forall<i> 0 <= i && i < ab.len() ==> ab[i].0 != k) &&
588            (forall<i> 0 <= i && i < bc.len() ==> bc[i].0 != k) &&
589            a.get(k) == b.get(k) && b.get(k) == c.get(k)
590        });
591    }
592}
593
594impl<'a, K, V> IntoIterator for &'a FMap<K, V> {
595    type Item = (&'a K, &'a V);
596    type IntoIter = FMap<&'a K, &'a V>;
597
598    #[check(ghost)]
599    #[ensures(result.len() == self.len())]
600    #[ensures(forall<k, v> (self.get(k) == Some(v)) == (result.get(&k) == Some(&v)))]
601    fn into_iter(self) -> FMap<&'a K, &'a V> {
602        self.as_ref_ghost()
603    }
604}
605
606impl<K, V> Resolve for FMap<K, V> {
607    #[logic(open, prophetic)]
608    #[creusot::trusted_trivial_if_param_trivial]
609    fn resolve(self) -> bool {
610        pearlite! { forall<k: K, v: V> self.get(k) == Some(v) ==> resolve(k) && resolve(v) }
611    }
612
613    #[trusted]
614    #[logic(open(self), prophetic)]
615    #[requires(structural_resolve(self))]
616    #[ensures(self.resolve())]
617    fn resolve_coherence(self) {}
618}
creusot_std/logic/fmap.rs

creusot_std/logic/
fmap.rs
