creusot_contracts/logic/
fmap.rs

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

creusot_contracts/logic/
fmap.rs
