5.4. Invoke on🔗

An invokeOn clause on a procedure specifies a pattern over the procedure's inputs. When the pattern matches any known facts in the proof context, the procedure is automatically invoked. This reduces the need for manually calling lemma procedures for verification purposes.

procedure PAndQ(x: int)
  invokeOn P(x)
  opaque
  ensures P(x) && Q(x);

Whenever P(x) is a known fact, the procedure PAndQ is automatically invoked, making its postcondition P(x) && Q(x) available without an explicit call. An obligation that mentions only Q(x) does not match the pattern, so the procedure stays dormant and its postcondition is not made available.

Note that preconditions act as an antecedent, not as a runtime check: if the preconditions are not provable at the match site, the postcondition simply remains unavailable rather than causing a failure. Additionally, the fact is program-wide — once a term matches the pattern anywhere, the postcondition is available to every proof obligation in the program, not just to a particular caller or region. Finer-grained scoping (e.g. per-caller or per-module) is planned as future work.