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

creusot_std/std/
option.rs
