Equality via extensionality

In the specification libraries section, we introduced the extensional equality operator =~= to check equivalence for Seq, Set, and Map.

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.a =~= f2.a);  // succeeds
    // assert(f1 == f2);    // FAILS
    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.)

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); // 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); // FAILS
    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); // FAILS
    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
}