Module external 

Specifications for functions from Rust standard library but not specified in vstd.

These specifications are determined with careful inspection of the std library source code and documentation, and trusted as TCB. They are subject to change if vstd covers more cases in the future.

Re-exports

pub use cmp::*;

pub use ilog2::*;

pub use int_specs::*;

pub use iter::*;

pub use nonnull::*;

pub use ptr::*;

pub use range::*;

pub use slice::*;

pub use smallvec::*;

pub use smart_ptr::*;

pub use time::*;

Modules

bits

Specifications for bit-related standard-library functions.

cmp

Specifications for the free comparison functions missing from vstd.

convert

derefDeprecated

ilog2

int_specs

Specs for stdlib methods on integer types that aren’t covered by vstd.

iter

Specification for owned-array iteration not yet modeled by vstd.

nonnull

ptr

range

slice

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]>).

smart_ptr

time

Structs

ExBitSlice

Opaque external wrapper for the borrowed bit-slice type.

ExBitVec

Opaque external wrapper for the owned bitmap type.

ExLsb0

Verus declaration for bitvec’s default Lsb0 bit order (a zero-sized marker).

Traits

ExBitOrder

Type-level declaration only; this does not assume any BitOrder semantics.

ExBitSliceIndex

Verus declaration for bitvec’s BitSliceIndex trait. Only the associated types are surfaced; id-alloc uses the Range<usize> instance, whose Immut is a &BitSlice.

ExBitStore

Type-level declaration only; this does not assume any BitStore semantics.

Functions

_verus_external_fn_specification_1__60__32_BitVec_32__60__32_T_44__32_O_32__62__32_as_32_Deref_32__62__32__58__58__32_deref^⚠

_verus_external_fn_specification_2__60__32_BitVec_32__60__32_T_44__32_O_32__62__32_as_32_DerefMut_32__62__32__58__58__32_deref__mut^⚠

_verus_external_fn_specification_3_BitVec_32__58__58__32__60__32_T_44__32_O_32__62__32__58__58__32_with__capacity^⚠

_verus_external_fn_specification_4_BitVec_32__58__58__32__60__32_T_44__32_O_32__62__32__58__58__32_resize^⚠

_verus_external_fn_specification_5_BitVec_32__58__58__32__60__32_T_44__32_O_32__62__32__58__58__32_len^⚠

_verus_external_fn_specification_6__60__32_BitVec_32__60__32_T_44__32_O_32__62__32_as_32_Index_32__60__32_Idx_32__62__32__62__32__58__58__32_index^⚠

_verus_external_fn_specification_7_BitSlice_32__58__58__32__60__32_T_44__32_O_32__62__32__58__58__32_set^⚠

_verus_external_fn_specification_8_BitSlice_32__58__58__32__60__32_T_44__32_O_44__32__62__32__58__58__32_get^⚠

_verus_external_fn_specification_9_BitSlice_32__58__58__32__60__32_T_44__32_O_32__62__32__58__58__32_first__zero^⚠

_verus_external_fn_specification_59_core_32__58__58__32_hint_32__58__58__32_spin__loop^⚠

axiom_bitslice_get_range

axiom_bitvec_index_req

axiom_bitvec_index_usize

axiom_bitvec_len_bound

axiom_range_bitslice_get_model

axiom_u8_bitvec_model

axiom_u32_bitvec_model

axiom_u64_bitvec_model

axiom_usize_bitslice_index_model

axiom_usize_bitvec_model

bitslice_get_value

bitslice_view

bitvec_index_value

bitvec_view

group_bitvec_models

obeys_bitslice_get_model

obeys_bitslice_index_model

obeys_bitvec_model