Struct VstdSpecsForRustStdLib

Source

pub struct VstdSpecsForRustStdLib;

Implementations§

Source §

impl VstdSpecsForRustStdLib

Source

pub unsafe exec fn _verus_external_fn_specification_060323832__39_a_32__91_T_59__32_N_93__32_as_32_core_325858__32_iter_325858__32_IntoIterator_3262325858__32_into__iter<'a, T, const N: usize>( s: &'a [T; N], ) -> iter : Iter<'a, T>

ensures

iter == spec_array_iter(s),

IteratorSpec::decrease(&iter) is Some,

IteratorSpec::initial_value_relation(&iter, &iter),

Specification for <&'a [T; N] as core::iter::IntoIterator>::into_iter

Source

pub unsafe exec fn _verus_external_fn_specification_16032__91_T_59__32_N_93326232585832_as__slice<T, const N: usize>( ar: &[T; N], ) -> out : &[T]

ensures

ar@ == out@,

Specification for [<[T; N]>::as_slice]

Source §

impl VstdSpecsForRustStdLib

Source

pub unsafe exec fn _verus_external_fn_specification_26032_f32_32_as_32_Clone_3262325858__32_clone( f: &f32, ) -> res : f32

ensures

res == f,

Specification for <f32 as Clone>::clone

Source

pub unsafe exec fn _verus_external_fn_specification_36032_f64_32_as_32_Clone_3262325858__32_clone( f: &f64, ) -> res : f64

ensures

res == f,

Specification for <f64 as Clone>::clone

Source §

impl VstdSpecsForRustStdLib

Source

pub unsafe exec fn _verus_external_fn_specification_4_core_325858__32_mem_325858__32_size__of_3258583260__32_V_32__62_<V>() -> u : usize

ensures

u as nat == size_of::<V>(),

Specification for core::mem::size_of::<V>

Source

pub unsafe exec fn _verus_external_fn_specification_5_core_325858__32_mem_325858__32_align__of_3258583260__32_V_32__62_<V>() -> u : usize

ensures

u as nat == align_of::<V>(),

Specification for core::mem::align_of::<V>

Source

pub unsafe exec fn _verus_external_fn_specification_6_core_325858__32_mem_325858__32_sizeofval_3258583260__32_V_32__62_<V: ?Sized>( val: &V, ) -> u : usize

ensures

u as nat == spec_size_of_val::<V>(val),

Specification for core::mem::size_of_val::<V>

Source

pub unsafe exec fn _verus_external_fn_specification_7_core_325858__32_mem_325858__32_alignofval_3258583260__32_V_32__62_<V: ?Sized>( val: &V, ) -> u : usize

ensures

u as nat == spec_align_of_val::<V>(val),

Specification for core::mem::align_of_val::<V>

Source §

impl VstdSpecsForRustStdLib

Source

pub unsafe exec fn _verus_external_fn_specification_115560324232_mut_32_T_3262325858__32_addr<T: PointeeSized>( p: *mut T, ) -> addr : usize

ensures

addr == spec_addr(p),

Specification for <*mut T>::addr

Source

pub unsafe exec fn _verus_external_fn_specification_115660324232_mut_32_T_3262325858__32_with__addr<T: PointeeSized>( p: mut T, addr: usize, ) -> q : mut T

ensures

q == spec_with_addr(p, addr),

Specification for <*mut T>::with_addr

Source §

impl VstdSpecsForRustStdLib

Source

pub unsafe exec fn _verus_external_fn_specification_115360324232_const_32_T_3262325858__32_addr<T: PointeeSized>( p: *const T, ) -> addr : usize

ensures

addr == spec_addr(p),

Specification for <*const T>::addr

Source

pub unsafe exec fn _verus_external_fn_specification_115460324232_const_32_T_3262325858__32_with__addr<T: PointeeSized>( p: const T, addr: usize, ) -> q : const T

ensures

q == spec_with_addr(p, addr),

Specification for <*const T>::with_addr

Source §

impl VstdSpecsForRustStdLib

Source

pub unsafe exec fn _verus_external_fn_specification_860324232_mut_32_T_32_as_32_PartialEq_3260324232_mut_32_T_32623262325858__32_eq<T: PointeeSized>( x: &mut T, y: &mut T, ) -> res : bool

ensures

res <==> (x@.addr == y@.addr) && (x@.metadata == y@.metadata),

Specification for <*mut T as PartialEq<*mut T>>::eq Compares the address and metadata of two pointers.

Note that this does NOT compare provenance, which does not exist in the runtime pointer representation (i.e., it only exists in the Rust abstract machine).

Source

pub unsafe exec fn _verus_external_fn_specification_960324232_const_32_T_32_as_32_PartialEq_3260324232_const_32_T_32623262325858__32_eq<T: PointeeSized>( x: &const T, y: &const T, ) -> res : bool

ensures

res <==> (x@.addr == y@.addr) && (x@.metadata == y@.metadata),

Specification for <*const T as PartialEq<*const T>>::eq Compares the address and metadata of two pointers.

Note that this does NOT compare provenance, which does not exist in the runtime pointer representation (i.e., it only exists in the Rust abstract machine).

Source

pub unsafe exec fn _verus_external_fn_specification_10_core_325858__32_ptr_325858__32_null<T: PointeeSized + Pointee<Metadata = ()>>() -> res : *const T

ensures

res == ptr_null::<T>(),

Specification for core::ptr::null

Source

pub unsafe exec fn _verus_external_fn_specification_11_core_325858__32_ptr_325858__32_null__mut<T: PointeeSized + Pointee<Metadata = ()>>() -> res : *mut T

ensures

res == ptr_null_mut::<T>(),

Specification for core::ptr::null_mut

Source §

impl VstdSpecsForRustStdLib

Source

pub unsafe exec fn _verus_external_fn_specification_126032__91_T_93326232585832_len<T>( slice: &[T], ) -> len : usize

returns

spec_slice_len(slice),

Specification for [<[T]>::len]

Source

pub unsafe exec fn _verus_external_fn_specification_136032__91_T_93326232585832_is__empty<T>( slice: &[T], ) -> b : bool

ensures

b <==> slice@.len() == 0,

Specification for [<[T]>::is_empty]

Source

pub unsafe exec fn _verus_external_fn_specification_146032__91_T_93326232585832_get_3258583260__32_I_32__62_<T, I>( slice: &[T], i: I, ) -> b : Option<&>::Output>
where I: SliceIndex<[T]>,

returns

spec_slice_get(slice, i),

Specification for [<[T]>::get::]

Source §

impl VstdSpecsForRustStdLib

Source

pub unsafe exec fn _verus_external_fn_specification_15_str_325858__32_is__ascii( s: &str, ) -> b : bool

ensures

b == is_ascii(s),

Specification for str::is_ascii

Source

pub unsafe exec fn _verus_external_fn_specification_16_str_325858__32_to__owned( s: &str, ) -> res : String

ensures

s@ == res@,

Specification for str::to_owned

Source

pub unsafe exec fn _verus_external_fn_specification_17_str_325858__32_as__bytes( s: &str, ) -> b : &[u8] ⓘ

ensures

b@ == s.spec_bytes(),

Specification for str::as_bytes

Source

pub unsafe exec fn _verus_external_fn_specification_18_str_325858__32_len( s: &str, ) -> usize

returns

s.spec_bytes().len() as usize,

Specification for str::len

Source

pub unsafe exec fn _verus_external_fn_specification_19_str_325858__32_is__empty( s: &str, ) -> bool

returns

s@.len() == 0,

Specification for str::is_empty

Source

pub unsafe exec fn _verus_external_fn_specification_20_str_325858__32_ischarboundary( s: &str, index: usize, ) -> bool

returns

is_char_boundary(s.spec_bytes(), index as int),

Specification for str::is_char_boundary

Source

pub unsafe exec fn _verus_external_fn_specification_21_str_325858__32_split__at( s: &str, mid: usize, ) -> res : (&str, &str)

requires

is_char_boundary(s.spec_bytes(), mid as int),

ensures

res.0.spec_bytes() =~= s.spec_bytes().subrange(0, mid as int),

res.1.spec_bytes() =~= s.spec_bytes().subrange(mid as int, s.spec_bytes().len() as int),

Specification for str::split_at

Source

pub unsafe exec fn _verus_external_fn_specification_22_str_325858__32_fromutf8unchecked( v: &[u8], ) -> res : &str

requires

valid_utf8(v@),

ensures

res.spec_bytes() =~= v@,

Specification for str::from_utf8_unchecked

Source

pub unsafe exec fn _verus_external_fn_specification_236032_T_32_as_32_ToString_3262325858__32_to__string<T: Display + ?Sized>( t: &T, ) -> res : String

ensures

to_string_from_display_ensures::<T>(t, res),

Specification for <T as ToString>::to_string

Source

pub unsafe exec fn _verus_external_fn_specification_24_String_325858__32_as__str<'a>( s: &'a String, ) -> res : &'a str

ensures

res@ == s@,

Specification for String::as_str

Source

pub unsafe exec fn _verus_external_fn_specification_256032_String_32_as_32_core_325858__32_ops_325858__32_Deref_3262325858__32_deref<'a>( s: &'a String, ) -> res : &'a str

ensures

res@ == s@,

Specification for <String as core::ops::Deref>::deref

Source

pub unsafe exec fn _verus_external_fn_specification_266032_String_32_as_32_Clone_3262325858__32_clone( s: &String, ) -> res : String

ensures

res == s,

Specification for <String as Clone>::clone

Source

pub unsafe exec fn _verus_external_fn_specification_276032_String_32_as_32_PartialEq_3262325858__32_eq( s: &String, other: &String, ) -> res : bool

ensures

res == (s@ == other@),

Specification for <String as PartialEq>::eq

Source

pub unsafe exec fn _verus_external_fn_specification_28_String_325858__32_new() -> res : String

ensures

res@ == Seq::<char>::empty(),

Specification for String::new

Source

pub unsafe exec fn _verus_external_fn_specification_296032_String_32_as_32_core_325858__32_default_325858__32_Default_3262325858__32_default() -> r : String

ensures

r@ == Seq::<char>::empty(),

Specification for <String as core::default::Default>::default

Source

pub unsafe exec fn _verus_external_fn_specification_30_str_325858__32_chars( s: &str, ) -> iter : Chars<'_>

ensures

iter == spec_iter(s),

IteratorSpec::decrease(&iter) is Some,

IteratorSpec::initial_value_relation(&iter, &iter),

Specification for str::chars

Source §

impl VstdSpecsForRustStdLib

Source

pub unsafe exec fn _verus_external_fn_specification_31_alloc_325858__32_boxed_325858__32_boxassumeinitintovec__unsafe<T, const N: usize>( vals: Box<MaybeUninit<[T; N]>>, ) -> result : Vec<T>

requires

vals.mem_contents() is Init,

ensures

vals.mem_contents() matches MemContents::Init(array) && result@ == array@,

Specification for [alloc::boxed::box_assume_init_into_vec_unsafe]

Source

pub unsafe exec fn _verus_external_fn_specification_32_alloc_325858__32_intrinsics_325858__32_writeboxvia__move<T>( _0: Box<MaybeUninit<T>>, v: T, ) -> result : Box<MaybeUninit<T>>

ensures

result.mem_contents() == MemContents::Init(v),

Specification for alloc::intrinsics::write_box_via_move

Source

pub unsafe exec fn _verus_external_fn_specification_33_alloc_325858__32_boxed_325858__32_Box_3258583260__32_T_3262325858__32_new__uninit<T>() -> Box<MaybeUninit<T>>

Specification for alloc::boxed::Box::<T>::new_uninit

Source §

Specification for AtomicU8::swap

Source §

impl VstdSpecsForRustStdLib

Source

pub unsafe exec fn _verus_external_fn_specification_446032_AtomicU8_3262325858__32_fetch__add( atomic: &AtomicU8, val: u8, order: Ordering, ) -> u8

Specification for AtomicU8::fetch_add

Source

pub unsafe exec fn _verus_external_fn_specification_456032_AtomicU8_3262325858__32_fetch__sub( atomic: &AtomicU8, val: u8, order: Ordering, ) -> u8

Specification for AtomicU8::fetch_sub

Source

pub unsafe exec fn _verus_external_fn_specification_466032_AtomicU8_3262325858__32_fetch__min( atomic: &AtomicU8, val: u8, order: Ordering, ) -> u8

Specification for AtomicU8::fetch_min

Source

pub unsafe exec fn _verus_external_fn_specification_476032_AtomicU8_3262325858__32_fetch__max( atomic: &AtomicU8, val: u8, order: Ordering, ) -> u8

Specification for AtomicU8::fetch_max

Source §

Specification for AtomicU16::swap

Source §

impl VstdSpecsForRustStdLib

Source

pub unsafe exec fn _verus_external_fn_specification_586032_AtomicU16_3262325858__32_fetch__add( atomic: &AtomicU16, val: u16, order: Ordering, ) -> u16

Specification for AtomicU16::fetch_add

Source

pub unsafe exec fn _verus_external_fn_specification_596032_AtomicU16_3262325858__32_fetch__sub( atomic: &AtomicU16, val: u16, order: Ordering, ) -> u16

Specification for AtomicU16::fetch_sub

Source

pub unsafe exec fn _verus_external_fn_specification_606032_AtomicU16_3262325858__32_fetch__min( atomic: &AtomicU16, val: u16, order: Ordering, ) -> u16

Specification for AtomicU16::fetch_min

Source

pub unsafe exec fn _verus_external_fn_specification_616032_AtomicU16_3262325858__32_fetch__max( atomic: &AtomicU16, val: u16, order: Ordering, ) -> u16

Specification for AtomicU16::fetch_max

Source §

Specification for AtomicU32::swap

Source §

impl VstdSpecsForRustStdLib

Source

pub unsafe exec fn _verus_external_fn_specification_726032_AtomicU32_3262325858__32_fetch__add( atomic: &AtomicU32, val: u32, order: Ordering, ) -> u32

Specification for AtomicU32::fetch_add

Source

pub unsafe exec fn _verus_external_fn_specification_736032_AtomicU32_3262325858__32_fetch__sub( atomic: &AtomicU32, val: u32, order: Ordering, ) -> u32

Specification for AtomicU32::fetch_sub

Source

pub unsafe exec fn _verus_external_fn_specification_746032_AtomicU32_3262325858__32_fetch__min( atomic: &AtomicU32, val: u32, order: Ordering, ) -> u32

Specification for AtomicU32::fetch_min

Source

pub unsafe exec fn _verus_external_fn_specification_756032_AtomicU32_3262325858__32_fetch__max( atomic: &AtomicU32, val: u32, order: Ordering, ) -> u32

Specification for AtomicU32::fetch_max

Source §

Specification for AtomicU64::swap

Source §

impl VstdSpecsForRustStdLib

Source

pub unsafe exec fn _verus_external_fn_specification_866032_AtomicU64_3262325858__32_fetch__add( atomic: &AtomicU64, val: u64, order: Ordering, ) -> u64

Specification for AtomicU64::fetch_add

Source

pub unsafe exec fn _verus_external_fn_specification_876032_AtomicU64_3262325858__32_fetch__sub( atomic: &AtomicU64, val: u64, order: Ordering, ) -> u64

Specification for AtomicU64::fetch_sub

Source

pub unsafe exec fn _verus_external_fn_specification_886032_AtomicU64_3262325858__32_fetch__min( atomic: &AtomicU64, val: u64, order: Ordering, ) -> u64

Specification for AtomicU64::fetch_min

Source

pub unsafe exec fn _verus_external_fn_specification_896032_AtomicU64_3262325858__32_fetch__max( atomic: &AtomicU64, val: u64, order: Ordering, ) -> u64

Specification for AtomicU64::fetch_max

Source §

Specification for AtomicUsize::swap

Source §

impl VstdSpecsForRustStdLib

Source

pub unsafe exec fn _verus_external_fn_specification_1006032_AtomicUsize_3262325858__32_fetch__add( atomic: &AtomicUsize, val: usize, order: Ordering, ) -> usize

Specification for AtomicUsize::fetch_add

Source

pub unsafe exec fn _verus_external_fn_specification_1016032_AtomicUsize_3262325858__32_fetch__sub( atomic: &AtomicUsize, val: usize, order: Ordering, ) -> usize

Specification for AtomicUsize::fetch_sub

Source

pub unsafe exec fn _verus_external_fn_specification_1026032_AtomicUsize_3262325858__32_fetch__min( atomic: &AtomicUsize, val: usize, order: Ordering, ) -> usize

Specification for AtomicUsize::fetch_min

Source

pub unsafe exec fn _verus_external_fn_specification_1036032_AtomicUsize_3262325858__32_fetch__max( atomic: &AtomicUsize, val: usize, order: Ordering, ) -> usize

Specification for AtomicUsize::fetch_max

Source §

Specification for AtomicI8::swap

Source §

impl VstdSpecsForRustStdLib

Source

pub unsafe exec fn _verus_external_fn_specification_1146032_AtomicI8_3262325858__32_fetch__add( atomic: &AtomicI8, val: i8, order: Ordering, ) -> i8

Specification for AtomicI8::fetch_add

Source

pub unsafe exec fn _verus_external_fn_specification_1156032_AtomicI8_3262325858__32_fetch__sub( atomic: &AtomicI8, val: i8, order: Ordering, ) -> i8

Specification for AtomicI8::fetch_sub

Source

pub unsafe exec fn _verus_external_fn_specification_1166032_AtomicI8_3262325858__32_fetch__min( atomic: &AtomicI8, val: i8, order: Ordering, ) -> i8

Specification for AtomicI8::fetch_min

Source

pub unsafe exec fn _verus_external_fn_specification_1176032_AtomicI8_3262325858__32_fetch__max( atomic: &AtomicI8, val: i8, order: Ordering, ) -> i8

Specification for AtomicI8::fetch_max

Source §

Specification for AtomicI16::swap

Source §

impl VstdSpecsForRustStdLib

Source

pub unsafe exec fn _verus_external_fn_specification_1286032_AtomicI16_3262325858__32_fetch__add( atomic: &AtomicI16, val: i16, order: Ordering, ) -> i16

Specification for AtomicI16::fetch_add

Source

pub unsafe exec fn _verus_external_fn_specification_1296032_AtomicI16_3262325858__32_fetch__sub( atomic: &AtomicI16, val: i16, order: Ordering, ) -> i16

Specification for AtomicI16::fetch_sub

Source

pub unsafe exec fn _verus_external_fn_specification_1306032_AtomicI16_3262325858__32_fetch__min( atomic: &AtomicI16, val: i16, order: Ordering, ) -> i16

Specification for AtomicI16::fetch_min

Source

pub unsafe exec fn _verus_external_fn_specification_1316032_AtomicI16_3262325858__32_fetch__max( atomic: &AtomicI16, val: i16, order: Ordering, ) -> i16

Specification for AtomicI16::fetch_max

Source §

Specification for AtomicI32::swap

Source §

impl VstdSpecsForRustStdLib

Source

pub unsafe exec fn _verus_external_fn_specification_1426032_AtomicI32_3262325858__32_fetch__add( atomic: &AtomicI32, val: i32, order: Ordering, ) -> i32

Specification for AtomicI32::fetch_add

Source

pub unsafe exec fn _verus_external_fn_specification_1436032_AtomicI32_3262325858__32_fetch__sub( atomic: &AtomicI32, val: i32, order: Ordering, ) -> i32

Specification for AtomicI32::fetch_sub

Source

pub unsafe exec fn _verus_external_fn_specification_1446032_AtomicI32_3262325858__32_fetch__min( atomic: &AtomicI32, val: i32, order: Ordering, ) -> i32

Specification for AtomicI32::fetch_min

Source

pub unsafe exec fn _verus_external_fn_specification_1456032_AtomicI32_3262325858__32_fetch__max( atomic: &AtomicI32, val: i32, order: Ordering, ) -> i32

