Module smallvec 

Verus specifications for the third-party smallvec crate, trusted as TCB from inspection of the smallvec-1.15.0 source (src/lib.rs) and centralized here rather than beside an OSTD caller. cpu/set.rs is currently the only consumer (SmallVec<[u64; 2]>).

The model is a Seq<A::Item>: the views below equate every executed SmallVec operation to a Seq operation, and Deref/DerefMut bridge to the std [A::Item] slice so that indexing, len, and iter reuse vstd’s slice specifications rather than being re-axiomatized.

Every operation below is guarded by obeys_smallvec_array::<A> (see its documentation).

Allocation-growth panics (capacity overflow past isize::MAX) are noted on each spec and, where a requires fits, excluded by that precondition; SmallVec::reserve rounds the capacity up to the next power of two, so those bounds use a factor of 2.

Structs

ExSmallVec

Opaque external wrapper for the owned small-vector type SmallVec<A>.

ExSmallVecIntoIter

Verus proxy for the owned SmallVec iterator smallvec::IntoIter (mirrors the array-IntoIter precedent in crate::external::iter).

Traits

ExArray

Verus declaration for smallvec::Array; only the element type Item is surfaced.

Functions

_verus_external_fn_specification_46_SmallVec_32__58__58__32__60__32_A_32__62__32__58__58__32_new^⚠

_verus_external_fn_specification_47_SmallVec_32__58__58__32__60__32_A_32__62__32__58__58__32_with__capacity^⚠

_verus_external_fn_specification_48_SmallVec_32__58__58__32__60__32_A_32__62__32__58__58__32_len^⚠

_verus_external_fn_specification_49_SmallVec_32__58__58__32__60__32_A_32__62__32__58__58__32_index^⚠

_verus_external_fn_specification_50_SmallVec_32__58__58__32__60__32_A_32__62__32__58__58__32_index__mut^⚠

_verus_external_fn_specification_51_SmallVec_32__58__58__32__60__32_A_32__62__32__58__58__32_push^⚠

_verus_external_fn_specification_52_SmallVec_32__58__58__32__60__32_A_32__62__32__58__58__32_resize^⚠

_verus_external_fn_specification_53_SmallVec_32__58__58__32__60__32_A_32__62__32__58__58__32_as__slice^⚠

_verus_external_fn_specification_54_SmallVec_32__58__58__32__60__32_A_32__62__32__58__58__32_as__mut__slice^⚠

_verus_external_fn_specification_55__60__32_SmallVec_32__60__32_A_32__62__32_as_32_Deref_32__62__32__58__58__32_deref^⚠

_verus_external_fn_specification_56__60__32_SmallVec_32__60__32_A_32__62__32_as_32_DerefMut_32__62__32__58__58__32_deref__mut^⚠

_verus_external_fn_specification_57__60__32_SmallVec_32__60__32_A_32__62__32_as_32_IntoIterator_32__62__32__58__58__32_into__iter^⚠

axiom_smallvec_array_size_of_array

axiom_smallvec_from_iter_ensures

axiom_smallvec_index_req

group_smallvec_models

lemma_smallvec_array_atomic_u64_2

lemma_smallvec_array_u64_2

obeys_smallvec_array

smallvec_array_size

smallvec_view