vstd::std_specs

Struct VstdSpecsForRustStdLib

Source 
pub struct VstdSpecsForRustStdLib;

Implementations§

Source§

impl VstdSpecsForRustStdLib

Source

pub unsafe exec fn _verus_external_fn_specification_0__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]

ensures
ar@ == out@,

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

Source§

impl VstdSpecsForRustStdLib

Source

pub unsafe exec fn _verus_external_fn_specification_1_core_32__58__58__32_mem_32__58__58__32_size__of_32__58__58__32__60__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_2_core_32__58__58__32_mem_32__58__58__32_align__of_32__58__58__32__60__32_V_32__62_<V>() -> u : usize

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

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

Source§

impl VstdSpecsForRustStdLib

Source

pub unsafe exec fn _verus_external_fn_specification_720__60__32__42__32_mut_32_T_32__62__32__58__58__32_addr<T: ?Sized>( p: *mut T, ) -> addr : usize

ensures
addr == spec_addr(p),

Specification for [<*mut T>::addr]

Source

pub unsafe exec fn _verus_external_fn_specification_721__60__32__42__32_mut_32_T_32__62__32__58__58__32_with__addr<T: ?Sized>( 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_718__60__32__42__32_const_32_T_32__62__32__58__58__32_addr<T: ?Sized>( p: *const T, ) -> addr : usize

ensures
addr == spec_addr(p),

Specification for [<*const T>::addr]

Source

pub unsafe exec fn _verus_external_fn_specification_719__60__32__42__32_const_32_T_32__62__32__58__58__32_with__addr<T: ?Sized>( 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_3__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: ?Sized>( 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]

Source

pub unsafe exec fn _verus_external_fn_specification_4__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: ?Sized>( 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]

Source

pub unsafe exec fn _verus_external_fn_specification_5_core_32__58__58__32_ptr_32__58__58__32_null<T: ?Sized + Pointee<Metadata = ()>>() -> res : *const T

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

Specification for core::ptr::null

Source

pub unsafe exec fn _verus_external_fn_specification_6_core_32__58__58__32_ptr_32__58__58__32_null__mut<T: ?Sized + 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_7__60__32__91_T_93__32__62__32__58__58__32_len<T>( slice: &[T], ) -> len : usize

ensures
len == spec_slice_len(slice),

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

Source

pub unsafe exec fn _verus_external_fn_specification_8__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]>,

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

Source§

impl VstdSpecsForRustStdLib

Source

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

ensures
b == str_slice_is_ascii(s),

Specification for str::is_ascii

Source

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

ensures
s@ == res@,
s.is_ascii() == res.is_ascii(),

Specification for str::to_owned

Source

pub unsafe exec fn _verus_external_fn_specification_11__60__32_T_32_as_32_ToString_32__62__32__58__58__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_12_String_32__58__58__32_is__ascii( s: &String, ) -> b : bool

ensures
b == string_is_ascii(s),

Specification for String::is_ascii

Source

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

ensures
res@ == s@,
s.is_ascii() == res.is_ascii(),

Specification for String::as_str

Source

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

ensures
res == s,

Specification for [<String as Clone>::clone]

Source

pub unsafe exec fn _verus_external_fn_specification_15__60__32_String_32_as_32_PartialEq_32__62__32__58__58__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_16_str_32__58__58__32_chars( s: &str, ) -> chars : Chars<'_>

ensures
({
    let (index, c) = chars@;
    &&& index == 0
    &&& c == s@

}),

Specification for str::chars

Source

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

ensures
({
    let (old_index, old_seq) = old(chars)@;
    match r {
        None => (
            &&& chars@ == old(chars)@
            &&& old_index >= old_seq.len()

        ),
        Some(k) => {
            let (new_index, new_seq) = chars@;
            &&& 0 <= old_index < old_seq.len()
            &&& new_seq == old_seq
            &&& new_index == old_index + 1
            &&& k == old_seq[old_index]

        }
    }
}),

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

Source§

impl VstdSpecsForRustStdLib

Source

pub unsafe exec fn _verus_external_fn_specification_18_alloc_32__58__58__32_boxed_32__58__58__32_box__new<T>( x: T, ) -> result : Box<T>

ensures
*result == x,

Specification for alloc::boxed::box_new

Source§

impl VstdSpecsForRustStdLib

Source

pub unsafe exec fn _verus_external_fn_specification_708__60__32_AtomicU8_32__62__32__58__58__32_new( v: u8, ) -> AtomicU8

Specification for AtomicU8::new

Source

pub unsafe exec fn _verus_external_fn_specification_709__60__32_AtomicU8_32__62__32__58__58__32_compare__exchange( atomic: &AtomicU8, current: u8, new: u8, success: Ordering, failure: Ordering, ) -> Result<u8, u8>

Specification for AtomicU8::compare_exchange

Source

pub unsafe exec fn _verus_external_fn_specification_710__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>

Specification for AtomicU8::compare_exchange_weak

Source

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

Specification for AtomicU8::fetch_and

Source

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

Specification for AtomicU8::fetch_nand

Source

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

Specification for AtomicU8::fetch_or

Source

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

Specification for AtomicU8::fetch_xor

Source

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

Specification for AtomicU8::load

Source

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

Specification for AtomicU8::store

Source

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

Specification for AtomicU8::swap

Source§

impl VstdSpecsForRustStdLib

Source

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

Specification for AtomicU8::fetch_add

Source

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

Specification for AtomicU8::fetch_sub

Source

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

Specification for AtomicU8::fetch_min

Source

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

Specification for AtomicU8::fetch_max

Source§

impl VstdSpecsForRustStdLib

Source

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

Specification for AtomicU16::new

Source

pub unsafe exec fn _verus_external_fn_specification_695__60__32_AtomicU16_32__62__32__58__58__32_compare__exchange( atomic: &AtomicU16, current: u16, new: u16, success: Ordering, failure: Ordering, ) -> Result<u16, u16>

Specification for AtomicU16::compare_exchange

Source

pub unsafe exec fn _verus_external_fn_specification_696__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>

Specification for AtomicU16::compare_exchange_weak

Source

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

Specification for AtomicU16::fetch_and

Source

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

Specification for AtomicU16::fetch_nand

Source

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

Specification for AtomicU16::fetch_or

Source

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

Specification for AtomicU16::fetch_xor

Source

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

Specification for AtomicU16::load

Source

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

Specification for AtomicU16::store

Source

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

Specification for AtomicU16::swap

Source§

impl VstdSpecsForRustStdLib

Source

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

Specification for AtomicU16::fetch_add

Source

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

Specification for AtomicU16::fetch_sub

Source

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

Specification for AtomicU16::fetch_min

Source

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

Specification for AtomicU16::fetch_max

Source§

impl VstdSpecsForRustStdLib

Source

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

Specification for AtomicU32::new

Source

pub unsafe exec fn _verus_external_fn_specification_681__60__32_AtomicU32_32__62__32__58__58__32_compare__exchange( atomic: &AtomicU32, current: u32, new: u32, success: Ordering, failure: Ordering, ) -> Result<u32, u32>

Specification for AtomicU32::compare_exchange

Source

pub unsafe exec fn _verus_external_fn_specification_682__60__32_AtomicU32_32__62__32__58__58__32_compare__exchange__weak( atomic: &AtomicU32, current: u32, new: u32, success: Ordering, failure: Ordering, ) -> Result<u32, u32>

Specification for AtomicU32::compare_exchange_weak

Source

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

Specification for AtomicU32::fetch_and

Source

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

Specification for AtomicU32::fetch_nand

Source

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

Specification for AtomicU32::fetch_or

Source

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

Specification for AtomicU32::fetch_xor

Source

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

Specification for AtomicU32::load

Source

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

Specification for AtomicU32::store

Source

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

Specification for AtomicU32::swap

Source§

impl VstdSpecsForRustStdLib

Source

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

Specification for AtomicU32::fetch_add

Source

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

Specification for AtomicU32::fetch_sub

Source

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

Specification for AtomicU32::fetch_min

Source

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

Specification for AtomicU32::fetch_max

Source§

impl VstdSpecsForRustStdLib

Source

pub unsafe exec fn _verus_external_fn_specification_666__60__32_AtomicU64_32__62__32__58__58__32_new( v: u64, ) -> AtomicU64

Specification for AtomicU64::new

Source

pub unsafe exec fn _verus_external_fn_specification_667__60__32_AtomicU64_32__62__32__58__58__32_compare__exchange( atomic: &AtomicU64, current: u64, new: u64, success: Ordering, failure: Ordering, ) -> Result<u64, u64>

Specification for AtomicU64::compare_exchange

Source

pub unsafe exec fn _verus_external_fn_specification_668__60__32_AtomicU64_32__62__32__58__58__32_compare__exchange__weak( atomic: &AtomicU64, current: u64, new: u64, success: Ordering, failure: Ordering, ) -> Result<u64, u64>

Specification for AtomicU64::compare_exchange_weak

Source

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

Specification for AtomicU64::fetch_and

Source

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

Specification for AtomicU64::fetch_nand

Source

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

Specification for AtomicU64::fetch_or

Source

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

Specification for AtomicU64::fetch_xor

Source

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

Specification for AtomicU64::load

Source

pub unsafe exec fn _verus_external_fn_specification_674__60__32_AtomicU64_32__62__32__58__58__32_store( atomic: &AtomicU64, val: u64, order: Ordering, )

Specification for AtomicU64::store

Source

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

Specification for AtomicU64::swap

Source§

impl VstdSpecsForRustStdLib

Source

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

Specification for AtomicU64::fetch_add

Source

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

Specification for AtomicU64::fetch_sub

Source

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

Specification for AtomicU64::fetch_min

Source

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

Specification for AtomicU64::fetch_max

Source§

impl VstdSpecsForRustStdLib

Source

pub unsafe exec fn _verus_external_fn_specification_652__60__32_AtomicUsize_32__62__32__58__58__32_new( v: usize, ) -> AtomicUsize

Specification for AtomicUsize::new

Source

pub unsafe exec fn _verus_external_fn_specification_653__60__32_AtomicUsize_32__62__32__58__58__32_compare__exchange( atomic: &AtomicUsize, current: usize, new: usize, success: Ordering, failure: Ordering, ) -> Result<usize, usize>

Specification for AtomicUsize::compare_exchange

Source

pub unsafe exec fn _verus_external_fn_specification_654__60__32_AtomicUsize_32__62__32__58__58__32_compare__exchange__weak( atomic: &AtomicUsize, current: usize, new: usize, success: Ordering, failure: Ordering, ) -> Result<usize, usize>

Specification for AtomicUsize::compare_exchange_weak

Source

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

Specification for AtomicUsize::fetch_and

Source

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

Specification for AtomicUsize::fetch_nand

Source

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

Specification for AtomicUsize::fetch_or

Source

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

Specification for AtomicUsize::fetch_xor

Source

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

Specification for AtomicUsize::load

Source

pub unsafe exec fn _verus_external_fn_specification_660__60__32_AtomicUsize_32__62__32__58__58__32_store( atomic: &AtomicUsize, val: usize, order: Ordering, )

Specification for AtomicUsize::store

Source

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

Specification for AtomicUsize::swap

Source§

impl VstdSpecsForRustStdLib

Source

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

Specification for AtomicUsize::fetch_add

Source

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

Specification for AtomicUsize::fetch_sub

Source

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

Specification for AtomicUsize::fetch_min

Source

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

Specification for AtomicUsize::fetch_max

Source§

impl VstdSpecsForRustStdLib

Source

pub unsafe exec fn _verus_external_fn_specification_638__60__32_AtomicI8_32__62__32__58__58__32_new( v: i8, ) -> AtomicI8

Specification for AtomicI8::new

Source

pub unsafe exec fn _verus_external_fn_specification_639__60__32_AtomicI8_32__62__32__58__58__32_compare__exchange( atomic: &AtomicI8, current: i8, new: i8, success: Ordering, failure: Ordering, ) -> Result<i8, i8>

Specification for AtomicI8::compare_exchange

Source

pub unsafe exec fn _verus_external_fn_specification_640__60__32_AtomicI8_32__62__32__58__58__32_compare__exchange__weak( atomic: &AtomicI8, current: i8, new: i8, success: Ordering, failure: Ordering, ) -> Result<i8, i8>

Specification for AtomicI8::compare_exchange_weak

Source

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

Specification for AtomicI8::fetch_and

Source

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

Specification for AtomicI8::fetch_nand

Source

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

Specification for AtomicI8::fetch_or

Source

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

Specification for AtomicI8::fetch_xor

Source

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

Specification for AtomicI8::load

Source

pub unsafe exec fn _verus_external_fn_specification_646__60__32_AtomicI8_32__62__32__58__58__32_store( atomic: &AtomicI8, val: i8, order: Ordering, )

Specification for AtomicI8::store

Source

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

Specification for AtomicI8::swap

Source§

impl VstdSpecsForRustStdLib

Source

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

Specification for AtomicI8::fetch_add

Source

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

Specification for AtomicI8::fetch_sub

Source

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

Specification for AtomicI8::fetch_min

Source

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

Specification for AtomicI8::fetch_max

Source§

impl VstdSpecsForRustStdLib

Source

pub unsafe exec fn _verus_external_fn_specification_624__60__32_AtomicI16_32__62__32__58__58__32_new( v: i16, ) -> AtomicI16

Specification for AtomicI16::new

Source

pub unsafe exec fn _verus_external_fn_specification_625__60__32_AtomicI16_32__62__32__58__58__32_compare__exchange( atomic: &AtomicI16, current: i16, new: i16, success: Ordering, failure: Ordering, ) -> Result<i16, i16>

Specification for AtomicI16::compare_exchange

Source

pub unsafe exec fn _verus_external_fn_specification_626__60__32_AtomicI16_32__62__32__58__58__32_compare__exchange__weak( atomic: &AtomicI16, current: i16, new: i16, success: Ordering, failure: Ordering, ) -> Result<i16, i16>

Specification for AtomicI16::compare_exchange_weak

Source

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

Specification for AtomicI16::fetch_and

Source

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

Specification for AtomicI16::fetch_nand

Source

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

Specification for AtomicI16::fetch_or

Source

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

Specification for AtomicI16::fetch_xor

Source

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

Specification for AtomicI16::load

Source

pub unsafe exec fn _verus_external_fn_specification_632__60__32_AtomicI16_32__62__32__58__58__32_store( atomic: &AtomicI16, val: i16, order: Ordering, )

Specification for AtomicI16::store

Source

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

Specification for AtomicI16::swap

Source§

impl VstdSpecsForRustStdLib

Source

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

Specification for AtomicI16::fetch_add

Source

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

Specification for AtomicI16::fetch_sub

Source

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

Specification for AtomicI16::fetch_min

Source

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

Specification for AtomicI16::fetch_max

Source§

impl VstdSpecsForRustStdLib

Source

pub unsafe exec fn _verus_external_fn_specification_610__60__32_AtomicI32_32__62__32__58__58__32_new( v: i32, ) -> AtomicI32

Specification for AtomicI32::new

Source

pub unsafe exec fn _verus_external_fn_specification_611__60__32_AtomicI32_32__62__32__58__58__32_compare__exchange( atomic: &AtomicI32, current: i32, new: i32, success: Ordering, failure: Ordering, ) -> Result<i32, i32>

Specification for AtomicI32::compare_exchange

Source

pub unsafe exec fn _verus_external_fn_specification_612__60__32_AtomicI32_32__62__32__58__58__32_compare__exchange__weak( atomic: &AtomicI32, current: i32, new: i32, success: Ordering, failure: Ordering, ) -> Result<i32, i32>

Specification for AtomicI32::compare_exchange_weak

Source

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

Specification for AtomicI32::fetch_and

Source

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

Specification for AtomicI32::fetch_nand

Source

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

Specification for AtomicI32::fetch_or

Source

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

Specification for AtomicI32::fetch_xor

Source

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

Specification for AtomicI32::load

Source

pub unsafe exec fn _verus_external_fn_specification_618__60__32_AtomicI32_32__62__32__58__58__32_store( atomic: &AtomicI32, val: i32, order: Ordering, )

Specification for AtomicI32::store

Source

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

Specification for AtomicI32::swap

Source§

impl VstdSpecsForRustStdLib

Source

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

Specification for AtomicI32::fetch_add

Source

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

Specification for AtomicI32::fetch_sub

Source

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

Specification for AtomicI32::fetch_min

Source

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

Specification for AtomicI32::fetch_max

Source§

impl VstdSpecsForRustStdLib

Source

pub unsafe exec fn _verus_external_fn_specification_596__60__32_AtomicI64_32__62__32__58__58__32_new( v: i64, ) -> AtomicI64

Specification for AtomicI64::new

Source

pub unsafe exec fn _verus_external_fn_specification_597__60__32_AtomicI64_32__62__32__58__58__32_compare__exchange( atomic: &AtomicI64, current: i64, new: i64, success: Ordering, failure: Ordering, ) -> Result<i64, i64>

Specification for AtomicI64::compare_exchange

Source

pub unsafe exec fn _verus_external_fn_specification_598__60__32_AtomicI64_32__62__32__58__58__32_compare__exchange__weak( atomic: &AtomicI64, current: i64, new: i64, success: Ordering, failure: Ordering, ) -> Result<i64, i64>

Specification for AtomicI64::compare_exchange_weak

Source

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

Specification for AtomicI64::fetch_and

Source

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

Specification for AtomicI64::fetch_nand

Source

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

Specification for AtomicI64::fetch_or

Source

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

Specification for AtomicI64::fetch_xor

Source

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

Specification for AtomicI64::load

Source

pub unsafe exec fn _verus_external_fn_specification_604__60__32_AtomicI64_32__62__32__58__58__32_store( atomic: &AtomicI64, val: i64, order: Ordering, )

Specification for AtomicI64::store

Source

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

Specification for AtomicI64::swap

Source§

impl VstdSpecsForRustStdLib

Source

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

Specification for AtomicI64::fetch_add

Source

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

Specification for AtomicI64::fetch_sub

Source

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

Specification for AtomicI64::fetch_min

Source

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

Specification for AtomicI64::fetch_max

Source§

impl VstdSpecsForRustStdLib

Source

pub unsafe exec fn _verus_external_fn_specification_582__60__32_AtomicIsize_32__62__32__58__58__32_new( v: isize, ) -> AtomicIsize

Specification for AtomicIsize::new

Source

pub unsafe exec fn _verus_external_fn_specification_583__60__32_AtomicIsize_32__62__32__58__58__32_compare__exchange( atomic: &AtomicIsize, current: isize, new: isize, success: Ordering, failure: Ordering, ) -> Result<isize, isize>

Specification for AtomicIsize::compare_exchange

Source

pub unsafe exec fn _verus_external_fn_specification_584__60__32_AtomicIsize_32__62__32__58__58__32_compare__exchange__weak( atomic: &AtomicIsize, current: isize, new: isize, success: Ordering, failure: Ordering, ) -> Result<isize, isize>

Specification for AtomicIsize::compare_exchange_weak

Source

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

Specification for AtomicIsize::fetch_and

Source

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

Specification for AtomicIsize::fetch_nand

Source

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

Specification for AtomicIsize::fetch_or

Source

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

Specification for AtomicIsize::fetch_xor

Source

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

Specification for AtomicIsize::load

Source

pub unsafe exec fn _verus_external_fn_specification_590__60__32_AtomicIsize_32__62__32__58__58__32_store( atomic: &AtomicIsize, val: isize, order: Ordering, )

Specification for AtomicIsize::store

Source

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

Specification for AtomicIsize::swap

Source§

impl VstdSpecsForRustStdLib

Source

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

Specification for AtomicIsize::fetch_add

Source

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

Specification for AtomicIsize::fetch_sub

Source

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

Specification for AtomicIsize::fetch_min

Source

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

Specification for AtomicIsize::fetch_max

Source§

impl VstdSpecsForRustStdLib

Source

pub unsafe exec fn _verus_external_fn_specification_568__60__32_AtomicBool_32__62__32__58__58__32_new( v: bool, ) -> AtomicBool

Specification for AtomicBool::new

Source

pub unsafe exec fn _verus_external_fn_specification_569__60__32_AtomicBool_32__62__32__58__58__32_compare__exchange( atomic: &AtomicBool, current: bool, new: bool, success: Ordering, failure: Ordering, ) -> Result<bool, bool>

Specification for AtomicBool::compare_exchange

Source

pub unsafe exec fn _verus_external_fn_specification_570__60__32_AtomicBool_32__62__32__58__58__32_compare__exchange__weak( atomic: &AtomicBool, current: bool, new: bool, success: Ordering, failure: Ordering, ) -> Result<bool, bool>

Specification for AtomicBool::compare_exchange_weak

Source

pub unsafe exec fn _verus_external_fn_specification_571__60__32_AtomicBool_32__62__32__58__58__32_fetch__and( atomic: &AtomicBool, val: bool, order: Ordering, ) -> bool

Specification for AtomicBool::fetch_and

Source

pub unsafe exec fn _verus_external_fn_specification_572__60__32_AtomicBool_32__62__32__58__58__32_fetch__nand( atomic: &AtomicBool, val: bool, order: Ordering, ) -> bool

Specification for AtomicBool::fetch_nand

Source

pub unsafe exec fn _verus_external_fn_specification_573__60__32_AtomicBool_32__62__32__58__58__32_fetch__or( atomic: &AtomicBool, val: bool, order: Ordering, ) -> bool

Specification for AtomicBool::fetch_or

Source

pub unsafe exec fn _verus_external_fn_specification_574__60__32_AtomicBool_32__62__32__58__58__32_fetch__xor( atomic: &AtomicBool, val: bool, order: Ordering, ) -> bool

Specification for AtomicBool::fetch_xor

Source

pub unsafe exec fn _verus_external_fn_specification_575__60__32_AtomicBool_32__62__32__58__58__32_load( atomic: &AtomicBool, order: Ordering, ) -> bool

Specification for AtomicBool::load

Source

pub unsafe exec fn _verus_external_fn_specification_576__60__32_AtomicBool_32__62__32__58__58__32_store( atomic: &AtomicBool, val: bool, order: Ordering, )

Specification for AtomicBool::store

Source

pub unsafe exec fn _verus_external_fn_specification_577__60__32_AtomicBool_32__62__32__58__58__32_swap( atomic: &AtomicBool, val: bool, order: Ordering, ) -> bool

Specification for AtomicBool::swap

Source§

impl VstdSpecsForRustStdLib

Source

pub unsafe exec fn _verus_external_fn_specification_19_u8_32__58__58__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_20_u8_32__58__58__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_21_u8_32__58__58__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_22_u8_32__58__58__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_23_u16_32__58__58__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_24_u16_32__58__58__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_25_u16_32__58__58__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_26_u16_32__58__58__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_27_u32_32__58__58__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_28_u32_32__58__58__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_29_u32_32__58__58__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_30_u32_32__58__58__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_31_u64_32__58__58__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_32_u64_32__58__58__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_33_u64_32__58__58__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_34_u64_32__58__58__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_35__60__32_bool_32_as_32_Clone_32__62__32__58__58__32_clone( b: &bool, ) -> res : bool

Specification for [<bool as Clone>::clone]

Source

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

Specification for [<char as Clone>::clone]

Source

pub unsafe exec fn _verus_external_fn_specification_37__60__32__38__32__39_b_32_T_32_as_32_Clone_32__62__32__58__58__32_clone<'b, 'a, T: ?Sized>( 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_38__60__32_Tracked_32__60__32_T_32__62__32_as_32_Clone_32__62__32__58__58__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_39__60__32_Ghost_32__60__32_T_32__62__32_as_32_Clone_32__62__32__58__58__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_40__60__32_bool_32_as_32_PartialEq_32__60__32_bool_32__62__32__62__32__58__58__32_eq( x: &bool, y: &bool, ) -> bool

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

Source

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

Specification for [<bool as PartialEq<bool>>::ne]

Source

pub unsafe exec fn _verus_external_fn_specification_42__60__32_f32_32_as_32_PartialEq_32__60__32_f32_32__62__32__62__32__58__58__32_eq( x: &f32, y: &f32, ) -> o : bool

ensures
eq_ensures::<f32>(*x, *y, o),

Specification for [<f32 as PartialEq<f32>>::eq]

Source

pub unsafe exec fn _verus_external_fn_specification_43__60__32_f32_32_as_32_PartialEq_32__60__32_f32_32__62__32__62__32__58__58__32_ne( x: &f32, y: &f32, ) -> o : bool

ensures
ne_ensures::<f32>(*x, *y, o),

Specification for [<f32 as PartialEq<f32>>::ne]

Source

pub unsafe exec fn _verus_external_fn_specification_44__60__32_f32_32_as_32_PartialOrd_32__60__32_f32_32__62__32__62__32__58__58__32_partial__cmp( x: &f32, y: &f32, ) -> o : Option<Ordering>

ensures
partial_cmp_ensures::<f32>(*x, *y, o),

Specification for [<f32 as PartialOrd<f32>>::partial_cmp]

Source

pub unsafe exec fn _verus_external_fn_specification_45__60__32_f32_32_as_32_PartialOrd_32__60__32_f32_32__62__32__62__32__58__58__32_lt( x: &f32, y: &f32, ) -> o : bool

ensures
lt_ensures::<f32>(*x, *y, o),

Specification for [<f32 as PartialOrd<f32>>::lt]

Source

pub unsafe exec fn _verus_external_fn_specification_46__60__32_f32_32_as_32_PartialOrd_32__60__32_f32_32__62__32__62__32__58__58__32_le( x: &f32, y: &f32, ) -> o : bool

ensures
le_ensures::<f32>(*x, *y, o),

Specification for [<f32 as PartialOrd<f32>>::le]

Source

pub unsafe exec fn _verus_external_fn_specification_47__60__32_f32_32_as_32_PartialOrd_32__60__32_f32_32__62__32__62__32__58__58__32_gt( x: &f32, y: &f32, ) -> o : bool

ensures
gt_ensures::<f32>(*x, *y, o),

Specification for [<f32 as PartialOrd<f32>>::gt]

Source

pub unsafe exec fn _verus_external_fn_specification_48__60__32_f32_32_as_32_PartialOrd_32__60__32_f32_32__62__32__62__32__58__58__32_ge( x: &f32, y: &f32, ) -> o : bool

ensures
ge_ensures::<f32>(*x, *y, o),

Specification for [<f32 as PartialOrd<f32>>::ge]

Source

pub unsafe exec fn _verus_external_fn_specification_49__60__32_f64_32_as_32_PartialEq_32__60__32_f64_32__62__32__62__32__58__58__32_eq( x: &f64, y: &f64, ) -> o : bool

ensures
eq_ensures::<f64>(*x, *y, o),

Specification for [<f64 as PartialEq<f64>>::eq]

Source

pub unsafe exec fn _verus_external_fn_specification_50__60__32_f64_32_as_32_PartialEq_32__60__32_f64_32__62__32__62__32__58__58__32_ne( x: &f64, y: &f64, ) -> o : bool

ensures
ne_ensures::<f64>(*x, *y, o),

Specification for [<f64 as PartialEq<f64>>::ne]

Source

pub unsafe exec fn _verus_external_fn_specification_51__60__32_f64_32_as_32_PartialOrd_32__60__32_f64_32__62__32__62__32__58__58__32_partial__cmp( x: &f64, y: &f64, ) -> o : Option<Ordering>

ensures
partial_cmp_ensures::<f64>(*x, *y, o),

Specification for [<f64 as PartialOrd<f64>>::partial_cmp]

Source

pub unsafe exec fn _verus_external_fn_specification_52__60__32_f64_32_as_32_PartialOrd_32__60__32_f64_32__62__32__62__32__58__58__32_lt( x: &f64, y: &f64, ) -> o : bool

ensures
lt_ensures::<f64>(*x, *y, o),

Specification for [<f64 as PartialOrd<f64>>::lt]

Source

pub unsafe exec fn _verus_external_fn_specification_53__60__32_f64_32_as_32_PartialOrd_32__60__32_f64_32__62__32__62__32__58__58__32_le( x: &f64, y: &f64, ) -> o : bool

ensures
le_ensures::<f64>(*x, *y, o),

Specification for [<f64 as PartialOrd<f64>>::le]

Source

pub unsafe exec fn _verus_external_fn_specification_54__60__32_f64_32_as_32_PartialOrd_32__60__32_f64_32__62__32__62__32__58__58__32_gt( x: &f64, y: &f64, ) -> o : bool

ensures
gt_ensures::<f64>(*x, *y, o),

Specification for [<f64 as PartialOrd<f64>>::gt]

Source

pub unsafe exec fn _verus_external_fn_specification_55__60__32_f64_32_as_32_PartialOrd_32__60__32_f64_32__62__32__62__32__58__58__32_ge( x: &f64, y: &f64, ) -> o : bool

ensures
ge_ensures::<f64>(*x, *y, o),

Specification for [<f64 as PartialOrd<f64>>::ge]

Source§

impl VstdSpecsForRustStdLib

Source

pub unsafe exec fn _verus_external_fn_specification_56_Result_32__58__58__32__60__32_T_44__32_E_32__62__32__58__58__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_57_Option_32__58__58__32__60__32_T_32__62__32__58__58__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_58_Option_32__58__58__32__60__32_T_32__62__32__58__58__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_59_Result_32__58__58__32__60__32_T_44__32_F_32__62__32__58__58__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_60_T_32__58__58__32_into<T, U: From<T>>( a: T, ) -> ret : U

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

Specification for [T::into]

Source

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

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

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

Source

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

ensures
r == i,

Specification for [I::into_iter]

Source

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

ensures
c == b,

Specification for core::intrinsics::likely

Source

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

ensures
c == b,

Specification for core::intrinsics::unlikely

Source

pub unsafe exec fn _verus_external_fn_specification_65_bool_32__58__58__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_66__60__32_u16_32_as_32_core_32__58__58__32_convert_32__58__58__32_From_32__60__32_u8_32__62__32__62__32__58__58__32_from( a: u8, ) -> ret : u16

ensures
ret == a as u16,

Specification for [<u16 as core::convert::From<u8>>::from]

Source

pub unsafe exec fn _verus_external_fn_specification_67__60__32_u32_32_as_32_core_32__58__58__32_convert_32__58__58__32_From_32__60__32_u8_32__62__32__62__32__58__58__32_from( a: u8, ) -> ret : u32

ensures
ret == a as u32,

Specification for [<u32 as core::convert::From<u8>>::from]

Source

pub unsafe exec fn _verus_external_fn_specification_68__60__32_u64_32_as_32_core_32__58__58__32_convert_32__58__58__32_From_32__60__32_u8_32__62__32__62__32__58__58__32_from( a: u8, ) -> ret : u64

ensures
ret == a as u64,

Specification for [<u64 as core::convert::From<u8>>::from]

Source

pub unsafe exec fn _verus_external_fn_specification_69__60__32_usize_32_as_32_core_32__58__58__32_convert_32__58__58__32_From_32__60__32_u8_32__62__32__62__32__58__58__32_from( a: u8, ) -> ret : usize

ensures
ret == a as usize,

Specification for [<usize as core::convert::From<u8>>::from]

Source

pub unsafe exec fn _verus_external_fn_specification_70__60__32_u128_32_as_32_core_32__58__58__32_convert_32__58__58__32_From_32__60__32_u8_32__62__32__62__32__58__58__32_from( a: u8, ) -> ret : u128

ensures
ret == a as u128,

Specification for [<u128 as core::convert::From<u8>>::from]

Source§

impl VstdSpecsForRustStdLib

Source

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

ensures
ret == a as u32,

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

Source

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

ensures
ret == a as u64,

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

Source

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

ensures
ret == a as usize,

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

Source

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

ensures
ret == a as u128,

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

Source§

impl VstdSpecsForRustStdLib

Source

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

ensures
ret == a as u64,

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

Source

pub unsafe exec fn _verus_external_fn_specification_76__60__32_u128_32_as_32_core_32__58__58__32_convert_32__58__58__32_From_32__60__32_u32_32__62__32__62__32__58__58__32_from( a: u32, ) -> ret : u128

ensures
ret == a as u128,

Specification for [<u128 as core::convert::From<u32>>::from]

Source§

impl VstdSpecsForRustStdLib

Source

pub unsafe exec fn _verus_external_fn_specification_77__60__32_u128_32_as_32_core_32__58__58__32_convert_32__58__58__32_From_32__60__32_u64_32__62__32__62__32__58__58__32_from( a: u64, ) -> ret : u128

ensures
ret == a as u128,

Specification for [<u128 as core::convert::From<u64>>::from]

Source§

impl VstdSpecsForRustStdLib

Source

pub unsafe exec fn _verus_external_fn_specification_78__60__32_isize_32_as_32_core_32__58__58__32_ops_32__58__58__32_Neg_32__62__32__58__58__32_neg( x: isize, ) -> isize

Specification for [<isize as core::ops::Neg>::neg]

Source

pub unsafe exec fn _verus_external_fn_specification_79__60__32_i8_32_as_32_core_32__58__58__32_ops_32__58__58__32_Neg_32__62__32__58__58__32_neg( x: i8, ) -> i8

Specification for [<i8 as core::ops::Neg>::neg]

Source

pub unsafe exec fn _verus_external_fn_specification_80__60__32_i16_32_as_32_core_32__58__58__32_ops_32__58__58__32_Neg_32__62__32__58__58__32_neg( x: i16, ) -> i16

Specification for [<i16 as core::ops::Neg>::neg]

Source

pub unsafe exec fn _verus_external_fn_specification_81__60__32_i32_32_as_32_core_32__58__58__32_ops_32__58__58__32_Neg_32__62__32__58__58__32_neg( x: i32, ) -> i32

Specification for [<i32 as core::ops::Neg>::neg]

Source

pub unsafe exec fn _verus_external_fn_specification_82__60__32_i64_32_as_32_core_32__58__58__32_ops_32__58__58__32_Neg_32__62__32__58__58__32_neg( x: i64, ) -> i64

Specification for [<i64 as core::ops::Neg>::neg]

Source

pub unsafe exec fn _verus_external_fn_specification_83__60__32_i128_32_as_32_core_32__58__58__32_ops_32__58__58__32_Neg_32__62__32__58__58__32_neg( x: i128, ) -> i128

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

Source§

impl VstdSpecsForRustStdLib

Source

pub unsafe exec fn _verus_external_fn_specification_84__60__32_bool_32_as_32_core_32__58__58__32_ops_32__58__58__32_Not_32__62__32__58__58__32_not( x: bool, ) -> bool

Specification for [<bool as core::ops::Not>::not]

Source

pub unsafe exec fn _verus_external_fn_specification_85__60__32_usize_32_as_32_core_32__58__58__32_ops_32__58__58__32_Not_32__62__32__58__58__32_not( x: usize, ) -> usize

Specification for [<usize as core::ops::Not>::not]

Source

pub unsafe exec fn _verus_external_fn_specification_86__60__32_u8_32_as_32_core_32__58__58__32_ops_32__58__58__32_Not_32__62__32__58__58__32_not( x: u8, ) -> u8

Specification for [<u8 as core::ops::Not>::not]

Source

pub unsafe exec fn _verus_external_fn_specification_87__60__32_u16_32_as_32_core_32__58__58__32_ops_32__58__58__32_Not_32__62__32__58__58__32_not( x: u16, ) -> u16

Specification for [<u16 as core::ops::Not>::not]

Source

pub unsafe exec fn _verus_external_fn_specification_88__60__32_u32_32_as_32_core_32__58__58__32_ops_32__58__58__32_Not_32__62__32__58__58__32_not( x: u32, ) -> u32

Specification for [<u32 as core::ops::Not>::not]

Source

pub unsafe exec fn _verus_external_fn_specification_89__60__32_u64_32_as_32_core_32__58__58__32_ops_32__58__58__32_Not_32__62__32__58__58__32_not( x: u64, ) -> u64

Specification for [<u64 as core::ops::Not>::not]

Source

pub unsafe exec fn _verus_external_fn_specification_90__60__32_u128_32_as_32_core_32__58__58__32_ops_32__58__58__32_Not_32__62__32__58__58__32_not( x: u128, ) -> u128

Specification for [<u128 as core::ops::Not>::not]

Source

pub unsafe exec fn _verus_external_fn_specification_91__60__32_isize_32_as_32_core_32__58__58__32_ops_32__58__58__32_Not_32__62__32__58__58__32_not( x: isize, ) -> isize

Specification for [<isize as core::ops::Not>::not]

Source

pub unsafe exec fn _verus_external_fn_specification_92__60__32_i8_32_as_32_core_32__58__58__32_ops_32__58__58__32_Not_32__62__32__58__58__32_not( x: i8, ) -> i8

Specification for [<i8 as core::ops::Not>::not]

Source

pub unsafe exec fn _verus_external_fn_specification_93__60__32_i16_32_as_32_core_32__58__58__32_ops_32__58__58__32_Not_32__62__32__58__58__32_not( x: i16, ) -> i16

Specification for [<i16 as core::ops::Not>::not]

Source

pub unsafe exec fn _verus_external_fn_specification_94__60__32_i32_32_as_32_core_32__58__58__32_ops_32__58__58__32_Not_32__62__32__58__58__32_not( x: i32, ) -> i32

Specification for [<i32 as core::ops::Not>::not]

Source

pub unsafe exec fn _verus_external_fn_specification_95__60__32_i64_32_as_32_core_32__58__58__32_ops_32__58__58__32_Not_32__62__32__58__58__32_not( x: i64, ) -> i64

Specification for [<i64 as core::ops::Not>::not]

Source

pub unsafe exec fn _verus_external_fn_specification_96__60__32_i128_32_as_32_core_32__58__58__32_ops_32__58__58__32_Not_32__62__32__58__58__32_not( x: i128, ) -> i128

Specification for [<i128 as core::ops::Not>::not]

Source§

impl VstdSpecsForRustStdLib

Source

pub unsafe exec fn _verus_external_fn_specification_97__60__32_usize_32_as_32_core_32__58__58__32_ops_32__58__58__32_Add_32__62__32__58__58__32_add( x: usize, y: usize, ) -> usize

Specification for [<usize as core::ops::Add>::add]

Source

pub unsafe exec fn _verus_external_fn_specification_98__60__32_u8_32_as_32_core_32__58__58__32_ops_32__58__58__32_Add_32__62__32__58__58__32_add( x: u8, y: u8, ) -> u8

Specification for [<u8 as core::ops::Add>::add]

Source

pub unsafe exec fn _verus_external_fn_specification_99__60__32_u16_32_as_32_core_32__58__58__32_ops_32__58__58__32_Add_32__62__32__58__58__32_add( x: u16, y: u16, ) -> u16

Specification for [<u16 as core::ops::Add>::add]

Source

pub unsafe exec fn _verus_external_fn_specification_100__60__32_u32_32_as_32_core_32__58__58__32_ops_32__58__58__32_Add_32__62__32__58__58__32_add( x: u32, y: u32, ) -> u32

Specification for [<u32 as core::ops::Add>::add]

Source

pub unsafe exec fn _verus_external_fn_specification_101__60__32_u64_32_as_32_core_32__58__58__32_ops_32__58__58__32_Add_32__62__32__58__58__32_add( x: u64, y: u64, ) -> u64

Specification for [<u64 as core::ops::Add>::add]

Source

pub unsafe exec fn _verus_external_fn_specification_102__60__32_u128_32_as_32_core_32__58__58__32_ops_32__58__58__32_Add_32__62__32__58__58__32_add( x: u128, y: u128, ) -> u128

Specification for [<u128 as core::ops::Add>::add]

Source

pub unsafe exec fn _verus_external_fn_specification_103__60__32_isize_32_as_32_core_32__58__58__32_ops_32__58__58__32_Add_32__62__32__58__58__32_add( x: isize, y: isize, ) -> isize

Specification for [<isize as core::ops::Add>::add]

Source

pub unsafe exec fn _verus_external_fn_specification_104__60__32_i8_32_as_32_core_32__58__58__32_ops_32__58__58__32_Add_32__62__32__58__58__32_add( x: i8, y: i8, ) -> i8

Specification for [<i8 as core::ops::Add>::add]

Source

pub unsafe exec fn _verus_external_fn_specification_105__60__32_i16_32_as_32_core_32__58__58__32_ops_32__58__58__32_Add_32__62__32__58__58__32_add( x: i16, y: i16, ) -> i16

Specification for [<i16 as core::ops::Add>::add]

Source

pub unsafe exec fn _verus_external_fn_specification_106__60__32_i32_32_as_32_core_32__58__58__32_ops_32__58__58__32_Add_32__62__32__58__58__32_add( x: i32, y: i32, ) -> i32

Specification for [<i32 as core::ops::Add>::add]

Source

pub unsafe exec fn _verus_external_fn_specification_107__60__32_i64_32_as_32_core_32__58__58__32_ops_32__58__58__32_Add_32__62__32__58__58__32_add( x: i64, y: i64, ) -> i64

Specification for [<i64 as core::ops::Add>::add]

Source

pub unsafe exec fn _verus_external_fn_specification_108__60__32_i128_32_as_32_core_32__58__58__32_ops_32__58__58__32_Add_32__62__32__58__58__32_add( x: i128, y: i128, ) -> i128

Specification for [<i128 as core::ops::Add>::add]

Source§

impl VstdSpecsForRustStdLib

Source

pub unsafe exec fn _verus_external_fn_specification_109__60__32_usize_32_as_32_core_32__58__58__32_ops_32__58__58__32_Sub_32__62__32__58__58__32_sub( x: usize, y: usize, ) -> usize

Specification for [<usize as core::ops::Sub>::sub]

Source

pub unsafe exec fn _verus_external_fn_specification_110__60__32_u8_32_as_32_core_32__58__58__32_ops_32__58__58__32_Sub_32__62__32__58__58__32_sub( x: u8, y: u8, ) -> u8

Specification for [<u8 as core::ops::Sub>::sub]

Source

pub unsafe exec fn _verus_external_fn_specification_111__60__32_u16_32_as_32_core_32__58__58__32_ops_32__58__58__32_Sub_32__62__32__58__58__32_sub( x: u16, y: u16, ) -> u16

Specification for [<u16 as core::ops::Sub>::sub]

Source

pub unsafe exec fn _verus_external_fn_specification_112__60__32_u32_32_as_32_core_32__58__58__32_ops_32__58__58__32_Sub_32__62__32__58__58__32_sub( x: u32, y: u32, ) -> u32

Specification for [<u32 as core::ops::Sub>::sub]

Source

pub unsafe exec fn _verus_external_fn_specification_113__60__32_u64_32_as_32_core_32__58__58__32_ops_32__58__58__32_Sub_32__62__32__58__58__32_sub( x: u64, y: u64, ) -> u64

Specification for [<u64 as core::ops::Sub>::sub]

Source

pub unsafe exec fn _verus_external_fn_specification_114__60__32_u128_32_as_32_core_32__58__58__32_ops_32__58__58__32_Sub_32__62__32__58__58__32_sub( x: u128, y: u128, ) -> u128

Specification for [<u128 as core::ops::Sub>::sub]

Source

pub unsafe exec fn _verus_external_fn_specification_115__60__32_isize_32_as_32_core_32__58__58__32_ops_32__58__58__32_Sub_32__62__32__58__58__32_sub( x: isize, y: isize, ) -> isize

Specification for [<isize as core::ops::Sub>::sub]

Source

pub unsafe exec fn _verus_external_fn_specification_116__60__32_i8_32_as_32_core_32__58__58__32_ops_32__58__58__32_Sub_32__62__32__58__58__32_sub( x: i8, y: i8, ) -> i8

Specification for [<i8 as core::ops::Sub>::sub]

Source

pub unsafe exec fn _verus_external_fn_specification_117__60__32_i16_32_as_32_core_32__58__58__32_ops_32__58__58__32_Sub_32__62__32__58__58__32_sub( x: i16, y: i16, ) -> i16

Specification for [<i16 as core::ops::Sub>::sub]

Source

pub unsafe exec fn _verus_external_fn_specification_118__60__32_i32_32_as_32_core_32__58__58__32_ops_32__58__58__32_Sub_32__62__32__58__58__32_sub( x: i32, y: i32, ) -> i32

Specification for [<i32 as core::ops::Sub>::sub]

Source

pub unsafe exec fn _verus_external_fn_specification_119__60__32_i64_32_as_32_core_32__58__58__32_ops_32__58__58__32_Sub_32__62__32__58__58__32_sub( x: i64, y: i64, ) -> i64

Specification for [<i64 as core::ops::Sub>::sub]

Source

pub unsafe exec fn _verus_external_fn_specification_120__60__32_i128_32_as_32_core_32__58__58__32_ops_32__58__58__32_Sub_32__62__32__58__58__32_sub( x: i128, y: i128, ) -> i128

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

Source§

impl VstdSpecsForRustStdLib

Source

pub unsafe exec fn _verus_external_fn_specification_121__60__32_usize_32_as_32_core_32__58__58__32_ops_32__58__58__32_Mul_32__62__32__58__58__32_mul( x: usize, y: usize, ) -> usize

Specification for [<usize as core::ops::Mul>::mul]

Source

pub unsafe exec fn _verus_external_fn_specification_122__60__32_u8_32_as_32_core_32__58__58__32_ops_32__58__58__32_Mul_32__62__32__58__58__32_mul( x: u8, y: u8, ) -> u8

Specification for [<u8 as core::ops::Mul>::mul]

Source

pub unsafe exec fn _verus_external_fn_specification_123__60__32_u16_32_as_32_core_32__58__58__32_ops_32__58__58__32_Mul_32__62__32__58__58__32_mul( x: u16, y: u16, ) -> u16

Specification for [<u16 as core::ops::Mul>::mul]

Source

pub unsafe exec fn _verus_external_fn_specification_124__60__32_u32_32_as_32_core_32__58__58__32_ops_32__58__58__32_Mul_32__62__32__58__58__32_mul( x: u32, y: u32, ) -> u32

Specification for [<u32 as core::ops::Mul>::mul]

Source

pub unsafe exec fn _verus_external_fn_specification_125__60__32_u64_32_as_32_core_32__58__58__32_ops_32__58__58__32_Mul_32__62__32__58__58__32_mul( x: u64, y: u64, ) -> u64

Specification for [<u64 as core::ops::Mul>::mul]

Source

pub unsafe exec fn _verus_external_fn_specification_126__60__32_u128_32_as_32_core_32__58__58__32_ops_32__58__58__32_Mul_32__62__32__58__58__32_mul( x: u128, y: u128, ) -> u128

Specification for [<u128 as core::ops::Mul>::mul]

Source

pub unsafe exec fn _verus_external_fn_specification_127__60__32_isize_32_as_32_core_32__58__58__32_ops_32__58__58__32_Mul_32__62__32__58__58__32_mul( x: isize, y: isize, ) -> isize

Specification for [<isize as core::ops::Mul>::mul]

Source

pub unsafe exec fn _verus_external_fn_specification_128__60__32_i8_32_as_32_core_32__58__58__32_ops_32__58__58__32_Mul_32__62__32__58__58__32_mul( x: i8, y: i8, ) -> i8

Specification for [<i8 as core::ops::Mul>::mul]

Source

pub unsafe exec fn _verus_external_fn_specification_129__60__32_i16_32_as_32_core_32__58__58__32_ops_32__58__58__32_Mul_32__62__32__58__58__32_mul( x: i16, y: i16, ) -> i16

Specification for [<i16 as core::ops::Mul>::mul]

Source

pub unsafe exec fn _verus_external_fn_specification_130__60__32_i32_32_as_32_core_32__58__58__32_ops_32__58__58__32_Mul_32__62__32__58__58__32_mul( x: i32, y: i32, ) -> i32

Specification for [<i32 as core::ops::Mul>::mul]

Source

pub unsafe exec fn _verus_external_fn_specification_131__60__32_i64_32_as_32_core_32__58__58__32_ops_32__58__58__32_Mul_32__62__32__58__58__32_mul( x: i64, y: i64, ) -> i64

Specification for [<i64 as core::ops::Mul>::mul]

Source

pub unsafe exec fn _verus_external_fn_specification_132__60__32_i128_32_as_32_core_32__58__58__32_ops_32__58__58__32_Mul_32__62__32__58__58__32_mul( x: i128, y: i128, ) -> i128

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

Source§

impl VstdSpecsForRustStdLib

Source

pub unsafe exec fn _verus_external_fn_specification_133__60__32_usize_32_as_32_core_32__58__58__32_ops_32__58__58__32_Div_32__62__32__58__58__32_div( x: usize, y: usize, ) -> usize

Specification for [<usize as core::ops::Div>::div]

Source

pub unsafe exec fn _verus_external_fn_specification_134__60__32_u8_32_as_32_core_32__58__58__32_ops_32__58__58__32_Div_32__62__32__58__58__32_div( x: u8, y: u8, ) -> u8

Specification for [<u8 as core::ops::Div>::div]

Source

pub unsafe exec fn _verus_external_fn_specification_135__60__32_u16_32_as_32_core_32__58__58__32_ops_32__58__58__32_Div_32__62__32__58__58__32_div( x: u16, y: u16, ) -> u16

Specification for [<u16 as core::ops::Div>::div]

Source

pub unsafe exec fn _verus_external_fn_specification_136__60__32_u32_32_as_32_core_32__58__58__32_ops_32__58__58__32_Div_32__62__32__58__58__32_div( x: u32, y: u32, ) -> u32

Specification for [<u32 as core::ops::Div>::div]

Source

pub unsafe exec fn _verus_external_fn_specification_137__60__32_u64_32_as_32_core_32__58__58__32_ops_32__58__58__32_Div_32__62__32__58__58__32_div( x: u64, y: u64, ) -> u64

Specification for [<u64 as core::ops::Div>::div]

Source

pub unsafe exec fn _verus_external_fn_specification_138__60__32_u128_32_as_32_core_32__58__58__32_ops_32__58__58__32_Div_32__62__32__58__58__32_div( x: u128, y: u128, ) -> u128

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

Source§

impl VstdSpecsForRustStdLib

Source

pub unsafe exec fn _verus_external_fn_specification_139__60__32_isize_32_as_32_core_32__58__58__32_ops_32__58__58__32_Div_32__62__32__58__58__32_div( x: isize, y: isize, ) -> isize

Specification for [<isize as core::ops::Div>::div]

Source

pub unsafe exec fn _verus_external_fn_specification_140__60__32_i8_32_as_32_core_32__58__58__32_ops_32__58__58__32_Div_32__62__32__58__58__32_div( x: i8, y: i8, ) -> i8

Specification for [<i8 as core::ops::Div>::div]

Source

pub unsafe exec fn _verus_external_fn_specification_141__60__32_i16_32_as_32_core_32__58__58__32_ops_32__58__58__32_Div_32__62__32__58__58__32_div( x: i16, y: i16, ) -> i16

Specification for [<i16 as core::ops::Div>::div]

Source

pub unsafe exec fn _verus_external_fn_specification_142__60__32_i32_32_as_32_core_32__58__58__32_ops_32__58__58__32_Div_32__62__32__58__58__32_div( x: i32, y: i32, ) -> i32

Specification for [<i32 as core::ops::Div>::div]

Source

pub unsafe exec fn _verus_external_fn_specification_143__60__32_i64_32_as_32_core_32__58__58__32_ops_32__58__58__32_Div_32__62__32__58__58__32_div( x: i64, y: i64, ) -> i64

Specification for [<i64 as core::ops::Div>::div]

Source

pub unsafe exec fn _verus_external_fn_specification_144__60__32_i128_32_as_32_core_32__58__58__32_ops_32__58__58__32_Div_32__62__32__58__58__32_div( x: i128, y: i128, ) -> i128

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

Source§

impl VstdSpecsForRustStdLib

Source

pub unsafe exec fn _verus_external_fn_specification_145__60__32_usize_32_as_32_core_32__58__58__32_ops_32__58__58__32_Rem_32__62__32__58__58__32_rem( x: usize, y: usize, ) -> usize

Specification for [<usize as core::ops::Rem>::rem]

Source

pub unsafe exec fn _verus_external_fn_specification_146__60__32_u8_32_as_32_core_32__58__58__32_ops_32__58__58__32_Rem_32__62__32__58__58__32_rem( x: u8, y: u8, ) -> u8

Specification for [<u8 as core::ops::Rem>::rem]

Source

pub unsafe exec fn _verus_external_fn_specification_147__60__32_u16_32_as_32_core_32__58__58__32_ops_32__58__58__32_Rem_32__62__32__58__58__32_rem( x: u16, y: u16, ) -> u16

Specification for [<u16 as core::ops::Rem>::rem]

Source

pub unsafe exec fn _verus_external_fn_specification_148__60__32_u32_32_as_32_core_32__58__58__32_ops_32__58__58__32_Rem_32__62__32__58__58__32_rem( x: u32, y: u32, ) -> u32

Specification for [<u32 as core::ops::Rem>::rem]

Source

pub unsafe exec fn _verus_external_fn_specification_149__60__32_u64_32_as_32_core_32__58__58__32_ops_32__58__58__32_Rem_32__62__32__58__58__32_rem( x: u64, y: u64, ) -> u64

Specification for [<u64 as core::ops::Rem>::rem]

Source

pub unsafe exec fn _verus_external_fn_specification_150__60__32_u128_32_as_32_core_32__58__58__32_ops_32__58__58__32_Rem_32__62__32__58__58__32_rem( x: u128, y: u128, ) -> u128

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

Source§

impl VstdSpecsForRustStdLib

Source

pub unsafe exec fn _verus_external_fn_specification_151__60__32_isize_32_as_32_core_32__58__58__32_ops_32__58__58__32_Rem_32__62__32__58__58__32_rem( x: isize, y: isize, ) -> isize

Specification for [<isize as core::ops::Rem>::rem]

Source

pub unsafe exec fn _verus_external_fn_specification_152__60__32_i8_32_as_32_core_32__58__58__32_ops_32__58__58__32_Rem_32__62__32__58__58__32_rem( x: i8, y: i8, ) -> i8

Specification for [<i8 as core::ops::Rem>::rem]

Source

pub unsafe exec fn _verus_external_fn_specification_153__60__32_i16_32_as_32_core_32__58__58__32_ops_32__58__58__32_Rem_32__62__32__58__58__32_rem( x: i16, y: i16, ) -> i16

Specification for [<i16 as core::ops::Rem>::rem]

Source

pub unsafe exec fn _verus_external_fn_specification_154__60__32_i32_32_as_32_core_32__58__58__32_ops_32__58__58__32_Rem_32__62__32__58__58__32_rem( x: i32, y: i32, ) -> i32

Specification for [<i32 as core::ops::Rem>::rem]

Source

pub unsafe exec fn _verus_external_fn_specification_155__60__32_i64_32_as_32_core_32__58__58__32_ops_32__58__58__32_Rem_32__62__32__58__58__32_rem( x: i64, y: i64, ) -> i64

Specification for [<i64 as core::ops::Rem>::rem]

Source

pub unsafe exec fn _verus_external_fn_specification_156__60__32_i128_32_as_32_core_32__58__58__32_ops_32__58__58__32_Rem_32__62__32__58__58__32_rem( x: i128, y: i128, ) -> i128

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

Source§

impl VstdSpecsForRustStdLib

Source

pub unsafe exec fn _verus_external_fn_specification_157__60__32_usize_32_as_32_core_32__58__58__32_ops_32__58__58__32_BitAnd_32__62__32__58__58__32_bitand( x: usize, y: usize, ) -> usize

Specification for [<usize as core::ops::BitAnd>::bitand]

Source

pub unsafe exec fn _verus_external_fn_specification_158__60__32_u8_32_as_32_core_32__58__58__32_ops_32__58__58__32_BitAnd_32__62__32__58__58__32_bitand( x: u8, y: u8, ) -> u8

Specification for [<u8 as core::ops::BitAnd>::bitand]

Source

pub unsafe exec fn _verus_external_fn_specification_159__60__32_u16_32_as_32_core_32__58__58__32_ops_32__58__58__32_BitAnd_32__62__32__58__58__32_bitand( x: u16, y: u16, ) -> u16

Specification for [<u16 as core::ops::BitAnd>::bitand]

Source

pub unsafe exec fn _verus_external_fn_specification_160__60__32_u32_32_as_32_core_32__58__58__32_ops_32__58__58__32_BitAnd_32__62__32__58__58__32_bitand( x: u32, y: u32, ) -> u32

Specification for [<u32 as core::ops::BitAnd>::bitand]

Source

pub unsafe exec fn _verus_external_fn_specification_161__60__32_u64_32_as_32_core_32__58__58__32_ops_32__58__58__32_BitAnd_32__62__32__58__58__32_bitand( x: u64, y: u64, ) -> u64

Specification for [<u64 as core::ops::BitAnd>::bitand]

Source

pub unsafe exec fn _verus_external_fn_specification_162__60__32_u128_32_as_32_core_32__58__58__32_ops_32__58__58__32_BitAnd_32__62__32__58__58__32_bitand( x: u128, y: u128, ) -> u128

Specification for [<u128 as core::ops::BitAnd>::bitand]

Source

pub unsafe exec fn _verus_external_fn_specification_163__60__32_isize_32_as_32_core_32__58__58__32_ops_32__58__58__32_BitAnd_32__62__32__58__58__32_bitand( x: isize, y: isize, ) -> isize

Specification for [<isize as core::ops::BitAnd>::bitand]

Source

pub unsafe exec fn _verus_external_fn_specification_164__60__32_i8_32_as_32_core_32__58__58__32_ops_32__58__58__32_BitAnd_32__62__32__58__58__32_bitand( x: i8, y: i8, ) -> i8

Specification for [<i8 as core::ops::BitAnd>::bitand]

Source

pub unsafe exec fn _verus_external_fn_specification_165__60__32_i16_32_as_32_core_32__58__58__32_ops_32__58__58__32_BitAnd_32__62__32__58__58__32_bitand( x: i16, y: i16, ) -> i16

Specification for [<i16 as core::ops::BitAnd>::bitand]

Source

pub unsafe exec fn _verus_external_fn_specification_166__60__32_i32_32_as_32_core_32__58__58__32_ops_32__58__58__32_BitAnd_32__62__32__58__58__32_bitand( x: i32, y: i32, ) -> i32

Specification for [<i32 as core::ops::BitAnd>::bitand]

Source

pub unsafe exec fn _verus_external_fn_specification_167__60__32_i64_32_as_32_core_32__58__58__32_ops_32__58__58__32_BitAnd_32__62__32__58__58__32_bitand( x: i64, y: i64, ) -> i64

Specification for [<i64 as core::ops::BitAnd>::bitand]

Source

pub unsafe exec fn _verus_external_fn_specification_168__60__32_i128_32_as_32_core_32__58__58__32_ops_32__58__58__32_BitAnd_32__62__32__58__58__32_bitand( x: i128, y: i128, ) -> i128

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

Source§

impl VstdSpecsForRustStdLib

Source

pub unsafe exec fn _verus_external_fn_specification_169__60__32_usize_32_as_32_core_32__58__58__32_ops_32__58__58__32_BitOr_32__62__32__58__58__32_bitor( x: usize, y: usize, ) -> usize

Specification for [<usize as core::ops::BitOr>::bitor]

Source

pub unsafe exec fn _verus_external_fn_specification_170__60__32_u8_32_as_32_core_32__58__58__32_ops_32__58__58__32_BitOr_32__62__32__58__58__32_bitor( x: u8, y: u8, ) -> u8

Specification for [<u8 as core::ops::BitOr>::bitor]

Source

pub unsafe exec fn _verus_external_fn_specification_171__60__32_u16_32_as_32_core_32__58__58__32_ops_32__58__58__32_BitOr_32__62__32__58__58__32_bitor( x: u16, y: u16, ) -> u16

Specification for [<u16 as core::ops::BitOr>::bitor]

Source

pub unsafe exec fn _verus_external_fn_specification_172__60__32_u32_32_as_32_core_32__58__58__32_ops_32__58__58__32_BitOr_32__62__32__58__58__32_bitor( x: u32, y: u32, ) -> u32

Specification for [<u32 as core::ops::BitOr>::bitor]

Source

pub unsafe exec fn _verus_external_fn_specification_173__60__32_u64_32_as_32_core_32__58__58__32_ops_32__58__58__32_BitOr_32__62__32__58__58__32_bitor( x: u64, y: u64, ) -> u64

Specification for [<u64 as core::ops::BitOr>::bitor]

Source

pub unsafe exec fn _verus_external_fn_specification_174__60__32_u128_32_as_32_core_32__58__58__32_ops_32__58__58__32_BitOr_32__62__32__58__58__32_bitor( x: u128, y: u128, ) -> u128

Specification for [<u128 as core::ops::BitOr>::bitor]

Source

pub unsafe exec fn _verus_external_fn_specification_175__60__32_isize_32_as_32_core_32__58__58__32_ops_32__58__58__32_BitOr_32__62__32__58__58__32_bitor( x: isize, y: isize, ) -> isize

Specification for [<isize as core::ops::BitOr>::bitor]

Source

pub unsafe exec fn _verus_external_fn_specification_176__60__32_i8_32_as_32_core_32__58__58__32_ops_32__58__58__32_BitOr_32__62__32__58__58__32_bitor( x: i8, y: i8, ) -> i8

Specification for [<i8 as core::ops::BitOr>::bitor]

Source

pub unsafe exec fn _verus_external_fn_specification_177__60__32_i16_32_as_32_core_32__58__58__32_ops_32__58__58__32_BitOr_32__62__32__58__58__32_bitor( x: i16, y: i16, ) -> i16

Specification for [<i16 as core::ops::BitOr>::bitor]

Source

pub unsafe exec fn _verus_external_fn_specification_178__60__32_i32_32_as_32_core_32__58__58__32_ops_32__58__58__32_BitOr_32__62__32__58__58__32_bitor( x: i32, y: i32, ) -> i32

Specification for [<i32 as core::ops::BitOr>::bitor]

Source

pub unsafe exec fn _verus_external_fn_specification_179__60__32_i64_32_as_32_core_32__58__58__32_ops_32__58__58__32_BitOr_32__62__32__58__58__32_bitor( x: i64, y: i64, ) -> i64

Specification for [<i64 as core::ops::BitOr>::bitor]

Source

pub unsafe exec fn _verus_external_fn_specification_180__60__32_i128_32_as_32_core_32__58__58__32_ops_32__58__58__32_BitOr_32__62__32__58__58__32_bitor( x: i128, y: i128, ) -> i128

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

Source§

impl VstdSpecsForRustStdLib

Source

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

Specification for [<bool as core::ops::BitXor>::bitxor]

Source

pub unsafe exec fn _verus_external_fn_specification_182__60__32_usize_32_as_32_core_32__58__58__32_ops_32__58__58__32_BitXor_32__62__32__58__58__32_bitxor( x: usize, y: usize, ) -> usize

Specification for [<usize as core::ops::BitXor>::bitxor]

Source

pub unsafe exec fn _verus_external_fn_specification_183__60__32_u8_32_as_32_core_32__58__58__32_ops_32__58__58__32_BitXor_32__62__32__58__58__32_bitxor( x: u8, y: u8, ) -> u8

Specification for [<u8 as core::ops::BitXor>::bitxor]

Source

pub unsafe exec fn _verus_external_fn_specification_184__60__32_u16_32_as_32_core_32__58__58__32_ops_32__58__58__32_BitXor_32__62__32__58__58__32_bitxor( x: u16, y: u16, ) -> u16

Specification for [<u16 as core::ops::BitXor>::bitxor]

Source

pub unsafe exec fn _verus_external_fn_specification_185__60__32_u32_32_as_32_core_32__58__58__32_ops_32__58__58__32_BitXor_32__62__32__58__58__32_bitxor( x: u32, y: u32, ) -> u32

Specification for [<u32 as core::ops::BitXor>::bitxor]

Source

pub unsafe exec fn _verus_external_fn_specification_186__60__32_u64_32_as_32_core_32__58__58__32_ops_32__58__58__32_BitXor_32__62__32__58__58__32_bitxor( x: u64, y: u64, ) -> u64

Specification for [<u64 as core::ops::BitXor>::bitxor]

Source

pub unsafe exec fn _verus_external_fn_specification_187__60__32_u128_32_as_32_core_32__58__58__32_ops_32__58__58__32_BitXor_32__62__32__58__58__32_bitxor( x: u128, y: u128, ) -> u128

Specification for [<u128 as core::ops::BitXor>::bitxor]

Source

pub unsafe exec fn _verus_external_fn_specification_188__60__32_isize_32_as_32_core_32__58__58__32_ops_32__58__58__32_BitXor_32__62__32__58__58__32_bitxor( x: isize, y: isize, ) -> isize

Specification for [<isize as core::ops::BitXor>::bitxor]

Source

pub unsafe exec fn _verus_external_fn_specification_189__60__32_i8_32_as_32_core_32__58__58__32_ops_32__58__58__32_BitXor_32__62__32__58__58__32_bitxor( x: i8, y: i8, ) -> i8

Specification for [<i8 as core::ops::BitXor>::bitxor]

Source

pub unsafe exec fn _verus_external_fn_specification_190__60__32_i16_32_as_32_core_32__58__58__32_ops_32__58__58__32_BitXor_32__62__32__58__58__32_bitxor( x: i16, y: i16, ) -> i16

Specification for [<i16 as core::ops::BitXor>::bitxor]

Source

pub unsafe exec fn _verus_external_fn_specification_191__60__32_i32_32_as_32_core_32__58__58__32_ops_32__58__58__32_BitXor_32__62__32__58__58__32_bitxor( x: i32, y: i32, ) -> i32

Specification for [<i32 as core::ops::BitXor>::bitxor]

Source

pub unsafe exec fn _verus_external_fn_specification_192__60__32_i64_32_as_32_core_32__58__58__32_ops_32__58__58__32_BitXor_32__62__32__58__58__32_bitxor( x: i64, y: i64, ) -> i64

Specification for [<i64 as core::ops::BitXor>::bitxor]

Source

pub unsafe exec fn _verus_external_fn_specification_193__60__32_i128_32_as_32_core_32__58__58__32_ops_32__58__58__32_BitXor_32__62__32__58__58__32_bitxor( x: i128, y: i128, ) -> i128

Specification for [<i128 as core::ops::BitXor>::bitxor]

Source§

impl VstdSpecsForRustStdLib

Source

pub unsafe exec fn _verus_external_fn_specification_194__60__32_usize_32_as_32_core_32__58__58__32_ops_32__58__58__32_Shl_32__62__32__58__58__32_shl( x: usize, y: usize, ) -> usize

Specification for [<usize as core::ops::Shl>::shl]

Source

pub unsafe exec fn _verus_external_fn_specification_195__60__32_u8_32_as_32_core_32__58__58__32_ops_32__58__58__32_Shl_32__62__32__58__58__32_shl( x: u8, y: u8, ) -> u8

Specification for [<u8 as core::ops::Shl>::shl]

Source

pub unsafe exec fn _verus_external_fn_specification_196__60__32_u16_32_as_32_core_32__58__58__32_ops_32__58__58__32_Shl_32__62__32__58__58__32_shl( x: u16, y: u16, ) -> u16

Specification for [<u16 as core::ops::Shl>::shl]

Source

pub unsafe exec fn _verus_external_fn_specification_197__60__32_u32_32_as_32_core_32__58__58__32_ops_32__58__58__32_Shl_32__62__32__58__58__32_shl( x: u32, y: u32, ) -> u32

Specification for [<u32 as core::ops::Shl>::shl]

Source

pub unsafe exec fn _verus_external_fn_specification_198__60__32_u64_32_as_32_core_32__58__58__32_ops_32__58__58__32_Shl_32__62__32__58__58__32_shl( x: u64, y: u64, ) -> u64

Specification for [<u64 as core::ops::Shl>::shl]

Source

pub unsafe exec fn _verus_external_fn_specification_199__60__32_u128_32_as_32_core_32__58__58__32_ops_32__58__58__32_Shl_32__62__32__58__58__32_shl( x: u128, y: u128, ) -> u128

Specification for [<u128 as core::ops::Shl>::shl]

Source

pub unsafe exec fn _verus_external_fn_specification_200__60__32_isize_32_as_32_core_32__58__58__32_ops_32__58__58__32_Shl_32__62__32__58__58__32_shl( x: isize, y: isize, ) -> isize

Specification for [<isize as core::ops::Shl>::shl]

Source

pub unsafe exec fn _verus_external_fn_specification_201__60__32_i8_32_as_32_core_32__58__58__32_ops_32__58__58__32_Shl_32__62__32__58__58__32_shl( x: i8, y: i8, ) -> i8

Specification for [<i8 as core::ops::Shl>::shl]

Source

pub unsafe exec fn _verus_external_fn_specification_202__60__32_i16_32_as_32_core_32__58__58__32_ops_32__58__58__32_Shl_32__62__32__58__58__32_shl( x: i16, y: i16, ) -> i16

Specification for [<i16 as core::ops::Shl>::shl]

Source

pub unsafe exec fn _verus_external_fn_specification_203__60__32_i32_32_as_32_core_32__58__58__32_ops_32__58__58__32_Shl_32__62__32__58__58__32_shl( x: i32, y: i32, ) -> i32

Specification for [<i32 as core::ops::Shl>::shl]

Source

pub unsafe exec fn _verus_external_fn_specification_204__60__32_i64_32_as_32_core_32__58__58__32_ops_32__58__58__32_Shl_32__62__32__58__58__32_shl( x: i64, y: i64, ) -> i64

Specification for [<i64 as core::ops::Shl>::shl]

Source

pub unsafe exec fn _verus_external_fn_specification_205__60__32_i128_32_as_32_core_32__58__58__32_ops_32__58__58__32_Shl_32__62__32__58__58__32_shl( x: i128, y: i128, ) -> i128

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

Source§

impl VstdSpecsForRustStdLib

Source

pub unsafe exec fn _verus_external_fn_specification_206__60__32_usize_32_as_32_core_32__58__58__32_ops_32__58__58__32_Shr_32__62__32__58__58__32_shr( x: usize, y: usize, ) -> usize

Specification for [<usize as core::ops::Shr>::shr]

Source

pub unsafe exec fn _verus_external_fn_specification_207__60__32_u8_32_as_32_core_32__58__58__32_ops_32__58__58__32_Shr_32__62__32__58__58__32_shr( x: u8, y: u8, ) -> u8

Specification for [<u8 as core::ops::Shr>::shr]

Source

pub unsafe exec fn _verus_external_fn_specification_208__60__32_u16_32_as_32_core_32__58__58__32_ops_32__58__58__32_Shr_32__62__32__58__58__32_shr( x: u16, y: u16, ) -> u16

Specification for [<u16 as core::ops::Shr>::shr]

Source

pub unsafe exec fn _verus_external_fn_specification_209__60__32_u32_32_as_32_core_32__58__58__32_ops_32__58__58__32_Shr_32__62__32__58__58__32_shr( x: u32, y: u32, ) -> u32

Specification for [<u32 as core::ops::Shr>::shr]

Source

pub unsafe exec fn _verus_external_fn_specification_210__60__32_u64_32_as_32_core_32__58__58__32_ops_32__58__58__32_Shr_32__62__32__58__58__32_shr( x: u64, y: u64, ) -> u64

Specification for [<u64 as core::ops::Shr>::shr]

Source

pub unsafe exec fn _verus_external_fn_specification_211__60__32_u128_32_as_32_core_32__58__58__32_ops_32__58__58__32_Shr_32__62__32__58__58__32_shr( x: u128, y: u128, ) -> u128

Specification for [<u128 as core::ops::Shr>::shr]

Source

pub unsafe exec fn _verus_external_fn_specification_212__60__32_isize_32_as_32_core_32__58__58__32_ops_32__58__58__32_Shr_32__62__32__58__58__32_shr( x: isize, y: isize, ) -> isize

Specification for [<isize as core::ops::Shr>::shr]

Source

pub unsafe exec fn _verus_external_fn_specification_213__60__32_i8_32_as_32_core_32__58__58__32_ops_32__58__58__32_Shr_32__62__32__58__58__32_shr( x: i8, y: i8, ) -> i8

Specification for [<i8 as core::ops::Shr>::shr]

Source

pub unsafe exec fn _verus_external_fn_specification_214__60__32_i16_32_as_32_core_32__58__58__32_ops_32__58__58__32_Shr_32__62__32__58__58__32_shr( x: i16, y: i16, ) -> i16

Specification for [<i16 as core::ops::Shr>::shr]

Source

pub unsafe exec fn _verus_external_fn_specification_215__60__32_i32_32_as_32_core_32__58__58__32_ops_32__58__58__32_Shr_32__62__32__58__58__32_shr( x: i32, y: i32, ) -> i32

Specification for [<i32 as core::ops::Shr>::shr]

Source

pub unsafe exec fn _verus_external_fn_specification_216__60__32_i64_32_as_32_core_32__58__58__32_ops_32__58__58__32_Shr_32__62__32__58__58__32_shr( x: i64, y: i64, ) -> i64

Specification for [<i64 as core::ops::Shr>::shr]

Source

pub unsafe exec fn _verus_external_fn_specification_217__60__32_i128_32_as_32_core_32__58__58__32_ops_32__58__58__32_Shr_32__62__32__58__58__32_shr( x: i128, y: i128, ) -> i128

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

Source§

impl VstdSpecsForRustStdLib

Source

pub unsafe exec fn _verus_external_fn_specification_218__60__32_f32_32_as_32_core_32__58__58__32_ops_32__58__58__32_Neg_32__62__32__58__58__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_219__60__32_f32_32_as_32_core_32__58__58__32_ops_32__58__58__32_Add_32__62__32__58__58__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_220__60__32_f32_32_as_32_core_32__58__58__32_ops_32__58__58__32_Sub_32__62__32__58__58__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_221__60__32_f32_32_as_32_core_32__58__58__32_ops_32__58__58__32_Mul_32__62__32__58__58__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_222__60__32_f32_32_as_32_core_32__58__58__32_ops_32__58__58__32_Div_32__62__32__58__58__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_223__60__32_f64_32_as_32_core_32__58__58__32_ops_32__58__58__32_Neg_32__62__32__58__58__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_224__60__32_f64_32_as_32_core_32__58__58__32_ops_32__58__58__32_Add_32__62__32__58__58__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_225__60__32_f64_32_as_32_core_32__58__58__32_ops_32__58__58__32_Sub_32__62__32__58__58__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_226__60__32_f64_32_as_32_core_32__58__58__32_ops_32__58__58__32_Mul_32__62__32__58__58__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_227__60__32_f64_32_as_32_core_32__58__58__32_ops_32__58__58__32_Div_32__62__32__58__58__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_228_DefaultHasher_32__58__58__32_new() -> result : DefaultHasher

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

Specification for DefaultHasher::new

Source

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

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

Specification for DefaultHasher::write

Source

pub unsafe exec fn _verus_external_fn_specification_230_DefaultHasher_32__58__58__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_231_Keys_32__58__58__32__60__32__39_a_44__32_Key_44__32_Value_32__62__32__58__58__32_next<'a, Key, Value>( keys: &mut Keys<'a, Key, Value>, ) -> r : Option<&'a Key>

ensures
({
    let (old_index, old_seq) = old(keys)@;
    match r {
        None => (
            &&& keys@ == old(keys)@
            &&& old_index >= old_seq.len()

        ),
        Some(k) => {
            let (new_index, new_seq) = keys@;
            &&& 0 <= old_index < old_seq.len()
            &&& new_seq == old_seq
            &&& new_index == old_index + 1
            &&& k == old_seq[old_index]

        }
    }
}),

Specification for [Keys::<'a, Key, Value>::next]

Source

pub unsafe exec fn _verus_external_fn_specification_232_Values_32__58__58__32__60__32__39_a_44__32_Key_44__32_Value_32__62__32__58__58__32_next<'a, Key, Value>( values: &mut Values<'a, Key, Value>, ) -> r : Option<&'a Value>

ensures
({
    let (old_index, old_seq) = old(values)@;
    match r {
        None => (
            &&& values@ == old(values)@
            &&& old_index >= old_seq.len()

        ),
        Some(v) => {
            let (new_index, new_seq) = values@;
            &&& 0 <= old_index < old_seq.len()
            &&& new_seq == old_seq
            &&& new_index == old_index + 1
            &&& v == old_seq[old_index]

        }
    }
}),

Specification for [Values::<'a, Key, Value>::next]

Source

pub unsafe exec fn _verus_external_fn_specification_233_hash__map_32__58__58__32_Iter_32__58__58__32__60__32__39_a_44__32_Key_44__32_Value_32__62__32__58__58__32_next<'a, Key, Value>( iter: &mut Iter<'a, Key, Value>, ) -> r : Option<(&'a Key, &'a Value)>

ensures
({
    let (old_index, old_seq) = old(iter)@;
    match r {
        None => (
            &&& iter@ == old(iter)@
            &&& old_index >= old_seq.len()

        ),
        Some((k, v)) => {
            let (new_index, new_seq) = iter@;
            let (old_k, old_v) = old_seq[old_index];
            &&& 0 <= old_index < old_seq.len()
            &&& new_seq == old_seq
            &&& new_index == old_index + 1
            &&& k == old_k
            &&& v == old_v
            &&& old_seq.to_set().contains((*k, *v))

        }
    }
}),

Specification for [hash_map::Iter::<'a, Key, Value>::next]

Source

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

ensures
obeys_key_model::<Key>() && builds_valid_hashers::<S>()
    ==> {
        let (index, s) = iter@;
        &&& index == 0
        &&& s.to_set() == m@.kv_pairs()
        &&& s.no_duplicates()

    },

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

Source

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

ensures
len == spec_hash_map_len(m),

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

Source

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

ensures
res == m@.is_empty(),

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

Source

pub unsafe exec fn _verus_external_fn_specification_237__60__32_HashMap_32__58__58__32__60__32_K_44__32_V_44__32_S_32__62__32_as_32_Clone_32__62__32__58__58__32_clone<K: Clone, V: Clone, S: Clone>( this: &HashMap<K, V, S>, ) -> other : HashMap<K, V, S>

ensures
other@ == this@,

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

Source

pub unsafe exec fn _verus_external_fn_specification_238_HashMap_32__58__58__32__60__32_Key_44__32_Value_32__62__32__58__58__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_239_HashMap_32__58__58__32__60__32_Key_44__32_Value_32__62__32__58__58__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_240_HashMap_32__58__58__32__60__32_Key_44__32_Value_44__32_S_44__32__62__32__58__58__32_reserve<Key: Eq + Hash, Value, S: BuildHasher>( m: &mut HashMap<Key, Value, S>, additional: usize, )

ensures
m@ == old(m)@,

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

Source

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

ensures
obeys_key_model::<Key>() && builds_valid_hashers::<S>()
    ==> {
        &&& 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>::insert

Source

pub unsafe exec fn _verus_external_fn_specification_242_HashMap_32__58__58__32__60__32_Key_44__32_Value_44__32_S_32__62__32__58__58__32_contains__key_32__58__58__32__60__32_Q_32__62_<Key: Borrow<Q> + Hash + Eq, Value, S: BuildHasher, Q: Hash + Eq + ?Sized>( m: &HashMap<Key, Value, S>, 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>::contains_key::<Q>

Source

pub unsafe exec fn _verus_external_fn_specification_243_HashMap_32__58__58__32__60__32_Key_44__32_Value_44__32_S_32__62__32__58__58__32_get_32__58__58__32__60__32_Q_32__62_<'a, Key: Borrow<Q> + Hash + Eq, Value, S: BuildHasher, Q: Hash + Eq + ?Sized>( m: &'a HashMap<Key, Value, S>, 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>::get::<Q>

Source

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

ensures
obeys_key_model::<Key>() && builds_valid_hashers::<S>()
    ==> {
        &&& borrowed_key_removed(old(m)@, 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>::remove::<Q>

Source

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

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

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

Source

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

ensures
obeys_key_model::<Key>() && builds_valid_hashers::<S>()
    ==> {
        let (index, s) = keys@;
        &&& index == 0
        &&& s.to_set() == m@.dom()
        &&& s.no_duplicates()

    },

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

Source

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

ensures
obeys_key_model::<Key>() && builds_valid_hashers::<S>()
    ==> {
        let (index, s) = values@;
        &&& index == 0
        &&& s.to_set() == m@.values()

    },

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

Source

pub unsafe exec fn _verus_external_fn_specification_248_hash__set_32__58__58__32_Iter_32__58__58__32__60__32__39_a_44__32_Key_32__62__32__58__58__32_next<'a, Key>( elements: &mut Iter<'a, Key>, ) -> r : Option<&'a Key>

ensures
({
    let (old_index, old_seq) = old(elements)@;
    match r {
        None => (
            &&& elements@ == old(elements)@
            &&& old_index >= old_seq.len()

        ),
        Some(element) => {
            let (new_index, new_seq) = elements@;
            &&& 0 <= old_index < old_seq.len()
            &&& new_seq == old_seq
            &&& new_index == old_index + 1
            &&& element == old_seq[old_index]

        }
    }
}),

Specification for [hash_set::Iter::<'a, Key>::next]

Source

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

ensures
len == spec_hash_set_len(m),

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

Source

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

ensures
res == m@.is_empty(),

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

Source

pub unsafe exec fn _verus_external_fn_specification_251_HashSet_32__58__58__32__60__32_Key_32__62__32__58__58__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_252_HashSet_32__58__58__32__60__32_Key_32__62__32__58__58__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_253_HashSet_32__58__58__32__60__32_Key_44__32_S_32__62__32__58__58__32_reserve<Key: Eq + Hash, S: BuildHasher>( m: &mut HashSet<Key, S>, additional: usize, )

ensures
m@ == old(m)@,

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

Source

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

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

    },

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

Source

pub unsafe exec fn _verus_external_fn_specification_255_HashSet_32__58__58__32__60__32_Key_44__32_S_32__62__32__58__58__32_contains<Key: Borrow<Q> + Hash + Eq, S: BuildHasher, Q: Hash + Eq + ?Sized>( m: &HashSet<Key, S>, 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>::contains

Source

pub unsafe exec fn _verus_external_fn_specification_256_HashSet_32__58__58__32__60__32_Key_44__32_S_32__62__32__58__58__32_get_32__58__58__32__60__32_Q_32__62_<'a, Key: Borrow<Q> + Hash + Eq, S: BuildHasher, Q: Hash + Eq + ?Sized>( m: &'a HashSet<Key, S>, 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>::get::<Q>

Source

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

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

    },

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

Source

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

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

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

Source

pub unsafe exec fn _verus_external_fn_specification_259_HashSet_32__58__58__32__60__32_Key_44__32_S_32__62__32__58__58__32_iter<'a, Key, S>( m: &'a HashSet<Key, S>, ) -> r : Iter<'a, Key>

ensures
obeys_key_model::<Key>() && builds_valid_hashers::<S>()
    ==> {
        let (index, s) = r@;
        &&& index == 0
        &&& s.to_set() == m@
        &&& s.no_duplicates()

    },

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

Source§

impl VstdSpecsForRustStdLib

Source

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

ensures
res == x,

Specification for [<u8 as Clone>::clone]

Source

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

Specification for [<u8 as PartialEq<u8>>::eq]

Source

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

Specification for [<u8 as PartialEq<u8>>::ne]

Source

pub unsafe exec fn _verus_external_fn_specification_263__60__32_u8_32_as_32_Ord_32__62__32__58__58__32_cmp( x: &u8, y: &u8, ) -> Ordering

Specification for [<u8 as Ord>::cmp]

Source

pub unsafe exec fn _verus_external_fn_specification_264__60__32_u8_32_as_32_PartialOrd_32__60__32_u8_32__62__32__62__32__58__58__32_partial__cmp( x: &u8, y: &u8, ) -> Option<Ordering>

Specification for [<u8 as PartialOrd<u8>>::partial_cmp]

Source

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

Specification for [<u8 as PartialOrd<u8>>::lt]

Source

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

Specification for [<u8 as PartialOrd<u8>>::le]

Source

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

Specification for [<u8 as PartialOrd<u8>>::gt]

Source

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

Specification for [<u8 as PartialOrd<u8>>::ge]

Source

pub unsafe exec fn _verus_external_fn_specification_269__60__32_u8_32__62__32__58__58__32_wrapping__add( x: u8, y: u8, ) -> u8

Specification for u8::wrapping_add

Source

pub unsafe exec fn _verus_external_fn_specification_270__60__32_u8_32__62__32__58__58__32_wrapping__add__signed( x: u8, y: i8, ) -> u8

Specification for u8::wrapping_add_signed

Source

pub unsafe exec fn _verus_external_fn_specification_271__60__32_u8_32__62__32__58__58__32_wrapping__sub( x: u8, y: u8, ) -> u8

Specification for u8::wrapping_sub

Source

pub unsafe exec fn _verus_external_fn_specification_272__60__32_u8_32__62__32__58__58__32_wrapping__mul( x: u8, y: u8, ) -> u8

Specification for u8::wrapping_mul

Source

pub unsafe exec fn _verus_external_fn_specification_273__60__32_u8_32__62__32__58__58__32_checked__add( x: u8, y: u8, ) -> Option<u8>

Specification for u8::checked_add

Source

pub unsafe exec fn _verus_external_fn_specification_274__60__32_u8_32__62__32__58__58__32_checked__add__signed( x: u8, y: i8, ) -> Option<u8>

Specification for u8::checked_add_signed

Source

pub unsafe exec fn _verus_external_fn_specification_275__60__32_u8_32__62__32__58__58__32_checked__sub( x: u8, y: u8, ) -> Option<u8>

Specification for u8::checked_sub

Source

pub unsafe exec fn _verus_external_fn_specification_276__60__32_u8_32__62__32__58__58__32_checked__mul( x: u8, y: u8, ) -> Option<u8>

Specification for u8::checked_mul

Source

pub unsafe exec fn _verus_external_fn_specification_277__60__32_u8_32__62__32__58__58__32_checked__div( lhs: u8, rhs: u8, ) -> result : Option<u8>

ensures
result == checked_div(lhs, rhs),

Specification for u8::checked_div

Source

pub unsafe exec fn _verus_external_fn_specification_278__60__32_u8_32__62__32__58__58__32_checked__div__euclid( lhs: u8, rhs: u8, ) -> result : Option<u8>

ensures
result == checked_div(lhs, rhs),

Specification for u8::checked_div_euclid

Source§

impl VstdSpecsForRustStdLib

Source

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

ensures
res == x,

Specification for [<i8 as Clone>::clone]

Source

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

Specification for [<i8 as PartialEq<i8>>::eq]

Source

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

Specification for [<i8 as PartialEq<i8>>::ne]

Source

pub unsafe exec fn _verus_external_fn_specification_282__60__32_i8_32_as_32_Ord_32__62__32__58__58__32_cmp( x: &i8, y: &i8, ) -> Ordering

Specification for [<i8 as Ord>::cmp]

Source

pub unsafe exec fn _verus_external_fn_specification_283__60__32_i8_32_as_32_PartialOrd_32__60__32_i8_32__62__32__62__32__58__58__32_partial__cmp( x: &i8, y: &i8, ) -> Option<Ordering>

Specification for [<i8 as PartialOrd<i8>>::partial_cmp]

Source

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

Specification for [<i8 as PartialOrd<i8>>::lt]

Source

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

Specification for [<i8 as PartialOrd<i8>>::le]

Source

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

Specification for [<i8 as PartialOrd<i8>>::gt]

Source

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

Specification for [<i8 as PartialOrd<i8>>::ge]

Source

pub unsafe exec fn _verus_external_fn_specification_288__60__32_i8_32__62__32__58__58__32_wrapping__add( x: i8, y: i8, ) -> i8

Specification for i8::wrapping_add

Source

pub unsafe exec fn _verus_external_fn_specification_289__60__32_i8_32__62__32__58__58__32_wrapping__add__unsigned( x: i8, y: u8, ) -> i8

Specification for i8::wrapping_add_unsigned

Source

pub unsafe exec fn _verus_external_fn_specification_290__60__32_i8_32__62__32__58__58__32_wrapping__sub( x: i8, y: i8, ) -> res : i8

Specification for i8::wrapping_sub

Source

pub unsafe exec fn _verus_external_fn_specification_291__60__32_i8_32__62__32__58__58__32_wrapping__mul( x: i8, y: i8, ) -> i8

Specification for i8::wrapping_mul

Source

pub unsafe exec fn _verus_external_fn_specification_292__60__32_i8_32__62__32__58__58__32_checked__add( x: i8, y: i8, ) -> Option<i8>

Specification for i8::checked_add

Source

pub unsafe exec fn _verus_external_fn_specification_293__60__32_i8_32__62__32__58__58__32_checked__add__unsigned( x: i8, y: u8, ) -> Option<i8>

Specification for i8::checked_add_unsigned

Source

pub unsafe exec fn _verus_external_fn_specification_294__60__32_u8_32__62__32__58__58__32_saturating__add( x: u8, y: u8, ) -> u8

Specification for u8::saturating_add

Source

pub unsafe exec fn _verus_external_fn_specification_295__60__32_i8_32__62__32__58__58__32_checked__sub( x: i8, y: i8, ) -> Option<i8>

Specification for i8::checked_sub

Source

pub unsafe exec fn _verus_external_fn_specification_296__60__32_i8_32__62__32__58__58__32_checked__sub__unsigned( x: i8, y: u8, ) -> Option<i8>

Specification for i8::checked_sub_unsigned

Source

pub unsafe exec fn _verus_external_fn_specification_297__60__32_i8_32__62__32__58__58__32_checked__mul( x: i8, y: i8, ) -> Option<i8>

Specification for i8::checked_mul

Source§

impl VstdSpecsForRustStdLib

Source

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

ensures
res == x,

Specification for [<u16 as Clone>::clone]

Source

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

Specification for [<u16 as PartialEq<u16>>::eq]

Source

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

Specification for [<u16 as PartialEq<u16>>::ne]

Source

pub unsafe exec fn _verus_external_fn_specification_301__60__32_u16_32_as_32_Ord_32__62__32__58__58__32_cmp( x: &u16, y: &u16, ) -> Ordering

Specification for [<u16 as Ord>::cmp]

Source

pub unsafe exec fn _verus_external_fn_specification_302__60__32_u16_32_as_32_PartialOrd_32__60__32_u16_32__62__32__62__32__58__58__32_partial__cmp( x: &u16, y: &u16, ) -> Option<Ordering>

Specification for [<u16 as PartialOrd<u16>>::partial_cmp]

Source

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

Specification for [<u16 as PartialOrd<u16>>::lt]

Source

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

Specification for [<u16 as PartialOrd<u16>>::le]

Source

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

Specification for [<u16 as PartialOrd<u16>>::gt]

Source

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

Specification for [<u16 as PartialOrd<u16>>::ge]

Source

pub unsafe exec fn _verus_external_fn_specification_307__60__32_u16_32__62__32__58__58__32_wrapping__add( x: u16, y: u16, ) -> u16

Specification for u16::wrapping_add

Source

pub unsafe exec fn _verus_external_fn_specification_308__60__32_u16_32__62__32__58__58__32_wrapping__add__signed( x: u16, y: i16, ) -> u16

Specification for u16::wrapping_add_signed

Source

pub unsafe exec fn _verus_external_fn_specification_309__60__32_u16_32__62__32__58__58__32_wrapping__sub( x: u16, y: u16, ) -> u16

Specification for u16::wrapping_sub

Source

pub unsafe exec fn _verus_external_fn_specification_310__60__32_u16_32__62__32__58__58__32_wrapping__mul( x: u16, y: u16, ) -> u16

Specification for u16::wrapping_mul

Source

pub unsafe exec fn _verus_external_fn_specification_311__60__32_u16_32__62__32__58__58__32_checked__add( x: u16, y: u16, ) -> Option<u16>

Specification for u16::checked_add

Source

pub unsafe exec fn _verus_external_fn_specification_312__60__32_u16_32__62__32__58__58__32_checked__add__signed( x: u16, y: i16, ) -> Option<u16>

Specification for u16::checked_add_signed

Source

pub unsafe exec fn _verus_external_fn_specification_313__60__32_u16_32__62__32__58__58__32_checked__sub( x: u16, y: u16, ) -> Option<u16>

Specification for u16::checked_sub

Source

pub unsafe exec fn _verus_external_fn_specification_314__60__32_u16_32__62__32__58__58__32_checked__mul( x: u16, y: u16, ) -> Option<u16>

Specification for u16::checked_mul

Source

pub unsafe exec fn _verus_external_fn_specification_315__60__32_u16_32__62__32__58__58__32_checked__div( lhs: u16, rhs: u16, ) -> result : Option<u16>

ensures
result == checked_div(lhs, rhs),

Specification for u16::checked_div

Source

pub unsafe exec fn _verus_external_fn_specification_316__60__32_u16_32__62__32__58__58__32_checked__div__euclid( lhs: u16, rhs: u16, ) -> result : Option<u16>

ensures
result == checked_div(lhs, rhs),

Specification for u16::checked_div_euclid

Source§

impl VstdSpecsForRustStdLib

Source

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

ensures
res == x,

Specification for [<i16 as Clone>::clone]

Source

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

Specification for [<i16 as PartialEq<i16>>::eq]

Source

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

Specification for [<i16 as PartialEq<i16>>::ne]

Source

pub unsafe exec fn _verus_external_fn_specification_320__60__32_i16_32_as_32_Ord_32__62__32__58__58__32_cmp( x: &i16, y: &i16, ) -> Ordering

Specification for [<i16 as Ord>::cmp]

Source

pub unsafe exec fn _verus_external_fn_specification_321__60__32_i16_32_as_32_PartialOrd_32__60__32_i16_32__62__32__62__32__58__58__32_partial__cmp( x: &i16, y: &i16, ) -> Option<Ordering>

Specification for [<i16 as PartialOrd<i16>>::partial_cmp]

Source

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

Specification for [<i16 as PartialOrd<i16>>::lt]

Source

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

Specification for [<i16 as PartialOrd<i16>>::le]

Source

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

Specification for [<i16 as PartialOrd<i16>>::gt]

Source

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

Specification for [<i16 as PartialOrd<i16>>::ge]

Source

pub unsafe exec fn _verus_external_fn_specification_326__60__32_i16_32__62__32__58__58__32_wrapping__add( x: i16, y: i16, ) -> i16

Specification for i16::wrapping_add

Source

pub unsafe exec fn _verus_external_fn_specification_327__60__32_i16_32__62__32__58__58__32_wrapping__add__unsigned( x: i16, y: u16, ) -> i16

Specification for i16::wrapping_add_unsigned

Source

pub unsafe exec fn _verus_external_fn_specification_328__60__32_i16_32__62__32__58__58__32_wrapping__sub( x: i16, y: i16, ) -> res : i16

Specification for i16::wrapping_sub

Source

pub unsafe exec fn _verus_external_fn_specification_329__60__32_i16_32__62__32__58__58__32_wrapping__mul( x: i16, y: i16, ) -> i16

Specification for i16::wrapping_mul

Source

pub unsafe exec fn _verus_external_fn_specification_330__60__32_i16_32__62__32__58__58__32_checked__add( x: i16, y: i16, ) -> Option<i16>

Specification for i16::checked_add

Source

pub unsafe exec fn _verus_external_fn_specification_331__60__32_i16_32__62__32__58__58__32_checked__add__unsigned( x: i16, y: u16, ) -> Option<i16>

Specification for i16::checked_add_unsigned

Source

pub unsafe exec fn _verus_external_fn_specification_332__60__32_u16_32__62__32__58__58__32_saturating__add( x: u16, y: u16, ) -> u16

Specification for u16::saturating_add

Source

pub unsafe exec fn _verus_external_fn_specification_333__60__32_i16_32__62__32__58__58__32_checked__sub( x: i16, y: i16, ) -> Option<i16>

Specification for i16::checked_sub

Source

pub unsafe exec fn _verus_external_fn_specification_334__60__32_i16_32__62__32__58__58__32_checked__sub__unsigned( x: i16, y: u16, ) -> Option<i16>

Specification for i16::checked_sub_unsigned

Source

pub unsafe exec fn _verus_external_fn_specification_335__60__32_i16_32__62__32__58__58__32_checked__mul( x: i16, y: i16, ) -> Option<i16>

Specification for i16::checked_mul

Source§

impl VstdSpecsForRustStdLib

Source

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

ensures
res == x,

Specification for [<u32 as Clone>::clone]

Source

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

Specification for [<u32 as PartialEq<u32>>::eq]

Source

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

Specification for [<u32 as PartialEq<u32>>::ne]

Source

pub unsafe exec fn _verus_external_fn_specification_339__60__32_u32_32_as_32_Ord_32__62__32__58__58__32_cmp( x: &u32, y: &u32, ) -> Ordering

Specification for [<u32 as Ord>::cmp]

Source

pub unsafe exec fn _verus_external_fn_specification_340__60__32_u32_32_as_32_PartialOrd_32__60__32_u32_32__62__32__62__32__58__58__32_partial__cmp( x: &u32, y: &u32, ) -> Option<Ordering>

Specification for [<u32 as PartialOrd<u32>>::partial_cmp]

Source

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

Specification for [<u32 as PartialOrd<u32>>::lt]

Source

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

Specification for [<u32 as PartialOrd<u32>>::le]

Source

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

Specification for [<u32 as PartialOrd<u32>>::gt]

Source

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

Specification for [<u32 as PartialOrd<u32>>::ge]

Source

pub unsafe exec fn _verus_external_fn_specification_345__60__32_u32_32__62__32__58__58__32_wrapping__add( x: u32, y: u32, ) -> u32

Specification for u32::wrapping_add

Source

pub unsafe exec fn _verus_external_fn_specification_346__60__32_u32_32__62__32__58__58__32_wrapping__add__signed( x: u32, y: i32, ) -> u32

Specification for u32::wrapping_add_signed

Source

pub unsafe exec fn _verus_external_fn_specification_347__60__32_u32_32__62__32__58__58__32_wrapping__sub( x: u32, y: u32, ) -> u32

Specification for u32::wrapping_sub

Source

pub unsafe exec fn _verus_external_fn_specification_348__60__32_u32_32__62__32__58__58__32_wrapping__mul( x: u32, y: u32, ) -> u32

Specification for u32::wrapping_mul

Source

pub unsafe exec fn _verus_external_fn_specification_349__60__32_u32_32__62__32__58__58__32_checked__add( x: u32, y: u32, ) -> Option<u32>

Specification for u32::checked_add

Source

pub unsafe exec fn _verus_external_fn_specification_350__60__32_u32_32__62__32__58__58__32_checked__add__signed( x: u32, y: i32, ) -> Option<u32>

Specification for u32::checked_add_signed

Source

pub unsafe exec fn _verus_external_fn_specification_351__60__32_u32_32__62__32__58__58__32_checked__sub( x: u32, y: u32, ) -> Option<u32>

Specification for u32::checked_sub

Source

pub unsafe exec fn _verus_external_fn_specification_352__60__32_u32_32__62__32__58__58__32_checked__mul( x: u32, y: u32, ) -> Option<u32>

Specification for u32::checked_mul

Source

pub unsafe exec fn _verus_external_fn_specification_353__60__32_u32_32__62__32__58__58__32_checked__div( lhs: u32, rhs: u32, ) -> result : Option<u32>

ensures
result == checked_div(lhs, rhs),

Specification for u32::checked_div

Source

pub unsafe exec fn _verus_external_fn_specification_354__60__32_u32_32__62__32__58__58__32_checked__div__euclid( lhs: u32, rhs: u32, ) -> result : Option<u32>

ensures
result == checked_div(lhs, rhs),

Specification for u32::checked_div_euclid

Source§

impl VstdSpecsForRustStdLib

Source

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

ensures
res == x,

Specification for [<i32 as Clone>::clone]

Source

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

Specification for [<i32 as PartialEq<i32>>::eq]

Source

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

Specification for [<i32 as PartialEq<i32>>::ne]

Source

pub unsafe exec fn _verus_external_fn_specification_358__60__32_i32_32_as_32_Ord_32__62__32__58__58__32_cmp( x: &i32, y: &i32, ) -> Ordering

Specification for [<i32 as Ord>::cmp]

Source

pub unsafe exec fn _verus_external_fn_specification_359__60__32_i32_32_as_32_PartialOrd_32__60__32_i32_32__62__32__62__32__58__58__32_partial__cmp( x: &i32, y: &i32, ) -> Option<Ordering>

Specification for [<i32 as PartialOrd<i32>>::partial_cmp]

Source

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

Specification for [<i32 as PartialOrd<i32>>::lt]

Source

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

Specification for [<i32 as PartialOrd<i32>>::le]

Source

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

Specification for [<i32 as PartialOrd<i32>>::gt]

Source

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

Specification for [<i32 as PartialOrd<i32>>::ge]

Source

pub unsafe exec fn _verus_external_fn_specification_364__60__32_i32_32__62__32__58__58__32_wrapping__add( x: i32, y: i32, ) -> i32

Specification for i32::wrapping_add

Source

pub unsafe exec fn _verus_external_fn_specification_365__60__32_i32_32__62__32__58__58__32_wrapping__add__unsigned( x: i32, y: u32, ) -> i32

Specification for i32::wrapping_add_unsigned

Source

pub unsafe exec fn _verus_external_fn_specification_366__60__32_i32_32__62__32__58__58__32_wrapping__sub( x: i32, y: i32, ) -> res : i32

Specification for i32::wrapping_sub

Source

pub unsafe exec fn _verus_external_fn_specification_367__60__32_i32_32__62__32__58__58__32_wrapping__mul( x: i32, y: i32, ) -> i32

Specification for i32::wrapping_mul

Source

pub unsafe exec fn _verus_external_fn_specification_368__60__32_i32_32__62__32__58__58__32_checked__add( x: i32, y: i32, ) -> Option<i32>

Specification for i32::checked_add

Source

pub unsafe exec fn _verus_external_fn_specification_369__60__32_i32_32__62__32__58__58__32_checked__add__unsigned( x: i32, y: u32, ) -> Option<i32>

Specification for i32::checked_add_unsigned

Source

pub unsafe exec fn _verus_external_fn_specification_370__60__32_u32_32__62__32__58__58__32_saturating__add( x: u32, y: u32, ) -> u32

Specification for u32::saturating_add

Source

pub unsafe exec fn _verus_external_fn_specification_371__60__32_i32_32__62__32__58__58__32_checked__sub( x: i32, y: i32, ) -> Option<i32>

Specification for i32::checked_sub

Source

pub unsafe exec fn _verus_external_fn_specification_372__60__32_i32_32__62__32__58__58__32_checked__sub__unsigned( x: i32, y: u32, ) -> Option<i32>

Specification for i32::checked_sub_unsigned

Source

pub unsafe exec fn _verus_external_fn_specification_373__60__32_i32_32__62__32__58__58__32_checked__mul( x: i32, y: i32, ) -> Option<i32>

Specification for i32::checked_mul

Source§

impl VstdSpecsForRustStdLib

Source

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

ensures
res == x,

Specification for [<u64 as Clone>::clone]

Source

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

Specification for [<u64 as PartialEq<u64>>::eq]

Source

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

Specification for [<u64 as PartialEq<u64>>::ne]

Source

pub unsafe exec fn _verus_external_fn_specification_377__60__32_u64_32_as_32_Ord_32__62__32__58__58__32_cmp( x: &u64, y: &u64, ) -> Ordering

Specification for [<u64 as Ord>::cmp]

Source

pub unsafe exec fn _verus_external_fn_specification_378__60__32_u64_32_as_32_PartialOrd_32__60__32_u64_32__62__32__62__32__58__58__32_partial__cmp( x: &u64, y: &u64, ) -> Option<Ordering>

Specification for [<u64 as PartialOrd<u64>>::partial_cmp]

Source

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

Specification for [<u64 as PartialOrd<u64>>::lt]

Source

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

Specification for [<u64 as PartialOrd<u64>>::le]

Source

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

Specification for [<u64 as PartialOrd<u64>>::gt]

Source

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

Specification for [<u64 as PartialOrd<u64>>::ge]

Source

pub unsafe exec fn _verus_external_fn_specification_383__60__32_u64_32__62__32__58__58__32_wrapping__add( x: u64, y: u64, ) -> u64

Specification for u64::wrapping_add

Source

pub unsafe exec fn _verus_external_fn_specification_384__60__32_u64_32__62__32__58__58__32_wrapping__add__signed( x: u64, y: i64, ) -> u64

Specification for u64::wrapping_add_signed

Source

pub unsafe exec fn _verus_external_fn_specification_385__60__32_u64_32__62__32__58__58__32_wrapping__sub( x: u64, y: u64, ) -> u64

Specification for u64::wrapping_sub

Source

pub unsafe exec fn _verus_external_fn_specification_386__60__32_u64_32__62__32__58__58__32_wrapping__mul( x: u64, y: u64, ) -> u64

Specification for u64::wrapping_mul

Source

pub unsafe exec fn _verus_external_fn_specification_387__60__32_u64_32__62__32__58__58__32_checked__add( x: u64, y: u64, ) -> Option<u64>

Specification for u64::checked_add

Source

pub unsafe exec fn _verus_external_fn_specification_388__60__32_u64_32__62__32__58__58__32_checked__add__signed( x: u64, y: i64, ) -> Option<u64>

Specification for u64::checked_add_signed

Source

pub unsafe exec fn _verus_external_fn_specification_389__60__32_u64_32__62__32__58__58__32_checked__sub( x: u64, y: u64, ) -> Option<u64>

Specification for u64::checked_sub

Source

pub unsafe exec fn _verus_external_fn_specification_390__60__32_u64_32__62__32__58__58__32_checked__mul( x: u64, y: u64, ) -> Option<u64>

Specification for u64::checked_mul

Source

pub unsafe exec fn _verus_external_fn_specification_391__60__32_u64_32__62__32__58__58__32_checked__div( lhs: u64, rhs: u64, ) -> result : Option<u64>

ensures
result == checked_div(lhs, rhs),

Specification for u64::checked_div

Source

pub unsafe exec fn _verus_external_fn_specification_392__60__32_u64_32__62__32__58__58__32_checked__div__euclid( lhs: u64, rhs: u64, ) -> result : Option<u64>

ensures
result == checked_div(lhs, rhs),

Specification for u64::checked_div_euclid

Source§

impl VstdSpecsForRustStdLib

Source

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

ensures
res == x,

Specification for [<i64 as Clone>::clone]

Source

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

Specification for [<i64 as PartialEq<i64>>::eq]

Source

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

Specification for [<i64 as PartialEq<i64>>::ne]

Source

pub unsafe exec fn _verus_external_fn_specification_396__60__32_i64_32_as_32_Ord_32__62__32__58__58__32_cmp( x: &i64, y: &i64, ) -> Ordering

Specification for [<i64 as Ord>::cmp]

Source

pub unsafe exec fn _verus_external_fn_specification_397__60__32_i64_32_as_32_PartialOrd_32__60__32_i64_32__62__32__62__32__58__58__32_partial__cmp( x: &i64, y: &i64, ) -> Option<Ordering>

Specification for [<i64 as PartialOrd<i64>>::partial_cmp]

Source

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

Specification for [<i64 as PartialOrd<i64>>::lt]

Source

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

Specification for [<i64 as PartialOrd<i64>>::le]

Source

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

Specification for [<i64 as PartialOrd<i64>>::gt]

Source

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

Specification for [<i64 as PartialOrd<i64>>::ge]

Source

pub unsafe exec fn _verus_external_fn_specification_402__60__32_i64_32__62__32__58__58__32_wrapping__add( x: i64, y: i64, ) -> i64

Specification for i64::wrapping_add

Source

pub unsafe exec fn _verus_external_fn_specification_403__60__32_i64_32__62__32__58__58__32_wrapping__add__unsigned( x: i64, y: u64, ) -> i64

Specification for i64::wrapping_add_unsigned

Source

pub unsafe exec fn _verus_external_fn_specification_404__60__32_i64_32__62__32__58__58__32_wrapping__sub( x: i64, y: i64, ) -> res : i64

Specification for i64::wrapping_sub

Source

pub unsafe exec fn _verus_external_fn_specification_405__60__32_i64_32__62__32__58__58__32_wrapping__mul( x: i64, y: i64, ) -> i64

Specification for i64::wrapping_mul

Source

pub unsafe exec fn _verus_external_fn_specification_406__60__32_i64_32__62__32__58__58__32_checked__add( x: i64, y: i64, ) -> Option<i64>

Specification for i64::checked_add

Source

pub unsafe exec fn _verus_external_fn_specification_407__60__32_i64_32__62__32__58__58__32_checked__add__unsigned( x: i64, y: u64, ) -> Option<i64>

Specification for i64::checked_add_unsigned

Source

pub unsafe exec fn _verus_external_fn_specification_408__60__32_u64_32__62__32__58__58__32_saturating__add( x: u64, y: u64, ) -> u64

Specification for u64::saturating_add

Source

pub unsafe exec fn _verus_external_fn_specification_409__60__32_i64_32__62__32__58__58__32_checked__sub( x: i64, y: i64, ) -> Option<i64>

Specification for i64::checked_sub

Source

pub unsafe exec fn _verus_external_fn_specification_410__60__32_i64_32__62__32__58__58__32_checked__sub__unsigned( x: i64, y: u64, ) -> Option<i64>

Specification for i64::checked_sub_unsigned

Source

pub unsafe exec fn _verus_external_fn_specification_411__60__32_i64_32__62__32__58__58__32_checked__mul( x: i64, y: i64, ) -> Option<i64>

Specification for i64::checked_mul

Source§

impl VstdSpecsForRustStdLib

Source

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

ensures
res == x,

Specification for [<u128 as Clone>::clone]

Source

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

Specification for [<u128 as PartialEq<u128>>::eq]

Source

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

Specification for [<u128 as PartialEq<u128>>::ne]

Source

pub unsafe exec fn _verus_external_fn_specification_415__60__32_u128_32_as_32_Ord_32__62__32__58__58__32_cmp( x: &u128, y: &u128, ) -> Ordering

Specification for [<u128 as Ord>::cmp]

Source

pub unsafe exec fn _verus_external_fn_specification_416__60__32_u128_32_as_32_PartialOrd_32__60__32_u128_32__62__32__62__32__58__58__32_partial__cmp( x: &u128, y: &u128, ) -> Option<Ordering>

Specification for [<u128 as PartialOrd<u128>>::partial_cmp]

Source

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

Specification for [<u128 as PartialOrd<u128>>::lt]

Source

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

Specification for [<u128 as PartialOrd<u128>>::le]

Source

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

Specification for [<u128 as PartialOrd<u128>>::gt]

Source

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

Specification for [<u128 as PartialOrd<u128>>::ge]

Source

pub unsafe exec fn _verus_external_fn_specification_421__60__32_u128_32__62__32__58__58__32_wrapping__add( x: u128, y: u128, ) -> u128

Specification for u128::wrapping_add

Source

pub unsafe exec fn _verus_external_fn_specification_422__60__32_u128_32__62__32__58__58__32_wrapping__add__signed( x: u128, y: i128, ) -> u128

Specification for u128::wrapping_add_signed

Source

pub unsafe exec fn _verus_external_fn_specification_423__60__32_u128_32__62__32__58__58__32_wrapping__sub( x: u128, y: u128, ) -> u128

Specification for u128::wrapping_sub

Source

pub unsafe exec fn _verus_external_fn_specification_424__60__32_u128_32__62__32__58__58__32_wrapping__mul( x: u128, y: u128, ) -> u128

Specification for u128::wrapping_mul

Source

pub unsafe exec fn _verus_external_fn_specification_425__60__32_u128_32__62__32__58__58__32_checked__add( x: u128, y: u128, ) -> Option<u128>

Specification for u128::checked_add

Source

pub unsafe exec fn _verus_external_fn_specification_426__60__32_u128_32__62__32__58__58__32_checked__add__signed( x: u128, y: i128, ) -> Option<u128>

Specification for u128::checked_add_signed

Source

pub unsafe exec fn _verus_external_fn_specification_427__60__32_u128_32__62__32__58__58__32_checked__sub( x: u128, y: u128, ) -> Option<u128>

Specification for u128::checked_sub

Source

pub unsafe exec fn _verus_external_fn_specification_428__60__32_u128_32__62__32__58__58__32_checked__mul( x: u128, y: u128, ) -> Option<u128>

Specification for u128::checked_mul

Source

pub unsafe exec fn _verus_external_fn_specification_429__60__32_u128_32__62__32__58__58__32_checked__div( lhs: u128, rhs: u128, ) -> result : Option<u128>

ensures
result == checked_div(lhs, rhs),

Specification for u128::checked_div

Source

pub unsafe exec fn _verus_external_fn_specification_430__60__32_u128_32__62__32__58__58__32_checked__div__euclid( lhs: u128, rhs: u128, ) -> result : Option<u128>

ensures
result == checked_div(lhs, rhs),

Specification for u128::checked_div_euclid

Source§

impl VstdSpecsForRustStdLib

Source

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

ensures
res == x,

Specification for [<i128 as Clone>::clone]

Source

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

Specification for [<i128 as PartialEq<i128>>::eq]

Source

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

Specification for [<i128 as PartialEq<i128>>::ne]

Source

pub unsafe exec fn _verus_external_fn_specification_434__60__32_i128_32_as_32_Ord_32__62__32__58__58__32_cmp( x: &i128, y: &i128, ) -> Ordering

Specification for [<i128 as Ord>::cmp]

Source

pub unsafe exec fn _verus_external_fn_specification_435__60__32_i128_32_as_32_PartialOrd_32__60__32_i128_32__62__32__62__32__58__58__32_partial__cmp( x: &i128, y: &i128, ) -> Option<Ordering>

Specification for [<i128 as PartialOrd<i128>>::partial_cmp]

Source

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

Specification for [<i128 as PartialOrd<i128>>::lt]

Source

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

Specification for [<i128 as PartialOrd<i128>>::le]

Source

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

Specification for [<i128 as PartialOrd<i128>>::gt]

Source

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

Specification for [<i128 as PartialOrd<i128>>::ge]

Source

pub unsafe exec fn _verus_external_fn_specification_440__60__32_i128_32__62__32__58__58__32_wrapping__add( x: i128, y: i128, ) -> i128

Specification for i128::wrapping_add

Source

pub unsafe exec fn _verus_external_fn_specification_441__60__32_i128_32__62__32__58__58__32_wrapping__add__unsigned( x: i128, y: u128, ) -> i128

Specification for i128::wrapping_add_unsigned

Source

pub unsafe exec fn _verus_external_fn_specification_442__60__32_i128_32__62__32__58__58__32_wrapping__sub( x: i128, y: i128, ) -> res : i128

Specification for i128::wrapping_sub

Source

pub unsafe exec fn _verus_external_fn_specification_443__60__32_i128_32__62__32__58__58__32_wrapping__mul( x: i128, y: i128, ) -> i128

Specification for i128::wrapping_mul

Source

pub unsafe exec fn _verus_external_fn_specification_444__60__32_i128_32__62__32__58__58__32_checked__add( x: i128, y: i128, ) -> Option<i128>

Specification for i128::checked_add

Source

pub unsafe exec fn _verus_external_fn_specification_445__60__32_i128_32__62__32__58__58__32_checked__add__unsigned( x: i128, y: u128, ) -> Option<i128>

Specification for i128::checked_add_unsigned

Source

pub unsafe exec fn _verus_external_fn_specification_446__60__32_u128_32__62__32__58__58__32_saturating__add( x: u128, y: u128, ) -> u128

Specification for u128::saturating_add

Source

pub unsafe exec fn _verus_external_fn_specification_447__60__32_i128_32__62__32__58__58__32_checked__sub( x: i128, y: i128, ) -> Option<i128>

Specification for i128::checked_sub

Source

pub unsafe exec fn _verus_external_fn_specification_448__60__32_i128_32__62__32__58__58__32_checked__sub__unsigned( x: i128, y: u128, ) -> Option<i128>

Specification for i128::checked_sub_unsigned

Source

pub unsafe exec fn _verus_external_fn_specification_449__60__32_i128_32__62__32__58__58__32_checked__mul( x: i128, y: i128, ) -> Option<i128>

Specification for i128::checked_mul

Source§

impl VstdSpecsForRustStdLib

Source

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

ensures
res == x,

Specification for [<usize as Clone>::clone]

Source

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

Specification for [<usize as PartialEq<usize>>::eq]

Source

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

Specification for [<usize as PartialEq<usize>>::ne]

Source

pub unsafe exec fn _verus_external_fn_specification_453__60__32_usize_32_as_32_Ord_32__62__32__58__58__32_cmp( x: &usize, y: &usize, ) -> Ordering

Specification for [<usize as Ord>::cmp]

Source

pub unsafe exec fn _verus_external_fn_specification_454__60__32_usize_32_as_32_PartialOrd_32__60__32_usize_32__62__32__62__32__58__58__32_partial__cmp( x: &usize, y: &usize, ) -> Option<Ordering>

Specification for [<usize as PartialOrd<usize>>::partial_cmp]

Source

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

Specification for [<usize as PartialOrd<usize>>::lt]

Source

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

Specification for [<usize as PartialOrd<usize>>::le]

Source

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

Specification for [<usize as PartialOrd<usize>>::gt]

Source

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

Specification for [<usize as PartialOrd<usize>>::ge]

Source

pub unsafe exec fn _verus_external_fn_specification_459__60__32_usize_32__62__32__58__58__32_wrapping__add( x: usize, y: usize, ) -> usize

Specification for usize::wrapping_add

Source

pub unsafe exec fn _verus_external_fn_specification_460__60__32_usize_32__62__32__58__58__32_wrapping__add__signed( x: usize, y: isize, ) -> usize

Specification for usize::wrapping_add_signed

Source

pub unsafe exec fn _verus_external_fn_specification_461__60__32_usize_32__62__32__58__58__32_wrapping__sub( x: usize, y: usize, ) -> usize

Specification for usize::wrapping_sub

Source

pub unsafe exec fn _verus_external_fn_specification_462__60__32_usize_32__62__32__58__58__32_wrapping__mul( x: usize, y: usize, ) -> usize

Specification for usize::wrapping_mul

Source

pub unsafe exec fn _verus_external_fn_specification_463__60__32_usize_32__62__32__58__58__32_checked__add( x: usize, y: usize, ) -> Option<usize>

Specification for usize::checked_add

Source

pub unsafe exec fn _verus_external_fn_specification_464__60__32_usize_32__62__32__58__58__32_checked__add__signed( x: usize, y: isize, ) -> Option<usize>

Specification for usize::checked_add_signed

Source

pub unsafe exec fn _verus_external_fn_specification_465__60__32_usize_32__62__32__58__58__32_checked__sub( x: usize, y: usize, ) -> Option<usize>

Specification for usize::checked_sub

Source

pub unsafe exec fn _verus_external_fn_specification_466__60__32_usize_32__62__32__58__58__32_checked__mul( x: usize, y: usize, ) -> Option<usize>

Specification for usize::checked_mul

Source

pub unsafe exec fn _verus_external_fn_specification_467__60__32_usize_32__62__32__58__58__32_checked__div( lhs: usize, rhs: usize, ) -> result : Option<usize>

ensures
result == checked_div(lhs, rhs),

Specification for usize::checked_div

Source

pub unsafe exec fn _verus_external_fn_specification_468__60__32_usize_32__62__32__58__58__32_checked__div__euclid( lhs: usize, rhs: usize, ) -> result : Option<usize>

ensures
result == checked_div(lhs, rhs),

Specification for usize::checked_div_euclid

Source§

impl VstdSpecsForRustStdLib

Source

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

ensures
res == x,

Specification for [<isize as Clone>::clone]

Source

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

Specification for [<isize as PartialEq<isize>>::eq]

Source

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

Specification for [<isize as PartialEq<isize>>::ne]

Source

pub unsafe exec fn _verus_external_fn_specification_472__60__32_isize_32_as_32_Ord_32__62__32__58__58__32_cmp( x: &isize, y: &isize, ) -> Ordering

Specification for [<isize as Ord>::cmp]

Source

pub unsafe exec fn _verus_external_fn_specification_473__60__32_isize_32_as_32_PartialOrd_32__60__32_isize_32__62__32__62__32__58__58__32_partial__cmp( x: &isize, y: &isize, ) -> Option<Ordering>

Specification for [<isize as PartialOrd<isize>>::partial_cmp]

Source

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

Specification for [<isize as PartialOrd<isize>>::lt]

Source

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

Specification for [<isize as PartialOrd<isize>>::le]

Source

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

Specification for [<isize as PartialOrd<isize>>::gt]

Source

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

Specification for [<isize as PartialOrd<isize>>::ge]

Source

pub unsafe exec fn _verus_external_fn_specification_478__60__32_isize_32__62__32__58__58__32_wrapping__add( x: isize, y: isize, ) -> isize

Specification for isize::wrapping_add

Source

pub unsafe exec fn _verus_external_fn_specification_479__60__32_isize_32__62__32__58__58__32_wrapping__add__unsigned( x: isize, y: usize, ) -> isize

Specification for isize::wrapping_add_unsigned

Source

pub unsafe exec fn _verus_external_fn_specification_480__60__32_isize_32__62__32__58__58__32_wrapping__sub( x: isize, y: isize, ) -> res : isize

Specification for isize::wrapping_sub

Source

pub unsafe exec fn _verus_external_fn_specification_481__60__32_isize_32__62__32__58__58__32_wrapping__mul( x: isize, y: isize, ) -> isize

Specification for isize::wrapping_mul

Source

pub unsafe exec fn _verus_external_fn_specification_482__60__32_isize_32__62__32__58__58__32_checked__add( x: isize, y: isize, ) -> Option<isize>

Specification for isize::checked_add

Source

pub unsafe exec fn _verus_external_fn_specification_483__60__32_isize_32__62__32__58__58__32_checked__add__unsigned( x: isize, y: usize, ) -> Option<isize>

Specification for isize::checked_add_unsigned

Source

pub unsafe exec fn _verus_external_fn_specification_484__60__32_usize_32__62__32__58__58__32_saturating__add( x: usize, y: usize, ) -> usize

Specification for usize::saturating_add

Source

pub unsafe exec fn _verus_external_fn_specification_485__60__32_isize_32__62__32__58__58__32_checked__sub( x: isize, y: isize, ) -> Option<isize>

Specification for isize::checked_sub

Source

pub unsafe exec fn _verus_external_fn_specification_486__60__32_isize_32__62__32__58__58__32_checked__sub__unsigned( x: isize, y: usize, ) -> Option<isize>

Specification for isize::checked_sub_unsigned

Source

pub unsafe exec fn _verus_external_fn_specification_487__60__32_isize_32__62__32__58__58__32_checked__mul( x: isize, y: isize, ) -> Option<isize>

Specification for isize::checked_mul

Source§

impl VstdSpecsForRustStdLib

Source

pub unsafe exec fn _verus_external_fn_specification_488_u32_32__58__58__32_checked__rem( lhs: u32, rhs: u32, ) -> result : Option<u32>

ensures
rhs == 0 ==> result is None,
rhs != 0 ==> result == Some((lhs % rhs) as u32),

Specification for u32::checked_rem

Source

pub unsafe exec fn _verus_external_fn_specification_489_u32_32__58__58__32_checked__rem__euclid( lhs: u32, rhs: u32, ) -> result : Option<u32>

ensures
rhs == 0 ==> result is None,
rhs != 0 ==> result == Some((lhs % rhs) as u32),

Specification for u32::checked_rem_euclid

Source

pub unsafe exec fn _verus_external_fn_specification_490_i32_32__58__58__32_checked__div( lhs: i32, rhs: i32, ) -> result : Option<i32>

ensures
rhs == 0 ==> result is None,
({
    let x = lhs as int;
    let d = rhs as int;
    let output = if x == 0 {
        0
    } else if x > 0 && d > 0 {
        x / d
    } else if x < 0 && d < 0 {
        ((x * -1) / (d * -1))
    } else if x < 0 {
        ((x * -1) / d) * -1
    } else {
        (x / (d * -1)) * -1
    };
    if output < i32::MIN || output > i32::MAX {
        result is None
    } else {
        result == Some(output as i32)
    }
}),

Specification for i32::checked_div

Source

pub unsafe exec fn _verus_external_fn_specification_491_i32_32__58__58__32_checked__div__euclid( lhs: i32, rhs: i32, ) -> result : Option<i32>

ensures
rhs == 0 ==> result is None,
lhs / rhs < i32::MIN || lhs / rhs > i32::MAX ==> result is None,
i32::MIN <= lhs / rhs <= i32::MAX ==> result == Some((lhs / rhs) as i32),

Specification for i32::checked_div_euclid

Source

pub unsafe exec fn _verus_external_fn_specification_492_i32_32__58__58__32_checked__rem( lhs: i32, rhs: i32, ) -> result : Option<i32>

ensures
rhs == 0 ==> result is None,
({
    let x = lhs as int;
    let d = rhs as int;
    let output = if x == 0 {
        0
    } else if x > 0 && d > 0 {
        x % d
    } else if x < 0 && d < 0 {
        ((x * -1) % (d * -1)) * -1
    } else if x < 0 {
        ((x * -1) % d) * -1
    } else {
        x % (d * -1)
    };
    if output < i32::MIN || output > i32::MAX {
        result is None
    } else {
        result == Some(output as i32)
    }
}),

Specification for i32::checked_rem

Source

pub unsafe exec fn _verus_external_fn_specification_493_i32_32__58__58__32_checked__rem__euclid( lhs: i32, rhs: i32, ) -> result : Option<i32>

ensures
rhs == 0 ==> result is None,
lhs % rhs < i32::MIN || lhs % rhs > i32::MAX ==> result is None,
i32::MIN <= lhs % rhs <= i32::MAX ==> result == Some((lhs % rhs) as i32),

Specification for i32::checked_rem_euclid

Source§

impl VstdSpecsForRustStdLib

Source

pub unsafe exec fn _verus_external_fn_specification_494_Option_32__58__58__32__60__32_T_32__62__32__58__58__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_495_Option_32__58__58__32__60__32_T_32__62__32__58__58__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_496_Option_32__58__58__32__60__32_T_32__62__32__58__58__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_497_Option_32__58__58__32__60__32_T_32__62__32__58__58__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_498_Option_32__58__58__32__60__32_T_32__62__32__58__58__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_499_Option_32__58__58__32__60__32_T_32__62__32__58__58__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_500_Option_32__58__58__32__60__32_T_32__62__32__58__58__32_take<T>( option: &mut Option<T>, ) -> t : Option<T>

ensures
t == old(option),
*option is None,

Specification for Option::<T>::take

Source

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

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_502__60__32_Option_32__60__32_T_32__62__32_as_32_Clone_32__62__32__58__58__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_503__60__32_Option_32__60__32_T_32__62__32_as_32_PartialEq_32__62__32__58__58__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_504__60__32_Option_32__60__32_T_32__62__32_as_32_PartialOrd_32__62__32__58__58__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_505__60__32_Option_32__60__32_T_32__62__32_as_32_Ord_32__62__32__58__58__32_cmp<T: Ord>( x: &Option<T>, y: &Option<T>, ) -> Ordering

Specification for [<Option<T> as Ord>::cmp]

Source

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

ensures
res == spec_ok_or(option, err),

Specification for Option::ok_or

Source§

impl VstdSpecsForRustStdLib

Source

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

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

Specification for Range::<A>::next

Source

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

ensures
(U::obeys_partial_cmp_spec() && <Idx as PartialOrdSpec<U>>::obeys_partial_cmp_spec())
    ==> ret == (r.start.is_le(i) && i.is_lt(&r.end)),

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§

impl VstdSpecsForRustStdLib

Source

pub unsafe exec fn _verus_external_fn_specification_509_Result_32__58__58__32__60__32_T_44__32_E_32__62__32__58__58__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_510_Result_32__58__58__32__60__32_T_44__32_E_32__62__32__58__58__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_511_Result_32__58__58__32__60__32_T_44__32_E_32__62__32__58__58__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_512_Result_32__58__58__32__60__32_T_44__32_E_32__62__32__58__58__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_513_Result_32__58__58__32__60__32_T_44__32_E_32__62__32__58__58__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_514_Result_32__58__58__32__60__32_T_44__32_E_32__62__32__58__58__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_515_Result_32__58__58__32__60__32_T_44__32_E_32__62__32__58__58__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_516_Result_32__58__58__32__60__32_T_44__32_E_32__62__32__58__58__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_517_Result_32__58__58__32__60__32_T_44__32_E_32__62__32__58__58__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_518_Result_32__58__58__32__60__32_T_44__32_E_32__62__32__58__58__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_519_core_32__58__58__32_hint_32__58__58__32_unreachable__unchecked() -> !

requires
false,

Specification for core::hint::unreachable_unchecked

Source

pub unsafe exec fn _verus_external_fn_specification_520_Iter_32__58__58__32__60__32__39_a_44__32_T_32__62__32__58__58__32_next<'a, T>( elements: &mut Iter<'a, T>, ) -> r : Option<&'a T>

ensures
({
    let (old_index, old_seq) = old(elements)@;
    match r {
        None => (
            &&& elements@ == old(elements)@
            &&& old_index >= old_seq.len()

        ),
        Some(element) => {
            let (new_index, new_seq) = elements@;
            &&& 0 <= old_index < old_seq.len()
            &&& new_seq == old_seq
            &&& new_index == old_index + 1
            &&& element == old_seq[old_index]

        }
    }
}),

Specification for [Iter::<'a, T>::next]

Source

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

ensures
({
    let (index, seq) = iter@;
    &&& index == 0
    &&& seq == s@

}),

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

Source§

impl VstdSpecsForRustStdLib

Source

pub unsafe exec fn _verus_external_fn_specification_522_Vec_32__58__58__32__60__32_T_44__32_A_32__62__32__58__58__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_523_Vec_32__58__58__32__60__32_T_32__62__32__58__58__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_524_Vec_32__58__58__32__60__32_T_32__62__32__58__58__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_525_Vec_32__58__58__32__60__32_T_44__32_A_32__62__32__58__58__32_reserve<T, A: Allocator>( vec: &mut Vec<T, A>, additional: usize, )

ensures
vec@ == old(vec)@,

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

Source

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

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

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

Source

pub unsafe exec fn _verus_external_fn_specification_527_Vec_32__58__58__32__60__32_T_44__32_A_32__62__32__58__58__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])
        && vec@ == old(vec)@.subrange(0, old(vec)@.len() - 1),
old(vec)@.len() == 0 ==> value == None::<T> && vec@ == old(vec)@,

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

Source

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

ensures
vec@ == old(vec)@ + old(other)@,
other@ == Seq::<T>::empty(),

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

Source

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

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

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

Source

pub unsafe exec fn _verus_external_fn_specification_530_Vec_32__58__58__32__60__32_T_44__32_A_32__62__32__58__58__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],
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_531_Vec_32__58__58__32__60__32_T_44__32_A_32__62__32__58__58__32_insert<T, A: Allocator>( vec: &mut Vec<T, A>, i: usize, element: T, )

requires
i <= old(vec).len(),
ensures
vec@ == old(vec)@.insert(i as int, element),

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

Source

pub unsafe exec fn _verus_external_fn_specification_532_Vec_32__58__58__32__60__32_T_44__32_A_32__62__32__58__58__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],
vec@ == old(vec)@.remove(i as int),

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

Source

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

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

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

Source

pub unsafe exec fn _verus_external_fn_specification_534_Vec_32__58__58__32__60__32_T_44__32_A_32__62__32__58__58__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_535__60__32_Vec_32__60__32_T_44__32_A_32__62__32_as_32_core_32__58__58__32_ops_32__58__58__32_Deref_32__62__32__58__58__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_536_Vec_32__58__58__32__60__32_T_44__32_A_32__62__32__58__58__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
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_537__60__32_Vec_32__60__32_T_44__32_A_32__62__32_as_32_Clone_32__62__32__58__58__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_538_Vec_32__58__58__32__60__32_T_44__32_A_32__62__32__58__58__32_truncate<T, A: Allocator>( vec: &mut Vec<T, A>, len: usize, )

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

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

Source

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

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

    },

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

Source

pub unsafe exec fn _verus_external_fn_specification_540_IntoIter_32__58__58__32__60__32_T_44__32_A_32__62__32__58__58__32_next<T, A: Allocator>( elements: &mut IntoIter<T, A>, ) -> r : Option<T>

ensures
({
    let (old_index, old_seq) = old(elements)@;
    match r {
        None => (
            &&& elements@ == old(elements)@
            &&& old_index >= old_seq.len()

        ),
        Some(element) => {
            let (new_index, new_seq) = elements@;
            &&& 0 <= old_index < old_seq.len()
            &&& new_seq == old_seq
            &&& new_index == old_index + 1
            &&& element == old_seq[old_index]

        }
    }
}),

