[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.