creusot_std/std/
convert.rs

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

creusot_std/std/
convert.rs
