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

vstd/std_specs/
core.rs
