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

creusot_std/logic/
fmap.rs
