Struct VstdSpecsForRustStdLib

Source

pub struct VstdSpecsForRustStdLib;

Implementations§

Source §

impl VstdSpecsForRustStdLib

Source

pub unsafe exec fn _verus_external_fn_specification_8656032__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_861_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_862_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_863_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_864_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_86860324232_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_86960324232_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_86660324232_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_86760324232_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_85760324232_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_85860324232_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_859_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_860_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_8546032__91_T_93326232585832_len<T>( slice: &[T], ) -> len : usize

ensures

len == spec_slice_len(slice),

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

Source

pub unsafe exec fn _verus_external_fn_specification_8556032__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_8566032__91_T_93326232585832_get_3258583260__32_I_32__62_<T, I>( slice: &[T], i: I, ) -> b : Option<&>::Output>
where I: SliceIndex<[T]>,

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

Source §

impl VstdSpecsForRustStdLib

Source

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

ensures

b == str_slice_is_ascii(s),

Specification for str::is_ascii

Source

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

ensures

s@ == res@,

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

Specification for str::to_owned

Source

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

ensures

b == string_is_ascii(s),

Specification for String::is_ascii

Source

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

ensures

res@ == s@,

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

Specification for String::as_str

Source

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

ensures

res@ == s@,

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

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

Source

pub unsafe exec fn _verus_external_fn_specification_8486032_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_8496032_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_850_String_325858__32_new() -> res : String

ensures

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

string_is_ascii(&res),

Specification for String::new

Source

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

ensures

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

string_is_ascii(&r),

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

Source

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

ensures

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

}),

Specification for str::chars

Source

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

ensures

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

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

        }
    }
}),

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

Source §

impl VstdSpecsForRustStdLib

Source

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

ensures

*result == x,

Specification for [alloc::boxed::box_new]

Source §

Specification for AtomicU8::swap

Source §

impl VstdSpecsForRustStdLib

Source

pub unsafe exec fn _verus_external_fn_specification_8276032_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_8286032_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_8296032_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_8306032_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_8136032_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_8146032_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_8156032_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_8166032_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_7996032_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_8006032_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_8016032_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_8026032_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_7856032_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_7866032_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_7876032_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_7886032_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_7716032_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_7726032_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_7736032_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_7746032_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_7576032_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_7586032_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_7596032_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_7606032_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_7436032_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_7446032_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_7456032_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_7466032_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_7296032_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_7306032_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_7316032_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_7326032_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_7156032_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_7166032_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_7176032_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_7186032_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_7016032_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_7026032_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_7036032_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_7046032_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_675_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_676_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_677_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_678_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_679_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_680_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_681_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_682_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_683_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_684_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_685_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_686_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_687_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_688_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_689_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_690_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_6696032_bool_32_as_32_Clone_3262325858__32_clone( b: &bool, ) -> res : bool

Specification for <bool as Clone>::clone

Source

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

Specification for <char as Clone>::clone

Source

pub unsafe exec fn _verus_external_fn_specification_67160323832__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_6726032__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_6736032_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_6746032_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_6536032_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_649_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_650_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_651_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_652_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_6466032_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_6476032_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_6486032_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_6376032_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_6386032_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_6396032_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_6406032_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_6356032_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 <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_594_core_325858__32_mem_325858__32_swap_3258583260__32_T_32__62_<T>( a: &mut T, b: &mut T, )

ensures

*a == *old(b),

*b == *old(a),

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

Source

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

ensures

r == i,

Specification for ::into_iter

Source

pub unsafe exec fn _verus_external_fn_specification_596_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_597_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_598_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_5936032_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_5926032_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_5916032_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_5906032_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_5896032_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_5886032_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_5876032_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_5866032_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_5856032_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_5846032_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_5836032_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_5826032_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_5816032_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_5806032_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_5796032_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_57860324041__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_5776032_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_5726032_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_57360323832__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_5746032_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_5756032__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_5766032__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_568_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_569_ManuallyDrop_3258583260__32_T_3262325858__32_into__inner<T>( m: ManuallyDrop<T>, ) -> T

Specification for ManuallyDrop::<T>::into_inner

Source

pub unsafe exec fn _verus_external_fn_specification_5706032_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_5716032_ManuallyDrop_326032_T_326232_as_32_Deref_3262325858__32_deref<T: ?Sized>( m: &ManuallyDrop<T>, ) -> res : &T

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

Source §

impl VstdSpecsForRustStdLib

Source

pub unsafe exec fn _verus_external_fn_specification_564_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_565_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_566_MaybeUninit_3258583260__32_T_3262325858__32_assume__init<T>( m: MaybeUninit<T>, ) -> T

requires

m.mem_contents().is_init(),

Specification for MaybeUninit::<T>::assume_init

