Trigger annotations

To every quantifier expression (forall, exists, choose) in the program, including “implicit” quantifiers such as in broadcast lemmas.

There are many implications of triggers on proof automation that Verus developers should be aware of. See the relevant chapter of the guide, particulary the section on multiple triggers and matching loops.

This page explains the procedure Verus uses to determine these triggers from Verus source code.

Terminology: trigger groups and trigger expressions

Every quantifier has a number of quantifier variables. To control how the solver instantiates these variables, trigger groups are used.

• To every quantifier, Verus determines a collection of trigger groups.
• Every trigger group is a collection of trigger expressions.

By necessity, any trigger group is only well-formed if every quantifier variable is used by at least one trigger expression in the group.

Note that:

• The SMT solver will instantiate any quantifier whenever any trigger group fires.
• However, a trigger group will only fire if every expression in the group matches.

Therefore:

• Having more trigger groups makes the quantifier be instantiated more often.
• A trigger group with more trigger expressions will fire less often.

Selecting trigger groups

Verus determines the collection of trigger groups as follows:

• Verus finds all applicable #[trigger] and #[trigger(n)] annotations in the body of the quantifier.
  • In the case of nested quantifiers, every #[trigger] or #[trigger(n)] annotation is applicable to exactly one quantifier expression: the innermost quantifier which binds a variable used by the trigger expression.
• All applicable expressions marked by #[trigger] become a trigger group.
• All applicable expressions marked by #[trigger(n)] for the same n become a trigger group.
• Every annotation #![trigger EXPR1, …, EXPRk] at the root of the quantifier expression becomes a trigger group.
• If, after all of the above, no trigger groups have been identified, Verus may use heuristics to determine the trigger group(s) based on the body of the quantifier expression.
  • If #![all_triggers] is provided, Verus uses an “aggressive” strategy, all trigger groups that can reasonably be inferred as applicable from the body.
  • If #![auto] is provided, Verus uses a “conservative” strategy that selects only on trigger group.
  • If neither #![all_triggers] nor #![auto] are provided, Verus uses the same “conservative” strategy as it does for #![auto].
• If, after all of the above, Verus is unable to find any trigger groups, it produces an error.

Trigger logging

By default, Verus often prints verbose information about selected triggers in cases where Verus’s heuristics are “un-confident” in the selected trigger groups. You can silence this information on a case-by-case basis using the #![auto] attribute. When #![auto] is applied to a quantifier, this tells Verus that you want the automatically selected triggers even when Verus is un-confident, in which case this logging will be silenced.

The behavior can be configured through the command line: