creusot_std/std/
ops.rs

1use crate::prelude::*;
2#[cfg(creusot)]
3use core::convert::Infallible;
4#[cfg(feature = "nightly")]
5use core::marker::Tuple;
6use core::ops::*;
7
8// Note: we should NOT give a generic extern spec for Deref::deref, since this
9// method is an exception being used both as a logic function and as a program
10// function. See #1235.
11
12/// `FnOnceExt` is an extension trait for the `FnOnce` trait, used for
13/// adding a specification to closures. It should not be used directly.
14#[cfg(feature = "nightly")]
15pub trait FnOnceExt<Args: Tuple> {
16    type Output;
17
18    #[logic(prophetic)]
19    fn precondition(self, a: Args) -> bool;
20
21    #[logic(prophetic)]
22    fn postcondition_once(self, a: Args, res: Self::Output) -> bool;
23}
24
25#[cfg(not(feature = "nightly"))]
26pub trait FnOnceExt<Args> {
27    type Output;
28}
29
30/// `FnMutExt` is an extension trait for the `FnMut` trait, used for
31/// adding a specification to closures. It should not be used directly.
32#[cfg(feature = "nightly")]
33pub trait FnMutExt<Args: Tuple>: FnOnceExt<Args> {
34    #[logic(prophetic)]
35    fn postcondition_mut(self, _: Args, _: Self, _: Self::Output) -> bool;
36
37    #[logic(prophetic)]
38    fn hist_inv(self, _: Self) -> bool;
39
40    #[logic(law)]
41    #[requires(self.postcondition_mut(args, res_state, res))]
42    #[ensures(
43        #[trigger(self.postcondition_mut(args, res_state, res))]
44        #[trigger(self.hist_inv(res_state))]
45        self.hist_inv(res_state))]
46    fn postcondition_mut_hist_inv(self, args: Args, res_state: Self, res: Self::Output);
47
48    #[logic(law)]
49    #[ensures(#[trigger(self.hist_inv(self))] self.hist_inv(self))]
50    fn hist_inv_refl(self);
51
52    #[logic(law)]
53    #[requires(self.hist_inv(b))]
54    #[requires(b.hist_inv(c))]
55    #[ensures(
56        #[trigger(self.hist_inv(b), b.hist_inv(c))]
57        #[trigger(self.hist_inv(b), self.hist_inv(c))]
58        #[trigger(b.hist_inv(c), self.hist_inv(c))]
59        self.hist_inv(c))]
60    fn hist_inv_trans(self, b: Self, c: Self);
61
62    #[logic(law)]
63    #[ensures(#[trigger(self.postcondition_once(args, res))]
64        self.postcondition_once(args, res) ==
65              exists<res_state: Self> self.postcondition_mut(args, res_state, res) && resolve(res_state))]
66    fn fn_mut_once(self, args: Args, res: Self::Output);
67}
68
69#[cfg(not(feature = "nightly"))]
70pub trait FnMutExt<Args>: FnOnceExt<Args> {}
71
72/// `FnExt` is an extension trait for the `Fn` trait, used for
73/// adding a specification to closures. It should not be used directly.
74#[cfg(feature = "nightly")]
75pub trait FnExt<Args: Tuple>: FnMutExt<Args> {
76    #[logic(prophetic)]
77    fn postcondition(self, _: Args, _: Self::Output) -> bool;
78
79    #[logic(law)]
80    #[ensures(#[trigger(self.postcondition_mut(args, res_state, res))]
81        self.postcondition_mut(args, res_state, res) == (self.postcondition(args, res) && self == res_state))]
82    fn fn_mut(self, args: Args, res_state: Self, res: Self::Output);
83
84    #[logic(law)]
85    #[ensures(#[trigger(self.postcondition_once(args, res))]
86        self.postcondition_once(args, res) == (self.postcondition(args, res) && resolve(self)))]
87    fn fn_once(self, args: Args, res: Self::Output);
88
89    #[logic(law)]
90    #[ensures(#[trigger(self.hist_inv(res_state))] self.hist_inv(res_state) == (self == res_state))]
91    fn fn_hist_inv(self, res_state: Self);
92}
93
94/// `FnExt` is an extension trait for the `Fn` trait, used for
95/// adding a specification to closures. It should not be used directly.
96#[cfg(not(feature = "nightly"))]
97pub trait FnExt<Args>: FnMutExt<Args> {}
98
99#[cfg(feature = "nightly")]
100impl<Args: Tuple, F: ?Sized + FnOnce<Args>> FnOnceExt<Args> for F {
101    type Output = <Self as FnOnce<Args>>::Output;
102
103    #[logic(open, prophetic)]
104    #[allow(unused_variables)]
105    #[intrinsic("precondition")]
106    fn precondition(self, args: Args) -> bool {
107        dead
108    }
109
110    #[logic(open, prophetic)]
111    #[allow(unused_variables)]
112    #[intrinsic("postcondition_once")]
113    fn postcondition_once(self, args: Args, result: Self::Output) -> bool {
114        dead
115    }
116}
117
118#[cfg(feature = "nightly")]
119impl<Args: Tuple, F: ?Sized + FnMut<Args>> FnMutExt<Args> for F {
120    #[logic(open, prophetic)]
121    #[allow(unused_variables)]
122    #[intrinsic("postcondition_mut")]
123    fn postcondition_mut(self, args: Args, result_state: Self, result: Self::Output) -> bool {
124        dead
125    }
126
127    #[logic(open, prophetic)]
128    #[allow(unused_variables)]
129    #[intrinsic("hist_inv")]
130    fn hist_inv(self, result_state: Self) -> bool {
131        dead
132    }
133
134    #[trusted]
135    #[logic(law)]
136    #[requires(self.postcondition_mut(args, res_state, res))]
137    #[ensures(
138        #[trigger(self.postcondition_mut(args, res_state, res))]
139        #[trigger(self.hist_inv(res_state))]
140        self.hist_inv(res_state))]
141    fn postcondition_mut_hist_inv(self, args: Args, res_state: Self, res: Self::Output) {}
142
143    #[trusted]
144    #[logic(law)]
145    #[ensures(#[trigger(self.hist_inv(self))] self.hist_inv(self))]
146    fn hist_inv_refl(self) {}
147
148    #[trusted]
149    #[logic(law)]
150    #[requires(self.hist_inv(b))]
151    #[requires(b.hist_inv(c))]
152    #[ensures(
153        #[trigger(self.hist_inv(b), b.hist_inv(c))]
154        #[trigger(self.hist_inv(b), self.hist_inv(c))]
155        #[trigger(b.hist_inv(c), self.hist_inv(c))]
156        self.hist_inv(c))]
157    fn hist_inv_trans(self, b: Self, c: Self) {}
158
159    #[logic(law)]
160    #[trusted]
161    #[ensures(#[trigger(self.postcondition_once(args, res))]
162        self.postcondition_once(args, res) ==
163              exists<res_state: Self> self.postcondition_mut(args, res_state, res) && resolve(res_state))]
164    fn fn_mut_once(self, args: Args, res: Self::Output) {}
165}
166
167#[cfg(feature = "nightly")]
168impl<Args: Tuple, F: ?Sized + Fn<Args>> FnExt<Args> for F {
169    #[logic(open, prophetic)]
170    #[allow(unused_variables)]
171    #[intrinsic("postcondition")]
172    fn postcondition(self, args: Args, result: Self::Output) -> bool {
173        dead
174    }
175
176    #[logic(law)]
177    #[trusted]
178    #[ensures(#[trigger(self.postcondition_mut(args, res_state, res))]
179        self.postcondition_mut(args, res_state, res) == (self.postcondition(args, res) && self == res_state))]
180    fn fn_mut(self, args: Args, res_state: Self, res: Self::Output) {}
181
182    #[logic(law)]
183    #[trusted]
184    #[ensures(#[trigger(self.postcondition_once(args, res))]
185        self.postcondition_once(args, res) == (self.postcondition(args, res) && resolve(self)))]
186    fn fn_once(self, args: Args, res: Self::Output) {}
187
188    #[logic(law)]
189    #[trusted]
190    #[ensures(#[trigger(self.hist_inv(res_state))] self.hist_inv(res_state) == (self == res_state))]
191    fn fn_hist_inv(self, res_state: Self) {}
192}
193
194extern_spec! {
195    mod core {
196        mod ops {
197            trait FnOnce<Args> where Args: Tuple {
198                #[requires(self.precondition(arg))]
199                #[ensures(self.postcondition_once(arg, result))]
200                fn call_once(self, arg: Args) -> Self::Output;
201            }
202
203            trait FnMut<Args> where Args: Tuple {
204                #[requires((*self).precondition(arg))]
205                #[ensures((*self).postcondition_mut(arg, ^self, result))]
206                fn call_mut(&mut self, arg: Args) -> Self::Output;
207            }
208
209            trait Fn<Args> where Args: Tuple {
210                #[requires((*self).precondition(arg))]
211                #[ensures((*self).postcondition(arg, result))]
212                fn call(&self, arg: Args) -> Self::Output;
213            }
214
215            trait Deref {
216                #[check(ghost)]
217                #[requires(false)]
218                fn deref(&self) -> &Self::Target;
219            }
220
221            trait DerefMut {
222                #[check(ghost)]
223                #[requires(false)]
224                fn deref_mut(&mut self) -> &mut Self::Target;
225            }
226        }
227    }
228
229    impl<'a, T> Deref for &'a T {
230        #[check(ghost)]
231        #[ensures(*result == **self)]
232        fn deref<'b>(&'b self) -> &'b T {
233            *self
234        }
235    }
236
237    impl<'a, T> Deref for &'a mut T {
238        #[check(ghost)]
239        #[ensures(*result == **self)]
240        fn deref<'b>(&'b self) -> &'b T {
241            *self
242        }
243    }
244
245    impl<'a, T> DerefMut for &'a mut T {
246        #[check(ghost)]
247        #[ensures(*result == **self)]
248        #[ensures(^result == *^self)]
249        #[ensures(^*self == ^^self)]
250        fn deref_mut<'b>(&'b mut self) -> &'b mut T {
251            *self
252        }
253    }
254}
255
256impl<T: DeepModel> DeepModel for Bound<T> {
257    type DeepModelTy = Bound<T::DeepModelTy>;
258
259    #[logic(open)]
260    fn deep_model(self) -> Self::DeepModelTy {
261        match self {
262            Bound::Included(b) => Bound::Included(b.deep_model()),
263            Bound::Excluded(b) => Bound::Excluded(b.deep_model()),
264            Bound::Unbounded => Bound::Unbounded,
265        }
266    }
267}
268
269/// Methods for the specification of [`std::ops::RangeBounds`].
270pub trait RangeBounds<T: ?Sized + DeepModel<DeepModelTy: OrdLogic>>:
271    core::ops::RangeBounds<T>
272{
273    #[logic]
274    fn start_bound_logic(&self) -> Bound<&T>;
275
276    #[logic]
277    fn end_bound_logic(&self) -> Bound<&T>;
278}
279
280/// Membership to an interval `(Bound<T>, Bound<T>)`.
281#[logic(open)]
282pub fn between<T: OrdLogic>(lo: Bound<T>, item: T, hi: Bound<T>) -> bool {
283    lower_bound(lo, item) && upper_bound(item, hi)
284}
285
286/// Comparison with a lower bound.
287#[logic(open)]
288pub fn lower_bound<T: OrdLogic>(lo: Bound<T>, item: T) -> bool {
289    pearlite! {
290        match lo {
291            Bound::Included(lo) => lo <= item,
292            Bound::Excluded(lo) => lo < item,
293            Bound::Unbounded => true,
294        }
295    }
296}
297
298/// Comparison with an upper bound.
299#[logic(open)]
300pub fn upper_bound<T: OrdLogic>(item: T, hi: Bound<T>) -> bool {
301    pearlite! {
302        match hi {
303            Bound::Included(hi) => item <= hi,
304            Bound::Excluded(lo) => lo < item,
305            Bound::Unbounded => true,
306        }
307    }
308}
309
310extern_spec! {
311    mod core {
312        mod ops {
313            trait RangeBounds<T>
314            where
315                Self: RangeBounds<T>,
316                T: ?Sized + DeepModel,
317                T::DeepModelTy: OrdLogic,
318            {
319                #[ensures(result == self.start_bound_logic())]
320                fn start_bound(&self) -> Bound<&T>;
321
322                #[ensures(result == self.end_bound_logic())]
323                fn end_bound(&self) -> Bound<&T>;
324
325                #[ensures(result == between(self.start_bound_logic().deep_model(), item.deep_model(), self.end_bound_logic().deep_model()))]
326                fn contains<U>(&self, item: &U) -> bool
327                where
328                    T: PartialOrd<U>,
329                    U: ?Sized + PartialOrd<T> + DeepModel<DeepModelTy = T::DeepModelTy>;
330
331                #[ensures(result == !exists<item: T::DeepModelTy> between(self.start_bound_logic().deep_model(), item, self.end_bound_logic().deep_model()))]
332                fn is_empty(&self) -> bool
333                where T: PartialOrd;
334            }
335        }
336    }
337
338    impl<T: Copy> Bound<&T> {
339        #[erasure]
340        #[ensures(result == match self {
341            Bound::Unbounded => Bound::Unbounded,
342            Bound::Included(x) => Bound::Included(*x),
343            Bound::Excluded(x) => Bound::Excluded(*x),
344        })]
345        fn copied(self) -> Bound<T> {
346            match self {
347                Bound::Unbounded => Bound::Unbounded,
348                Bound::Included(x) => Bound::Included(*x),
349                Bound::Excluded(x) => Bound::Excluded(*x),
350            }
351        }
352    }
353}
354
355impl<T: DeepModel<DeepModelTy: OrdLogic>> RangeBounds<T> for RangeFull {
356    #[logic(open)]
357    fn start_bound_logic(&self) -> Bound<&T> {
358        Bound::Unbounded
359    }
360
361    #[logic(open)]
362    fn end_bound_logic(&self) -> Bound<&T> {
363        Bound::Unbounded
364    }
365}
366
367impl<T: DeepModel<DeepModelTy: OrdLogic>> RangeBounds<T> for RangeFrom<T> {
368    #[logic(open)]
369    fn start_bound_logic(&self) -> Bound<&T> {
370        Bound::Included(&self.start)
371    }
372
373    #[logic(open)]
374    fn end_bound_logic(&self) -> Bound<&T> {
375        Bound::Unbounded
376    }
377}
378
379impl<T: DeepModel<DeepModelTy: OrdLogic>> RangeBounds<T> for RangeTo<T> {
380    #[logic(open)]
381    fn start_bound_logic(&self) -> Bound<&T> {
382        Bound::Unbounded
383    }
384
385    #[logic(open)]
386    fn end_bound_logic(&self) -> Bound<&T> {
387        Bound::Excluded(&self.end)
388    }
389}
390
391impl<T: DeepModel<DeepModelTy: OrdLogic>> RangeBounds<T> for Range<T> {
392    #[logic(open)]
393    fn start_bound_logic(&self) -> Bound<&T> {
394        Bound::Included(&self.start)
395    }
396
397    #[logic(open)]
398    fn end_bound_logic(&self) -> Bound<&T> {
399        Bound::Excluded(&self.end)
400    }
401}
402
403impl<T: DeepModel<DeepModelTy: OrdLogic>> RangeBounds<T> for RangeInclusive<T> {
404    #[logic(open)]
405    fn start_bound_logic(&self) -> Bound<&T> {
406        Bound::Included(&self.start_log())
407    }
408
409    #[logic(opaque)]
410    fn end_bound_logic(&self) -> Bound<&T> {
411        dead
412    }
413}
414
415impl<T: DeepModel<DeepModelTy: OrdLogic>> RangeBounds<T> for RangeToInclusive<T> {
416    #[logic(open)]
417    fn start_bound_logic(&self) -> Bound<&T> {
418        Bound::Unbounded
419    }
420
421    #[logic(open)]
422    fn end_bound_logic(&self) -> Bound<&T> {
423        Bound::Included(&self.end)
424    }
425}
426
427impl<T: DeepModel<DeepModelTy: OrdLogic>> RangeBounds<T> for (Bound<T>, Bound<T>) {
428    #[logic(open)]
429    fn start_bound_logic(&self) -> Bound<&T> {
430        match *self {
431            (Bound::Included(ref start), _) => Bound::Included(start),
432            (Bound::Excluded(ref start), _) => Bound::Excluded(start),
433            (Bound::Unbounded, _) => Bound::Unbounded,
434        }
435    }
436
437    #[logic(open)]
438    fn end_bound_logic(&self) -> Bound<&T> {
439        match *self {
440            (_, Bound::Included(ref end)) => Bound::Included(end),
441            (_, Bound::Excluded(ref end)) => Bound::Excluded(end),
442            (_, Bound::Unbounded) => Bound::Unbounded,
443        }
444    }
445}
446
447impl<'a, T: ?Sized + 'a + DeepModel<DeepModelTy: OrdLogic>> RangeBounds<T>
448    for (Bound<&'a T>, Bound<&'a T>)
449{
450    #[logic(open)]
451    fn start_bound_logic(&self) -> Bound<&T> {
452        self.0
453    }
454
455    #[logic(open)]
456    fn end_bound_logic(&self) -> Bound<&T> {
457        self.1
458    }
459}
460
461impl<T: DeepModel<DeepModelTy: OrdLogic>> RangeBounds<T> for RangeFrom<&T> {
462    #[logic(open)]
463    fn start_bound_logic(&self) -> Bound<&T> {
464        Bound::Included(self.start)
465    }
466
467    #[logic(open)]
468    fn end_bound_logic(&self) -> Bound<&T> {
469        Bound::Unbounded
470    }
471}
472
473impl<T: DeepModel<DeepModelTy: OrdLogic>> RangeBounds<T> for RangeTo<&T> {
474    #[logic(open)]
475    fn start_bound_logic(&self) -> Bound<&T> {
476        Bound::Unbounded
477    }
478
479    #[logic(open)]
480    fn end_bound_logic(&self) -> Bound<&T> {
481        Bound::Excluded(self.end)
482    }
483}
484
485impl<T: DeepModel<DeepModelTy: OrdLogic>> RangeBounds<T> for Range<&T> {
486    #[logic(open)]
487    fn start_bound_logic(&self) -> Bound<&T> {
488        Bound::Included(self.start)
489    }
490
491    #[logic(open)]
492    fn end_bound_logic(&self) -> Bound<&T> {
493        Bound::Excluded(self.end)
494    }
495}
496
497// I don't know why this impl is different from the one for `RangeInclusive<T>`.
498impl<T: DeepModel<DeepModelTy: OrdLogic>> RangeBounds<T> for RangeInclusive<&T> {
499    #[logic(open)]
500    fn start_bound_logic(&self) -> Bound<&T> {
501        Bound::Included(&self.start_log())
502    }
503
504    #[logic(open)]
505    fn end_bound_logic(&self) -> Bound<&T> {
506        Bound::Included(&self.end_log())
507    }
508}
509
510impl<T: DeepModel<DeepModelTy: OrdLogic>> RangeBounds<T> for RangeToInclusive<&T> {
511    #[logic(open)]
512    fn start_bound_logic(&self) -> Bound<&T> {
513        Bound::Unbounded
514    }
515
516    #[logic(open)]
517    fn end_bound_logic(&self) -> Bound<&T> {
518        Bound::Included(self.end)
519    }
520}
521
522#[cfg(feature = "nightly")]
523impl<T: DeepModel<DeepModelTy: OrdLogic>> RangeBounds<T> for core::range::Range<T> {
524    #[logic(open)]
525    fn start_bound_logic(&self) -> Bound<&T> {
526        Bound::Included(&self.start)
527    }
528
529    #[logic(open)]
530    fn end_bound_logic(&self) -> Bound<&T> {
531        Bound::Excluded(&self.end)
532    }
533}
534
535#[cfg(feature = "nightly")]
536impl<T: DeepModel<DeepModelTy: OrdLogic>> RangeBounds<T> for core::range::Range<&T> {
537    #[logic(open)]
538    fn start_bound_logic(&self) -> Bound<&T> {
539        Bound::Included(self.start)
540    }
541
542    #[logic(open)]
543    fn end_bound_logic(&self) -> Bound<&T> {
544        Bound::Excluded(self.end)
545    }
546}
547
548#[cfg(feature = "nightly")]
549impl<T: DeepModel<DeepModelTy: OrdLogic>> RangeBounds<T> for core::range::RangeFrom<T> {
550    #[logic(open)]
551    fn start_bound_logic(&self) -> Bound<&T> {
552        Bound::Included(&self.start)
553    }
554
555    #[logic(open)]
556    fn end_bound_logic(&self) -> Bound<&T> {
557        Bound::Unbounded
558    }
559}
560
561#[cfg(feature = "nightly")]
562impl<T: DeepModel<DeepModelTy: OrdLogic>> RangeBounds<T> for core::range::RangeFrom<&T> {
563    #[logic(open)]
564    fn start_bound_logic(&self) -> Bound<&T> {
565        Bound::Included(self.start)
566    }
567
568    #[logic(open)]
569    fn end_bound_logic(&self) -> Bound<&T> {
570        Bound::Unbounded
571    }
572}
573
574#[cfg(feature = "nightly")]
575impl<T: DeepModel<DeepModelTy: OrdLogic>> RangeBounds<T> for core::range::RangeInclusive<T> {
576    #[logic(open)]
577    fn start_bound_logic(&self) -> Bound<&T> {
578        Bound::Included(&self.start)
579    }
580
581    #[logic(open)]
582    fn end_bound_logic(&self) -> Bound<&T> {
583        Bound::Included(&self.last)
584    }
585}
586
587#[cfg(feature = "nightly")]
588impl<T: DeepModel<DeepModelTy: OrdLogic>> RangeBounds<T> for core::range::RangeInclusive<&T> {
589    #[logic(open)]
590    fn start_bound_logic(&self) -> Bound<&T> {
591        Bound::Included(self.start)
592    }
593
594    #[logic(open)]
595    fn end_bound_logic(&self) -> Bound<&T> {
596        Bound::Included(self.last)
597    }
598}
599
600pub trait RangeInclusiveExt<Idx> {
601    #[logic]
602    fn new_log(start: Idx, end: Idx) -> Self
603    where
604        Idx: DeepModel,
605        Idx::DeepModelTy: OrdLogic;
606
607    #[logic]
608    fn start_log(self) -> Idx;
609
610    #[logic]
611    fn end_log(self) -> Idx;
612
613    #[logic]
614    fn is_empty_log(self) -> bool
615    where
616        Idx: DeepModel,
617        Idx::DeepModelTy: OrdLogic;
618}
619
620impl<Idx> RangeInclusiveExt<Idx> for RangeInclusive<Idx> {
621    #[logic(opaque)]
622    #[trusted]
623    #[ensures(start == result.start_log())]
624    #[ensures(end == result.end_log())]
625    #[ensures(start.deep_model() <= end.deep_model() ==> !result.is_empty_log())]
626    fn new_log(start: Idx, end: Idx) -> Self
627    where
628        Idx: DeepModel,
629        Idx::DeepModelTy: OrdLogic,
630    {
631        dead
632    }
633
634    #[logic(opaque)]
635    fn start_log(self) -> Idx {
636        dead
637    }
638
639    #[logic(opaque)]
640    fn end_log(self) -> Idx {
641        dead
642    }
643
644    #[logic(opaque)]
645    #[trusted]
646    #[ensures(!result ==> self.start_log().deep_model() <= self.end_log().deep_model())]
647    fn is_empty_log(self) -> bool
648    where
649        Idx: DeepModel,
650        Idx::DeepModelTy: OrdLogic,
651    {
652        dead
653    }
654}
655
656extern_spec! {
657    impl<Idx> RangeInclusive<Idx> {
658        #[ensures(result.start_log() == start)]
659        #[ensures(result.end_log() == end)]
660        #[ensures(start.deep_model() <= end.deep_model() ==> !result.is_empty_log())]
661        fn new(start: Idx, end: Idx) -> Self
662            where Idx: DeepModel, Idx::DeepModelTy: OrdLogic;
663
664        #[ensures(*result == self.start_log())]
665        fn start(&self) -> &Idx;
666
667        #[ensures(*result == self.end_log())]
668        fn end(&self) -> &Idx;
669    }
670
671    impl<Idx: PartialOrd<Idx> + DeepModel> RangeInclusive<Idx>
672    where Idx::DeepModelTy: OrdLogic
673    {
674        #[ensures(result == self.is_empty_log())]
675        fn is_empty(&self) -> bool;
676    }
677}
678
679extern_spec! {
680    mod core {
681        mod ops {
682            trait FromResidual<R> where Self: Sized {
683                #[requires(true)]
684                fn from_residual(residual: R) -> Self;
685            }
686        }
687    }
688
689    impl<T> Try for Option<T> {
690        #[ensures(result == Some(output))]
691        fn from_output(output: T) -> Self {
692            Some(output)
693        }
694
695        #[ensures(match self {
696            Some(v) => result == ControlFlow::Continue(v),
697            None => result == ControlFlow::Break(None)
698        })]
699        fn branch(self) -> ControlFlow<Option<Infallible>, T> {
700            match self {
701                Some(v) => ControlFlow::Continue(v),
702                None => ControlFlow::Break(None),
703            }
704        }
705    }
706
707    impl<T> FromResidual<Option<Infallible>> for Option<T> {
708        #[ensures(result == None)]
709        fn from_residual(residual: Option<Infallible>) -> Self {
710            match residual {
711                None => None,
712            }
713        }
714    }
715
716    impl<T, E> Try for Result<T, E> {
717        #[ensures(result == Ok(output))]
718        fn from_output(output: T) -> Self {
719            Ok(output)
720        }
721
722        #[ensures(match self {
723            Ok(v) => result == ControlFlow::Continue(v),
724            Err(e) => result == ControlFlow::Break(Err(e))
725        })]
726        fn branch(self) -> ControlFlow<Result<Infallible, E>, T> {
727            match self {
728                Ok(v) => ControlFlow::Continue(v),
729                Err(e) => ControlFlow::Break(Err(e)),
730            }
731        }
732    }
733
734    impl<T, E, F: From<E>> FromResidual<Result<Infallible, E>> for Result<T, F> {
735        #[ensures(match (result, residual) {
736            (Err(result), Err(residual)) => F::from.postcondition((residual,), result),
737            _ => false,
738        })]
739        fn from_residual(residual: Result<Infallible, E>) -> Self {
740            match residual {
741                Err(e) => Err(core::convert::From::from(e)),
742            }
743        }
744    }
745}
746
747// Specification stub for `residual_into_try_type`, used by the `try` desugarization.
748#[cfg(creusot)]
749#[allow(dead_code)]
750#[ensures(FromResidual::from_residual.postcondition((r,), result))]
751#[intrinsic("residual_into_try_type")]
752#[creusot::extern_spec]
753fn residual_into_try_type<R: Residual<O>, O>(r: R) -> <R as Residual<O>>::TryType {
754    FromResidual::from_residual(r)
755}
756
757/// Dummy impls that don't use the unstable traits Tuple, FnOnce<Args>, FnMut<Args>, Fn<Args>
758#[cfg(not(feature = "nightly"))]
759mod impls {
760    use crate::std::ops::*;
761
762    impl<O, F: FnOnce() -> O> FnOnceExt<()> for F {
763        type Output = O;
764    }
765    impl<O, F: FnMut() -> O> FnMutExt<()> for F {}
766    impl<O, F: Fn() -> O> FnExt<()> for F {}
767
768    macro_rules! impl_fn {
769        ( $( $tuple:tt ),+ ) => {
770            impl<$($tuple),+, O, F: FnOnce($($tuple),+) -> O> FnOnceExt<($($tuple),+,)> for F {
771                type Output = O;
772            }
773            impl<$($tuple),+, O, F: FnMut($($tuple),+) -> O> FnMutExt<($($tuple),+,)> for F {}
774            impl<$($tuple),+, O, F: Fn($($tuple),+) -> O> FnExt<($($tuple),+,)> for F {}
775        };
776    }
777
778    impl_fn! { A1 }
779    impl_fn! { A1, A2 }
780    impl_fn! { A1, A2, A3 }
781    impl_fn! { A1, A2, A3, A4 }
782    impl_fn! { A1, A2, A3, A4, A5 }
783    impl_fn! { A1, A2, A3, A4, A5, A6 }
784    impl_fn! { A1, A2, A3, A4, A5, A6, A7 }
785    impl_fn! { A1, A2, A3, A4, A5, A6, A7, A8 }
786    impl_fn! { A1, A2, A3, A4, A5, A6, A7, A8, A9 }
787}
creusot_std/std/ops.rs

creusot_std/std/
ops.rs
