Executable libraries: Vec

The previous section discussed the mathematical collection types Seq, Set, and Map. This section will discuss Vec, an executable implementation of Seq. Verus supports some functionality of Rust’s std::vec::Vec type. To use Vec, include use std::vec::Vec; in your code.

You can allocate Vec using Vec::new and then push elements into it:

fn test_vec1() {
    let mut v: Vec<u32> = Vec::new();
    v.push(0);
    v.push(10);
    v.push(20);
    v.push(30);
    v.push(40);
    assert(v.len() == 5);
    assert(v[2] == 20);
    assert(v[3] == 30);
    v.set(2, 21);
    assert(v[2] == 21);
    assert(v[3] == 30);
}

The code above is able to make assertions directly about the Vec value v. You could also write more compilicated specifications and proofs about Vec values. In general, though, Verus encourages programmers to write spec functions and proof functions about mathematical types like Seq, Set, and Map instead of hard-wiring the specifications and proofs to particular concrete datatypes like Vec. This allows spec functions and proof functions to focus on the essential ideas, written in terms of mathematical types like Seq, Set, Map, int, and nat, rather than having to fiddle around with finite-width integers like usize, worry about arithmetic overflow, etc.

Of course, there needs to be a connection between the mathematical types and the concrete types, and specifications in exec functions will commonly have to move back and forth between mathematical abstractions and concrete reality. To make this easier, Verus supports the syntactic sugar @ for extracting a mathematical view from a concrete type. For example, v@ returns a Seq of all the elements in the vector v:

spec fn has_five_sorted_numbers(s: Seq<u32>) -> bool {
    s.len() == 5 && s[0] <= s[1] <= s[2] <= s[3] <= s[4]
}

fn test_vec2() {
    let mut v: Vec<u32> = Vec::new();
    v.push(0);
    v.push(10);
    v.push(20);
    v.push(30);
    v.push(40);
    v.set(2, 21);
    assert(v@ =~= seq![0, 10, 21, 30, 40]);
    assert(v@ =~= seq![0, 10] + seq![21] + seq![30, 40]);
    assert(v@[2] == 21);
    assert(v@[3] == 30);
    assert(v@.subrange(2, 4) =~= seq![21, 30]);
    assert(has_five_sorted_numbers(v@));
}

Using the Seq view of the Vec allows us to use the various features of Seq, such as concatenation and subsequences, when writing specifications about the Vec contents.

Verus support for std::vec::Vec is currently being expanded. For up-to-date documentation, visit this link. Note that these functions provide specifications for std::vec::Vec functions. Thus, for example, ex_vec_insert represents support for the Vec function insert. Code written in Verus should use insert rather than ex_vec_insert.

Documentation for std::vec::Vec functionality can be found here.