Specification for AtomicI32::fetch_max

Source §

Specification for AtomicI64::swap

Source §

impl VstdSpecsForRustStdLib

Source

pub unsafe exec fn _verus_external_fn_specification_1566032_AtomicI64_3262325858__32_fetch__add( atomic: &AtomicI64, val: i64, order: Ordering, ) -> i64

Specification for AtomicI64::fetch_add

Source

pub unsafe exec fn _verus_external_fn_specification_1576032_AtomicI64_3262325858__32_fetch__sub( atomic: &AtomicI64, val: i64, order: Ordering, ) -> i64

Specification for AtomicI64::fetch_sub

Source

pub unsafe exec fn _verus_external_fn_specification_1586032_AtomicI64_3262325858__32_fetch__min( atomic: &AtomicI64, val: i64, order: Ordering, ) -> i64

Specification for AtomicI64::fetch_min

Source

pub unsafe exec fn _verus_external_fn_specification_1596032_AtomicI64_3262325858__32_fetch__max( atomic: &AtomicI64, val: i64, order: Ordering, ) -> i64

Specification for AtomicI64::fetch_max

Source §

Specification for AtomicIsize::swap

Source §

impl VstdSpecsForRustStdLib

Source

pub unsafe exec fn _verus_external_fn_specification_1706032_AtomicIsize_3262325858__32_fetch__add( atomic: &AtomicIsize, val: isize, order: Ordering, ) -> isize

Specification for AtomicIsize::fetch_add

Source

pub unsafe exec fn _verus_external_fn_specification_1716032_AtomicIsize_3262325858__32_fetch__sub( atomic: &AtomicIsize, val: isize, order: Ordering, ) -> isize

Specification for AtomicIsize::fetch_sub

Source

pub unsafe exec fn _verus_external_fn_specification_1726032_AtomicIsize_3262325858__32_fetch__min( atomic: &AtomicIsize, val: isize, order: Ordering, ) -> isize

Specification for AtomicIsize::fetch_min

Source

pub unsafe exec fn _verus_external_fn_specification_1736032_AtomicIsize_3262325858__32_fetch__max( atomic: &AtomicIsize, val: isize, order: Ordering, ) -> isize

Specification for AtomicIsize::fetch_max

Source §

Specification for AtomicBool::swap

Source §

impl VstdSpecsForRustStdLib

Source

pub unsafe exec fn _verus_external_fn_specification_184_u8_325858__32_trailing__zeros( i: u8, ) -> r : u32

ensures

r == u8_trailing_zeros(i),

Specification for u8::trailing_zeros

Source

pub unsafe exec fn _verus_external_fn_specification_185_u8_325858__32_trailing__ones( i: u8, ) -> r : u32

ensures

r == u8_trailing_ones(i),

Specification for u8::trailing_ones

Source

pub unsafe exec fn _verus_external_fn_specification_186_u8_325858__32_leading__zeros( i: u8, ) -> r : u32

ensures

r == u8_leading_zeros(i),

Specification for u8::leading_zeros

Source

pub unsafe exec fn _verus_external_fn_specification_187_u8_325858__32_leading__ones( i: u8, ) -> r : u32

ensures

r == u8_leading_ones(i),

Specification for u8::leading_ones

Source

pub unsafe exec fn _verus_external_fn_specification_188_u16_325858__32_trailing__zeros( i: u16, ) -> r : u32

ensures

r == u16_trailing_zeros(i),

Specification for u16::trailing_zeros

Source

pub unsafe exec fn _verus_external_fn_specification_189_u16_325858__32_trailing__ones( i: u16, ) -> r : u32

ensures

r == u16_trailing_ones(i),

Specification for u16::trailing_ones

Source

pub unsafe exec fn _verus_external_fn_specification_190_u16_325858__32_leading__zeros( i: u16, ) -> r : u32

ensures

r == u16_leading_zeros(i),

Specification for u16::leading_zeros

Source

pub unsafe exec fn _verus_external_fn_specification_191_u16_325858__32_leading__ones( i: u16, ) -> r : u32

ensures

r == u16_leading_ones(i),

Specification for u16::leading_ones

Source

pub unsafe exec fn _verus_external_fn_specification_192_u32_325858__32_trailing__zeros( i: u32, ) -> r : u32

ensures

r == u32_trailing_zeros(i),

Specification for u32::trailing_zeros

Source

pub unsafe exec fn _verus_external_fn_specification_193_u32_325858__32_trailing__ones( i: u32, ) -> r : u32

ensures

r == u32_trailing_ones(i),

Specification for u32::trailing_ones

Source

pub unsafe exec fn _verus_external_fn_specification_194_u32_325858__32_leading__zeros( i: u32, ) -> r : u32

ensures

r == u32_leading_zeros(i),

Specification for u32::leading_zeros

Source

pub unsafe exec fn _verus_external_fn_specification_195_u32_325858__32_leading__ones( i: u32, ) -> r : u32

ensures

r == u32_leading_ones(i),

Specification for u32::leading_ones

Source

pub unsafe exec fn _verus_external_fn_specification_196_u64_325858__32_trailing__zeros( i: u64, ) -> r : u32

ensures

r == u64_trailing_zeros(i),

Specification for u64::trailing_zeros

Source

pub unsafe exec fn _verus_external_fn_specification_197_u64_325858__32_trailing__ones( i: u64, ) -> r : u32

ensures

r == u64_trailing_ones(i),

Specification for u64::trailing_ones

Source

pub unsafe exec fn _verus_external_fn_specification_198_u64_325858__32_leading__zeros( i: u64, ) -> r : u32

ensures

r as int == u64_leading_zeros(i),

Specification for u64::leading_zeros

Source

pub unsafe exec fn _verus_external_fn_specification_199_u64_325858__32_leading__ones( i: u64, ) -> r : u32

ensures

r == u64_leading_ones(i),

Specification for u64::leading_ones

Source §

impl VstdSpecsForRustStdLib

Source

pub unsafe exec fn _verus_external_fn_specification_200_char_325858__32_len__utf8( c: char, ) -> usize

returns

encode_scalar(c as u32).len() as usize,

Specification for char::len_utf8 The byte width of c’s UTF-8 encoding, using the same scalar-value boundaries as encode_scalar.

Source

pub unsafe exec fn _verus_external_fn_specification_201_char_325858__32_is__whitespace( c: char, ) -> res : bool

returns

is_white_space(c),

Specification for char::is_whitespace

Source §

impl VstdSpecsForRustStdLib

Source

pub unsafe exec fn _verus_external_fn_specification_2026032_bool_32_as_32_Clone_3262325858__32_clone( b: &bool, ) -> res : bool

returns

b,

Specification for <bool as Clone>::clone

Source

pub unsafe exec fn _verus_external_fn_specification_2036032_char_32_as_32_Clone_3262325858__32_clone( c: &char, ) -> res : char

returns

c,

Specification for <char as Clone>::clone

Source

pub unsafe exec fn _verus_external_fn_specification_20460323832__39_b_32_T_32_as_32_Clone_3262325858__32_clone<'b, 'a, T: PointeeSized>( b: &'a &'b T, ) -> res : &'b T

ensures

res == b,

Specification for <&'b T as Clone>::clone

Source

pub unsafe exec fn _verus_external_fn_specification_2056032__91_T_59__32_N_93__32_as_32_Clone_3262325858__32_clone<T: Clone, const N: usize>( a: &[T; N], ) -> res : [T; N]

ensures

forall |i| 0 <= i < N ==> cloned::<T>(a@[i], res@[i]),

a@ =~= res@ ==> a@ == res@,

Specification for <[T; N] as Clone>::clone

Source

pub unsafe exec fn _verus_external_fn_specification_2066032_Tracked_326032_T_326232_as_32_Clone_3262325858__32_clone<T: Copy>( b: &Tracked<T>, ) -> res : Tracked<T>

ensures

res == b,

Specification for <Tracked<T> as Clone>::clone

Source

pub unsafe exec fn _verus_external_fn_specification_2076032_Ghost_326032_T_326232_as_32_Clone_3262325858__32_clone<T>( b: &Ghost<T>, ) -> res : Ghost<T>

ensures

res == b,

Specification for <Ghost<T> as Clone>::clone

Source §

impl VstdSpecsForRustStdLib

Source

pub unsafe exec fn _verus_external_fn_specification_2086032_bool_32_as_32_PartialEq_326032_bool_32623262325858__32_eq( x: &bool, y: &bool, ) -> bool

Specification for <bool as PartialEq<bool>>::eq

Source

pub unsafe exec fn _verus_external_fn_specification_232_Result_3258583260__32_T_44__32_E_3262325858__32_branch<T, E>( result: Result<T, E>, ) -> cf : ControlFlow<<Result<T, E> as Try>::Residual, <Result<T, E> as Try>::Output>

ensures

cf
    == match result {
        Ok(v) => ControlFlow::Continue(v),
        Err(e) => ControlFlow::Break(Err(e)),
    },

Specification for Result::<T, E>::branch

Source

pub unsafe exec fn _verus_external_fn_specification_233_Option_3258583260__32_T_3262325858__32_branch<T>( option: Option<T>, ) -> cf : ControlFlow<<Option<T> as Try>::Residual, <Option<T> as Try>::Output>

ensures

cf
    == match option {
        Some(v) => ControlFlow::Continue(v),
        None => ControlFlow::Break(None),
    },

Specification for Option::<T>::branch

Source

pub unsafe exec fn _verus_external_fn_specification_234_Option_3258583260__32_T_3262325858__32_from__residual<T>( option: Option<Infallible>, ) -> option2 : Option<T>

ensures

option.is_none(),

option2.is_none(),

Specification for Option::<T>::from_residual

Source

pub unsafe exec fn _verus_external_fn_specification_235_Result_3258583260__32_T_44__32_F_3262325858__32_from__residual<T, E, F: From<E>>( result: Result<Infallible, E>, ) -> result2 : Result<T, F>

ensures

match (result, result2) {
    (Err(e), Err(e2)) => spec_from::<F, E>(e, e2),
    _ => false,
},

Specification for Result::<T, F>::from_residual

Source §

impl VstdSpecsForRustStdLib

Source

pub unsafe exec fn _verus_external_fn_specification_2366032_T_32_as_32_Into_326032_U_32623262325858__32_into<T, U: From<T>>( a: T, ) -> ret : U

ensures

call_ensures(U::from, (a,), ret),

Specification for <T as Into>::into

Source

pub unsafe exec fn _verus_external_fn_specification_2376032_T_32_as_32_TryInto_326032_U_32623262325858__32_try__into<T, U: TryFrom<T>>( a: T, ) -> ret : Result<U, U::Error>

ensures

call_ensures(U::try_from, (a,), ret),

Specification for <T as TryInto>::try_into

Source

pub unsafe exec fn _verus_external_fn_specification_2386032_T_32_as_32_TryFrom_326032_U_32623262325858__32_try__from<T, U: Into<T>>( a: U, ) -> ret : Result<T, <T as TryFrom>::Error>

ensures

ret.is_ok(),

call_ensures(U::into, (a,), ret.unwrap()),

Specification for <T as TryFrom>::try_from

Source §

Source

pub unsafe exec fn _verus_external_fn_specification_2446032_u32_32_as_32_core_325858__32_convert_325858__32_From_326032_u16_32623262325858__32_from( a: u16, ) -> ret : u32

Specification for <u32 as core::convert::From<u16>>::from

Source

pub unsafe exec fn _verus_external_fn_specification_2456032_u64_32_as_32_core_325858__32_convert_325858__32_From_326032_u16_32623262325858__32_from( a: u16, ) -> ret : u64

Specification for <u64 as core::convert::From<u16>>::from

Source

pub unsafe exec fn _verus_external_fn_specification_2466032_usize_32_as_32_core_325858__32_convert_325858__32_From_326032_u16_32623262325858__32_from( a: u16, ) -> ret : usize

Specification for <usize as core::convert::From<u16>>::from

Source

pub unsafe exec fn _verus_external_fn_specification_2476032_u128_32_as_32_core_325858__32_convert_325858__32_From_326032_u16_32623262325858__32_from( a: u16, ) -> ret : u128

Specification for <u128 as core::convert::From<u16>>::from

Source §

impl VstdSpecsForRustStdLib

Source

pub unsafe exec fn _verus_external_fn_specification_2486032_u64_32_as_32_core_325858__32_convert_325858__32_From_326032_u32_32623262325858__32_from( a: u32, ) -> ret : u64

Specification for <u64 as core::convert::From<u32>>::from

Specification for <i32 as core::convert::From<i8>>::from

Source

pub unsafe exec fn _verus_external_fn_specification_2536032_i64_32_as_32_core_325858__32_convert_325858__32_From_326032_i8_32623262325858__32_from( a: i8, ) -> ret : i64

Specification for <i8 as TryFrom<u16>>::try_from

Source §

Specification for <isize as TryFrom<u32>>::try_from

Source §

Specification for <isize as TryFrom<u64>>::try_from

Source §

Specification for <isize as TryFrom<u128>>::try_from

Source §

Source §

pub unsafe exec fn _verus_external_fn_specification_352_core_325858__32_mem_325858__32_swap_3258583260__32_T_32__62_<T>( a: &mut T, b: &mut T, )

ensures

*final(a) == *old(b),

*final(b) == *old(a),

Specification for core::mem::swap::<T>

Source

pub unsafe exec fn _verus_external_fn_specification_353_core_325858__32_intrinsics_325858__32_likely( b: bool, ) -> c : bool

ensures

c == b,

Specification for core::intrinsics::likely

Source

pub unsafe exec fn _verus_external_fn_specification_354_core_325858__32_intrinsics_325858__32_unlikely( b: bool, ) -> c : bool

ensures

c == b,

Specification for core::intrinsics::unlikely

Source

pub unsafe exec fn _verus_external_fn_specification_355_bool_325858__32_then<T, F: FnOnce() -> T>( b: bool, f: F, ) -> ret : Option<T>

ensures

if b { ret.is_some() && f.ensures((), ret.unwrap()) } else { ret.is_none() },

Specification for bool::then

Source §

impl VstdSpecsForRustStdLib

Source

pub unsafe exec fn _verus_external_fn_specification_3566032_bool_32_as_32_core_325858__32_default_325858__32_Default_3262325858__32_default() -> r : bool

ensures

r == false,

Specification for <bool as core::default::Default>::default

Source §

impl VstdSpecsForRustStdLib

Source

pub unsafe exec fn _verus_external_fn_specification_3576032_char_32_as_32_core_325858__32_default_325858__32_Default_3262325858__32_default() -> r : char

ensures

r == '\0',

Specification for <char as core::default::Default>::default

Source §

impl VstdSpecsForRustStdLib

Source

pub unsafe exec fn _verus_external_fn_specification_3586032_f32_32_as_32_core_325858__32_default_325858__32_Default_3262325858__32_default() -> r : f32

ensures

r == 0.0f32,

Specification for <f32 as core::default::Default>::default

Source §

impl VstdSpecsForRustStdLib

Source

pub unsafe exec fn _verus_external_fn_specification_3596032_f64_32_as_32_core_325858__32_default_325858__32_Default_3262325858__32_default() -> r : f64

ensures

r == 0.0f64,

Specification for <f64 as core::default::Default>::default

Source §

impl VstdSpecsForRustStdLib

Source

pub unsafe exec fn _verus_external_fn_specification_3606032_i8_32_as_32_core_325858__32_default_325858__32_Default_3262325858__32_default() -> r : i8

ensures

r == 0i8,

Specification for <i8 as core::default::Default>::default

Source §

impl VstdSpecsForRustStdLib

Source

pub unsafe exec fn _verus_external_fn_specification_3616032_i16_32_as_32_core_325858__32_default_325858__32_Default_3262325858__32_default() -> r : i16

ensures

r == 0i16,

Specification for <i16 as core::default::Default>::default

Source §

impl VstdSpecsForRustStdLib

Source

pub unsafe exec fn _verus_external_fn_specification_3626032_i32_32_as_32_core_325858__32_default_325858__32_Default_3262325858__32_default() -> r : i32

ensures

r == 0i32,

Specification for <i32 as core::default::Default>::default

Source §

impl VstdSpecsForRustStdLib

Source

pub unsafe exec fn _verus_external_fn_specification_3636032_i64_32_as_32_core_325858__32_default_325858__32_Default_3262325858__32_default() -> r : i64

ensures

r == 0i64,

Specification for <i64 as core::default::Default>::default

Source §

impl VstdSpecsForRustStdLib

Source

pub unsafe exec fn _verus_external_fn_specification_3646032_i128_32_as_32_core_325858__32_default_325858__32_Default_3262325858__32_default() -> r : i128

ensures

r == 0i128,

Specification for <i128 as core::default::Default>::default

Source §

impl VstdSpecsForRustStdLib

Source

pub unsafe exec fn _verus_external_fn_specification_3656032_isize_32_as_32_core_325858__32_default_325858__32_Default_3262325858__32_default() -> r : isize

ensures

r == 0isize,

Specification for <isize as core::default::Default>::default

Source §

impl VstdSpecsForRustStdLib

Source

pub unsafe exec fn _verus_external_fn_specification_3666032_u8_32_as_32_core_325858__32_default_325858__32_Default_3262325858__32_default() -> r : u8

ensures

r == 0u8,

Specification for <u8 as core::default::Default>::default

Source §

impl VstdSpecsForRustStdLib

Source

pub unsafe exec fn _verus_external_fn_specification_3676032_u16_32_as_32_core_325858__32_default_325858__32_Default_3262325858__32_default() -> r : u16

ensures

r == 0u16,

Specification for <u16 as core::default::Default>::default

Source §

impl VstdSpecsForRustStdLib

Source

pub unsafe exec fn _verus_external_fn_specification_3686032_u32_32_as_32_core_325858__32_default_325858__32_Default_3262325858__32_default() -> r : u32

ensures

r == 0u32,

Specification for <u32 as core::default::Default>::default

Source §

impl VstdSpecsForRustStdLib

Source

pub unsafe exec fn _verus_external_fn_specification_3696032_u64_32_as_32_core_325858__32_default_325858__32_Default_3262325858__32_default() -> r : u64

ensures

r == 0u64,

Specification for <u64 as core::default::Default>::default

Source §

impl VstdSpecsForRustStdLib

Source

pub unsafe exec fn _verus_external_fn_specification_3706032_u128_32_as_32_core_325858__32_default_325858__32_Default_3262325858__32_default() -> r : u128

ensures

r == 0u128,

Specification for <u128 as core::default::Default>::default

Source §

impl VstdSpecsForRustStdLib

Source

pub unsafe exec fn _verus_external_fn_specification_37160324041__32_as_32_core_325858__32_default_325858__32_Default_3262325858__32_default() -> r : ()

ensures

r == (),

Specification for <() as core::default::Default>::default

Source §

impl VstdSpecsForRustStdLib

Source

pub unsafe exec fn _verus_external_fn_specification_3726032_usize_32_as_32_core_325858__32_default_325858__32_Default_3262325858__32_default() -> r : usize

ensures

r == 0usize,

Specification for <usize as core::default::Default>::default

Source §

impl VstdSpecsForRustStdLib

Source

pub unsafe exec fn _verus_external_fn_specification_3736032_Option_326032_T_326232_as_32_core_325858__32_default_325858__32_Default_3262325858__32_default<T>() -> r : Option<T>

ensures

r == Option::<T>::None,

Specification for <Option<T> as core::default::Default>::default

Source

pub unsafe exec fn _verus_external_fn_specification_37460323832__39_a_32_str_32_as_32_core_325858__32_default_325858__32_Default_3262325858__32_default<'a>() -> r : &'a str

ensures

r == "",

Specification for <&'a str as core::default::Default>::default

Source

