creusot_contracts/std/
tuples.rs

1use crate::prelude::*;
2
3impl DeepModel for () {
4    type DeepModelTy = ();
5
6    #[logic(open, inline)]
7    fn deep_model(self) -> Self::DeepModelTy {
8        pearlite! { () }
9    }
10}
11
12macro_rules! tuple_impls {
13    ( $( ($name:ident, $idx:tt) )+ ) => {
14        impl<$($name: DeepModel),+> DeepModel for ($($name,)+) {
15            type DeepModelTy = ($($name::DeepModelTy,)+);
16
17            #[logic(open, inline)]
18            fn deep_model(self) -> Self::DeepModelTy {
19                pearlite! { ($(self.$idx.deep_model(),)+) }
20            }
21        }
22
23        extern_spec! {
24            impl<$($name: Default),+> Default for ($($name,)+) {
25                #[ensures($($name::default.postcondition((), result.$idx))&&+)]
26                fn default() -> ($($name,)+);
27            }
28        }
29    };
30}
31
32tuple_impls! { (T,0) }
33tuple_impls! { (U,0) (T,1) }
34tuple_impls! { (V,0) (U,1) (T,2) }
35tuple_impls! { (W,0) (V,1) (U,2) (T,3) }
36tuple_impls! { (X,0) (W,1) (V,2) (U,3) (T,4) }
37tuple_impls! { (Y,0) (X,1) (W,2) (V,3) (U,4) (T,5) }
38tuple_impls! { (Z,0) (Y,1) (X,2) (W,3) (V,4) (U,5) (T,6) }
39tuple_impls! { (A,0) (Z,1) (Y,2) (X,3) (W,4) (V,5) (U,6) (T,7) }
40tuple_impls! { (B,0) (A,1) (Z,2) (Y,3) (X,4) (W,5) (V,6) (U,7) (T,8) }
41tuple_impls! { (C,0) (B,1) (A,2) (Z,3) (Y,4) (X,5) (W,6) (V,7) (U,8) (T,9) }
42tuple_impls! { (D,0) (C,1) (B,2) (A,3) (Z,4) (Y,5) (X,6) (W,7) (V,8) (U,9) (T,10) }
43tuple_impls! { (E,0) (D,1) (C,2) (B,3) (A,4) (Z,5) (Y,6) (X,7) (W,8) (V,9) (U,10) (T,11) }
creusot_contracts/std/tuples.rs

creusot_contracts/std/
tuples.rs
