Struct VstdSpecsForRustStdLib

Source

pub struct VstdSpecsForRustStdLib;

Implementations§

Source §

impl VstdSpecsForRustStdLib

Source

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

ensures

IteratorSpec::remaining(&iter) == s@.as_ref(),

IteratorSpec::decrease(&iter) is Some,

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

Source

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

ensures

ar@ == out@,

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

Source §

impl VstdSpecsForRustStdLib

Source

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

ensures

res == f,

Specification for <f32 as Clone>::clone

Source

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

ensures

res == f,

Specification for <f64 as Clone>::clone

Source §

impl VstdSpecsForRustStdLib

Source

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

ensures

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

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

Source

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

ensures

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

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

Source

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

ensures

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

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

Source

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

ensures

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

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

Source §

impl VstdSpecsForRustStdLib

Source

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

ensures

addr == spec_addr(p),

Specification for <*mut T>::addr

Source

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

ensures

q == spec_with_addr(p, addr),

Specification for <*mut T>::with_addr

Source §

impl VstdSpecsForRustStdLib

Source

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

ensures

addr == spec_addr(p),

Specification for <*const T>::addr

Source

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

ensures

q == spec_with_addr(p, addr),

Specification for <*const T>::with_addr

Source §

impl VstdSpecsForRustStdLib

Source

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

ensures

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

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

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

Source

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

ensures

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

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

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

Source

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

ensures

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

Specification for core::ptr::null

Source

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

ensures

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

Specification for core::ptr::null_mut

Source §

impl VstdSpecsForRustStdLib

Source

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

returns

spec_slice_len(slice),

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

Source

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

ensures

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

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

Source §

impl VstdSpecsForRustStdLib

Source

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

ensures

b == is_ascii(s),

Specification for str::is_ascii

Source

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

ensures

s@ == res@,

Specification for str::to_owned

Source

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

ensures

b@ == s.spec_bytes(),

Specification for str::as_bytes

Source

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

returns

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

Specification for str::len

Source

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

returns

s@.len() == 0,

Specification for str::is_empty

Source

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

returns

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

Specification for str::is_char_boundary

Source

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

requires

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

ensures

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

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

Specification for str::split_at

Source

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

requires

valid_utf8(v@),

ensures

res.spec_bytes() =~= v@,

Specification for str::from_utf8_unchecked

Source

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

ensures

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

Specification for <T as ToString>::to_string

Source

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

ensures

res@ == s@,

Specification for String::as_str

Source

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

ensures

res@ == s@,

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

Source

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

ensures

res == s,

Specification for <String as Clone>::clone

Source

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

ensures

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

Specification for <String as PartialEq>::eq

Source

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

ensures

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

Specification for String::new

Source

pub unsafe exec fn _verus_external_fn_specification_28_String_325858__32_push( s: &mut String, c: char, )

ensures

final(s)@ == old(s)@.push(c),

Specification for String::push

Source

pub unsafe exec fn _verus_external_fn_specification_29_String_325858__32_pop( s: &mut String, ) -> res : Option<char>

ensures

old(s)@.len() == 0 ==> res is None && final(s)@ == old(s)@,

old(s)@.len() > 0 ==> res == Some(old(s)@.last()) && final(s)@ == old(s)@.drop_last(),

Specification for String::pop

Source

pub unsafe exec fn _verus_external_fn_specification_30_String_325858__32_push__str( s: &mut String, other: &str, )

ensures

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

Specification for String::push_str

Source

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

ensures

res == (s@.len() == 0),

Specification for String::is_empty

Source

pub unsafe exec fn _verus_external_fn_specification_32_String_325858__32_clear( s: &mut String, )

ensures

final(s)@ == Seq::<char>::empty(),

Specification for String::clear

Source

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

ensures

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

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

Source

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

ensures

IteratorSpec::remaining(&iter) == s@,

IteratorSpec::decrease(&iter) is Some,

Specification for str::chars

Source §

impl VstdSpecsForRustStdLib

Source

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

requires

vals.mem_contents() is Init,

ensures

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

Specification for [alloc::boxed::box_assume_init_into_vec_unsafe]

Source

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

ensures

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

Specification for alloc::intrinsics::write_box_via_move

Source

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

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

Source §

Source §

impl VstdSpecsForRustStdLib

Source

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

Specification for AtomicU8::fetch_add

Source

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

Specification for AtomicU8::fetch_sub

Source

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

Specification for AtomicU8::fetch_min

Source

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

Specification for AtomicU8::fetch_max

Source §

Specification for AtomicU16::swap

Source §

impl VstdSpecsForRustStdLib

Source

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

Specification for AtomicU16::fetch_add

Source

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

Specification for AtomicU16::fetch_sub

Source

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

Specification for AtomicU16::fetch_min

Source

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

Specification for AtomicU16::fetch_max

Source §

Specification for AtomicU32::swap

Source §

impl VstdSpecsForRustStdLib

Source

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

Specification for AtomicU32::fetch_add

Source

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

Specification for AtomicU32::fetch_sub

Source

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

Specification for AtomicU32::fetch_min

Source

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

Specification for AtomicU32::fetch_max

Source §

Specification for AtomicU64::swap

Source §

impl VstdSpecsForRustStdLib

Source

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

Specification for AtomicU64::fetch_add

Source

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

Specification for AtomicU64::fetch_sub

Source

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

Specification for AtomicU64::fetch_min

Source

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

Specification for AtomicU64::fetch_max

Source §

Specification for AtomicUsize::swap

Source §

impl VstdSpecsForRustStdLib

Source

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

Specification for AtomicUsize::fetch_add

Source

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

Specification for AtomicUsize::fetch_sub

Source

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

Specification for AtomicUsize::fetch_min

Source

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

Specification for AtomicUsize::fetch_max

Source §

Specification for AtomicI8::swap

Source §

impl VstdSpecsForRustStdLib

Source

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

Specification for AtomicI8::fetch_add

Source

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

Specification for AtomicI8::fetch_sub

Source

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

Specification for AtomicI8::fetch_min

Source

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

Specification for AtomicI8::fetch_max

Source §

Specification for AtomicI16::swap

Source §

impl VstdSpecsForRustStdLib

Source

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

Specification for AtomicI16::fetch_add

Source

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

Specification for AtomicI16::fetch_sub

Source

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

Specification for AtomicI16::fetch_min

Source

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

Specification for AtomicI16::fetch_max

Source §

Specification for AtomicI32::swap

Source §

impl VstdSpecsForRustStdLib

Source

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

Specification for AtomicI32::fetch_add

Source

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

Specification for AtomicI32::fetch_sub

Source

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

Specification for AtomicI32::fetch_min

Source

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

Specification for AtomicI32::fetch_max

Source §

Specification for AtomicI64::swap

Source §

impl VstdSpecsForRustStdLib

Source

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

Specification for AtomicI64::fetch_add

Source

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

Specification for AtomicI64::fetch_sub

Source

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

Specification for AtomicI64::fetch_min

Source

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

Specification for AtomicI64::fetch_max

Source §

Specification for AtomicIsize::swap

Source §

impl VstdSpecsForRustStdLib

Source

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

Specification for AtomicIsize::fetch_add

Source

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

Specification for AtomicIsize::fetch_sub

Source

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

Specification for AtomicIsize::fetch_min

Source

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

Specification for AtomicIsize::fetch_max

Source §

Specification for AtomicBool::swap

Source §

impl VstdSpecsForRustStdLib

Source

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

ensures

r == u8_trailing_zeros(i),

Specification for u8::trailing_zeros

Source

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

ensures

r == u8_trailing_ones(i),

Specification for u8::trailing_ones

Source

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

ensures

r == u8_leading_zeros(i),

Specification for u8::leading_zeros

Source

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

ensures

r == u8_leading_ones(i),

Specification for u8::leading_ones

Source

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

ensures

r == u16_trailing_zeros(i),

Specification for u16::trailing_zeros

Source

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

ensures

r == u16_trailing_ones(i),

Specification for u16::trailing_ones

Source

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

ensures

r == u16_leading_zeros(i),

Specification for u16::leading_zeros

Source

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

ensures

r == u16_leading_ones(i),

Specification for u16::leading_ones

Source

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

ensures

r == u32_trailing_zeros(i),

Specification for u32::trailing_zeros

Source

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

ensures

r == u32_trailing_ones(i),

Specification for u32::trailing_ones

Source

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

ensures

r == u32_leading_zeros(i),

Specification for u32::leading_zeros

Source

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

ensures

r == u32_leading_ones(i),

Specification for u32::leading_ones

Source

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

ensures

r == u64_trailing_zeros(i),

Specification for u64::trailing_zeros

Source

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

ensures

r == u64_trailing_ones(i),

Specification for u64::trailing_ones

Source

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

ensures

r as int == u64_leading_zeros(i),

Specification for u64::leading_zeros

Source

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

ensures

r == u64_leading_ones(i),

Specification for u64::leading_ones

Source §

impl VstdSpecsForRustStdLib

Source

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

returns

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

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

Source

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

returns

is_white_space(c),

Specification for char::is_whitespace

Source §

impl VstdSpecsForRustStdLib

Source

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

returns

b,

Specification for <bool as Clone>::clone

Source

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

returns

c,

Specification for <char as Clone>::clone

Source

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

ensures

res == b,

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

Source

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

ensures

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

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

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

Source

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

ensures

res == b,

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

Source

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

ensures

res == b,

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

Source §

