vstd/std_specs/
convert.rs

1#![allow(unused_imports)]
2use super::super::prelude::*;
3
4use core::convert::{From, Into};
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::into ](a: T) -> (ret: U)
49    ensures
50        call_ensures(U::from, (a,), ret),
51;
52
53} // verus!
54macro_rules! impl_from_spec {
55    ($from: ty => [$($to: ty)*]) => {
56        verus!{
57        $(
58        pub assume_specification[ <$to as core::convert::From<$from>>::from ](a: $from) -> (ret: $to);
59
60        impl FromSpecImpl<$from> for $to {
61            open spec fn obeys_from_spec() -> bool {
62                true
63            }
64
65            open spec fn from_spec(v: $from) -> $to {
66                v as $to
67            }
68        }
69        )*
70        }
71    };
72}
73
74impl_from_spec! {u8 => [u16 u32 u64 usize u128]}
75impl_from_spec! {u16 => [u32 u64 usize u128]}
76impl_from_spec! {u32 => [u64 u128]}
77impl_from_spec! {u64 => [u128]}
vstd/std_specs/convert.rs

vstd/std_specs/
convert.rs
