Struct VstdSpecsForRustStdLib

Source

pub struct VstdSpecsForRustStdLib;

Implementations§

Source §

impl VstdSpecsForRustStdLib

Source

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

ensures

iter == spec_array_iter(s),

IteratorSpec::decrease(&iter) is Some,

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

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

Source

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

ensures

ar@ == out@,

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

Source §

impl VstdSpecsForRustStdLib

Source

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

ensures

res == f,

Specification for <f32 as Clone>::clone

Source

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

ensures

res == f,

Specification for <f64 as Clone>::clone

Source §

impl VstdSpecsForRustStdLib

Source

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

ensures

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

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

Source

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

ensures

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

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

Source

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

ensures

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

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

Source

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

ensures

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

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

Source §

impl VstdSpecsForRustStdLib

Source

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

ensures

addr == spec_addr(p),

Specification for <*mut T>::addr

Source

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

ensures

q == spec_with_addr(p, addr),

Specification for <*mut T>::with_addr

Source §

impl VstdSpecsForRustStdLib

Source

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

ensures

addr == spec_addr(p),

Specification for <*const T>::addr

Source

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

ensures

q == spec_with_addr(p, addr),

Specification for <*const T>::with_addr

Source §

impl VstdSpecsForRustStdLib

Source

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

ensures

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

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

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

Source

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

ensures

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

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

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

Source

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

ensures

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

Specification for core::ptr::null

Source

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

ensures

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

Specification for core::ptr::null_mut

Source §

impl VstdSpecsForRustStdLib

Source

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

returns

spec_slice_len(slice),

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

Source

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

ensures

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

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

Source

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

returns

spec_slice_get(slice, i),

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

Source §

impl VstdSpecsForRustStdLib

Source

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

ensures

b == is_ascii(s),

Specification for str::is_ascii

Source

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

ensures

s@ == res@,

Specification for str::to_owned

Source

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

ensures

b@ == s.spec_bytes(),

Specification for str::as_bytes

Source

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

returns

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

Specification for str::len

Source

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

returns

s@.len() == 0,

Specification for str::is_empty

Source

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

returns

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

Specification for str::is_char_boundary

Source

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

requires

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

ensures

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

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

Specification for str::split_at

Source

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

requires

valid_utf8(v@),

ensures

res.spec_bytes() =~= v@,

Specification for str::from_utf8_unchecked

Source

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

ensures

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

Specification for <T as ToString>::to_string

Source

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

ensures

res@ == s@,

Specification for String::as_str

Source

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

ensures

res@ == s@,

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

Source

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

ensures

res == s,

Specification for <String as Clone>::clone

Source

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

ensures

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

Specification for <String as PartialEq>::eq

Source

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

ensures

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

Specification for String::new

Source

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

ensures

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

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

Source

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

ensures

iter == spec_iter(s),

IteratorSpec::decrease(&iter) is Some,

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

Specification for str::chars

Source

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

ensures

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

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

Source §

impl VstdSpecsForRustStdLib

Source

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

requires

vals.mem_contents() is Init,

ensures

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

Specification for [alloc::boxed::box_assume_init_into_vec_unsafe]

Source

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

ensures

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

Specification for alloc::intrinsics::write_box_via_move

Source

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

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

Source §

Specification for AtomicU8::swap

Source §

impl VstdSpecsForRustStdLib

Source

pub unsafe exec fn _verus_external_fn_specification_10016032_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_10026032_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_10036032_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_10046032_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_9876032_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_9886032_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_9896032_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_9906032_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_9736032_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_9746032_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_9756032_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_9766032_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_9596032_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_9606032_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_9616032_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_9626032_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_9456032_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_9466032_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_9476032_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_9486032_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_9316032_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_9326032_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_9336032_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_9346032_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_9176032_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_9186032_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_9196032_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_9206032_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_9036032_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_9046032_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_9056032_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_9066032_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_8896032_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_8906032_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_8916032_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_8926032_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_8756032_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_8766032_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_8776032_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_8786032_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_35_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_36_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_37_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_38_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_39_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_40_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_41_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_42_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_43_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_44_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_45_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_46_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_47_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_48_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_49_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_50_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_516032_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_526032_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_5360323832__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_546032__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_556032_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_566032_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_576032_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_81_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_82_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_83_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_84_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_856032_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_866032_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_876032_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_936032_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_946032_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_956032_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_966032_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_976032_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_1026032_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_201_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_202_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_203_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_204_bool_325858__32_then<T, F: FnOnce() -> T>( b: bool, f: F, ) -> ret : Option<T>