pub unsafe exec fn _verus_external_fn_specification_3756032_core_325858__32_marker_325858__32_PhantomData_326032_T_443262__32_as_32_core_325858__32_default_325858__32_Default_3262325858__10_default<T: PointeeSized>() -> r : PhantomData<T>

ensures

r == core::marker::PhantomData::<T>,

Specification for <core::marker::PhantomData<T> as core::default::Default>::default

Source

pub unsafe exec fn _verus_external_fn_specification_3766032__40_U_44__32_T_444132_as_32_core_325858__32_default_325858__32_Default_3262325858__32_default<U: Default, T: Default>() -> r : (U, T)

ensures

call_ensures(U::default, (), r.0),

call_ensures(T::default, (), r.1),

Specification for <(U, T) as core::default::Default>::default

Source

pub unsafe exec fn _verus_external_fn_specification_3776032__40_V_44__32_U_44__32_T_41__32_as_32_core_325858__32_default_325858__32_Default_3262325858__32_default<V: Default, U: Default, T: Default>() -> r : (V, U, T)

ensures

call_ensures(V::default, (), r.0),

call_ensures(U::default, (), r.1),

call_ensures(T::default, (), r.2),

Specification for <(V, U, T) as core::default::Default>::default

Source §

impl VstdSpecsForRustStdLib

Source

pub unsafe exec fn _verus_external_fn_specification_3786032_I_32_as_32_IntoIterator_3262325858__32_into__iter<I: Iterator>( i: I, ) -> r : I

ensures

r == i,

Specification for ::into_iter

Source §

impl VstdSpecsForRustStdLib

Source

pub unsafe exec fn _verus_external_fn_specification_379_ManuallyDrop_3258583260__32_T_3262325858__32_new<T>( value: T, ) -> res : ManuallyDrop<T>

ensures

res@ == value,

Specification for ManuallyDrop::<T>::new

Source

pub unsafe exec fn _verus_external_fn_specification_380_ManuallyDrop_3258583260__32_T_3262325858__32_into__inner<T>( m: ManuallyDrop<T>, ) -> T

returns

m@,

Specification for ManuallyDrop::<T>::into_inner

Source

pub unsafe exec fn _verus_external_fn_specification_3816032_ManuallyDrop_326032_T_326232_as_32_Clone_3262325858__32_clone<T: Clone + ?Sized>( m: &ManuallyDrop<T>, ) -> res : ManuallyDrop<T>

ensures

cloned(m@, res@),

Specification for <ManuallyDrop<T> as Clone>::clone

Source

pub unsafe exec fn _verus_external_fn_specification_3826032_ManuallyDrop_326032_T_326232_as_32_Deref_3262325858__32_deref<T: ?Sized>( m: &ManuallyDrop<T>, ) -> res : &T

returns

m.view_ref(),

Specification for <ManuallyDrop<T> as Deref>::deref

Source §

impl VstdSpecsForRustStdLib

Source

pub unsafe exec fn _verus_external_fn_specification_383_MaybeUninit_3258583260__32_T_3262325858__32_new<T>( val: T, ) -> res : MaybeUninit<T>

ensures

res.mem_contents() == MemContents::Init(val),

Specification for MaybeUninit::<T>::new

Source

pub unsafe exec fn _verus_external_fn_specification_384_MaybeUninit_3258583260__32_T_3262325858__32_uninit<T>() -> res : MaybeUninit<T>

ensures

res.mem_contents() == MemContents::Uninit,

Specification for MaybeUninit::<T>::uninit

Source

pub unsafe exec fn _verus_external_fn_specification_385_MaybeUninit_3258583260__32_T_3262325858__32_assume__init<T>( m: MaybeUninit<T>, ) -> T

requires

m.mem_contents().is_init(),

returns

m.mem_contents().value(),

Specification for MaybeUninit::<T>::assume_init

Source

pub unsafe exec fn _verus_external_fn_specification_386_MaybeUninit_3258583260__32_T_3262325858__32_assumeinitref<T>( m: &MaybeUninit<T>, ) -> ret : &T

requires

m.mem_contents().is_init(),

ensures

ret == m.mem_contents().value(),

Specification for MaybeUninit::<T>::assume_init_ref

Source

pub unsafe exec fn _verus_external_fn_specification_387_MaybeUninit_3258583260__32_T_3262325858__32_assumeinitmut<T>( m: &mut MaybeUninit<T>, ) -> ret : &mut T

requires

m.mem_contents().is_init(),

ensures

*ret == old(m).mem_contents().value(),

final(m).mem_contents().is_init(),

final(m).mem_contents().value() == *final(ret),

Specification for MaybeUninit::<T>::assume_init_mut

Source §

Specification for <i128 as core::ops::Neg>::neg

Source §

Source §

Specification for <i128 as core::ops::AddAssign>::add_assign

Source §

Specification for <i128 as core::ops::Sub>::sub

Source §

Specification for <i128 as core::ops::SubAssign>::sub_assign

Source §

Specification for <i128 as core::ops::Mul>::mul

Source §

Specification for <i128 as core::ops::MulAssign>::mul_assign

Source §

Specification for <u128 as core::ops::Div>::div

Source §

Specification for <u128 as core::ops::DivAssign>::div_assign

Source §

Specification for <i128 as core::ops::Div>::div

Source §

Specification for <i128 as core::ops::DivAssign>::div_assign

Source §

Specification for <u128 as core::ops::Rem>::rem

Source §

Specification for <u128 as core::ops::RemAssign>::rem_assign

Source §

Specification for <i128 as core::ops::Rem>::rem

Source §

Specification for <i128 as core::ops::RemAssign>::rem_assign

Source §

Specification for <i128 as core::ops::BitAnd>::bitand

Source §

Specification for <i128 as core::ops::BitAndAssign>::bitand_assign

Source §

Specification for <i128 as core::ops::BitOr>::bitor

Source §

Specification for <i128 as core::ops::BitOrAssign>::bitor_assign

Source §

Source §

Specification for <i128 as core::ops::Shl>::shl

Source §

Specification for <i128 as core::ops::ShlAssign>::shl_assign

Source §

Specification for <i128 as core::ops::Shr>::shr

Source §

Specification for <i128 as core::ops::ShrAssign>::shr_assign

Source §

impl VstdSpecsForRustStdLib

Source

pub unsafe exec fn _verus_external_fn_specification_6486032_f32_32_as_32_core_325858__32_ops_325858__32_Neg_3262325858__32_neg( x: f32, ) -> o : f32

ensures

neg_ensures::<f32>(x, o),

Specification for <f32 as core::ops::Neg>::neg

Source

pub unsafe exec fn _verus_external_fn_specification_6496032_f32_32_as_32_core_325858__32_ops_325858__32_Add_3262325858__32_add( x: f32, y: f32, ) -> o : f32

ensures

add_ensures::<f32>(x, y, o),

Specification for <f32 as core::ops::Add>::add

Source

pub unsafe exec fn _verus_external_fn_specification_6506032_f32_32_as_32_core_325858__32_ops_325858__32_Sub_3262325858__32_sub( x: f32, y: f32, ) -> o : f32

ensures

sub_ensures::<f32>(x, y, o),

Specification for <f32 as core::ops::Sub>::sub

Source

pub unsafe exec fn _verus_external_fn_specification_6516032_f32_32_as_32_core_325858__32_ops_325858__32_Mul_3262325858__32_mul( x: f32, y: f32, ) -> o : f32

ensures

mul_ensures::<f32>(x, y, o),

Specification for <f32 as core::ops::Mul>::mul

Source

pub unsafe exec fn _verus_external_fn_specification_6526032_f32_32_as_32_core_325858__32_ops_325858__32_Div_3262325858__32_div( x: f32, y: f32, ) -> o : f32

ensures

div_ensures::<f32>(x, y, o),

Specification for <f32 as core::ops::Div>::div

Source

pub unsafe exec fn _verus_external_fn_specification_6536032_f64_32_as_32_core_325858__32_ops_325858__32_Neg_3262325858__32_neg( x: f64, ) -> o : f64

ensures

neg_ensures::<f64>(x, o),

Specification for <f64 as core::ops::Neg>::neg

Source

pub unsafe exec fn _verus_external_fn_specification_6546032_f64_32_as_32_core_325858__32_ops_325858__32_Add_3262325858__32_add( x: f64, y: f64, ) -> o : f64

ensures

add_ensures::<f64>(x, y, o),

Specification for <f64 as core::ops::Add>::add

Source

pub unsafe exec fn _verus_external_fn_specification_6556032_f64_32_as_32_core_325858__32_ops_325858__32_Sub_3262325858__32_sub( x: f64, y: f64, ) -> o : f64

ensures

sub_ensures::<f64>(x, y, o),

Specification for <f64 as core::ops::Sub>::sub

Source

pub unsafe exec fn _verus_external_fn_specification_6566032_f64_32_as_32_core_325858__32_ops_325858__32_Mul_3262325858__32_mul( x: f64, y: f64, ) -> o : f64

ensures

mul_ensures::<f64>(x, y, o),

Specification for <f64 as core::ops::Mul>::mul

Source

pub unsafe exec fn _verus_external_fn_specification_6576032_f64_32_as_32_core_325858__32_ops_325858__32_Div_3262325858__32_div( x: f64, y: f64, ) -> o : f64

ensures

div_ensures::<f64>(x, y, o),

Specification for <f64 as core::ops::Div>::div

Source §

impl VstdSpecsForRustStdLib

Source

pub unsafe exec fn _verus_external_fn_specification_658_BTreeMap_3258583260__32_Key_44__32_Value_44__32_A_3262325858__32_iter<'a, Key, Value, A: Allocator + Clone>( m: &'a BTreeMap<Key, Value, A>, ) -> iter : Iter<'a, Key, Value>

ensures

key_obeys_cmp_spec::<Key>()
    ==> {
        &&& iter == spec_btree_map_iter(m)
        &&& iter.remaining().no_duplicates()
        &&& IteratorSpec::decrease(&iter) is Some
        &&& IteratorSpec::initial_value_relation(&iter, &iter)
        &&& increasing_seq(iter.remaining().map_values(|kv: (&Key, &Value)| *kv.0))

    },

Specification for BTreeMap::<Key, Value, A>::iter

Source

pub unsafe exec fn _verus_external_fn_specification_659_BTreeMap_3258583260__32_Key_44__32_Value_44__32_A_3262325858__32_len<Key, Value, A: Allocator + Clone>( m: &BTreeMap<Key, Value, A>, ) -> len : usize

ensures

len == spec_btree_map_len(m),

Specification for BTreeMap::<Key, Value, A>::len

Source

pub unsafe exec fn _verus_external_fn_specification_660_BTreeMap_3258583260__32_Key_44__32_Value_44__32_A_3262325858__32_is__empty<Key, Value, A: Allocator + Clone>( m: &BTreeMap<Key, Value, A>, ) -> res : bool

ensures

res == m@.is_empty(),

Specification for BTreeMap::<Key, Value, A>::is_empty

Source

pub unsafe exec fn _verus_external_fn_specification_6616032_BTreeMap_3258583260__32_K_44__32_V_44__32_A_443262__32_as_32_Clone_3262325858__32_clone<K: Clone, V: Clone, A: Allocator + Clone>( this: &BTreeMap<K, V, A>, ) -> other : BTreeMap<K, V, A>

ensures

other@ == this@,

Specification for <BTreeMap<K, V, A> as Clone>::clone

Source

pub unsafe exec fn _verus_external_fn_specification_662_BTreeMap_3258583260__32_Key_44__32_Value_3262325858__32_new<Key, Value>() -> m : BTreeMap<Key, Value>

ensures

m@ == Map::<Key, Value>::empty(),

Specification for BTreeMap::<Key, Value>::new

Source

pub unsafe exec fn _verus_external_fn_specification_6636032_BTreeMap_326032_K_44__32_V_326232_as_32_core_325858__32_default_325858__32_Default_3262325858__32_default<K, V>() -> m : BTreeMap<K, V>

ensures

m@ == Map::<K, V>::empty(),

Specification for <BTreeMap<K, V> as core::default::Default>::default

Source

pub unsafe exec fn _verus_external_fn_specification_664_BTreeMap_3258583260__32_Key_44__32_Value_44__32_A_44326232585832_insert<Key: Ord, Value, A: Allocator + Clone>( m: &mut BTreeMap<Key, Value, A>, k: Key, v: Value, ) -> result : Option<Value>

ensures

obeys_cmp::<Key>()
    ==> {
        &&& final(m)@ == old(m)@.insert(k, v)
        &&& match result {
            Some(v) => old(m)@.contains_key(k) && v == old(m)[k],
            None => !old(m)@.contains_key(k),
        }

    },

Specification for BTreeMap::<Key, Value, A>::insert

Source

pub unsafe exec fn _verus_external_fn_specification_665_BTreeMap_3258583260__32_Key_44__32_Value_44__32_A_3262325858__32_contains__key_3258583260__32_Q_32__62_<Key: Borrow<Q> + Ord, Value, A: Allocator + Clone, Q: Ord + ?Sized>( m: &BTreeMap<Key, Value, A>, k: &Q, ) -> result : bool

ensures

obeys_cmp::<Key>() ==> result == contains_borrowed_key(m@, k),

Specification for BTreeMap::<Key, Value, A>::contains_key::<Q>

Source

pub unsafe exec fn _verus_external_fn_specification_666_BTreeMap_3258583260__32_Key_44__32_Value_44__32_A_3262325858__32_get_3258583260__32_Q_32__62_<'a, Key: Borrow<Q> + Ord, Value, A: Allocator + Clone, Q: Ord + ?Sized>( m: &'a BTreeMap<Key, Value, A>, k: &Q, ) -> result : Option<&'a Value>

ensures

obeys_cmp::<Key>()
    ==> match result {
        Some(v) => maps_borrowed_key_to_value(m@, k, *v),
        None => !contains_borrowed_key(m@, k),
    },

Specification for BTreeMap::<Key, Value, A>::get::<Q>

Source

pub unsafe exec fn _verus_external_fn_specification_667_BTreeMap_3258583260__32_Key_44__32_Value_44__32_A_3262325858__32_remove_3258583260__32_Q_32__62_<Key: Borrow<Q> + Ord, Value, A: Allocator + Clone, Q: Ord + ?Sized>( m: &mut BTreeMap<Key, Value, A>, k: &Q, ) -> result : Option<Value>

ensures

obeys_cmp::<Key>()
    ==> {
        &&& borrowed_key_removed(old(m)@, final(m)@, k)
        &&& match result {
            Some(v) => maps_borrowed_key_to_value(old(m)@, k, v),
            None => !contains_borrowed_key(old(m)@, k),
        }

    },

Specification for BTreeMap::<Key, Value, A>::remove::<Q>

Source

pub unsafe exec fn _verus_external_fn_specification_668_BTreeMap_3258583260__32_Key_44__32_Value_44__32_A_3262325858__32_clear<Key, Value, A: Allocator + Clone>( m: &mut BTreeMap<Key, Value, A>, )

ensures

final(m)@ == Map::<Key, Value>::empty(),

Specification for BTreeMap::<Key, Value, A>::clear

Source

pub unsafe exec fn _verus_external_fn_specification_669_BTreeMap_3258583260__32_Key_44__32_Value_44__32_A_3262325858__32_keys<'a, Key, Value, A: Allocator + Clone>( m: &'a BTreeMap<Key, Value, A>, ) -> keys : Keys<'a, Key, Value>

ensures

key_obeys_cmp_spec::<Key>()
    ==> {
        &&& keys == spec_keys_iter(m)
        &&& IteratorSpec::decrease(&keys) is Some
        &&& IteratorSpec::initial_value_relation(&keys, &keys)

    },

Specification for BTreeMap::<Key, Value, A>::keys

Source

pub unsafe exec fn _verus_external_fn_specification_670_BTreeMap_3258583260__32_Key_44__32_Value_44__32_A_3262325858__32_values<'a, Key, Value, A: Allocator + Clone>( m: &'a BTreeMap<Key, Value, A>, ) -> values : Values<'a, Key, Value>

ensures

key_obeys_cmp_spec::<Key>()
    ==> {
        &&& values == spec_values_iter(m)
        &&& IteratorSpec::decrease(&values) is Some
        &&& IteratorSpec::initial_value_relation(&values, &values)
        &&& exists |key_seq: Seq<Key>| {
            &&& increasing_seq(key_seq)
            &&& key_seq.to_set() == m@.dom()
            &&& key_seq.no_duplicates()
            &&& IteratorSpec::remaining(&values) == key_seq.map(|i: int, k| &m@[k])

        }

    },

Specification for BTreeMap::<Key, Value, A>::values

Source

pub unsafe exec fn _verus_external_fn_specification_671_BTreeSet_3258583260__32_Key_44__32_A_3262325858__32_len<Key, A: Allocator + Clone>( m: &BTreeSet<Key, A>, ) -> len : usize

ensures

len == spec_btree_set_len(m),

Specification for BTreeSet::<Key, A>::len

Source

pub unsafe exec fn _verus_external_fn_specification_672_BTreeSet_3258583260__32_Key_44__32_A_3262325858__32_is__empty<Key, A: Allocator + Clone>( m: &BTreeSet<Key, A>, ) -> res : bool

ensures

res == m@.is_empty(),

Specification for BTreeSet::<Key, A>::is_empty

Source

pub unsafe exec fn _verus_external_fn_specification_6736032_BTreeSet_3258583260__32_K_44__32_A_326232_as_32_Clone_3262325858__32_clone<K: Clone, A: Allocator + Clone>( this: &BTreeSet<K, A>, ) -> other : BTreeSet<K, A>

ensures

other@ == this@,

Specification for <BTreeSet<K, A> as Clone>::clone

Source

pub unsafe exec fn _verus_external_fn_specification_674_BTreeSet_3258583260__32_Key_3262325858__32_new<Key>() -> m : BTreeSet<Key>

ensures

m@ == Set::<Key>::empty(),

Specification for BTreeSet::<Key>::new

Source

pub unsafe exec fn _verus_external_fn_specification_6756032_BTreeSet_326032_T_326232_as_32_core_325858__32_default_325858__32_Default_3262325858__32_default<T>() -> m : BTreeSet<T>

ensures

m@ == Set::<T>::empty(),

Specification for <BTreeSet<T> as core::default::Default>::default

Source

pub unsafe exec fn _verus_external_fn_specification_676_BTreeSet_3258583260__32_Key_44__32_A_3262325858__32_insert<Key: Ord, A: Allocator + Clone>( m: &mut BTreeSet<Key, A>, k: Key, ) -> result : bool

ensures

obeys_cmp::<Key>()
    ==> {
        &&& final(m)@ == old(m)@.insert(k)
        &&& result == !old(m)@.contains(k)

    },

Specification for BTreeSet::<Key, A>::insert

Source

pub unsafe exec fn _verus_external_fn_specification_677_BTreeSet_3258583260__32_Key_44__32_A_44326232585832_contains<Key: Borrow<Q> + Ord, A: Allocator + Clone, Q: Ord + ?Sized>( m: &BTreeSet<Key, A>, k: &Q, ) -> result : bool

ensures

obeys_cmp::<Key>() ==> result == set_contains_borrowed_key(m@, k),

Specification for BTreeSet::<Key, A>::contains

Source

pub unsafe exec fn _verus_external_fn_specification_678_BTreeSet_3258583260__32_Key_44__32_A_3262325858__32_get_3258583260__32_Q_32__62_<'a, Key: Borrow<Q> + Ord, A: Allocator + Clone, Q: Ord + ?Sized>( m: &'a BTreeSet<Key, A>, k: &Q, ) -> result : Option<&'a Key>

ensures

obeys_cmp::<Key>()
    ==> match result {
        Some(v) => sets_borrowed_key_to_key(m@, k, v),
        None => !set_contains_borrowed_key(m@, k),
    },

Specification for BTreeSet::<Key, A>::get::<Q>

Source

