Equality via extensionality

The specification libraries section introduced the extensional equality operator =~= to check equivalence for collection types like Seq, Set, and Map. Extensional equality proves that two collections are equal by proving that the collections contain equal elements. This can be used, for example, to prove that the sequences s1, s2, and s3 are equal because they have the same elements (0, 10, 20, 30, 40), even though this sequences were constructed in different ways:

proof fn check_eq(x: Seq<int>, y: Seq<int>)
    requires
        x == y,
{
}

proof fn test_eq2() {
    let s1: Seq<int> = seq![0, 10, 20, 30, 40];
    let s2: Seq<int> = seq![0, 10] + seq![20] + seq![30, 40];
    let s3: Seq<int> = Seq::new(5, |i: int| 10 * i);
    assert(s1 =~= s2);
    assert(s1 =~= s3);
    check_eq(s1, s2); // succeeds
    check_eq(s1, s3); // succeeds
}

Assertions like assert(s1 =~= s2) are common for proving equality via extensionality. Note that by default, Verus promotes == to =~= inside assert, ensures, and invariant, so that, for example, assert(s1 == s2) actually means assert(s1 =~= s2). This is convenient in many cases where extensional equality is merely a minor step in a larger proof, and you don’t want to clutter the proof with low-level details about equality. For proofs where extensional equality is the key step, you may want to explicitly write assert(s1 =~= s2) for documentation’s sake.

(If you don’t want Verus to auto-promote == to =~=, perhaps because you want to see exactly where extensional equality is really needed, the #[verifier::auto_ext_equal(...)] and #![verifier::auto_ext_equal(...)] attributes can override Verus’s default behavior. See ext_equal.rs for examples.)

Extensional equality for structs and enums

Suppose that a struct or enum datatype has a field containing Seq, Set, and Map, and suppose that we’d like to prove that two values of the datatype are equal. We could do this by using =~= on each field individually:

    struct Foo {
        a: Seq<int>,
        b: Set<int>,
    }

    proof fn ext_equal_struct() {
        let f1 = Foo { a: seq![1, 2, 3], b: set!{4, 5, 6} };
        let f2 = Foo { a: seq![1, 2].push(3), b: set!{5, 6}.insert(4) };
        // assert(f1 == f2);    // FAILS -- need to use =~= first
        assert(f1.a =~= f2.a);  // succeeds
        assert(f1.b =~= f2.b);  // succeeds
        assert(f1 == f2);  // succeeds, now that we've used =~= on .a and .b
    }

However, it’s rather painful to use =~= on each field every time to check for equivalence. To help with this, Verus supports the #[verifier::ext_equal] attribute to mark datatypes that need extensionality on Seq, Set, Map, Multiset, spec_fn fields or fields of other #[verifier::ext_equal] datatypes. For example:

#[verifier::ext_equal]  // necessary for invoking =~= on the struct
struct Foo {
    a: Seq<int>,
    b: Set<int>,
}

proof fn ext_equal_struct() {
    let f1 = Foo { a: seq![1, 2, 3], b: set!{4, 5, 6} };
    let f2 = Foo { a: seq![1, 2].push(3), b: set!{5, 6}.insert(4) };
    assert(f1 =~= f2);  // succeeds
}

(Note: adding #[verifier::ext_equal] does not change the meaning of ==; it just makes it more convenient to use =~= to prove == on datatypes.)

Deep extensional equality

Collection datatypes like sequences and sets can contain other collection datatypes as elements (for example, a sequence of sequences, or set of sequences). The =~= operator only applies extensionality to the top-level collection, not to the nested elements of the collection. To also apply extensionality to the elements, Verus provides a “deep” extensional equality operator =~~= that handles arbitrary nesting of collections, spec_fn, and datatypes. For example:

proof fn ext_equal_nested() {
    let inner: Set<int> = set!{1, 2, 3};
    let s1: Seq<Set<int>> = seq![inner];
    let s2 = s1.update(0, s1[0].insert(1));
    let s3 = s1.update(0, s1[0].insert(2).insert(3));
    // assert(s2 =~= s3); // FAILS
    assert(s2 =~~= s3);  // succeeds
    let s4: Seq<Seq<Set<int>>> = seq![s1];
    let s5: Seq<Seq<Set<int>>> = seq![s2];
    assert(s4 =~~= s5);  // succeeds
}

The same applies to spec_fn, as in:

#[verifier::ext_equal]  // necessary for invoking =~= on the struct
struct Bar {
    a: spec_fn(int) -> int,
}

proof fn ext_equal_fnspec(n: int) {
    // basic case
    let f1 = (|i: int| i + 1);
    let f2 = (|i: int| 1 + i);
    assert(f1 =~= f2);  // succeeds
    // struct case
    let b1 = Bar { a: |i: int| if i == 1 { i } else { 1 } };
    let b2 = Bar { a: |i: int| 1int };
    assert(b1 =~= b2);  // succeeds
    // nested case
    let i1 = (|i: int| i + 2);
    let i2 = (|i: int| 2 + i);
    let n1: Seq<spec_fn(int) -> int> = seq![i1];
    let n2: Seq<spec_fn(int) -> int> = seq![i2];
    // assert(n1 =~= n2); // FAILS
    assert(n1 =~~= n2);  // succeeds
}