Source-level Z3 :pattern hints for user-written quantifiers

[wirerhino]

Summary

Request: expose SMT-LIB :pattern annotation on user-written \A/\E quantifiers via a TLAPS surface-syntax pragma, so users can guide Z3's MBQI quantifier instantiation on heavily-quantified obligations.

Motivation (empirical, from production HFT verification project)

We maintain ~81 TLA+ specs / 564 invariants / 17 modules, including Raft consensus, matching engine (AMM with curve executors), and lock-tracking proof families. Recent verification campaigns surfaced a recurring SMT cascade pattern on heavily-quantified TypeOK-class obligations:

• ChronosRaftProofs.tla TypeOK QED — 9-fact SMT cascade taking 15-30 minutes cold per backend (Z3 / cvc4 / Spass)
• 26→0 axiom-removal campaign — apex obligations (LeaderElectionLogPrefixOfLog, ClientRequestNoForwardEntry, LogMatchingLocalAxiom) routinely require 6-axis defense-in-depth (TLAPS + Coq + Lean + Why3 + Z3-standalone + Apalache) because Z3's MBQI loops on \A s \in Server: P(s) shapes when Server carries multiple per-element typing facts (currentTerm[s] \in Nat, votedFor[s] \in Server \cup {NULL}, log[s] \in Seq(LogEntry), role[s] \in {Follower, Candidate, Leader}).

Empirically, the structural workarounds we've discovered (per-element typing, drop-SUFFICES-use-ASSUME/PROVE, function-builder per-conjunct case split, lift-typing-facts-as-explicit-sub-step) buy 30-90% wall-clock improvements but require restructuring proofs around what is fundamentally an SMT-instantiation issue. A source-level :pattern hint would let users keep proof structure idiomatic and instead constrain Z3's instantiator directly.

Current state

The internal SMT translator already wires :pattern annotations end-to-end:

• src/expr/e_t.ml:496 — pattern_prop : expr list pfuncs, the property attached to expressions
• src/expr/e_t.ml:499-518 — add_pats / remove_pats / map_pats / fold_pats operators
• src/backend/smt.ml:618-637 — internal add_patterns injects pattern_prop on translator-emitted \A bs : Mem(_, ex) <=> _ shapes for abstracted operators
• src/backend/smtlib.ml:236-250 — pp_print_pat emits (! <expr> :pattern (<pat>)) SMT-LIB output

So the SMT-emitter is fully working — but the only writer is the internal add_patterns site, which fires a hard-coded shape on translator-injected operators. Empirically (verified in our .tlacache/<spec>.tlaps/tlapm_*.smt output), :pattern clauses appear ONLY on built-in TLA+ axioms (smt__TLA____SetExtTrigger, smt__TLA____Mem, smt__TLA____FunIsafcn, etc.) — never on user-defined operators (Server, currentTerm, LogEntry).

Pragma-key parser routes only prover / timeout / tactic (src/backend/prep.ml:1117-1181); any other key raises \"Unknown keyword in proof method definition\" (prep.ml:1182). The grammar (src/expr/e_parser.ml:1132-1134 read_method_arg) accepts arbitrary identifier-keyed args and string_or_float_of_expr-typed values.

Proposed surface syntax

Two compatible options, in order of cleanness:

Option A — pragma-attached BY (preferred, smallest delta)

