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 these sequences were constructed in different ways:

{{#include ../../../../examples/guide/lib_examples.rs:test_eq2}}

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:

{{#include ../../../../examples/guide/ext_equal.rs:ext_eq_struct_fields}}

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:

{{#include ../../../../examples/guide/ext_equal.rs:ext_eq_struct}}

(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:

{{#include ../../../../examples/guide/ext_equal.rs:ext_eq_nested}}

The same applies to spec_fn, as in:

{{#include ../../../../examples/guide/ext_equal.rs:ext_eq_fnspec}}