pub unsafe exec fn _verus_external_fn_specification_679_BTreeSet_3258583260__32_Key_44__32_A_44326232585832_remove_3258583260__32_Q_32__62_<Key: Borrow<Q> + Ord, A: Allocator + Clone, Q: Ord + ?Sized>( m: &mut BTreeSet<Key, A>, k: &Q, ) -> result : bool

ensures

obeys_cmp::<Key>()
    ==> {
        &&& sets_differ_by_borrowed_key(old(m)@, final(m)@, k)
        &&& result == set_contains_borrowed_key(old(m)@, k)

    },

Specification for BTreeSet::<Key, A>::remove::<Q>

Source

pub unsafe exec fn _verus_external_fn_specification_680_BTreeSet_3258583260__32_Key_44__32_A_3262325858__32_clear<Key, A>( m: &mut BTreeSet<Key, A>, )
where A: Clone + Allocator,

ensures

final(m)@ == Set::<Key>::empty(),

Specification for BTreeSet::<Key, A>::clear

Source

pub unsafe exec fn _verus_external_fn_specification_681_BTreeSet_3258583260__32_Key_44__32_A_3262325858__32_iter<'a, Key, A: Allocator + Clone>( m: &'a BTreeSet<Key, A>, ) -> r : Iter<'a, Key>

ensures

key_obeys_cmp_spec::<Key>()
    ==> {
        &&& r == spec_btree_keys_iter(m)
        &&& IteratorSpec::decrease(&r) is Some
        &&& IteratorSpec::initial_value_relation(&r, &r)

    },

Specification for BTreeSet::<Key, A>::iter

Source §

impl VstdSpecsForRustStdLib

Source

pub unsafe exec fn _verus_external_fn_specification_725_OccupiedEntry_325858__32_key<'a, 'b, K, V, A: Allocator>( entry: &'b OccupiedEntry<'a, K, V, A>, ) -> key : &'b K

returns

&entry.spec_key(),

Specification for OccupiedEntry::key

Source §

impl VstdSpecsForRustStdLib

Source

pub unsafe exec fn _verus_external_fn_specification_726_VacantEntry_325858__32_key<'a, 'b, K: 'a, V: 'a, A: Allocator>( entry: &'b VacantEntry<'a, K, V, A>, ) -> key : &'b K

returns

&entry.spec_key(),

Specification for VacantEntry::key

Source §

impl VstdSpecsForRustStdLib

Source

pub unsafe exec fn _verus_external_fn_specification_682_DefaultHasher_325858__32_new() -> result : DefaultHasher

ensures

result@ == Seq::<Seq<u8>>::empty(),

Specification for DefaultHasher::new

Source

pub unsafe exec fn _verus_external_fn_specification_683_DefaultHasher_325858__32_write( state: &mut DefaultHasher, bytes: &[u8], )

ensures

final(state)@ == old(state)@.push(bytes@),

Specification for DefaultHasher::write

Source

pub unsafe exec fn _verus_external_fn_specification_684_DefaultHasher_325858__32_finish( state: &DefaultHasher, ) -> result : u64

ensures

result == DefaultHasher::spec_finish(state@),

Specification for DefaultHasher::finish

Source

pub unsafe exec fn _verus_external_fn_specification_685_HashMap_3258583260__32_Key_44__32_Value_44__32_S_44__32_A_3262325858__32_iter<'a, Key, Value, S, A: Allocator>( m: &'a HashMap<Key, Value, S, A>, ) -> iter : Iter<'a, Key, Value>

ensures

obeys_key_model::<Key>() && builds_valid_hashers::<S>()
    ==> {
        &&& iter == spec_hash_map_iter(m)
        &&& iter.remaining().no_duplicates()
        &&& IteratorSpec::decrease(&iter) is Some
        &&& IteratorSpec::initial_value_relation(&iter, &iter)

    },

Specification for HashMap::<Key, Value, S, A>::iter

Source

pub unsafe exec fn _verus_external_fn_specification_686_HashMap_3258583260__32_Key_44__32_Value_44__32_S_44__32_A_3262325858__32_len<Key, Value, S, A: Allocator>( m: &HashMap<Key, Value, S, A>, ) -> len : usize

ensures

len == spec_hash_map_len(m),

Specification for HashMap::<Key, Value, S, A>::len

Source

pub unsafe exec fn _verus_external_fn_specification_687_HashMap_3258583260__32_Key_44__32_Value_44__32_S_44__32_A_3262325858__32_is__empty<Key, Value, S, A: Allocator>( m: &HashMap<Key, Value, S, A>, ) -> res : bool

ensures

res == m@.is_empty(),

Specification for HashMap::<Key, Value, S, A>::is_empty

Source

pub unsafe exec fn _verus_external_fn_specification_6886032_HashMap_3258583260__32_K_44__32_V_44__32_S_44__32_A_443262__32_as_32_Clone_3262325858__32_clone<K: Clone, V: Clone, S: Clone, A: Allocator + Clone>( this: &HashMap<K, V, S, A>, ) -> other : HashMap<K, V, S, A>

ensures

other@.dom() == this@.dom(),

forall |key| other@.dom().contains(key) ==> cloned(this@[key], #[trigger] other@[key]),

Specification for <HashMap<K, V, S, A> as Clone>::clone

Source

pub unsafe exec fn _verus_external_fn_specification_689_HashMap_3258583260__32_Key_44__32_Value_3262325858__32_new<Key, Value>() -> m : HashMap<Key, Value, RandomState>

ensures

m@ == Map::<Key, Value>::empty(),

Specification for HashMap::<Key, Value>::new

Source

pub unsafe exec fn _verus_external_fn_specification_6906032_HashMap_326032_K_44__32_V_44__32_S_443262__32_as_32_core_325858__32_default_325858__32_Default_3262325858__32_default<K, V, S: Default>() -> m : HashMap<K, V, S>

ensures

m@ == Map::<K, V>::empty(),

Specification for <HashMap<K, V, S> as core::default::Default>::default

Source

pub unsafe exec fn _verus_external_fn_specification_691_HashMap_3258583260__32_Key_44__32_Value_3262325858__32_with__capacity<Key, Value>( capacity: usize, ) -> m : HashMap<Key, Value, RandomState>

ensures

m@ == Map::<Key, Value>::empty(),

Specification for HashMap::<Key, Value>::with_capacity

Source

pub unsafe exec fn _verus_external_fn_specification_692_HashMap_3258583260__32_Key_44__32_Value_44__32_S_44__32_A_44326232585832_reserve<Key: Eq + Hash, Value, S: BuildHasher, A: Allocator>( m: &mut HashMap<Key, Value, S, A>, additional: usize, )

ensures

final(m)@ == old(m)@,

Specification for HashMap::<Key, Value, S, A>::reserve

Source

pub unsafe exec fn _verus_external_fn_specification_693_HashMap_3258583260__32_Key_44__32_Value_44__32_S_44__32_A_44326232585832_insert<Key: Eq + Hash, Value, S: BuildHasher, A: Allocator>( m: &mut HashMap<Key, Value, S, A>, k: Key, v: Value, ) -> result : Option<Value>

ensures

obeys_key_model::<Key>() && builds_valid_hashers::<S>()
    ==> {
        &&& final(m)@ == old(m)@.insert(k, v)
        &&& match result {
            Some(v) => old(m)@.contains_key(k) && v == old(m)[k],
            None => !old(m)@.contains_key(k),
        }

    },

Specification for HashMap::<Key, Value, S, A>::insert

Source

pub unsafe exec fn _verus_external_fn_specification_694_HashMap_3258583260__32_Key_44__32_Value_44__32_S_44__32_A_3262325858__32_contains__key_3258583260__32_Q_32__62_<Key: Borrow<Q> + Hash + Eq, Value, S: BuildHasher, A: Allocator, Q: Hash + Eq + ?Sized>( m: &HashMap<Key, Value, S, A>, k: &Q, ) -> result : bool

ensures

obeys_key_model::<Key>() && builds_valid_hashers::<S>()
    ==> result == contains_borrowed_key(m@, k),

Specification for HashMap::<Key, Value, S, A>::contains_key::<Q>

Source

pub unsafe exec fn _verus_external_fn_specification_695_HashMap_3258583260__32_Key_44__32_Value_44__32_S_44__32_A_3262325858__32_get_3258583260__32_Q_32__62_<'a, Key: Borrow<Q> + Hash + Eq, Value, S: BuildHasher, A: Allocator, Q: Hash + Eq + ?Sized>( m: &'a HashMap<Key, Value, S, A>, k: &Q, ) -> result : Option<&'a Value>

ensures

obeys_key_model::<Key>() && builds_valid_hashers::<S>()
    ==> match result {
        Some(v) => maps_borrowed_key_to_value(m@, k, *v),
        None => !contains_borrowed_key(m@, k),
    },

Specification for HashMap::<Key, Value, S, A>::get::<Q>

Source

pub unsafe exec fn _verus_external_fn_specification_696_HashMap_3258583260__32_Key_44__32_Value_44__32_S_44__32_A_3262325858__32_remove_3258583260__32_Q_32__62_<Key: Borrow<Q> + Hash + Eq, Value, S: BuildHasher, A: Allocator, Q: Hash + Eq + ?Sized>( m: &mut HashMap<Key, Value, S, A>, k: &Q, ) -> result : Option<Value>

ensures

obeys_key_model::<Key>() && builds_valid_hashers::<S>()
    ==> {
        &&& borrowed_key_removed(old(m)@, final(m)@, k)
        &&& match result {
            Some(v) => maps_borrowed_key_to_value(old(m)@, k, v),
            None => !contains_borrowed_key(old(m)@, k),
        }

    },

Specification for HashMap::<Key, Value, S, A>::remove::<Q>

Source

pub unsafe exec fn _verus_external_fn_specification_697_HashMap_3258583260__32_Key_44__32_Value_44__32_S_44__32_A_3262325858__32_clear<Key, Value, S, A: Allocator>( m: &mut HashMap<Key, Value, S, A>, )

ensures

final(m)@ == Map::<Key, Value>::empty(),

Specification for HashMap::<Key, Value, S, A>::clear

Source

pub unsafe exec fn _verus_external_fn_specification_698_HashMap_3258583260__32_Key_44__32_Value_44__32_S_44__32_A_3262325858__32_keys<'a, Key, Value, S, A: Allocator>( m: &'a HashMap<Key, Value, S, A>, ) -> keys : Keys<'a, Key, Value>

ensures

obeys_key_model::<Key>() && builds_valid_hashers::<S>()
    ==> {
        &&& keys == spec_keys_iter(m)
        &&& IteratorSpec::decrease(&keys) is Some
        &&& IteratorSpec::initial_value_relation(&keys, &keys)

    },

Specification for HashMap::<Key, Value, S, A>::keys

Source

pub unsafe exec fn _verus_external_fn_specification_699_HashMap_3258583260__32_Key_44__32_Value_44__32_S_44__32_A_3262325858__32_values<'a, Key, Value, S, A: Allocator>( m: &'a HashMap<Key, Value, S, A>, ) -> values : Values<'a, Key, Value>

ensures

obeys_key_model::<Key>() && builds_valid_hashers::<S>()
    ==> {
        &&& values == spec_values_iter(m)
        &&& IteratorSpec::decrease(&values) is Some
        &&& IteratorSpec::initial_value_relation(&values, &values)

    },

Specification for HashMap::<Key, Value, S, A>::values

Source

pub unsafe exec fn _verus_external_fn_specification_700_HashSet_3258583260__32_Key_44__32_S_44__32_A_3262325858__32_len<Key, S, A: Allocator>( m: &HashSet<Key, S, A>, ) -> len : usize

ensures

len == spec_hash_set_len(m),

Specification for HashSet::<Key, S, A>::len

Source

pub unsafe exec fn _verus_external_fn_specification_701_HashSet_3258583260__32_Key_44__32_S_44__32_A_3262325858__32_is__empty<Key, S, A: Allocator>( m: &HashSet<Key, S, A>, ) -> res : bool

ensures

res == m@.is_empty(),

Specification for HashSet::<Key, S, A>::is_empty

Source

pub unsafe exec fn _verus_external_fn_specification_702_HashSet_3258583260__32_Key_3262325858__32_new<Key>() -> m : HashSet<Key, RandomState>

ensures

m@ == Set::<Key>::empty(),

Specification for HashSet::<Key>::new

Source

pub unsafe exec fn _verus_external_fn_specification_7036032_HashSet_326032_T_44__32_S_443262__32_as_32_core_325858__32_default_325858__32_Default_3262325858__32_default<T, S: Default>() -> m : HashSet<T, S>

ensures

m@ == Set::<T>::empty(),

Specification for <HashSet<T, S> as core::default::Default>::default

Source

pub unsafe exec fn _verus_external_fn_specification_704_HashSet_3258583260__32_Key_3262325858__32_with__capacity<Key>( capacity: usize, ) -> m : HashSet<Key, RandomState>

ensures

m@ == Set::<Key>::empty(),

Specification for HashSet::<Key>::with_capacity

Source

pub unsafe exec fn _verus_external_fn_specification_705_HashSet_3258583260__32_Key_44__32_S_44__32_A_44326232585832_reserve<Key: Eq + Hash, S: BuildHasher, A: Allocator>( m: &mut HashSet<Key, S, A>, additional: usize, )

ensures

final(m)@ == old(m)@,

Specification for HashSet::<Key, S, A>::reserve

Source

pub unsafe exec fn _verus_external_fn_specification_706_HashSet_3258583260__32_Key_44__32_S_44__32_A_44326232585832_insert<Key: Eq + Hash, S: BuildHasher, A: Allocator>( m: &mut HashSet<Key, S, A>, k: Key, ) -> result : bool

ensures

obeys_key_model::<Key>() && builds_valid_hashers::<S>()
    ==> {
        &&& final(m)@ == old(m)@.insert(k)
        &&& result == !old(m)@.contains(k)

    },

Specification for HashSet::<Key, S, A>::insert

Source

pub unsafe exec fn _verus_external_fn_specification_707_HashSet_3258583260__32_Key_44__32_S_44__32_A_3262325858__32_contains<Key: Borrow<Q> + Hash + Eq, S: BuildHasher, A: Allocator, Q: Hash + Eq + ?Sized>( m: &HashSet<Key, S, A>, k: &Q, ) -> result : bool

ensures

obeys_key_model::<Key>() && builds_valid_hashers::<S>()
    ==> result == set_contains_borrowed_key(m@, k),

Specification for HashSet::<Key, S, A>::contains

Source

pub unsafe exec fn _verus_external_fn_specification_708_HashSet_3258583260__32_Key_44__32_S_44__32_A_3262325858__32_get_3258583260__32_Q_32__62_<'a, Key: Borrow<Q> + Hash + Eq, S: BuildHasher, A: Allocator, Q: Hash + Eq + ?Sized>( m: &'a HashSet<Key, S, A>, k: &Q, ) -> result : Option<&'a Key>

ensures

obeys_key_model::<Key>() && builds_valid_hashers::<S>()
    ==> match result {
        Some(v) => sets_borrowed_key_to_key(m@, k, v),
        None => !set_contains_borrowed_key(m@, k),
    },

Specification for HashSet::<Key, S, A>::get::<Q>

Source

pub unsafe exec fn _verus_external_fn_specification_709_HashSet_3258583260__32_Key_44__32_S_44__32_A_3262325858__32_remove_3258583260__32_Q_32__62_<Key: Borrow<Q> + Hash + Eq, S: BuildHasher, A: Allocator, Q: Hash + Eq + ?Sized>( m: &mut HashSet<Key, S, A>, k: &Q, ) -> result : bool

ensures

obeys_key_model::<Key>() && builds_valid_hashers::<S>()
    ==> {
        &&& sets_differ_by_borrowed_key(old(m)@, final(m)@, k)
        &&& result == set_contains_borrowed_key(old(m)@, k)

    },

Specification for HashSet::<Key, S, A>::remove::<Q>

Source

pub unsafe exec fn _verus_external_fn_specification_710_HashSet_3258583260__32_Key_44__32_S_44__32_A_3262325858__32_clear<Key, S, A: Allocator>( m: &mut HashSet<Key, S, A>, )

ensures

final(m)@ == Set::<Key>::empty(),

Specification for HashSet::<Key, S, A>::clear

Source

pub unsafe exec fn _verus_external_fn_specification_711_HashSet_3258583260__32_Key_44__32_S_44__32_A_3262325858__32_iter<'a, Key, S, A: Allocator>( m: &'a HashSet<Key, S, A>, ) -> hash_keys : Iter<'a, Key>

ensures

obeys_key_model::<Key>() && builds_valid_hashers::<S>()
    ==> {
        &&& hash_keys == spec_hash_keys_iter(m)
        &&& IteratorSpec::decrease(&hash_keys) is Some
        &&& IteratorSpec::initial_value_relation(&hash_keys, &hash_keys)

    },

Specification for HashSet::<Key, S, A>::iter

Source

pub unsafe exec fn _verus_external_fn_specification_712_HashMap_3258583260__32_Key_44__32_Value_44__32_S_44__32_A_44326232585832_entry<'a, Key: Hash + Eq, Value, S: BuildHasher, A: Allocator>( m: &'a mut HashMap<Key, Value, S, A>, key: Key, ) -> entry : Entry<'a, Key, Value, A>

ensures

obeys_key_model::<Key>() && builds_valid_hashers::<S>()
    ==> (entry.key() == key && entry.value() == old(m)@.get(key)
        && final(m)@
            == (match entry.final_value() {
                Some(value) => old(m)@.insert(key, value),
                None => old(m)@.remove(key),
            })),

Specification for HashMap::<Key, Value, S, A>::entry

Source

pub unsafe exec fn _verus_external_fn_specification_713_Entry_325858__32_key<'a, 'b, K, V, A: Allocator>( entry: &'b Entry<'a, K, V, A>, ) -> key : &'b K

returns

&entry.spec_key(),

Specification for Entry::key

Source

pub unsafe exec fn _verus_external_fn_specification_714_Entry_325858__32_or__insert<'a, K, V, A: Allocator>( entry: Entry<'a, K, V, A>, default: V, ) -> value : &'a mut V

ensures

*value
    == (match entry.value() {
        Some(v) => v,
        None => default,
    }),

entry.final_value() == Some(*final(value)),

Specification for Entry::or_insert

Source

pub unsafe exec fn _verus_external_fn_specification_715_Entry_325858__32_insert__entry<'a, K, V, A: Allocator>( entry: Entry<'a, K, V, A>, value: V, ) -> occ_entry : OccupiedEntry<'a, K, V, A>

ensures

occ_entry.key() == entry.key(),

occ_entry.value() == value,

entry.final_value() == occ_entry.final_value(),

Specification for Entry::insert_entry

Source

pub unsafe exec fn _verus_external_fn_specification_716_OccupiedEntry_325858__32_remove__entry<'a, K, V, A: Allocator>( entry: OccupiedEntry<'a, K, V, A>, ) -> kv : (K, V)

ensures

entry.final_value() == None,

returns

(*entry.key(), entry.value()),

Specification for OccupiedEntry::remove_entry

Source

pub unsafe exec fn _verus_external_fn_specification_717_OccupiedEntry_325858__32_get<'a, 'b, K, V, A: Allocator>( entry: &'b OccupiedEntry<'a, K, V, A>, ) -> value : &'b V

ensures

*value == entry.value(),

Specification for OccupiedEntry::get

Source

pub unsafe exec fn _verus_external_fn_specification_718_OccupiedEntry_325858__32_get__mut<'a, 'b, K, V, A: Allocator>( entry: &'b mut OccupiedEntry<'a, K, V, A>, ) -> value : &'b mut V

ensures

*value == old(entry).value(),

final(entry).key() == old(entry).key(),

final(entry).value() == *final(value),

final(entry).final_value() == old(entry).final_value(),

Specification for OccupiedEntry::get_mut

Source

