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 ExHash: PointeeSized {
96    type ExternalTraitSpecificationFor: core::hash::Hash;
97}
98
99#[verifier::external_trait_specification]
100pub trait ExPtrPointee: PointeeSized {
101    type ExternalTraitSpecificationFor: core::ptr::Pointee;
102
103    type Metadata:
104        Copy + Send + Sync + Ord + core::hash::Hash + Unpin + core::fmt::Debug + Sized + core::marker::Freeze;
105}
106
107#[verifier::external_trait_specification]
108pub trait ExBorrow<Borrowed> where Borrowed: ?Sized {
109    type ExternalTraitSpecificationFor: core::borrow::Borrow<Borrowed>;
110}
111
112#[verifier::external_trait_specification]
113pub trait ExStructural {
114    type ExternalTraitSpecificationFor: Structural;
115}
116
117// Since this trait involves the unstable library feature `const_destruct`,
118// we only enable it when verifying core
119#[cfg(verus_verify_core)]
120#[verifier::external_trait_specification]
121trait ExDestruct: PointeeSized {
122    type ExternalTraitSpecificationFor: core::marker::Destruct;
123}
124
125#[verifier::external_trait_specification]
126pub trait ExMetaSized {
127    type ExternalTraitSpecificationFor: core::marker::MetaSized;
128}
129
130pub assume_specification<T>[ core::mem::swap::<T> ](a: &mut T, b: &mut T)
131    ensures
132        *final(a) == *old(b),
133        *final(b) == *old(a),
134    opens_invariants none
135    no_unwind
136;
137
138#[verifier::external_type_specification]
139pub struct ExOrdering(core::cmp::Ordering);
140
141#[verifier::external_type_specification]
142#[verifier::accept_recursive_types(V)]
143#[verifier::ext_equal]
144pub struct ExOption<V>(core::option::Option<V>);
145
146#[verifier::external_type_specification]
147#[verifier::accept_recursive_types(T)]
148#[verifier::reject_recursive_types_in_ground_variants(E)]
149pub struct ExResult<T, E>(core::result::Result<T, E>);
150
151// I don't really expect this to be particularly useful;
152// this is mostly here because I wanted an easy way to test
153// the combination of external_type_specification & external_body
154// in a cross-crate context.
155#[verifier::external_type_specification]
156#[verifier::external_body]
157pub struct ExDuration(core::time::Duration);
158
159#[verifier::external_type_specification]
160#[verifier::accept_recursive_types(V)]
161pub struct ExPhantomData<V: PointeeSized>(core::marker::PhantomData<V>);
162
163pub assume_specification[ core::intrinsics::likely ](b: bool) -> (c: bool)
164    ensures
165        c == b,
166;
167
168pub assume_specification[ core::intrinsics::unlikely ](b: bool) -> (c: bool)
169    ensures
170        c == b,
171;
172
173pub assume_specification<T, F: FnOnce() -> T>[ bool::then ](b: bool, f: F) -> (ret: Option<T>)
174    requires
175        b ==> f.requires(()),
176    ensures
177        if b {
178            ret.is_some() && f.ensures((), ret.unwrap())
179        } else {
180            ret.is_none()
181        },
182;
183
184pub assume_specification<T> [core::hint::must_use] (value: T) -> (ret: T)
185    ensures
186        ret == value,
187;
188
189pub assume_specification [core::panicking::panic] (s: &'static str) -> !
190    requires
191        false,
192;
193
194pub assume_specification [core::panicking::panic_fmt] (s: core::fmt::Arguments<'_>) -> !
195    requires
196        false,
197;
198
199} // verus!
200
201#[verifier::external_type_specification]
202#[verifier::external_body]
203#[verifier::accept_recursive_types(T)]
204pub struct ExAssertParamIsClone<T: Clone + PointeeSized>(core::clone::AssertParamIsClone<T>);
vstd/std_specs/core.rs

vstd/std_specs/
core.rs
