creusot_contracts/std/
ops.rs

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

creusot_contracts/std/
ops.rs
