vstd/std_specs/
core.rs

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

vstd/std_specs/
core.rs