ensures

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

Specification for bool::then

Source §

impl VstdSpecsForRustStdLib

Source

pub unsafe exec fn _verus_external_fn_specification_2056032_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_2066032_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_2076032_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_2086032_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_2096032_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_2106032_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_2116032_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_2126032_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_2136032_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_2146032_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_2156032_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_2166032_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_2176032_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_2186032_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_2196032_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_22060324041__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_2216032_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_2226032_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_22360323832__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_2246032_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_2256032__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_2266032__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_2276032_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_228_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_229_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_2306032_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_2316032_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_232_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_233_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_234_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_235_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_236_MaybeUninit_3258583260__32_T_3262325858__32_assumeinitmut<T>( m: &mut MaybeUninit<T>, ) -> ret : &mut T

requires

m.mem_contents().is_init(),

ensures

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

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

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

Specification for MaybeUninit::<T>::assume_init_mut

Source §

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

Source §

Source §

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

Source §

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

Source §

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

Source §

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

Source §

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

Source §

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

Source §

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

Source §

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

Source §

Source §

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

Source §

impl VstdSpecsForRustStdLib

Source

pub unsafe exec fn _verus_external_fn_specification_3776032_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_3786032_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_3796032_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_3806032_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_3816032_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_3826032_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_3836032_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_3846032_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_3856032_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_3866032_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_387_BTreeMap_3258583260__32_Key_44__32_Value_44__32_A_3262325858__32_iter<'a, Key, Value, A: Allocator + Clone>( m: &'a BTreeMap<Key, Value, A>, ) -> iter : Iter<'a, Key, Value>

ensures

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

    },

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

Source

pub unsafe exec fn _verus_external_fn_specification_388_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_389_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_3906032_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_391_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_3926032_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_393_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_394_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_395_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_396_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_397_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_398_BTreeMap_3258583260__32_Key_44__32_Value_44__32_A_3262325858__32_keys<'a, Key, Value, A: Allocator + Clone>( m: &'a BTreeMap<Key, Value, A>, ) -> keys : Keys<'a, Key, Value>

ensures

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

    },

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

Source

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

ensures

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

        }

    },

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

Source

pub unsafe exec fn _verus_external_fn_specification_400_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_401_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_4026032_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_403_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_4046032_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_405_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_406_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_407_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_408_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_409_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_410_BTreeSet_3258583260__32_Key_44__32_A_3262325858__32_iter<'a, Key, A: Allocator + Clone>( m: &'a BTreeSet<Key, A>, ) -> r : Iter<'a, Key>

ensures

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

    },

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

Source §

impl VstdSpecsForRustStdLib

Source

pub unsafe exec fn _verus_external_fn_specification_454_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_455_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_411_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_412_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_413_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_414_HashMap_3258583260__32_Key_44__32_Value_44__32_S_44__32_A_3262325858__32_iter<'a, Key, Value, S, A: Allocator>( m: &'a HashMap<Key, Value, S, A>, ) -> iter : Iter<'a, Key, Value>

ensures

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

    },

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

Source

pub unsafe exec fn _verus_external_fn_specification_415_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_416_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_4176032_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@ == this@,

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

Source

pub unsafe exec fn _verus_external_fn_specification_418_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_4196032_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_420_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_421_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_422_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_423_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_424_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_425_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_426_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_427_HashMap_3258583260__32_Key_44__32_Value_44__32_S_44__32_A_3262325858__32_keys<'a, Key, Value, S, A: Allocator>( m: &'a HashMap<Key, Value, S, A>, ) -> keys : Keys<'a, Key, Value>

ensures

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

    },

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

Source

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

ensures

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

    },

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

Source

pub unsafe exec fn _verus_external_fn_specification_429_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_430_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_431_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_4326032_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_433_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_434_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_435_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_436_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_437_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_438_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_439_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_440_HashSet_3258583260__32_Key_44__32_S_44__32_A_3262325858__32_iter<'a, Key, S, A: Allocator>( m: &'a HashSet<Key, S, A>, ) -> hash_keys : Iter<'a, Key>

ensures

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

    },

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

Source