Specification for IntoIter::<T, A>::next

Source

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

ensures
iter@ == (0int, vec@),

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

Source§

impl VstdSpecsForRustStdLib

Source

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

requires
i < v.len(),
ensures
result == v.spec_index(i as int),

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

Source

pub unsafe exec fn _verus_external_fn_specification_543_VecDeque_32__58__58__32__60__32_T_44__32_A_32__62__32__58__58__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_544_VecDeque_32__58__58__32__60__32_T_32__62__32__58__58__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_545_VecDeque_32__58__58__32__60__32_T_32__62__32__58__58__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_546_VecDeque_32__58__58__32__60__32_T_44__32_A_32__62__32__58__58__32_reserve<T, A: Allocator>( v: &mut VecDeque<T, A>, additional: usize, )

ensures
v@ == old(v)@,

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

Source

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

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

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

Source

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

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

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

Source

pub unsafe exec fn _verus_external_fn_specification_549_VecDeque_32__58__58__32__60__32_T_44__32_A_32__62__32__58__58__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]
        &&& v@ == old(v)@.subrange(0, old(v)@.len() as int - 1)

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

    ),
},

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

Source

pub unsafe exec fn _verus_external_fn_specification_550_VecDeque_32__58__58__32__60__32_T_44__32_A_32__62__32__58__58__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]
        &&& v@ == old(v)@.subrange(1, old(v)@.len() as int)

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

    ),
},

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

