Triggers

Triggers guide the SMT solver when instantiating quantified formulas. Use forallWith to provide explicit triggers when automatic inference is insufficient or causes performance issues.

What Are Triggers?

When the verifier encounters a forall expression, the underlying SMT solver must decide when to instantiate the quantified variable with concrete values. Triggers are patterns that tell the solver: "whenever you see this expression in the proof context, instantiate the quantifier."

Without good triggers, the solver may:

• Never instantiate the quantifier (missing proofs)
• Instantiate too many times (timeouts)
• Choose suboptimal instantiation points (slow verification)

Automatic vs Explicit Triggers

The forall function uses automatic trigger inference:

trigger-auto-inference.sr9

// Automatic trigger inference with forall
persistent actor {
  public func check() : async () {
    ghost {
      let data : [Bool] = [true, true];

      // forall automatically infers data[i] as trigger
      assert forall<Nat>(pure func (i : Nat) : Bool =
        i < data.size() ==> data[i] == data[i]);
    };
  };
}

The verifier automatically selects data[i] as the trigger. This works well for simple cases.

For complex properties or when inference fails, use forallWith with explicit triggers:

forall-trigger.sr9

// Use forallWith for explicit trigger control
persistent actor {
  public func check() : async () {
    ghost {
      let data : [Bool] = [true, true, true];

      // Explicit trigger: data[i] guides instantiation
      assert forallWith<Nat>(
        pure func (i : Nat) : Bool = i < data.size() ==> data[i] == data[i],
        [pure func (i : Nat) : Bool = data[i]]
      );
    };
  };
}

forallWith Syntax

forallWith<T>(
  pure func (x : T) : Bool = property,
  [pure func (x : T) : Bool = trigger_expression, ...]
)

The second argument is an array of trigger functions. Each function must:

• Have the same parameter type as the quantifier
• Produce a trigger term whose value is ignored
• Contain a "call-like" expression that mentions the bound variable

The trigger function bodies are pure verifier terms. They are checked for the same pure-context restrictions as quantified predicates.

Valid Trigger Expressions

Triggers must be "call-like" expressions. Valid triggers include:

Expression Type	Example
Array access	arr[i]
Function call	f(x)
Field access	record.field
Predicate application	Set.contains(x, s)
Map lookup	Map.contains(k, m)
Sequence index	Seq.get(seq, i)

Invalid Trigger Expressions

Comparison and arithmetic operators are not valid triggers:

trigger-invalid_reject.sr9

// REJECTED: Comparison operators are not valid triggers
persistent actor {
  public func check() : async () {
    ghost {
      // k > 0 is a comparison, not call-like
      assert forallWith<Nat>(
        pure func (k : Nat) : Bool = k >= 0,
        [pure func (k : Nat) : Bool = k > 0]  // Invalid trigger
      );
    };
  };
}

This fails with error: forallWith trigger must be call-like.

Invalid trigger expressions include:

Expression Type	Example	Why Invalid
Comparison	x > 0, x == y	Not call-like
Arithmetic	x + 1, x * 2	Not call-like
Logical operators	a and b, a or b	Not call-like
Literals	42, true	No bound variable

Multiple Triggers

When a property involves multiple collections or expressions, provide multiple triggers:

trigger-multi.sr9

// Multiple triggers for properties spanning multiple arrays
persistent actor {
  public func check() : async () {
    ghost {
      let a : [Bool] = [true, true];
      let b : [Bool] = [true, true];

      // Two triggers: a[i] and b[i]
      // Either trigger can cause instantiation
      assert forallWith<Nat>(
        pure func (i : Nat) : Bool =
          (i < a.size() and i < b.size()) ==> (a[i] == a[i] and b[i] == b[i]),
        [
          pure func (i : Nat) : Bool = a[i],
          pure func (i : Nat) : Bool = b[i]
        ]
      );
    };
  };
}

For a single-binder quantifier, each explicit trigger is emitted as its own trigger pattern, so any one of them can cause instantiation. For multi-binder quantifiers, the selected trigger terms are emitted as one trigger set so the solver has enough information to bind all variables together.

Triggers with Collections

Use explicit triggers when working with Map and Set operations:

trigger-map-set.sr9

