Adding Ambient Facts to the Proof Environment with broadcast
In a typical Verus project, a developer might prove a fact (e.g., that reversing a sequence preserves its length) in a proof function, e.g.,
pub proof fn seq_reverse_len<A>(s: Seq<A>)
ensures
reverse(s).len() == s.len(),
{
...
}
To make use of this fact, the developer must explicitly invoke the proof function, e.g.,
fn example(s: Seq<bool>) {
let t = reverse(s);
// assert(t.len() == s.len()); // FAILS
seq_reverse(s); // Adds the proof's fact to the proof environment
assert(t.len() == s.len()); // SUCCEEDS
}
However, in some cases, a proof fact is so useful that a developer always wants it to be in scope, without manually invoking the corresponding proof. For example, the fact that an empty sequence’s length is zero is so “obvious” that most programmers will expect Verus to always know it. This feature should be used with caution, however, as every extra ambient fact slows the prover’s overall performance.
Suppose that after considering the impact on the solver’s performance, the
programmer decides to make the above fact about reverse
ambient. To do so,
they can add the broadcast
modifier in the
definition of seq_reverse_len
: pub broadcast proof fn seq_reverse_len<A>(s: Seq<A>)
.
The effect is to introduce the following
quantified fact to the proof environment:
forall |s| reverse(s).len() == s.len()
Because this introduces a quantifier, Verus will typically ask you to
explicitly choose a trigger, e.g., by adding a #[trigger]
annotation.
Hence, the final version of our example might look like this:
pub broadcast proof fn seq_reverse_len<A>(s: Seq<A>)
ensures
#[trigger] reverse(s).len() == s.len(),
{
...
}
To bring this ambient lemma into scope, for a specific proof, or for an entire
module, you can use broadcast use seq_reverse_len;
.
Some of these broadcast-ed lemmas are available in the verus standard library vstd
,
some as part of broadcast “groups”, which combine a number of properties into a single
group name, which can be brought into scope with broadcast use broadcast_group_name;
.
We are working on extending the discoverablility of these groups in the standard library
documentation: they currently appear as regular functions.