Source

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

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_4146032_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_4156032_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_4166032_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_4176032_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_4186032_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_4196032_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_4206032_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_4216032_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_4226032_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_4236032_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_380_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_381_DefaultHasher_325858__32_write( state: &mut DefaultHasher, bytes: &[u8], )

ensures

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

Specification for DefaultHasher::write

Source

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

ensures

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

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

        }
    }
}),

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

Source

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

ensures

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

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

        }
    }
}),

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

Source

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

ensures

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

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

        }
    }
}),

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

Source

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

ensures

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

    },

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

Source

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

ensures

len == spec_hash_map_len(m),

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

Source

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

ensures

res == m@.is_empty(),

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

Source

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

ensures

other@ == this@,

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

Source

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

ensures

m@ == old(m)@,

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

Source

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

ensures

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

    },

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

Source

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

ensures

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

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

Source

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

ensures

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

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

Source

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

ensures

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

    },

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

Source

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

ensures

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

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

Source

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

ensures

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

    },

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

Source

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

ensures

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

    },

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

Source

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

ensures

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

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

        }
    }
}),

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

Source

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

ensures

len == spec_hash_set_len(m),

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

Source

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

ensures

res == m@.is_empty(),

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

Source

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

ensures

m@ == old(m)@,

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

Source

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

ensures

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

    },

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

Source

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

ensures

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

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

Source

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

ensures

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

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

Source

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

ensures

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

    },

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

Source

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

ensures

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

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

Source

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

ensures

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

    },

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

Source §

impl VstdSpecsForRustStdLib

Source

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

ensures

res == x,

Specification for u8::checked_rem

Source

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

Specification for u8::checked_rem_euclid

Source

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

Specification for u8::saturating_add

Source

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

Specification for u8::saturating_sub

Source

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

Specification for u8::is_multiple_of

Source §

impl VstdSpecsForRustStdLib

Source

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

ensures

res == x,

Source

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

ensures

res == x,

Specification for u16::checked_rem

Source

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

Specification for u16::checked_rem_euclid

Source

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

Specification for u16::saturating_add

Source

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

Specification for u16::saturating_sub

Source

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

Specification for u16::is_multiple_of

Source §

impl VstdSpecsForRustStdLib

Source

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

ensures

res == x,

Source

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

ensures

res == x,

Specification for u32::checked_rem

Source

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

Specification for u32::checked_rem_euclid

Source

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

Specification for u32::saturating_add

Source

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

Specification for u32::saturating_sub

Source

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

Specification for u32::is_multiple_of

Source §

impl VstdSpecsForRustStdLib

Source

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

ensures

res == x,

Source

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

ensures

res == x,

Specification for u64::checked_rem

Source

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

Specification for u64::checked_rem_euclid

Source

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

Specification for u64::saturating_add

Source

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

Specification for u64::saturating_sub

Source

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

Specification for u64::is_multiple_of

Source §

impl VstdSpecsForRustStdLib

Source

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

ensures

res == x,

Source

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

ensures

res == x,

Specification for u128::checked_rem

Source

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

Specification for u128::checked_rem_euclid

Source

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

Specification for u128::saturating_add

Source

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

Specification for u128::saturating_sub

Source

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

Specification for u128::is_multiple_of

Source §

impl VstdSpecsForRustStdLib

Source

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

ensures

res == x,

Source

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

ensures

res == x,

Specification for usize::checked_rem

Source

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

Specification for usize::checked_rem_euclid

Source

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

Specification for usize::saturating_add

Source

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

Specification for usize::saturating_sub

Source

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

Specification for usize::is_multiple_of

Source §

impl VstdSpecsForRustStdLib

Source

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

ensures

res == x,

Source

pub unsafe exec fn _verus_external_fn_specification_81_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_82_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_83_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_84_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_85_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_86_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_87_Option_3258583260__32_T_3262325858__32_take<T>( option: &mut Option<T>, ) -> t : Option<T>

ensures

t == *old(option),

*option is None,

Specification for Option::<T>::take

Source

pub unsafe exec fn _verus_external_fn_specification_88_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_89_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_90_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_91_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_92_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_93_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_946032_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_956032_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_966032_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_77_Range_3258583260__32_A_3262325858__32_next<A: Step>( range: &mut Range<A>, ) -> r : Option<A>

ensures

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

Specification for Range::<A>::next

Source

pub unsafe exec fn _verus_external_fn_specification_78_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_79_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_80_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 §

impl VstdSpecsForRustStdLib

Source

pub unsafe exec fn _verus_external_fn_specification_67_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_68_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_69_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_70_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_71_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_72_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_73_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_74_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_75_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_76_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_58_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_59_Iter_32585832603239_a_44__32_T_3262325858__32_next<'a, T>( elements: &mut Iter<'a, T>, ) -> r : Option<&'a T>