pub unsafe exec fn _verus_external_fn_specification_719_OccupiedEntry_325858__32_into__mut<'a, K, V, A: Allocator>( entry: OccupiedEntry<'a, K, V, A>, ) -> value : &mut V

ensures

*value == entry.value(),

entry.final_value() == Some(*final(value)),

Specification for OccupiedEntry::into_mut

Source

pub unsafe exec fn _verus_external_fn_specification_720_OccupiedEntry_325858__32_insert<'a, K, V, A: Allocator>( entry: &mut OccupiedEntry<'a, K, V, A>, value: V, ) -> old_value : V

ensures

old_value == old(entry).value(),

final(entry).key() == old(entry).key(),

final(entry).value() == value,

final(entry).final_value() == old(entry).final_value(),

Specification for OccupiedEntry::insert

Source

pub unsafe exec fn _verus_external_fn_specification_721_OccupiedEntry_325858__32_remove<'a, K, V, A: Allocator>( entry: OccupiedEntry<'a, K, V, A>, ) -> value : V

ensures

value == entry.value(),

entry.final_value() == None,

Specification for OccupiedEntry::remove

Source

pub unsafe exec fn _verus_external_fn_specification_722_VacantEntry_325858__32_into__key<'a, K: 'a, V: 'a, A: Allocator>( entry: VacantEntry<'a, K, V, A>, ) -> key : K

ensures

key == entry.key(),

entry.final_value() == None,

Specification for VacantEntry::into_key

Source

pub unsafe exec fn _verus_external_fn_specification_723_VacantEntry_325858__32_insert<'a, K: 'a, V: 'a, A: Allocator>( entry: VacantEntry<'a, K, V, A>, value: V, ) -> value_ref : &mut V

ensures

*value_ref == value,

entry.final_value() == Some(*final(value_ref)),

Specification for VacantEntry::insert

Source

pub unsafe exec fn _verus_external_fn_specification_724_VacantEntry_325858__32_insert__entry<'a, K: 'a, V: 'a, A: Allocator>( entry: VacantEntry<'a, K, V, A>, value: V, ) -> occ_entry : OccupiedEntry<'a, K, V, A>

ensures

occ_entry.key() == entry.key(),

occ_entry.value() == value,

entry.final_value() == occ_entry.final_value(),

Specification for VacantEntry::insert_entry

Source §

impl VstdSpecsForRustStdLib

Source

pub unsafe exec fn _verus_external_fn_specification_7276032_u8_32_as_32_Clone_3262325858__32_clone( x: &u8, ) -> res : u8

ensures

res == x,

Source

pub unsafe exec fn _verus_external_fn_specification_7536032_i8_32_as_32_Clone_3262325858__32_clone( x: &i8, ) -> res : i8

ensures

res == x,

Source

pub unsafe exec fn _verus_external_fn_specification_7776032_u16_32_as_32_Clone_3262325858__32_clone( x: &u16, ) -> res : u16

ensures

res == x,

Source

pub unsafe exec fn _verus_external_fn_specification_8036032_i16_32_as_32_Clone_3262325858__32_clone( x: &i16, ) -> res : i16

ensures

res == x,

Source

pub unsafe exec fn _verus_external_fn_specification_8276032_u32_32_as_32_Clone_3262325858__32_clone( x: &u32, ) -> res : u32

ensures

res == x,

Source

pub unsafe exec fn _verus_external_fn_specification_8536032_i32_32_as_32_Clone_3262325858__32_clone( x: &i32, ) -> res : i32

ensures

res == x,

Source

pub unsafe exec fn _verus_external_fn_specification_8776032_u64_32_as_32_Clone_3262325858__32_clone( x: &u64, ) -> res : u64

ensures

res == x,

Source

pub unsafe exec fn _verus_external_fn_specification_9036032_i64_32_as_32_Clone_3262325858__32_clone( x: &i64, ) -> res : i64

ensures

res == x,

Source

pub unsafe exec fn _verus_external_fn_specification_9276032_u128_32_as_32_Clone_3262325858__32_clone( x: &u128, ) -> res : u128

ensures

res == x,

Source

pub unsafe exec fn _verus_external_fn_specification_9536032_i128_32_as_32_Clone_3262325858__32_clone( x: &i128, ) -> res : i128

ensures

res == x,

Source

pub unsafe exec fn _verus_external_fn_specification_9776032_usize_32_as_32_Clone_3262325858__32_clone( x: &usize, ) -> res : usize

ensures

res == x,

Source

pub unsafe exec fn _verus_external_fn_specification_10036032_isize_32_as_32_Clone_3262325858__32_clone( x: &isize, ) -> res : isize

ensures

res == x,

Source

pub unsafe exec fn _verus_external_fn_specification_1027_Option_3258583260__32_T_3262325858__32_is__some<T>( option: &Option<T>, ) -> b : bool

ensures

b == is_some(option),

Specification for Option::<T>::is_some

Source

pub unsafe exec fn _verus_external_fn_specification_1028_Option_3258583260__32_T_3262325858__32_is__none<T>( option: &Option<T>, ) -> b : bool

ensures

b == is_none(option),

Specification for Option::<T>::is_none

Source

pub unsafe exec fn _verus_external_fn_specification_1029_Option_3258583260__32_T_3262325858__32_as__ref<T>( option: &Option<T>, ) -> a : Option<&T>

ensures

a is Some <==> option is Some,

a is Some ==> option->0 == a->0,

Specification for Option::<T>::as_ref

Source

pub unsafe exec fn _verus_external_fn_specification_1030_Option_3258583260__32_T_3262325858__32_unwrap<T>( option: Option<T>, ) -> t : T

requires

option is Some,

ensures

t == spec_unwrap(option),

Specification for Option::<T>::unwrap

Source

pub unsafe exec fn _verus_external_fn_specification_1031_Option_3258583260__32_T_3262325858__32_unwrap__or<T>( option: Option<T>, default: T, ) -> t : T

ensures

t == spec_unwrap_or(option, default),

Specification for Option::<T>::unwrap_or

Source

pub unsafe exec fn _verus_external_fn_specification_1032_Option_3258583260__32_T_3262325858__32_expect<T>( option: Option<T>, msg: &str, ) -> t : T

requires

option is Some,

ensures

t == spec_expect(option, msg),

Specification for Option::<T>::expect

Source

pub unsafe exec fn _verus_external_fn_specification_1033_Option_3258583260__32_T_3262325858__32_take<T>( option: &mut Option<T>, ) -> t : Option<T>

ensures

t == *old(option),

*final(option) is None,

Specification for Option::<T>::take

Source

pub unsafe exec fn _verus_external_fn_specification_1034_Option_3258583260__32_T_3262325858__32_map<T, U, F: FnOnce(T) -> U>( a: Option<T>, f: F, ) -> ret : Option

requires

a.is_some() ==> f.requires((a.unwrap(),)),

ensures

ret.is_some() == a.is_some(),

ret.is_some() ==> f.ensures((a.unwrap(),), ret.unwrap()),

Specification for Option::<T>::map

Source

pub unsafe exec fn _verus_external_fn_specification_1035_Option_325858326032383239_a_32_T_3262325858__32_cloned<'a, T: Clone>( opt: Option<&'a T>, ) -> res : Option<T>

ensures

opt.is_none() ==> res.is_none(),

opt.is_some() ==> res.is_some() && cloned::<T>(*opt.unwrap(), res.unwrap()),

Specification for Option::<&'a T>::cloned

Source

pub unsafe exec fn _verus_external_fn_specification_1036_Option_3258583260__32_T_3262325858__32_and__then<T, U, F: FnOnce(T) -> Option>( option: Option<T>, f: F, ) -> res : Option

requires

option.is_some() ==> f.requires((option.unwrap(),)),

ensures

option.is_none() ==> res.is_none(),

option.is_some() ==> f.ensures((option.unwrap(),), res),

Specification for Option::<T>::and_then

Source

pub unsafe exec fn _verus_external_fn_specification_1037_Option_3258583260__32_T_3262325858__32_okorelse<T, E, F: FnOnce() -> E>( option: Option<T>, err: F, ) -> res : Result<T, E>

requires

option.is_none() ==> err.requires(()),

ensures

option.is_some() ==> res == Ok::<T, E>(option.unwrap()),

option.is_none()
    ==> {
        &&& res.is_err()
        &&& err.ensures((), res->Err_0)

    },

Specification for Option::<T>::ok_or_else

Source

pub unsafe exec fn _verus_external_fn_specification_1038_Option_3258583260__32_T_3262325858__32_unwrapordefault<T: Default>( option: Option<T>, ) -> res : T

ensures

option.is_some() ==> res == option.unwrap(),

option.is_none() ==> T::default.ensures((), res),

Specification for Option::<T>::unwrap_or_default

Source

pub unsafe exec fn _verus_external_fn_specification_1039_Option_3258583260__32_T_3262325858__32_unwraporelse<T, F: FnOnce() -> T>( option: Option<T>, f: F, ) -> res : T

requires

option.is_none() ==> f.requires(()),

ensures

option.is_some() ==> res == option.unwrap(),

option.is_none() ==> f.ensures((), res),

Specification for Option::<T>::unwrap_or_else

Source

pub unsafe exec fn _verus_external_fn_specification_10406032_Option_326032_T_326232_as_32_Clone_3262325858__32_clone<T: Clone>( opt: &Option<T>, ) -> res : Option<T>

ensures

opt.is_none() ==> res.is_none(),

opt.is_some() ==> res.is_some() && cloned::<T>(opt.unwrap(), res.unwrap()),

Specification for <Option<T> as Clone>::clone

Source

pub unsafe exec fn _verus_external_fn_specification_10416032_Option_326032_T_326232_as_32_PartialEq_3262325858__32_eq<T: PartialEq>( x: &Option<T>, y: &Option<T>, ) -> bool

Specification for <Option<T> as PartialEq>::eq

Source

pub unsafe exec fn _verus_external_fn_specification_10426032_Option_326032_T_326232_as_32_PartialOrd_3262325858__32_partial__cmp<T: PartialOrd>( x: &Option<T>, y: &Option<T>, ) -> Option<Ordering>

Specification for <Option<T> as PartialOrd>::partial_cmp

Source

pub unsafe exec fn _verus_external_fn_specification_1050_Range_3258583260__32_Idx_3262325858__32_contains<Idx, U>( r: &Range<Idx>, i: &U, ) -> ret : bool
where Idx: PartialOrd + PartialOrd<Idx>, U: ?Sized + PartialOrd<Idx>,

ensures

<Range<Idx> as ContainsSpec<Idx, U>>::obeys_contains() ==> ret == r.contains_spec(i),

Specification for Range::<Idx>::contains Range::contains method is valid and safe to use only when cmp operations are implemented to satisfy obeys_partial_cmp_spec. Specifically, the comparison must be deterministic, and lt (less than) and le (less than or equal to) must define total orders. If using Range::contains with types that do not satisfy obeys_partial_cmp_spec, no spec is provided.

Source

pub unsafe exec fn _verus_external_fn_specification_1051_RangeInclusive_3258583260__32_Idx_3262325858__32_contains<Idx, U>( r: &RangeInclusive<Idx>, i: &U, ) -> ret : bool
where Idx: PartialOrd + PartialOrd<Idx>, U: ?Sized + PartialOrd<Idx>,

ensures

<RangeInclusive<Idx> as ContainsSpec<Idx, U>>::obeys_contains()
    ==> ret == r.contains_spec(i),

Specification for RangeInclusive::<Idx>::contains

Source

pub unsafe exec fn _verus_external_fn_specification_1052_RangeInclusive_3258583260__32_Idx_3262325858__32_new<Idx>( start: Idx, end: Idx, ) -> ret : RangeInclusive<Idx>

ensures

ret == spec_range_inclusive_new(start, end),

Specification for RangeInclusive::<Idx>::new

Source

pub unsafe exec fn _verus_external_fn_specification_10536032_Range_326032_A_326232_as_32_Iterator_3262325858__32_next<A: Step>( range: &mut Range<A>, ) -> r : Option<A>

ensures

(*final(range), r) == spec_range_next(*old(range)),

Specification for <Range<A> as Iterator>::next

Source

pub unsafe exec fn _verus_external_fn_specification_10546032_Range_326032_T_326232_as_32_RangeBounds_326032_T_32623262325858__32_start__bound<'s, T>( range: &'s Range<T>, ) -> result : Bound<&'s T>

ensures

spec_bound(result) == SpecBound::Included(&range.start),

Specification for <Range<T> as RangeBounds<T>>::start_bound

Source

pub unsafe exec fn _verus_external_fn_specification_10556032_Range_326032_T_326232_as_32_RangeBounds_326032_T_32623262325858__32_end__bound<'s, T>( range: &'s Range<T>, ) -> result : Bound<&'s T>

ensures

spec_bound(result) == SpecBound::Excluded(&range.end),

Specification for <Range<T> as RangeBounds<T>>::end_bound

Source

pub unsafe exec fn _verus_external_fn_specification_10566032_RangeFull_32_as_32_RangeBounds_326032_T_32623262325858__32_start__bound<'s, T: ?Sized>( range: &'s RangeFull, ) -> result : Bound<&'s T>

ensures

spec_bound(result) == SpecBound::Unbounded,

Specification for <RangeFull as RangeBounds<T>>::start_bound

Source

pub unsafe exec fn _verus_external_fn_specification_10576032_RangeFull_32_as_32_RangeBounds_326032_T_32623262325858__32_end__bound<'s, T: ?Sized>( range: &'s RangeFull, ) -> result : Bound<&'s T>

ensures

spec_bound(result) == SpecBound::Unbounded,

Specification for <RangeFull as RangeBounds<T>>::end_bound

Source

pub unsafe exec fn _verus_external_fn_specification_10586032_RangeFrom_326032_T_326232_as_32_RangeBounds_326032_T_32623262325858__32_start__bound<'s, T>( range: &'s RangeFrom<T>, ) -> result : Bound<&'s T>

ensures

spec_bound(result) == SpecBound::Included(&range.start),

Specification for <RangeFrom<T> as RangeBounds<T>>::start_bound

Source

pub unsafe exec fn _verus_external_fn_specification_10596032_RangeFrom_326032_T_326232_as_32_RangeBounds_326032_T_32623262325858__32_end__bound<'s, T>( range: &'s RangeFrom<T>, ) -> result : Bound<&'s T>

ensures

spec_bound(result) == SpecBound::Unbounded,

Specification for <RangeFrom<T> as RangeBounds<T>>::end_bound

Source

pub unsafe exec fn _verus_external_fn_specification_10606032_RangeTo_326032_T_326232_as_32_RangeBounds_326032_T_32623262325858__32_start__bound<'s, T>( range: &'s RangeTo<T>, ) -> result : Bound<&'s T>

ensures

spec_bound(result) == SpecBound::Unbounded,

Specification for <RangeTo<T> as RangeBounds<T>>::start_bound

Source

pub unsafe exec fn _verus_external_fn_specification_10616032_RangeTo_326032_T_326232_as_32_RangeBounds_326032_T_32623262325858__32_end__bound<'s, T>( range: &'s RangeTo<T>, ) -> result : Bound<&'s T>

ensures

spec_bound(result) == SpecBound::Excluded(&range.end),

Specification for <RangeTo<T> as RangeBounds<T>>::end_bound

Source

pub unsafe exec fn _verus_external_fn_specification_10626032_RangeInclusive_326032_T_326232_as_32_RangeBounds_326032_T_32623262325858__32_start__bound<'s, T>( range: &'s RangeInclusive<T>, ) -> result : Bound<&'s T>

ensures

spec_bound(result) == SpecBound::Included(&range@.start),

Specification for <RangeInclusive<T> as RangeBounds<T>>::start_bound

Source

pub unsafe exec fn _verus_external_fn_specification_10636032_RangeInclusive_326032_T_326232_as_32_RangeBounds_326032_T_32623262325858__32_end__bound<'s, T>( range: &'s RangeInclusive<T>, ) -> result : Bound<&'s T>

ensures

spec_bound(result) == SpecBound::Included(&range@.end),

Specification for <RangeInclusive<T> as RangeBounds<T>>::end_bound

Source

pub unsafe exec fn _verus_external_fn_specification_10646032_RangeToInclusive_326032_T_326232_as_32_RangeBounds_326032_T_32623262325858__32_start__bound<'s, T>( range: &'s RangeToInclusive<T>, ) -> result : Bound<&'s T>

ensures

spec_bound(result) == SpecBound::Unbounded,

Specification for <RangeToInclusive<T> as RangeBounds<T>>::start_bound

Source

pub unsafe exec fn _verus_external_fn_specification_10656032_RangeToInclusive_326032_T_326232_as_32_RangeBounds_326032_T_32623262325858__32_end__bound<'s, T>( range: &'s RangeToInclusive<T>, ) -> result : Bound<&'s T>

ensures

spec_bound(result) == SpecBound::Included(&range.end),

Specification for <RangeToInclusive<T> as RangeBounds<T>>::end_bound

Source

pub unsafe exec fn _verus_external_fn_specification_10666032__40_Bound_326032_T_3262324432_Bound_326032_T_326241__32_as_32_RangeBounds_326032_T_32623262325858__32_start__bound<'s, T>( range: &'s (Bound<T>, Bound<T>), ) -> result : Bound<&'s T>

ensures

spec_bound(result) == spec_bound_ref(&range.0),

Specification for <(Bound<T>, Bound<T>) as RangeBounds<T>>::start_bound

Source

pub unsafe exec fn _verus_external_fn_specification_10676032__40_Bound_326032_T_3262324432_Bound_326032_T_326241__32_as_32_RangeBounds_326032_T_32623262325858__32_end__bound<'s, T>( range: &'s (Bound<T>, Bound<T>), ) -> result : Bound<&'s T>

ensures

spec_bound(result) == spec_bound_ref(&range.1),

Specification for <(Bound<T>, Bound<T>) as RangeBounds<T>>::end_bound

Source §

impl VstdSpecsForRustStdLib

Source

pub unsafe exec fn _verus_external_fn_specification_1068_Result_3258583260__32_T_44__32_E_3262325858__32_is__ok<T, E>( r: &Result<T, E>, ) -> b : bool

ensures

b == is_ok(r),

Specification for Result::<T, E>::is_ok

Source

pub unsafe exec fn _verus_external_fn_specification_1069_Result_3258583260__32_T_44__32_E_3262325858__32_is__err<T, E>( r: &Result<T, E>, ) -> b : bool

ensures

b == is_err(r),

Specification for Result::<T, E>::is_err

Source

pub unsafe exec fn _verus_external_fn_specification_1070_Result_3258583260__32_T_44__32_E_3262325858__32_as__ref<T, E>( result: &Result<T, E>, ) -> r : Result<&T, &E>

ensures

r is Ok <==> result is Ok,

r is Ok ==> result->Ok_0 == r->Ok_0,

r is Err <==> result is Err,

r is Err ==> result->Err_0 == r->Err_0,

Specification for Result::<T, E>::as_ref

Source

pub unsafe exec fn _verus_external_fn_specification_1071_Result_3258583260__32_T_44__32_E_3262325858__32_unwrap<T, E: Debug>( result: Result<T, E>, ) -> t : T

requires

result is Ok,

ensures

t == result->Ok_0,

Specification for Result::<T, E>::unwrap

Source

pub unsafe exec fn _verus_external_fn_specification_1072_Result_3258583260__32_T_44__32_E_3262325858__32_unwrap__err<T: Debug, E>( result: Result<T, E>, ) -> e : E

requires

result is Err,

ensures

e == result->Err_0,

Specification for Result::<T, E>::unwrap_err

Source

pub unsafe exec fn _verus_external_fn_specification_1073_Result_3258583260__32_T_44__32_E_3262325858__32_expect<T, E: Debug>( result: Result<T, E>, msg: &str, ) -> t : T

requires

result is Ok,

ensures

