Skip to main content

Existential Quantification (exists)

The exists function expresses that at least one value of a type satisfies a property. It is a verification construct for contracts, ghost code, assertions, invariants, and lemmas, not a runtime search operation.

Syntax​

exists<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 there exists some value of type T for which this expression is true. The function literal is lowered to a verifier quantifier; it is not an ordinary first-class function value.

Basic Usage​

Use exists in ghost blocks and contracts to assert that a value with certain properties exists:

exists-basic.sr9
// Assert that a specific value exists
persistent actor {
  public func check() : async () {
    ghost {
      let target : Nat = 42;
      assert exists<Nat>(pure func (n : Nat) : Bool = n == target);
    };
  };
}

The verifier proves that a natural number equal to 42 exists.

Array Search Pattern​

A common use of exists is asserting that an array contains an element with a certain property:

exists-array.sr9
// Assert that at least one positive element exists
persistent actor {
  public func check() : async () {
    let _arr : [var Int] = [var -5, 10, -3];
    ghost {
      let n = _arr.size();
      assert exists<Nat>(pure func (i : Nat) : Bool =
        (i < n) and (_arr[i] > 0));
    };
  };
}

The pattern (i < n) and property(arr[i]) uses conjunction (and) to combine the bounds check with the property. This differs from forall, which uses implication (==>).

Nested Quantifiers​

You can nest exists to quantify over multiple values:

exists-nested.sr9
// Assert that two values exist satisfying a property
persistent actor {
  public func check() : async () {
    ghost {
      let sum : Nat = 10;
      assert exists<Nat>(pure func (i : Nat) : Bool =
        exists<Nat>(pure func (j : Nat) : Bool =
          (i == 2) and (j == 8) and (i + j == sum)));
    };
  };
}

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

Using exists in Contracts​

Quantifiers work in ensures clauses to express postconditions:

exists-contract.sr9
// Use exists in postcondition
persistent actor {
  ghost var g : Nat = 0;

  public func increment() : async () modifies g
    ensures exists<Nat>(pure func (k : Nat) : Bool = k == old(g));
  {
    ghost { g := g + 1 };
  };
}

The postcondition states that there exists some value equal to the old value of g.

Combining forall and exists​

You can combine universal and existential quantifiers to express complex properties:

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));
    };
  };
}

This asserts that for every natural number, there exists a successor. The nesting order matters: forall ... exists means "for all x, there is some y" while exists ... forall means "there is some y that works for all x".

Collections​

Use exists with spec collections to express membership:

exists-map.sr9
// Use exists with Map containment
persistent actor {
  public func check() : async () {
    ghost {
      let m : Map<Nat, Int> = Map.update(Map.empty(), 1, 10);
      let key : Nat = 1;
      assert Map.contains(key, m);
      assert exists<Nat>(pure func (k : Nat) : Bool =
        (k == key) and Map.contains(k, m));
    };
  };
}

The same pattern works with Set.contains and sequence membership or index properties from Seq.

Negation Pattern​

Use not exists to assert that no value satisfies a property:

exists-negation.sr9
// Use not exists to assert no element satisfies a property
persistent actor {
  public func check() : async () {
    let _arr : [var Int] = [var 1, 2, 3];
    ghost {
      let n = _arr.size();
      assert not exists<Nat>(pure func (i : Nat) : Bool =
        (i < n) and (_arr[i] == 1000));
    };
  };
}

This is logically equivalent to forall<Nat>(pure func (i : Nat) : Bool = (i < n) ==> arr[i] != 1000), but the negated exists form often reads more naturally.

Domain Constraints​

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

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

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

Note that for exists, domain constraints are combined with conjunction (&&), not implication. This ensures the verifier only considers values that satisfy Sector9's Motoko-derived Nat semantics.

Witness Requirements​

exists requires the verifier to find or infer a witness. The SMT solver performs best when:

  • A concrete witness value is available in scope
  • The property uniquely determines the witness
  • The quantified domain is bounded by a guard such as i < arr.size()
// Assert that a specific value exists
persistent actor {
  public func check() : async () {
    ghost {
      let target : Nat = 42;
      assert exists<Nat>(pure func (n : Nat) : Bool = n == target);
    };
  };
}

The first example may fail because the solver has no concrete witness. The second succeeds because target provides a known value.

No existsWith​

Unlike forall, which has a forallWith variant for explicit triggers, there is no existsWith function. Automatic trigger inference handles exists expressions. If you need fine-grained control, refactor to use forall with negation:

// Instead of hypothetical existsWith:
not forall<T>(pure func (x : T) : Bool = not property(x))

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

Common Mistakes​

Disjunctions in Witnesses​

SMT solvers struggle with disjunctions inside existential quantifiers:

// May fail even though witnesses exist
assert exists<Nat>(pure func (n : Nat) : Bool = (n == 3) or (n == 7));

The solver cannot easily prove such assertions because it must commit to one disjunct. Prefer using concrete witnesses or split into separate assertions.

Avoid assertions that require the solver to search an infinite space without guidance:

// May timeout or fail
assert exists<Nat>(pure func (n : Nat) : Bool = isPrime(n) and n > 1000);

Provide hints by introducing named witnesses or bounding the search space.

Performance Considerations​

Existential quantifiers present unique challenges for SMT solvers:

  • Provide witnesses when possible - Assertions with concrete values in scope verify faster
  • Bound quantification - Use (i < n) and property rather than unbounded properties
  • Avoid complex nested quantifiers - forall ... exists combinations can cause timeouts
  • Prefer negated forall for absence when needed - Sometimes not forall ... not is more efficient than not exists, especially when you already have a good universal trigger

Summary​

  • exists<T>(pure func (x : T) : Bool = ...) asserts at least one value satisfies the property
  • Use conjunction (and) to combine bounds with properties, unlike forall which uses implication
  • Nest exists for multiple bound variables
  • Combine with forall for complex properties; order determines meaning
  • Use not exists to assert no value satisfies a property
  • Domain constraints for Nat types use conjunction, not implication
  • There is no existsWith; use automatic triggers or refactor to negated forall
  • Provide concrete witnesses when possible for reliable verification