ensures

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

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

        }
    }
}),

Specification for Iter::<'a, T>::next

Source

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

ensures

({
    let (index, seq) = iter@;
    &&& index == 0
    &&& seq == s@

}),

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

Source

pub unsafe exec fn _verus_external_fn_specification_616032__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_626032__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_656032__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_30_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_31_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_326032_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_33_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_34_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_35_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_36_Vec_3258583260__32_T_44__32_A_3262325858__32_reserve<T, A: Allocator>( vec: &mut Vec<T, A>, additional: usize, )

ensures

vec@ == old(vec)@,

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

Source

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

vec@ == old(vec)@,

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

Source

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

ensures

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

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

Source

pub unsafe exec fn _verus_external_fn_specification_39_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])
        && vec@ == old(vec)@.subrange(0, old(vec)@.len() - 1),

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

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

Source

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

ensures

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

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

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

Source

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

ensures

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

forall |i: int| {
    0 <= i < vec@.len()
        ==> if i < old(vec)@.len() {
            vec@[i] == old(vec)@[i]
        } else {
            cloned::<T>(other@[i - old(vec)@.len()], vec@[i])
        }
},

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

Source

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

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_43_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

vec@ == old(vec)@.insert(i as int, element),

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

Source

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

vec@ == old(vec)@.remove(i as int),

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

Source

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

ensures

vec.view() == Seq::<T>::empty(),

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

Source

pub unsafe exec fn _verus_external_fn_specification_47_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_496032_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_50_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

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_516032_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_52_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() ==> vec@ == old(vec)@.subrange(0, len as int),

len > old(vec).len() ==> vec@ == old(vec)@,

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

Source

pub unsafe exec fn _verus_external_fn_specification_53_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() ==> vec@ == old(vec)@.subrange(0, len as int),

len > old(vec).len()
    ==> {
        &&& vec@.len() == len
        &&& vec@.subrange(0, old(vec).len() as int) == old(vec)@
        &&& forall |i| old(vec).len() <= i < len ==> cloned::<T>(value, vec@[i])

    },

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

Source

pub unsafe exec fn _verus_external_fn_specification_546032_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_55_IntoIter_3258583260__32_T_44__32_A_3262325858__32_next<T, A: Allocator>( elements: &mut IntoIter<T, A>, ) -> r : Option<T>

ensures

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

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

        }
    }
}),

Specification for IntoIter::<T, A>::next

Source

pub unsafe exec fn _verus_external_fn_specification_56_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_57_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@ == (0int, vec@),

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

Source §

impl VstdSpecsForRustStdLib

Source

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

requires

i < v.len(),

ensures

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

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

Source

pub unsafe exec fn _verus_external_fn_specification_11_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_12_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_136032_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_14_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_15_VecDeque_3258583260__32_T_44__32_A_3262325858__32_reserve<T, A: Allocator>( v: &mut VecDeque<T, A>, additional: usize, )

ensures

v@ == old(v)@,

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

Source

pub unsafe exec fn _verus_external_fn_specification_16_VecDeque_3258583260__32_T_44__32_A_3262325858__32_push__back<T, A: Allocator>( v: &mut VecDeque<T, A>, value: T, )

ensures

v@ == old(v)@.push(value),

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

Source

pub unsafe exec fn _verus_external_fn_specification_17_VecDeque_3258583260__32_T_44__32_A_3262325858__32_push__front<T, A: Allocator>( v: &mut VecDeque<T, A>, value: T, )

ensures

v@ == seq![value] + old(v)@,

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

Source

pub unsafe exec fn _verus_external_fn_specification_18_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]
        &&& v@ == old(v)@.subrange(0, old(v)@.len() as int - 1)

    ),
    None => (
        &&& old(v)@.len() == 0
        &&& v@ == old(v)@

    ),
},

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

Source

pub unsafe exec fn _verus_external_fn_specification_19_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]
        &&& v@ == old(v)@.subrange(1, old(v)@.len() as int)

    ),
    None => (
        &&& old(v)@.len() == 0
        &&& v@ == old(v)@

    ),
},

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

Source

pub unsafe exec fn _verus_external_fn_specification_20_VecDeque_3258583260__32_T_44__32_A_3262325858__32_append<T, A: Allocator>( v: &mut VecDeque<T, A>, other: &mut VecDeque<T, A>, )

ensures

v@ == old(v)@ + old(other)@,

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

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

Source

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

v@ == old(v)@.insert(i as int, element),

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

Source

pub unsafe exec fn _verus_external_fn_specification_22_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]
        &&& v@ == old(v)@.remove(i as int)

    ),
    None => (
        &&& old(v)@.len() <= i
        &&& v@ == old(v)@

    ),
},

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

Source