pub unsafe exec fn _verus_external_fn_specification_441_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_442_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_443_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_444_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_445_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_446_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_447_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_448_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_449_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_450_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_451_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_452_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_453_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_4566032_u8_32_as_32_Clone_3262325858__32_clone( x: &u8, ) -> res : u8

ensures

res == x,

Source

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

ensures

res == x,

Source

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

ensures

res == x,

Source

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

ensures

res == x,

Source

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

ensures

res == x,

Source

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

ensures

res == x,

Source

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

ensures

res == x,

Source

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

ensures

res == x,

Source

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

ensures

res == x,

Source

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

ensures

res == x,

Source

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

ensures

res == x,

Source

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

ensures

res == x,

Source

pub unsafe exec fn _verus_external_fn_specification_756_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_757_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_758_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_759_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_760_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_761_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_762_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_763_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_764_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_765_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_766_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_767_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_768_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_7696032_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_7706032_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_7716032_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_779_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_780_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_781_RangeInclusive_3258583260__32_Idx_3262325858__32_new<Idx>( start: Idx, end: Idx, ) -> ret : RangeInclusive<Idx>

ensures

ret@.start == start,

ret@.end == end,

ret@.exhausted == false,

Specification for RangeInclusive::<Idx>::new

Source

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

ensures

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

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

Source §

impl VstdSpecsForRustStdLib

Source

pub unsafe exec fn _verus_external_fn_specification_783_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_784_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_785_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_786_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_787_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_788_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_789_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_790_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_791_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_792_Result_3258583260__32_T_44__32_E_3262325858__32_err<T, E>( result: Result<T, E>, ) -> opt : Option<E>

ensures

opt == err(result),

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

Source §

impl VstdSpecsForRustStdLib

Source

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

returns

slice@[i as int],

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

Source

pub unsafe exec fn _verus_external_fn_specification_7946032_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_7956032__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_7966032__91_T_59__32_N_93__32_as_32_Index_326032_I_32623262325858__32_index<T, I, const N: usize>( array: &[T; N], index: I, ) -> output : &<[T; N] as Index>::Output
where [T]: Index,

ensures

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

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

Source

pub unsafe exec fn _verus_external_fn_specification_797_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_7986032__91_T_93326232585832_iter<'a, T>( s: &'a [T], ) -> iter : Iter<'a, T>

ensures

iter == spec_slice_iter(s),

IteratorSpec::decrease(&iter) is Some,

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

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

Source

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

ensures

iter == spec_slice_iter(s),

IteratorSpec::decrease(&iter) is Some,

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

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

Source

pub unsafe exec fn _verus_external_fn_specification_8006032__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_8016032__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_8046032__91_T_93326232585832_split__at<T>( slice: &[T], mid: usize, ) -> ret : (&[T], &[T])

requires

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

ensures

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

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

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

Source §

impl VstdSpecsForRustStdLib

Source

pub unsafe exec fn _verus_external_fn_specification_806_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_807_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_8086032_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_809_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_810_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_811_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_812_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_813_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_814_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_815_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_816_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_817_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_818_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_819_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_820_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_8216032_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_822_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_823_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_824_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_8266032_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_8276032_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_828_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_8296032_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_830_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_831_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_8326032_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_833_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_834_Vec_3258583260__32_T_44__32_A_3262325858__32_into__iter<T, A: Allocator>( vec: Vec<T, A>, ) -> iter : <Vec<T, A> as IntoIterator>::IntoIter ⓘ

ensures

iter == spec_into_iter(vec),

IteratorSpec::decrease(&iter) is Some,

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

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

Source

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

ensures

iter == spec_into_iter_borrowed(vec),

IteratorSpec::decrease(&iter) is Some,

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

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

Source §

impl VstdSpecsForRustStdLib

Source

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

ensures

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

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

Source

pub unsafe exec fn _verus_external_fn_specification_837_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_838_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_8396032_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_840_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_841_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_842_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_843_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_844_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_845_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_846_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_847_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_848_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_849_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_850_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_8516032_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_852_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_853_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_854_VecDeque_3258583260__32_T_44__32_A_3262325858__32_iter<'a, T, A: Allocator>( v: &'a VecDeque<T, A>, ) -> iter : Iter<'a, T>

ensures

iter == spec_iter(v),

IteratorSpec::decrease(&iter) is Some,

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

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

Source §

impl VstdSpecsForRustStdLib

Source