// Triggers with Map and Set operations
persistent actor {
  public func check() : async () {
    ghost {
      let m : Map<Nat, Int> = Map.update(Map.empty(), 1, 10);
      let dom = Map.domain(m);

      // Explicit triggers on collection operations
      assert forallWith<Nat>(
        pure func (k : Nat) : Bool = Set.contains(k, dom) ==> Map.contains(k, m),
        [
          pure func (k : Nat) : Bool = Map.contains(k, m),
          pure func (k : Nat) : Bool = Set.contains(k, dom)
        ]
      );
    };
  };
}

Collection operations like Map.contains and Set.contains make effective triggers because they are call-like and frequently appear in proof contexts.

Binder Coverage

Triggers must mention all bound variables. For multi-parameter quantifiers, the union of trigger expressions must cover every binder:

// Two binders: i and j
forallWith<Nat>(
  pure func (i : Nat) : Bool = forallWith<Nat>(
    pure func (j : Nat) : Bool = property(i, j),
    [pure func (j : Nat) : Bool = f(i, j)]  // Covers j, outer covers i
  ),
  [pure func (i : Nat) : Bool = g(i)]  // Covers i
)

If triggers do not cover all binders, the verifier appends automatically inferred triggers to complete coverage when it can find them. If the combined set still cannot cover the binders with call-like terms, the proof has no useful instantiation pattern and usually needs a simpler predicate or explicit triggers.

Trigger Inference Details

When you use forall without explicit triggers, the verifier:

1. Collects all "call-like" subexpressions from the quantifier body
2. Filters to expressions that mention bound variables
3. Ranks candidates by type (array locations preferred over generic calls)
4. Selects up to 2 trigger terms for single-binder quantifiers
5. For multi-binder quantifiers, uses greedy set cover to select up to 3 trigger terms that cover the binders

Priority order for trigger selection:

1. Mutable record array element references
2. Address-based references
3. Array location expressions
4. Snapshot reads
5. Generic call-like expressions

When to Use Explicit Triggers

Use forallWith when:

• Verification times out - Automatic inference may select too many triggers
• Proof fails unexpectedly - The inferred trigger may not match proof context
• Properties span multiple arrays - Explicit triggers clarify instantiation points
• Working with custom predicates - Ensure your predicate appears as trigger

Common Patterns

Array Bounds with Explicit Trigger

forallWith<Nat>(
  pure func (i : Nat) : Bool = i < arr.size() ==> arr[i] >= 0,
  [pure func (i : Nat) : Bool = arr[i]]
)

Two-Array Correspondence

forallWith<Nat>(
  pure func (i : Nat) : Bool = i < a.size() ==> a[i] == b[i],
  [
    pure func (i : Nat) : Bool = a[i],
    pure func (i : Nat) : Bool = b[i]
  ]
)

Map Domain Membership

forallWith<Nat>(
  pure func (k : Nat) : Bool = Map.contains(k, m) ==> Map.get(m, k) > 0,
  [pure func (k : Nat) : Bool = Map.contains(k, m)]
)

No existsWith

There is no existsWith function. Existential quantifiers use automatic trigger inference. If you need explicit trigger control for existence proofs, use the equivalence:

// Instead of hypothetical existsWith:
not forallWith<T>(
  pure func (x : T) : Bool = not property(x),
  [pure func (x : T) : Bool = trigger(x)]
)

// Equivalent to:
exists<T>(pure func (x : T) : Bool = property(x))

Performance Tips

• Keep triggers simple - Complex triggers cause over-instantiation
• Prefer array accesses - arr[i] is usually the best trigger for array properties
• Avoid nested triggers - Deeply nested quantifiers with many triggers cause exponential blowup
• Use one trigger when sufficient - More triggers means more instantiation opportunities
• Match proof context - Triggers should match expressions that appear during verification
• Prefer stable domain terms - For map/set facts, membership predicates like Map.contains(k, m) and Set.contains(k, s) are usually better triggers than value arithmetic

Summary

• Triggers guide SMT solver instantiation for quantifiers
• Use forall for automatic trigger inference in simple cases
• Use forallWith with explicit triggers when inference fails or causes timeouts
• Triggers must be "call-like": array accesses, function calls, or field accesses
• Comparison operators (<, >=, ==) are not valid triggers
• Multiple triggers can be provided; the union must cover all bound variables
• There is no existsWith; use automatic inference or negated forallWith

Related Topics

• Quantifier patterns for examples that need trigger-friendly predicates
• Performance: triggers for diagnosing slow or unstable quantifier proofs
• Spec collections for Map, Set, Seq, and Multiset operations that make useful trigger terms
• Universal quantifiers for forallWith syntax in context