creusot_std/std/
option.rs

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

creusot_std/std/
option.rs