Source

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

ensures
v@ == old(v)@ + old(other)@,
other@ == Seq::<T>::empty(),

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

Source

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

requires
i <= old(v).len(),
ensures
v@ == old(v)@.insert(i as int, element),

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

Source

pub unsafe exec fn _verus_external_fn_specification_553_VecDeque_32__58__58__32__60__32_T_44__32_A_32__62__32__58__58__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]
        &&& v@ == old(v)@.remove(i as int)

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

    ),
},

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

Source

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

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

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

Source

pub unsafe exec fn _verus_external_fn_specification_555_VecDeque_32__58__58__32__60__32_T_44__32_A_32__62__32__58__58__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
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_556__60__32_VecDeque_32__60__32_T_44__32_A_32__62__32_as_32_Clone_32__62__32__58__58__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_557_VecDeque_32__58__58__32__60__32_T_44__32_A_32__62__32__58__58__32_truncate<T, A: Allocator>( v: &mut VecDeque<T, A>, len: usize, )

ensures
len <= old(v).len() ==> v@ == old(v)@.subrange(0, len as int),
len > old(v).len() ==> v@ == old(v)@,

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

Source

pub unsafe exec fn _verus_external_fn_specification_558_VecDeque_32__58__58__32__60__32_T_44__32_A_32__62__32__58__58__32_resize<T: Clone, A: Allocator>( v: &mut VecDeque<T, A>, len: usize, value: T, )

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

    },

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

