Skip to main content

Quantifier Patterns

Common quantifier idioms for real-world verification scenarios.

This page collects patterns that go beyond basic syntax. For fundamentals, see forall, exists, and triggers.

Actor Invariants with Quantifiers​

Use quantified actor invariants to express properties that must hold for all elements of a collection across all public method calls:

quantifier-pattern-actor-inv.sr9
// Actor invariant with quantified property
persistent actor {
  var balances : [var Nat] = [var 10, 20, 30];

  // All balances are non-negative
  invariant forall<Nat>(pure func (i : Nat) : Bool =
    i < balances.size() ==> balances[i] >= 0);

  public func deposit(account : Nat, amount : Nat) : async ()
    modifies balances
    entry_requires account < balances.size();
    requires account < balances.size();
    ensures balances[account] == old(balances[account]) + amount;
  {
    balances[account] := balances[account] + amount;
  };
}

The invariant forall<Nat>(pure func (i : Nat) : Bool = i < balances.size() ==> balances[i] >= 0) is:

  • Assumed at the start of every public method
  • Proven at the end of every public method
  • Re-established after any await boundary

This pattern works well for:

  • Array bounds and value constraints
  • Collection membership properties
  • Consistency between related fields

For the lifecycle of actor invariants around calls and commit points, see actor invariant preservation and async interference.

Loop Invariants with Quantifiers​

When processing arrays in loops, quantified invariants often partition the array into "processed" and "unprocessed" regions:

quantifier-pattern-loop-inv.sr9
// Loop invariant with quantified property
persistent actor {
  var data : [var Nat] = [var 1, 2, 3, 4, 5];

  public func doubleAll() : async ()
    reads data
    modifies data
    ensures forall<Nat>(pure func (i : Nat) : Bool =
      i < data.size() ==> data[i] == old(data[i]) * 2);
  {
    var idx : Nat = 0;
    while (idx < data.size()) {
      loop:invariant idx <= data.size();
      // Elements before idx have been doubled
      loop:invariant forall<Nat>(pure func (j : Nat) : Bool =
        j < idx ==> data[j] == old(data[j]) * 2);
      // Elements at or after idx are unchanged
      loop:invariant forall<Nat>(pure func (j : Nat) : Bool =
        (j >= idx and j < data.size()) ==> data[j] == old(data[j]));
      data[idx] := data[idx] * 2;
      idx := idx + 1;
    };
  };
}

The pattern uses two invariants:

  1. Processed region: j < idx ==> data[j] == old(data[j]) * 2 - elements before the index have been transformed
  2. Unprocessed region: (j >= idx and j < data.size()) ==> data[j] == old(data[j]) - elements at or after the index are unchanged

This partitioning technique is essential for proving postconditions about loops that modify arrays. It builds on the same induction rule described in loop invariant discovery. If the loop body reads or writes actor fields, keep the reads and modifies footprint in sync with the quantified postcondition.

Sorted Array Pattern​

Express "array is sorted" using nested quantifiers:

quantifier-pattern-sorted.sr9
// Sorted array invariant pattern
persistent actor {
  var items : [var Int] = [var 1, 3, 5, 7];

  // Express "array is sorted" with quantified invariant
  invariant forall<Nat>(pure func (i : Nat) : Bool =
    forall<Nat>(pure func (j : Nat) : Bool =
      (i < items.size() and j < items.size() and i < j)
        ==> items[i] <= items[j]));

  public func getFirst() : async Int reads items {
    items[0]
  };
}

The pattern (i < j) ==> items[i] <= items[j] captures the sorted property: for any two in-bounds indices where the first is smaller, the element at the first index is less than or equal to the element at the second.

Uniqueness Pattern​

Assert that all elements in an array are distinct:

quantifier-pattern-unique.sr9
// Uniqueness pattern: all elements are distinct
persistent actor {
  public func checkUnique() : async () {
    ghost {
      let arr : [Int] = [1, 2, 3, 4, 5];
      let n = arr.size();

      // Assert all elements are unique
      assert forall<Nat>(pure func (i : Nat) : Bool =
        forall<Nat>(pure func (j : Nat) : Bool =
          (i < n and j < n and i != j) ==> arr[i] != arr[j]));
    };
  };
}

The pattern (i != j) ==> arr[i] != arr[j] ensures no two different in-bounds positions contain the same value.

Range Pattern​

Constrain all elements to fall within bounds:

quantifier-pattern-range.sr9
// Range pattern: all values within bounds
persistent actor {
  var temperatures : [var Int] = [var 20, 22, 19, 25];

  // All temperatures between 0 and 100
  invariant forall<Nat>(pure func (i : Nat) : Bool =
    i < temperatures.size() ==> (temperatures[i] >= 0 and temperatures[i] <= 100));

  public func setTemp(idx : Nat, value : Int) : async ()
    modifies temperatures
    entry_requires idx < temperatures.size();
    entry_requires value >= 0 and value <= 100;
    requires idx < temperatures.size();
    requires value >= 0 and value <= 100;
  {
    temperatures[idx] := value;
  };
}

This pattern combines the universal quantifier with conjunction to express multiple constraints on each element.

State Comparison with old()​

Use old() inside quantifiers to express relationships between pre-state and post-state:

