vstd/std_specs/
convert.rs

1#![allow(unused_imports)]
2use super::super::prelude::*;
3
4use core::convert::{From, Into, TryFrom, TryInto};
5
6verus! {
7
8#[verifier::external_trait_specification]
9#[verifier::external_trait_extension(FromSpec via FromSpecImpl)]
10pub trait ExFrom<T>: Sized {
11    type ExternalTraitSpecificationFor: core::convert::From<T>;
12
13    spec fn obeys_from_spec() -> bool;
14
15    spec fn from_spec(v: T) -> Self;
16
17    fn from(v: T) -> (ret: Self)
18        ensures
19            Self::obeys_from_spec() ==> ret == Self::from_spec(v),
20    ;
21}
22
23impl<T> FromSpecImpl<T> for T {
24    open spec fn obeys_from_spec() -> bool {
25        true
26    }
27
28    open spec fn from_spec(v: T) -> Self {
29        v
30    }
31}
32
33#[verifier::external_trait_specification]
34#[verifier::external_trait_extension(IntoSpec via IntoSpecImpl)]
35pub trait ExInto<T>: Sized {
36    type ExternalTraitSpecificationFor: core::convert::Into<T>;
37
38    spec fn obeys_into_spec() -> bool;
39
40    spec fn into_spec(self) -> T;
41
42    fn into(self) -> (ret: T)
43        ensures
44            Self::obeys_into_spec() ==> ret == Self::into_spec(self),
45    ;
46}
47
48impl<T, U: From<T>> IntoSpecImpl<U> for T {
49    open spec fn obeys_into_spec() -> bool {
50        <U as FromSpec<Self>>::obeys_from_spec()
51    }
52
53    open spec fn into_spec(self) -> U {
54        <U as FromSpec<Self>>::from_spec(self)
55    }
56}
57
58pub assume_specification<T, U: From<T>>[ <T as Into<U>>::into ](a: T) -> (ret: U)
59    ensures
60        call_ensures(U::from, (a,), ret),
61;
62
63#[verifier::external_type_specification]
64#[verifier::external_body]
65pub struct ExTryFromIntError(core::num::TryFromIntError);
66
67#[verifier::external_trait_specification]
68#[verifier::external_trait_extension(TryFromSpec via TryFromSpecImpl)]
69pub trait ExTryFrom<T>: Sized {
70    type ExternalTraitSpecificationFor: TryFrom<T>;
71
72    type Error;
73
74    spec fn obeys_try_from_spec() -> bool;
75
76    spec fn try_from_spec(v: T) -> Result<Self, Self::Error>;
77
78    fn try_from(v: T) -> (ret: Result<Self, Self::Error>)
79        ensures
80            Self::obeys_try_from_spec() ==> ret == Self::try_from_spec(v),
81    ;
82}
83
84#[verifier::external_trait_specification]
85#[verifier::external_trait_extension(TryIntoSpec via TryIntoSpecImpl)]
86pub trait ExTryInto<T>: Sized {
87    type ExternalTraitSpecificationFor: TryInto<T>;
88
89    type Error;
90
91    spec fn obeys_try_into_spec() -> bool;
92
93    spec fn try_into_spec(self) -> Result<T, Self::Error>;
94
95    fn try_into(self) -> (ret: Result<T, Self::Error>)
96        ensures
97            Self::obeys_try_into_spec() ==> ret == Self::try_into_spec(self),
98    ;
99}
100
101impl<T, U: TryFrom<T>> TryIntoSpecImpl<U> for T {
102    open spec fn obeys_try_into_spec() -> bool {
103        <U as TryFromSpec<Self>>::obeys_try_from_spec()
104    }
105
106    open spec fn try_into_spec(self) -> Result<U, U::Error> {
107        <U as TryFromSpec<Self>>::try_from_spec(self)
108    }
109}
110
111pub assume_specification<T, U: TryFrom<T>>[ <T as TryInto<U>>::try_into ](a: T) -> (ret: Result<
112    U,
113    U::Error,
114>)
115    ensures
116        call_ensures(U::try_from, (a,), ret),
117;
118
119pub assume_specification<T, U: Into<T>>[ <T as TryFrom<U>>::try_from ](a: U) -> (ret: Result<
120    T,
121    <T as TryFrom<U>>::Error,
122>)
123    ensures
124        ret.is_ok(),
125        call_ensures(U::into, (a,), ret.unwrap()),
126;
127
128} // verus!
129macro_rules! impl_from_spec {
130    ($from: ty => [$($to: ty)*]) => {
131        verus!{
132        $(
133        pub assume_specification[ <$to as core::convert::From<$from>>::from ](a: $from) -> (ret: $to);
134
135        impl FromSpecImpl<$from> for $to {
136            open spec fn obeys_from_spec() -> bool {
137                true
138            }
139
140            open spec fn from_spec(v: $from) -> $to {
141                v as $to
142            }
143        }
144        )*
145        }
146    };
147}
148
149impl_from_spec! {u8 => [u16 u32 u64 usize u128 i16 i32 i64 i128 isize]}
150impl_from_spec! {u16 => [u32 u64 usize u128 i32 i64 i128]}
151impl_from_spec! {u32 => [u64 u128 i64 i128]}
152impl_from_spec! {u64 => [u128 i128]}
153impl_from_spec! {i8 => [i16 i32 i64 isize i128]}
154impl_from_spec! {i16 => [i32 i64 isize i128]}
155impl_from_spec! {i32 => [i64 i128]}
156impl_from_spec! {i64 => [i128]}
157
158macro_rules! impl_int_try_from_spec {
159    ($from:ty => [$($to:ty)*]) => {
160        verus!{
161        $(
162        pub assume_specification[ <$to as TryFrom<$from>>::try_from ](a: $from) -> (ret: Result<$to, <$to as TryFrom<$from>>::Error>);
163
164        impl TryFromSpecImpl<$from> for $to {
165            open spec fn obeys_try_from_spec() -> bool {
166                true
167            }
168
169            open spec fn try_from_spec(v: $from) -> Result<Self, Self::Error> {
170                if Self::MIN <= v <= Self::MAX {
171                    Ok(v as $to)
172                } else {
173                    Err(arbitrary())
174                }
175            }
176        }
177        )*
178        }
179    };
180}
181
182impl_int_try_from_spec! { u8 => [i8] }
183impl_int_try_from_spec! { u16 => [u8 i8 i16 isize] }
184impl_int_try_from_spec! { u32 => [u8 u16 i8 i16 i32 usize isize] }
185impl_int_try_from_spec! { u64 => [u8 u16 u32 i8 i16 i32 i64 usize isize] }
186impl_int_try_from_spec! { u128 => [u8 u16 u32 u64 i8 i16 i32 i64 i128 usize isize] }
187impl_int_try_from_spec! { usize => [u8 u16 u32 u64 u128 i8 i16 i32 i64 isize] }
188impl_int_try_from_spec! { i8 => [u8 u16 u32 u64 u128 usize] }
189impl_int_try_from_spec! { i16 => [u8 u16 u32 u64 u128 i8 usize] }
190impl_int_try_from_spec! { i32 => [u8 u16 u32 u64 u128 i8 i16 usize isize] }
191impl_int_try_from_spec! { i64 => [u8 u16 u32 u64 u128 i8 i16 i32 usize isize] }
192impl_int_try_from_spec! { i128 => [u8 u16 u32 u64 u128 i8 i16 i32 i64 usize isize] }
193impl_int_try_from_spec! { isize => [u8 u16 u32 u64 u128 i8 i16 i32 i64 i128 usize] }
vstd/std_specs/convert.rs

vstd/std_specs/
convert.rs
