Trigger Management

Triggers guide when the SMT solver instantiates quantified variables. Poor trigger choices cause verification to time out or fail to prove valid properties. This page covers how to diagnose and fix trigger-related performance issues.

Why Triggers Matter for Performance

Quantifiers like forall and exists create proof obligations that the solver must instantiate. A trigger is a pattern that tells the solver when to apply the quantifier. Without good triggers, three problems occur:

Problem	Symptom	Cause
Never instantiates	Proof fails unexpectedly	Trigger too restrictive, doesn't appear in proof
Over-instantiates	Verification times out	Trigger too general, matches everywhere
Wrong instantiation	Slow verification	Trigger matches irrelevant terms

Diagnosing Trigger Problems

Symptoms of Bad Triggers

Timeout with quantifiers: If verification times out and the code contains forall or exists, triggers are the first suspect.

XDG_CACHE_HOME=/tmp/sector9 ./bin/sector9 --verify --verify-timeout-ms 60000 myfile.mo
# Times out after 60 seconds

Silent proof failure: A property you expect to hold fails without a clear counterexample. The quantifier was never instantiated.

Inspecting Generated Triggers

Use --viper to see what triggers Sector9 generates:

XDG_CACHE_HOME=/tmp/sector9 ./bin/sector9 --viper --deterministic myfile.mo > output.vpr

In the Viper output, triggers appear in braces:

forall i: Int :: {($loc(data, i)).$array$bool}
  ((i >= 0) ==> ((i < $size(data)) ==> ...))
              ^^^^^^^^^^^^^^^^^^^^^^^^^
              This is the trigger pattern

If you see multiple triggers or complex expressions, that may explain timeout behavior.

Automatic vs Explicit Triggers

Automatic Inference (forall)

Sector9 automatically infers triggers for plain forall:

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 selects data[i] as the trigger because it's a call-like expression mentioning the bound variable i.

When automatic inference works well:

• Single array access in the body
• Simple properties with one collection
• Clear call-like expressions available

Explicit Triggers (forallWith)

When automatic inference causes problems, use forallWith to specify 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]]
      );
    };
  };
}

Use explicit triggers when:

• Verification times out with forall
• Automatic inference picks poor candidates
• You need precise control over instantiation

Valid Trigger Expressions

Triggers must be call-like expressions. The solver uses these as matching patterns.

Valid	Example	Why
Array access	arr[i]	Index lookup is call-like
Function call	f(x), Map.contains(k, m)	Direct function application
Field access	record.field	Projection is call-like
Collection ops	Set.contains(x, s)	Predicate application

Invalid	Example	Why
Comparison	x > 0, i < n	Not call-like
Arithmetic	x + 1, i * 2	Not call-like
Logical ops	a and b	Not call-like
Literals	42, true	No bound variable

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: forallWith trigger must be call-like

Multiple Triggers

When a property involves multiple collections, use 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]
        ]
      );
    };
  };
}

Each trigger provides an instantiation opportunity. The solver can apply the quantifier when a matching term appears in the proof context.

Binder coverage rule: The union of all triggers should mention every bound variable. If your triggers don't cover all variables, Sector9 may append inferred triggers, which can make performance less predictable.

Avoiding Common Performance Problems

Problem 1: Matching Loops

A matching loop occurs when instantiating a quantifier creates new terms that match the same trigger, causing infinite instantiation.

// DANGEROUS: triggers on magic(i), but body contains magic(magic(i))
forallWith<Nat>(
  pure func (i : Nat) : Bool = magic(magic(i)) == magic(2 * i) + i,
  [pure func (i : Nat) : Bool = magic(i)]  // Causes matching loop
)

Fix: Choose triggers that don't appear recursively in the body.

Problem 2: Over-Instantiation

Complex or numerous triggers cause the solver to instantiate too many times:

// SLOW: Too many triggers, each causes separate instantiation
forallWith<Nat>(
  pure func (i : Nat) : Bool = arr[i] > 0,
  [
    pure func (i : Nat) : Bool = arr[i],
    pure func (i : Nat) : Bool = arr[i + 1],
    pure func (i : Nat) : Bool = arr[i * 2]  // Many instantiation points
  ]
)

Fix: Use the minimum number of triggers needed. One well-chosen trigger is usually better than many.

Problem 3: Restrictive Triggers

A trigger too specific to appear in the proof context causes silent failure:

// TOO RESTRICTIVE: triple-nested pattern rarely appears
forallWith<Nat>(
  pure func (i : Nat) : Bool = magic(magic(i)) == magic(2 * i),
  [pure func (i : Nat) : Bool = magic(magic(magic(i)))]  // Never matches
)

Fix: Use triggers that match expressions actually appearing in the proof.

Problem 4: Nested Quantifiers

Deeply nested quantifiers multiply instantiation cost exponentially:

// EXPENSIVE: 4 levels of nesting
forall<Nat>(pure func (i : Nat) : Bool =
  forall<Nat>(pure func (j : Nat) : Bool =
    forall<Nat>(pure func (k : Nat) : Bool =
      forall<Nat>(pure func (l : Nat) : Bool =
        someProperty(i, j, k, l)))))

Fix: Limit nesting to 2-3 levels. Refactor properties or use lemmas to break apart deep nesting.

Performance Checklist

1. Prefer array accesses - arr[i] is the most stable trigger pattern
2. Use one trigger when possible - More triggers mean more instantiation attempts
3. Keep triggers simple - Complex expressions increase matching overhead
4. Match proof context - Triggers should be expressions that appear during verification
5. Cover all binders - Ensure every bound variable appears in some trigger
6. Avoid arithmetic in triggers - arr[i+1] creates many potential matches
7. Check generated Viper - Use --viper to inspect actual trigger selection
8. Test with timeout - Run --verify-timeout-ms 30000 to catch slow verification early

When to Use Each Approach

Situation	Recommendation
Simple array bounds	Use forall with automatic inference
Single collection property	Use forall first, switch to forallWith if slow
Multiple collections	Use forallWith with one trigger per collection
Verification times out	Add explicit triggers with forallWith
Complex nested quantifiers	Break into smaller lemmas, use explicit triggers
Map/Set domain properties	Use Map.contains or Set.contains as triggers

See Also

• Quantifiers - Core quantifier syntax
• Triggers - Detailed trigger mechanics
• Timeout Control - Managing verification time

Summary

• Triggers guide SMT solver quantifier instantiation
• Bad triggers cause timeouts or silent proof failures
• Use --viper to inspect generated triggers
• Prefer simple, call-like expressions as triggers
• Use forallWith when automatic inference causes problems
• Keep trigger count minimal and avoid deep nesting