Specification libraries: Seq, Set, Map

The Verus libraries contain types Seq<T>, Set<T>, and Map<Key, Value> for representing sequences, sets, and maps in specifications. In contrast to executable Rust collection datatypes in std::collections, the Seq, Set and Map types represent collections of arbitrary size. For example, while the len() method of std::collections::HashSet returns a length of type usize, which is bounded, the len() methods of Seq and Set return lengths of type nat, which is unbounded. Furthermore, Set and Map can represent infinite sets and maps. (Sequences, on the other hand, are always finite.) This allows specifications to talk about collections that are larger than could be contained in the physical memory of a computer.

Constructing and using Seq, Set, Map

The seq!, set!, and map! macros construct values of type Seq, Set, and Map with particular contents:

proof fn test_seq1() {
    let s: Seq<int> = seq![0, 10, 20, 30, 40];
    assert(s.len() == 5);
    assert(s[2] == 20);
    assert(s[3] == 30);
}

proof fn test_set1() {
    let s: Set<int> = set![0, 10, 20, 30, 40];
    assert(s.finite());
    assert(s.contains(20));
    assert(s.contains(30));
    assert(!s.contains(60));
}

proof fn test_map1() {
    let m: Map<int, int> = map![0 => 0, 10 => 100, 20 => 200, 30 => 300, 40 => 400];
    assert(m.dom().contains(20));
    assert(m.dom().contains(30));
    assert(!m.dom().contains(60));
    assert(m[20] == 200);
    assert(m[30] == 300);
}

The macros above can only construct finite sequences, sets, and maps. There are also functions Seq::new, Set::new, and Map::new, which can allocate both finite values and (for sets and maps) infinite values:

proof fn test_seq2() {
    let s: Seq<int> = Seq::new(5, |i: int| 10 * i);
    assert(s.len() == 5);
    assert(s[2] == 20);
    assert(s[3] == 30);
}

proof fn test_set2() {
    let s: Set<int> = Set::new(|i: int| 0 <= i <= 40 && i % 10 == 0);
    assert(s.contains(20));
    assert(s.contains(30));
    assert(!s.contains(60));

    let s_infinite: Set<int> = Set::new(|i: int| i % 10 == 0);
    assert(s_infinite.contains(20));
    assert(s_infinite.contains(30));
    assert(!s_infinite.contains(35));
}

proof fn test_map2() {
    let m: Map<int, int> = Map::new(|i: int| 0 <= i <= 40 && i % 10 == 0, |i: int| 10 * i);
    assert(m[20] == 200);
    assert(m[30] == 300);

    let m_infinite: Map<int, int> = Map::new(|i: int| i % 10 == 0, |i: int| 10 * i);
    assert(m_infinite[20] == 200);
    assert(m_infinite[30] == 300);
    assert(m_infinite[90] == 900);
}

Each Map<Key, Value> value has a domain of type Set<Key> given by .dom(). In the test_map2 example above, m’s domain is the finite set {0, 10, 20, 30, 40}, while m_infinite’s domain is the infinite set {..., -20, 10, 0, 10, 20, ...}.

For more operations, including sequence contenation (.add or +), sequence update, sequence subrange, set union (.union or +), set intersection (.intersect), etc., see:

Proving properties of Seq, Set, Map

The SMT solver will prove some properties about Seq, Set, and Map automatically, as shown in the examples above. However, some other properties may require calling lemmas in the library or may require proofs by induction.

If two collections (Seq, Set, or Map) have the same elements, Verus considers them to be equal. This is known as equality via extensionality. However, the SMT solver will in general not automatically recognize that the two collections are equal if the collections were constructed in different ways. For example, the following 3 sequences are equal, but asserting equality fails:

proof fn test_eq_fail() {
    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); // FAILS, even though it's true
    assert(s1 === s3); // FAILS, even though it's true
}

To convince the SMT solver that s1, s2, and s3 are equal, we have to explicitly assert the equality via the extensional equality operator =~=, rather than just the ordinary equality operator ==. Using =~= forces the SMT solver to check that all the elements of the collections are equal, which it would not ordinarily do. Once we’ve explicitly proven equality via extensionality, we can then successfully assert ==:

proof fn test_eq() {
    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);
    assert(s1 === s2);  // succeeds
    assert(s1 === s3);  // succeeds
}

(See the Equality via extensionality section for more details.)

Proofs about set cardinality (Set::len) and set finiteness (Set::finite) often require inductive proofs. For example, the exact cardinality of the intersection of two sets depends on which elements the two sets have in common. If the two sets are disjoint, the intersection’s cardinality will be 0, but otherwise, the intersections’s cardinality will be some non-zero value. Let’s try to prove that the intersection’s cardinality is no larger than either of the two sets’ cardinalities. Without loss of generality, we can just prove that the intersection’s cardinality is no larger than the first set’s cardinality: s1.intersect(s2).len() <= s1.len().

