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

vstd/std_specs/
convert.rs
