Quantifiers

Verum has first-class quantifier expressions — forall and exists — usable anywhere an expression is expected: inside refinements, ensures / requires clauses, @verify checks, and theorem statements. They are not runtime primitives; the compiler lowers them to SMT terms for the verifier.

The three binding forms

forall_expr =
    'forall' , quantifier_binding , { ',' , quantifier_binding } , '.' , expression ;

exists_expr =
    'exists' , quantifier_binding , { ',' , quantifier_binding } , '.' , expression ;

quantifier_binding =
    pattern , [ ':' , type_expr ] , [ 'in' , expression ]
    , [ 'where' , expression ] ;

The grammar unifies three styles:

Type-based — the set is the type

forall x: Int. x + 0 == x
exists y: Float. y * y == 2.0

Read: "for every integer x, x + 0 == x", "there exists a float y with y² = 2".

Collection-based — the set is a value

forall x in xs. x > 0
exists u in users. u.is_admin()

Read: "every element of xs is positive", "there is an admin in users".

The collection expression must implement IntoIterator and its item type is inferred.

Combined — explicit type, explicit domain

forall x: Int in 0..100. x * 2 < 200

Useful when the type of the domain is ambiguous (generics, literals, slice ranges).

Guards — where Q(x)

An optional where clause filters the domain:

forall x in items where x.is_valid(). x.score > 0
exists n: Int in 0..1000 where n % 7 == 0. n > 500

Semantically, forall x in S where Q(x). P(x) is ∀ x∈S. Q(x) ⇒ P(x); exists x in S where Q(x). P(x) is ∃ x∈S. Q(x) ∧ P(x).

Multiple binders

Quantifiers take a comma-separated list of bindings:

forall x: Int, y: Int. x + y == y + x

exists i in 0..xs.len(), j in 0..xs.len()
    where i != j. xs[i] == xs[j]     // list has a duplicate

Later binders can reference earlier ones — they are nested left to right:

forall i in 0..n, j in 0..i. a[i] >= a[j]    // sorted array

Equivalent to the explicit nesting forall i. forall j. ....

Where they are allowed

In refinements

Quantifiers on a field's refinement constrain every value:

type SortedList is List<Int>
    where forall i in 0..self.len()-1. (self)[i] <= (self)[i+1];

type UniqueIds is List<Id>
    where forall i in 0..self.len(), j in 0..self.len()
           where i != j. (self)[i] != (self)[j];

Why the parentheses, and why one line

self[i] inside a quantifier body is rejected — unexpected operator '==' — while self[0] == 1 in a refinement without a quantifier, and xs[i] for a parameter inside one, both parse. (self)[i] and self.get(i) are the two spellings that work today. And the binder list has to stay on one line: forall i in …, with j in … on the next is refused.

A quantified refinement on a TYPE does not parse yet

The quantifier is fine and the where is fine — it is the pair, in type position, that the parser does not take:

type C is Int where value > 0;                        parses
fn f(..) where ensures (forall i in 0..3. xs[i] > 0)  parses
type D is List<Int> where forall i in 0..3. self[i] > 0;
  -> error<E018>: Parse error: unexpected operator `>`,
                  expected operator `=>`

grammar/verum.ebnf allows it — value_where_clause = 'where', ['value'], refinement_expr and refinement_expr = expression, and a quantifier is an expression. So the grammar and this page agree, and the parser is the one out of step.

Until it catches up, write the quantified form in requires / ensures on the functions that build or consume the value — the section below — which does parse and is checked.

In requires / ensures

Function pre- and post-conditions:

fn dedup<T: Eq>(xs: &List<T>) -> List<T>
    where ensures forall x in result.
                    (xs.contains(x)) &&
                    count(result, x) == 1
{
    ...
}

In @verify

SMT-backed spec checks:

@verify(formal)
fn all_positive(xs: &List<Int>) -> Bool
    where ensures result == (forall x in xs. x > 0)
{
    xs.iter().all(|x| x > 0)
}

In theorems and lemmas

The proof DSL uses them routinely — see proof-dsl:

theorem sum_nonneg(xs: &List<Int>)
    requires forall x in xs. x >= 0
    ensures  xs.sum() >= 0
{
    proof by induction xs
}

Patterns as binders

The binder is a pattern, not just an identifier, so you can destructure:

forall (k, v) in map. v > 0
forall Entry { id, priority } in queue. priority >= 0

This works because the quantifier binding clause uses the pattern production of the grammar.

The . separator

A quantifier's body is introduced by . (a literal dot). It is always required — it keeps parsing unambiguous between the binder list and the body:

forall x: Int. x * 2 == x + x        // ok
forall x: Int x * 2 == x + x         // parse error — need `.`

Semantics and termination

Quantifiers are pure logic: they have no runtime execution model. Verum does not attempt to evaluate them — it checks them.

• Over a finite collection (the in form), an SMT solver will typically unfold the quantifier into a conjunction or disjunction.
• Over an infinite type (e.g. Int), the verifier relies on the SMT theory (QF_LIA, QF_NIA, QF_LRA, arrays, etc.) to discharge the goal.

If the SMT router gives up, consider switching to @verify(thorough) (parallel portfolio) or writing an explicit proof via proof-dsl.

Writing quantifiers that the SMT solver can solve

A few rules of thumb:

1. Prefer bounded domains. forall i in 0..n. ... is almost always easier than forall i: Int. 0 <= i < n => ....
2. Unfold nested quantifiers. forall i. exists j. P is harder than exists j. forall i. P when the choice is independent of i. Reorder if the math allows.
3. Use refinement types to elide quantifiers. A type like List<Int> { forall x in self. x > 0 } pushes the quantifier to the type boundary, letting every callsite drop the precondition.
4. Avoid exists in postconditions. An ensures with exists is a skolemisation — the solver must produce a witness. Provide one when possible.

Notation cheatsheet

∀ / ∃ form	Verum syntax
∀x: T. P(x)	forall x: T. P(x)
∃x: T. P(x)	exists x: T. P(x)
∀x ∈ S. P(x)	forall x in S. P(x)
∃x ∈ S. P(x)	exists x in S. P(x)
∀x ∈ S. Q(x) ⇒ P(x)	forall x in S where Q(x). P(x)
∃x ∈ S. Q(x) ∧ P(x)	exists x in S where Q(x). P(x)
∀x y. P(x, y)	forall x, y. P(x, y)
∀i. ∀j. 0 ≤ j < i < n ⇒ …	forall i in 0..n, j in 0..i. ...

See also

• Refinement Types.
• Proof DSL — theorems, tactics.
• Dependent Types — Π/Σ.
• verification/smt-routing.