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_101760324232_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_101860324232_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_101560324232_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_101660324232_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

pub unsafe exec fn _verus_external_fn_specification_31_Chars_32585832603239_a_3262325858__32_next<'a>( chars: &mut Chars<'a>, ) -> ret : Option<char>

ensures

next_post(old(chars), final(chars), ret),

Specification for Chars::<'a>::next

Source §

impl VstdSpecsForRustStdLib

Source

pub unsafe exec fn _verus_external_fn_specification_32_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_33_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_34_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_456032_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_466032_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_476032_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_486032_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_596032_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_606032_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_616032_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_626032_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_736032_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_746032_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_756032_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_766032_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_876032_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_886032_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_896032_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_906032_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_1016032_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_1026032_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_1036032_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_1046032_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_1156032_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_1166032_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_1176032_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_1186032_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_1296032_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_1306032_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_1316032_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_1326032_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_1436032_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_1446032_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_1456032_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_1466032_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_1576032_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_1586032_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_1596032_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_1606032_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_1716032_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_1726032_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_1736032_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_1746032_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_185_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_186_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_187_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_188_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_189_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_190_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_191_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_192_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_193_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_194_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_195_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_196_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_197_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_198_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_199_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_200_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_2016032_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_2026032_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_20360323832__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_2046032__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_2056032_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_2066032_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_2076032_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_231_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_232_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_233_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_234_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_2356032_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_2366032_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_2376032_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_2436032_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_2446032_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_2456032_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_2466032_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_2476032_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_2526032_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_351_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_352_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_353_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_354_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_3556032_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_3566032_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_3576032_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_3586032_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_3596032_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_3606032_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_3616032_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_3626032_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_3636032_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_3646032_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_3656032_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_3666032_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_3676032_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_3686032_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_3696032_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_37060324041__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_3716032_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_3726032_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_37360323832__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_3746032_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_3756032__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_3766032__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_3776032_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_378_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_379_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_3806032_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_3816032_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_382_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_383_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_384_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_385_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_386_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::Sub>::sub

Source §

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

Source §

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

Source §

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

Source §

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

Source §

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

Source §

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

Source §

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

Source §

Source §

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

Source §

impl VstdSpecsForRustStdLib

Source

pub unsafe exec fn _verus_external_fn_specification_5276032_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_5286032_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_5296032_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_5306032_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_5316032_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_5326032_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_5336032_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_5346032_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_5356032_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_5366032_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_537_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_538_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_539_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_5406032_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_541_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_5426032_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_543_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_544_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_545_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_546_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_547_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_548_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_549_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_550_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_551_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_5526032_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_553_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_5546032_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_555_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_556_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_557_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_558_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_559_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_560_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_604_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_605_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_561_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_562_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_563_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_564_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_565_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_566_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_5676032_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_568_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_5696032_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_570_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_571_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_572_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_573_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_574_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_575_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_576_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_577_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_578_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_579_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_580_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_581_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_5826032_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_583_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_584_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_585_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_586_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_587_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_588_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_589_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_590_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_591_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_592_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_593_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_594_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_595_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_596_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_597_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_598_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_599_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_600_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_601_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_602_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_603_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_6066032_u8_32_as_32_Clone_3262325858__32_clone( x: &u8, ) -> res : u8

ensures

res == x,

Source

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

ensures

res == x,

Source

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

ensures

res == x,

Source

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

ensures

res == x,

Source

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

ensures

res == x,

Source

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

ensures

res == x,

Source

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

ensures

res == x,

Source

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

ensures

res == x,

Source

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

ensures

res == x,

Source

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

ensures

res == x,

Source

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

ensures

res == x,

Source

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

ensures

res == x,

Source

pub unsafe exec fn _verus_external_fn_specification_906_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_907_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_908_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_909_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_910_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_911_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_912_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_913_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_914_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_915_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_916_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_917_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_918_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_9196032_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_9206032_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_9216032_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_929_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_930_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_931_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_9326032_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 §

impl VstdSpecsForRustStdLib

Source

pub unsafe exec fn _verus_external_fn_specification_933_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_934_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_935_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_936_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_937_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_938_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_939_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_940_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_941_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_942_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_9436032_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_9446032_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_9456032__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_9466032__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_947_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_9486032__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_94960323832__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_9506032__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_9516032__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_9546032__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 §

impl VstdSpecsForRustStdLib

Source

