Struct vstd::std_specs::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
is_sized::<V>(),
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
is_sized::<V>(),
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_427__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_428__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_425__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_426__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_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_4_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_5__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_6__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_7_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_8_str_32__58__58__32_to__string( s: &str, ) -> res : String

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

Specification for str::to_string

source

pub unsafe exec fn _verus_external_fn_specification_9_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_10_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_11__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_12__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§

impl VstdSpecsForRustStdLib

source

pub unsafe exec fn _verus_external_fn_specification_415__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_416__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_417__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_418__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_419__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_420__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_421__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_422__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_423__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_424__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_411__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_412__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_413__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_414__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_401__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_402__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_403__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_404__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_405__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_406__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_407__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_408__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_409__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_410__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_397__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_398__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_399__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_400__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_387__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_388__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_389__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_390__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_391__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_392__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_393__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_394__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_395__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_396__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_383__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_384__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_385__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_386__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_373__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_374__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_375__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_376__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_377__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_378__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_379__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_380__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_381__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_382__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_369__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_370__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_371__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_372__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_359__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_360__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_361__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_362__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_363__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_364__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_365__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_366__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_367__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_368__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_355__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_356__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_357__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_358__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_345__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_346__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_347__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_348__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_349__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_350__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_351__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_352__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_353__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_354__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_341__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_342__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_343__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_344__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_331__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_332__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_333__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_334__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_335__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_336__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_337__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_338__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_339__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_340__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_327__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_328__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_329__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_330__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_317__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_318__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_319__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_320__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_321__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_322__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_323__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_324__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_325__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_326__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_313__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_314__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_315__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_316__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_303__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_304__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_305__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_306__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_307__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_308__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_309__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_310__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_311__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_312__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_299__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_300__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_301__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_302__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_289__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_290__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_291__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_292__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_293__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_294__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_295__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_296__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_297__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_298__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_285__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_286__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_287__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_288__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_275__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_276__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_277__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_278__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_279__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_280__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_281__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_282__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_283__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_284__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_13_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_14_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_15_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_16_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_17_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_18_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_19_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_20_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_21_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_22_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_23_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_24_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_25_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_26_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_27_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_28_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_29__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_30__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_31__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_32__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_33__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_34_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_35_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_36_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_37_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_38_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_39_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_40_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_41_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_42_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_43_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

pub unsafe exec fn _verus_external_fn_specification_44_core_32__58__58__32_hint_32__58__58__32_unreachable__unchecked() -> !

requires
false,

Specification for core::hint::unreachable_unchecked

source§

impl VstdSpecsForRustStdLib

source

