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

creusot_std/std/
ops.rs
