[CatarinaGamboa]

In VS Code, the language server verifies the whole source tree again on every save, in the same JVM, and asks Z3 mostly the same queries each time. On the study workspace (proposal-C-stars, 15 files) a save makes about 1,100 queries. About 96% of them depend only on the library specs: the typestate state machines built for state hints, and the satisfiability check of each @StateRefinement.

This PR keeps solver results across verification runs, in memory, so a save after the first one only asks Z3 the queries that changed.

How a query is identified

The cache sits in SMTEvaluator, around the only place the verifier calls Z3. The key (smt/QueryCache.java) is everything TranslatorToZ3 reads to build the query:

• the expression, node by node (an ExpressionVisitor, so a new AST node does not compile until the key handles it), with static final constants including their resolved values;
• for each variable: its type (the enum constants for an enum) and its supertypes;
• every enum, ghost and ghost state in the context.

Variables are renamed in order of first appearance. A query whose fresh variables were numbered differently because of an edit earlier in the file is still found. Names that denote enum constants (Mode.Photo) are values, not variables, so they are never renamed. The translator and the cache share the helper that names them.

Results only live in memory, for as long as the process runs, so the verifier and the solver cannot change under them.

What is never reused:

• Unknown results are never kept.
• Translation errors (e.g. a name that is not found) are never kept.
• Counterexamples are only reused when the variables have exactly the same names. Otherwise a caller that needs one asks Z3 again. Callers that only use the yes/no answer (checkStateSMT, which builds the state machines and checks state refinements, and the constraint simplifier) say so and get the cached answer.

Keeping it correct

• Switch: -Dliquidjava.cache=on|off|check (default on). check recomputes every result it finds in the cache and throws an AssertionError on any difference. An AssertionError is not caught by the code that recovers from exceptions, so a mismatch cannot be hidden.

• The whole test suite runs in check mode (surefire systemPropertyVariables). Every cache hit during mvn test is verified against a fresh solver call.

• TestQueryCache verifies a program, edits one thing the queries depend on without changing their text, and verifies it again in the same JVM, as the language server does after a save. The cached result must equal an uncached run, and the edit must change the result. The edits:

  • a typestate transition;
  • a state refinement that can never hold;
  • a parameter's type (int → long: v > 0 implies v >= 1 only for integers);
  • the constants of an enum;
  • the type of a ghost (int → double).

  Each test also checks that both versions of the program reach the solver, so a test cannot pass because the edited program fails to parse.

• enumConstantsAreValuesNotVariables: photo(Mode.Photo) and photo(Mode.Video) differ only in the enum constant, and the second call must be reported. A first version of this PR renamed enum constants like variables, so both calls shared one key and the second could have reused the first's "ok". The check mode caught this while I was reviewing the code, and this test fails on that version.

• QueryCacheTest checks the renaming, and that variable types and supertypes are part of the key.

• Mutation check: I removed each part of the key in turn. Removing any of these makes a test fail:

  • variable types;
  • ghost declarations;
  • literal values;
  • supertypes;
  • the exclusion of enum constants from renaming.

Same results

I compared every diagnostic, with its full rendered message, hints and counterexamples included, against main. These results are for the final version. All cases ran in a single JVM, so specs are shared between cases and the cache gets many hits:

Corpus	Cases	check mode: mismatches / crashes	on mode: verdict / message diffs vs main
testSuite	298	0 / 0	0 / 0
Study exercises (exercises, exercises-oss)	98	0 / 0	0 / 1*
Barista conformance tests	3,262	0 / 0	0 / 0

* The variable number in one message (transactionCommitted²⁷ vs ²⁸). The messages are otherwise identical. This is the existing determinism issue described below.

mvn test: 205 tests, 0 failures.

Timings

Study workspace, the same 15 files verified 5 times in one JVM, like 5 saves. The machine was shared, so main-thread CPU time is shown too:

	cache off	cache on
First save, CPU	14.2 s	9.1 s (queries repeat within a run)
Later saves, CPU	9.1–10.4 s	2.2–4.6 s
Z3 solves, all 5 saves	5,965	716

Corpus totals (each corpus in one JVM, on a shared machine): Barista 9,667 s → 349 s, exercises 207 s → 77 s.

The CLI verifies once and exits. It still benefits within a run, from repeated queries, and otherwise behaves as before.

Not changed / known

• Dead code: SMTEvaluator lost a catch (SyntaxException) that nothing could throw. It only compiled because TranslatorToZ3.close() declares throws Exception, and with the solving moved into its own method it no longer compiles.
• Key maintenance: if TranslatorToZ3 starts reading something new from the context, the key must include it. The class comment says so, and check mode in the tests is the safety net.
• An existing determinism issue on main: the numbering of fresh variables in one message (transactionCommitted²⁷ vs ²⁸ in E_OSS_A1_50) depends on what was verified earlier in the same JVM. It shows with the cache off as well, and does not affect verdicts. I'll look into it separately.

🤖 Generated with Claude Code

[rcosta358]

lgtm