Source

pub unsafe exec fn _verus_external_fn_specification_559_Iter_32__58__58__32__60__32__39_a_44__32_T_32__62__32__58__58__32_next<'a, T>( elements: &mut Iter<'a, T>, ) -> r : Option<&'a T>

ensures
({
    let (old_index, old_seq) = old(elements)@;
    match r {
        None => (
            &&& elements@ == old(elements)@
            &&& old_index >= old_seq.len()

        ),
        Some(element) => {
            let (new_index, new_seq) = elements@;
            &&& 0 <= old_index < old_seq.len()
            &&& new_seq == old_seq
            &&& new_index == old_index + 1
            &&& element == old_seq[old_index]

        }
    }
}),

Specification for [Iter::<'a, T>::next]

Source

pub unsafe exec fn _verus_external_fn_specification_560_VecDeque_32__58__58__32__60__32_T_44__32_A_32__62__32__58__58__32_iter<'a, T, A: Allocator>( v: &'a VecDeque<T, A>, ) -> r : Iter<'a, T>

ensures
r@ == (0int, v@),

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

Source§

impl VstdSpecsForRustStdLib

Source

pub unsafe exec fn _verus_external_fn_specification_561__60__32__91_T_93__32__62__32__58__58__32_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_562_Box_32__58__58__32__60__32_T_32__62__32__58__58__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_563_Rc_32__58__58__32__60__32_T_32__62__32__58__58__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_564_Arc_32__58__58__32__60__32_T_32__62__32__58__58__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_565__60__32_Box_32__60__32_T_44__32_A_32__62__32_as_32_Clone_32__62__32__58__58__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_566_Rc_32__58__58__32__60__32_T_44__32_A_32__62__32__58__58__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_567_Rc_32__58__58__32__60__32_T_44__32_A_32__62__32__58__58__32_into__inner<T, A: Allocator>( v: Rc<T, A>, ) -> result : Option<T>