t == result->Ok_0,

Specification for Result::<T, E>::expect

Source

pub unsafe exec fn _verus_external_fn_specification_1074_Result_3258583260__32_T_44__32_E_3262325858__32_map<T, E, U, F: FnOnce(T) -> U>( result: Result<T, E>, op: F, ) -> mapped_result : Result<U, E>

requires

result.is_ok() ==> op.requires((result->Ok_0,)),

ensures

result.is_ok()
    ==> mapped_result.is_ok() && op.ensures((result->Ok_0,), mapped_result->Ok_0),

result.is_err() ==> mapped_result == Result::<U, E>::Err(result->Err_0),

Specification for Result::<T, E>::map

Source

pub unsafe exec fn _verus_external_fn_specification_1075_Result_3258583260__32_T_44__32_E_3262325858__32_map__err<T, E, F, O: FnOnce(E) -> F>( result: Result<T, E>, op: O, ) -> mapped_result : Result<T, F>

requires

result.is_err() ==> op.requires((result->Err_0,)),

ensures

result.is_err()
    ==> mapped_result.is_err() && op.ensures((result->Err_0,), mapped_result->Err_0),

result.is_ok() ==> mapped_result == Result::<T, F>::Ok(result->Ok_0),

Specification for Result::<T, E>::map_err

Source

pub unsafe exec fn _verus_external_fn_specification_1076_Result_3258583260__32_T_44__32_E_3262325858__32_ok<T, E>( result: Result<T, E>, ) -> opt : Option<T>

ensures

opt == ok(result),

Specification for Result::<T, E>::ok

Source

pub unsafe exec fn _verus_external_fn_specification_1077_Result_3258583260__32_T_44__32_E_3262325858__32_err<T, E>( result: Result<T, E>, ) -> opt : Option<E>

ensures

opt == err(result),

Specification for Result::<T, E>::err

Source §

impl VstdSpecsForRustStdLib

Source

pub unsafe exec fn _verus_external_fn_specification_10786032_usize_32_as_32_SliceIndex_326032__91_T_933262326232585832_index<T>( i: usize, slice: &[T], ) -> &T

returns

slice@[i as int],

Specification for <usize as SliceIndex<[T]>>::index

Source

pub unsafe exec fn _verus_external_fn_specification_10796032_Range_326032_usize_326232_as_32_SliceIndex_326032__91_T_933262326232585832_index<T>( i: Range<usize>, slice: &[T], ) -> r : &[T]

ensures

r@ == slice@.subrange(i.start as int, i.end as int),

Specification for <Range<usize> as SliceIndex<[T]>>::index

Source

pub unsafe exec fn _verus_external_fn_specification_10806032__91_T_93__32_as_32_Index_326032_I_32623262325858__32_index<T, I: SliceIndex<[T]>>( slice: &[T], index: I, ) -> output : &>::Output

ensures

call_ensures(<I as SliceIndex<[T]>>::index, (index, slice), output),

Specification for <[T] as Index>::index

Source

pub unsafe exec fn _verus_external_fn_specification_10816032__91_T_59__32_N_93__32_as_32_Index_326032_I_32623262325858__32_index<T, I, const N: usize>( array: &[T; N], index: I, ) -> output : &<[T; N] as Index>::Output
where [T]: Index,

ensures

call_ensures(<[T] as Index<I>>::index, (array, index), output),

Specification for <[T; N] as Index>::index

Source

pub unsafe exec fn _verus_external_fn_specification_1082_core_325858__32_hint_325858__32_unreachable__unchecked() -> !

requires

false,

Specification for core::hint::unreachable_unchecked

Source

pub unsafe exec fn _verus_external_fn_specification_10836032__91_T_93326232585832_iter<'a, T>( s: &'a [T], ) -> iter : Iter<'a, T>

ensures

iter == spec_slice_iter(s),

IteratorSpec::decrease(&iter) is Some,

IteratorSpec::initial_value_relation(&iter, &iter),

Specification for [<[T]>::iter]

Source

pub unsafe exec fn _verus_external_fn_specification_108460323832__39_a_32__91_T_93__32_as_32_core_325858__32_iter_325858__32_IntoIterator_3262325858__32_into__iter<'a, T>( s: &'a [T], ) -> iter : Iter<'a, T>

ensures

iter == spec_slice_iter(s),

IteratorSpec::decrease(&iter) is Some,

IteratorSpec::initial_value_relation(&iter, &iter),

Specification for <&'a [T] as core::iter::IntoIterator>::into_iter

Source

pub unsafe exec fn _verus_external_fn_specification_10856032__91_T_93326232585832_first<T>( slice: &[T], ) -> res : Option<&T>

ensures

slice.len() == 0 ==> res.is_none(),

slice.len() != 0 ==> res.is_some() && res.unwrap() == slice[0],

Specification for [<[T]>::first]

Source

pub unsafe exec fn _verus_external_fn_specification_10866032__91_T_93326232585832_last<T>( slice: &[T], ) -> res : Option<&T>

ensures

slice.len() == 0 ==> res.is_none(),

slice.len() != 0 ==> res.is_some() && res.unwrap() == slice@.last(),

Specification for [<[T]>::last]

Source

pub unsafe exec fn _verus_external_fn_specification_10896032__91_T_93326232585832_split__at<T>( slice: &[T], mid: usize, ) -> ret : (&[T], &[T])

requires

0 <= mid <= slice.len(),

ensures

ret.0@ == slice@.subrange(0, mid as int),

ret.1@ == slice@.subrange(mid as int, slice@.len() as int),

Specification for [<[T]>::split_at]

Source

pub unsafe exec fn _verus_external_fn_specification_10916032__91_T_93326232585832_splitatchecked<T>( slice: &[T], mid: usize, ) -> ret : Option<(&[T], &[T])>

ensures

mid <= slice.len()
    ==> (ret matches Some(
        (a, b),
    ) && a@ == slice@.subrange(0, mid as int)
        && b@ == slice@.subrange(mid as int, slice@.len() as int)),

mid > slice.len() ==> ret is None,

Specification for [<[T]>::split_at_checked]

Source

pub unsafe exec fn _verus_external_fn_specification_10926032__91_T_93326232585832_copyfromslice<T: Copy>( dst: &mut [T], src: &[T], )

requires

old(dst)@.len() == src@.len(),

ensures

final(dst)@ == src@,

Specification for [<[T]>::copy_from_slice] Copy the contents of src into dst, which must have the same length.

Source

pub unsafe exec fn _verus_external_fn_specification_10936032__91_T_93326232585832_copy__within_3258583260__32_R_32__62_<T: Copy, R: RangeBounds<usize>>( slice: &mut [T], src: R, dest: usize, )

requires

slice_range_valid(&src, old(slice)@.len()),

(dest as int) + (slice_range_end(&src, old(slice)@.len()) - slice_range_start(&src))
    <= old(slice)@.len(),

ensures

final(slice)@
    == copy_within_result(
        old(slice)@,
        slice_range_start(&src),
        slice_range_end(&src, old(slice)@.len()),
        dest as int,
    ),

Specification for [<[T]>::copy_within::<R>] Copy the elements in range src within the slice to start at index dest.

Source §

impl VstdSpecsForRustStdLib

Source

pub unsafe exec fn _verus_external_fn_specification_1094_Vec_3258583260__32_T_44__32_A_3262325858__32_len<T, A: Allocator>( vec: &Vec<T, A>, ) -> len : usize

ensures

len == spec_vec_len(vec),

Specification for Vec::<T, A>::len

Source

pub unsafe exec fn _verus_external_fn_specification_1095_Vec_3258583260__32_T_3262325858__32_new<T>() -> v : Vec<T>

ensures

v@ == Seq::<T>::empty(),

Specification for Vec::<T>::new

Source

pub unsafe exec fn _verus_external_fn_specification_10966032_Vec_326032_T_326232_as_32_core_325858__32_default_325858__32_Default_3262325858__32_default<T>() -> v : Vec<T>

ensures

v@ == Seq::<T>::empty(),

Specification for <Vec<T> as core::default::Default>::default

Source

pub unsafe exec fn _verus_external_fn_specification_1097_Vec_3258583260__32_T_44__32_A_3262325858__32_new__in<T, A: Allocator>( alloc: A, ) -> v : Vec<T, A>

ensures

v@ == Seq::<T>::empty(),

Specification for Vec::<T, A>::new_in

Source

pub unsafe exec fn _verus_external_fn_specification_1098_Vec_3258583260__32_T_3262325858__32_with__capacity<T>( capacity: usize, ) -> v : Vec<T>

ensures

v@ == Seq::<T>::empty(),

Specification for Vec::<T>::with_capacity

Source

pub unsafe exec fn _verus_external_fn_specification_1099_Vec_3258583260__32_T_44__32_A_3262325858__32_withcapacityin<T, A: Allocator>( capacity: usize, alloc: A, ) -> v : Vec<T, A>

ensures

v@ == Seq::<T>::empty(),

Specification for Vec::<T, A>::with_capacity_in

Source

pub unsafe exec fn _verus_external_fn_specification_1100_Vec_3258583260__32_T_44__32_A_3262325858__32_reserve<T, A: Allocator>( vec: &mut Vec<T, A>, additional: usize, )

ensures

final(vec)@ == old(vec)@,

Specification for Vec::<T, A>::reserve

Source

pub unsafe exec fn _verus_external_fn_specification_1101_Vec_3258583260__32_T_44__32_A_3262325858__32_try__reserve<T, A: Allocator>( vec: &mut Vec<T, A>, additional: usize, ) -> result : Result<(), TryReserveError>

ensures

final(vec)@ == old(vec)@,

Specification for Vec::<T, A>::try_reserve

Source

pub unsafe exec fn _verus_external_fn_specification_1102_Vec_3258583260__32_T_44__32_A_3262325858__32_push<T, A: Allocator>( vec: &mut Vec<T, A>, value: T, )

ensures

final(vec)@ == old(vec)@.push(value),

Specification for Vec::<T, A>::push

Source

pub unsafe exec fn _verus_external_fn_specification_1103_Vec_3258583260__32_T_44__32_A_3262325858__32_pop<T, A: Allocator>( vec: &mut Vec<T, A>, ) -> value : Option<T>

ensures

old(vec)@.len() > 0
    ==> value == Some(old(vec)@[old(vec)@.len() - 1])
        && final(vec)@ == old(vec)@.subrange(0, old(vec)@.len() - 1),

old(vec)@.len() == 0 ==> value == None::<T> && final(vec)@ == old(vec)@,

Specification for Vec::<T, A>::pop

Source

pub unsafe exec fn _verus_external_fn_specification_1104_Vec_3258583260__32_T_44__32_A_3262325858__32_append<T, A: Allocator>( vec: &mut Vec<T, A>, other: &mut Vec<T, A>, )

ensures

final(vec)@ == old(vec)@ + old(other)@,

final(other)@ == Seq::<T>::empty(),

Specification for Vec::<T, A>::append

Source

pub unsafe exec fn _verus_external_fn_specification_1105_Vec_3258583260__32_T_44__32_A_3262325858__32_extendfromslice<T: Clone, A: Allocator>( vec: &mut Vec<T, A>, other: &[T], )

ensures

final(vec)@.len() == old(vec)@.len() + other@.len(),

forall |i: int| {
    0 <= i < final(vec)@.len()
        ==> if i < old(vec)@.len() {
            final(vec)@[i] == old(vec)@[i]
        } else {
            cloned::<T>(other@[i - old(vec)@.len()], final(vec)@[i])
        }
},

Specification for Vec::<T, A>::extend_from_slice

Source

pub unsafe exec fn _verus_external_fn_specification_1106_Vec_3258583260__32_T_44__32_A_3262325858__32_index<T, I: SliceIndex<[T]>, A: Allocator>( vec: &Vec<T, A>, i: I, ) -> r : &<Vec<T, A> as Index>::Output ⓘ

ensures

exists |s: &[T]| (
    #[trigger] s@ == vec@ && call_ensures(<I as SliceIndex<[T]>>::index, (i, s), r)
),

Specification for Vec::<T, A>::index

Source

pub unsafe exec fn _verus_external_fn_specification_1107_Vec_3258583260__32_T_44__32_A_3262325858__32_swap__remove<T, A: Allocator>( vec: &mut Vec<T, A>, i: usize, ) -> element : T

requires

i < old(vec).len(),

ensures

element == old(vec)[i as int],

final(vec)@ == old(vec)@.update(i as int, old(vec)@.last()).drop_last(),

Specification for Vec::<T, A>::swap_remove

Source

pub unsafe exec fn _verus_external_fn_specification_1108_Vec_3258583260__32_T_44__32_A_3262325858__32_insert<T, A: Allocator>( vec: &mut Vec<T, A>, i: usize, element: T, )

requires

i <= old(vec).len(),

ensures

final(vec)@ == old(vec)@.insert(i as int, element),

Specification for Vec::<T, A>::insert

Source

pub unsafe exec fn _verus_external_fn_specification_11096032_Vec_326032_T_44__32_A_32623262325858__32_is__empty<T, A: Allocator>( v: &Vec<T, A>, ) -> res : bool

ensures

res <==> v@.len() == 0,

Specification for Vec::<T, A>::is_empty

Source

pub unsafe exec fn _verus_external_fn_specification_1110_Vec_3258583260__32_T_44__32_A_3262325858__32_remove<T, A: Allocator>( vec: &mut Vec<T, A>, i: usize, ) -> element : T

requires

i < old(vec).len(),

ensures

element == old(vec)[i as int],

final(vec)@ == old(vec)@.remove(i as int),

Specification for Vec::<T, A>::remove

Source

pub unsafe exec fn _verus_external_fn_specification_1111_Vec_3258583260__32_T_44__32_A_3262325858__32_clear<T, A: Allocator>( vec: &mut Vec<T, A>, )

ensures

final(vec).view() == Seq::<T>::empty(),

Specification for Vec::<T, A>::clear

Source

pub unsafe exec fn _verus_external_fn_specification_1112_Vec_3258583260__32_T_44__32_A_3262325858__32_as__slice<T, A: Allocator>( vec: &Vec<T, A>, ) -> slice : &[T]

ensures

slice@ == vec@,

Specification for Vec::<T, A>::as_slice

Source

pub unsafe exec fn _verus_external_fn_specification_11146032_Vec_326032_T_44__32_A_326232_as_32_core_325858__32_ops_325858__32_Deref_3262325858__32_deref<T, A: Allocator>( vec: &Vec<T, A>, ) -> slice : &[T]

ensures

slice@ == vec@,

Specification for <Vec<T, A> as core::ops::Deref>::deref

Source

pub unsafe exec fn _verus_external_fn_specification_11156032_Vec_326032_T_44__32_A_326232_as_32_core_325858__32_ops_325858__32_DerefMut_3262325858__32_deref__mut<T, A: Allocator>( vec: &mut Vec<T, A>, ) -> slice : &mut [T]

ensures

slice@ == old(vec)@,

final(slice)@ == final(vec)@,

Specification for <Vec<T, A> as core::ops::DerefMut>::deref_mut

Source

pub unsafe exec fn _verus_external_fn_specification_1116_Vec_3258583260__32_T_44__32_A_3262325858__32_split__off<T, A: Allocator + Clone>( vec: &mut Vec<T, A>, at: usize, ) -> return_value : Vec<T, A>

requires

at <= old(vec)@.len(),

ensures

final(vec)@ == old(vec)@.subrange(0, at as int),

return_value@ == old(vec)@.subrange(at as int, old(vec)@.len() as int),

Specification for Vec::<T, A>::split_off

Source

pub unsafe exec fn _verus_external_fn_specification_11176032_Vec_326032_T_44__32_A_326232_as_32_Clone_3262325858__32_clone<T: Clone, A: Allocator + Clone>( vec: &Vec<T, A>, ) -> res : Vec<T, A>

ensures

res.len() == vec.len(),

forall |i| 0 <= i < vec.len() ==> cloned::<T>(vec[i], res[i]),

vec_clone_trigger(*vec, res),

vec@ =~= res@ ==> vec@ == res@,

Specification for <Vec<T, A> as Clone>::clone

Source

pub unsafe exec fn _verus_external_fn_specification_1118_Vec_3258583260__32_T_44__32_A_3262325858__32_truncate<T, A: Allocator>( vec: &mut Vec<T, A>, len: usize, )

ensures

len <= old(vec).len() ==> final(vec)@ == old(vec)@.subrange(0, len as int),

len > old(vec).len() ==> final(vec)@ == old(vec)@,

Specification for Vec::<T, A>::truncate

Source

pub unsafe exec fn _verus_external_fn_specification_1119_Vec_3258583260__32_T_44__32_A_3262325858__32_resize<T: Clone, A: Allocator>( vec: &mut Vec<T, A>, len: usize, value: T, )

ensures

len <= old(vec).len() ==> final(vec)@ == old(vec)@.subrange(0, len as int),

len > old(vec).len()
    ==> {
        &&& final(vec)@.len() == len
        &&& final(vec)@.subrange(0, old(vec).len() as int) == old(vec)@
        &&& forall |i| old(vec).len() <= i < len ==> cloned::<T>(value, final(vec)@[i])

    },

Specification for Vec::<T, A>::resize

Source

pub unsafe exec fn _verus_external_fn_specification_11206032_Vec_326032_T_44__32_A1_326232_as_32_PartialEq_326032_Vec_326032_U_44__32_A2_326232623262325858__32_eq<T: PartialEq, U, A1: Allocator, A2: Allocator>( x: &Vec<T, A1>, y: &Vec<U, A2>, ) -> bool

Specification for <Vec<T, A1> as PartialEq<Vec<U, A2>>>::eq

Source

pub unsafe exec fn _verus_external_fn_specification_1121_alloc_325858__32_vec_325858__32_from__elem<T: Clone>( elem: T, n: usize, ) -> v : Vec<T>

ensures

v.len() == n,

forall |i| 0 <= i < n ==> cloned(elem, #[trigger] v@[i]),

Specification for [alloc::vec::from_elem]

Source

pub unsafe exec fn _verus_external_fn_specification_1122_Vec_3258583260__32_T_44__32_A_3262325858__32_into__iter<T, A: Allocator>( vec: Vec<T, A>, ) -> iter : <Vec<T, A> as IntoIterator>::IntoIter ⓘ

ensures

iter == spec_into_iter(vec),

IteratorSpec::decrease(&iter) is Some,

IteratorSpec::initial_value_relation(&iter, &iter),

Specification for Vec::<T, A>::into_iter

Source

pub unsafe exec fn _verus_external_fn_specification_112360323832__39_a_32_Vec_326032_T_44__32_A_326232_as_32_core_325858__32_iter_325858__32_IntoIterator_3262325858__32_into__iter<'a, T, A: Allocator>( vec: &'a Vec<T, A>, ) -> iter : <&'a Vec<T, A> as IntoIterator>::IntoIter ⓘ

ensures

iter == spec_into_iter_borrowed(vec),

IteratorSpec::decrease(&iter) is Some,

IteratorSpec::initial_value_relation(&iter, &iter),

Specification for <&'a Vec<T, A> as core::iter::IntoIterator>::into_iter

Source §

impl VstdSpecsForRustStdLib

Source

pub unsafe exec fn _verus_external_fn_specification_1124_VecDeque_3258583260__32_T_44__32_A_3262325858__32_index<T, A: Allocator>( v: &VecDeque<T, A>, i: usize, ) -> result : &T

ensures

result == v.spec_index(i as int),

Specification for VecDeque::<T, A>::index

Source

pub unsafe exec fn _verus_external_fn_specification_1125_VecDeque_3258583260__32_T_44__32_A_3262325858__32_len<T, A: Allocator>( v: &VecDeque<T, A>, ) -> len : usize

ensures

len == spec_vec_dequeue_len(v),

Specification for VecDeque::<T, A>::len

Source

