[CatarinaGamboa]

Closes #183. Closes #176.

What changes

The Found box of the Verification tab gets plain step headers and, when the verifier could not prove Expected, a Summary step. Every step the verifier sends stays reachable with the arrows, as the PM decided: "Let's show it all, we will work on those identifiers after."

• The chain stays, one conjunct per line, from Wrap the Verification panel at spaces and operators, one conjunct per line #189. The ∀x column (each binder still links to its source line) and the → arrows are kept, as the PM asked. The line layout comes from main's Wrap the Verification panel at spaces and operators, one conjunct per line #189 (getExpressionLines): one top-level conjunct per line, and a conditional's branches on indented lines. This PR does not split anything itself.
• "Could not prove it" says so, one step ahead. When the verifier's message ends with expected … but could not prove it (A1_56, A2_04), Found opens on a Summary step that reads Nothing is known here that could prove Expected. This is the wording of the verifier's Unknown category. The ← arrow goes back to the newest step, e.g. ∀undoManager undoManager == #getUndoManager_result, also when there was only one step.
• Every step is shown. Found shows every step of the verifier's derivation, oldest (Original) to newest, plus the Summary when there is one. Older steps whose facts use generated names (#if_condition, #switch_selector, extended#1) are shown too, as are runs of the same pass, one step per pass.
• Step header (Show the name of the newest Found step instead of "Simplified" #176, per the PM's decision there). The header shows Original, Simplified, or the name of a display step such as Relevant to Expected. An (i) icon after it gives a plain-language tooltip of what that step changed, e.g. "Replaced variables with the values they are equal to." Raw pass names (Binder, Substitution) are no longer shown. The tooltips cover every pass verifier 0.0.38 names: Substitution, Function Substitution, Binder, Known Enum Values, Folding, Arithmetic, Logical, Constraint, and the display step Relevant to Expected.

Steps on the six study exercises (main → this PR). Each count is the verifier's own step count, plus one for the Summary:

Exercise	main	this PR
A1_56 (could not prove it)	19	20 (Summary + 19)
A2_04 (could not prove it)	6	7 (Summary + 6)
A1_09	10	10
A1_01	7	7
A1_38	4	4
A2_10	3	3

No step repeats the one before it. The verifier records a step only when a pass changes the chain (VCSimplification.simplifyOnce returns the same result when the chain is equal). So the client needs no check for identical steps. A step can still look the same as the one before when the pass only changed a row Found does not draw, such as ∀#if_condition true →. Such a step is shown anyway.

Changes in this rework

• Every step is shown (PM's decision). The filter that hid older steps with generated names is removed. So are the merging of runs of the same pass into one step and the de-duplication of steps that looked like the step before. Its code (getVCSteps, sameLines, GENERATED_NAME) and its test are gone, and vc-changes.ts is back to main. Before this rework, A1_56 showed the Summary and 1 step, A1_09 1 step, A1_01 2 and A1_38 1.
• Generated names are left for later. #if_condition, #switch_selector and instance tags like extended#1 now show in the older steps. Render the verifier's line-tagged variable names instead of superscript counters #175 (line tags) and Explain the verifier's generated names (#if_condition, call results, …) on hover #195 (hover explanations) will handle them.
• Earlier in this rework: rebased on main (verifier 0.0.38, Wrap the Verification panel at spaces and operators, one conjunct per line #189, Show the message notes and the counterexample in the hover #190, Show every declared-here position and its gloss in the IDE panel #191, Show the Context tab's refinements as the error messages show them #186). The Summary is keyed on the message, not on errorCategory (see below), so this PR is client-only.

Why the client, not the verifier

The verifier's messages already leave generated names out: the hover of all six study exercises reads fine. The header and Summary only change how the view presents the steps the verifier sends.

Screenshots (headless VS Code, light theme, verifier 0.0.38)

Before: main (e333873). After: this branch (af43c9c).

A1_56 (could not prove it)

Before (19 steps)	Before, oldest step	After: opens on the Summary (20/20)	After, one step back (19/20)	After, oldest step (Original, 1/20)

A1_09 (path condition and state)

Before (10 steps)	After: Relevant to Expected (10/10)	After, one step back (9/10)	After, oldest step (1/10)

A2_10 (refinement error, three steps on both)

Before	After, Simplified 3/3	After, Original 1/3

A1_01, A1_38, A2_04

	Before	After	After, one step back	After, oldest step
A1_01 (7 steps)
A1_38 (4 steps)
A2_04 (Summary + 6)

For the PM

• When should the Summary show? It is keyed on the message ending in but could not prove it, not on errorCategory. In 0.0.38 the two differ for some state errors. For example, if Found states only a non-state ghost of the receiver (size(b) > 0), the category is unknown but the message reads found size(b) > 0 but expected open(b). The message is what the hover shows, so it decides here. For refinement errors they agree, as they do on all six study exercises. Is keying on the message right?

Tests

vc-implications.spec.ts has two tests, each failing on main:

• every step of the verifier is shown, including an original chain with #if_condition and two Binder steps in a row, each under Original, Simplified or Relevant to Expected with its tooltip (it also fails on the previous head, 55510f8, which hid these steps);
• the Summary when the message says could not prove it, with the chain one step back.

The test for skipping steps with generated names and merging pass runs is removed with that code.

Local results on af43c9c: npm run test:unit (134 passed), test:typecheck, lint, server mvn -B package (42 tests), integration xvfb-run -a npm test on VS Code 1.82.0 (minimum; 9 + 1 passing). Codex review of this rework: one round, whose only finding (the Summary keyed on the message) was declined as in rounds 1 and 2.

🤖 Generated with Claude Code

[CatarinaGamboa]

Codex review, round 1 (codex exec review --base origin/main)

I found no actionable regression in the diff. The client typecheck and focused VC implication tests pass.

Nothing to fix.

🤖 Generated with Claude Code

[CatarinaGamboa]

Clean-code review (clean-code-principles skill, on this PR's diff)

• client/src/webview/views/diagnostics/vc-implications.ts:98 - [core-kiss] The merge test relied on undefined > 0 being false for the first step. Fixed (0f68b5f: the condition now checks last !== undefined once and reads as "same facts, or same pass after the original").
• client/src/webview/views/diagnostics/vc-implications.ts:39 - [core-encapsulation] "Nothing is known" is keyed off the verifier's message text (… but could not prove it). Declined for now: it keeps Found and the hover in agreement by construction, and a structured flag needs a verifier release. Listed as a PM question in the description.
• client/src/webview/views/diagnostics/vc-implications.ts:87 - [func-single-purpose] getVCSteps picks the steps and then collects each step's passes. Declined: 27 lines, both halves share the derivation and facts arrays; splitting adds parameters without making either clearer.
• client/src/webview/views/diagnostics/vc-implications.ts:24-35 - [core-dry] Two description maps. Declined: membership in the pass map is what tells a display step (shown by name) from an internal pass, so the split carries meaning.
• client/src/webview/views/diagnostics/vc-changes.ts:15 - [org-package-cohesion] getFacts reads the chain in the diff module. Declined: it replaces getImplicationLines, which lived there; moving it is churn.

🤖 Generated with Claude Code

[CatarinaGamboa]

Codex review, round 2

[P1] Preserve the implication between assumptions and conclusion — vc-changes.ts:15-20. When a VC contains an antecedent and a conclusion, getFacts renders every predicate as an independent fact. For example, x > 0 => x > 1 is displayed as though both are known, even though the latter is the proposition being checked.

Declined. The chain sent as found has no conclusion: what is checked is Expected, shown in its own section. The verifier reads Found's rows as a conjunction (VCImplication.toPredicate() / toConjunctions(), and VCBinderSimplification: "Found reads its rows as a conjunction, so P && true -> P"), and the hover message prints them joined with && (e.g. A1_09: found newMode == BORDERLESS && (…) but expected …). Listing them as facts is the same reading.

🤖 Generated with Claude Code

[CatarinaGamboa]

Codex review, round 3

[P1] Preserve source navigation for Found variables — vc-changes.ts:15-19. Rendering only predicates removes the source-highlight button that let users jump to a binder's declaration.

Declined here, raised for the PM. The links lived on the ∀x binders, which this PR removes because novices are not told what they mean. Putting a link on each fact is a design question (see "For the PM" in the description). One caveat: the translation table is keyed by display name, so every #case_condition row would link to the same case. The Context tab and Locations still link to the code.

[P2] Do not hide Found facts based solely on the error message — vc-implications.ts:173-175. Failure to prove Expected does not mean nothing is known.

Declined, intended. The sentence does not claim that nothing is known. It says nothing is known here that could prove Expected, which is the verifier's own reading: it prints "could not prove it" exactly when no fact of Found bears on Expected (no fact linked to Expected, or for a state error none that names a state). It also uses the wording of the verifier's Unknown category. Showing the unrelated facts (A1_56: undoManager == #getUndoManager_result) is what the study renders flagged as contradicting the hover. Keying it off the message keeps Found and the hover in agreement; a structured flag from the verifier is listed as a PM question.

Codex's remaining findings are design decisions already listed for the PM, so the loop stops here.

🤖 Generated with Claude Code

[CatarinaGamboa]

Error category instead of the message text (3209ab8, 02de671)

• The server sends the verifier's ErrorCategory as errorCategory on LJErrorDTO, lowercase and hyphenated like HintDTO.kind. lsp4j leaves the field out when the verifier gives none. Found says Nothing is known here that could prove Expected. when it is unknown; the verifier uses unknown exactly when the message says "but could not prove it". The regex on the message is gone.
• Re-rendered end to end with verifier 0.0.37: A1_56 and A2_04 are unknown and look as in the screenshots; A1_09 is path-dependent-state and A2_10 out-of-domain, both unchanged.
• Tests: two assertions in DiagnosticConverterTest (unknown on a refinement error, absent on an uncategorized state error); the client test now passes the category with a neutral message. mvn -B test, test:unit, test:typecheck and lint pass.

Codex review, round 4 (on 3209ab8)

[P2] Show a fallback when every predicate is true — vc-changes.ts:17-20. When a non-unknown error has a VC chain containing only true, Found renders blank. This is a real case for state refinement errors with no category.

Fixed in 02de671. Found also says that nothing known proves Expected when its newest step states nothing. This covers a state error the verifier leaves uncategorized because the state is checked elsewhere. A second case of the same test covers it.

[P2] Preserve source navigation for Found variables — vc-changes.ts:23-27.

Declined, as in round 3: left to the PM (see the description).

Codex review, round 5 (on 02de671)

I found no actionable regressions in the diff. The client typecheck and unit tests, and the server tests, passed.

🤖 Generated with Claude Code

[CatarinaGamboa]

Codex review, round 6 (after keeping the binders and implications, with a line per conjunct)

1. [P2] "the verifier sends FunctionSubstitution". Not changed: VCSimplificationPass.getName() in verifier 0.0.37 splits camel case, so VCFunctionSubstitution is sent as Function Substitution, which is what the map uses.

[CatarinaGamboa]

Codex review, round 7

1. [P2] An && inside a string literal (value == "a&&b") was split across two lines. Fixed: the splitter now skips string literals, and the test covers it.

[CatarinaGamboa]

Codex review, round 8

1. [P2] a || b && c was split into a || b and c, which shows the wrong grouping. Fixed: a fact with an ||, --> or ?: outside parentheses stays on one line. The test covers all three.
2. [P2] "constant folding is not in the map". Not changed: that string is only a fixture in DiagnosticConverterTest. The verifier class is VCFolding, sent as Folding, which the map has.

[CatarinaGamboa]

Codex review, round 1 (codex exec review --base origin/main, on the reworked branch: #185 rebased on main, its own conjunct splitting dropped in favour of #189's)

One finding:

• [P2] Summary picked from the message suffix alone ("Found x >= 0, Expected x > 0 can still end in but could not prove it"). Declined. In verifier 0.0.38 (ErrorMessage.of) the message says expected … but could not prove it only when no fact of Found is linked to the terms of Expected (for a state error: when none of the linked facts names a state). x >= 0 is linked to x > 0, so that message reads found x >= 0 but expected x > 0 and Found shows the chain. The Summary therefore appears exactly when the verifier itself says nothing found could prove Expected.

[CatarinaGamboa]

Codex review, round 2

Two findings, both declined:

• [P2] "constant folding" is not in the tooltip map. That name is only test data in DiagnosticConverterTest (a hand-built VCSimplificationResult). Verifier 0.0.38 names each pass from its class (VCSimplificationPass.getName): Substitution, Function Substitution, Binder, Known Enum Values, Folding, Arithmetic, Logical, Constraint, plus the display step Relevant to Expected. The map covers all of them.
• [P2] Summary for Found x > 0 vs Expected x > 1 (same as round 1). Checked against 0.0.38 with the server jar: f(@Refinement("x > 0") int x) { @Refinement("y > 1") int y = x; } gives found x > 0 && y == x but expected y > 1, so Found shows the chain, not the Summary. could not prove it only comes when no found fact is linked to Expected.

[CatarinaGamboa]

Codex review, round 3 (codex exec with the diff and the round 1–2 declines in the prompt)

One finding, declined:

• [P2] Steps with x#1 are dropped. This is by design (item 2 of this PR, unchanged by the rework). An older step is hidden when its chain uses a generated or numbered name (#if_condition, extended#1), because those names are explained nowhere; the newest step is always shown. When the newest step has such a name too, the older ones are hidden as well, which is the intent. Instance tags under "For the PM" covers this.

[CatarinaGamboa]

Codex review, round 4

One finding, fixed:

• [P3] The Relevant to Expected tooltip was too narrow. It said the step keeps "the facts that share a term with Expected", but verifier 0.0.38's VCRelevantFacts also keeps facts linked to Expected through other facts (compressionSet(q) via p == q for Expected tilingSet(p)). It now reads Kept only the facts that Expected depends on, directly or through other facts. (55510f8)

[CatarinaGamboa]

Clean-code review (clean-code-principles checklist, on the reworked diff)

No changes needed.

• core-dry: the conjunct splitting is gone. Found now uses Wrap the Verification panel at spaces and operators, one conjunct per line #189's getExpressionLines through renderVCLine, and the step filter reuses getImplicationLines, which is only exported now. So there is one line model for both.
• solid-srp: getVCSteps picks which steps to show, getStepLabel names them, and renderSelectedStep renders. Each does one job.
• name-searchable: the pass names, tooltip texts and the verifier's could not prove it ending are named constants.
• Coupling to note (accepted): NOT_PROVEN matches the verifier's message wording. That wording is pinned with the verifier version in server/pom.xml. A verifier bump that rewords it would stop the Summary from appearing, but would not show anything wrong.

[CatarinaGamboa]

Codex review, round 1 on "show every step" (codex exec review --base origin/main, on af43c9c: the step filter, the pass-run merging and the look-alike de-duplication removed)

One finding, declined:

• [P1] Summary picked from the message suffix alone (Found x >= 0, Expected x > 0). Declined, as in rounds 1 and 2: in verifier 0.0.38 (ErrorMessage.of) the message ends in but could not prove it only when no fact of Found is linked to Expected, so x >= 0 vs x > 0 gets found x >= 0 but expected x > 0 and Found opens on the chain. The Summary is also kept by the PM's decision; whether to key it on the message stays an open question for the PM in the PR body.

Nothing was found in the change itself (every step shown, header and tooltip per step).