vstd/std_specs/
core.rs

1use super::super::prelude::*;
2
3use verus as verus_;
4
5verus_! {
6
7#[verifier::external_trait_specification]
8pub trait ExDeref {
9    type ExternalTraitSpecificationFor: core::ops::Deref;
10
11    type Target: ?Sized;
12
13    fn deref(&self) -> &Self::Target;
14}
15
16#[verifier::external_trait_specification]
17pub trait ExIndex<Idx> where Idx: ?Sized {
18    type ExternalTraitSpecificationFor: core::ops::Index<Idx>;
19
20    type Output: ?Sized;
21}
22
23#[verifier::external_trait_specification]
24pub trait ExIndexMut<Idx>: core::ops::Index<Idx> where Idx: ?Sized {
25    type ExternalTraitSpecificationFor: core::ops::IndexMut<Idx>;
26}
27
28#[verifier::external_trait_specification]
29pub trait ExInteger: Copy {
30    type ExternalTraitSpecificationFor: Integer;
31}
32
33#[verifier::external_trait_specification]
34pub trait ExSpecOrd<Rhs> {
35    type ExternalTraitSpecificationFor: SpecOrd<Rhs>;
36}
37
38#[verifier::external_trait_specification]
39pub trait ExAllocator {
40    type ExternalTraitSpecificationFor: core::alloc::Allocator;
41}
42
43#[verifier::external_trait_specification]
44pub trait ExFreeze {
45    type ExternalTraitSpecificationFor: core::marker::Freeze;
46}
47
48#[verifier::external_trait_specification]
49pub trait ExDebug {
50    type ExternalTraitSpecificationFor: core::fmt::Debug;
51}
52
53#[verifier::external_trait_specification]
54pub trait ExDisplay {
55    type ExternalTraitSpecificationFor: core::fmt::Display;
56}
57
58#[verifier::external_trait_specification]
59pub trait ExFrom<T>: Sized {
60    type ExternalTraitSpecificationFor: core::convert::From<T>;
61
62    fn from(v: T) -> (ret: Self);
63}
64
65#[verifier::external_trait_specification]
66pub trait ExInto<T>: Sized {
67    type ExternalTraitSpecificationFor: core::convert::Into<T>;
68
69    fn into(self) -> (ret: T);
70}
71
72pub assume_specification<T, U: From<T>>[ T::into ](a: T) -> (ret: U)
73    ensures
74        call_ensures(U::from, (a,), ret),
75;
76
77#[verifier::external_trait_specification]
78pub trait ExHash {
79    type ExternalTraitSpecificationFor: core::hash::Hash;
80}
81
82#[verifier::external_trait_specification]
83pub trait ExPtrPointee {
84    type ExternalTraitSpecificationFor: core::ptr::Pointee;
85
86    type Metadata:
87        Copy + Send + Sync + Ord + core::hash::Hash + Unpin + core::fmt::Debug + Sized + core::marker::Freeze;
88}
89
90#[verifier::external_trait_specification]
91pub trait ExIterator {
92    type ExternalTraitSpecificationFor: core::iter::Iterator;
93
94    type Item;
95
96    fn next(&mut self) -> Option<Self::Item>;
97}
98
99#[verifier::external_trait_specification]
100pub trait ExIntoIterator {
101    type ExternalTraitSpecificationFor: core::iter::IntoIterator;
102}
103
104#[verifier::external_trait_specification]
105pub trait ExIterStep: Clone + PartialOrd + Sized {
106    type ExternalTraitSpecificationFor: core::iter::Step;
107}
108
109#[verifier::external_trait_specification]
110pub trait ExBorrow<Borrowed> where Borrowed: ?Sized {
111    type ExternalTraitSpecificationFor: core::borrow::Borrow<Borrowed>;
112}
113
114#[verifier::external_trait_specification]
115pub trait ExStructural {
116    type ExternalTraitSpecificationFor: Structural;
117}
118
119pub assume_specification<T>[ core::mem::swap::<T> ](a: &mut T, b: &mut T)
120    ensures
121        *a == *old(b),
122        *b == *old(a),
123    opens_invariants none
124    no_unwind
125;
126
127#[verifier::external_type_specification]
128pub struct ExOrdering(core::cmp::Ordering);
129
130#[verifier::external_type_specification]
131#[verifier::accept_recursive_types(V)]
132#[verifier::ext_equal]
133pub struct ExOption<V>(core::option::Option<V>);
134
135#[verifier::external_type_specification]
136#[verifier::accept_recursive_types(T)]
137#[verifier::reject_recursive_types_in_ground_variants(E)]
138pub struct ExResult<T, E>(core::result::Result<T, E>);
139
140pub open spec fn iter_into_iter_spec<I: Iterator>(i: I) -> I {
141    i
142}
143
144#[verifier::when_used_as_spec(iter_into_iter_spec)]
145pub assume_specification<I: Iterator>[ I::into_iter ](i: I) -> (r: I)
146    ensures
147        r == i,
148;
149
150// I don't really expect this to be particularly useful;
151// this is mostly here because I wanted an easy way to test
152// the combination of external_type_specification & external_body
153// in a cross-crate context.
154#[verifier::external_type_specification]
155#[verifier::external_body]
156pub struct ExDuration(core::time::Duration);
157
158#[verifier::external_type_specification]
159#[verifier::accept_recursive_types(V)]
160pub struct ExPhantomData<V: ?Sized>(core::marker::PhantomData<V>);
161
162pub assume_specification[ core::intrinsics::likely ](b: bool) -> (c: bool)
163    ensures
164        c == b,
165;
166
167pub assume_specification[ core::intrinsics::unlikely ](b: bool) -> (c: bool)
168    ensures
169        c == b,
170;
171
172pub assume_specification<T, F: FnOnce() -> T>[ bool::then ](b: bool, f: F) -> (ret: Option<T>)
173    ensures
174        if b {
175            ret.is_some() && f.ensures((), ret.unwrap())
176        } else {
177            ret.is_none()
178        },
179;
180
181#[verifier::external_type_specification]
182#[verifier::external_body]
183#[verifier::reject_recursive_types_in_ground_variants(V)]
184pub struct ExManuallyDrop<V: ?Sized>(core::mem::ManuallyDrop<V>);
185
186// A private seal trait to prevent a trait from being implemented outside of vstd.
187pub(crate) trait TrustedSpecSealed {}
188
189#[allow(private_bounds)]
190pub trait IndexSetTrustedSpec<Idx>: core::ops::IndexMut<Idx> + TrustedSpecSealed {
191    spec fn spec_index_set_requires(&self, index: Idx) -> bool;
192
193    spec fn spec_index_set_ensures(
194        &self,
195        new_container: &Self,
196        index: Idx,
197        val: Self::Output,
198    ) -> bool where Self::Output: Sized;
199}
200
201// TODO(uutaal): Do not need index_set once mutable reference support lands.
202// Use index_set to replace IndexMut in assign-operator.
203// Users must provide IndexSetTrustedSpec to use it.
204// It could be replaced after mutable reference is fully supported
205// Avoid call it explicitly.
206#[verifier(external_body)]
207pub fn index_set<T, Idx, E>(container: &mut T, index: Idx, val: E) where
208    T: ?Sized + core::ops::IndexMut<Idx> + core::ops::Index<Idx, Output = E> + IndexSetTrustedSpec<
209        Idx,
210    >,
211
212    requires
213        old(container).spec_index_set_requires(index),
214    ensures
215        old(container).spec_index_set_ensures(container, index, val),
216    no_unwind
217{
218    container[index] = val;
219}
220
221} // verus!
222macro_rules! impl_from_spec {
223    ($from: ty => [$($to: ty)*]) => {
224        verus!{
225        $(
226        pub assume_specification[ <$to as core::convert::From<$from>>::from ](a: $from) -> (ret: $to)
227            ensures
228                ret == a as $to,
229        ;
230        )*
231        }
232    };
233}
234
235impl_from_spec! {u8 => [u16 u32 u64 usize u128]}
236impl_from_spec! {u16 => [u32 u64 usize u128]}
237impl_from_spec! {u32 => [u64 u128]}
238impl_from_spec! {u64 => [u128]}
239
240#[verifier::external_type_specification]
241#[verifier::external_body]
242#[verifier::accept_recursive_types(T)]
243pub struct ExAssertParamIsClone<T: Clone + ?Sized>(core::clone::AssertParamIsClone<T>);
vstd/std_specs/core.rs

vstd/std_specs/
core.rs
