[CatarinaGamboa]

Closes #183. Closes #176.

What changes

The Found box of the Verification tab only shows what a novice can read (advisor's rule for the study: if users are not told what it means, don't show it).

• The chain, with a line per conjunct. The ∀x column (each binder still links to its source line) and the → arrows stay, as the PM asked. Each fact is split at its top-level &&, one conjunct per line under its binder, with && at the end of every line but the last. A && inside parentheses or a ternary stays on its line.
• "Could not prove it" says so, one step ahead. When the verifier's error category is unknown, which it is exactly when the message says "expected … but could not prove it" (A1_56, A2_04), Found opens on a Summary step reading Nothing is known here that could prove Expected. (the wording of the verifier's Unknown category). The arrows go back to the chain, e.g. ∀undoManager undoManager == #getUndoManager_result, also when there was only one step. It does the same when the newest step states nothing. The server now sends that category as errorCategory on LJErrorDTO, lowercase and hyphenated like HintDTO.kind; lsp4j leaves the field out when the verifier gives none.
• Steps worth showing. Older steps are shown only when their facts use no generated name (#if_condition, #switch_selector, extended#1), one step per run of the same pass, and none that looks like the step before. A1_56 went from 19 steps to none, A1_01 from 7 to 2.
• Step header (Show the name of the newest Found step instead of "Simplified" #176, per the PM's decision there). Original, Simplified, or the name of a display step such as Relevant to Expected; an (i) icon after the label gives a plain-language tooltip of what changed since the step before, e.g. "Replaced variables with the values they are equal to." Raw pass names (Binder, Substitution) are no longer shown.

Why the client, not the verifier

The verifier's messages already leave these names out: the hover of all six study exercises reads fine. Binder names reach users only through the IDE's binder column. Generated names inside facts appear only in the steps before simplification. So the fix belongs in the view. The only server change sends the category that verifier 0.0.37 already computes; no verifier change is needed.

Screenshots (headless VS Code, light theme)

Current (binders, arrows, a line per conjunct)

A1_56, opens on the summary	A1_56, one step back

A1_09	A2_10

The rest are from the first version, before the review, which had no binders or arrows. Before: main with verifier 0.0.37 (pr-screenshots/study-0.0.37). After: that first version.

A1_56 (could not prove it)

Before	Before, oldest of 19 steps	After

A1_09 (path condition and state)

Before	After

A2_10 (refinement error, two steps)

Before	After, Simplified 2/2	After, Original 1/2

A1_01, A1_38, A2_04

	Before	After
A1_01
A1_38
A2_04

For the PM

• Source links on binders are gone with the binder column (Make source-linked refinement binders visibly clickable #118 made ∀x clickable to its source). The Context tab and Locations still link to the code. Should a fact link to its source line, e.g. through a small "line 62" link after it? One caveat: the translation table is keyed by display name, so all #case_condition rows share one entry and would link to the same case.
• Instance tags (extended#1) only hide older steps here; Render the verifier's line-tagged variable names instead of superscript counters #175 replaces them with line tags (x@51), and those steps will show again then.

Tests

vc-changes.spec.ts (binder column and arrows) is replaced by three tests in vc-implications.spec.ts, each failing on main: facts without binders/arrows/true and the Original/Simplified header; skipping steps with generated names and merging a pass run under a display step's name; the "nothing is known" sentence, for an unknown category and for a Found that states nothing. DiagnosticConverterTest gains two assertions on errorCategory. npm run test:unit (124 tests), test:typecheck, lint and server mvn -B test pass locally.

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