creusot_std/std/
convert.rs

1use crate::prelude::*;
2#[cfg(all(creusot, feature = "std"))]
3use alloc::alloc::Allocator;
4#[cfg(all(creusot, not(feature = "std")))]
5use alloc::boxed::Box;
6
7extern_spec! {
8    mod core {
9        mod convert {
10            trait From<T> where Self: From<T> {
11                // #[requires(true)]
12                fn from(value: T) -> Self;
13            }
14        }
15    }
16
17    impl<T> From<T> for T {
18        #[check(ghost)]
19        #[ensures(result == self)]
20        fn from(self) -> T;
21    }
22
23    impl<T, U> Into<U> for T
24    where
25        U: From<T>,
26    {
27        // FIXME: inherit terminates/ghost status
28        #[requires(<U as From<T>>::from.precondition((self,)))]
29        #[ensures(<U as From<T>>::from.postcondition((self,), result))]
30        fn into(self) -> U {
31            U::from(self)
32        }
33    }
34
35    impl<T> From<T> for Option<T> {
36        #[check(ghost)]
37        #[ensures(result == Some(x))]
38        fn from(x: T) -> Self;
39    }
40
41    impl<T> From<T> for Box<T> {
42        #[check(ghost)]
43        #[ensures(*result == x)]
44        fn from(x: T) -> Self;
45    }
46
47    impl<T: Clone> From<&[T]> for Box<[T]>
48    {
49        // FIXME: inherit ghost/terminates from clone
50        #[ensures(result@.len() == s@.len())]
51        #[ensures(forall<i> 0 <= i && i < s@.len() ==> <T as Clone>::clone.postcondition((&s@[i],), result@[i]))]
52        fn from(s: &[T]) -> Self;
53        // To verify: uses CloneToUninit
54    }
55
56    impl<T: Clone> From<&mut [T]> for Box<[T]>
57    {
58        // FIXME: inherit ghost/terminates from clone
59        #[ensures(result@.len() == s@.len())]
60        #[ensures(forall<i> 0 <= i && i < s@.len() ==> <T as Clone>::clone.postcondition((&s@[i],), result@[i]))]
61        #[ensures(^s == *s)]
62        fn from(s: &mut [T]) -> Self {
63            Box::<[T]>::from(&*s)
64        }
65    }
66
67    impl<T, const N: usize> From<[T; N]> for Box<[T]> {
68        #[check(ghost)]
69        #[ensures(result@ == s@)]
70        fn from(s: [T; N]) -> Self {
71            Box::new(s)
72        }
73    }
74}
75
76#[cfg(feature = "std")]
77extern_spec! {
78    impl<T: Clone> From<&[T]> for Vec<T>
79    {
80        // FIXME: inherit ghost/terminates from clone
81        #[ensures(result@.len() == s@.len())]
82        #[ensures(forall<i> 0 <= i && i < s@.len() ==> <T as Clone>::clone.postcondition((&s@[i],), result@[i]))]
83        fn from(s: &[T]) -> Self {
84            s.to_vec()
85        }
86    }
87
88    impl<T: Clone> From<&mut [T]> for Vec<T>
89    {
90        // FIXME: inherit ghost/terminates from clone
91        #[ensures(result@.len() == s@.len())]
92        #[ensures(forall<i> 0 <= i && i < s@.len() ==> <T as Clone>::clone.postcondition((&s@[i],), result@[i]))]
93        #[ensures(^s == *s)]
94        fn from(s: &mut [T]) -> Self {
95            s.to_vec()
96        }
97    }
98
99    impl<T, A: Allocator> From<Box<[T], A>> for Vec<T, A> {
100        #[check(ghost)]
101        #[ensures(result@ == s@)]
102        fn from(s: Box<[T], A>) -> Self {
103            s.into_vec()
104        }
105    }
106
107    impl<T: Clone, const N: usize> From<&[T; N]> for Vec<T> {
108        // FIXME: inherit ghost/terminates from clone
109        #[ensures(result@.len() == N@)]
110        #[ensures(forall<i> 0 <= i && i < s@.len() ==> <T as Clone>::clone.postcondition((&s@[i],), result@[i]))]
111        fn from(s: &[T; N]) -> Self {
112            Vec::<T>::from(s.as_slice())
113        }
114    }
115
116    impl<T: Clone, const N: usize> From<&mut [T; N]> for Vec<T> {
117        // FIXME: inherit ghost/terminates from clone
118        #[ensures(result@.len() == N@)]
119        #[ensures(forall<i> 0 <= i && i < s@.len() ==> <T as Clone>::clone.postcondition((&s@[i],), result@[i]))]
120        #[ensures(^s == *s)]
121        fn from(s: &mut [T; N]) -> Self {
122            Vec::<T>::from(s.as_mut_slice())
123        }
124    }
125
126    impl<T, const N: usize> From<[T; N]> for Vec<T> {
127        #[check(ghost)]
128        #[ensures(result@ == s@)]
129        fn from(s: [T; N]) -> Self {
130            <[T]>::into_vec(Box::new(s))
131        }
132    }
133
134    impl<T, A: Allocator> From<Vec<T, A>> for Box<[T], A> {
135        #[check(ghost)]
136        #[ensures(result@ == v@)]
137        fn from(v: Vec<T, A>) -> Self {
138            v.into_boxed_slice()
139        }
140    }
141}
142
143macro_rules! spec_from {
144    ($src:ty => $tgt:ty) => {
145        extern_spec! {
146            impl From<$src> for $tgt {
147                #[check(ghost)]
148                #[ensures(result == (small as Self))]
149                fn from(small: $src) -> Self {
150                    small as Self
151                }
152            }
153        }
154    };
155}
156
157spec_from!(bool => u8);
158spec_from!(bool => u16);
159spec_from!(bool => u32);
160spec_from!(bool => u64);
161spec_from!(bool => u128);
162spec_from!(bool => usize);
163spec_from!(bool => i8);
164spec_from!(bool => i16);
165spec_from!(bool => i32);
166spec_from!(bool => i64);
167spec_from!(bool => i128);
168spec_from!(bool => isize);
169
170// unsigned -> unsigned
171spec_from!(u8 => u16);
172spec_from!(u8 => u32);
173spec_from!(u8 => u64);
174spec_from!(u8 => u128);
175spec_from!(u8 => usize);
176spec_from!(u16 => u32);
177spec_from!(u16 => u64);
178spec_from!(u16 => u128);
179spec_from!(u16 => usize);
180spec_from!(u32 => u64);
181spec_from!(u32 => u128);
182spec_from!(u64 => u128);
183
184// signed -> signed
185spec_from!(i8 => i16);
186spec_from!(i8 => i32);
187spec_from!(i8 => i64);
188spec_from!(i8 => i128);
189spec_from!(i8 => isize);
190spec_from!(i16 => i32);
191spec_from!(i16 => i64);
192spec_from!(i16 => i128);
193spec_from!(i16 => isize);
194spec_from!(i32 => i64);
195spec_from!(i32 => i128);
196spec_from!(i64 => i128);
197
198// unsigned -> signed
199spec_from!(u8 => i16);
200spec_from!(u8 => i32);
201spec_from!(u8 => i64);
202spec_from!(u8 => i128);
203spec_from!(u8 => isize);
204spec_from!(u16 => i32);
205spec_from!(u16 => i64);
206spec_from!(u16 => i128);
207spec_from!(u32 => i64);
208spec_from!(u32 => i128);
209spec_from!(u64 => i128);
creusot_std/std/convert.rs

creusot_std/std/
convert.rs
