creusot_std/std/
option.rs

1#[cfg(creusot)]
2use crate::logic::{Mapping, such_that};
3use crate::{logic::ord::ord_laws_impl, prelude::*};
4use core::option::*;
5#[cfg(creusot)]
6use core::{cmp::Ordering, marker::Destruct};
7
8impl<T: DeepModel> DeepModel for Option<T> {
9    type DeepModelTy = Option<T::DeepModelTy>;
10
11    #[logic(open, inline)]
12    fn deep_model(self) -> Self::DeepModelTy {
13        match self {
14            Some(t) => Some(t.deep_model()),
15            None => None,
16        }
17    }
18}
19
20extern_spec! {
21    impl<T: PartialEq + DeepModel> PartialEq for Option<T> {
22        #[allow(unstable_name_collisions)]
23        #[ensures(result == (self.deep_model() == rhs.deep_model()))]
24        fn eq(&self, rhs: &Self) -> bool {
25            match (self, rhs) {
26                (None, None) => true,
27                (Some(x), Some(y)) => x == y,
28                _ => false,
29            }
30        }
31    }
32
33    impl<T: Clone> Clone for Option<T> {
34        #[ensures(match (*self, result) {
35            (None, None) => true,
36            (Some(s), Some(r)) => T::clone.postcondition((&s,), r),
37            _ => false
38        })]
39        fn clone(&self) -> Option<T> {
40            match self {
41                None => None,
42                Some(x) => Some(x.clone())
43            }
44        }
45    }
46
47    impl<T> Option<T> {
48        #[check(ghost)]
49        #[erasure]
50        #[ensures(result == (*self != None))]
51        fn is_some(&self) -> bool {
52            match *self {
53                Some(_) => true,
54                None => false,
55            }
56        }
57
58        #[erasure]
59        #[requires(match self { None => true, Some(t) => f.precondition((t,)) })]
60        #[ensures(match self {
61            None => result == false,
62            Some(t) => f.postcondition_once((t,), result),
63        })]
64        fn is_some_and(self, f: impl FnOnce(T) -> bool + Destruct) -> bool {
65            match self {
66                None => false,
67                Some(t) => f(t),
68            }
69        }
70
71        #[check(ghost)]
72        #[erasure]
73        #[ensures(result == (*self == None))]
74        fn is_none(&self) -> bool {
75            !self.is_some()
76        }
77
78        #[check(ghost)]
79        #[erasure]
80        #[ensures(*self == None ==> result == None)]
81        #[ensures(
82            *self == None || exists<r: &T> result == Some(r) && *self == Some(*r)
83        )]
84        fn as_ref(&self) -> Option<&T> {
85            match *self {
86                Some(ref t) => Some(t),
87                None => None,
88            }
89        }
90
91        #[check(ghost)]
92        #[erasure]
93        #[ensures(*self == None ==> result == None && ^self == None)]
94        #[ensures(
95            *self == None
96            || exists<r: &mut T> result == Some(r) && *self == Some(*r) && ^self == Some(^r)
97        )]
98        fn as_mut(&mut self) -> Option<&mut T> {
99            match *self {
100                Some(ref mut t) => Some(t),
101                None => None,
102            }
103        }
104
105        // FIXME: specify those once we have a specification for `Pin`
106        // const fn as_pin_ref(self: Pin<&Option<T>>) -> Option<Pin<&T>>;
107        // const fn as_pin_mut(self: Pin<&mut Option<T>>) -> Option<Pin<&mut T>>;
108
109        #[check(ghost)]
110        #[ensures(match *self {
111            None => result@.len() == 0,
112            Some(t) => result@.len() == 1 && result@[0] == t
113        })]
114        fn as_slice(&self) -> &[T] {
115            match self {
116                None => &[],
117                Some(t) => core::slice::from_ref(t),
118            }
119        }
120
121        #[check(ghost)]
122        #[ensures(match *self {
123            None => result@.len() == 0,
124            Some(_) => exists<b:&mut T>
125                *self == Some(*b) && ^self == Some(^b) &&
126                (*result)@[0] == *b && (^result)@[0] == ^b &&
127                (*result)@.len() == 1 && (^result)@.len() == 1,
128        })]
129        fn as_mut_slice(&mut self) -> &mut [T] {
130            match self {
131                None => &mut [],
132                Some(t) => core::slice::from_mut(t),
133            }
134        }
135
136        #[check(ghost)]
137        #[requires(self != None)]
138        #[ensures(Some(result) == self)]
139        fn expect(self, msg: &str) -> T {
140            match self {
141                None => panic!(),
142                Some(t) => t,
143            }
144        }
145
146        #[check(ghost)]
147        #[requires(self != None)]
148        #[ensures(Some(result) == self)]
149        fn unwrap(self) -> T {
150            match self {
151                None => panic!(),
152                Some(t) => t,
153            }
154        }
155
156        #[check(ghost)]
157        #[erasure]
158        #[ensures(self == None ==> result == default)]
159        #[ensures(self == None || (self == Some(result) && resolve(default)))]
160        fn unwrap_or(self, default: T) -> T {
161            match self {
162                Some(t) => t,
163                None => default,
164            }
165        }
166
167        #[erasure]
168        #[requires(self == None ==> f.precondition(()))]
169        #[ensures(match self {
170            None => f.postcondition_once((), result),
171            Some(t) => result == t
172        })]
173        fn unwrap_or_else<F>(self, f: F) -> T
174        where
175            F: FnOnce() -> T {
176            match self {
177                Some(t) => t,
178                None => f(),
179            }
180        }
181
182        #[erasure]
183        #[ensures(self == None ==> T::default.postcondition((), result))]
184        #[ensures(self == None || self == Some(result))]
185        fn unwrap_or_default(self) -> T
186        where
187            T: Default {
188            match self {
189                Some(t) => t,
190                None => T::default(),
191            }
192        }
193
194        #[check(ghost)]
195        #[requires(self != None)]
196        #[ensures(Some(result) == self)]
197        unsafe fn unwrap_unchecked(self) -> T {
198            match self {
199                None => panic!(),
200                Some(t) => t,
201            }
202        }
203
204        #[erasure]
205        #[requires(match self { None => true, Some(t) => f.precondition((t,)) })]
206        #[ensures(match self {
207            None => result == None,
208            Some(t) => exists<r> result == Some(r) && f.postcondition_once((t,), r),
209        })]
210        fn map<U, F: FnOnce(T) -> U>(self, f: F) -> Option<U> {
211            match self {
212                Some(t) => Some(f(t)),
213                None => None,
214            }
215        }
216
217        #[requires(match self { None => true, Some(t) => f.precondition((&t,)) })]
218        #[ensures(result == self)]
219        #[ensures(match self {
220            None => true,
221            Some(t) => f.postcondition_once((&t,), ()),
222        })]
223        fn inspect<F: FnOnce(&T)>(self, f: F) -> Option<T> {
224            match self {
225                None => None,
226                Some(t) => { f(&t); Some(t) }
227            }
228        }
229
230        #[requires(match self { None => true, Some(t) => f.precondition((t,)) })]
231        #[ensures(match self {
232            None => result == default,
233            Some(t) => f.postcondition_once((t,), result)
234        })]
235        fn map_or<U, F: FnOnce(T) -> U>(self, default: U, f: F) -> U {
236            match self {
237                None => default,
238                Some(t) => f(t),
239            }
240        }
241
242        #[requires(match self {
243            None => default.precondition(()),
244            Some(t) => f.precondition((t,)),
245        })]
246        #[ensures(match self {
247            None => default.postcondition_once((), result),
248            Some(t) => f.postcondition_once((t,), result),
249        })]
250        fn map_or_else<U, D: FnOnce() -> U, F: FnOnce(T) -> U>(self, default: D, f: F) -> U {
251            match self {
252                None => default(),
253                Some(t) => f(t),
254            }
255        }
256
257        #[check(ghost)]
258        #[ensures(match self {
259            None => result == Err(err),
260            Some(t) => result == Ok(t) && resolve(err),
261        })]
262        fn ok_or<E>(self, err: E) -> Result<T, E> {
263            match self {
264                None => Err(err),
265                Some(t) => Ok(t),
266            }
267        }
268
269        #[requires(self == None ==> err.precondition(()))]
270        #[ensures(match self {
271            None => exists<r> result == Err(r) && err.postcondition_once((), r),
272            Some(t) => result == Ok(t),
273        })]
274        fn ok_or_else<E, F: FnOnce() -> E>(self, err: F) -> Result<T, E> {
275            match self {
276                None => Err(err()),
277                Some(t) => Ok(t),
278            }
279        }
280
281        #[requires(match self {
282            None => true,
283            Some(x) => T::deref.precondition((x,)),
284        })]
285        #[ensures(match (self, result) {
286            (None, None) => true,
287            (Some(x), Some(r)) => T::deref.postcondition((x,), r),
288            _ => false,
289        })]
290        fn as_deref(&self) -> Option<&<T as ::core::ops::Deref>::Target>
291            where T: ::core::ops::Deref,
292        {
293            match self {
294                Some(x) => Some(&*x),
295                None => None,
296            }
297        }
298
299        #[requires(match *self {
300            None => true,
301            Some(cur) => forall<bor: &mut T> *bor == cur ==> T::deref_mut.precondition((bor,)),
302        })]
303        #[ensures(match (*self, ^self, result) {
304            (None, None, None) => true,
305            (Some(cur), Some(fin), Some(r)) => exists<bor: &mut T> *bor == cur && ^bor == fin && T::deref_mut.postcondition((bor,), r),
306            _ => false,
307        })]
308        fn as_deref_mut(&mut self) -> Option<&mut<T as ::core::ops::Deref>::Target>
309            where T: ::core::ops::DerefMut,
310        {
311            match self {
312                Some(x) => Some(&mut *x),
313                None => None,
314            }
315        }
316
317        #[ensures(match *self {
318            None => exists<it: &mut Iter<'_, T>> it.completed() && *it == result,
319            Some(x) => exists<s: Seq<&T>, it: &mut Iter<'_, T>> {
320                it.completed() && s.len() == 1 && *s[0] == x && result.produces(s, *it)
321            }
322        })]
323        fn iter(&self) -> Iter<'_, T>;
324
325        #[ensures(match (*self, ^self) {
326            (None, None) => exists<it: &mut IterMut<'_, T>> it.completed() && *it == result,
327            (Some(cur), Some(fin)) => exists<s: Seq<&mut T>, it: &mut IterMut<'_, T>> {
328                it.completed() && s.len() == 1 && *s[0] == cur && ^s[0] == fin && result.produces(s, *it)
329            },
330            _ => false,
331        })]
332        fn iter_mut(&mut self) -> IterMut<'_, T>;
333
334
335        #[check(ghost)]
336        #[ensures(self == None ==> result == None && resolve(optb))]
337        #[ensures(self == None || (result == optb && resolve(self)))]
338        fn and<U>(self, optb: Option<U>) -> Option<U> {
339            match self {
340                None => None,
341                Some(_) => optb,
342            }
343        }
344
345        #[requires(match self { None => true, Some(t) => f.precondition((t,)) })]
346        #[ensures(match self {
347            None => result == None,
348            Some(t) => f.postcondition_once((t,), result),
349        })]
350        fn and_then<U, F: FnOnce(T) -> Option<U>>(self, f: F) -> Option<U> {
351            match self {
352                None => None,
353                Some(t) => f(t),
354            }
355        }
356
357        #[requires(match self { None => true, Some(t) => predicate.precondition((&t,)) })]
358        #[ensures(match self {
359            None => result == None,
360            Some(t) => match result {
361                None => predicate.postcondition_once((&t,), false) && resolve(t),
362                Some(r) => predicate.postcondition_once((&t,), true) && r == t,
363            },
364        })]
365        fn filter<P: FnOnce(&T) -> bool>(self, predicate: P) -> Option<T> {
366            match self {
367                None => None,
368                Some(t) => if predicate(&t) { Some(t) } else { None }
369            }
370        }
371
372        #[check(ghost)]
373        #[ensures(self == None ==> result == optb)]
374        #[ensures(self == None || (result == self && resolve(optb)))]
375        fn or(self, optb: Option<T>) -> Option<T> {
376            match self {
377                None => optb,
378                Some(t) => Some(t),
379            }
380        }
381
382        #[requires(self == None ==> f.precondition(()))]
383        #[ensures(match self {
384            None => f.postcondition_once((), result),
385            Some(t) => result == Some(t),
386        })]
387        fn or_else<F: FnOnce() -> Option<T>>(self, f: F) -> Option<T> {
388            match self {
389                None => f(),
390                Some(t) => Some(t),
391            }
392        }
393
394        #[check(ghost)]
395        #[ensures(match (self, optb) {
396            (None, None)         => result == None,
397            (Some(t1), Some(t2)) => result == None && resolve(t1) && resolve(t2),
398            (Some(t), None)      => result == Some(t),
399            (None, Some(t))      => result == Some(t),
400        })]
401        fn xor(self, optb: Option<T>) -> Option<T> {
402            match (self, optb) {
403                (Some(t), None) | (None, Some(t)) => Some(t),
404                _ => None,
405            }
406        }
407
408        #[check(ghost)]
409        #[ensures(match *self { Some(t) => resolve(t), None => true })]
410        #[ensures(*result == value && ^self == Some(^result))]
411        fn insert(&mut self, value: T) -> &mut T {
412            *self = Some(value);
413            match self {
414                None => unreachable!(),
415                Some(v) => v,
416            }
417        }
418
419        #[check(ghost)]
420        #[ensures(match *self {
421            None => *result == value && ^self == Some(^result),
422            Some(_) => *self == Some(*result) && ^self == Some(^result) && resolve(value),
423        })]
424        fn get_or_insert(&mut self, value: T) -> &mut T {
425            match self {
426                None => *self = Some(value),
427                Some(_) => {}
428            }
429            match self {
430                None => unreachable!(),
431                Some(v) => v,
432            }
433        }
434
435        #[requires(match self {
436            None => T::default.precondition(()),
437            Some(_) => true,
438        })]
439        #[ensures(match *self {
440            None => T::default.postcondition((), *result) && ^self == Some(^result),
441            Some(_) => *self == Some(*result) && ^self == Some(^result),
442        })]
443        fn get_or_insert_default(&mut self) -> &mut T
444            where T: Default,
445        {
446            self.get_or_insert(T::default())
447        }
448
449        #[requires(*self == None ==> f.precondition(()))]
450        #[ensures(match *self {
451            None => f.postcondition_once((), *result) && ^self == Some(^result),
452            Some(_) => *self == Some(*result) && ^self == Some(^result),
453        })]
454        fn get_or_insert_with<F: FnOnce() -> T>(&mut self, f: F) -> &mut T {
455            match self {
456                None => { *self = Some(f()); self.as_mut().unwrap() }
457                Some(t) => t,
458            }
459        }
460
461        #[check(ghost)]
462        #[ensures(result == *self && ^self == None)]
463        fn take(&mut self) -> Option<T> {
464            core::mem::replace(self, None)
465        }
466
467        #[requires(match *self {
468            None => true,
469            Some(t) => forall<b:&mut T> inv(b) && *b == t ==> predicate.precondition((b,)),
470        })]
471        #[ensures(match *self {
472            None => result == None && ^self == None,
473            Some(cur) =>
474                exists<b: &mut T, res: bool> inv(b) && cur == *b && predicate.postcondition_once((b,), res) &&
475                    if res {
476                        ^self == None && result == Some(^b)
477                    } else {
478                        ^self == Some(^b) && result == None
479                    }
480        })]
481        fn take_if<P: FnOnce(&mut T) -> bool>(&mut self, predicate: P) -> Option<T> {
482            match self {
483                None => None,
484                Some(t) => if predicate(t) { self.take() } else { None },
485            }
486        }
487
488        #[check(ghost)]
489        #[ensures(result == *self && ^self == Some(value))]
490        fn replace(&mut self, value: T) -> Option<T> {
491            core::mem::replace(self, Some(value))
492        }
493
494        #[check(ghost)]
495        #[ensures(match (self, other) {
496            (None, _)          => result == None && resolve(other),
497            (_, None)          => result == None && resolve(self),
498            (Some(t), Some(u)) => result == Some((t, u)),
499        })]
500        fn zip<U>(self, other: Option<U>) -> Option<(T, U)> {
501            match (self, other) {
502                (Some(t), Some(u)) => Some((t, u)),
503                _ => None,
504            }
505        }
506    }
507
508    impl<T, U> Option<(T, U)> {
509        #[check(ghost)]
510        #[ensures(match self {
511            None => result == (None, None),
512            Some((t, u)) => result == (Some(t), Some(u)),
513        })]
514        fn unzip(self) -> (Option<T>, Option<U>) {
515            match self {
516                Some((t, u)) => (Some(t), Some(u)),
517                None => (None, None),
518            }
519        }
520    }
521
522    impl<T> Option<&T> {
523        #[check(ghost)]
524        #[ensures(match self {
525            None => result == None,
526            Some(s) => result == Some(*s)
527        })]
528        fn copied(self) -> Option<T>
529        where
530            T: Copy
531        {
532            match self {
533                None => None,
534                Some(t) => Some(*t),
535            }
536        }
537
538        #[ensures(match (self, result) {
539            (None, None) => true,
540            (Some(s), Some(r)) =>T::clone.postcondition((s,), r),
541            _ => false
542        })]
543        fn cloned(self) -> Option<T>
544        where
545            T: Clone
546        {
547            match self {
548                None => None,
549                Some(t) => Some(t.clone()),
550            }
551        }
552    }
553
554    impl<T> Option<&mut T> {
555        #[check(ghost)]
556        #[ensures(match self {
557            None => result == None,
558            Some(s) => result == Some(*s) && ^s == *s
559        })]
560        fn copied(self) -> Option<T>
561        where
562            T: Copy
563        {
564            match self {
565                None => None,
566                Some(t) => Some(*t),
567            }
568        }
569
570        #[ensures(match (self, result) {
571            (None, None) => true,
572            (Some(s), Some(r)) => T::clone.postcondition((s,), r) && ^s == *s,
573            _ => false
574        })]
575        fn cloned(self) -> Option<T>
576        where
577            T: Clone
578        {
579            match self {
580                None => None,
581                Some(t) => Some(t.clone()),
582            }
583        }
584    }
585
586    impl<T, E> Option<Result<T, E>> {
587        #[check(ghost)]
588        #[ensures(match self {
589            None => result == Ok(None),
590            Some(Ok(ok)) => result == Ok(Some(ok)),
591            Some(Err(err)) => result == Err(err),
592        })]
593        fn transpose(self) -> Result<Option<T>, E> {
594            match self {
595                None => Ok(None),
596                Some(Ok(ok)) => Ok(Some(ok)),
597                Some(Err(err)) => Err(err),
598            }
599        }
600    }
601
602    impl<T> Option<Option<T>> {
603        #[check(ghost)]
604        #[ensures(self == None ==> result == None)]
605        #[ensures(self == None || self == Some(result))]
606        fn flatten(self) -> Option<T> {
607            match self {
608                None => None,
609                Some(opt) => opt,
610            }
611        }
612    }
613
614    impl<T> IntoIterator for Option<T>{
615        #[check(ghost)]
616        #[ensures(self == result@)]
617        fn into_iter(self) -> IntoIter<T>;
618    }
619
620    impl<'a, T> IntoIterator for &'a Option<T>{
621        #[check(ghost)]
622        #[ensures(*self == match result@ { None => None, Some(r) => Some(*r) })]
623        fn into_iter(self) -> Iter<'a, T>;
624    }
625
626    impl<'a, T> IntoIterator for &'a mut Option<T>{
627        #[check(ghost)]
628        #[ensures(*self == match result@ { None => None, Some(r) => Some(*r) })]
629        #[ensures(^self == match result@ { None => None, Some(r) => Some(^r) })]
630        fn into_iter(self) -> IterMut<'a, T>;
631    }
632
633    impl<T> Default for Option<T> {
634        #[check(ghost)]
635        #[ensures(result == None)]
636        fn default() -> Option<T>;
637    }
638}
639
640impl<T: OrdLogic> OrdLogic for Option<T> {
641    #[logic(open)]
642    fn cmp_log(self, o: Self) -> Ordering {
643        match (self, o) {
644            (None, None) => Ordering::Equal,
645            (None, Some(_)) => Ordering::Less,
646            (Some(_), None) => Ordering::Greater,
647            (Some(x), Some(y)) => x.cmp_log(y),
648        }
649    }
650
651    ord_laws_impl! {}
652}
653
654impl<T> View for IntoIter<T> {
655    type ViewTy = Option<T>;
656
657    #[logic(opaque)]
658    fn view(self) -> Option<T> {
659        dead
660    }
661}
662
663impl<T> IteratorSpec for IntoIter<T> {
664    #[logic(open, prophetic)]
665    fn completed(&mut self) -> bool {
666        pearlite! { (*self)@ == None && resolve(self) }
667    }
668
669    #[logic(open)]
670    fn produces(self, visited: Seq<Self::Item>, o: Self) -> bool {
671        pearlite! {
672            visited == Seq::empty() && self == o ||
673            exists<e: Self::Item> self@ == Some(e) && visited == Seq::singleton(e) && o@ == None
674        }
675    }
676
677    #[logic(law)]
678    #[ensures(self.produces(Seq::empty(), self))]
679    fn produces_refl(self) {}
680
681    #[logic(law)]
682    #[requires(a.produces(ab, b))]
683    #[requires(b.produces(bc, c))]
684    #[ensures(a.produces(ab.concat(bc), c))]
685    fn produces_trans(a: Self, ab: Seq<Self::Item>, b: Self, bc: Seq<Self::Item>, c: Self) {}
686}
687
688impl<'a, T> View for Iter<'a, T> {
689    type ViewTy = Option<&'a T>;
690
691    #[logic(opaque)]
692    fn view(self) -> Option<&'a T> {
693        dead
694    }
695}
696
697impl<T> IteratorSpec for Iter<'_, T> {
698    #[logic(open, prophetic)]
699    fn completed(&mut self) -> bool {
700        pearlite! { (*self)@ == None && resolve(self) }
701    }
702
703    #[logic(open)]
704    fn produces(self, visited: Seq<Self::Item>, o: Self) -> bool {
705        pearlite! {
706            visited == Seq::empty() && self == o ||
707            exists<e: Self::Item> self@ == Some(e) && visited == Seq::singleton(e) && o@ == None
708        }
709    }
710
711    #[logic(law)]
712    #[ensures(self.produces(Seq::empty(), self))]
713    fn produces_refl(self) {}
714
715    #[logic(law)]
716    #[requires(a.produces(ab, b))]
717    #[requires(b.produces(bc, c))]
718    #[ensures(a.produces(ab.concat(bc), c))]
719    fn produces_trans(a: Self, ab: Seq<Self::Item>, b: Self, bc: Seq<Self::Item>, c: Self) {}
720}
721
722impl<'a, T> View for IterMut<'a, T> {
723    type ViewTy = Option<&'a mut T>;
724
725    #[logic(opaque)]
726    fn view(self) -> Option<&'a mut T> {
727        dead
728    }
729}
730
731impl<T> IteratorSpec for IterMut<'_, T> {
732    #[logic(open, prophetic)]
733    fn completed(&mut self) -> bool {
734        pearlite! { (*self)@ == None && resolve(self) }
735    }
736
737    #[logic(open)]
738    fn produces(self, visited: Seq<Self::Item>, o: Self) -> bool {
739        pearlite! {
740            visited == Seq::empty() && self == o ||
741            exists<e: Self::Item> self@ == Some(e) && visited == Seq::singleton(e) && o@ == None
742        }
743    }
744
745    #[logic(law)]
746    #[ensures(self.produces(Seq::empty(), self))]
747    fn produces_refl(self) {}
748
749    #[logic(law)]
750    #[requires(a.produces(ab, b))]
751    #[requires(b.produces(bc, c))]
752    #[ensures(a.produces(ab.concat(bc), c))]
753    fn produces_trans(a: Self, ab: Seq<Self::Item>, b: Self, bc: Seq<Self::Item>, c: Self) {}
754}
755
756pub trait OptionExt<T> {
757    /// Same as [`Option::unwrap`], but in logic.
758    #[logic]
759    #[requires(false)]
760    fn unwrap_logic(self) -> T;
761
762    /// Same as [`Option::and_then`], but in logic.
763    #[logic]
764    fn and_then_logic<U>(self, f: Mapping<T, Option<U>>) -> Option<U>;
765
766    /// Same as [`Option::map`], but in logic.
767    #[logic]
768    fn map_logic<U>(self, f: Mapping<T, U>) -> Option<U>;
769}
770
771impl<T> OptionExt<T> for Option<T> {
772    #[logic(open)]
773    #[requires(self != None)]
774    fn unwrap_logic(self) -> T {
775        match self {
776            Some(x) => x,
777            None => such_that(|_| true),
778        }
779    }
780
781    #[logic(open)]
782    fn and_then_logic<U>(self, f: Mapping<T, Option<U>>) -> Option<U> {
783        match self {
784            None => None,
785            Some(x) => f.get(x),
786        }
787    }
788
789    #[logic(open)]
790    fn map_logic<U>(self, f: Mapping<T, U>) -> Option<U> {
791        match self {
792            None => None,
793            Some(x) => Some(f.get(x)),
794        }
795    }
796}
creusot_std/std/option.rs

creusot_std/std/
option.rs
