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

vstd/std_specs/
core.rs
