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
}