pub unsafe exec fn _verus_external_fn_specification_8556032__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_856_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_8576032_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_858_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_8596032_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_860_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_8616032_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_8626032_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_863_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_864_Rc_3258583260__32_T_44__32_A_3262325858__32_into__inner<T, A: Allocator>( v: Rc<T, A>, ) -> result : Option<T>

ensures

result matches Some(t) ==> t == *v,

Source §

open spec fn obeys_into_spec() -> bool

{ <U as FromSpec<Self>>::obeys_from_spec() }

Source §

open spec fn into_spec(self) -> U

{ U::from_spec(self) }

Source §

impl<T, U> TryFrom for T
where U: Into<T>,

Source §

type Error = Infallible

The type returned in the event of a conversion error.

Source §

fn try_from(value: U) -> Result<T, <T as TryFrom>::Error>

Performs the conversion.

fn try_into(self) -> Result<U, >::Error>

Performs the conversion.

Source §

impl<T, VERUS_SPEC__A> TryIntoSpec<T> for VERUS_SPEC__A
where VERUS_SPEC__A: TryInto<T>,

Source §

exec fn obeys_try_into_spec() -> bool

Source §

exec fn try_into_spec(self) -> Result<T, <VERUS_SPEC__A as TryInto<T>>::Error>

Source §

impl<T, U> TryIntoSpecImpl for T
where U: TryFrom<T>,

Source §

open spec fn obeys_try_into_spec() -> bool

{ <U as TryFromSpec<Self>>::obeys_try_from_spec() }

Source §

open spec fn try_into_spec(self) -> Result<U, >::Error>

{ <U as TryFromSpec<Self>>::try_from_spec(self) }

§

impl<A> SpecEq<&A> for A
where A: ?Sized,

§

impl<A> SpecEq<&mut A> for A
where A: ?Sized,

§

impl<A> SpecEq<A> for A
where A: ?Sized,

§

impl<A> SpecEq<Ghost<A>> for A

§

VstdSpecsForRustStdLib

Struct VstdSpecsForRustStdLib Copy item path

Implementations§

impl VstdSpecsForRustStdLib

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

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

impl VstdSpecsForRustStdLib

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

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

impl VstdSpecsForRustStdLib

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

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

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

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

impl VstdSpecsForRustStdLib

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

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

impl VstdSpecsForRustStdLib

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

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

impl VstdSpecsForRustStdLib

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

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

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

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

impl VstdSpecsForRustStdLib

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

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

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

impl VstdSpecsForRustStdLib

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

impl VstdSpecsForRustStdLib

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

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

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

impl VstdSpecsForRustStdLib

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

pub unsafe exec fn _verus_external_fn_specification_1006__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_1007__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_1008__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_1009__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_1010__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_1011__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_1012__60__32_AtomicU8_32__62__32__58__58__32_load( atomic: &AtomicU8, order: Ordering, ) -> u8

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

pub unsafe exec fn _verus_external_fn_specification_1014__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_1001__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_1002__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_1003__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_1004__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_991__60__32_AtomicU16_32__62__32__58__58__32_new( v: u16, ) -> AtomicU16

pub unsafe exec fn _verus_external_fn_specification_992__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_993__60__32_AtomicU16_32__62__32__58__58__32_compare__exchange__weak( atomic: &AtomicU16, current: u16, new: u16, success: Ordering, failure: Ordering, ) -> Result<u16, u16>

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

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

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

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

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

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

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

impl VstdSpecsForRustStdLib

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

Struct VstdSpecsForRustStdLib

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

pub unsafe exec fn _verus_external_fn_specification_10066032_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_10076032_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_10086032_AtomicU8_3262325858__32_fetch__and( atomic: &AtomicU8, val: u8, order: Ordering, ) -> u8

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

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

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

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

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

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

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

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

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

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

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

pub unsafe exec fn _verus_external_fn_specification_9926032_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_9936032_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_9946032_AtomicU16_3262325858__32_fetch__and( atomic: &AtomicU16, val: u16, order: Ordering, ) -> u16

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

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

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

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

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

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

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

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

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

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

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

pub unsafe exec fn _verus_external_fn_specification_9786032_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_9796032_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_9806032_AtomicU32_3262325858__32_fetch__and( atomic: &AtomicU32, val: u32, order: Ordering, ) -> u32

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

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

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

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

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

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

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

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