Equality

Equality behaves differently in ghost code than in executable code. In executable code, Rust defines == to mean a call to the eq function of the PartialEq trait:

fn equal1(x: u8, y: u8) {
    let eq1 = x == y;  // means x.eq(y) in Rust
    let eq2 = y == x;  // means y.eq(x) in Rust
    assert(eq1 ==> eq2);  // succeeds
}

For built-in integer types like u8, the x.eq(y) function is defined as we’d expect, returning true if x and y hold the same integers. For user-defined types, though, eq could have other behaviors: it might have side effects, behave nondeterministically, or fail to fulfill its promise to implement an equivalence relation, even if the type implements the Rust Eq trait:

fn equal2<A: Eq>(x: A, y: A) {
    let eq1 = x == y; // means x.eq(y) in Rust
    let eq2 = y == x; // means y.eq(x) in Rust
    assert(eq1 ==> eq2); // won't work; we can't be sure that A is an equivalence relation
}

In ghost code, by contrast, the == operator is always an equivalence relation (i.e. it is reflexive, symmetric, and transitive):

fn equal3(x: u8, y: u8) {
    assert({
        let eq1 = x == y;
        let eq2 = y == x;
        eq1 ==> eq2
    });
}

Verus defines == in ghost code to be true when:

• for two integers or booleans, the values are equal
• for two structs or enums, the types are the same and the fields are equal
• for two & references, two Box values, two Rc values, or two Arc values, the pointed-to values are the same
• for two RefCell values or two Cell values, the pointers to the interior data are equal (not the interior contents)

In addition, collection dataypes such as Seq<T>, Set<T>, and Map<Key, Value> have their own definitions of ==, where two sequences, two sets, or two maps are equal if their elements are equal. As explained more in specification libraries and extensional equality, these sometimes require the “extensional equality” operator =~= to help prove equality between two sequences, two sets, or two maps.