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

creusot_std/logic/
fmap.rs
