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]
40pub trait ExDerefMut: core::ops::Deref + PointeeSized {
41    type ExternalTraitSpecificationFor: core::ops::DerefMut;
42
43    fn deref_mut(&mut self) -> &mut Self::Target;
44}
45
46#[verifier::external_trait_specification]
47#[verifier::external_trait_extension(IndexSpec via IndexSpecImpl)]
48pub trait ExIndex<Idx> where Idx: ?Sized {
49    type ExternalTraitSpecificationFor: core::ops::Index<Idx>;
50
51    type Output: ?Sized;
52
53    spec fn index_req(&self, index: &Idx) -> bool;
54
55    fn index(&self, index: Idx) -> (output: &Self::Output) where Idx: Sized
56        requires
57            self.index_req(&index);
58}
59
60#[verifier::external_trait_specification]
61pub trait ExIndexMut<Idx>: core::ops::Index<Idx> where Idx: ?Sized {
62    type ExternalTraitSpecificationFor: core::ops::IndexMut<Idx>;
63}
64
65#[verifier::external_trait_specification]
66pub trait ExInteger: Copy {
67    type ExternalTraitSpecificationFor: Integer;
68}
69
70#[verifier::external_trait_specification]
71pub trait ExSpecOrd<Rhs> {
72    type ExternalTraitSpecificationFor: SpecOrd<Rhs>;
73}
74
75#[cfg(not(verus_verify_core))]
76#[verifier::external_trait_specification]
77pub trait ExAllocator {
78    type ExternalTraitSpecificationFor: core::alloc::Allocator;
79}
80
81#[verifier::external_trait_specification]
82pub trait ExFreeze: PointeeSized {
83    type ExternalTraitSpecificationFor: core::marker::Freeze;
84}
85
86#[verifier::external_trait_specification]
87pub trait ExDebug: PointeeSized {
88    type ExternalTraitSpecificationFor: core::fmt::Debug;
89}
90
91#[verifier::external_trait_specification]
92pub trait ExDisplay: PointeeSized {
93    type ExternalTraitSpecificationFor: core::fmt::Display;
94}
95
96#[verifier::external_trait_specification]
97pub trait ExHash: PointeeSized {
98    type ExternalTraitSpecificationFor: core::hash::Hash;
99}
100
101#[verifier::external_trait_specification]
102pub trait ExPtrPointee: PointeeSized {
103    type ExternalTraitSpecificationFor: core::ptr::Pointee;
104
105    type Metadata:
106        Copy + Send + Sync + Ord + core::hash::Hash + Unpin + core::fmt::Debug + Sized + core::marker::Freeze;
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
119// Since this trait involves the unstable library feature `const_destruct`,
120// we only enable it when verifying core
121#[cfg(verus_verify_core)]
122#[verifier::external_trait_specification]
123trait ExDestruct: PointeeSized {
124    type ExternalTraitSpecificationFor: core::marker::Destruct;
125}
126
127#[verifier::external_trait_specification]
128pub trait ExMetaSized {
129    type ExternalTraitSpecificationFor: core::marker::MetaSized;
130}
131
132pub assume_specification<T>[ core::mem::swap::<T> ](a: &mut T, b: &mut T)
133    ensures
134        *final(a) == *old(b),
135        *final(b) == *old(a),
136    opens_invariants none
137    no_unwind
138;
139
140#[verifier::external_type_specification]
141pub struct ExOrdering(core::cmp::Ordering);
142
143#[verifier::external_type_specification]
144#[verifier::accept_recursive_types(V)]
145#[verifier::ext_equal]
146pub struct ExOption<V>(core::option::Option<V>);
147
148#[verifier::external_type_specification]
149#[verifier::accept_recursive_types(T)]
150#[verifier::reject_recursive_types_in_ground_variants(E)]
151pub struct ExResult<T, E>(core::result::Result<T, E>);
152
153// I don't really expect this to be particularly useful;
154// this is mostly here because I wanted an easy way to test
155// the combination of external_type_specification & external_body
156// in a cross-crate context.
157#[verifier::external_type_specification]
158#[verifier::external_body]
159pub struct ExDuration(core::time::Duration);
160
161#[verifier::external_type_specification]
162#[verifier::accept_recursive_types(V)]
163pub struct ExPhantomData<V: PointeeSized>(core::marker::PhantomData<V>);
164
165pub assume_specification[ core::intrinsics::likely ](b: bool) -> (c: bool)
166    ensures
167        c == b,
168;
169
170pub assume_specification[ core::intrinsics::unlikely ](b: bool) -> (c: bool)
171    ensures
172        c == b,
173;
174
175pub assume_specification<T, F: FnOnce() -> T>[ bool::then ](b: bool, f: F) -> (ret: Option<T>)
176    ensures
177        if b {
178            ret.is_some() && f.ensures((), ret.unwrap())
179        } else {
180            ret.is_none()
181        },
182;
183
184// A private seal trait to prevent a trait from being implemented outside of vstd.
185pub(crate) trait TrustedSpecSealed {}
186
187#[allow(private_bounds)]
188pub trait IndexSetTrustedSpec<Idx>: core::ops::IndexMut<Idx> + TrustedSpecSealed {
189    spec fn spec_index_set_requires(&self, index: Idx) -> bool;
190
191    spec fn spec_index_set_ensures(
192        &self,
193        new_container: &Self,
194        index: Idx,
195        val: Self::Output,
196    ) -> bool where Self::Output: Sized;
197}
198
199// TODO(uutaal): Do not need index_set once mutable reference support lands.
200// Use index_set to replace IndexMut in assign-operator.
201// Users must provide IndexSetTrustedSpec to use it.
202// It could be replaced after mutable reference is fully supported
203// Avoid call it explicitly.
204#[verifier(external_body)]
205pub fn index_set<T, Idx, E>(container: &mut T, index: Idx, val: E) where
206    T: ?Sized + core::ops::IndexMut<Idx> + core::ops::Index<Idx, Output = E> + IndexSetTrustedSpec<
207        Idx,
208    >,
209
210    requires
211        old(container).spec_index_set_requires(index),
212    ensures
213        old(container).spec_index_set_ensures(final(container), index, val),
214    no_unwind
215{
216    container[index] = val;
217}
218
219} // verus!
220
221#[verifier::external_type_specification]
222#[verifier::external_body]
223#[verifier::accept_recursive_types(T)]
224pub struct ExAssertParamIsClone<T: Clone + PointeeSized>(core::clone::AssertParamIsClone<T>);
vstd/std_specs/core.rs

vstd/std_specs/
core.rs