impl VstdSpecsForRustStdLib

Source

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

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

Source

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

ensures

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

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

Source

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

ensures

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

Specification for Option::<T>::branch

Source

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

ensures

option.is_none(),

option2.is_none(),

Specification for Option::<T>::from_residual

Source

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

ensures

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

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

Source §

impl VstdSpecsForRustStdLib

Source

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

ensures

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

Specification for <T as Into>::into

Source

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

ensures

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

Specification for <T as TryInto>::try_into

Source

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

ensures

ret.is_ok(),

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

Specification for <T as TryFrom>::try_from

Source §

Source

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

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

Source

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

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

Source

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

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

Source

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

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

Source §

impl VstdSpecsForRustStdLib

Source

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

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

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

Source

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

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

Source §

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

Source §

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

Source §

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

Source §

Source §

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

ensures

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

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

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

Source

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

ensures

c == b,

Specification for core::intrinsics::likely

Source

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

ensures

c == b,

Specification for core::intrinsics::unlikely

Source

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

requires

b ==> f.requires(()),

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_365_core_325858__32_hint_325858__32_must__use<T>( value: T, ) -> ret : T

ensures

ret == value,

Specification for core::hint::must_use

Source

pub unsafe exec fn _verus_external_fn_specification_366_core_325858__32_panicking_325858__32_panic( s: &'static str, ) -> !

requires

false,

Specification for core::panicking::panic

Source

pub unsafe exec fn _verus_external_fn_specification_367_core_325858__32_panicking_325858__32_panic__fmt( s: Arguments<'_>, ) -> !

requires

false,

Specification for core::panicking::panic_fmt

Source §

impl VstdSpecsForRustStdLib

Source

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

ensures

r == false,

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

Source §

impl VstdSpecsForRustStdLib

Source

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

ensures

r == '\0',

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

Source §

impl VstdSpecsForRustStdLib

Source

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

ensures

r == 0.0f32,

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

Source §

impl VstdSpecsForRustStdLib

Source

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

ensures

r == 0.0f64,

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

Source §

impl VstdSpecsForRustStdLib

Source

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

ensures

r == 0i8,

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

Source §

impl VstdSpecsForRustStdLib

Source

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

ensures

r == 0i16,

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

Source §

impl VstdSpecsForRustStdLib

Source

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

ensures

r == 0i32,

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

Source §

impl VstdSpecsForRustStdLib

Source

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

ensures

r == 0i64,

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

Source §

impl VstdSpecsForRustStdLib

Source

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

ensures

r == 0i128,

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

Source §

impl VstdSpecsForRustStdLib

Source

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

ensures

r == 0isize,

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

Source §

impl VstdSpecsForRustStdLib

Source

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

ensures

r == 0u8,

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

Source §

impl VstdSpecsForRustStdLib

Source

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

ensures

r == 0u16,

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

Source §

impl VstdSpecsForRustStdLib

Source

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

ensures

r == 0u32,

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

Source §

impl VstdSpecsForRustStdLib

Source

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

ensures

r == 0u64,

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

Source §

impl VstdSpecsForRustStdLib

Source

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

ensures

r == 0u128,

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

Source §

impl VstdSpecsForRustStdLib

Source

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

ensures

r == (),

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

Source §

impl VstdSpecsForRustStdLib

Source

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

ensures

r == 0usize,

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

Source §

impl VstdSpecsForRustStdLib

Source

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

ensures

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

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

Source

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

ensures

r == "",

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

Source

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

ensures

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

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

Source

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

ensures

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

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

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

Source

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

ensures

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

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

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

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

Source §

impl VstdSpecsForRustStdLib

Source

pub unsafe exec fn _verus_external_fn_specification_392_Arguments_32585832603239_a_3262325858__32_from__str<'a>( s: &'static str, ) -> Arguments<'a>

Specification for Arguments::<'a>::from_str

Source

pub unsafe exec fn _verus_external_fn_specification_393_Arguments_32585832603239_a_3262325858__32_fromstrnonconst<'a>( s: &'static str, ) -> Arguments<'a>

Specification for Arguments::<'a>::from_str_nonconst

Source

pub unsafe exec fn _verus_external_fn_specification_395_alloc_325858__32_fmt_325858__32_format( args: Arguments<'_>, ) -> String

Specification for alloc::fmt::format

Source §

impl VstdSpecsForRustStdLib

Source

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

ensures

r == i,

Specification for ::into_iter

Source §

impl VstdSpecsForRustStdLib

Source

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

ensures

res@ == value,

Specification for ManuallyDrop::<T>::new

Source

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

returns

m@,

Specification for ManuallyDrop::<T>::into_inner

Source

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

ensures

cloned(m@, res@),

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

Source

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

returns

m.view_ref(),

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

Source §

impl VstdSpecsForRustStdLib

Source

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

ensures

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

Specification for MaybeUninit::<T>::new

Source

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

ensures

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

Specification for MaybeUninit::<T>::uninit

Source

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

requires

m.mem_contents().is_init(),

returns

m.mem_contents().value(),

Specification for MaybeUninit::<T>::assume_init

Source

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

requires

m.mem_contents().is_init(),

ensures

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

Specification for MaybeUninit::<T>::assume_init_ref

Source

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

requires

m.mem_contents().is_init(),

ensures

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

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

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

Specification for MaybeUninit::<T>::assume_init_mut

Source §

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

Source §

Source §

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

Source §

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

Source §

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

Source §

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

Source §

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

Source §

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

Source §

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

Source §

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

Source §

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

Source §

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

Source §

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

Source §

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

Source §

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

Source §

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

Source §

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

Source §

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

Source §

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

Source §

Source §

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

Source §

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

Source §

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

Source §

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

Source §

impl VstdSpecsForRustStdLib

Source

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

ensures

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

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

Source

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

ensures

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

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

Source

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

ensures

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

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

Source

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

ensures

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

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

Source

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

ensures

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

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

Source

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

ensures

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

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

Source

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

ensures

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

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

Source

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

ensures

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

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

Source

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

ensures

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

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

Source

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

ensures

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

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

Source §

impl VstdSpecsForRustStdLib

Source

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

ensures

key_obeys_cmp_spec::<Key>()
    ==> {
        &&& IteratorSpec::remaining(&iter).len() == m@.dom().len()
        &&& forall |i: int| {
            0 <= i < IteratorSpec::remaining(&iter).len()
                ==> m@.contains_key(*IteratorSpec::remaining(&iter)[i].0)
                    && m@[*IteratorSpec::remaining(&iter)[i].0]
                        == *IteratorSpec::remaining(&iter)[i].1
        }
        &&& forall |k: Key| (
            #[trigger] m@.contains_key(k)
                ==> IteratorSpec::remaining(&iter).contains((&k, &m@[k]))
        )
        &&& IteratorSpec::remaining(&iter).unref().to_set() == m@.kv_pairs()
        &&& iter.remaining().no_duplicates()
        &&& into_iter(iter) == IteratorSpec::remaining(&iter).unref()
        &&& IteratorSpec::decrease(&iter) is Some
        &&& increasing_seq(iter.remaining().map_values(|kv: (&Key, &Value)| *kv.0))

    },

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

Source

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

ensures

len == spec_btree_map_len(m),

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

Source

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

ensures

res == m@.is_empty(),

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

Source

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

ensures

other@ == this@,

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

Source

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

ensures

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

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

Source

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

ensures

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

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

Source

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

ensures

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

    },

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

Source

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

ensures

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

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

Source

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

ensures

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

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

Source

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

ensures

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

    },

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

Source

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

ensures

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

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

Source

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

ensures

key_obeys_cmp_spec::<Key>()
    ==> {
        &&& IteratorSpec::remaining(&keys).unref().to_set() == m@.dom()
        &&& IteratorSpec::remaining(&keys).no_duplicates()
        &&& IteratorSpec::remaining(&keys).len() == m@.dom().len()
        &&& increasing_seq(IteratorSpec::remaining(&keys))
        &&& into_iter_keys(keys) == IteratorSpec::remaining(&keys).unref()
        &&& IteratorSpec::decrease(&keys) is Some

    },

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

Source

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

ensures

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

        }

    },

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

Source

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

ensures

len == spec_btree_set_len(m),

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

Source

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

ensures

res == m@.is_empty(),

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

Source

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

ensures

other@ == this@,

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

Source

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

ensures

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

Specification for BTreeSet::<Key>::new

Source

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

ensures

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

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

Source

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

ensures

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

    },

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

Source

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

ensures

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

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

Source

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

ensures

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

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

Source

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

ensures

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

    },

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

Source

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

ensures

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

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

Source

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

ensures

key_obeys_cmp_spec::<Key>()
    ==> {
        &&& IteratorSpec::remaining(&r).unref().to_set() == m@
        &&& IteratorSpec::remaining(&r).no_duplicates()
        &&& IteratorSpec::remaining(&r).len() == m@.len()
        &&& increasing_seq(IteratorSpec::remaining(&r))
        &&& into_iter_btree_keys(r) == IteratorSpec::remaining(&r).unref()
        &&& IteratorSpec::decrease(&r) is Some

    },

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

Source §

impl VstdSpecsForRustStdLib

Source

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

returns

&entry.spec_key(),

Specification for OccupiedEntry::key

Source §

impl VstdSpecsForRustStdLib

Source

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

returns

&entry.spec_key(),

Specification for VacantEntry::key

Source §

impl VstdSpecsForRustStdLib

