Skip to main content

Universal Quantification (forall)

The forall function expresses that a property holds for all values of a type. It is a verification construct: use it in contracts, ghost code, invariants, assertions, and lemmas, not as runtime control flow.

Syntax​

forall<T>(pure func (x : T) : Bool = property)

The argument is a pure func literal that takes a bound variable and returns a boolean expression. The quantifier asserts that this expression is true for every possible value of type T. The function literal is lowered to a verifier quantifier; it is not an ordinary first-class function value.

Basic Usage​

Use forall in ghost blocks and contracts to express universal properties:

forall-basic.sr9
// Prove that addition is commutative for all natural numbers
persistent actor {
  public func check() : async () {
    ghost {
      assert forall<Nat>(pure func (i : Nat) : Bool =
        forall<Nat>(pure func (j : Nat) : Bool =
          i + j == j + i));
    };
  };
}

The verifier proves the quantified assertion in the current proof context. Arithmetic facts like this are usually handled by the backend arithmetic theory; collection and array facts often need guards, triggers, or helper lemmas.

Array Bounds Pattern​

The most common use of forall is expressing properties over array indices. Use implication (==>) to guard the property with bounds:

forall-array.sr9
// Prove all array elements are positive
persistent actor {
  public func check() : async () {
    ghost {
      let arr : [Nat] = [1, 2, 3, 4, 5];
      let n : Nat = arr.size();

      // Guard property with bounds check
      assert forall<Nat>(pure func (i : Nat) : Bool =
        (i < n) ==> (arr[i] >= 1));
    };
  };
}

The pattern i < arr.size() ==> property(arr[i]) ensures the property only applies to valid indices. This is the same guard shape you use in loop invariants when proving that each processed element of an array was updated correctly.

Nested Quantifiers​

You can nest forall to quantify over multiple variables:

forall-nested.sr9
// Prove associativity with three bound variables
persistent actor {
  public func check() : async () {
    ghost {
      assert forall<Nat>(pure func (a : Nat) : Bool =
        forall<Nat>(pure func (b : Nat) : Bool =
          forall<Nat>(pure func (c : Nat) : Bool =
            (a + b) + c == a + (b + c))));
    };
  };
}

Each nested quantifier introduces a new bound variable with its own scope.

Using forall in Contracts​

Quantifiers work in requires and ensures clauses:

forall-contract.sr9
// Use forall in preconditions and postconditions
persistent actor {
  var data : [var Nat] = [var 1, 2, 3];

  // Require all elements positive, ensure they stay positive
  public func increment() : async ()
    reads data
    modifies data
    requires forall<Nat>(pure func (i : Nat) : Bool =
      i < data.size() ==> data[i] > 0);
    ensures forall<Nat>(pure func (i : Nat) : Bool =
      i < data.size() ==> data[i] > 0);
  {
    var idx : Nat = 0;
    while (idx < data.size()) {
      loop:invariant idx <= data.size();
      loop:invariant forall<Nat>(pure func (j : Nat) : Bool =
        j < data.size() ==> data[j] > 0);
      data[idx] := data[idx] + 1;
      idx := idx + 1;
    };
  };
}

Collections​

Use forall with spec collections to express membership properties:

forall-set.sr9
// Quantify over set membership
persistent actor {
  public func check() : async () {
    ghost {
      let s : Set<Nat> = Set.singleton(1);

      // All elements in the set are non-negative
      assert forall<Nat>(pure func (k : Nat) : Bool =
        Set.contains(k, s) ==> k >= 0);
    };
  };
}

The same pattern works with Map.contains, Set.contains, and sequence index properties from Seq.

Explicit Triggers with forallWith​

When automatic trigger inference fails or causes performance issues, use forallWith to provide explicit triggers:

forallWith<T>(
  pure func (x : T) : Bool = property,
  [pure func (x : T) : Bool = trigger_expression]
)
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]]
      );
    };
  };
}

Triggers must be "call-like" expressions: function calls, array accesses, field accesses, sequence indexing, or predicate applications. Comparison operators (<, >=, ==) are not valid triggers. See Triggers for the full selection rules.

Domain Constraints​

When you quantify over Nat types, the verifier automatically adds x >= 0 constraints. This transformation happens internally:

// You write:
forall<Nat>(pure func (i : Nat) : Bool = property(i))

// Verifier generates:
forall i : Int :: (i >= 0) ==> property(i)

This preserves Sector9's Motoko-derived semantics where Nat values are non-negative.

Common Mistakes​

Missing Bounds Guard​

// CORRECT: Bounds guard limits property to valid indices
persistent actor {
  public func check() : async () {
    ghost {
      let arr : [Nat] = [1, 2, 3];

      // Only prove for indices within bounds
      assert forall<Nat>(pure func (i : Nat) : Bool =
        i < arr.size() ==> arr[i] >= 1);
    };
  };
}

Without the bounds guard, the quantifier tries to prove the property for all natural numbers, including indices beyond the array size.

Invalid Trigger Expression​

Triggers must be call-like. Comparison expressions are rejected:

// REJECTED: k > 0 is a comparison, not call-like
forallWith<Nat>(
  pure func (k : Nat) : Bool = k >= 0,
  [pure func (k : Nat) : Bool = k > 0]
)

Use function calls or array accesses as triggers instead.

Performance Considerations​

Quantifiers can cause SMT solver timeouts if not used carefully:

  • Minimize nesting depth - Deeply nested quantifiers increase solver complexity exponentially
  • Use explicit triggers - When automatic inference produces too many triggers, use forallWith
  • Keep trigger expressions simple - Triggers guide solver instantiation; complex triggers cause over-instantiation
  • Prefer bounded quantification - i < n ==> property(i) is more efficient than unbounded quantification
  • Factor reusable facts into lemmas - If several methods repeat the same quantified argument, state it once as a lemma

Summary​

  • forall<T>(pure func (x : T) : Bool = ...) asserts a property holds for all values
  • Use implication (==>) to guard properties with bounds or membership tests
  • Nest forall for multiple bound variables
  • Use forallWith when you need explicit trigger control
  • Triggers must be call-like: function calls, array reads, or field accesses
  • Domain constraints for Nat types are added automatically