creusot_std/std/
option.rs

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

creusot_std/std/
option.rs