The proof (which is found in set_lib.rs) is by induction on the size of the set s1. In the induction step, we need to make s1 smaller, which means we need to remove an element from it. The two methods .choose and .remove allow us to choose an arbitrary element from s1 and remove it:

let a = s1.choose();
... s1.remove(a) ...

Based on this, we expect an inductive proof to look something like the following, where the inductive step removes s1.choose():

pub proof fn lemma_len_intersect<A>(s1: Set<A>, s2: Set<A>)
    requires
        s1.finite(),
    ensures
        s1.intersect(s2).len() <= s1.len(),
    decreases
        s1.len(),
{
    if s1.is_empty() {

    } else {
        let a = s1.choose();

        lemma_len_intersect(s1.remove(a), s2);
    }
}

Unfortunately, Verus fails to verify this proof. Therefore, we’ll need to fill in the base case and induction case with some more detail. Before adding this detail to the code, let’s think about what a fully explicit proof might look like if we wrote it out by hand:

pub proof fn lemma_len_intersect<A>(s1: Set<A>, s2: Set<A>)
    requires
        s1.finite(),
    ensures
        s1.intersect(s2).len() <= s1.len(),
    decreases
        s1.len(),
{
    if s1.is_empty() {
        // s1 is the empty set.
        // Therefore, s1.intersect(s2) is also empty.
        // So both s1.len() and s1.intersect(s2).len() are 0,
        // and 0 <= 0.
    } else {
        // s1 is not empty, so it has at least one element.
        // Let a be an element from s1.
        // Let s1' be the set s1 with the element a removed (i.e. s1' == s1 - {a}).
        // Removing an element decreases the cardinality by 1, so s1'.len() == s1.len() - 1.
        // By induction, s1'.intersect(s2).len() <= s1'.len(), so:
        //   (s1 - {a}).intersect(s2).len() <= s1'.len()
        //   (s1.intersect(s2) - {a}).len() <= s1'.len()
        //   (s1.intersect(s2) - {a}).len() <= s1.len() - 1
        // case a in s1.intersect(s2):
        //   (s1.intersect(s2) - {a}).len() == s1.intersect(s2).len() - 1
        // case a not in s1.intersect(s2):
        //   (s1.intersect(s2) - {a}).len() == s1.intersect(s2).len()
        // In either case:
        //   s1.intersect(s2).len() <= (s1.intersect(s2) - {a}).len() + 1
        // Putting all the inequalities together:
        //   s1.intersect(s2).len() <= (s1.intersect(s2) - {a}).len() + 1 <= (s1.len() - 1) + 1
        // So:
        //   s1.intersect(s2).len() <= (s1.len() - 1) + 1
        //   s1.intersect(s2).len() <= s1.len()
    }
}

For such a simple property, this is a surprisingly long proof! Fortunately, the SMT solver can automatically prove most of the steps written above. What it will not automatically prove, though, is any step requiring equality via extensionality, as discussed earlier. The two crucial steps requiring equality via extensionality are:

“Therefore, s1.intersect(s2) is also empty.”
Replacing (s1 - {a}).intersect(s2) with s1.intersect(s2) - {a}

For these, we need to explicitly invoke =~=:

pub proof fn lemma_len_intersect<A>(s1: Set<A>, s2: Set<A>)
    requires
        s1.finite(),
    ensures
        s1.intersect(s2).len() <= s1.len(),
    decreases
        s1.len(),
{
    if s1.is_empty() {
        assert(s1.intersect(s2) =~= s1);
    } else {
        let a = s1.choose();
        assert(s1.intersect(s2).remove(a) =~= s1.remove(a).intersect(s2));
        lemma_len_intersect(s1.remove(a), s2);
    }
}

With this, Verus and the SMT solver successfully complete the proof. However, Verus and the SMT solver aren’t the only audience for this proof. Anyone maintaining this code might want to know why we invoked =~=, and we probably shouldn’t force them to work out the entire hand-written proof above to rediscover this. So although it’s not strictly necessary, it’s probably polite to wrap the assertions in assert...by to indicate the purpose of the =~=:

pub proof fn lemma_len_intersect<A>(s1: Set<A>, s2: Set<A>)
    requires
        s1.finite(),
    ensures
        s1.intersect(s2).len() <= s1.len(),
    decreases s1.len(),
{
    if s1.is_empty() {
        assert(s1.intersect(s2).len() == 0) by {
            assert(s1.intersect(s2) =~= s1);
        }
    } else {
        let a = s1.choose();
        lemma_len_intersect(s1.remove(a), s2);
        // by induction: s1.remove(a).intersect(s2).len() <= s1.remove(a).len()
        assert(s1.intersect(s2).remove(a).len() <= s1.remove(a).len()) by {
            assert(s1.intersect(s2).remove(a) =~= s1.remove(a).intersect(s2));
        }
        // simplifying ".remove(a).len()" yields s1.intersect(s2).len() <= s1.len())

    }
}

Verus Tutorial and Reference

Specification libraries: Seq, Set, Map

Constructing and using Seq, Set, Map

Proving properties of Seq, Set, Map