pub unsafe exec fn _verus_external_fn_specification_956_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_957_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_9586032_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_959_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_960_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_961_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_962_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_963_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_964_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_965_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_966_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_967_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_968_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_969_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_970_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_9716032_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_972_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_973_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_974_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_9766032_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_9776032_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_978_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_9796032_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_980_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_981_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_9826032_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_983_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_984_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_98560323832__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_986_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_987_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_988_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_9896032_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_990_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_991_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_992_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_993_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_994_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_995_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_996_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_997_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_998_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_999_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_1000_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_10016032_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_1002_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_1003_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_1004_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_10056032__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_1006_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_10076032_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_1008_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_10096032_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_1010_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_10116032_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_10126032_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_1013_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_1014_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_1017__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_1018__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_1015__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_1016__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<'_>

pub unsafe exec fn _verus_external_fn_specification_31_Chars_32__58__58__32__60__32__39_a_32__62__32__58__58__32_next<'a>( chars: &mut Chars<'a>, ) -> ret : Option<char>

impl VstdSpecsForRustStdLib

pub unsafe exec fn _verus_external_fn_specification_32_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_33_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_34_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_35__60__32_AtomicU8_32__62__32__58__58__32_new( v: u8, ) -> AtomicU8

pub unsafe exec fn _verus_external_fn_specification_36__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_37__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_38__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_39__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_40__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_41__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_42__60__32_AtomicU8_32__62__32__58__58__32_load( atomic: &AtomicU8, order: Ordering, ) -> u8

pub unsafe exec fn _verus_external_fn_specification_43__60__32_AtomicU8_32__62__32__58__58__32_store( atomic: &AtomicU8, val: u8, order: Ordering, )

pub unsafe exec fn _verus_external_fn_specification_44__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_45__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_46__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_47__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_48__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_49__60__32_AtomicU16_32__62__32__58__58__32_new( v: u16, ) -> AtomicU16

pub unsafe exec fn _verus_external_fn_specification_50__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_51__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_52__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_53__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_54__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_55__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_56__60__32_AtomicU16_32__62__32__58__58__32_load( atomic: &AtomicU16, order: Ordering, ) -> u16

pub unsafe exec fn _verus_external_fn_specification_57__60__32_AtomicU16_32__62__32__58__58__32_store( atomic: &AtomicU16, val: u16, order: Ordering, )

pub unsafe exec fn _verus_external_fn_specification_58__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_59__60__32_AtomicU16_32__62__32__58__58__32_fetch__add( 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_101760324232_mut_32_T_3262325858__32_addr<T: PointeeSized>( p: *mut T, ) -> addr : usize

pub unsafe exec fn _verus_external_fn_specification_101860324232_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_101560324232_const_32_T_3262325858__32_addr<T: PointeeSized>( p: *const T, ) -> addr : usize

pub unsafe exec fn _verus_external_fn_specification_101660324232_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_Chars_32585832603239_a_3262325858__32_next<'a>( chars: &mut Chars<'a>, ) -> ret : Option<char>

pub unsafe exec fn _verus_external_fn_specification_32_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_33_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_34_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_356032_AtomicU8_3262325858__32_new( v: u8, ) -> AtomicU8

pub unsafe exec fn _verus_external_fn_specification_366032_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_376032_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_386032_AtomicU8_3262325858__32_fetch__and( atomic: &AtomicU8, val: u8, order: Ordering, ) -> u8

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

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

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

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

pub unsafe exec fn _verus_external_fn_specification_436032_AtomicU8_3262325858__32_store( atomic: &AtomicU8, val: u8, order: Ordering, )

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

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

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

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

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

pub unsafe exec fn _verus_external_fn_specification_496032_AtomicU16_3262325858__32_new( v: u16, ) -> AtomicU16

pub unsafe exec fn _verus_external_fn_specification_506032_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_516032_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_526032_AtomicU16_3262325858__32_fetch__and( atomic: &AtomicU16, val: u16, order: Ordering, ) -> u16

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

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

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

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

pub unsafe exec fn _verus_external_fn_specification_576032_AtomicU16_3262325858__32_store( atomic: &AtomicU16, val: u16, order: Ordering, )

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

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

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

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

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

pub unsafe exec fn _verus_external_fn_specification_636032_AtomicU32_3262325858__32_new( v: u32, ) -> AtomicU32

pub unsafe exec fn _verus_external_fn_specification_646032_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_656032_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_666032_AtomicU32_3262325858__32_fetch__and( atomic: &AtomicU32, val: u32, order: Ordering, ) -> u32

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

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

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

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

pub unsafe exec fn _verus_external_fn_specification_716032_AtomicU32_3262325858__32_store( atomic: &AtomicU32, val: u32, order: Ordering, )

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

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

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