Pattern(p) == TRUE (*{ by (prover:\"smt3\"; pattern:@) }*)

THEOREM TypeOK
  PROOF
  <1>1. \A s \in Server: currentTerm[s] \in Nat
    BY DEF Init, Next, vars, Pattern(<<currentTerm[s]>>)
  <1>2. ...

The pattern: key takes a structured-expression argument (currently read_method_arg accepts only Bstring/Bfloat/Bdef); needs grammar widening to accept Btuple/Bexpr of patterns.

Option B — pattern-attached label (alternative)

THEOREM \A s \in Server: P(s) /\ Q(s)
  PROOF (*{ pattern: <<P(s)>> }*)
  ...

Requires a new pragma site distinct from method-args (currently pragma is consumed only on operator-defs and BY).

We'd recommend Option A as a strictly additive parser change (read_method_arg extension) + new pragma key in compute_meth (route pattern: <expr> to attach pattern_prop on the surrounding obligation).

Empirical wallclock targets

Based on our tlapsProveChronosRaft campaign (commit 2080dc3f8 ClientRequestNoForwardEntry, 13456 obligations PROVED, 6-axis defense):

• Z3 MBQI cold path on TypeOK: 15-30min observed; target with explicit :pattern (<<currentTerm[s]>>): <2min (4-10× speedup, comparable to documented Z3-pattern speedups in IronFleet/Verus).
• Total Raft module wallclock (tlapsProveChronosRaftProofs): currently ~50min cold; target <15min.
• Apex axiom-removal campaign: 6-axis defense requirement could collapse to TLAPS-alone for ~40% of axioms if MBQI patterns were guidable.

Why this matters for the broader TLA+ community

The IronFleet / Verus / Dafny ecosystems all expose source-level pattern hints precisely because heavily-quantified specifications hit MBQI saturation in practice. TLAPS is currently the only major TLA+/proof-management toolchain that emits SMT-LIB but blocks users from controlling the pattern annotations — even though the internal infrastructure (pattern_prop, pp_print_pat) is fully operational. Adding a source-level frontend would make TLAPS competitive with these systems on quantifier-heavy proofs.

Acceptance criteria suggestion

1. New pragma key pattern: <expr-list> accepted in read_method_arg grammar.
2. compute_meth (prep.ml) routes the new key to attach Smt.pattern_prop on the obligation's quantifier-bound conclusion (mirroring the internal add_patterns mechanism).
3. New stdlib operator in library/TLAPS.tla:
   Pattern(p) == TRUE (*{ by (pattern:@) }*)
4. Documentation example in doc/web/ showing pattern-hint usage on a TypeOK-shaped THEOREM.
5. Round-trip test: cited pattern appears in .tlacache/<spec>.tlaps/tlapm_*.smt :pattern (...) output.
6. No regression on existing test corpus (make test).

We would be happy to contribute a PR if the design direction is acceptable to the maintainers — wanted to validate the approach + namespace choice (pattern: vs trigger: vs qid:) before opening one.

References

• src/expr/e_t.ml:496-518 — pattern_prop infrastructure (already exists)
• src/backend/smt.ml:618-637 — internal add_patterns site (only current writer)
• src/backend/smtlib.ml:236-250 — :pattern SMT-LIB emitter (already wired)
• src/expr/e_parser.ml:1128-1154 — pragma grammar (extension target)
• src/backend/prep.ml:1105-1186 — pragma key consumer / compute_meth (extension target)
• library/TLAPS.tla:39-115 — current pragma surface (one new operator to add)

Empirical context: #261 (LSP proof decomposition, also targets quantifier obligation handling) is adjacent work in the same neighborhood.

[wirerhino]

Update — patch landed in fork, end-to-end empirically validated.

Implemented the proposed Option A design at https://github.com/wirerhino/tlapm/tree/feat/source-pattern-hints (commits be0aed4 + 10d04af). Patch is 111 LOC additive, untouched outside the pattern: arm + pat_hints accumulator + add_pats call site:

• src/backend/prep.ml — new pattern: arm in compute_meth; signature widened to Method.t * Expr.T.expr list; two call sites in find_meth updated; pat_hints accumulator wired through Expr.T.add_pats to attach to obligation conclusion.
• library/TLAPS.tla — Pattern(p) and PatternT(p, X) operators added with documentation.

Empirical validation — PatternSmoke.tla:

THEOREM ASSUME NEW s \in Server, myFn \in [Server -> Nat]
        PROVE  myFn[s] \in Nat
  BY Pattern(<<myFn[s]>>)

Built with patched tlapm, ran with --method z3 --debug tempfiles. Generated tlapm_*.smt2 contains:

(! (smt__TLA____Mem (smt__TLA____FunApp smt__CONSTANT__myFn__ smt__CONSTANT__s__) smt__TLA____NatSet)
   :pattern ((smt__TLA____Tuple__1
               (smt__TLA____FunApp smt__CONSTANT__myFn__ smt__CONSTANT__s__))))
   :named |Goal|))

— the user-supplied pattern <<myFn[s]>> propagates through to the Z3 :pattern annotation on the goal, attached via the existing pp_print_pat emitter at smtlib.ml:236-250. First ever source-level :pattern annotation emitted by tlapm.

The patch is ready for upstream review whenever the maintainers want to evaluate the design direction. Happy to open a PR against tlaplus/tlapm:main directly if the approach (pattern: key in read_method_arg, hint-only pragmas falling back to default method, add_pats on conclusion) is acceptable. If a different namespace (trigger: / qid:) or attachment site (e.g. on specific quantifier sub-expressions rather than the whole conclusion) is preferred, equally happy to revise.

cc @damiendoligez @muenchnerkindl @ahelwer

[ahelwer]

Per the CONTRIBUTING.md doc, please engage with the community before submitting large patch-sets or features. However, when you do so, it is expected that you engage as a human instead of sending a LLM text wall. You can re-open a new issue on this topic by typing up your motivation for having an agent submit this patch, or posting to the mailing list (again, not using a LLM) or joining the monthly community meeting: https://zoom-lfx.platform.linuxfoundation.org/meetings/tla?view=month

I will amend the CONTRIBUTING.md with language dissuading people from posting LLM text walls. This behavior is not appreciated.

[wirerhino]

@ahelwer Apologies, things got out of hand. I would also suggest to make the markdown and the repository AI friendly to prevent agents from taking independent autonomous actions.

Cheers

[lemmy]

@wirerhino How does the current markdown and repository cause agents to take autonomous actions?

[wirerhino]

@lemmy advanced AI models are fully capable of such things to pursue their target, even if explicitly told to not do so, they are statistical models after all. AI models take autonomous actions by design, the tricky part is steering and driving them. Introducing in the readme of the repository explicit clauses meant for for AI/LLMs would inform them to stop their action because it's not compliant. I don't know if you saw on LinkedIn some snapshot of people who were able to trigger autonomous actions from the recruitment agencies llms by adding specific sections on their resume, what I am suggesting here is to do the same thing, but on the opposite. I honestly hope the contribution was valuable anyway, and apologies again for the fuss

[muenchnerkindl]

Coming back to the proposed extension and putting aside the LLM aspect, I am a bit torn on the proposal. One of the basic design tenets of TLAPS has been to require users to break down a proof to a level of detail that can be checked fully automatically by existing automatic backends, without giving precise instructions to the backend on the mechanics of the proof. That's why TLAPS does not have a tactic language that exists in other proof assistants. Adding triggers for the SMT solvers risks opening a rabbit hole of gaining in automation while making proofs harder to maintain and more dependent on a particular solver, or even version of a solver.

That being said, full separation of concerns is not achievable, and TLAPS has long had some proof pragmas for backends. Also, as observed in the feature requests, adding triggers to the SMT input is mandatory for getting satisfactory proof automation. The current triggers were carefully designed for the fragment of TLA+ set theory that SMT supports, but since they are invisible to the user, they cannot be extended. In this sense, giving power users the ability to add custom triggers may be a reasonable suggestion. Also, adding triggers is logically harmless, as they cannot introduce unsoundness.

I have a technical question that I cannot find the answer to in the feature request: triggers are associated with (universal) quantifiers in the SMT input, but adding a Pattern pragma in the justification of the proof step does not indicate explicitly which quantifier(s) the pattern should apply to. In the provided example, there is only one quantifier, so there is no choice. However, in general there will be many quantifiers available in the context of a proof step that the pattern could potentially be attached to, and it is not clear to me which ones are chosen. (Attaching the pattern to all universal quantifiers in the context is logically harmless but may trigger too many instantiations and thus be counterproductive.)

It would appear more interesting to me to let users associate custom background SMT theories with certain TLA+ modules, a bit like TLC has Java overrides. Such extensions would be soundness-critical and would have to be carefully validated, for example by justifying the proposed axioms through proofs in Isabelle/TLA+, but they could be much more powerful than adding triggers locally. And of course they would contain relevant triggers similar to the built-in background SMT theories.