vstd/std_specs/
default.rs

1use super::super::prelude::*;
2use core::marker::PointeeSized;
3
4verus! {
5
6#[verifier::external_trait_specification]
7pub trait ExDefault: Sized {
8    type ExternalTraitSpecificationFor: core::default::Default;
9
10    fn default() -> (r: Self);
11}
12
13} // verus!
14macro_rules! assume_default_value {
15    ($t:ty, $default_value:expr) => {
16        verus! {
17            pub assume_specification [ <$t as core::default::Default>::default ]() -> (r: $t)
18                ensures
19                    r == $default_value,
20            ;
21        }
22    };
23}
24
25assume_default_value!(bool, false);
26assume_default_value!(char, '\0');
27assume_default_value!(f32, 0.0f32);
28assume_default_value!(f64, 0.0f64);
29assume_default_value!(i8, 0i8);
30assume_default_value!(i16, 0i16);
31assume_default_value!(i32, 0i32);
32assume_default_value!(i64, 0i64);
33assume_default_value!(i128, 0i128);
34assume_default_value!(isize, 0isize);
35assume_default_value!(u8, 0u8);
36assume_default_value!(u16, 0u16);
37assume_default_value!(u32, 0u32);
38assume_default_value!(u64, 0u64);
39assume_default_value!(u128, 0u128);
40assume_default_value!((), ());
41assume_default_value!(usize, 0usize);
42
43// manually implementation for Option<T>, &str, PhantomData<T>, (U, T), (V, U, T)
44verus! {
45
46pub assume_specification<T>[ <Option<T> as core::default::Default>::default ]() -> (r: Option<T>)
47    ensures
48        r == Option::<T>::None,
49;
50
51pub assume_specification<'a>[ <&'a str as core::default::Default>::default ]() -> (r: &'a str)
52    ensures
53        r == "",
54;
55
56pub assume_specification<T: PointeeSized>[ <core::marker::PhantomData<
57    T,
58> as core::default::Default>::default ]() -> (r: core::marker::PhantomData<T>)
59    ensures
60        r == core::marker::PhantomData::<T>,
61;
62
63pub assume_specification<U: core::default::Default, T: core::default::Default>[ <(
64    U,
65    T,
66) as core::default::Default>::default ]() -> (r: (U, T))
67    ensures
68        call_ensures(U::default, (), r.0),
69        call_ensures(T::default, (), r.1),
70;
71
72pub assume_specification<
73    V: core::default::Default,
74    U: core::default::Default,
75    T: core::default::Default,
76>[ <(V, U, T) as core::default::Default>::default ]() -> (r: (V, U, T))
77    ensures
78        call_ensures(V::default, (), r.0),
79        call_ensures(U::default, (), r.1),
80        call_ensures(T::default, (), r.2),
81;
82
83} // verus!
vstd/std_specs/default.rs

vstd/std_specs/
default.rs
