vstd_extra/external/
smallvec.rs

1//! Verus specifications for the third-party `smallvec` crate, trusted as TCB from
2//! inspection of the `smallvec-1.15.0` source (`src/lib.rs`) and centralized here
3//! rather than beside an OSTD caller. `cpu/set.rs` is currently the only consumer
4//! (`SmallVec<[u64; 2]>`).
5//!
6//! The model is a `Seq<A::Item>`: the views below equate every executed `SmallVec`
7//! operation to a `Seq` operation, and `Deref`/`DerefMut` bridge to the std
8//! `[A::Item]` slice so that indexing, `len`, and `iter` reuse `vstd`'s slice
9//! specifications rather than being re-axiomatized.
10//!
11//! Every operation below is guarded by `obeys_smallvec_array::<A>`
12//! (see its documentation).
13//!
14//! Allocation-growth panics (capacity overflow past `isize::MAX`) are noted on each
15//! spec and, where a `requires` fits, excluded by that precondition;
16//! `SmallVec::reserve` rounds the capacity up to the next power of two, so those
17//! bounds use a factor of 2.
18use core::{
19    ops::{Deref, DerefMut, Index, IndexMut},
20    slice::SliceIndex,
21    sync::atomic::AtomicU64,
22};
23use smallvec::{Array, SmallVec};
24use vstd::{
25    layout::{align_of, size_of},
26    prelude::*,
27    slice::SliceIndexSpec,
28    std_specs::iter::{FromIteratorSpec, IteratorSpec},
29};
30
31verus! {
32
33// `global layout` accepts only named types, so aliases are needed for arrays.
34type U64Array2 = [u64; 2];
35
36type AtomicU64Array2 = [AtomicU64; 2];
37
38global layout u64 is size == 8, align == 8;
39
40global layout U64Array2 is size == 16, align == 8;
41
42global layout AtomicU64 is size == 8, align == 8;
43
44global layout AtomicU64Array2 is size == 16, align == 8;
45
46/// Verus declaration for `smallvec::Array`; only the element type `Item` is surfaced.
47#[verifier::external_trait_specification]
48pub trait ExArray {
49    type ExternalTraitSpecificationFor: Array;
50
51    type Item;
52}
53
54/// Opaque external wrapper for the owned small-vector type `SmallVec<A>`.
55#[verifier::external_type_specification]
56#[verifier::external_body]
57#[verifier::reject_recursive_types(A)]
58pub struct ExSmallVec<A: Array>(SmallVec<A>);
59
60/// The contents of a `SmallVec`, modelled as a sequence of its elements.
61pub uninterp spec fn smallvec_view<A: Array>(v: &SmallVec<A>) -> Seq<A::Item>;
62
63/// The element count that `A`'s smallvec `Array` impl reports (`A::size()`).
64/// Bound-free on purpose: smallvec implements `Array` for `[T; N]` only for a
65/// fixed list of lengths (its `const_generics` feature is off), so an `Array`
66/// bound would make `[T; N]` with generic `N` fail to typecheck (E0277), and
67/// the size mirror below could not be stated for every `N`.
68pub uninterp spec fn smallvec_array_size<A>() -> nat;
69
70/// Whether `A` is a well-formed standard `Array` impl, i.e. smallvec's
71/// `SmallVec::new` construction assert holds: the reported element count and
72/// the alignment of `A` are consistent with the real layouts of `A` and
73/// `A::Item`. The two array instances used by OSTD satisfy this guard via the
74/// concrete lemmas below; any other impl needs corresponding layout and size facts.
75pub open spec fn obeys_smallvec_array<A: Array>() -> bool {
76    size_of::<A>() == smallvec_array_size::<A>() * size_of::<A::Item>() && align_of::<A>()
77        >= align_of::<A::Item>()
78}
79
80/// Mirrors smallvec's `Array::size()`: an array `[T; N]` reports its own
81/// length `N`. Trusted from the smallvec 1.15.0 source; impls exist only for
82/// its fixed size list (no `const_generics`), and other sizes can't be used
83/// as `A: Array` anywhere below.
84pub broadcast axiom fn axiom_smallvec_array_size_of_array<T, const N: usize>()
85    ensures
86        #![trigger smallvec_array_size::<[T; N]>()]
87        smallvec_array_size::<[T; N]>() == N,
88;
89
90/// The `[u64; 2]` used by `CpuSet` is a well-formed `SmallVec` backing store.
91/// Its concrete layout declarations above are checked by rustc.
92pub broadcast proof fn lemma_smallvec_array_u64_2()
93    ensures
94        #[trigger] obeys_smallvec_array::<[u64; 2]>(),
95{
96    broadcast use axiom_smallvec_array_size_of_array;
97
98}
99
100/// The `[AtomicU64; 2]` used by `AtomicCpuSet` is a well-formed `SmallVec`
101/// backing store. Its concrete layout declarations above are checked by rustc.
102pub broadcast proof fn lemma_smallvec_array_atomic_u64_2()
103    ensures
104        #[trigger] obeys_smallvec_array::<[AtomicU64; 2]>(),
105{
106    broadcast use axiom_smallvec_array_size_of_array;
107
108}
109
110/// `SmallVec`'s single-position indexing precondition is the slice bounds check.
111pub broadcast axiom fn axiom_smallvec_index_req<A: Array>(v: &SmallVec<A>, index: usize)
112    requires
113        obeys_smallvec_array::<A>(),
114    ensures
115        #![trigger <SmallVec<A> as vstd::std_specs::core::IndexSpec<usize>>::index_req(v, &index)]
116        <SmallVec<A> as vstd::std_specs::core::IndexSpec<usize>>::index_req(v, &index) == (index
117            < smallvec_view(v).len()),
118;
119
120pub broadcast group group_smallvec_models {
121    lemma_smallvec_array_u64_2,
122    lemma_smallvec_array_atomic_u64_2,
123    axiom_smallvec_index_req,
124}
125
126/// Constructs a new, empty `SmallVec`.
127///
128/// Asserts at construction that `A` is a well-formed `Array` impl; the guard admits
129/// only the trusted instances in `group_smallvec_models`.
130pub assume_specification<A: Array>[ SmallVec::<A>::new ]() -> (ret: SmallVec<A>)
131    requires
132        obeys_smallvec_array::<A>(),
133    ensures
134        smallvec_view(&ret) == Seq::<A::Item>::empty(),
135;
136
137/// Constructs a new, empty `SmallVec` with the given heap capacity, which is not modelled.
138///
139/// Panics on capacity overflow if `n * size_of::<A::Item>()` exceeds `isize::MAX`; the bound
140/// is enforced by `Layout::from_size_align` in the private `layout_array` (called from `try_grow`).
141pub assume_specification<A: Array>[ SmallVec::<A>::with_capacity ](n: usize) -> (ret: SmallVec<A>)
142    requires
143        obeys_smallvec_array::<A>(),
144        n * size_of::<A::Item>() <= isize::MAX,
145    ensures
146        smallvec_view(&ret) == Seq::<A::Item>::empty(),
147;
148
149/// The number of elements.
150pub assume_specification<A: Array>[ SmallVec::<A>::len ](v: &SmallVec<A>) -> usize
151    requires
152        obeys_smallvec_array::<A>(),
153    returns
154        smallvec_view(v).len() as usize,
155;
156
157/// Borrows the element at `index`.
158pub assume_specification<A: Array, I: SliceIndex<[A::Item]>>[ SmallVec::<A>::index ](
159    v: &SmallVec<A>,
160    index: I,
161) -> (output: &<I as SliceIndex<[A::Item]>>::Output)
162    ensures
163        obeys_smallvec_array::<A>() ==> exists|slice: &[A::Item]| #[trigger]
164            slice@ == smallvec_view(v) && call_ensures(
165                <I as SliceIndex<[A::Item]>>::index,
166                (index, slice),
167                output,
168            ),
169;
170
171/// Mutably borrows the element at `index`; writes through the borrow are reflected
172/// in the `SmallVec`'s final view.
173pub assume_specification<A: Array, I: SliceIndex<[A::Item]>>[ SmallVec::<A>::index_mut ](
174    v: &mut SmallVec<A>,
175    index: I,
176) -> (output: &mut <I as SliceIndex<[A::Item]>>::Output)
177    ensures
178        obeys_smallvec_array::<A>() ==> exists|slice: &mut [A::Item]| #[trigger]
179            slice@ == smallvec_view(old(v)) && final(slice)@ == smallvec_view(final(v))
180                && call_ensures(<I as SliceIndex<[A::Item]>>::index_mut, (index, slice), output),
181;
182
183/// Appends `value` to the end.
184///
185/// Panics on capacity overflow when full, if growing to the next power of two of
186/// `len + 1` would exceed `isize::MAX / size_of::<A::Item>()`; the bound uses a
187/// factor of 2 for the power-of-two rounding.
188pub assume_specification<A: Array>[ SmallVec::<A>::push ](v: &mut SmallVec<A>, value: A::Item)
189    requires
190        obeys_smallvec_array::<A>(),
191        2 * (smallvec_view(v).len() + 1) * size_of::<A::Item>() <= isize::MAX,
192    ensures
193        smallvec_view(final(v)) == smallvec_view(old(v)).push(value),
194;
195
196/// Resizes so the length is `new_len`, cloning `value` into new positions. Mirrors `Vec::resize`.
197///
198/// Panics on capacity overflow when growing, if the allocation rounded up to the
199/// next power of two of `new_len` would exceed `isize::MAX / size_of::<A::Item>()`.
200pub assume_specification<A: Array>[ SmallVec::<A>::resize ](
201    v: &mut SmallVec<A>,
202    new_len: usize,
203    value: A::Item,
204) where A::Item: Clone
205    requires
206        obeys_smallvec_array::<A>(),
207        2 * new_len * size_of::<A::Item>() <= isize::MAX,
208    ensures
209        new_len <= smallvec_view(old(v)).len() ==> smallvec_view(final(v)) == smallvec_view(
210            old(v),
211        )[..new_len],
212        new_len > smallvec_view(old(v)).len() ==> {
213            &&& smallvec_view(final(v)).len() == new_len
214            &&& smallvec_view(final(v))[..smallvec_view(old(v)).len()] == smallvec_view(old(v))
215            &&& forall|i: int|
216                #![trigger smallvec_view(final(v))[i]]
217                smallvec_view(old(v)).len() <= i < new_len ==> cloned::<A::Item>(
218                    value,
219                    smallvec_view(final(v))[i],
220                )
221        },
222;
223
224/// Views the elements as a borrowed slice.
225pub assume_specification<A: Array>[ SmallVec::<A>::as_slice ](v: &SmallVec<A>) -> (ret: &[A::Item])
226    requires
227        obeys_smallvec_array::<A>(),
228    ensures
229        ret@ == smallvec_view(v),
230;
231
232/// Views the elements as a mutably borrowed slice; writes through the returned borrow are
233/// reflected in the `SmallVec`'s final view.
234pub assume_specification<A: Array>[ SmallVec::<A>::as_mut_slice ](v: &mut SmallVec<A>) -> (ret:
235    &mut [A::Item])
236    requires
237        obeys_smallvec_array::<A>(),
238    ensures
239        ret@ == smallvec_view(old(v)),
240        final(ret)@ == smallvec_view(final(v)),
241;
242
243/// `SmallVec` derefs to a slice over exactly its own elements; the guard is an
244/// ensures-implication since `requires` is disallowed on trait-method specs.
245pub assume_specification<A: Array>[ <SmallVec<A> as Deref>::deref ](v: &SmallVec<A>) -> (ret:
246    &[A::Item])
247    ensures
248        obeys_smallvec_array::<A>() ==> ret@ == smallvec_view(v),
249;
250
251/// `SmallVec` derefs mutably to a slice over exactly its own elements; a mutation performed
252/// through the returned borrow is reflected in the `SmallVec`'s final view (guard as an
253/// ensures-implication for the same reason as [`Deref`]).
254pub assume_specification<A: Array>[ <SmallVec<A> as DerefMut>::deref_mut ](
255    v: &mut SmallVec<A>,
256) -> (ret: &mut [A::Item])
257    ensures
258        obeys_smallvec_array::<A>() ==> {
259            &&& ret@ == smallvec_view(old(v))
260            &&& final(ret)@ == smallvec_view(final(v))
261        },
262;
263
264/// Verus proxy for the owned `SmallVec` iterator `smallvec::IntoIter`
265/// (mirrors the array-IntoIter precedent in `crate::external::iter`).
266#[verifier::external_type_specification]
267#[verifier::external_body]
268#[verifier::reject_recursive_types(A)]
269pub struct ExSmallVecIntoIter<A: Array>(smallvec::IntoIter<A>);
270
271/// Consumes the `SmallVec`, yielding exactly its elements from left to right,
272/// once each. Guarded as an ensures-implication since `requires` is
273/// disallowed on trait-method specs (same as [`Deref`]).
274pub assume_specification<A: Array>[ <SmallVec<A> as IntoIterator>::into_iter ](
275    v: SmallVec<A>,
276) -> (iter: <SmallVec<A> as IntoIterator>::IntoIter)
277    ensures
278        obeys_smallvec_array::<A>() ==> {
279            &&& IteratorSpec::obeys_prophetic_iter_laws(&iter)
280            &&& IteratorSpec::will_return_none(&iter)
281            &&& IteratorSpec::remaining(&iter) == smallvec_view(&v)
282            &&& IteratorSpec::decrease(&iter) == Some(smallvec_view(&v).len())
283        },
284;
285
286/// Collecting a terminated iterator into a `SmallVec` yields exactly its
287/// remaining elements, in order. Stated as an axiom because the orphan rule
288/// (E0117) prevents implementing `FromIteratorSpecImpl` for `SmallVec` here.
289pub broadcast axiom fn axiom_smallvec_from_iter_ensures<A: Array>(
290    remaining: Seq<A::Item>,
291    s: SmallVec<A>,
292)
293    ensures
294        obeys_smallvec_array::<A>() ==> #[trigger] FromIteratorSpec::from_iter_ensures(remaining, s)
295            == (remaining == smallvec_view(&s)),
296;
297
298} // verus!
vstd_extra/external/smallvec.rs

vstd_extra/external/
smallvec.rs
