Spec quantifiers (forall, exists)
For an intuition-guided introduction to quantifiers and triggers, see the Quantifiers tutorial, specifically forall and triggers and exists and choose.
Both forall and exists are spec-mode only expressions.
Syntax
forall_expr ::= forall |binders...| spec_expr
exists_expr ::= exists |binders...| spec_expr
The body spec_expr may include trigger annotations.
Typing
The body spec_expr must have type bool. The bound variables are available as spec-mode
variables within the body. Both forall and exists expressions have type bool.
Semantics
forall|x: T| P(x) is true if and only if P(x) is true for every value x of type T.
exists|x: T| P(x) is true if and only if there exists at least one value x of type T
such that P(x) is true.
The two are duals. Verus uses classical logic, so:
exists|x: T| P(x) ≡ !forall|x: T| !P(x)
Both quantifiers support binding multiple variables simultaneously, which is equivalent to nesting single-variable quantifiers:
// These two are equivalent:
forall|i: int, j: int| i < j ==> f(i) <= f(j)
forall|i: int| forall|j: int| i < j ==> f(i) <= f(j)Triggers
Because quantifiers range over infinite domains, the SMT solver does not enumerate all possible instantiations. Instead it uses triggers: syntactic patterns that, when matched by terms in the proof context, cause the quantifier to be instantiated with the matching values.
Every quantifier must have at least one trigger group. Verus can choose triggers automatically, or they can be specified explicitly using annotations on the quantifier body:
| Annotation | Meaning |
|---|---|
#[trigger] on a sub-expression | That sub-expression is a trigger (grouped with other #[trigger] annotations) |
#[trigger(n)] on a sub-expression | That sub-expression is part of trigger group n |
#![trigger expr1, expr2, ...] at the root of the body | expr1, expr2, ... form a single trigger group |
#![auto] at the root of the body | Use automatic trigger selection and suppress the trigger-logging note |
#![all_triggers] at the root of the body | Use aggressive automatic trigger selection |
For full details on how Verus selects and validates trigger groups, see Trigger annotations.