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    // NOTE: this used as a precondition for both `Index` and `IndexMut`,
54    // since both share the same `s[i]` syntax.
55    spec fn index_req(&self, index: &Idx) -> bool;
56
57    fn index(&self, index: Idx) -> (output: &Self::Output) where Idx: Sized
58        requires
59            self.index_req(&index),
60    ;
61}
62
63#[verifier::external_trait_specification]
64pub trait ExIndexMut<Idx>: core::ops::Index<Idx> where Idx: ?Sized {
65    type ExternalTraitSpecificationFor: core::ops::IndexMut<Idx>;
66
67    fn index_mut(&mut self, index: Idx) -> (output: &mut Self::Output) where Idx: Sized
68        requires
69            self.index_req(&index),
70    ;
71}
72
73#[verifier::external_trait_specification]
74pub trait ExInteger: Copy {
75    type ExternalTraitSpecificationFor: Integer;
76}
77
78#[verifier::external_trait_specification]
79pub trait ExSpecOrd<Rhs> {
80    type ExternalTraitSpecificationFor: SpecOrd<Rhs>;
81}
82
83#[cfg(not(verus_verify_core))]
84#[verifier::external_trait_specification]
85pub trait ExAllocator {
86    type ExternalTraitSpecificationFor: core::alloc::Allocator;
87}
88
89#[verifier::external_trait_specification]
90pub trait ExFreeze: PointeeSized {
91    type ExternalTraitSpecificationFor: core::marker::Freeze;
92}
93
94#[verifier::external_trait_specification]
95pub trait ExDebug: PointeeSized {
96    type ExternalTraitSpecificationFor: core::fmt::Debug;
97}
98
99#[verifier::external_trait_specification]
100pub trait ExDisplay: PointeeSized {
101    type ExternalTraitSpecificationFor: core::fmt::Display;
102}
103
104#[verifier::external_trait_specification]
105pub trait ExHash: PointeeSized {
106    type ExternalTraitSpecificationFor: core::hash::Hash;
107}
108
109#[verifier::external_trait_specification]
110pub trait ExPtrPointee: PointeeSized {
111    type ExternalTraitSpecificationFor: core::ptr::Pointee;
112
113    type Metadata:
114        Copy + Send + Sync + Ord + core::hash::Hash + Unpin + core::fmt::Debug + Sized + core::marker::Freeze;
115}
116
117#[verifier::external_trait_specification]
118pub trait ExBorrow<Borrowed> where Borrowed: ?Sized {
119    type ExternalTraitSpecificationFor: core::borrow::Borrow<Borrowed>;
120}
121
122#[verifier::external_trait_specification]
123pub trait ExStructural {
124    type ExternalTraitSpecificationFor: Structural;
125}
126
127// Since this trait involves the unstable library feature `const_destruct`,
128// we only enable it when verifying core
129#[cfg(verus_verify_core)]
130#[verifier::external_trait_specification]
131trait ExDestruct: PointeeSized {
132    type ExternalTraitSpecificationFor: core::marker::Destruct;
133}
134
135#[verifier::external_trait_specification]
136pub trait ExMetaSized {
137    type ExternalTraitSpecificationFor: core::marker::MetaSized;
138}
139
140pub assume_specification<T>[ core::mem::swap::<T> ](a: &mut T, b: &mut T)
141    ensures
142        *final(a) == *old(b),
143        *final(b) == *old(a),
144    opens_invariants none
145    no_unwind
146;
147
148#[verifier::external_type_specification]
149pub struct ExOrdering(core::cmp::Ordering);
150
151#[verifier::external_type_specification]
152#[verifier::accept_recursive_types(V)]
153#[verifier::ext_equal]
154pub struct ExOption<V>(core::option::Option<V>);
155
156#[verifier::external_type_specification]
157#[verifier::accept_recursive_types(T)]
158#[verifier::reject_recursive_types_in_ground_variants(E)]
159pub struct ExResult<T, E>(core::result::Result<T, E>);
160
161// I don't really expect this to be particularly useful;
162// this is mostly here because I wanted an easy way to test
163// the combination of external_type_specification & external_body
164// in a cross-crate context.
165#[verifier::external_type_specification]
166#[verifier::external_body]
167pub struct ExDuration(core::time::Duration);
168
169#[verifier::external_type_specification]
170#[verifier::accept_recursive_types(V)]
171pub struct ExPhantomData<V: PointeeSized>(core::marker::PhantomData<V>);
172
173pub assume_specification[ core::intrinsics::likely ](b: bool) -> (c: bool)
174    ensures
175        c == b,
176;
177
178pub assume_specification[ core::intrinsics::unlikely ](b: bool) -> (c: bool)
179    ensures
180        c == b,
181;
182
183pub assume_specification<T, F: FnOnce() -> T>[ bool::then ](b: bool, f: F) -> (ret: Option<T>)
184    requires
185        b ==> f.requires(()),
186    ensures
187        if b {
188            ret.is_some() && f.ensures((), ret.unwrap())
189        } else {
190            ret.is_none()
191        },
192;
193
194} // verus!
195
196#[verifier::external_type_specification]
197#[verifier::external_body]
198#[verifier::accept_recursive_types(T)]
199pub struct ExAssertParamIsClone<T: Clone + PointeeSized>(core::clone::AssertParamIsClone<T>);
vstd/std_specs/core.rs

vstd/std_specs/
core.rs