pub unsafe exec fn _verus_external_fn_specification_23_VecDeque_3258583260__32_T_44__32_A_3262325858__32_clear<T, A: Allocator>( v: &mut VecDeque<T, A>, )

ensures

v.view() == Seq::<T>::empty(),

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

Source

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

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_256032_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_26_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() ==> v@ == old(v)@.subrange(0, len as int),

len > old(v).len() ==> v@ == old(v)@,

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

Source

pub unsafe exec fn _verus_external_fn_specification_27_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() ==> v@ == old(v)@.subrange(0, len as int),

len > old(v).len()
    ==> {
        &&& v@.len() == len
        &&& v@.subrange(0, old(v).len() as int) == old(v)@
        &&& forall |i| old(v).len() <= i < len ==> cloned::<T>(value, v@[i])

    },

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

Source

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

ensures

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

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

        }
    }
}),

Specification for Iter::<'a, T>::next

Source

pub unsafe exec fn _verus_external_fn_specification_29_VecDeque_3258583260__32_T_44__32_A_3262325858__32_iter<'a, T, A: Allocator>( v: &'a VecDeque<T, A>, ) -> r : Iter<'a, T>

ensures

r@ == (0int, v@),

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

Source §

impl VstdSpecsForRustStdLib

Source

pub unsafe exec fn _verus_external_fn_specification_06032__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_1_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_26032_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_3_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_46032_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_5_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_66032_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_76032_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_8_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_9_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) }

VstdSpecsForRustStdLib

Struct VstdSpecsForRustStdLib Copy item path

Implementations§

impl VstdSpecsForRustStdLib

pub unsafe exec fn _verus_external_fn_specification_865__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_861_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_862_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_863_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_864_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_868__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_869__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_866__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_867__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_857__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_858__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_859_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_860_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_854__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_855__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_856__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_842_str_32__58__58__32_is__ascii( s: &str, ) -> b : bool

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

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

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

pub unsafe exec fn _verus_external_fn_specification_847__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_848__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_849__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_850_String_32__58__58__32_new() -> res : String

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

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

impl VstdSpecsForRustStdLib

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

impl VstdSpecsForRustStdLib

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

pub unsafe exec fn _verus_external_fn_specification_832__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_833__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_834__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_835__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_836__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_837__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_838__60__32_AtomicU8_32__62__32__58__58__32_load( atomic: &AtomicU8, order: Ordering, ) -> u8

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

pub unsafe exec fn _verus_external_fn_specification_840__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_827__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_828__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_829__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_830__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_817__60__32_AtomicU16_32__62__32__58__58__32_new( v: u16, ) -> AtomicU16

pub unsafe exec fn _verus_external_fn_specification_818__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_819__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_820__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_821__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_822__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_823__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_824__60__32_AtomicU16_32__62__32__58__58__32_load( atomic: &AtomicU16, order: Ordering, ) -> u16

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

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

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

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

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

impl VstdSpecsForRustStdLib

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

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

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

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

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

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

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

Struct VstdSpecsForRustStdLib

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

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

pub unsafe exec fn _verus_external_fn_specification_863_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_864_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_86860324232_mut_32_T_3262325858__32_addr<T: PointeeSized>( p: *mut T, ) -> addr : usize

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

pub unsafe exec fn _verus_external_fn_specification_86760324232_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_85760324232_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_85860324232_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_859_core_325858__32_ptr_325858__32_null<T: PointeeSized + Pointee<Metadata = ()>>() -> res : *const T

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

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

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

pub unsafe exec fn _verus_external_fn_specification_8566032__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_842_str_325858__32_is__ascii( s: &str, ) -> b : bool

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

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

pub unsafe exec fn _verus_external_fn_specification_845_String_325858__32_is__ascii( s: &String, ) -> b : bool

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

pub unsafe exec fn _verus_external_fn_specification_8476032_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_8486032_String_32_as_32_Clone_3262325858__32_clone( s: &String, ) -> res : String

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

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

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

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

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

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

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

pub unsafe exec fn _verus_external_fn_specification_8326032_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_8336032_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_8346032_AtomicU8_3262325858__32_fetch__and( atomic: &AtomicU8, val: u8, order: Ordering, ) -> u8

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

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

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

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

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

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

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

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

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

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

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

pub unsafe exec fn _verus_external_fn_specification_8186032_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_8196032_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_8206032_AtomicU16_3262325858__32_fetch__and( atomic: &AtomicU16, val: u16, order: Ordering, ) -> u16

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

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

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

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

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

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

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

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

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

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

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

pub unsafe exec fn _verus_external_fn_specification_8046032_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_8056032_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_8066032_AtomicU32_3262325858__32_fetch__and( atomic: &AtomicU32, val: u32, order: Ordering, ) -> u32

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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