pub unsafe exec fn _verus_external_fn_specification_1126_VecDeque_3258583260__32_T_3262325858__32_new<T>() -> v : VecDeque<T>

ensures

v@ == Seq::<T>::empty(),

Specification for VecDeque::<T>::new

Source

pub unsafe exec fn _verus_external_fn_specification_11276032_VecDeque_326032_T_326232_as_32_core_325858__32_default_325858__32_Default_3262325858__32_default<T>() -> v : VecDeque<T>

ensures

v@ == Seq::<T>::empty(),

Specification for <VecDeque<T> as core::default::Default>::default

Source

pub unsafe exec fn _verus_external_fn_specification_1128_VecDeque_3258583260__32_T_3262325858__32_with__capacity<T>( capacity: usize, ) -> v : VecDeque<T>

ensures

v@ == Seq::<T>::empty(),

Specification for VecDeque::<T>::with_capacity

Source

pub unsafe exec fn _verus_external_fn_specification_1129_VecDeque_3258583260__32_T_44__32_A_3262325858__32_reserve<T, A: Allocator>( v: &mut VecDeque<T, A>, additional: usize, )

ensures

final(v)@ == old(v)@,

Specification for VecDeque::<T, A>::reserve

Source

pub unsafe exec fn _verus_external_fn_specification_1130_VecDeque_3258583260__32_T_44__32_A_3262325858__32_push__back<T, A: Allocator>( v: &mut VecDeque<T, A>, value: T, )

ensures

final(v)@ == old(v)@.push(value),

Specification for VecDeque::<T, A>::push_back

Source

pub unsafe exec fn _verus_external_fn_specification_1131_VecDeque_3258583260__32_T_44__32_A_3262325858__32_push__front<T, A: Allocator>( v: &mut VecDeque<T, A>, value: T, )

ensures

final(v)@ == seq![value] + old(v)@,

Specification for VecDeque::<T, A>::push_front

Source

pub unsafe exec fn _verus_external_fn_specification_1132_VecDeque_3258583260__32_T_44__32_A_3262325858__32_pop__back<T, A: Allocator>( v: &mut VecDeque<T, A>, ) -> value : Option<T>

ensures

match value {
    Some(x) => (
        &&& old(v)@.len() > 0
        &&& x == old(v)@[old(v)@.len() - 1]
        &&& final(v)@ == old(v)@.subrange(0, old(v)@.len() as int - 1)

    ),
    None => (
        &&& old(v)@.len() == 0
        &&& final(v)@ == old(v)@

    ),
},

Specification for VecDeque::<T, A>::pop_back

Source

pub unsafe exec fn _verus_external_fn_specification_1133_VecDeque_3258583260__32_T_44__32_A_3262325858__32_pop__front<T, A: Allocator>( v: &mut VecDeque<T, A>, ) -> value : Option<T>

ensures

match value {
    Some(x) => (
        &&& old(v)@.len() > 0
        &&& x == old(v)@[0]
        &&& final(v)@ == old(v)@.subrange(1, old(v)@.len() as int)

    ),
    None => (
        &&& old(v)@.len() == 0
        &&& final(v)@ == old(v)@

    ),
},

Specification for VecDeque::<T, A>::pop_front

Source

pub unsafe exec fn _verus_external_fn_specification_1134_VecDeque_3258583260__32_T_44__32_A_3262325858__32_append<T, A: Allocator>( v: &mut VecDeque<T, A>, other: &mut VecDeque<T, A>, )

ensures

final(v)@ == old(v)@ + old(other)@,

final(other)@ == Seq::<T>::empty(),

Specification for VecDeque::<T, A>::append

Source

pub unsafe exec fn _verus_external_fn_specification_1135_VecDeque_3258583260__32_T_44__32_A_3262325858__32_insert<T, A: Allocator>( v: &mut VecDeque<T, A>, i: usize, element: T, )

requires

i <= old(v).len(),

ensures

final(v)@ == old(v)@.insert(i as int, element),

Specification for VecDeque::<T, A>::insert

Source

pub unsafe exec fn _verus_external_fn_specification_1136_VecDeque_3258583260__32_T_44__32_A_3262325858__32_remove<T, A: Allocator>( v: &mut VecDeque<T, A>, i: usize, ) -> element : Option<T>

ensures

match element {
    Some(x) => (
        &&& i < old(v)@.len()
        &&& x == old(v)@[i as int]
        &&& final(v)@ == old(v)@.remove(i as int)

    ),
    None => (
        &&& old(v)@.len() <= i
        &&& final(v)@ == old(v)@

    ),
},

Specification for VecDeque::<T, A>::remove

Source

pub unsafe exec fn _verus_external_fn_specification_1137_VecDeque_3258583260__32_T_44__32_A_3262325858__32_clear<T, A: Allocator>( v: &mut VecDeque<T, A>, )

ensures

final(v).view() == Seq::<T>::empty(),

Specification for VecDeque::<T, A>::clear

Source

pub unsafe exec fn _verus_external_fn_specification_1138_VecDeque_3258583260__32_T_44__32_A_3262325858__32_split__off<T, A: Allocator + Clone>( v: &mut VecDeque<T, A>, at: usize, ) -> return_value : VecDeque<T, A>

requires

at <= old(v)@.len(),

ensures

final(v)@ == old(v)@.subrange(0, at as int),

return_value@ == old(v)@.subrange(at as int, old(v)@.len() as int),

Specification for VecDeque::<T, A>::split_off

Source

pub unsafe exec fn _verus_external_fn_specification_11396032_VecDeque_326032_T_44__32_A_326232_as_32_Clone_3262325858__32_clone<T: Clone, A: Allocator + Clone>( v: &VecDeque<T, A>, ) -> res : VecDeque<T, A>

ensures

res.len() == v.len(),

forall |i| 0 <= i < v.len() ==> cloned::<T>(v[i], res[i]),

vec_dequeue_clone_trigger(*v, res),

v@ =~= res@ ==> v@ == res@,

Specification for <VecDeque<T, A> as Clone>::clone

Source

pub unsafe exec fn _verus_external_fn_specification_1140_VecDeque_3258583260__32_T_44__32_A_3262325858__32_truncate<T, A: Allocator>( v: &mut VecDeque<T, A>, len: usize, )

ensures

len <= old(v).len() ==> final(v)@ == old(v)@.subrange(0, len as int),

len > old(v).len() ==> final(v)@ == old(v)@,

Specification for VecDeque::<T, A>::truncate

Source

pub unsafe exec fn _verus_external_fn_specification_1141_VecDeque_3258583260__32_T_44__32_A_3262325858__32_resize<T: Clone, A: Allocator>( v: &mut VecDeque<T, A>, len: usize, value: T, )

ensures

len <= old(v).len() ==> final(v)@ == old(v)@.subrange(0, len as int),

len > old(v).len()
    ==> {
        &&& final(v)@.len() == len
        &&& final(v)@.subrange(0, old(v).len() as int) == old(v)@
        &&& forall |i| old(v).len() <= i < len ==> cloned::<T>(value, final(v)@[i])

    },

Specification for VecDeque::<T, A>::resize

Source

pub unsafe exec fn _verus_external_fn_specification_1142_VecDeque_3258583260__32_T_44__32_A_3262325858__32_iter<'a, T, A: Allocator>( v: &'a VecDeque<T, A>, ) -> iter : Iter<'a, T>

ensures

iter == spec_iter(v),

IteratorSpec::decrease(&iter) is Some,

IteratorSpec::initial_value_relation(&iter, &iter),

Specification for VecDeque::<T, A>::iter

Source §

impl VstdSpecsForRustStdLib

Source

pub unsafe exec fn _verus_external_fn_specification_11436032__91_T_93326232585832_into__vec<T, A: Allocator>( b: Box<[T], A>, ) -> v : Vec<T, A>

ensures

v@ == b@,

Specification for [<[T]>::into_vec]

Source

pub unsafe exec fn _verus_external_fn_specification_1144_Box_3258583260__32_T_3262325858__32_new<T>( t: T, ) -> v : Box<T>

ensures

*v == t,

Specification for Box::<T>::new

Source

pub unsafe exec fn _verus_external_fn_specification_11456032_Box_326032_T_443262__32_as_32_core_325858__32_default_325858__32_Default_3262325858__32_default<T: Default>() -> res : Box<T>

ensures

T::default.ensures((), *res),

Specification for <Box<T> as core::default::Default>::default

Source

pub unsafe exec fn _verus_external_fn_specification_1146_Rc_3258583260__32_T_3262325858__32_new<T>( t: T, ) -> v : Rc<T>

ensures

*v == t,

Specification for Rc::<T>::new

Source

pub unsafe exec fn _verus_external_fn_specification_11476032_Rc_326032_T_443262__32_as_32_core_325858__32_default_325858__32_Default_3262325858__32_default<T: Default>() -> res : Rc<T>

ensures

T::default.ensures((), *res),

Specification for <Rc<T> as core::default::Default>::default

Source

pub unsafe exec fn _verus_external_fn_specification_1148_Arc_3258583260__32_T_3262325858__32_new<T>( t: T, ) -> v : Arc<T>

ensures

*v == t,

Specification for Arc::<T>::new

Source

pub unsafe exec fn _verus_external_fn_specification_11496032_Arc_326032_T_443262__32_as_32_core_325858__32_default_325858__32_Default_3262325858__32_default<T: Default>() -> res : Arc<T>

ensures

T::default.ensures((), *res),

Specification for <Arc<T> as core::default::Default>::default

Source

pub unsafe exec fn _verus_external_fn_specification_11506032_Box_326032_T_44__32_A_326232_as_32_Clone_3262325858__32_clone<T: Clone, A: Allocator + Clone>( b: &Box<T, A>, ) -> res : Box<T, A>

ensures

cloned::<T>(**b, *res),

Specification for <Box<T, A> as Clone>::clone

Source

pub unsafe exec fn _verus_external_fn_specification_1151_Rc_3258583260__32_T_44__32_A_3262325858__32_try__unwrap<T, A: Allocator>( v: Rc<T, A>, ) -> result : Result<T, Rc<T, A>>

ensures

match result {
    Ok(t) => t == *v,
    Err(e) => e == v,
},

Specification for Rc::<T, A>::try_unwrap

Source

pub unsafe exec fn _verus_external_fn_specification_1152_Rc_3258583260__32_T_44__32_A_3262325858__32_into__inner<T, A: Allocator>( v: Rc<T, A>, ) -> result : Option<T>

ensures

result matches Some(t) ==> t == *v,

Source §

open spec fn obeys_into_spec() -> bool

{ <U as FromSpec<Self>>::obeys_from_spec() }

Source §

open spec fn into_spec(self) -> U

{ U::from_spec(self) }

Source §

impl<T, U> TryFrom for T
where U: Into<T>,

Source §

type Error = Infallible

The type returned in the event of a conversion error.

Source §

fn try_from(value: U) -> Result<T, <T as TryFrom>::Error>

Performs the conversion.

fn try_into(self) -> Result<U, >::Error>

Performs the conversion.

Source §

impl<T, VERUS_SPEC__A> TryIntoSpec<T> for VERUS_SPEC__A
where VERUS_SPEC__A: TryInto<T>,

Source §

exec fn obeys_try_into_spec() -> bool

Source §

exec fn try_into_spec(self) -> Result<T, <VERUS_SPEC__A as TryInto<T>>::Error>

Source §

impl<T, U> TryIntoSpecImpl for T
where U: TryFrom<T>,

Source §

open spec fn obeys_try_into_spec() -> bool

{ <U as TryFromSpec<Self>>::obeys_try_from_spec() }

Source §

open spec fn try_into_spec(self) -> Result<U, >::Error>

{ <U as TryFromSpec<Self>>::try_from_spec(self) }

§

impl<A> SpecEq<&A> for A
where A: ?Sized,

§

impl<A> SpecEq<&mut A> for A
where A: ?Sized,

§

impl<A> SpecEq<A> for A
where A: ?Sized,

§

impl<A> SpecEq<Ghost<A>> for A

§

VstdSpecsForRustStdLib

Struct VstdSpecsForRustStdLib Copy item path

Implementations§

impl VstdSpecsForRustStdLib

pub unsafe exec fn _verus_external_fn_specification_0__60__32__38__32__39_a_32__91_T_59__32_N_93__32_as_32_core_32__58__58__32_iter_32__58__58__32_IntoIterator_32__62__32__58__58__32_into__iter<'a, T, const N: usize>( s: &'a [T; N], ) -> iter : Iter<'a, T>

pub unsafe exec fn _verus_external_fn_specification_1__60__32__91_T_59__32_N_93__32__62__32__58__58__32_as__slice<T, const N: usize>( ar: &[T; N], ) -> out : &[T]

impl VstdSpecsForRustStdLib

pub unsafe exec fn _verus_external_fn_specification_2__60__32_f32_32_as_32_Clone_32__62__32__58__58__32_clone( f: &f32, ) -> res : f32

pub unsafe exec fn _verus_external_fn_specification_3__60__32_f64_32_as_32_Clone_32__62__32__58__58__32_clone( f: &f64, ) -> res : f64

impl VstdSpecsForRustStdLib

pub unsafe exec fn _verus_external_fn_specification_4_core_32__58__58__32_mem_32__58__58__32_size__of_32__58__58__32__60__32_V_32__62_<V>() -> u : usize

pub unsafe exec fn _verus_external_fn_specification_5_core_32__58__58__32_mem_32__58__58__32_align__of_32__58__58__32__60__32_V_32__62_<V>() -> u : usize

pub unsafe exec fn _verus_external_fn_specification_6_core_32__58__58__32_mem_32__58__58__32_size__of__val_32__58__58__32__60__32_V_32__62_<V: ?Sized>( val: &V, ) -> u : usize

pub unsafe exec fn _verus_external_fn_specification_7_core_32__58__58__32_mem_32__58__58__32_align__of__val_32__58__58__32__60__32_V_32__62_<V: ?Sized>( val: &V, ) -> u : usize

impl VstdSpecsForRustStdLib

pub unsafe exec fn _verus_external_fn_specification_1155__60__32__42__32_mut_32_T_32__62__32__58__58__32_addr<T: PointeeSized>( p: *mut T, ) -> addr : usize

pub unsafe exec fn _verus_external_fn_specification_1156__60__32__42__32_mut_32_T_32__62__32__58__58__32_with__addr<T: PointeeSized>( p: *mut T, addr: usize, ) -> q : *mut T

impl VstdSpecsForRustStdLib

pub unsafe exec fn _verus_external_fn_specification_1153__60__32__42__32_const_32_T_32__62__32__58__58__32_addr<T: PointeeSized>( p: *const T, ) -> addr : usize

pub unsafe exec fn _verus_external_fn_specification_1154__60__32__42__32_const_32_T_32__62__32__58__58__32_with__addr<T: PointeeSized>( p: *const T, addr: usize, ) -> q : *const T

impl VstdSpecsForRustStdLib

pub unsafe exec fn _verus_external_fn_specification_8__60__32__42__32_mut_32_T_32_as_32_PartialEq_32__60__32__42__32_mut_32_T_32__62__32__62__32__58__58__32_eq<T: PointeeSized>( x: &*mut T, y: &*mut T, ) -> res : bool

pub unsafe exec fn _verus_external_fn_specification_9__60__32__42__32_const_32_T_32_as_32_PartialEq_32__60__32__42__32_const_32_T_32__62__32__62__32__58__58__32_eq<T: PointeeSized>( x: &*const T, y: &*const T, ) -> res : bool

pub unsafe exec fn _verus_external_fn_specification_10_core_32__58__58__32_ptr_32__58__58__32_null<T: PointeeSized + Pointee<Metadata = ()>>() -> res : *const T

pub unsafe exec fn _verus_external_fn_specification_11_core_32__58__58__32_ptr_32__58__58__32_null__mut<T: PointeeSized + Pointee<Metadata = ()>>() -> res : *mut T

impl VstdSpecsForRustStdLib

pub unsafe exec fn _verus_external_fn_specification_12__60__32__91_T_93__32__62__32__58__58__32_len<T>( slice: &[T], ) -> len : usize

pub unsafe exec fn _verus_external_fn_specification_13__60__32__91_T_93__32__62__32__58__58__32_is__empty<T>( slice: &[T], ) -> b : bool

pub unsafe exec fn _verus_external_fn_specification_14__60__32__91_T_93__32__62__32__58__58__32_get_32__58__58__32__60__32_I_32__62_<T, I>( slice: &[T], i: I, ) -> b : Option<&<I as SliceIndex<[T]>>::Output>where I: SliceIndex<[T]>,

impl VstdSpecsForRustStdLib

pub unsafe exec fn _verus_external_fn_specification_15_str_32__58__58__32_is__ascii( s: &str, ) -> b : bool

pub unsafe exec fn _verus_external_fn_specification_16_str_32__58__58__32_to__owned( s: &str, ) -> res : String

pub unsafe exec fn _verus_external_fn_specification_17_str_32__58__58__32_as__bytes( s: &str, ) -> b : &[u8] ⓘ

pub unsafe exec fn _verus_external_fn_specification_18_str_32__58__58__32_len( s: &str, ) -> usize

pub unsafe exec fn _verus_external_fn_specification_19_str_32__58__58__32_is__empty( s: &str, ) -> bool

pub unsafe exec fn _verus_external_fn_specification_20_str_32__58__58__32_is__char__boundary( s: &str, index: usize, ) -> bool

pub unsafe exec fn _verus_external_fn_specification_21_str_32__58__58__32_split__at( s: &str, mid: usize, ) -> res : (&str, &str)

pub unsafe exec fn _verus_external_fn_specification_22_str_32__58__58__32_from__utf8__unchecked( v: &[u8], ) -> res : &str

pub unsafe exec fn _verus_external_fn_specification_23__60__32_T_32_as_32_ToString_32__62__32__58__58__32_to__string<T: Display + ?Sized>( t: &T, ) -> res : String

pub unsafe exec fn _verus_external_fn_specification_24_String_32__58__58__32_as__str<'a>( s: &'a String, ) -> res : &'a str

pub unsafe exec fn _verus_external_fn_specification_25__60__32_String_32_as_32_core_32__58__58__32_ops_32__58__58__32_Deref_32__62__32__58__58__32_deref<'a>( s: &'a String, ) -> res : &'a str

pub unsafe exec fn _verus_external_fn_specification_26__60__32_String_32_as_32_Clone_32__62__32__58__58__32_clone( s: &String, ) -> res : String

pub unsafe exec fn _verus_external_fn_specification_27__60__32_String_32_as_32_PartialEq_32__62__32__58__58__32_eq( s: &String, other: &String, ) -> res : bool

pub unsafe exec fn _verus_external_fn_specification_28_String_32__58__58__32_new() -> res : String

pub unsafe exec fn _verus_external_fn_specification_29__60__32_String_32_as_32_core_32__58__58__32_default_32__58__58__32_Default_32__62__32__58__58__32_default() -> r : String

pub unsafe exec fn _verus_external_fn_specification_30_str_32__58__58__32_chars( s: &str, ) -> iter : Chars<'_>

impl VstdSpecsForRustStdLib

pub unsafe exec fn _verus_external_fn_specification_31_alloc_32__58__58__32_boxed_32__58__58__32_box__assume__init__into__vec__unsafe<T, const N: usize>( vals: Box<MaybeUninit<[T; N]>>, ) -> result : Vec<T>

pub unsafe exec fn _verus_external_fn_specification_32_alloc_32__58__58__32_intrinsics_32__58__58__32_write__box__via__move<T>( _0: Box<MaybeUninit<T>>, v: T, ) -> result : Box<MaybeUninit<T>>

pub unsafe exec fn _verus_external_fn_specification_33_alloc_32__58__58__32_boxed_32__58__58__32_Box_32__58__58__32__60__32_T_32__62__32__58__58__32_new__uninit<T>() -> Box<MaybeUninit<T>>

impl VstdSpecsForRustStdLib