Source

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

ensures

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

Specification for DefaultHasher::new

Source

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

ensures

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

Specification for DefaultHasher::write

Source

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

ensures

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

Specification for DefaultHasher::finish

Source

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

ensures

obeys_key_model::<Key>() && builds_valid_hashers::<S>()
    ==> {
        &&& IteratorSpec::remaining(&iter).len() == m@.dom().len()
        &&& forall |i: int| {
            0 <= i < IteratorSpec::remaining(&iter).len()
                ==> m@.contains_key(*IteratorSpec::remaining(&iter)[i].0)
                    && m@[*IteratorSpec::remaining(&iter)[i].0]
                        == *IteratorSpec::remaining(&iter)[i].1
        }
        &&& forall |k: Key| (
            #[trigger] m@.contains_key(k)
                ==> IteratorSpec::remaining(&iter).contains((&k, &m@[k]))
        )
        &&& IteratorSpec::remaining(&iter).unref().to_set() == m@.kv_pairs()
        &&& iter.remaining().no_duplicates()
        &&& into_iter(iter) == IteratorSpec::remaining(&iter).unref()
        &&& IteratorSpec::decrease(&iter) is Some

    },

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

Source

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

ensures

len == spec_hash_map_len(m),

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

Source

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

ensures

res == m@.is_empty(),

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

Source

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

ensures

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

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

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

Source

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

ensures

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

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

Source

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

ensures

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

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

Source

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

ensures

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

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

Source

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

ensures

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

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

Source

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

ensures

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

    },

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

Source

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

ensures

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

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

Source

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

ensures

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

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

Source

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

ensures

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

    },

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

Source

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

ensures

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

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

Source

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

ensures

obeys_key_model::<Key>() && builds_valid_hashers::<S>()
    ==> {
        &&& IteratorSpec::remaining(&keys).unref().to_set() == m@.dom()
        &&& IteratorSpec::remaining(&keys).no_duplicates()
        &&& IteratorSpec::remaining(&keys).len() == m@.dom().len()
        &&& into_iter_keys(keys) == IteratorSpec::remaining(&keys).unref()
        &&& IteratorSpec::decrease(&keys) is Some

    },

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

Source

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

ensures

obeys_key_model::<Key>() && builds_valid_hashers::<S>()
    ==> {
        &&& IteratorSpec::remaining(&values).unref().to_set() == m@.values()
        &&& IteratorSpec::remaining(&values).len() == m@.dom().len()
        &&& into_iter_values(values) == IteratorSpec::remaining(&values).unref()
        &&& IteratorSpec::decrease(&values) is Some

    },

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

Source

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

ensures

len == spec_hash_set_len(m),

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

Source

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

ensures

res == m@.is_empty(),

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

Source

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

ensures

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

Specification for HashSet::<Key>::new

Source

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

ensures

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

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

Source

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

ensures

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

Specification for HashSet::<Key>::with_capacity

Source

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

ensures

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

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

Source

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

ensures

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

    },

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

Source

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

ensures

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

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

Source

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

ensures

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

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

Source

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

ensures

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

    },

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

Source

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

ensures

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

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

Source

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

ensures

obeys_key_model::<Key>() && builds_valid_hashers::<S>()
    ==> {
        &&& IteratorSpec::remaining(&hash_keys).unref().to_set() == m@
        &&& IteratorSpec::remaining(&hash_keys).no_duplicates()
        &&& IteratorSpec::remaining(&hash_keys).len() == m@.len()
        &&& into_iter_hash_keys(hash_keys) == IteratorSpec::remaining(&hash_keys).unref()
        &&& IteratorSpec::decrease(&hash_keys) is Some

    },

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

Source

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

ensures

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

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

Source

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

returns

&entry.spec_key(),

Specification for Entry::key

Source

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

ensures

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

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

Specification for Entry::or_insert

Source

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

ensures

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

occ_entry.value() == value,

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

Specification for Entry::insert_entry

Source

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

ensures

entry.final_value() == None,

returns

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

Specification for OccupiedEntry::remove_entry

Source

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

ensures

*value == entry.value(),

Specification for OccupiedEntry::get

Source

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

ensures

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

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

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

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

Specification for OccupiedEntry::get_mut

Source

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

ensures

*value == entry.value(),

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

Specification for OccupiedEntry::into_mut

Source

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

ensures

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

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

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

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

Specification for OccupiedEntry::insert

Source

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

ensures

value == entry.value(),

entry.final_value() == None,

Specification for OccupiedEntry::remove

Source

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

ensures

key == entry.key(),

entry.final_value() == None,

Specification for VacantEntry::into_key

Source

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

ensures

*value_ref == value,

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

Specification for VacantEntry::insert

Source

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

ensures

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

occ_entry.value() == value,

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

Specification for VacantEntry::insert_entry

Source §

impl VstdSpecsForRustStdLib

Source

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

ensures

res == x,

Source

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

ensures

res == x,

Source

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

ensures

res == x,

Source

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

ensures

res == x,

Source

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

ensures

res == x,

Source

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

ensures

res == x,

Source

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

ensures

res == x,

Source

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

ensures

res == x,

Source

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

ensures

res == x,

Source

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

ensures

res == x,

Source

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

ensures

res == x,

Source

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

ensures

res == x,

Source

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

ensures

b == is_some(option),

Specification for Option::<T>::is_some

Source

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

ensures

b == is_none(option),

Specification for Option::<T>::is_none

Source

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

ensures

a is Some <==> option is Some,

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

Specification for Option::<T>::as_ref

Source

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

requires

option is Some,

ensures

t == spec_unwrap(option),

Specification for Option::<T>::unwrap

Source

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

ensures

t == spec_unwrap_or(option, default),

Specification for Option::<T>::unwrap_or

Source

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

requires

option is Some,

ensures

t == spec_expect(option, msg),

Specification for Option::<T>::expect

Source

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

ensures

t == *old(option),

*final(option) is None,

Specification for Option::<T>::take

Source

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

requires

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

ensures

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

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

Specification for Option::<T>::map

Source

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

ensures

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

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

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

Source

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

requires

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

ensures

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

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

Specification for Option::<T>::and_then

Source

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

requires

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

ensures

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

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

    },

Specification for Option::<T>::ok_or_else

Source

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

ensures

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

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

Specification for Option::<T>::unwrap_or_default

Source

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

requires

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

ensures

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

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

Specification for Option::<T>::unwrap_or_else

Source

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

ensures

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

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

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

Source

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

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

Source

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

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

Source

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

ensures

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

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

Source

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

ensures

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

Specification for RangeInclusive::<Idx>::contains

Source

pub unsafe exec fn _verus_external_fn_specification_1091_RangeInclusive_3258583260__32_Idx_3262325858__32_is__empty<Idx>( r: &RangeInclusive<Idx>, ) -> res : bool
where Idx: PartialOrd<Idx>,

ensures

<Idx as PartialOrdSpec<Idx>>::obeys_partial_cmp_spec()
    ==> res == spec_range_inclusive_is_empty(r),

Specification for RangeInclusive::<Idx>::is_empty

Source

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

ensures

ret@
    == (RangeInclusiveView {
        start,
        end,
        exhausted: false,
    }),

Specification for RangeInclusive::<Idx>::new

Source

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

ensures

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

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

Source

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

ensures

result == Bound::Included(&range.start),

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

Source

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

ensures

result == Bound::Excluded(&range.end),

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

Source

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

ensures

result == Bound::Unbounded,

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

Source

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

ensures

result == Bound::Unbounded,

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

Source

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

ensures

result == Bound::Included(&range.start),

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

Source

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

ensures

result == Bound::Unbounded,

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

Source

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

ensures

result == Bound::Unbounded,

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

Source

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

ensures

result == Bound::Excluded(&range.end),

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

Source

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

ensures

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

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

Source

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

ensures

result == spec_range_inclusive_end_bound(range),

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

Source

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

ensures

result == Bound::Unbounded,

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

Source

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

ensures

result == Bound::Included(&range.end),

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

Source

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

ensures

result == bound_as_ref(&range.0),

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

Source

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

ensures

result == bound_as_ref(&range.1),

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

Source §

impl VstdSpecsForRustStdLib

Source

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

ensures

b == is_ok(r),

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

Source

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

ensures

b == is_err(r),

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

Source

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

ensures

r is Ok <==> result is Ok,

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

r is Err <==> result is Err,

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

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

Source

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

requires

result is Ok,

ensures

t == result->Ok_0,

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

Source

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

requires

result is Err,

ensures

e == result->Err_0,

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

Source

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

requires

result is Ok,

ensures

t == result->Ok_0,

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

Source

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

requires

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

ensures

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

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

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

Source

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

requires

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

ensures

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

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

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

Source

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

ensures

opt == ok(result),

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

Source

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

ensures

opt == err(result),

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

ensures

*output == old(slice)@[i as int],

final(slice)@ == old(slice)@.update(i as int, *final(output)),

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

Source

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

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

Source

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

ensures

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

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

Source

pub unsafe exec fn _verus_external_fn_specification_11246032_Range_326032_usize_326232_as_32_SliceIndex_326032__91_T_933262326232585832_get__mut<T>( i: Range<usize>, slice: &mut [T], ) -> Option<&mut [T]>

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

Source

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

ensures

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

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

final(slice)@
    == old(slice)@.subrange(0, i.start as int) + final(r)@
        + old(slice)@.subrange(i.end as int, old(slice)@.len() as int),

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

