[CatarinaGamboa]

Fixes #297

A state error's Found now ends with a step called Relevant to Expected. This step keeps only the facts that the expected state depends on. The full Found is still the step before it. This is a display change only: the VC sent to the solver, the verdict, the hints and the category are all unchanged.

When a fact is left out (established independence)

Each fact (a conjunct of a Found row) is reduced to the solver terms it constrains:

• a ghost function applied to an object, f(x). A state stands for its state set function, so open(x) and state1(x) == state1(y) both constrain state1(x).
• a variable whose own value the fact constrains, such as mode, #canRedo_result, or x in x == y.

A fact is kept if it shares a term with Expected, either directly or through other kept facts. All other facts are left out. Different ghost functions, or the same function over different objects, are different solver terms, so a fact that shares no term with this group is independent of Expected.

To keep this safe, an object is never split into its ghost functions when any fact constrains it as a value (x == y) or passes it to an alias or an unknown function. In that case, all of its facts stay together. Conditions are not split either: facts under the same c ? … : … share c and stay together. No step is added when every fact or no fact is relevant. The pass works on expressions and ghost declarations, not on rendered names.

Before / after (CLI message, which uses the last step)

Example	Before	After
E_A3_07 scanner (the issue example)	startTiling(preview@53) && state2(preview@53) == state2(preview@52) && compressionSet(preview) && state1(preview) == state1(preview@53)	startTiling(preview@53) && state1(preview) == state1(preview@53)
Study A1_01 SlideRecoder	tilingNotExplicit(wParam) && compressionNotExplicit(wParam)	compressionNotExplicit(wParam)
A3_05 ScaledImageGenerator	startCompression(iwparam) && state1(iwparam) == 0	startCompression(iwparam)
ErrorTrafficLightRGB	green(tl@48) && red(tl) && r(tl) == r(tl@48) && g(tl) == g(tl@48) && b(tl) == b(tl@48)	red(tl)
ErrorArgumentPicksTheStateEarlier	tilingOff(param@24) && uncompressed(param@24) && tilingOff(param@25) && state2(param@25) == state2(param@24) && compressed(param) && state1(param) == state1(param@25)	tilingOff(param@25) && state1(param) == state1(param@25)

Expected is unchanged in every row. Across the 98 state-error cases in testSuite, 15 messages in 10 cases change. Only the Found text changes; other examples are resultset_forward_error, ErrorIteratorReturnHasNext, ErrorStateHintJoins and ErrorStateHintMultipleSets. The CLI output of the other 88 cases is byte-identical.

The six study exercises (proposal D): all report the same verdicts and lines. A1_01 gets the step, as shown above. A1_38 (open(buffered) && unmarked(buffered), where both state sets are in Expected), A1_09 (one conditional fact), and A1_56 (no Found, "could not prove it") have nothing safe to remove, so they get no step. A2_04 and A2_10 are refinement errors and are unaffected. In the A1_56 partial-fix variant (only redo() guarded), every fact sits under the shared #canRedo_result condition, so it also gets no step. Much of that noise comes from switch cases not being modelled (see the comment on #297).

Webview

The server already sends the whole history, so the extra step reaches the panel without any server change, and the back arrow returns to the full Found. However, vc-implications.ts labels the newest step "Simplified" and never shows its pass name. For the label "Relevant to Expected" to appear, vscode-liquidjava needs a one-line change: use simplification for index 0 when it is set. That change is not part of this PR.

Tests

• TestStateErrorContext#foundEndsWithTheFactsRelevantToTheExpectedStateSet: the message, the step name, and that stepping back shows the compression state set (existing fixture).
• VCSimplificationTest: two conservative cases where nothing may be left out: an object compared as a value, and an object passed to an unknown function. Each one fails if its rule is removed.

Full suite: 715 tests pass locally.

🤖 Generated with Claude Code

[CatarinaGamboa]

Codex review, round 1 (codex exec review --base origin/main): "The new filtering pass is limited to state-error diagnostics, and the targeted tests pass. I found no actionable regression in the diff." No findings, so the loop stops here.

[CatarinaGamboa]

Clean-code review (clean-code-principles)

Reviewed the diff only, weighed against the standing rules (smallest PR that tests well, match surrounding style, no tidy-only refactors, lean tests).