pub unsafe exec fn _verus_external_fn_specification_34__60__32_AtomicU8_32__62__32__58__58__32_new( v: u8, ) -> AtomicU8

pub unsafe exec fn _verus_external_fn_specification_35__60__32_AtomicU8_32__62__32__58__58__32_compare__exchange( atomic: &AtomicU8, current: u8, new: u8, success: Ordering, failure: Ordering, ) -> Result<u8, u8>

pub unsafe exec fn _verus_external_fn_specification_36__60__32_AtomicU8_32__62__32__58__58__32_compare__exchange__weak( atomic: &AtomicU8, current: u8, new: u8, success: Ordering, failure: Ordering, ) -> Result<u8, u8>

pub unsafe exec fn _verus_external_fn_specification_37__60__32_AtomicU8_32__62__32__58__58__32_fetch__and( atomic: &AtomicU8, val: u8, order: Ordering, ) -> u8

pub unsafe exec fn _verus_external_fn_specification_38__60__32_AtomicU8_32__62__32__58__58__32_fetch__nand( atomic: &AtomicU8, val: u8, order: Ordering, ) -> u8

pub unsafe exec fn _verus_external_fn_specification_39__60__32_AtomicU8_32__62__32__58__58__32_fetch__or( atomic: &AtomicU8, val: u8, order: Ordering, ) -> u8

pub unsafe exec fn _verus_external_fn_specification_40__60__32_AtomicU8_32__62__32__58__58__32_fetch__xor( atomic: &AtomicU8, val: u8, order: Ordering, ) -> u8

pub unsafe exec fn _verus_external_fn_specification_41__60__32_AtomicU8_32__62__32__58__58__32_load( atomic: &AtomicU8, order: Ordering, ) -> u8

pub unsafe exec fn _verus_external_fn_specification_42__60__32_AtomicU8_32__62__32__58__58__32_store( atomic: &AtomicU8, val: u8, order: Ordering, )

pub unsafe exec fn _verus_external_fn_specification_43__60__32_AtomicU8_32__62__32__58__58__32_swap( atomic: &AtomicU8, val: u8, order: Ordering, ) -> u8

impl VstdSpecsForRustStdLib

pub unsafe exec fn _verus_external_fn_specification_44__60__32_AtomicU8_32__62__32__58__58__32_fetch__add( atomic: &AtomicU8, val: u8, order: Ordering, ) -> u8

pub unsafe exec fn _verus_external_fn_specification_45__60__32_AtomicU8_32__62__32__58__58__32_fetch__sub( atomic: &AtomicU8, val: u8, order: Ordering, ) -> u8

pub unsafe exec fn _verus_external_fn_specification_46__60__32_AtomicU8_32__62__32__58__58__32_fetch__min( atomic: &AtomicU8, val: u8, order: Ordering, ) -> u8

pub unsafe exec fn _verus_external_fn_specification_47__60__32_AtomicU8_32__62__32__58__58__32_fetch__max( atomic: &AtomicU8, val: u8, order: Ordering, ) -> u8

impl VstdSpecsForRustStdLib

pub unsafe exec fn _verus_external_fn_specification_48__60__32_AtomicU16_32__62__32__58__58__32_new( v: u16, ) -> AtomicU16

pub unsafe exec fn _verus_external_fn_specification_49__60__32_AtomicU16_32__62__32__58__58__32_compare__exchange( atomic: &AtomicU16, current: u16, new: u16, success: Ordering, failure: Ordering, ) -> Result<u16, u16>

pub unsafe exec fn _verus_external_fn_specification_50__60__32_AtomicU16_32__62__32__58__58__32_compare__exchange__weak( atomic: &AtomicU16, current: u16, new: u16, success: Ordering, failure: Ordering, ) -> Result<u16, u16>

pub unsafe exec fn _verus_external_fn_specification_51__60__32_AtomicU16_32__62__32__58__58__32_fetch__and( atomic: &AtomicU16, val: u16, order: Ordering, ) -> u16

pub unsafe exec fn _verus_external_fn_specification_52__60__32_AtomicU16_32__62__32__58__58__32_fetch__nand( atomic: &AtomicU16, val: u16, order: Ordering, ) -> u16

pub unsafe exec fn _verus_external_fn_specification_53__60__32_AtomicU16_32__62__32__58__58__32_fetch__or( atomic: &AtomicU16, val: u16, order: Ordering, ) -> u16

pub unsafe exec fn _verus_external_fn_specification_54__60__32_AtomicU16_32__62__32__58__58__32_fetch__xor( atomic: &AtomicU16, val: u16, order: Ordering, ) -> u16

pub unsafe exec fn _verus_external_fn_specification_55__60__32_AtomicU16_32__62__32__58__58__32_load( atomic: &AtomicU16, order: Ordering, ) -> u16

pub unsafe exec fn _verus_external_fn_specification_56__60__32_AtomicU16_32__62__32__58__58__32_store( atomic: &AtomicU16, val: u16, order: Ordering, )

pub unsafe exec fn _verus_external_fn_specification_57__60__32_AtomicU16_32__62__32__58__58__32_swap( atomic: &AtomicU16, val: u16, order: Ordering, ) -> u16

impl VstdSpecsForRustStdLib

pub unsafe exec fn _verus_external_fn_specification_58__60__32_AtomicU16_32__62__32__58__58__32_fetch__add( atomic: &AtomicU16, val: u16, order: Ordering, ) -> u16

pub unsafe exec fn _verus_external_fn_specification_59__60__32_AtomicU16_32__62__32__58__58__32_fetch__sub( atomic: &AtomicU16, val: u16, order: Ordering, ) -> u16

Struct VstdSpecsForRustStdLib

pub unsafe exec fn _verus_external_fn_specification_060323832__39_a_32__91_T_59__32_N_93__32_as_32_core_325858__32_iter_325858__32_IntoIterator_3262325858__32_into__iter<'a, T, const N: usize>( s: &'a [T; N], ) -> iter : Iter<'a, T>

pub unsafe exec fn _verus_external_fn_specification_16032__91_T_59__32_N_93326232585832_as__slice<T, const N: usize>( ar: &[T; N], ) -> out : &[T]

pub unsafe exec fn _verus_external_fn_specification_26032_f32_32_as_32_Clone_3262325858__32_clone( f: &f32, ) -> res : f32

pub unsafe exec fn _verus_external_fn_specification_36032_f64_32_as_32_Clone_3262325858__32_clone( f: &f64, ) -> res : f64

pub unsafe exec fn _verus_external_fn_specification_4_core_325858__32_mem_325858__32_size__of_3258583260__32_V_32__62_<V>() -> u : usize

pub unsafe exec fn _verus_external_fn_specification_5_core_325858__32_mem_325858__32_align__of_3258583260__32_V_32__62_<V>() -> u : usize

pub unsafe exec fn _verus_external_fn_specification_6_core_325858__32_mem_325858__32_sizeofval_3258583260__32_V_32__62_<V: ?Sized>( val: &V, ) -> u : usize

pub unsafe exec fn _verus_external_fn_specification_7_core_325858__32_mem_325858__32_alignofval_3258583260__32_V_32__62_<V: ?Sized>( val: &V, ) -> u : usize

pub unsafe exec fn _verus_external_fn_specification_115560324232_mut_32_T_3262325858__32_addr<T: PointeeSized>( p: *mut T, ) -> addr : usize

pub unsafe exec fn _verus_external_fn_specification_115660324232_mut_32_T_3262325858__32_with__addr<T: PointeeSized>( p: mut T, addr: usize, ) -> q : mut T

pub unsafe exec fn _verus_external_fn_specification_115360324232_const_32_T_3262325858__32_addr<T: PointeeSized>( p: *const T, ) -> addr : usize

pub unsafe exec fn _verus_external_fn_specification_115460324232_const_32_T_3262325858__32_with__addr<T: PointeeSized>( p: const T, addr: usize, ) -> q : const T

pub unsafe exec fn _verus_external_fn_specification_860324232_mut_32_T_32_as_32_PartialEq_3260324232_mut_32_T_32623262325858__32_eq<T: PointeeSized>( x: &mut T, y: &mut T, ) -> res : bool

pub unsafe exec fn _verus_external_fn_specification_960324232_const_32_T_32_as_32_PartialEq_3260324232_const_32_T_32623262325858__32_eq<T: PointeeSized>( x: &const T, y: &const T, ) -> res : bool

pub unsafe exec fn _verus_external_fn_specification_10_core_325858__32_ptr_325858__32_null<T: PointeeSized + Pointee<Metadata = ()>>() -> res : *const T

pub unsafe exec fn _verus_external_fn_specification_11_core_325858__32_ptr_325858__32_null__mut<T: PointeeSized + Pointee<Metadata = ()>>() -> res : *mut T

pub unsafe exec fn _verus_external_fn_specification_126032__91_T_93326232585832_len<T>( slice: &[T], ) -> len : usize

pub unsafe exec fn _verus_external_fn_specification_136032__91_T_93326232585832_is__empty<T>( slice: &[T], ) -> b : bool

pub unsafe exec fn _verus_external_fn_specification_146032__91_T_93326232585832_get_3258583260__32_I_32__62_<T, I>( slice: &[T], i: I, ) -> b : Option<&<I as SliceIndex<[T]>>::Output>
where I: SliceIndex<[T]>,

pub unsafe exec fn _verus_external_fn_specification_15_str_325858__32_is__ascii( s: &str, ) -> b : bool

pub unsafe exec fn _verus_external_fn_specification_16_str_325858__32_to__owned( s: &str, ) -> res : String

pub unsafe exec fn _verus_external_fn_specification_17_str_325858__32_as__bytes( s: &str, ) -> b : &[u8] ⓘ

pub unsafe exec fn _verus_external_fn_specification_18_str_325858__32_len( s: &str, ) -> usize

pub unsafe exec fn _verus_external_fn_specification_19_str_325858__32_is__empty( s: &str, ) -> bool

pub unsafe exec fn _verus_external_fn_specification_20_str_325858__32_ischarboundary( s: &str, index: usize, ) -> bool

pub unsafe exec fn _verus_external_fn_specification_21_str_325858__32_split__at( s: &str, mid: usize, ) -> res : (&str, &str)

pub unsafe exec fn _verus_external_fn_specification_22_str_325858__32_fromutf8unchecked( v: &[u8], ) -> res : &str

pub unsafe exec fn _verus_external_fn_specification_236032_T_32_as_32_ToString_3262325858__32_to__string<T: Display + ?Sized>( t: &T, ) -> res : String

pub unsafe exec fn _verus_external_fn_specification_24_String_325858__32_as__str<'a>( s: &'a String, ) -> res : &'a str

pub unsafe exec fn _verus_external_fn_specification_256032_String_32_as_32_core_325858__32_ops_325858__32_Deref_3262325858__32_deref<'a>( s: &'a String, ) -> res : &'a str

pub unsafe exec fn _verus_external_fn_specification_266032_String_32_as_32_Clone_3262325858__32_clone( s: &String, ) -> res : String

pub unsafe exec fn _verus_external_fn_specification_276032_String_32_as_32_PartialEq_3262325858__32_eq( s: &String, other: &String, ) -> res : bool

pub unsafe exec fn _verus_external_fn_specification_28_String_325858__32_new() -> res : String

pub unsafe exec fn _verus_external_fn_specification_296032_String_32_as_32_core_325858__32_default_325858__32_Default_3262325858__32_default() -> r : String

pub unsafe exec fn _verus_external_fn_specification_30_str_325858__32_chars( s: &str, ) -> iter : Chars<'_>

pub unsafe exec fn _verus_external_fn_specification_31_alloc_325858__32_boxed_325858__32_boxassumeinitintovec__unsafe<T, const N: usize>( vals: Box<MaybeUninit<[T; N]>>, ) -> result : Vec<T>

pub unsafe exec fn _verus_external_fn_specification_32_alloc_325858__32_intrinsics_325858__32_writeboxvia__move<T>( _0: Box<MaybeUninit<T>>, v: T, ) -> result : Box<MaybeUninit<T>>

pub unsafe exec fn _verus_external_fn_specification_33_alloc_325858__32_boxed_325858__32_Box_3258583260__32_T_3262325858__32_new__uninit<T>() -> Box<MaybeUninit<T>>

pub unsafe exec fn _verus_external_fn_specification_346032_AtomicU8_3262325858__32_new( v: u8, ) -> AtomicU8

pub unsafe exec fn _verus_external_fn_specification_356032_AtomicU8_3262325858__32_compare__exchange( atomic: &AtomicU8, current: u8, new: u8, success: Ordering, failure: Ordering, ) -> Result<u8, u8>

pub unsafe exec fn _verus_external_fn_specification_366032_AtomicU8_3262325858__32_compareexchangeweak( atomic: &AtomicU8, current: u8, new: u8, success: Ordering, failure: Ordering, ) -> Result<u8, u8>

pub unsafe exec fn _verus_external_fn_specification_376032_AtomicU8_3262325858__32_fetch__and( atomic: &AtomicU8, val: u8, order: Ordering, ) -> u8

pub unsafe exec fn _verus_external_fn_specification_386032_AtomicU8_3262325858__32_fetch__nand( atomic: &AtomicU8, val: u8, order: Ordering, ) -> u8

pub unsafe exec fn _verus_external_fn_specification_396032_AtomicU8_3262325858__32_fetch__or( atomic: &AtomicU8, val: u8, order: Ordering, ) -> u8

pub unsafe exec fn _verus_external_fn_specification_406032_AtomicU8_3262325858__32_fetch__xor( atomic: &AtomicU8, val: u8, order: Ordering, ) -> u8

pub unsafe exec fn _verus_external_fn_specification_416032_AtomicU8_3262325858__32_load( atomic: &AtomicU8, order: Ordering, ) -> u8

pub unsafe exec fn _verus_external_fn_specification_426032_AtomicU8_3262325858__32_store( atomic: &AtomicU8, val: u8, order: Ordering, )

pub unsafe exec fn _verus_external_fn_specification_436032_AtomicU8_3262325858__32_swap( atomic: &AtomicU8, val: u8, order: Ordering, ) -> u8

pub unsafe exec fn _verus_external_fn_specification_446032_AtomicU8_3262325858__32_fetch__add( atomic: &AtomicU8, val: u8, order: Ordering, ) -> u8

pub unsafe exec fn _verus_external_fn_specification_456032_AtomicU8_3262325858__32_fetch__sub( atomic: &AtomicU8, val: u8, order: Ordering, ) -> u8

pub unsafe exec fn _verus_external_fn_specification_466032_AtomicU8_3262325858__32_fetch__min( atomic: &AtomicU8, val: u8, order: Ordering, ) -> u8

pub unsafe exec fn _verus_external_fn_specification_476032_AtomicU8_3262325858__32_fetch__max( atomic: &AtomicU8, val: u8, order: Ordering, ) -> u8

pub unsafe exec fn _verus_external_fn_specification_486032_AtomicU16_3262325858__32_new( v: u16, ) -> AtomicU16

pub unsafe exec fn _verus_external_fn_specification_496032_AtomicU16_3262325858__32_compare__exchange( atomic: &AtomicU16, current: u16, new: u16, success: Ordering, failure: Ordering, ) -> Result<u16, u16>

pub unsafe exec fn _verus_external_fn_specification_506032_AtomicU16_3262325858__32_compareexchangeweak( atomic: &AtomicU16, current: u16, new: u16, success: Ordering, failure: Ordering, ) -> Result<u16, u16>

pub unsafe exec fn _verus_external_fn_specification_516032_AtomicU16_3262325858__32_fetch__and( atomic: &AtomicU16, val: u16, order: Ordering, ) -> u16

pub unsafe exec fn _verus_external_fn_specification_526032_AtomicU16_3262325858__32_fetch__nand( atomic: &AtomicU16, val: u16, order: Ordering, ) -> u16

pub unsafe exec fn _verus_external_fn_specification_536032_AtomicU16_3262325858__32_fetch__or( atomic: &AtomicU16, val: u16, order: Ordering, ) -> u16

pub unsafe exec fn _verus_external_fn_specification_546032_AtomicU16_3262325858__32_fetch__xor( atomic: &AtomicU16, val: u16, order: Ordering, ) -> u16

pub unsafe exec fn _verus_external_fn_specification_556032_AtomicU16_3262325858__32_load( atomic: &AtomicU16, order: Ordering, ) -> u16

pub unsafe exec fn _verus_external_fn_specification_566032_AtomicU16_3262325858__32_store( atomic: &AtomicU16, val: u16, order: Ordering, )

pub unsafe exec fn _verus_external_fn_specification_576032_AtomicU16_3262325858__32_swap( atomic: &AtomicU16, val: u16, order: Ordering, ) -> u16

pub unsafe exec fn _verus_external_fn_specification_586032_AtomicU16_3262325858__32_fetch__add( atomic: &AtomicU16, val: u16, order: Ordering, ) -> u16

pub unsafe exec fn _verus_external_fn_specification_596032_AtomicU16_3262325858__32_fetch__sub( atomic: &AtomicU16, val: u16, order: Ordering, ) -> u16

pub unsafe exec fn _verus_external_fn_specification_606032_AtomicU16_3262325858__32_fetch__min( atomic: &AtomicU16, val: u16, order: Ordering, ) -> u16

pub unsafe exec fn _verus_external_fn_specification_616032_AtomicU16_3262325858__32_fetch__max( atomic: &AtomicU16, val: u16, order: Ordering, ) -> u16

pub unsafe exec fn _verus_external_fn_specification_626032_AtomicU32_3262325858__32_new( v: u32, ) -> AtomicU32

pub unsafe exec fn _verus_external_fn_specification_636032_AtomicU32_3262325858__32_compare__exchange( atomic: &AtomicU32, current: u32, new: u32, success: Ordering, failure: Ordering, ) -> Result<u32, u32>

pub unsafe exec fn _verus_external_fn_specification_646032_AtomicU32_3262325858__32_compareexchangeweak( atomic: &AtomicU32, current: u32, new: u32, success: Ordering, failure: Ordering, ) -> Result<u32, u32>

pub unsafe exec fn _verus_external_fn_specification_656032_AtomicU32_3262325858__32_fetch__and( atomic: &AtomicU32, val: u32, order: Ordering, ) -> u32

pub unsafe exec fn _verus_external_fn_specification_666032_AtomicU32_3262325858__32_fetch__nand( atomic: &AtomicU32, val: u32, order: Ordering, ) -> u32

pub unsafe exec fn _verus_external_fn_specification_676032_AtomicU32_3262325858__32_fetch__or( atomic: &AtomicU32, val: u32, order: Ordering, ) -> u32

pub unsafe exec fn _verus_external_fn_specification_686032_AtomicU32_3262325858__32_fetch__xor( atomic: &AtomicU32, val: u32, order: Ordering, ) -> u32

pub unsafe exec fn _verus_external_fn_specification_696032_AtomicU32_3262325858__32_load( atomic: &AtomicU32, order: Ordering, ) -> u32

pub unsafe exec fn _verus_external_fn_specification_706032_AtomicU32_3262325858__32_store( atomic: &AtomicU32, val: u32, order: Ordering, )

pub unsafe exec fn _verus_external_fn_specification_716032_AtomicU32_3262325858__32_swap( atomic: &AtomicU32, val: u32, order: Ordering, ) -> u32

pub unsafe exec fn _verus_external_fn_specification_726032_AtomicU32_3262325858__32_fetch__add( atomic: &AtomicU32, val: u32, order: Ordering, ) -> u32

pub unsafe exec fn _verus_external_fn_specification_736032_AtomicU32_3262325858__32_fetch__sub( atomic: &AtomicU32, val: u32, order: Ordering, ) -> u32

pub unsafe exec fn _verus_external_fn_specification_746032_AtomicU32_3262325858__32_fetch__min( atomic: &AtomicU32, val: u32, order: Ordering, ) -> u32