Source

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

Specification for <RangeTo<usize> as SliceIndex<[T]>>::get

Source

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

ensures

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

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

Source

pub unsafe exec fn _verus_external_fn_specification_11286032_RangeTo_326032_usize_326232_as_32_SliceIndex_326032__91_T_933262326232585832_get__mut<T>( i: RangeTo<usize>, slice: &mut [T], ) -> Option<&mut [T]>

Specification for <RangeTo<usize> as SliceIndex<[T]>>::get_mut

Source

pub unsafe exec fn _verus_external_fn_specification_11296032_RangeTo_326032_usize_326232_as_32_SliceIndex_326032__91_T_933262326232585832_index__mut<T>( i: RangeTo<usize>, slice: &mut [T], ) -> r : &mut [T]

ensures

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

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

final(slice)@ == final(r)@ + old(slice)@.subrange(i.end as int, old(slice)@.len() as int),

Specification for <RangeTo<usize> as SliceIndex<[T]>>::index_mut

Source

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

Specification for <RangeFrom<usize> as SliceIndex<[T]>>::get

Source

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

ensures

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

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

Source

pub unsafe exec fn _verus_external_fn_specification_11326032_RangeFrom_326032_usize_326232_as_32_SliceIndex_326032__91_T_933262326232585832_get__mut<T>( i: RangeFrom<usize>, slice: &mut [T], ) -> Option<&mut [T]>

Specification for <RangeFrom<usize> as SliceIndex<[T]>>::get_mut

Source

pub unsafe exec fn _verus_external_fn_specification_11336032_RangeFrom_326032_usize_326232_as_32_SliceIndex_326032__91_T_933262326232585832_index__mut<T>( i: RangeFrom<usize>, slice: &mut [T], ) -> r : &mut [T]

ensures

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

final(r)@ == final(slice)@.subrange(i.start as int, old(slice)@.len() as int),

final(slice)@ == old(slice)@.subrange(0, i.start as int) + final(r)@,

Specification for <RangeFrom<usize> as SliceIndex<[T]>>::index_mut

Source

pub unsafe exec fn _verus_external_fn_specification_11346032__91_T_93326232585832_starts__with<T: PartialEq>( slice: &[T], needle: &[T], ) -> result : bool

ensures

needle@.len() > slice@.len() ==> !result,

<T as super::cmp::PartialEqSpec<T>>::obeys_eq_spec()
    ==> (result == spec_slice_starts_with(slice, needle)),

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

Source

pub unsafe exec fn _verus_external_fn_specification_11356032__91_T_93326232585832_ends__with<T: PartialEq>( slice: &[T], needle: &[T], ) -> result : bool

ensures

needle@.len() > slice@.len() ==> !result,

<T as super::cmp::PartialEqSpec<T>>::obeys_eq_spec()
    ==> (result == spec_slice_ends_with(slice, needle)),

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

Source

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

Specification for <RangeToInclusive<usize> as SliceIndex<[T]>>::get

Source

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

ensures

r@ == slice@.subrange(0, i.end as int + 1),

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

Source

pub unsafe exec fn _verus_external_fn_specification_11386032_RangeToInclusive_326032_usize_326232_as_32_SliceIndex_326032__91_T_933262326232585832_get__mut<T>( i: RangeToInclusive<usize>, slice: &mut [T], ) -> Option<&mut [T]>

Specification for <RangeToInclusive<usize> as SliceIndex<[T]>>::get_mut

Source

pub unsafe exec fn _verus_external_fn_specification_11396032_RangeToInclusive_326032_usize_326232_as_32_SliceIndex_326032__91_T_933262326232585832_index__mut<T>( i: RangeToInclusive<usize>, slice: &mut [T], ) -> r : &mut [T]

ensures

r@ == old(slice)@.subrange(0, i.end as int + 1),

final(r)@ == final(slice)@.subrange(0, i.end as int + 1),

final(slice)@
    == final(r)@ + old(slice)@.subrange(i.end as int + 1, old(slice)@.len() as int),

Specification for <RangeToInclusive<usize> as SliceIndex<[T]>>::index_mut

Source

pub unsafe exec fn _verus_external_fn_specification_11406032_RangeFull_32_as_32_SliceIndex_326032__91_T_933262326232585832_get<T>( i: RangeFull, slice: &[T], ) -> Option<&[T]>

Specification for <RangeFull as SliceIndex<[T]>>::get

Source

pub unsafe exec fn _verus_external_fn_specification_11416032_RangeFull_32_as_32_SliceIndex_326032__91_T_933262326232585832_index<T>( i: RangeFull, slice: &[T], ) -> r : &[T]

ensures

r@ == slice@,

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

Source

pub unsafe exec fn _verus_external_fn_specification_11426032_RangeFull_32_as_32_SliceIndex_326032__91_T_933262326232585832_get__mut<T>( i: RangeFull, slice: &mut [T], ) -> Option<&mut [T]>

Specification for <RangeFull as SliceIndex<[T]>>::get_mut

Source

pub unsafe exec fn _verus_external_fn_specification_11436032_RangeFull_32_as_32_SliceIndex_326032__91_T_933262326232585832_index__mut<T>( i: RangeFull, slice: &mut [T], ) -> r : &mut [T]

ensures

r@ == old(slice)@,

final(slice)@ == final(r)@,

Specification for <RangeFull as SliceIndex<[T]>>::index_mut

Source

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

Specification for <RangeInclusive<usize> as SliceIndex<[T]>>::get

Source

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

ensures

r@ == slice@.subrange(slice_range_start(&i), slice_range_end(&i, slice@.len() as nat)),

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

Source

pub unsafe exec fn _verus_external_fn_specification_11466032_RangeInclusive_326032_usize_326232_as_32_SliceIndex_326032__91_T_933262326232585832_get__mut<T>( i: RangeInclusive<usize>, slice: &mut [T], ) -> Option<&mut [T]>

Specification for <RangeInclusive<usize> as SliceIndex<[T]>>::get_mut

Source

pub unsafe exec fn _verus_external_fn_specification_11476032_RangeInclusive_326032_usize_326232_as_32_SliceIndex_326032__91_T_933262326232585832_index__mut<T>( i: RangeInclusive<usize>, slice: &mut [T], ) -> r : &mut [T]

ensures

r@
    == old(slice)@
        .subrange(slice_range_start(&i), slice_range_end(&i, old(slice)@.len() as nat)),

final(r)@
    == final(slice)@
        .subrange(slice_range_start(&i), slice_range_end(&i, old(slice)@.len() as nat)),

final(slice)@
    == old(slice)@.subrange(0, slice_range_start(&i)) + final(r)@
        + old(slice)@
            .subrange(
                slice_range_end(&i, old(slice)@.len() as nat),
                old(slice)@.len() as int,
            ),

Specification for <RangeInclusive<usize> as SliceIndex<[T]>>::index_mut

Source

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

ensures

call_ensures(<I as SliceIndex<[T]>>::get, (i, slice), b),

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

Source

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

ensures

call_ensures(<I as SliceIndex<[T]>>::get_mut, (i, slice), b),

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

Source

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

ensures

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

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

Source

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

ensures

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

Specification for <[T] as IndexMut>::index_mut

Source

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

ensures

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

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

Source

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

ensures

exists |slice: &mut [T]| {
    &&& #[trigger] slice@ == old(array)@
    &&& final(slice)@ == final(array)@
    &&& call_ensures(<[T]>::index_mut, (slice, index), output)

},

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

Source

pub unsafe exec fn _verus_external_fn_specification_1154_core_325858__32_hint_325858__32_unreachable__unchecked() -> !

requires

false,

Specification for core::hint::unreachable_unchecked

Source

pub unsafe exec fn _verus_external_fn_specification_11556032__91_T_93__32_as_32_PartialEq_326032__91_U_933262326232585832_eq<T: PartialEq, U>( left: &[T], right: &[U], ) -> bool

Specification for <[T] as PartialEq<[U]>>::eq

Source

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

ensures

IteratorSpec::remaining(&iter) == s@.as_ref(),

into_iter_elts(iter) == IteratorSpec::remaining(&iter).unref(),

IteratorSpec::decrease(&iter) is Some,

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

Source

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

ensures

IteratorSpec::remaining(&iter) == s@.as_ref(),

into_iter_elts(iter) == IteratorSpec::remaining(&iter).unref(),

IteratorSpec::decrease(&iter) is Some,

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

Source

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

ensures

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

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

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

Source

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

ensures

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

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

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

Source

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

requires

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

ensures

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

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

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

Source

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

ensures

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

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

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

Source

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

requires

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

ensures

final(dst)@ == src@,

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

Source

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

requires

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

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

ensures

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

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

Source §

impl VstdSpecsForRustStdLib

Source

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

ensures

len == spec_vec_len(vec),

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

Source

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

ensures

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

Specification for Vec::<T>::new

Source

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

ensures

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

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

Source

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

ensures

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

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

Source

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

ensures

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

Specification for Vec::<T>::with_capacity

Source

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

ensures

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

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

Source

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

ensures

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

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

Source

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

ensures

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

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

Source

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

ensures

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

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

Source

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

ensures

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

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

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

Source

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

ensures

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

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

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

Source

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

ensures

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

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

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

Source

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

ensures

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

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

Source

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

requires

i < old(vec).len(),

ensures

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

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

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

Source

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

requires

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

ensures

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

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

Source

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

ensures

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

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

Source

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

requires

