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

creusot_std/std/
option.rs
