Trait PartialEqSpecImpl 

pub trait PartialEqSpecImpl<Rhs: PointeeSized = Self>: PointeeSized + PartialEq<Rhs> {
    // Required methods
    exec fn obeys_eq_spec() -> bool;
    exec fn eq_spec(&self, other: &Rhs) -> bool;
}

Required Methods

exec fn obeys_eq_spec() -> bool

exec fn eq_spec(&self, other: &Rhs) -> bool

Dyn Compatibility

This trait is not dyn compatible.

In older versions of Rust, dyn compatibility was called "object safety".

Implementations on Foreign Types

impl PartialEqSpecImpl for String

Available on verus_keep_ghost and crate feature alloc and non-verus_verify_core only.

open spec fn obeys_eq_spec() -> bool

{ true }

open spec fn eq_spec(&self, other: &String) -> bool

{ self@ == other@ }

impl PartialEqSpecImpl for bool

open spec fn obeys_eq_spec() -> bool

{ true }

open spec fn eq_spec(&self, other: &bool) -> bool

{ *self == *other }

impl PartialEqSpecImpl for char

open spec fn obeys_eq_spec() -> bool

{ true }

open spec fn eq_spec(&self, other: &char) -> bool

{ *self == *other }

impl PartialEqSpecImpl for i8

open spec fn obeys_eq_spec() -> bool

{ true }

open spec fn eq_spec(&self, other: &i8) -> bool

{ *self == *other }

impl PartialEqSpecImpl for i16

open spec fn obeys_eq_spec() -> bool

{ true }

open spec fn eq_spec(&self, other: &i16) -> bool

{ *self == *other }

impl PartialEqSpecImpl for i32

open spec fn obeys_eq_spec() -> bool

{ true }

open spec fn eq_spec(&self, other: &i32) -> bool

{ *self == *other }

impl PartialEqSpecImpl for i64

open spec fn obeys_eq_spec() -> bool

{ true }

open spec fn eq_spec(&self, other: &i64) -> bool

{ *self == *other }

impl PartialEqSpecImpl for i128

open spec fn obeys_eq_spec() -> bool

{ true }

open spec fn eq_spec(&self, other: &i128) -> bool

{ *self == *other }

impl PartialEqSpecImpl for isize

open spec fn obeys_eq_spec() -> bool

{ true }

open spec fn eq_spec(&self, other: &isize) -> bool

{ *self == *other }

impl PartialEqSpecImpl for str

Available on verus_keep_ghost and non-verus_verify_core only.

open spec fn obeys_eq_spec() -> bool

{ true }

open spec fn eq_spec(&self, other: &str) -> bool

{ self@ == other@ }

impl PartialEqSpecImpl for u8

open spec fn obeys_eq_spec() -> bool

{ true }

open spec fn eq_spec(&self, other: &u8) -> bool

{ *self == *other }

impl PartialEqSpecImpl for u16

open spec fn obeys_eq_spec() -> bool

{ true }

open spec fn eq_spec(&self, other: &u16) -> bool

{ *self == *other }

impl PartialEqSpecImpl for u32

open spec fn obeys_eq_spec() -> bool

{ true }

open spec fn eq_spec(&self, other: &u32) -> bool

{ *self == *other }

impl PartialEqSpecImpl for u64

open spec fn obeys_eq_spec() -> bool

{ true }

open spec fn eq_spec(&self, other: &u64) -> bool

{ *self == *other }

impl PartialEqSpecImpl for u128

open spec fn obeys_eq_spec() -> bool

{ true }

open spec fn eq_spec(&self, other: &u128) -> bool

{ *self == *other }

impl PartialEqSpecImpl for usize

open spec fn obeys_eq_spec() -> bool

{ true }

open spec fn eq_spec(&self, other: &usize) -> bool

{ *self == *other }

impl<'a, T, U, const N: usize> PartialEqSpecImpl<&'a [U]> for [T; N]

where T: PartialEq<U> + PartialEqSpec<U>,

open spec fn obeys_eq_spec() -> bool

{ <T as super::cmp::PartialEqSpec<U>>::obeys_eq_spec() }

open spec fn eq_spec(&self, other: &&'a [U]) -> bool

{
    &&& self@.len() == (*other)@.len()
    &&& forall |i: int| {
        0 <= i < self@.len()
            ==> <T as super::cmp::PartialEqSpec<U>>::eq_spec(&self@[i], &(*other)@[i])
    }

}

impl<'a, T, U, const N: usize> PartialEqSpecImpl<[U; N]> for &'a [T]

where T: PartialEq<U> + PartialEqSpec<U>,

open spec fn obeys_eq_spec() -> bool

{ <T as super::cmp::PartialEqSpec<U>>::obeys_eq_spec() }

open spec fn eq_spec(&self, other: &[U; N]) -> bool

{
    &&& (*self)@.len() == other@.len()
    &&& forall |i: int| {
        0 <= i < (*self)@.len()
            ==> <T as super::cmp::PartialEqSpec<U>>::eq_spec(&(*self)@[i], &other@[i])
    }

}

impl<A, B: PointeeSized> PartialEqSpecImpl<&B> for &A

where A: PartialEq<B> + PointeeSized,

open spec fn obeys_eq_spec() -> bool

{ <A as PartialEqSpec<B>>::obeys_eq_spec() }

open spec fn eq_spec(&self, other: &&B) -> bool

{ <A as PartialEqSpec<B>>::eq_spec(*self, *other) }

impl<A: PartialEq + PartialEqSpec, Z: PartialEq + PartialEqSpec, Y: PartialEq + PartialEqSpec, X: PartialEq + PartialEqSpec, W: PartialEq + PartialEqSpec, V: PartialEq + PartialEqSpec, U: PartialEq + PartialEqSpec, T: PartialEq + PartialEqSpec> PartialEqSpecImpl for (A, Z, Y, X, W, V, U, T)

open spec fn obeys_eq_spec() -> bool

{
    &&& A::obeys_eq_spec()
    &&& Z::obeys_eq_spec()
    &&& Y::obeys_eq_spec()
    &&& X::obeys_eq_spec()
    &&& W::obeys_eq_spec()
    &&& V::obeys_eq_spec()
    &&& U::obeys_eq_spec()
    &&& T::obeys_eq_spec()

}

open spec fn eq_spec(&self, other: &(A, Z, Y, X, W, V, U, T)) -> bool

{
    &&& A::eq_spec(&self.0, &other.0)
    &&& Z::eq_spec(&self.1, &other.1)
    &&& Y::eq_spec(&self.2, &other.2)
    &&& X::eq_spec(&self.3, &other.3)
    &&& W::eq_spec(&self.4, &other.4)
    &&& V::eq_spec(&self.5, &other.5)
    &&& U::eq_spec(&self.6, &other.6)
    &&& T::eq_spec(&self.7, &other.7)

}

impl<B: PartialEq + PartialEqSpec, A: PartialEq + PartialEqSpec, Z: PartialEq + PartialEqSpec, Y: PartialEq + PartialEqSpec, X: PartialEq + PartialEqSpec, W: PartialEq + PartialEqSpec, V: PartialEq + PartialEqSpec, U: PartialEq + PartialEqSpec, T: PartialEq + PartialEqSpec> PartialEqSpecImpl for (B, A, Z, Y, X, W, V, U, T)

open spec fn obeys_eq_spec() -> bool

{
    &&& B::obeys_eq_spec()
    &&& A::obeys_eq_spec()
    &&& Z::obeys_eq_spec()
    &&& Y::obeys_eq_spec()
    &&& X::obeys_eq_spec()
    &&& W::obeys_eq_spec()
    &&& V::obeys_eq_spec()
    &&& U::obeys_eq_spec()
    &&& T::obeys_eq_spec()

}

open spec fn eq_spec(&self, other: &(B, A, Z, Y, X, W, V, U, T)) -> bool

{
    &&& B::eq_spec(&self.0, &other.0)
    &&& A::eq_spec(&self.1, &other.1)
    &&& Z::eq_spec(&self.2, &other.2)
    &&& Y::eq_spec(&self.3, &other.3)
    &&& X::eq_spec(&self.4, &other.4)
    &&& W::eq_spec(&self.5, &other.5)
    &&& V::eq_spec(&self.6, &other.6)
    &&& U::eq_spec(&self.7, &other.7)
    &&& T::eq_spec(&self.8, &other.8)

}

impl<C: PartialEq + PartialEqSpec, B: PartialEq + PartialEqSpec, A: PartialEq + PartialEqSpec, Z: PartialEq + PartialEqSpec, Y: PartialEq + PartialEqSpec, X: PartialEq + PartialEqSpec, W: PartialEq + PartialEqSpec, V: PartialEq + PartialEqSpec, U: PartialEq + PartialEqSpec, T: PartialEq + PartialEqSpec> PartialEqSpecImpl for (C, B, A, Z, Y, X, W, V, U, T)

open spec fn obeys_eq_spec() -> bool

{
    &&& C::obeys_eq_spec()
    &&& B::obeys_eq_spec()
    &&& A::obeys_eq_spec()
    &&& Z::obeys_eq_spec()
    &&& Y::obeys_eq_spec()
    &&& X::obeys_eq_spec()
    &&& W::obeys_eq_spec()
    &&& V::obeys_eq_spec()
    &&& U::obeys_eq_spec()
    &&& T::obeys_eq_spec()

}

open spec fn eq_spec(&self, other: &(C, B, A, Z, Y, X, W, V, U, T)) -> bool

{
    &&& C::eq_spec(&self.0, &other.0)
    &&& B::eq_spec(&self.1, &other.1)
    &&& A::eq_spec(&self.2, &other.2)
    &&& Z::eq_spec(&self.3, &other.3)
    &&& Y::eq_spec(&self.4, &other.4)
    &&& X::eq_spec(&self.5, &other.5)
    &&& W::eq_spec(&self.6, &other.6)
    &&& V::eq_spec(&self.7, &other.7)
    &&& U::eq_spec(&self.8, &other.8)
    &&& T::eq_spec(&self.9, &other.9)

}

impl<D: PartialEq + PartialEqSpec, C: PartialEq + PartialEqSpec, B: PartialEq + PartialEqSpec, A: PartialEq + PartialEqSpec, Z: PartialEq + PartialEqSpec, Y: PartialEq + PartialEqSpec, X: PartialEq + PartialEqSpec, W: PartialEq + PartialEqSpec, V: PartialEq + PartialEqSpec, U: PartialEq + PartialEqSpec, T: PartialEq + PartialEqSpec> PartialEqSpecImpl for (D, C, B, A, Z, Y, X, W, V, U, T)

open spec fn obeys_eq_spec() -> bool

{
    &&& D::obeys_eq_spec()
    &&& C::obeys_eq_spec()
    &&& B::obeys_eq_spec()
    &&& A::obeys_eq_spec()
    &&& Z::obeys_eq_spec()
    &&& Y::obeys_eq_spec()
    &&& X::obeys_eq_spec()
    &&& W::obeys_eq_spec()
    &&& V::obeys_eq_spec()
    &&& U::obeys_eq_spec()
    &&& T::obeys_eq_spec()

}

open spec fn eq_spec(&self, other: &(D, C, B, A, Z, Y, X, W, V, U, T)) -> bool

{
    &&& D::eq_spec(&self.0, &other.0)
    &&& C::eq_spec(&self.1, &other.1)
    &&& B::eq_spec(&self.2, &other.2)
    &&& A::eq_spec(&self.3, &other.3)
    &&& Z::eq_spec(&self.4, &other.4)
    &&& Y::eq_spec(&self.5, &other.5)
    &&& X::eq_spec(&self.6, &other.6)
    &&& W::eq_spec(&self.7, &other.7)
    &&& V::eq_spec(&self.8, &other.8)
    &&& U::eq_spec(&self.9, &other.9)
    &&& T::eq_spec(&self.10, &other.10)

}

impl<E: PartialEq + PartialEqSpec, D: PartialEq + PartialEqSpec, C: PartialEq + PartialEqSpec, B: PartialEq + PartialEqSpec, A: PartialEq + PartialEqSpec, Z: PartialEq + PartialEqSpec, Y: PartialEq + PartialEqSpec, X: PartialEq + PartialEqSpec, W: PartialEq + PartialEqSpec, V: PartialEq + PartialEqSpec, U: PartialEq + PartialEqSpec, T: PartialEq + PartialEqSpec> PartialEqSpecImpl for (E, D, C, B, A, Z, Y, X, W, V, U, T)

open spec fn obeys_eq_spec() -> bool

{
    &&& E::obeys_eq_spec()
    &&& D::obeys_eq_spec()
    &&& C::obeys_eq_spec()
    &&& B::obeys_eq_spec()
    &&& A::obeys_eq_spec()
    &&& Z::obeys_eq_spec()
    &&& Y::obeys_eq_spec()
    &&& X::obeys_eq_spec()
    &&& W::obeys_eq_spec()
    &&& V::obeys_eq_spec()
    &&& U::obeys_eq_spec()
    &&& T::obeys_eq_spec()

}

open spec fn eq_spec(&self, other: &(E, D, C, B, A, Z, Y, X, W, V, U, T)) -> bool

{
    &&& E::eq_spec(&self.0, &other.0)
    &&& D::eq_spec(&self.1, &other.1)
    &&& C::eq_spec(&self.2, &other.2)
    &&& B::eq_spec(&self.3, &other.3)
    &&& A::eq_spec(&self.4, &other.4)
    &&& Z::eq_spec(&self.5, &other.5)
    &&& Y::eq_spec(&self.6, &other.6)
    &&& X::eq_spec(&self.7, &other.7)
    &&& W::eq_spec(&self.8, &other.8)
    &&& V::eq_spec(&self.9, &other.9)
    &&& U::eq_spec(&self.10, &other.10)
    &&& T::eq_spec(&self.11, &other.11)

}

impl<K: ObeysDeepEq + Hash + Eq, V: ObeysDeepEq, S: BuildHasher, A: Allocator> PartialEqSpecImpl for HashMap<K, V, S, A>

Available on verus_keep_ghost only.

HashMap’s == compares lengths and then values key by key, which is deep-view equality when both K and V obey deep equality.

open spec fn obeys_eq_spec() -> bool

{ crate::std_specs::hash::builds_valid_hashers::<S>() }

open spec fn eq_spec(&self, other: &Self) -> bool

{ self.deep_view() == other.deep_view() }

impl<T, U, const N: usize> PartialEqSpecImpl<[U; N]> for [T; N]

where T: PartialEq<U> + PartialEqSpec<U>,

open spec fn obeys_eq_spec() -> bool

{ <T as super::cmp::PartialEqSpec<U>>::obeys_eq_spec() }

open spec fn eq_spec(&self, other: &[U; N]) -> bool

{
    forall |i: int| {
        0 <= i < N
            ==> <T as super::cmp::PartialEqSpec<U>>::eq_spec(&self@[i], &other@[i])
    }
}

impl<T, U, const N: usize> PartialEqSpecImpl<[U; N]> for [T]

where T: PartialEq<U> + PartialEqSpec<U>,

open spec fn obeys_eq_spec() -> bool

{ <T as super::cmp::PartialEqSpec<U>>::obeys_eq_spec() }

open spec fn eq_spec(&self, other: &[U; N]) -> bool

{
    &&& self@.len() == other@.len()
    &&& forall |i: int| {
        0 <= i < self@.len()
            ==> <T as super::cmp::PartialEqSpec<U>>::eq_spec(&self@[i], &other@[i])
    }

}

impl<T, U, const N: usize> PartialEqSpecImpl<[U]> for [T; N]

where T: PartialEq<U> + PartialEqSpec<U>,

open spec fn obeys_eq_spec() -> bool

{ <T as super::cmp::PartialEqSpec<U>>::obeys_eq_spec() }

open spec fn eq_spec(&self, other: &[U]) -> bool

{
    &&& self@.len() == other@.len()
    &&& forall |i: int| {
        0 <= i < self@.len()
            ==> <T as super::cmp::PartialEqSpec<U>>::eq_spec(&self@[i], &other@[i])
    }

}

impl<T, U> PartialEqSpecImpl<[U]> for [T]

where T: PartialEq<U> + PartialEqSpec<U>,

open spec fn obeys_eq_spec() -> bool

{ <T as super::cmp::PartialEqSpec<U>>::obeys_eq_spec() }

open spec fn eq_spec(&self, other: &[U]) -> bool

{
    &&& self@.len() == other@.len()
    &&& forall |i: int| {
        0 <= i < self@.len()
            ==> <T as super::cmp::PartialEqSpec<U>>::eq_spec(&self@[i], &other@[i])
    }

}

impl<T: ObeysDeepEq + Hash + Eq, S: BuildHasher, A: Allocator> PartialEqSpecImpl for HashSet<T, S, A>

Available on verus_keep_ghost only.

HashSet’s == compares lengths and then membership, which is deep-view equality when T obeys deep equality.

open spec fn obeys_eq_spec() -> bool

{ crate::std_specs::hash::builds_valid_hashers::<S>() }

open spec fn eq_spec(&self, other: &Self) -> bool

{ self.deep_view() == other.deep_view() }

impl<T: ObeysDeepEq, E: ObeysDeepEq> PartialEqSpecImpl for Result<T, E>

Available on verus_keep_ghost only.

open spec fn obeys_eq_spec() -> bool

{ true }

open spec fn eq_spec(&self, other: &Self) -> bool

{ self.deep_view() == other.deep_view() }

impl<T: PartialEq + ?Sized, A: Allocator> PartialEqSpecImpl for Box<T, A>

Available on crate feature alloc only.

open spec fn obeys_eq_spec() -> bool

{ T::obeys_eq_spec() }

open spec fn eq_spec(&self, other: &Self) -> bool

{ <T as PartialEqSpec>::eq_spec(&**self, &**other) }

impl<T: PartialEq + PartialEqSpec> PartialEqSpecImpl for (T,)

open spec fn obeys_eq_spec() -> bool

{
    &&& T::obeys_eq_spec()

}

open spec fn eq_spec(&self, other: &(T,)) -> bool

{
    &&& T::eq_spec(&self.0, &other.0)

}

impl<T: PartialEqSpec<U>, U, A1: Allocator, A2: Allocator> PartialEqSpecImpl<Vec<U, A2>> for Vec<T, A1>

open spec fn obeys_eq_spec() -> bool

{ T::obeys_eq_spec() }

open spec fn eq_spec(&self, other: &Vec<U, A2>) -> bool

{
    &&& self.len() == other.len()
    &&& forall |i: int| 0 <= i < self.len() ==> self[i].eq_spec(&other[i])

}

impl<T: PartialEqSpec> PartialEqSpecImpl for Option<T>

open spec fn obeys_eq_spec() -> bool

{ T::obeys_eq_spec() }

open spec fn eq_spec(&self, other: &Option<T>) -> bool

{
    match (self, other) {
        (None, None) => true,
        (Some(x), Some(y)) => x.eq_spec(y),
        _ => false,
    }
}

impl<T: ZeroablePrimitive + PartialEqSpec> PartialEqSpecImpl for NonZero<T>

open spec fn obeys_eq_spec() -> bool

{ true }

open spec fn eq_spec(&self, other: &Self) -> bool

{ self.get().eq_spec(&other.get()) }

impl<U: PartialEq + PartialEqSpec, T: PartialEq + PartialEqSpec> PartialEqSpecImpl for (U, T)

open spec fn obeys_eq_spec() -> bool

{
    &&& U::obeys_eq_spec()
    &&& T::obeys_eq_spec()

}

open spec fn eq_spec(&self, other: &(U, T)) -> bool

{
    &&& U::eq_spec(&self.0, &other.0)
    &&& T::eq_spec(&self.1, &other.1)

}

impl<V: PartialEq + PartialEqSpec, U: PartialEq + PartialEqSpec, T: PartialEq + PartialEqSpec> PartialEqSpecImpl for (V, U, T)

open spec fn obeys_eq_spec() -> bool

{
    &&& V::obeys_eq_spec()
    &&& U::obeys_eq_spec()
    &&& T::obeys_eq_spec()

}

open spec fn eq_spec(&self, other: &(V, U, T)) -> bool

{
    &&& V::eq_spec(&self.0, &other.0)
    &&& U::eq_spec(&self.1, &other.1)
    &&& T::eq_spec(&self.2, &other.2)

}

impl<W: PartialEq + PartialEqSpec, V: PartialEq + PartialEqSpec, U: PartialEq + PartialEqSpec, T: PartialEq + PartialEqSpec> PartialEqSpecImpl for (W, V, U, T)

open spec fn obeys_eq_spec() -> bool

{
    &&& W::obeys_eq_spec()
    &&& V::obeys_eq_spec()
    &&& U::obeys_eq_spec()
    &&& T::obeys_eq_spec()

}

open spec fn eq_spec(&self, other: &(W, V, U, T)) -> bool

{
    &&& W::eq_spec(&self.0, &other.0)
    &&& V::eq_spec(&self.1, &other.1)
    &&& U::eq_spec(&self.2, &other.2)
    &&& T::eq_spec(&self.3, &other.3)

}

impl<X: PartialEq + PartialEqSpec, W: PartialEq + PartialEqSpec, V: PartialEq + PartialEqSpec, U: PartialEq + PartialEqSpec, T: PartialEq + PartialEqSpec> PartialEqSpecImpl for (X, W, V, U, T)

open spec fn obeys_eq_spec() -> bool

{
    &&& X::obeys_eq_spec()
    &&& W::obeys_eq_spec()
    &&& V::obeys_eq_spec()
    &&& U::obeys_eq_spec()
    &&& T::obeys_eq_spec()

}

open spec fn eq_spec(&self, other: &(X, W, V, U, T)) -> bool

{
    &&& X::eq_spec(&self.0, &other.0)
    &&& W::eq_spec(&self.1, &other.1)
    &&& V::eq_spec(&self.2, &other.2)
    &&& U::eq_spec(&self.3, &other.3)
    &&& T::eq_spec(&self.4, &other.4)

}

impl<Y: PartialEq + PartialEqSpec, X: PartialEq + PartialEqSpec, W: PartialEq + PartialEqSpec, V: PartialEq + PartialEqSpec, U: PartialEq + PartialEqSpec, T: PartialEq + PartialEqSpec> PartialEqSpecImpl for (Y, X, W, V, U, T)

open spec fn obeys_eq_spec() -> bool

{
    &&& Y::obeys_eq_spec()
    &&& X::obeys_eq_spec()
    &&& W::obeys_eq_spec()
    &&& V::obeys_eq_spec()
    &&& U::obeys_eq_spec()
    &&& T::obeys_eq_spec()

}

open spec fn eq_spec(&self, other: &(Y, X, W, V, U, T)) -> bool

{
    &&& Y::eq_spec(&self.0, &other.0)
    &&& X::eq_spec(&self.1, &other.1)
    &&& W::eq_spec(&self.2, &other.2)
    &&& V::eq_spec(&self.3, &other.3)
    &&& U::eq_spec(&self.4, &other.4)
    &&& T::eq_spec(&self.5, &other.5)

}

impl<Z: PartialEq + PartialEqSpec, Y: PartialEq + PartialEqSpec, X: PartialEq + PartialEqSpec, W: PartialEq + PartialEqSpec, V: PartialEq + PartialEqSpec, U: PartialEq + PartialEqSpec, T: PartialEq + PartialEqSpec> PartialEqSpecImpl for (Z, Y, X, W, V, U, T)

open spec fn obeys_eq_spec() -> bool

{
    &&& Z::obeys_eq_spec()
    &&& Y::obeys_eq_spec()
    &&& X::obeys_eq_spec()
    &&& W::obeys_eq_spec()
    &&& V::obeys_eq_spec()
    &&& U::obeys_eq_spec()
    &&& T::obeys_eq_spec()

}

open spec fn eq_spec(&self, other: &(Z, Y, X, W, V, U, T)) -> bool

{
    &&& Z::eq_spec(&self.0, &other.0)
    &&& Y::eq_spec(&self.1, &other.1)
    &&& X::eq_spec(&self.2, &other.2)
    &&& W::eq_spec(&self.3, &other.3)
    &&& V::eq_spec(&self.4, &other.4)
    &&& U::eq_spec(&self.5, &other.5)
    &&& T::eq_spec(&self.6, &other.6)

}

Implementors

impl<T: ObeysDeepEq + Hash + Eq> PartialEqSpecImpl for ExecMultiset<T>

Available on verus_keep_ghost only.

impl<T: ObeysDeepEq> PartialEqSpecImpl for ExecMemContents<T>

Available on verus_keep_ghost only.