i < old(vec).len(),

ensures

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

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

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

Source

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

ensures

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

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

Source

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

ensures

slice@ == vec@,

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

Source

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

ensures

slice@ == vec@,

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

Source

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

ensures

slice@ == old(vec)@,

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

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

Source

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

requires

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

ensures

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

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

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

Source

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

ensures

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

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

vec_clone_trigger(*vec, res),

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

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

Source

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

ensures

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

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

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

Source

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

ensures

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

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

    },

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

Source

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

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

Source

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

ensures

v.len() == n,

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

Specification for [alloc::vec::from_elem]

Source

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

ensures

IteratorSpec::remaining(&iter) == vec@,

into_iter_elts(iter) == IteratorSpec::remaining(&iter),

IteratorSpec::decrease(&iter) is Some,

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

Source

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

ensures

IteratorSpec::remaining(&iter) == vec@.as_ref(),

super::slice::into_iter_elts(iter) == IteratorSpec::remaining(&iter).unref(),

IteratorSpec::decrease(&iter) is Some,

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

Source §

impl VstdSpecsForRustStdLib

Source

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

ensures

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

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

Source

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

ensures

*output == old(v).spec_index(i as int),

final(v)@ == old(v)@.update(i as int, *final(output)),

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

Source

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

ensures

len == spec_vec_dequeue_len(v),

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

Source

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

ensures

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

Specification for VecDeque::<T>::new

Source

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

ensures

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

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

Source

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

ensures

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

Specification for VecDeque::<T>::with_capacity

Source

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

ensures

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

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

Source

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

ensures

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

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

Source

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

ensures

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

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

Source

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

ensures

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

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

    ),
},

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

Source

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

ensures

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

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

    ),
},

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

Source

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

ensures

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

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

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

Source

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

requires

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

ensures

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

Specification for VecDeque::<T, A>::insert

Source

pub unsafe exec fn _verus_external_fn_specification_1210_VecDeque_3258583260__32_T_44__32_A_3262325858__32_remove<T, A: Allocator>( v: &mut VecDeque<T, A>, i: usize, ) -> element : Option<T>

ensures

match element {
    Some(x) => (
        &&& i < old(v)@.len()
        &&& x == old(v)@[i as int]
        &&& final(v)@ == old(v)@.remove(i as int)

    ),
    None => (
        &&& old(v)@.len() <= i
        &&& final(v)@ == old(v)@

    ),
},

Specification for VecDeque::<T, A>::remove

Source

pub unsafe exec fn _verus_external_fn_specification_1211_VecDeque_3258583260__32_T_44__32_A_3262325858__32_clear<T, A: Allocator>( v: &mut VecDeque<T, A>, )

ensures

final(v).view() == Seq::<T>::empty(),

Specification for VecDeque::<T, A>::clear

Source

pub unsafe exec fn _verus_external_fn_specification_1212_VecDeque_3258583260__32_T_44__32_A_3262325858__32_split__off<T, A: Allocator + Clone>( v: &mut VecDeque<T, A>, at: usize, ) -> return_value : VecDeque<T, A>

requires

at <= old(v)@.len(),

ensures

final(v)@ == old(v)@.subrange(0, at as int),

return_value@ == old(v)@.subrange(at as int, old(v)@.len() as int),

Specification for VecDeque::<T, A>::split_off

Source

pub unsafe exec fn _verus_external_fn_specification_12136032_VecDeque_326032_T_44__32_A_326232_as_32_Clone_3262325858__32_clone<T: Clone, A: Allocator + Clone>( v: &VecDeque<T, A>, ) -> res : VecDeque<T, A>

ensures

res.len() == v.len(),

forall |i| 0 <= i < v.len() ==> cloned::<T>(v[i], res[i]),

vec_dequeue_clone_trigger(*v, res),

v@ =~= res@ ==> v@ == res@,

Specification for <VecDeque<T, A> as Clone>::clone

Source

pub unsafe exec fn _verus_external_fn_specification_1214_VecDeque_3258583260__32_T_44__32_A_3262325858__32_truncate<T, A: Allocator>( v: &mut VecDeque<T, A>, len: usize, )

ensures

len <= old(v).len() ==> final(v)@ == old(v)@.subrange(0, len as int),

len > old(v).len() ==> final(v)@ == old(v)@,

Specification for VecDeque::<T, A>::truncate

Source

pub unsafe exec fn _verus_external_fn_specification_1215_VecDeque_3258583260__32_T_44__32_A_3262325858__32_resize<T: Clone, A: Allocator>( v: &mut VecDeque<T, A>, len: usize, value: T, )

ensures

len <= old(v).len() ==> final(v)@ == old(v)@.subrange(0, len as int),

len > old(v).len()
    ==> {
        &&& final(v)@.len() == len
        &&& final(v)@.subrange(0, old(v).len() as int) == old(v)@
        &&& forall |i| old(v).len() <= i < len ==> cloned::<T>(value, final(v)@[i])

    },

Specification for VecDeque::<T, A>::resize

Source

pub unsafe exec fn _verus_external_fn_specification_1216_VecDeque_3258583260__32_T_44__32_A_3262325858__32_iter<'a, T, A: Allocator>( v: &'a VecDeque<T, A>, ) -> iter : Iter<'a, T>

ensures

IteratorSpec::remaining(&iter) == v@.as_ref(),

into_iter_elts(iter) == IteratorSpec::remaining(&iter),

IteratorSpec::decrease(&iter) is Some,

Specification for VecDeque::<T, A>::iter

Source §

impl VstdSpecsForRustStdLib

Source

pub unsafe exec fn _verus_external_fn_specification_12176032__91_T_93326232585832_into__vec<T, A: Allocator>( b: Box<[T], A>, ) -> v : Vec<T, A>

ensures

v@ == b@,

Specification for [<[T]>::into_vec]

Source

pub unsafe exec fn _verus_external_fn_specification_1218_Box_3258583260__32_T_3262325858__32_new<T>( t: T, ) -> v : Box<T>

ensures

*v == t,

Specification for Box::<T>::new

Source

pub unsafe exec fn _verus_external_fn_specification_12196032_Box_326032_T_443262__32_as_32_core_325858__32_default_325858__32_Default_3262325858__32_default<T: Default>() -> res : Box<T>

ensures

T::default.ensures((), *res),

Specification for <Box<T> as core::default::Default>::default

Source

pub unsafe exec fn _verus_external_fn_specification_1220_Rc_3258583260__32_T_3262325858__32_new<T>( t: T, ) -> v : Rc<T>

ensures

*v == t,

Specification for Rc::<T>::new

Source

pub unsafe exec fn _verus_external_fn_specification_12216032_Rc_326032_T_443262__32_as_32_core_325858__32_default_325858__32_Default_3262325858__32_default<T: Default>() -> res : Rc<T>

ensures

T::default.ensures((), *res),

Specification for <Rc<T> as core::default::Default>::default

Source

pub unsafe exec fn _verus_external_fn_specification_1222_Arc_3258583260__32_T_3262325858__32_new<T>( t: T, ) -> v : Arc<T>

ensures

*v == t,

Specification for Arc::<T>::new

Source

pub unsafe exec fn _verus_external_fn_specification_12236032_Arc_326032_T_443262__32_as_32_core_325858__32_default_325858__32_Default_3262325858__32_default<T: Default>() -> res : Arc<T>

ensures

T::default.ensures((), *res),

Specification for <Arc<T> as core::default::Default>::default

Source

pub unsafe exec fn _verus_external_fn_specification_12246032_Box_326032_T_44__32_A_326232_as_32_Clone_3262325858__32_clone<T: Clone, A: Allocator + Clone>( b: &Box<T, A>, ) -> res : Box<T, A>

ensures

cloned::<T>(**b, *res),

Specification for <Box<T, A> as Clone>::clone

Source

pub unsafe exec fn _verus_external_fn_specification_1225_Rc_3258583260__32_T_44__32_A_3262325858__32_try__unwrap<T, A: Allocator>( v: Rc<T, A>, ) -> result : Result<T, Rc<T, A>>

ensures

match result {
    Ok(t) => t == *v,
    Err(e) => e == v,
},

Specification for Rc::<T, A>::try_unwrap

Source

pub unsafe exec fn _verus_external_fn_specification_1226_Rc_3258583260__32_T_44__32_A_3262325858__32_into__inner<T, A: Allocator>( v: Rc<T, A>, ) -> result : Option<T>

ensures

result matches Some(t) ==> t == *v,

Source §

open spec fn obeys_into_spec() -> bool

{ <U as FromSpec<Self>>::obeys_from_spec() }

Source §

open spec fn into_spec(self) -> U

{ U::from_spec(self) }

fn try_from(value: U) -> Result<T, <T as TryFrom>::Error>

Performs the conversion.

fn try_into(self) -> Result<U, >::Error>

Performs the conversion.

Source §

impl<T, VERUS_SPEC__A> TryIntoSpec<T> for VERUS_SPEC__A
where VERUS_SPEC__A: TryInto<T>,

Source §

exec fn obeys_try_into_spec() -> bool

Source §

exec fn try_into_spec(self) -> Result<T, <VERUS_SPEC__A as TryInto<T>>::Error>

Source §

impl<T, U> TryIntoSpecImpl for T
where U: TryFrom<T>,

Source §

open spec fn obeys_try_into_spec() -> bool

{ <U as TryFromSpec<Self>>::obeys_try_from_spec() }

Source §

