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

creusot_std/std/
ops.rs
