vstd/std_specs/
core.rs

1use super::super::prelude::*;
2use core::marker::PointeeSized;
3
4use verus as verus_skip_verusfmt;
5verus_skip_verusfmt! {
6
7#[verifier::external_trait_specification]
8pub trait ExTuple {
9    type ExternalTraitSpecificationFor: core::marker::Tuple;
10}
11
12#[verifier::external_trait_specification]
13pub trait ExFnOnce<Args: core::marker::Tuple> {
14    type ExternalTraitSpecificationFor: core::ops::FnOnce<Args>;
15
16    type Output;
17}
18
19#[verifier::external_trait_specification]
20pub trait ExFnMut<Args: core::marker::Tuple>: FnOnce<Args> {
21    type ExternalTraitSpecificationFor: core::ops::FnMut<Args>;
22}
23
24#[verifier::external_trait_specification]
25pub trait ExFn<Args: core::marker::Tuple>: FnMut<Args> {
26    type ExternalTraitSpecificationFor: core::ops::Fn<Args>;
27}
28
29#[verifier::external_trait_specification]
30pub trait ExDeref: PointeeSized {
31    type ExternalTraitSpecificationFor: core::ops::Deref;
32
33    type Target: ?Sized;
34
35    fn deref(&self) -> &Self::Target;
36}
37
38#[verifier::external_trait_specification]
39pub trait ExDerefMut: core::ops::Deref + PointeeSized {
40    type ExternalTraitSpecificationFor: core::ops::DerefMut;
41
42    fn deref_mut(&mut self) -> &mut Self::Target;
43}
44
45#[verifier::external_trait_specification]
46#[verifier::external_trait_extension(IndexSpec via IndexSpecImpl)]
47pub trait ExIndex<Idx> where Idx: ?Sized {
48    type ExternalTraitSpecificationFor: core::ops::Index<Idx>;
49
50    type Output: ?Sized;
51
52    // NOTE: this used as a precondition for both `Index` and `IndexMut`,
53    // since both share the same `s[i]` syntax.
54    spec fn index_req(&self, index: &Idx) -> bool;
55
56    fn index(&self, index: Idx) -> (output: &Self::Output) where Idx: Sized
57        requires
58            self.index_req(&index),
59    ;
60}
61
62#[verifier::external_trait_specification]
63pub trait ExIndexMut<Idx>: core::ops::Index<Idx> where Idx: ?Sized {
64    type ExternalTraitSpecificationFor: core::ops::IndexMut<Idx>;
65
66    fn index_mut(&mut self, index: Idx) -> (output: &mut Self::Output) where Idx: Sized
67        requires
68            self.index_req(&index),
69    ;
70}
71
72#[verifier::external_trait_specification]
73pub trait ExInteger: Copy {
74    type ExternalTraitSpecificationFor: Integer;
75}
76
77#[verifier::external_trait_specification]
78pub trait ExSpecOrd<Rhs> {
79    type ExternalTraitSpecificationFor: SpecOrd<Rhs>;
80}
81
82#[cfg(not(verus_verify_core))]
83#[verifier::external_trait_specification]
84pub trait ExAllocator {
85    type ExternalTraitSpecificationFor: core::alloc::Allocator;
86}
87
88#[verifier::external_trait_specification]
89pub trait ExFreeze: PointeeSized {
90    type ExternalTraitSpecificationFor: core::marker::Freeze;
91}
92
93#[verifier::external_trait_specification]
94pub trait ExHash: PointeeSized {
95    type ExternalTraitSpecificationFor: core::hash::Hash;
96}
97
98#[verifier::external_trait_specification]
99pub trait ExPtrPointee: PointeeSized {
100    type ExternalTraitSpecificationFor: core::ptr::Pointee;
101
102    type Metadata:
103        Copy + Send + Sync + Ord + core::hash::Hash + Unpin + core::fmt::Debug + Sized + core::marker::Freeze;
104}
105
106#[verifier::external_trait_specification]
107pub trait ExBorrow<Borrowed> where Borrowed: ?Sized {
108    type ExternalTraitSpecificationFor: core::borrow::Borrow<Borrowed>;
109}
110
111#[verifier::external_trait_specification]
112pub trait ExStructural {
113    type ExternalTraitSpecificationFor: Structural;
114}
115
116// Since this trait involves the unstable library feature `const_destruct`,
117// we only enable it when verifying core
118#[cfg(verus_verify_core)]
119#[verifier::external_trait_specification]
120trait ExDestruct: PointeeSized {
121    type ExternalTraitSpecificationFor: core::marker::Destruct;
122}
123
124#[verifier::external_trait_specification]
125pub trait ExMetaSized {
126    type ExternalTraitSpecificationFor: core::marker::MetaSized;
127}
128
129pub assume_specification<T>[ core::mem::swap::<T> ](a: &mut T, b: &mut T)
130    ensures
131        *final(a) == *old(b),
132        *final(b) == *old(a),
133    opens_invariants none
134    no_unwind
135;
136
137#[verifier::external_type_specification]
138pub struct ExOrdering(core::cmp::Ordering);
139
140#[verifier::external_type_specification]
141#[verifier::accept_recursive_types(V)]
142#[verifier::ext_equal]
143pub struct ExOption<V>(core::option::Option<V>);
144
145#[verifier::external_type_specification]
146#[verifier::accept_recursive_types(T)]
147#[verifier::reject_recursive_types_in_ground_variants(E)]
148pub struct ExResult<T, E>(core::result::Result<T, E>);
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: PointeeSized>(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    requires
174        b ==> f.requires(()),
175    ensures
176        if b {
177            ret.is_some() && f.ensures((), ret.unwrap())
178        } else {
179            ret.is_none()
180        },
181;
182
183pub assume_specification<T> [core::hint::must_use] (value: T) -> (ret: T)
184    ensures
185        ret == value,
186;
187
188pub assume_specification [core::panicking::panic] (s: &'static str) -> !
189    requires
190        false,
191;
192
193pub assume_specification [core::panicking::panic_fmt] (s: core::fmt::Arguments<'_>) -> !
194    requires
195        false,
196;
197
198} // verus!
199
200#[verifier::external_type_specification]
201#[verifier::external_body]
202#[verifier::accept_recursive_types(T)]
203pub struct ExAssertParamIsClone<T: Clone + PointeeSized>(core::clone::AssertParamIsClone<T>);
vstd/std_specs/core.rs

vstd/std_specs/
core.rs
