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
114#[cfg(feature = "std")]
115extern_spec! {
116    impl<T> From<T> for Box<T> {
117        #[check(ghost)]
118        #[ensures(*result == x)]
119        fn from(x: T) -> Self;
120    }
121
122    impl<T: Clone> From<&[T]> for Box<[T]>
123    {
124        // FIXME: inherit ghost/terminates from clone
125        #[ensures(result@.len() == s@.len())]
126        #[ensures(forall<i> 0 <= i && i < s@.len() ==> <T as Clone>::clone.postcondition((&s@[i],), result@[i]))]
127        fn from(s: &[T]) -> Self;
128        // To verify: uses CloneToUninit
129    }
130
131    impl<T: Clone> From<&mut [T]> for Box<[T]>
132    {
133        // FIXME: inherit ghost/terminates from clone
134        #[ensures(result@.len() == s@.len())]
135        #[ensures(forall<i> 0 <= i && i < s@.len() ==> <T as Clone>::clone.postcondition((&s@[i],), result@[i]))]
136        #[ensures(^s == *s)]
137        fn from(s: &mut [T]) -> Self {
138            Box::<[T]>::from(&*s)
139        }
140    }
141
142    impl<T, const N: usize> From<[T; N]> for Box<[T]> {
143        #[check(ghost)]
144        #[ensures(result@ == s@)]
145        fn from(s: [T; N]) -> Self {
146            Box::new(s)
147        }
148    }
149
150    impl<T: Clone> From<&[T]> for Vec<T>
151    {
152        // FIXME: inherit ghost/terminates from clone
153        #[ensures(result@.len() == s@.len())]
154        #[ensures(forall<i> 0 <= i && i < s@.len() ==> <T as Clone>::clone.postcondition((&s@[i],), result@[i]))]
155        fn from(s: &[T]) -> Self {
156            s.to_vec()
157        }
158    }
159
160    impl<T: Clone> From<&mut [T]> for Vec<T>
161    {
162        // FIXME: inherit ghost/terminates from clone
163        #[ensures(result@.len() == s@.len())]
164        #[ensures(forall<i> 0 <= i && i < s@.len() ==> <T as Clone>::clone.postcondition((&s@[i],), result@[i]))]
165        #[ensures(^s == *s)]
166        fn from(s: &mut [T]) -> Self {
167            s.to_vec()
168        }
169    }
170
171    impl<T, A: Allocator> From<Box<[T], A>> for Vec<T, A> {
172        #[check(ghost)]
173        #[ensures(result@ == s@)]
174        fn from(s: Box<[T], A>) -> Self {
175            s.into_vec()
176        }
177    }
178
179    impl<T: Clone, const N: usize> From<&[T; N]> for Vec<T> {
180        // FIXME: inherit ghost/terminates from clone
181        #[ensures(result@.len() == N@)]
182        #[ensures(forall<i> 0 <= i && i < s@.len() ==> <T as Clone>::clone.postcondition((&s@[i],), result@[i]))]
183        fn from(s: &[T; N]) -> Self {
184            Vec::<T>::from(s.as_slice())
185        }
186    }
187
188    impl<T: Clone, const N: usize> From<&mut [T; N]> for Vec<T> {
189        // FIXME: inherit ghost/terminates from clone
190        #[ensures(result@.len() == N@)]
191        #[ensures(forall<i> 0 <= i && i < s@.len() ==> <T as Clone>::clone.postcondition((&s@[i],), result@[i]))]
192        #[ensures(^s == *s)]
193        fn from(s: &mut [T; N]) -> Self {
194            Vec::<T>::from(s.as_mut_slice())
195        }
196    }
197
198    impl<T, const N: usize> From<[T; N]> for Vec<T> {
199        #[check(ghost)]
200        #[ensures(result@ == s@)]
201        fn from(s: [T; N]) -> Self {
202            <[T]>::into_vec(Box::new(s))
203        }
204    }
205
206    impl<T, A: Allocator> From<Vec<T, A>> for Box<[T], A> {
207        #[check(ghost)]
208        #[ensures(result@ == v@)]
209        fn from(v: Vec<T, A>) -> Self {
210            v.into_boxed_slice()
211        }
212    }
213
214    impl From<&String> for String {
215        #[check(ghost)]
216        #[ensures(result@ == s@)]
217        fn from(s: &String) -> Self;
218    }
219
220    impl From<Box<str>> for String {
221        #[check(ghost)]
222        #[ensures(result@ == s@)]
223        fn from(s: Box<str>) -> Self;
224    }
225
226    impl From<String> for Box<str> {
227        #[check(ghost)]
228        #[ensures(result@ == s@)]
229        fn from(s: String) -> Self;
230    }
231
232    impl From<&str> for String {
233        #[check(ghost)]
234        #[ensures(result@ == s@)]
235        fn from(s: &str) -> Self;
236    }
237
238    impl From<&mut str> for String {
239        #[check(ghost)]
240        #[ensures(result@ == s@ && ^s == *s)]
241        fn from(s: &mut String) -> Self;
242    }
243
244    impl From<&mut str> for Box<str> {
245        #[check(ghost)]
246        #[ensures(result@ == s@ && ^s == *s)]
247        fn from(s: &mut str) -> Self;
248    }
249
250    impl From<char> for String {
251        #[check(ghost)]
252        #[ensures(result@ == seq![c])]
253        fn from(c: char) -> Self;
254    }
255
256    impl From<String> for Vec<u8> {
257        #[check(ghost)]
258        #[ensures(result@ == s@.to_bytes())]
259        fn from(s: String) -> Self;
260    }
261
262    impl From<&str> for Vec<u8> {
263        #[check(ghost)]
264        #[ensures(result@ == s@.to_bytes())]
265        fn from(s: &str) -> Self;
266    }
267}
268
269macro_rules! spec_from {
270    ($src:ty => $tgt:ty) => {
271        extern_spec! {
272            impl From<$src> for $tgt {
273                #[check(ghost)]
274                #[ensures(result == (small as Self))]
275                fn from(small: $src) -> Self {
276                    small as Self
277                }
278            }
279        }
280    };
281}
282
283spec_from!(bool => u8);
284spec_from!(bool => u16);
285spec_from!(bool => u32);
286spec_from!(bool => u64);
287spec_from!(bool => u128);
288spec_from!(bool => usize);
289spec_from!(bool => i8);
290spec_from!(bool => i16);
291spec_from!(bool => i32);
292spec_from!(bool => i64);
293spec_from!(bool => i128);
294spec_from!(bool => isize);
295
296// unsigned -> unsigned
297spec_from!(u8 => u16);
298spec_from!(u8 => u32);
299spec_from!(u8 => u64);
300spec_from!(u8 => u128);
301spec_from!(u8 => usize);
302spec_from!(u16 => u32);
303spec_from!(u16 => u64);
304spec_from!(u16 => u128);
305spec_from!(u16 => usize);
306spec_from!(u32 => u64);
307spec_from!(u32 => u128);
308spec_from!(u64 => u128);
309
310// signed -> signed
311spec_from!(i8 => i16);
312spec_from!(i8 => i32);
313spec_from!(i8 => i64);
314spec_from!(i8 => i128);
315spec_from!(i8 => isize);
316spec_from!(i16 => i32);
317spec_from!(i16 => i64);
318spec_from!(i16 => i128);
319spec_from!(i16 => isize);
320spec_from!(i32 => i64);
321spec_from!(i32 => i128);
322spec_from!(i64 => i128);
323
324// unsigned -> signed
325spec_from!(u8 => i16);
326spec_from!(u8 => i32);
327spec_from!(u8 => i64);
328spec_from!(u8 => i128);
329spec_from!(u8 => isize);
330spec_from!(u16 => i32);
331spec_from!(u16 => i64);
332spec_from!(u16 => i128);
333spec_from!(u32 => i64);
334spec_from!(u32 => i128);
335spec_from!(u64 => i128);
creusot_std/std/convert.rs

creusot_std/std/
convert.rs
