creusot_std/std/
convert.rs

1use crate::prelude::*;
2#[cfg(creusot)]
3use core::marker::PointeeSized;
4#[cfg(all(creusot, feature = "std"))]
5use std::alloc::Allocator;
6
7extern_spec! {
8    mod core {
9        mod convert {
10            trait AsRef<T: PointeeSized>: PointeeSized {
11                fn as_ref(&self) -> &T;
12            }
13
14            trait AsMut<T: PointeeSized>: PointeeSized {
15                fn as_mut(&mut self) -> &mut T;
16            }
17
18            trait From<T> {
19                fn from(value: T) -> Self;
20            }
21        }
22    }
23
24    impl<'a, T: ?Sized, U: ?Sized> AsRef<U> for &'a T
25    where
26        T: AsRef<U>,
27    {
28        #[requires(<T as AsRef<U>>::as_ref.precondition((*self,)))]
29        #[ensures(<T as AsRef<U>>::as_ref.postcondition((*self,), result))]
30        fn as_ref<'b>(&'b self) -> &'b U {
31            <T as AsRef<U>>::as_ref(*self)
32        }
33    }
34
35    impl<'a, T: ?Sized, U: ?Sized> AsRef<U> for &'a mut T
36    where
37        T: AsRef<U>,
38    {
39        #[requires(<T as AsRef<U>>::as_ref.precondition((*self,)))]
40        #[ensures(<T as AsRef<U>>::as_ref.postcondition((*self,), result))]
41        fn as_ref<'b>(&'b self) -> &'b U {
42            <T as AsRef<U>>::as_ref(*self)
43        }
44    }
45
46    impl<T> AsRef<[T]> for [T] {
47        #[check(ghost)]
48        #[ensures(result == self)]
49        fn as_ref(&self) -> &[T] {
50            self
51        }
52    }
53
54    impl AsRef<str> for str {
55        #[check(ghost)]
56        #[ensures(result == self)]
57        fn as_ref(&self) -> &str {
58            self
59        }
60    }
61
62    impl<'a, T: ?Sized, U: ?Sized> AsMut<U> for &'a mut T
63    where
64        T: AsMut<U>,
65    {
66        #[requires(<T as AsMut<U>>::as_mut.precondition((*self,)))]
67        #[ensures(^*self == ^^self)]
68        #[ensures(exists<s: &mut T> *s == **self && ^s == *^self &&
69            <T as AsMut<U>>::as_mut.postcondition((s,), result)
70        )]
71        fn as_mut<'b>(&'b mut self) -> &'b mut U {
72            (*self).as_mut()
73        }
74    }
75
76    impl<T> AsMut<[T]> for [T] {
77        #[check(ghost)]
78        #[ensures(result == self)]
79        fn as_mut(&mut self) -> &mut [T] {
80            self
81        }
82    }
83
84    impl AsMut<str> for str {
85        #[check(ghost)]
86        #[ensures(result == self)]
87        fn as_mut(&mut self) -> &mut str {
88            self
89        }
90    }
91
92    impl<T> From<T> for T {
93        #[check(ghost)]
94        #[ensures(result == self)]
95        fn from(self) -> T;
96    }
97
98    impl<T, U: From<T>> Into<U> for T {
99        // FIXME: inherit terminates/ghost status
100        #[requires(<U as From<T>>::from.precondition((self,)))]
101        #[ensures(<U as From<T>>::from.postcondition((self,), result))]
102        fn into(self) -> U {
103            U::from(self)
104        }
105    }
106
107    impl<T> From<T> for Option<T> {
108        #[check(ghost)]
109        #[ensures(result == Some(x))]
110        fn from(x: T) -> Self;
111    }
112
113    impl<T, U: TryFrom<T>> TryInto<U> for T {
114        #[requires(U::try_from.precondition((self,)))]
115        #[ensures(U::try_from.postcondition((self,), result))]
116        fn try_into(self) -> Result<U, U::Error> {
117            U::try_from(self)
118        }
119    }
120}
121
122#[cfg(feature = "std")]
123extern_spec! {
124    impl<T> From<T> for Box<T> {
125        #[check(ghost)]
126        #[ensures(*result == x)]
127        fn from(x: T) -> Self;
128    }
129
130    impl<T: Clone> From<&[T]> for Box<[T]>
131    {
132        // FIXME: inherit ghost/terminates from clone
133        #[ensures(result@.len() == s@.len())]
134        #[ensures(forall<i> 0 <= i && i < s@.len() ==> <T as Clone>::clone.postcondition((&s@[i],), result@[i]))]
135        fn from(s: &[T]) -> Self;
136        // To verify: uses CloneToUninit
137    }
138
139    impl<T: Clone> From<&mut [T]> for Box<[T]>
140    {
141        // FIXME: inherit ghost/terminates from clone
142        #[ensures(result@.len() == s@.len())]
143        #[ensures(forall<i> 0 <= i && i < s@.len() ==> <T as Clone>::clone.postcondition((&s@[i],), result@[i]))]
144        #[ensures(^s == *s)]
145        fn from(s: &mut [T]) -> Self {
146            Box::<[T]>::from(&*s)
147        }
148    }
149
150    impl<T, const N: usize> From<[T; N]> for Box<[T]> {
151        #[check(ghost)]
152        #[ensures(result@ == s@)]
153        fn from(s: [T; N]) -> Self {
154            Box::new(s)
155        }
156    }
157
158    impl<T: Clone> From<&[T]> for Vec<T>
159    {
160        // FIXME: inherit ghost/terminates from clone
161        #[ensures(result@.len() == s@.len())]
162        #[ensures(forall<i> 0 <= i && i < s@.len() ==> <T as Clone>::clone.postcondition((&s@[i],), result@[i]))]
163        fn from(s: &[T]) -> Self {
164            s.to_vec()
165        }
166    }
167
168    impl<T: Clone> From<&mut [T]> for Vec<T>
169    {
170        // FIXME: inherit ghost/terminates from clone
171        #[ensures(result@.len() == s@.len())]
172        #[ensures(forall<i> 0 <= i && i < s@.len() ==> <T as Clone>::clone.postcondition((&s@[i],), result@[i]))]
173        #[ensures(^s == *s)]
174        fn from(s: &mut [T]) -> Self {
175            s.to_vec()
176        }
177    }
178
179    impl<T, A: Allocator> From<Box<[T], A>> for Vec<T, A> {
180        #[check(ghost)]
181        #[ensures(result@ == s@)]
182        fn from(s: Box<[T], A>) -> Self {
183            s.into_vec()
184        }
185    }
186
187    impl<T: Clone, const N: usize> From<&[T; N]> for Vec<T> {
188        // FIXME: inherit ghost/terminates from clone
189        #[ensures(result@.len() == N@)]
190        #[ensures(forall<i> 0 <= i && i < s@.len() ==> <T as Clone>::clone.postcondition((&s@[i],), result@[i]))]
191        fn from(s: &[T; N]) -> Self {
192            Vec::<T>::from(s.as_slice())
193        }
194    }
195
196    impl<T: Clone, const N: usize> From<&mut [T; N]> for Vec<T> {
197        // FIXME: inherit ghost/terminates from clone
198        #[ensures(result@.len() == N@)]
199        #[ensures(forall<i> 0 <= i && i < s@.len() ==> <T as Clone>::clone.postcondition((&s@[i],), result@[i]))]
200        #[ensures(^s == *s)]
201        fn from(s: &mut [T; N]) -> Self {
202            Vec::<T>::from(s.as_mut_slice())
203        }
204    }
205
206    impl<T, const N: usize> From<[T; N]> for Vec<T> {
207        #[check(ghost)]
208        #[ensures(result@ == s@)]
209        fn from(s: [T; N]) -> Self {
210            <[T]>::into_vec(Box::new(s))
211        }
212    }
213
214    impl<T, A: Allocator> From<Vec<T, A>> for Box<[T], A> {
215        #[check(ghost)]
216        #[ensures(result@ == v@)]
217        fn from(v: Vec<T, A>) -> Self {
218            v.into_boxed_slice()
219        }
220    }
221
222    impl From<&String> for String {
223        #[check(ghost)]
224        #[ensures(result@ == s@)]
225        fn from(s: &String) -> Self;
226    }
227
228    impl From<Box<str>> for String {
229        #[check(ghost)]
230        #[ensures(result@ == s@)]
231        fn from(s: Box<str>) -> Self;
232    }
233
234    impl From<String> for Box<str> {
235        #[check(ghost)]
236        #[ensures(result@ == s@)]
237        fn from(s: String) -> Self;
238    }
239
240    impl From<&str> for String {
241        #[check(ghost)]
242        #[ensures(result@ == s@)]
243        fn from(s: &str) -> Self;
244    }
245
246    impl From<&mut str> for String {
247        #[check(ghost)]
248        #[ensures(result@ == s@ && ^s == *s)]
249        fn from(s: &mut String) -> Self;
250    }
251
252    impl From<&mut str> for Box<str> {
253        #[check(ghost)]
254        #[ensures(result@ == s@ && ^s == *s)]
255        fn from(s: &mut str) -> Self;
256    }
257
258    impl From<char> for String {
259        #[check(ghost)]
260        #[ensures(result@ == seq![c])]
261        fn from(c: char) -> Self;
262    }
263
264    impl From<String> for Vec<u8> {
265        #[check(ghost)]
266        #[ensures(result@ == s@.to_bytes())]
267        fn from(s: String) -> Self;
268    }
269
270    impl From<&str> for Vec<u8> {
271        #[check(ghost)]
272        #[ensures(result@ == s@.to_bytes())]
273        fn from(s: &str) -> Self;
274    }
275}
276
277macro_rules! spec_from {
278    ($src:ty => $tgt:ty) => {
279        extern_spec! {
280            impl From<$src> for $tgt {
281                #[check(ghost)]
282                #[ensures(result == (small as Self))]
283                fn from(small: $src) -> Self {
284                    small as Self
285                }
286            }
287        }
288    };
289}
290
291spec_from!(bool => u8);
292spec_from!(bool => u16);
293spec_from!(bool => u32);
294spec_from!(bool => u64);
295spec_from!(bool => u128);
296spec_from!(bool => usize);
297spec_from!(bool => i8);
298spec_from!(bool => i16);
299spec_from!(bool => i32);
300spec_from!(bool => i64);
301spec_from!(bool => i128);
302spec_from!(bool => isize);
303
304// unsigned -> unsigned
305spec_from!(u8 => u16);
306spec_from!(u8 => u32);
307spec_from!(u8 => u64);
308spec_from!(u8 => u128);
309spec_from!(u8 => usize);
310spec_from!(u16 => u32);
311spec_from!(u16 => u64);
312spec_from!(u16 => u128);
313spec_from!(u16 => usize);
314spec_from!(u32 => u64);
315spec_from!(u32 => u128);
316spec_from!(u64 => u128);
317
318// signed -> signed
319spec_from!(i8 => i16);
320spec_from!(i8 => i32);
321spec_from!(i8 => i64);
322spec_from!(i8 => i128);
323spec_from!(i8 => isize);
324spec_from!(i16 => i32);
325spec_from!(i16 => i64);
326spec_from!(i16 => i128);
327spec_from!(i16 => isize);
328spec_from!(i32 => i64);
329spec_from!(i32 => i128);
330spec_from!(i64 => i128);
331
332// unsigned -> signed
333spec_from!(u8 => i16);
334spec_from!(u8 => i32);
335spec_from!(u8 => i64);
336spec_from!(u8 => i128);
337spec_from!(u8 => isize);
338spec_from!(u16 => i32);
339spec_from!(u16 => i64);
340spec_from!(u16 => i128);
341spec_from!(u32 => i64);
342spec_from!(u32 => i128);
343spec_from!(u64 => i128);
creusot_std/std/convert.rs

creusot_std/std/
convert.rs