ensures
result matches Some(t) ==> t == v,

Specification for Rc::<T, A>::into_inner

Auto Trait Implementations§

Blanket Implementations§

Source§

impl<T> Any for T
where T: 'static + ?Sized,

Source§

fn type_id(&self) -> TypeId

Gets the TypeId of self. Read more
Source§

impl<T> Borrow<T> for T
where T: ?Sized,

Source§

fn borrow(&self) -> &T

Immutably borrows from an owned value. Read more
Source§

impl<T> BorrowMut<T> for T
where T: ?Sized,

Source§

fn borrow_mut(&mut self) -> &mut T

Mutably borrows from an owned value. Read more
Source§

impl<T> From<T> for T

Source§

fn from(t: T) -> T

Returns the argument unchanged.

Source§

impl<T, U> Into<U> for T
where U: From<T>,

Source§

fn into(self) -> U

Calls U::from(self).

That is, this conversion is whatever the implementation of From<T> for U chooses to do.

Source§

impl<T, U> TryFrom<U> 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<U>>::Error>

Performs the conversion.
Source§

impl<T, U> TryInto<U> for T
where U: TryFrom<T>,

Source§

type Error = <U as TryFrom<T>>::Error

The type returned in the event of a conversion error.
Source§

fn try_into(self) -> Result<U, <U as TryFrom<T>>::Error>

Performs the conversion.