creusot_contracts/std/
option.rs

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

creusot_contracts/std/
option.rs
