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

creusot_std/logic/
fmap.rs