open spec fn try_into_spec(self) -> Result<U, >::Error>

{ <U as TryFromSpec<Self>>::try_from_spec(self) }

VstdSpecsForRustStdLib

Struct VstdSpecsForRustStdLib Copy item path

Implementations§

impl VstdSpecsForRustStdLib

pub unsafe exec fn _verus_external_fn_specification_0__60__32__38__32__39_a_32__91_T_59__32_N_93__32_as_32_core_32__58__58__32_iter_32__58__58__32_IntoIterator_32__62__32__58__58__32_into__iter<'a, T, const N: usize>( s: &'a [T; N], ) -> iter : Iter<'a, T>

pub unsafe exec fn _verus_external_fn_specification_1__60__32__91_T_59__32_N_93__32__62__32__58__58__32_as__slice<T, const N: usize>( ar: &[T; N], ) -> out : &[T]

impl VstdSpecsForRustStdLib

pub unsafe exec fn _verus_external_fn_specification_2__60__32_f32_32_as_32_Clone_32__62__32__58__58__32_clone( f: &f32, ) -> res : f32

pub unsafe exec fn _verus_external_fn_specification_3__60__32_f64_32_as_32_Clone_32__62__32__58__58__32_clone( f: &f64, ) -> res : f64

impl VstdSpecsForRustStdLib

pub unsafe exec fn _verus_external_fn_specification_4_core_32__58__58__32_mem_32__58__58__32_size__of_32__58__58__32__60__32_V_32__62_<V>() -> u : usize

pub unsafe exec fn _verus_external_fn_specification_5_core_32__58__58__32_mem_32__58__58__32_align__of_32__58__58__32__60__32_V_32__62_<V>() -> u : usize

pub unsafe exec fn _verus_external_fn_specification_6_core_32__58__58__32_mem_32__58__58__32_size__of__val_32__58__58__32__60__32_V_32__62_<V: ?Sized>( val: &V, ) -> u : usize

pub unsafe exec fn _verus_external_fn_specification_7_core_32__58__58__32_mem_32__58__58__32_align__of__val_32__58__58__32__60__32_V_32__62_<V: ?Sized>( val: &V, ) -> u : usize

impl VstdSpecsForRustStdLib

pub unsafe exec fn _verus_external_fn_specification_1229__60__32__42__32_mut_32_T_32__62__32__58__58__32_addr<T: PointeeSized>( p: *mut T, ) -> addr : usize

pub unsafe exec fn _verus_external_fn_specification_1230__60__32__42__32_mut_32_T_32__62__32__58__58__32_with__addr<T: PointeeSized>( p: *mut T, addr: usize, ) -> q : *mut T

impl VstdSpecsForRustStdLib

pub unsafe exec fn _verus_external_fn_specification_1227__60__32__42__32_const_32_T_32__62__32__58__58__32_addr<T: PointeeSized>( p: *const T, ) -> addr : usize

pub unsafe exec fn _verus_external_fn_specification_1228__60__32__42__32_const_32_T_32__62__32__58__58__32_with__addr<T: PointeeSized>( p: *const T, addr: usize, ) -> q : *const T

impl VstdSpecsForRustStdLib

pub unsafe exec fn _verus_external_fn_specification_8__60__32__42__32_mut_32_T_32_as_32_PartialEq_32__60__32__42__32_mut_32_T_32__62__32__62__32__58__58__32_eq<T: PointeeSized>( x: &*mut T, y: &*mut T, ) -> res : bool

pub unsafe exec fn _verus_external_fn_specification_9__60__32__42__32_const_32_T_32_as_32_PartialEq_32__60__32__42__32_const_32_T_32__62__32__62__32__58__58__32_eq<T: PointeeSized>( x: &*const T, y: &*const T, ) -> res : bool

pub unsafe exec fn _verus_external_fn_specification_10_core_32__58__58__32_ptr_32__58__58__32_null<T: PointeeSized + Pointee<Metadata = ()>>() -> res : *const T

pub unsafe exec fn _verus_external_fn_specification_11_core_32__58__58__32_ptr_32__58__58__32_null__mut<T: PointeeSized + Pointee<Metadata = ()>>() -> res : *mut T

impl VstdSpecsForRustStdLib

pub unsafe exec fn _verus_external_fn_specification_12__60__32__91_T_93__32__62__32__58__58__32_len<T>( slice: &[T], ) -> len : usize

pub unsafe exec fn _verus_external_fn_specification_13__60__32__91_T_93__32__62__32__58__58__32_is__empty<T>( slice: &[T], ) -> b : bool

impl VstdSpecsForRustStdLib

pub unsafe exec fn _verus_external_fn_specification_14_str_32__58__58__32_is__ascii( s: &str, ) -> b : bool

pub unsafe exec fn _verus_external_fn_specification_15_str_32__58__58__32_to__owned( s: &str, ) -> res : String

pub unsafe exec fn _verus_external_fn_specification_16_str_32__58__58__32_as__bytes( s: &str, ) -> b : &[u8] ⓘ

pub unsafe exec fn _verus_external_fn_specification_17_str_32__58__58__32_len( s: &str, ) -> usize

pub unsafe exec fn _verus_external_fn_specification_18_str_32__58__58__32_is__empty( s: &str, ) -> bool

pub unsafe exec fn _verus_external_fn_specification_19_str_32__58__58__32_is__char__boundary( s: &str, index: usize, ) -> bool

pub unsafe exec fn _verus_external_fn_specification_20_str_32__58__58__32_split__at( s: &str, mid: usize, ) -> res : (&str, &str)

pub unsafe exec fn _verus_external_fn_specification_21_str_32__58__58__32_from__utf8__unchecked( v: &[u8], ) -> res : &str

pub unsafe exec fn _verus_external_fn_specification_22__60__32_T_32_as_32_ToString_32__62__32__58__58__32_to__string<T: Display + ?Sized>( t: &T, ) -> res : String

pub unsafe exec fn _verus_external_fn_specification_23_String_32__58__58__32_as__str<'a>( s: &'a String, ) -> res : &'a str

pub unsafe exec fn _verus_external_fn_specification_24__60__32_String_32_as_32_core_32__58__58__32_ops_32__58__58__32_Deref_32__62__32__58__58__32_deref<'a>( s: &'a String, ) -> res : &'a str

pub unsafe exec fn _verus_external_fn_specification_25__60__32_String_32_as_32_Clone_32__62__32__58__58__32_clone( s: &String, ) -> res : String

pub unsafe exec fn _verus_external_fn_specification_26__60__32_String_32_as_32_PartialEq_32__62__32__58__58__32_eq( s: &String, other: &String, ) -> res : bool

pub unsafe exec fn _verus_external_fn_specification_27_String_32__58__58__32_new() -> res : String

pub unsafe exec fn _verus_external_fn_specification_28_String_32__58__58__32_push( s: &mut String, c: char, )

pub unsafe exec fn _verus_external_fn_specification_29_String_32__58__58__32_pop( s: &mut String, ) -> res : Option<char>

pub unsafe exec fn _verus_external_fn_specification_30_String_32__58__58__32_push__str( s: &mut String, other: &str, )

pub unsafe exec fn _verus_external_fn_specification_31_String_32__58__58__32_is__empty( s: &String, ) -> res : bool

pub unsafe exec fn _verus_external_fn_specification_32_String_32__58__58__32_clear( s: &mut String, )

pub unsafe exec fn _verus_external_fn_specification_33__60__32_String_32_as_32_core_32__58__58__32_default_32__58__58__32_Default_32__62__32__58__58__32_default() -> r : String

pub unsafe exec fn _verus_external_fn_specification_34_str_32__58__58__32_chars( s: &str, ) -> iter : Chars<'_>

impl VstdSpecsForRustStdLib

pub unsafe exec fn _verus_external_fn_specification_35_alloc_32__58__58__32_boxed_32__58__58__32_box__assume__init__into__vec__unsafe<T, const N: usize>( vals: Box<MaybeUninit<[T; N]>>, ) -> result : Vec<T>

pub unsafe exec fn _verus_external_fn_specification_36_alloc_32__58__58__32_intrinsics_32__58__58__32_write__box__via__move<T>( _0: Box<MaybeUninit<T>>, v: T, ) -> result : Box<MaybeUninit<T>>

pub unsafe exec fn _verus_external_fn_specification_37_alloc_32__58__58__32_boxed_32__58__58__32_Box_32__58__58__32__60__32_T_32__62__32__58__58__32_new__uninit<T>() -> Box<MaybeUninit<T>>

impl VstdSpecsForRustStdLib

pub unsafe exec fn _verus_external_fn_specification_38__60__32__91_T_59__32_N_93__32_as_32_PartialEq_32__60__32__91_U_59__32_N_93__32__62__32__62__32__58__58__32_eq<T: PartialEq<U>, U, const N: usize>( left: &[T; N], right: &[U; N], ) -> bool

pub unsafe exec fn _verus_external_fn_specification_39__60__32__38__32__39_a_32__91_T_93__32_as_32_PartialEq_32__60__32__91_U_59__32_N_93__44__32__62__32__62__32__58__58__32_eq<'a, T: PartialEq<U>, U, const N: usize>( left: &&'a [T], right: &[U; N], ) -> bool

pub unsafe exec fn _verus_external_fn_specification_40__60__32__91_T_59__32_N_93__32_as_32_PartialEq_32__60__32__38__32__91_U_93__32__62__32__62__32__58__58__32_eq<'a, T: PartialEq<U>, U, const N: usize>( left: &[T; N], right: &&[U], ) -> bool