Finding	Verdict
VCRelevantFacts.java:60,64,81 - [core-dry] apply walks the nested rowFacts three times (forEach(facts -> facts.forEach(...)) twice, and a second mapToInt(List::size).sum() for the total)	Fixed in f413c9e. The facts are now flattened once into allFacts, which both loops use, and the total is allFacts.size(). No behaviour change.
VCRelevantFacts.java:79 - [core-dry] symbolsOf(fact, values) is computed again for each fact in the kept filter	Declined. Caching it per row needs a parallel nested list. The small cost is only paid when a state error is displayed.
VCRelevantFacts.java apply - [func-small] about 30 lines (collect, close over linked symbols, filter)	Declined. The three stages are separated by blank lines, and the fixed-point loop reads clearly in place. Extracting it would only move code.
VCRelevantFacts.java:59 - [func-few-arguments] addSymbols(expected, new HashMap<>(), values) passes a throwaway map	Declined. One recursive walk fills both sets. Splitting it in two would duplicate the traversal.
VCChecker.java ghostFunctionsOf and the VCRelevantFacts constructor @param describe the same contract	OK. One documents the implementation and the other the parameter it is passed as.
Comments and Javadoc - [doc-why-not-what]	OK. They state the soundness argument, not what the code does.
Tests - [lean tests] one integration assertion and two VCSimplificationTest cases	OK. Per the PR body, each test fails if its rule is removed.

Full suite locally after the fix: 715 tests, 0 failures.

[CatarinaGamboa]

Codex review, round 2 (soundness only)

Codex was asked to find concrete counterexamples where a dropped fact changes whether Found implies Expected, or where a kept fact misleads. It reported two findings, both from synthetic harnesses that call the pass directly.

1. A kept fact can outlive the row that binds its variable (∀q. state2(q) == 0 ⇒ state1(p) == state1(q), Expected state1(p) == 1, shown as state1(p) == state1(q)). Declined. The dropped row's only fact is about state2(q), which is independent of Expected. The kept fact still mentions q, and its name and line come from the translation table, not from the row. This matches main: NeededVariables already removes a binder row whose variable another row mentions ("a variable that another row mentions is already shown there").

2. Dropping an independent contradiction (state1(p) == 0 && state2(q) == 0 && state2(q) == 1, Expected state1(p) == 1). Declined, unreachable. Both callers of throwStateRefinementError (AuxStateHandler for invocations and for field writes) throw only after checkStateSMT fails, which means Found ∧ ¬Expected is satisfiable. An unknown result throws SMTUnknownError instead. So the full Found is satisfiable, and so is the dropped group. That group shares no term with the kept facts or with Expected, so Kept ∧ ¬Expected is satisfiable iff Found ∧ ¬Expected is. That is the equivalence the pass relies on, and Codex also notes that this path cannot emit the error.

Other cases Codex checked and found sound: a zero-argument ghost (rewritten to flag(p) and kept), and multi-argument or non-variable ghost arguments (their variables become value symbols, so their facts stay together).

No code change this round.

[CatarinaGamboa]

Codex review, round 3 (soundness only): no new findings

Codex was asked to dispute the round 2 declines only with a reachable counterexample, meaning a real program whose message is wrong. It ran the verifier on ErrorArgumentPicksTheStateEarlier and ErrorStateHintNaming, read the Z3 translation (makeFunctionInvocation, supertype coercion, field access, aliases), and reported no new findings.

The argument for why it holds. The pass can only be unsound if it under-links, i.e. if one Z3 term gets two different keys. Linking too much only keeps extra facts.

• Objects. An object is keyed by variable name, the same name its Z3 constant has. The supertype copies of a variable (storeVariablesSubtypes) keep that name.
• Ghost functions. A ghost is keyed by GhostFunction.getName(), both for a state's set and for a ghost called directly. So open(x) and state1(x) == state1(y) get the same key state1(x).
• Anything unresolved (a non-ghost function, an alias, a ghost with several or non-variable arguments) makes its variables value symbols. That keeps all the facts about those objects together.

Together with the satisfiability argument from round 2 (the error is only thrown when Found ∧ ¬Expected is satisfiable), a dropped group cannot change whether Found implies Expected.

Settled: no code change.