quantifier-pattern-old.sr9
// Using old() with quantifiers for state comparison
persistent actor {
  var values : [var Int] = [var 10, 20, 30];

  // Prove that increment preserves relative order
  public func incrementAll() : async ()
    reads values
    modifies values
    ensures forall<Nat>(pure func (i : Nat) : Bool =
      i < values.size() ==> values[i] == old(values[i]) + 1);
    // Relative order is preserved
    ensures forall<Nat>(pure func (i : Nat) : Bool =
      forall<Nat>(pure func (j : Nat) : Bool =
        (i < values.size() and j < values.size() and i < j
         and old(values[i]) < old(values[j]))
          ==> values[i] < values[j]));
  {
    var idx : Nat = 0;
    while (idx < values.size()) {
      loop:invariant idx <= values.size();
      loop:invariant forall<Nat>(pure func (k : Nat) : Bool =
        k < idx ==> values[k] == old(values[k]) + 1);
      loop:invariant forall<Nat>(pure func (k : Nat) : Bool =
        (k >= idx and k < values.size()) ==> values[k] == old(values[k]));
      values[idx] := values[idx] + 1;
      idx := idx + 1;
    };
  };
}

The postcondition values[i] == old(values[i]) + 1 expresses that each element increased by exactly one. The second postcondition proves that relative ordering is preserved.

Map Domain Patterns​

When working with maps, quantify over the domain using Set.contains:

ghost {
  let m : Map<Nat, Int> = Map.update(Map.empty(), 1, 10);
  let dom = Map.domain(m);

  // All keys in the domain are actually in the map
  assert forall<Nat>(pure func (k : Nat) : Bool =
    Set.contains(k, dom) ==> Map.contains(k, m));

  // All values in the map are positive
  assert forall<Nat>(pure func (k : Nat) : Bool =
    Map.contains(k, m) ==> Map.get(m, k) > 0);
}

Use Map.domain() to obtain a set of keys, then quantify over membership in that set. If a property only applies to present keys, guard it with Map.contains(k, m) before calling Map.get(m, k).

Existence with Witnesses​

When using exists, provide concrete witnesses when possible:

ghost {
  let arr : [Int] = [1, 2, 3, 4, 5];
  let target : Int = 3;

  // Good: witness is available in scope
  assert exists<Nat>(pure func (i : Nat) : Bool =
    (i < arr.size()) and (arr[i] == target));
}

The SMT solver performs better when it can find the witness from context rather than searching. For runtime search algorithms, use executable code and specify the result with exists; do not expect exists itself to compute a value.

Combining forall and exists​

Express "for every element, there exists a related element":

exists-forall.sr9
// Combine forall and exists: every number has a successor
persistent actor {
  public func check() : async () {
    ghost {
      assert forall<Nat>(pure func (i : Nat) : Bool =
        exists<Nat>(pure func (j : Nat) : Bool = j == i + 1));
    };
  };
}

Order matters:

  • forall ... exists: "for all x, there is some y" (each x may have a different y)
  • exists ... forall: "there is some y that works for all x" (one y must work everywhere)

Anti-Patterns​

Avoid forcing the solver to search infinite spaces:

// Provide a concrete witness
let w : Nat = 1009;  // Known prime > 1000
assert exists<Nat>(pure func (n : Nat) : Bool = n == w);

Missing Bounds​

Always guard array access with bounds checks:

// Guard with bounds check
assert forall<Nat>(pure func (i : Nat) : Bool =
  i < arr.size() ==> arr[i] >= 0);

Deep Nesting​

Excessive nesting causes exponential solver complexity:

// Factor into helper predicates or limit nesting depth
pure func pairProperty(i : Nat, j : Nat) : Bool {
  // Property for one pair
  i + j == j + i
};

assert forall<Nat>(pure func (i : Nat) : Bool =
  forall<Nat>(pure func (j : Nat) : Bool = pairProperty(i, j)));

Pattern Selection Guide​

GoalPattern
All elements satisfy propertyforall<Nat>(pure func (i : Nat) : Bool = i < size ==> property(arr[i]))
Some element satisfies propertyexists<Nat>(pure func (i : Nat) : Bool = (i < size) and property(arr[i]))
No element satisfies propertynot exists<Nat>(pure func (i : Nat) : Bool = (i < size) and property(arr[i]))
Array is sortedforall<Nat>(pure func (i : Nat) : Bool = forall<Nat>(pure func (j : Nat) : Bool = i < j ==> arr[i] <= arr[j]))
All elements uniqueforall<Nat>(pure func (i : Nat) : Bool = forall<Nat>(pure func (j : Nat) : Bool = i != j ==> arr[i] != arr[j]))
All values in rangeforall<Nat>(pure func (i : Nat) : Bool = i < size ==> (lo <= arr[i] and arr[i] <= hi))
Preservation across updateforall<Nat>(pure func (i : Nat) : Bool = i < size ==> arr[i] == old(arr[i]) + delta)
Map keys unchanged except oneforall<K>(pure func (k : K) : Bool = k != target ==> Map.getOr(m, k, d) == Map.getOr(old(m), k, d))
Set membership preservedforall<T>(pure func (x : T) : Bool = Set.contains(x, old(s)) ==> Set.contains(x, s))

Summary​

  • Use quantified actor invariants for properties that must hold across all methods
  • Partition arrays in loop invariants: processed vs unprocessed regions
  • Express sorted/unique/range constraints with nested or guarded quantifiers
  • Combine old() with quantifiers for state transition properties
  • Avoid unbounded search, missing bounds guards, and deep nesting
  • Provide concrete witnesses for existential claims when possible