pub unsafe exec fn _verus_external_fn_specification_41__60__32__91_T_93__32_as_32_PartialEq_32__60__32__91_U_59__32_N_93__32__62__32__62__32__58__58__32_eq<T: PartialEq<U>, U, const N: usize>( left: &[T], right: &[U; N], ) -> bool

pub unsafe exec fn _verus_external_fn_specification_42__60__32__91_T_59__32_N_93__32_as_32_PartialEq_32__60__32__91_U_93__32__62__32__62__32__58__58__32_eq<T: PartialEq<U>, U, const N: usize>( left: &[T; N], right: &[U], ) -> bool

impl VstdSpecsForRustStdLib

pub unsafe exec fn _verus_external_fn_specification_43__60__32_AtomicU8_32__62__32__58__58__32_new( v: u8, ) -> AtomicU8

pub unsafe exec fn _verus_external_fn_specification_44__60__32_AtomicU8_32__62__32__58__58__32_compare__exchange( atomic: &AtomicU8, current: u8, new: u8, success: Ordering, failure: Ordering, ) -> Result<u8, u8>

pub unsafe exec fn _verus_external_fn_specification_45__60__32_AtomicU8_32__62__32__58__58__32_compare__exchange__weak( atomic: &AtomicU8, current: u8, new: u8, success: Ordering, failure: Ordering, ) -> Result<u8, u8>

pub unsafe exec fn _verus_external_fn_specification_46__60__32_AtomicU8_32__62__32__58__58__32_fetch__and( atomic: &AtomicU8, val: u8, order: Ordering, ) -> u8

pub unsafe exec fn _verus_external_fn_specification_47__60__32_AtomicU8_32__62__32__58__58__32_fetch__nand( atomic: &AtomicU8, val: u8, order: Ordering, ) -> u8

pub unsafe exec fn _verus_external_fn_specification_48__60__32_AtomicU8_32__62__32__58__58__32_fetch__or( atomic: &AtomicU8, val: u8, order: Ordering, ) -> u8

pub unsafe exec fn _verus_external_fn_specification_49__60__32_AtomicU8_32__62__32__58__58__32_fetch__xor( atomic: &AtomicU8, val: u8, order: Ordering, ) -> u8

pub unsafe exec fn _verus_external_fn_specification_50__60__32_AtomicU8_32__62__32__58__58__32_load( atomic: &AtomicU8, order: Ordering, ) -> u8

pub unsafe exec fn _verus_external_fn_specification_51__60__32_AtomicU8_32__62__32__58__58__32_store( atomic: &AtomicU8, val: u8, order: Ordering, )

pub unsafe exec fn _verus_external_fn_specification_52__60__32_AtomicU8_32__62__32__58__58__32_swap( atomic: &AtomicU8, val: u8, order: Ordering, ) -> u8

impl VstdSpecsForRustStdLib

pub unsafe exec fn _verus_external_fn_specification_53__60__32_AtomicU8_32__62__32__58__58__32_fetch__add( atomic: &AtomicU8, val: u8, order: Ordering, ) -> u8

pub unsafe exec fn _verus_external_fn_specification_54__60__32_AtomicU8_32__62__32__58__58__32_fetch__sub( atomic: &AtomicU8, val: u8, order: Ordering, ) -> u8

pub unsafe exec fn _verus_external_fn_specification_55__60__32_AtomicU8_32__62__32__58__58__32_fetch__min( atomic: &AtomicU8, val: u8, order: Ordering, ) -> u8

pub unsafe exec fn _verus_external_fn_specification_56__60__32_AtomicU8_32__62__32__58__58__32_fetch__max( atomic: &AtomicU8, val: u8, order: Ordering, ) -> u8

impl VstdSpecsForRustStdLib

pub unsafe exec fn _verus_external_fn_specification_57__60__32_AtomicU16_32__62__32__58__58__32_new( v: u16, ) -> AtomicU16

pub unsafe exec fn _verus_external_fn_specification_58__60__32_AtomicU16_32__62__32__58__58__32_compare__exchange( atomic: &AtomicU16, current: u16, new: u16, success: Ordering, failure: Ordering, ) -> Result<u16, u16>

pub unsafe exec fn _verus_external_fn_specification_59__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>

Struct VstdSpecsForRustStdLib

pub unsafe exec fn _verus_external_fn_specification_060323832__39_a_32__91_T_59__32_N_93__32_as_32_core_325858__32_iter_325858__32_IntoIterator_3262325858__32_into__iter<'a, T, const N: usize>( s: &'a [T; N], ) -> iter : Iter<'a, T>

pub unsafe exec fn _verus_external_fn_specification_16032__91_T_59__32_N_93326232585832_as__slice<T, const N: usize>( ar: &[T; N], ) -> out : &[T]

pub unsafe exec fn _verus_external_fn_specification_26032_f32_32_as_32_Clone_3262325858__32_clone( f: &f32, ) -> res : f32

pub unsafe exec fn _verus_external_fn_specification_36032_f64_32_as_32_Clone_3262325858__32_clone( f: &f64, ) -> res : f64

pub unsafe exec fn _verus_external_fn_specification_4_core_325858__32_mem_325858__32_size__of_3258583260__32_V_32__62_<V>() -> u : usize

pub unsafe exec fn _verus_external_fn_specification_5_core_325858__32_mem_325858__32_align__of_3258583260__32_V_32__62_<V>() -> u : usize

pub unsafe exec fn _verus_external_fn_specification_6_core_325858__32_mem_325858__32_sizeofval_3258583260__32_V_32__62_<V: ?Sized>( val: &V, ) -> u : usize

pub unsafe exec fn _verus_external_fn_specification_7_core_325858__32_mem_325858__32_alignofval_3258583260__32_V_32__62_<V: ?Sized>( val: &V, ) -> u : usize

pub unsafe exec fn _verus_external_fn_specification_122960324232_mut_32_T_3262325858__32_addr<T: PointeeSized>( p: *mut T, ) -> addr : usize

pub unsafe exec fn _verus_external_fn_specification_123060324232_mut_32_T_3262325858__32_with__addr<T: PointeeSized>( p: mut T, addr: usize, ) -> q : mut T

pub unsafe exec fn _verus_external_fn_specification_122760324232_const_32_T_3262325858__32_addr<T: PointeeSized>( p: *const T, ) -> addr : usize

pub unsafe exec fn _verus_external_fn_specification_122860324232_const_32_T_3262325858__32_with__addr<T: PointeeSized>( p: const T, addr: usize, ) -> q : const T

pub unsafe exec fn _verus_external_fn_specification_860324232_mut_32_T_32_as_32_PartialEq_3260324232_mut_32_T_32623262325858__32_eq<T: PointeeSized>( x: &mut T, y: &mut T, ) -> res : bool

pub unsafe exec fn _verus_external_fn_specification_960324232_const_32_T_32_as_32_PartialEq_3260324232_const_32_T_32623262325858__32_eq<T: PointeeSized>( x: &const T, y: &const T, ) -> res : bool

pub unsafe exec fn _verus_external_fn_specification_10_core_325858__32_ptr_325858__32_null<T: PointeeSized + Pointee<Metadata = ()>>() -> res : *const T

pub unsafe exec fn _verus_external_fn_specification_11_core_325858__32_ptr_325858__32_null__mut<T: PointeeSized + Pointee<Metadata = ()>>() -> res : *mut T

pub unsafe exec fn _verus_external_fn_specification_126032__91_T_93326232585832_len<T>( slice: &[T], ) -> len : usize

pub unsafe exec fn _verus_external_fn_specification_136032__91_T_93326232585832_is__empty<T>( slice: &[T], ) -> b : bool

pub unsafe exec fn _verus_external_fn_specification_14_str_325858__32_is__ascii( s: &str, ) -> b : bool

pub unsafe exec fn _verus_external_fn_specification_15_str_325858__32_to__owned( s: &str, ) -> res : String

pub unsafe exec fn _verus_external_fn_specification_16_str_325858__32_as__bytes( s: &str, ) -> b : &[u8] ⓘ

pub unsafe exec fn _verus_external_fn_specification_17_str_325858__32_len( s: &str, ) -> usize

pub unsafe exec fn _verus_external_fn_specification_18_str_325858__32_is__empty( s: &str, ) -> bool

pub unsafe exec fn _verus_external_fn_specification_19_str_325858__32_ischarboundary( s: &str, index: usize, ) -> bool

pub unsafe exec fn _verus_external_fn_specification_20_str_325858__32_split__at( s: &str, mid: usize, ) -> res : (&str, &str)

pub unsafe exec fn _verus_external_fn_specification_21_str_325858__32_fromutf8unchecked( v: &[u8], ) -> res : &str

pub unsafe exec fn _verus_external_fn_specification_226032_T_32_as_32_ToString_3262325858__32_to__string<T: Display + ?Sized>( t: &T, ) -> res : String

pub unsafe exec fn _verus_external_fn_specification_23_String_325858__32_as__str<'a>( s: &'a String, ) -> res : &'a str

pub unsafe exec fn _verus_external_fn_specification_246032_String_32_as_32_core_325858__32_ops_325858__32_Deref_3262325858__32_deref<'a>( s: &'a String, ) -> res : &'a str

pub unsafe exec fn _verus_external_fn_specification_256032_String_32_as_32_Clone_3262325858__32_clone( s: &String, ) -> res : String