pub unsafe exec fn _verus_external_fn_specification_45__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_46__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_47__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_48__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_49__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_50__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_51__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_52__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_53__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_54__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_55__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_56__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_57_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_58_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_59_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_60_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_61_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_62_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_63_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_64_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_65_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_66_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_67_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_68_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_69_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_70_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_71_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 [Iter::<'a, Key>::next]

source

pub unsafe exec fn _verus_external_fn_specification_72_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_73_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_74_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_75_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_76_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_77_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_78_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_79_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_80_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_81_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_82__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_83__60__32_u8_32__62__32__58__58__32_wrapping__add( x: u8, y: u8, ) -> res : u8

ensures
res == wrapping_add(x, y),

Specification for u8::wrapping_add

source

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

ensures
res == wrapping_add_signed(x, y),

Specification for u8::wrapping_add_signed

source

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

ensures
res == wrapping_sub(x, y),

Specification for u8::wrapping_sub

source

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

ensures
res == checked_add(x, y),

Specification for u8::checked_add

source

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

ensures
res == checked_add_signed(x, y),

Specification for u8::checked_add_signed

source

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

ensures
res == checked_sub(x, y),

Specification for u8::checked_sub

source

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

ensures
result == checked_mul(lhs, rhs),

Specification for u8::checked_mul

source

pub unsafe exec fn _verus_external_fn_specification_90__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_91__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_92__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_93__60__32_i8_32__62__32__58__58__32_wrapping__add( x: i8, y: i8, ) -> res : i8

ensures
res == wrapping_add(x, y),

Specification for i8::wrapping_add

source

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

ensures
res == wrapping_add_unsigned(x, y),

Specification for i8::wrapping_add_unsigned

source

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

ensures
res == wrapping_sub(x, y),

Specification for i8::wrapping_sub

source

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

ensures
res == wrapping_mul(x, y),

Specification for i8::wrapping_mul

source

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

ensures
res == checked_add(x, y),

Specification for i8::checked_add

source

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

ensures
res == checked_add_unsigned(x, y),

Specification for i8::checked_add_unsigned

source

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

ensures
res == saturating_add(x, y),

Specification for u8::saturating_add

source

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

ensures
res == checked_sub(x, y),

Specification for i8::checked_sub

source

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

ensures
res == checked_sub_unsigned(x, y),

Specification for i8::checked_sub_unsigned

source

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

ensures
res == checked_mul(x, y),

Specification for i8::checked_mul

source§

impl VstdSpecsForRustStdLib

source

pub unsafe exec fn _verus_external_fn_specification_103__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_104__60__32_u16_32__62__32__58__58__32_wrapping__add( x: u16, y: u16, ) -> res : u16

ensures
res == wrapping_add(x, y),

Specification for u16::wrapping_add

source

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

ensures
res == wrapping_add_signed(x, y),

Specification for u16::wrapping_add_signed

source

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

ensures
res == wrapping_sub(x, y),

Specification for u16::wrapping_sub

source

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

ensures
res == checked_add(x, y),

Specification for u16::checked_add

source

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

ensures
res == checked_add_signed(x, y),

Specification for u16::checked_add_signed

source

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

ensures
res == checked_sub(x, y),

Specification for u16::checked_sub

source

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

ensures
result == checked_mul(lhs, rhs),

Specification for u16::checked_mul

source

pub unsafe exec fn _verus_external_fn_specification_111__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_112__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_113__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_114__60__32_i16_32__62__32__58__58__32_wrapping__add( x: i16, y: i16, ) -> res : i16

ensures
res == wrapping_add(x, y),

Specification for i16::wrapping_add

source

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

ensures
res == wrapping_add_unsigned(x, y),

Specification for i16::wrapping_add_unsigned

source

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

ensures
res == wrapping_sub(x, y),

Specification for i16::wrapping_sub

source

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

ensures
res == wrapping_mul(x, y),

Specification for i16::wrapping_mul

source

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

ensures
res == checked_add(x, y),

Specification for i16::checked_add

source

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

ensures
res == checked_add_unsigned(x, y),

Specification for i16::checked_add_unsigned

source

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

ensures
res == saturating_add(x, y),

Specification for u16::saturating_add

source

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

ensures
res == checked_sub(x, y),

Specification for i16::checked_sub

source

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

ensures
res == checked_sub_unsigned(x, y),

Specification for i16::checked_sub_unsigned

source

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

ensures
res == checked_mul(x, y),

Specification for i16::checked_mul

source§

impl VstdSpecsForRustStdLib

source

pub unsafe exec fn _verus_external_fn_specification_124__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_125__60__32_u32_32__62__32__58__58__32_wrapping__add( x: u32, y: u32, ) -> res : u32

ensures
res == wrapping_add(x, y),

Specification for u32::wrapping_add

source

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

ensures
res == wrapping_add_signed(x, y),

Specification for u32::wrapping_add_signed

source

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

ensures
res == wrapping_sub(x, y),

Specification for u32::wrapping_sub

source

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

ensures
res == checked_add(x, y),

Specification for u32::checked_add

source

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

ensures
res == checked_add_signed(x, y),

Specification for u32::checked_add_signed

source

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

ensures
res == checked_sub(x, y),

Specification for u32::checked_sub

source

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

ensures
result == checked_mul(lhs, rhs),

Specification for u32::checked_mul

source

pub unsafe exec fn _verus_external_fn_specification_132__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_133__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_134__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_135__60__32_i32_32__62__32__58__58__32_wrapping__add( x: i32, y: i32, ) -> res : i32

ensures
res == wrapping_add(x, y),

Specification for i32::wrapping_add

source

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

ensures
res == wrapping_add_unsigned(x, y),

Specification for i32::wrapping_add_unsigned

source

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

ensures
res == wrapping_sub(x, y),

Specification for i32::wrapping_sub

source

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

ensures
res == wrapping_mul(x, y),

Specification for i32::wrapping_mul

source

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

ensures
res == checked_add(x, y),

Specification for i32::checked_add

source

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

ensures
res == checked_add_unsigned(x, y),

Specification for i32::checked_add_unsigned

source

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

ensures
res == saturating_add(x, y),

Specification for u32::saturating_add

source

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

ensures
res == checked_sub(x, y),

Specification for i32::checked_sub

source

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

ensures
res == checked_sub_unsigned(x, y),

Specification for i32::checked_sub_unsigned

source

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

ensures
res == checked_mul(x, y),

Specification for i32::checked_mul

source§

impl VstdSpecsForRustStdLib

source

pub unsafe exec fn _verus_external_fn_specification_145__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_146__60__32_u64_32__62__32__58__58__32_wrapping__add( x: u64, y: u64, ) -> res : u64

ensures
res == wrapping_add(x, y),

Specification for u64::wrapping_add

source

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

ensures
res == wrapping_add_signed(x, y),

Specification for u64::wrapping_add_signed

source

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

ensures
res == wrapping_sub(x, y),

Specification for u64::wrapping_sub

source

pub unsafe exec fn _verus_external_fn_specification_149__60__32_u64_32__62__32__58__58__32_checked__add( x: u64, y: u64, ) -> res : Option<u64>

ensures
res == checked_add(x, y),

Specification for u64::checked_add

source

pub unsafe exec fn _verus_external_fn_specification_150__60__32_u64_32__62__32__58__58__32_checked__add__signed( x: u64, y: i64, ) -> res : Option<u64>

ensures
res == checked_add_signed(x, y),

Specification for u64::checked_add_signed

source

pub unsafe exec fn _verus_external_fn_specification_151__60__32_u64_32__62__32__58__58__32_checked__sub( x: u64, y: u64, ) -> res : Option<u64>

ensures
res == checked_sub(x, y),

Specification for u64::checked_sub

source

pub unsafe exec fn _verus_external_fn_specification_152__60__32_u64_32__62__32__58__58__32_checked__mul( lhs: u64, rhs: u64, ) -> result : Option<u64>

ensures
result == checked_mul(lhs, rhs),

Specification for u64::checked_mul

source

pub unsafe exec fn _verus_external_fn_specification_153__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_154__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_155__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_156__60__32_i64_32__62__32__58__58__32_wrapping__add( x: i64, y: i64, ) -> res : i64

ensures
res == wrapping_add(x, y),

Specification for i64::wrapping_add

source

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

ensures
res == wrapping_add_unsigned(x, y),

Specification for i64::wrapping_add_unsigned

source

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

ensures
res == wrapping_sub(x, y),

Specification for i64::wrapping_sub

source

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

ensures
res == wrapping_mul(x, y),

Specification for i64::wrapping_mul

source

pub unsafe exec fn _verus_external_fn_specification_160__60__32_i64_32__62__32__58__58__32_checked__add( x: i64, y: i64, ) -> res : Option<i64>

ensures
res == checked_add(x, y),

Specification for i64::checked_add

source

pub unsafe exec fn _verus_external_fn_specification_161__60__32_i64_32__62__32__58__58__32_checked__add__unsigned( x: i64, y: u64, ) -> res : Option<i64>

ensures
res == checked_add_unsigned(x, y),

Specification for i64::checked_add_unsigned

source

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

ensures
res == saturating_add(x, y),

Specification for u64::saturating_add

source

pub unsafe exec fn _verus_external_fn_specification_163__60__32_i64_32__62__32__58__58__32_checked__sub( x: i64, y: i64, ) -> res : Option<i64>

ensures
res == checked_sub(x, y),

Specification for i64::checked_sub

source

pub unsafe exec fn _verus_external_fn_specification_164__60__32_i64_32__62__32__58__58__32_checked__sub__unsigned( x: i64, y: u64, ) -> res : Option<i64>

ensures
res == checked_sub_unsigned(x, y),

Specification for i64::checked_sub_unsigned

source

pub unsafe exec fn _verus_external_fn_specification_165__60__32_i64_32__62__32__58__58__32_checked__mul( x: i64, y: i64, ) -> res : Option<i64>

ensures
res == checked_mul(x, y),

Specification for i64::checked_mul

source§

impl VstdSpecsForRustStdLib

source

pub unsafe exec fn _verus_external_fn_specification_166__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_167__60__32_u128_32__62__32__58__58__32_wrapping__add( x: u128, y: u128, ) -> res : u128

ensures
res == wrapping_add(x, y),

Specification for u128::wrapping_add

source

pub unsafe exec fn _verus_external_fn_specification_168__60__32_u128_32__62__32__58__58__32_wrapping__add__signed( x: u128, y: i128, ) -> res : u128

ensures
res == wrapping_add_signed(x, y),

Specification for u128::wrapping_add_signed

source

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

ensures
res == wrapping_sub(x, y),

Specification for u128::wrapping_sub

source

pub unsafe exec fn _verus_external_fn_specification_170__60__32_u128_32__62__32__58__58__32_checked__add( x: u128, y: u128, ) -> res : Option<u128>

ensures
res == checked_add(x, y),

Specification for u128::checked_add

source

pub unsafe exec fn _verus_external_fn_specification_171__60__32_u128_32__62__32__58__58__32_checked__add__signed( x: u128, y: i128, ) -> res : Option<u128>

ensures
res == checked_add_signed(x, y),

Specification for u128::checked_add_signed

source

pub unsafe exec fn _verus_external_fn_specification_172__60__32_u128_32__62__32__58__58__32_checked__sub( x: u128, y: u128, ) -> res : Option<u128>

ensures
res == checked_sub(x, y),

Specification for u128::checked_sub

source

pub unsafe exec fn _verus_external_fn_specification_173__60__32_u128_32__62__32__58__58__32_checked__mul( lhs: u128, rhs: u128, ) -> result : Option<u128>

ensures
result == checked_mul(lhs, rhs),

Specification for u128::checked_mul

source

pub unsafe exec fn _verus_external_fn_specification_174__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_175__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_176__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_177__60__32_i128_32__62__32__58__58__32_wrapping__add( x: i128, y: i128, ) -> res : i128

ensures
res == wrapping_add(x, y),

Specification for i128::wrapping_add

source

pub unsafe exec fn _verus_external_fn_specification_178__60__32_i128_32__62__32__58__58__32_wrapping__add__unsigned( x: i128, y: u128, ) -> res : i128

ensures
res == wrapping_add_unsigned(x, y),

Specification for i128::wrapping_add_unsigned

source

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

ensures
res == wrapping_sub(x, y),

Specification for i128::wrapping_sub

source

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

ensures
res == wrapping_mul(x, y),

Specification for i128::wrapping_mul

source

pub unsafe exec fn _verus_external_fn_specification_181__60__32_i128_32__62__32__58__58__32_checked__add( x: i128, y: i128, ) -> res : Option<i128>

ensures
res == checked_add(x, y),

Specification for i128::checked_add

source

pub unsafe exec fn _verus_external_fn_specification_182__60__32_i128_32__62__32__58__58__32_checked__add__unsigned( x: i128, y: u128, ) -> res : Option<i128>

ensures
res == checked_add_unsigned(x, y),

Specification for i128::checked_add_unsigned

source

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

ensures
res == saturating_add(x, y),

Specification for u128::saturating_add

source

pub unsafe exec fn _verus_external_fn_specification_184__60__32_i128_32__62__32__58__58__32_checked__sub( x: i128, y: i128, ) -> res : Option<i128>

ensures
res == checked_sub(x, y),

Specification for i128::checked_sub

source

pub unsafe exec fn _verus_external_fn_specification_185__60__32_i128_32__62__32__58__58__32_checked__sub__unsigned( x: i128, y: u128, ) -> res : Option<i128>

ensures
res == checked_sub_unsigned(x, y),

Specification for i128::checked_sub_unsigned

source

pub unsafe exec fn _verus_external_fn_specification_186__60__32_i128_32__62__32__58__58__32_checked__mul( x: i128, y: i128, ) -> res : Option<i128>

ensures
res == checked_mul(x, y),

Specification for i128::checked_mul

source§

impl VstdSpecsForRustStdLib

source

pub unsafe exec fn _verus_external_fn_specification_187__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_188__60__32_usize_32__62__32__58__58__32_wrapping__add( x: usize, y: usize, ) -> res : usize

ensures
res == wrapping_add(x, y),

Specification for usize::wrapping_add

source

pub unsafe exec fn _verus_external_fn_specification_189__60__32_usize_32__62__32__58__58__32_wrapping__add__signed( x: usize, y: isize, ) -> res : usize

ensures
res == wrapping_add_signed(x, y),

Specification for usize::wrapping_add_signed

source

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

ensures
res == wrapping_sub(x, y),

Specification for usize::wrapping_sub

source

pub unsafe exec fn _verus_external_fn_specification_191__60__32_usize_32__62__32__58__58__32_checked__add( x: usize, y: usize, ) -> res : Option<usize>

ensures
res == checked_add(x, y),

Specification for usize::checked_add

source

pub unsafe exec fn _verus_external_fn_specification_192__60__32_usize_32__62__32__58__58__32_checked__add__signed( x: usize, y: isize, ) -> res : Option<usize>

ensures
res == checked_add_signed(x, y),

Specification for usize::checked_add_signed

source

pub unsafe exec fn _verus_external_fn_specification_193__60__32_usize_32__62__32__58__58__32_checked__sub( x: usize, y: usize, ) -> res : Option<usize>

ensures
res == checked_sub(x, y),

Specification for usize::checked_sub

source

pub unsafe exec fn _verus_external_fn_specification_194__60__32_usize_32__62__32__58__58__32_checked__mul( lhs: usize, rhs: usize, ) -> result : Option<usize>

ensures
result == checked_mul(lhs, rhs),

Specification for usize::checked_mul

source

pub unsafe exec fn _verus_external_fn_specification_195__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_196__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_197__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_198__60__32_isize_32__62__32__58__58__32_wrapping__add( x: isize, y: isize, ) -> res : isize

ensures
res == wrapping_add(x, y),

Specification for isize::wrapping_add

source

pub unsafe exec fn _verus_external_fn_specification_199__60__32_isize_32__62__32__58__58__32_wrapping__add__unsigned( x: isize, y: usize, ) -> res : isize

ensures
res == wrapping_add_unsigned(x, y),

Specification for isize::wrapping_add_unsigned

source

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

ensures
res == wrapping_sub(x, y),

Specification for isize::wrapping_sub

source

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

ensures
res == wrapping_mul(x, y),

Specification for isize::wrapping_mul

source

pub unsafe exec fn _verus_external_fn_specification_202__60__32_isize_32__62__32__58__58__32_checked__add( x: isize, y: isize, ) -> res : Option<isize>

ensures
res == checked_add(x, y),

Specification for isize::checked_add

source

pub unsafe exec fn _verus_external_fn_specification_203__60__32_isize_32__62__32__58__58__32_checked__add__unsigned( x: isize, y: usize, ) -> res : Option<isize>

ensures
res == checked_add_unsigned(x, y),

Specification for isize::checked_add_unsigned

source

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

ensures
res == saturating_add(x, y),

Specification for usize::saturating_add

source

pub unsafe exec fn _verus_external_fn_specification_205__60__32_isize_32__62__32__58__58__32_checked__sub( x: isize, y: isize, ) -> res : Option<isize>

ensures
res == checked_sub(x, y),

Specification for isize::checked_sub

source

pub unsafe exec fn _verus_external_fn_specification_206__60__32_isize_32__62__32__58__58__32_checked__sub__unsigned( x: isize, y: usize, ) -> res : Option<isize>

ensures
res == checked_sub_unsigned(x, y),

Specification for isize::checked_sub_unsigned

source

pub unsafe exec fn _verus_external_fn_specification_207__60__32_isize_32__62__32__58__58__32_checked__mul( x: isize, y: isize, ) -> res : Option<isize>

ensures
res == checked_mul(x, y),

Specification for isize::checked_mul

source§

impl VstdSpecsForRustStdLib

source

pub unsafe exec fn _verus_external_fn_specification_208_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_209_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_210_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_211_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_212_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_213_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_214_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_215_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_216_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.get_Some_0() == a.get_Some_0(),

Specification for Option::<T>::as_ref

source

pub unsafe exec fn _verus_external_fn_specification_217_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_218_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_219_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_220_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_221__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_222_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_223_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§

impl VstdSpecsForRustStdLib

source

pub unsafe exec fn _verus_external_fn_specification_224_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_225_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_226_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.get_Ok_0() == r.get_Ok_0(),
r.is_Err() <==> result.is_Err(),
r.is_Err() ==> result.get_Err_0() == r.get_Err_0(),

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

source

pub unsafe exec fn _verus_external_fn_specification_227_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.get_Ok_0(),

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

source

pub unsafe exec fn _verus_external_fn_specification_228_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.get_Err_0(),

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

source

pub unsafe exec fn _verus_external_fn_specification_229_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.get_Ok_0(),)),
ensures
result.is_ok()
    ==> mapped_result.is_ok()
        && op.ensures((result.get_Ok_0(),), mapped_result.get_Ok_0()),
result.is_err() ==> mapped_result == Result::<U, E>::Err(result.get_Err_0()),

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

source

pub unsafe exec fn _verus_external_fn_specification_230_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.get_Err_0(),)),
ensures
result.is_err()
    ==> mapped_result.is_err()
        && op.ensures((result.get_Err_0(),), mapped_result.get_Err_0()),
result.is_ok() ==> mapped_result == Result::<T, F>::Ok(result.get_Ok_0()),

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

source

pub unsafe exec fn _verus_external_fn_specification_231_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_232_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_233_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_234_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_235_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_236_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_237_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_238_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_239_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_240_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_241_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_242_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_243_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_244_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_245_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_246__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_247_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_248_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§

impl VstdSpecsForRustStdLib

source

pub unsafe exec fn _verus_external_fn_specification_249_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_250_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_251_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_252_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_253_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_254_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_255_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_256_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_257_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_258_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_259_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_260_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_261_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_262_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_263__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_264_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_265_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_266_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_267_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_268__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_269_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_270_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_271_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_272__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_273_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_274_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.