pub unsafe exec fn _verus_external_fn_specification_266032_String_32_as_32_PartialEq_3262325858__32_eq( s: &String, other: &String, ) -> res : bool

pub unsafe exec fn _verus_external_fn_specification_27_String_325858__32_new() -> res : String

pub unsafe exec fn _verus_external_fn_specification_28_String_325858__32_push( s: &mut String, c: char, )

pub unsafe exec fn _verus_external_fn_specification_29_String_325858__32_pop( s: &mut String, ) -> res : Option<char>

pub unsafe exec fn _verus_external_fn_specification_30_String_325858__32_push__str( s: &mut String, other: &str, )

pub unsafe exec fn _verus_external_fn_specification_31_String_325858__32_is__empty( s: &String, ) -> res : bool

pub unsafe exec fn _verus_external_fn_specification_32_String_325858__32_clear( s: &mut String, )

pub unsafe exec fn _verus_external_fn_specification_336032_String_32_as_32_core_325858__32_default_325858__32_Default_3262325858__32_default() -> r : String

pub unsafe exec fn _verus_external_fn_specification_34_str_325858__32_chars( s: &str, ) -> iter : Chars<'_>

pub unsafe exec fn _verus_external_fn_specification_35_alloc_325858__32_boxed_325858__32_boxassumeinitintovec__unsafe<T, const N: usize>( vals: Box<MaybeUninit<[T; N]>>, ) -> result : Vec<T>

pub unsafe exec fn _verus_external_fn_specification_36_alloc_325858__32_intrinsics_325858__32_writeboxvia__move<T>( _0: Box<MaybeUninit<T>>, v: T, ) -> result : Box<MaybeUninit<T>>

pub unsafe exec fn _verus_external_fn_specification_37_alloc_325858__32_boxed_325858__32_Box_3258583260__32_T_3262325858__32_new__uninit<T>() -> Box<MaybeUninit<T>>

pub unsafe exec fn _verus_external_fn_specification_386032__91_T_59__32_N_93__32_as_32_PartialEq_326032__91_U_59__32_N_933262326232585832_eq<T: PartialEq<U>, U, const N: usize>( left: &[T; N], right: &[U; N], ) -> bool

pub unsafe exec fn _verus_external_fn_specification_3960323832__39_a_32__91_T_93__32_as_32_PartialEq_326032__91_U_59__32_N_934432623262325858__32_eq<'a, T: PartialEq<U>, U, const N: usize>( left: &&'a [T], right: &[U; N], ) -> bool

pub unsafe exec fn _verus_external_fn_specification_406032__91_T_59__32_N_93__32_as_32_PartialEq_3260323832__91_U_933262326232585832_eq<'a, T: PartialEq<U>, U, const N: usize>( left: &[T; N], right: &&[U], ) -> bool

pub unsafe exec fn _verus_external_fn_specification_416032__91_T_93__32_as_32_PartialEq_326032__91_U_59__32_N_933262326232585832_eq<T: PartialEq<U>, U, const N: usize>( left: &[T], right: &[U; N], ) -> bool

pub unsafe exec fn _verus_external_fn_specification_426032__91_T_59__32_N_93__32_as_32_PartialEq_326032__91_U_933262326232585832_eq<T: PartialEq<U>, U, const N: usize>( left: &[T; N], right: &[U], ) -> bool

pub unsafe exec fn _verus_external_fn_specification_436032_AtomicU8_3262325858__32_new( v: u8, ) -> AtomicU8

pub unsafe exec fn _verus_external_fn_specification_446032_AtomicU8_3262325858__32_compare__exchange( atomic: &AtomicU8, current: u8, new: u8, success: Ordering, failure: Ordering, ) -> Result<u8, u8>

pub unsafe exec fn _verus_external_fn_specification_456032_AtomicU8_3262325858__32_compareexchangeweak( atomic: &AtomicU8, current: u8, new: u8, success: Ordering, failure: Ordering, ) -> Result<u8, u8>

pub unsafe exec fn _verus_external_fn_specification_466032_AtomicU8_3262325858__32_fetch__and( atomic: &AtomicU8, val: u8, order: Ordering, ) -> u8

pub unsafe exec fn _verus_external_fn_specification_476032_AtomicU8_3262325858__32_fetch__nand( atomic: &AtomicU8, val: u8, order: Ordering, ) -> u8

pub unsafe exec fn _verus_external_fn_specification_486032_AtomicU8_3262325858__32_fetch__or( atomic: &AtomicU8, val: u8, order: Ordering, ) -> u8

pub unsafe exec fn _verus_external_fn_specification_496032_AtomicU8_3262325858__32_fetch__xor( atomic: &AtomicU8, val: u8, order: Ordering, ) -> u8

pub unsafe exec fn _verus_external_fn_specification_506032_AtomicU8_3262325858__32_load( atomic: &AtomicU8, order: Ordering, ) -> u8

pub unsafe exec fn _verus_external_fn_specification_516032_AtomicU8_3262325858__32_store( atomic: &AtomicU8, val: u8, order: Ordering, )

pub unsafe exec fn _verus_external_fn_specification_526032_AtomicU8_3262325858__32_swap( atomic: &AtomicU8, val: u8, order: Ordering, ) -> u8

pub unsafe exec fn _verus_external_fn_specification_536032_AtomicU8_3262325858__32_fetch__add( atomic: &AtomicU8, val: u8, order: Ordering, ) -> u8

pub unsafe exec fn _verus_external_fn_specification_546032_AtomicU8_3262325858__32_fetch__sub( atomic: &AtomicU8, val: u8, order: Ordering, ) -> u8

pub unsafe exec fn _verus_external_fn_specification_556032_AtomicU8_3262325858__32_fetch__min( atomic: &AtomicU8, val: u8, order: Ordering, ) -> u8

pub unsafe exec fn _verus_external_fn_specification_566032_AtomicU8_3262325858__32_fetch__max( atomic: &AtomicU8, val: u8, order: Ordering, ) -> u8

pub unsafe exec fn _verus_external_fn_specification_576032_AtomicU16_3262325858__32_new( v: u16, ) -> AtomicU16

pub unsafe exec fn _verus_external_fn_specification_586032_AtomicU16_3262325858__32_compare__exchange( atomic: &AtomicU16, current: u16, new: u16, success: Ordering, failure: Ordering, ) -> Result<u16, u16>

pub unsafe exec fn _verus_external_fn_specification_596032_AtomicU16_3262325858__32_compareexchangeweak( atomic: &AtomicU16, current: u16, new: u16, success: Ordering, failure: Ordering, ) -> Result<u16, u16>

pub unsafe exec fn _verus_external_fn_specification_606032_AtomicU16_3262325858__32_fetch__and( atomic: &AtomicU16, val: u16, order: Ordering, ) -> u16

pub unsafe exec fn _verus_external_fn_specification_616032_AtomicU16_3262325858__32_fetch__nand( atomic: &AtomicU16, val: u16, order: Ordering, ) -> u16

pub unsafe exec fn _verus_external_fn_specification_626032_AtomicU16_3262325858__32_fetch__or( atomic: &AtomicU16, val: u16, order: Ordering, ) -> u16

pub unsafe exec fn _verus_external_fn_specification_636032_AtomicU16_3262325858__32_fetch__xor( atomic: &AtomicU16, val: u16, order: Ordering, ) -> u16

pub unsafe exec fn _verus_external_fn_specification_646032_AtomicU16_3262325858__32_load( atomic: &AtomicU16, order: Ordering, ) -> u16

pub unsafe exec fn _verus_external_fn_specification_656032_AtomicU16_3262325858__32_store( atomic: &AtomicU16, val: u16, order: Ordering, )

pub unsafe exec fn _verus_external_fn_specification_666032_AtomicU16_3262325858__32_swap( atomic: &AtomicU16, val: u16, order: Ordering, ) -> u16

pub unsafe exec fn _verus_external_fn_specification_676032_AtomicU16_3262325858__32_fetch__add( atomic: &AtomicU16, val: u16, order: Ordering, ) -> u16

pub unsafe exec fn _verus_external_fn_specification_686032_AtomicU16_3262325858__32_fetch__sub( atomic: &AtomicU16, val: u16, order: Ordering, ) -> u16

pub unsafe exec fn _verus_external_fn_specification_696032_AtomicU16_3262325858__32_fetch__min( atomic: &AtomicU16, val: u16, order: Ordering, ) -> u16

pub unsafe exec fn _verus_external_fn_specification_706032_AtomicU16_3262325858__32_fetch__max( atomic: &AtomicU16, val: u16, order: Ordering, ) -> u16

pub unsafe exec fn _verus_external_fn_specification_716032_AtomicU32_3262325858__32_new( v: u32, ) -> AtomicU32

pub unsafe exec fn _verus_external_fn_specification_726032_AtomicU32_3262325858__32_compare__exchange( atomic: &AtomicU32, current: u32, new: u32, success: Ordering, failure: Ordering, ) -> Result<u32, u32>

pub unsafe exec fn _verus_external_fn_specification_736032_AtomicU32_3262325858__32_compareexchangeweak( atomic: &AtomicU32, current: u32, new: u32, success: Ordering, failure: Ordering, ) -> Result<u32, u32>

pub unsafe exec fn _verus_external_fn_specification_746032_AtomicU32_3262325858__32_fetch__and( atomic: &AtomicU32, val: u32, order: Ordering, ) -> u32