GeezerVison

…#459)

## Problem

When a method reads a field, Found shows a row for it under its internal
name, and the row says only `true`. Issue reproducer (`ArrayList.size()`
refined `_ == size(this) && _ >= 0`, `Random.nextInt(bound)` refined
`bound > 0`):

```
∀this#shop.Basket.items   true →
∀bound⁶                   bound⁶ == size(items) && bound⁶ >= 0
```

In the IDE the first row wraps over several lines, above the row that
matters. The message and the later row also write the field as `items`,
so it reads like the local it was copied into.

![A2_10 in VS Code,
before](https://raw.githubusercontent.com/liquid-java/liquidjava/pr-screenshots/issues/457/verification.png)

## Cause

1. `VCBinderSimplification` dropped a `true` binder only when no later
row mentioned its variable. Here `size(this#shop.Basket.items)` mentions
it. Every field, parameter, call result or local that is only passed
along keeps its `true` row this way. The `∀getUndoManager⁸⁵⁶ true` and
`∀#fresh… true` rows of #375 come from the same rule.
2. `VariableFormatter.format` left `this#<package>.<Class>.<field>`
unchanged. The binder, the counterexample and the extension's context
and translation-table keys therefore showed the internal name, while
`ExpressionNameResolver` cut it down to the bare `items` inside
expressions.

## Fix

### Which `true` rows stay

A binder refined only by `true` states no fact. It stays in Found only
when the error needs it:

- **Linked to Expected.** Some fact of the chain constrains the binder's
*value* and is linked to Expected, meaning it shares a term with
Expected directly or through other linked facts.
- Terms are variables and ghost or state applications such as `size(x)`.
- Facts are the rows' conjuncts. A negated disjunction is split first:
`!(p || q)` becomes `!p` and `!q`, so one combined guard does not link
everything.
- A variable of an **object** type that a fact names only as a ghost
argument (`x` in `b == size(x)`) is not constrained by that fact. Its
row would say nothing, so it goes. A primitive argument (`k` in `y ==
f(k)`) has a value of its own and is kept.
- **Expected constrains its value, in a refinement error only.** The
counterexample then shows that value; `filterCounterexample` lists only
binders. A state error has no counterexample, so there this alone keeps
nothing.

The rule depends only on the chain and Expected, not on Z3's model, and
it works the same way for both error kinds.

A kept `true` binder that comes after a row using its variable is moved
to just before that row. This is a separate `Binder` step.

Examples:

| Case | Rows (after) |
|---|---|
| issue reproducer | `∀bound⁶ bound⁶ == size(this.items) && bound⁶ >= 0`
(field only inside `size(...)`) |
| `if (port < 0) return; positive(t);` | `∀#fresh !(port < 0)`, `∀t
true`: `port` dropped (unlinked guard), `t` kept (Expected,
counterexample `t == 0`) |
| `if (p \|\| q) return; positive(t);` | `∀#fresh !(p \|\| q)`, `∀t
true`: `p` and `q` dropped |
| `int y = x + 1` refined `_ > 0` | `∀x true`, `∀y y == x + 1`: `x`
kept, linked through `y` |
| `ErrorStateHintPathDependent` (state) | `∀ready true`, `∀f ready ?
open(f) : created(f)`: `ready` kept |
| state errors whose Found is otherwise `true` | unchanged from `main`:
no `∀it true` / `∀this true` row is added |
| `for (int i = start; i < served; i++) positive(i);` | `∀Basket.served
true`, `∀i true`, `∀#fresh i < Basket.served`: `i` now before its first
use |

The linking is `VCSimplificationUtils.linkedConjuncts(conjuncts,
termsOf, seed)`. It does what `linkedTerms` in `RefinementError` does on
#460 (branch `fix/counterexample-expected-vars`, issue #453): the same
closure over shared terms, with the term function passed in. Once both
are merged, `linkedTerms` can call this helper with its `termsOf`, and
`splitConjuncts` can replace `getConjuncts` there, so the counterexample
and the rows are linked in the same way. I didn't touch
`filterCounterexample`.

### Simplification history (the VS Code arrows)

Dropping a `true` row is an ordinary simplification step of the `Binder`
pass, one binder per step. It goes into `VCSimplificationResult`'s
origin chain, which the extension's server sends whole
(`VCSimplificationResultDTO.origin`). The panel steps back through that
chain, and its last step is the untouched `Original` with every binder.

What the panel shows for the issue reproducer:

| Step | `main` (2 steps) | this branch (3 steps) |
|---|---|---|
| 1 Original | `∀this#shop.Basket.items true`<br>`∀items⁵ items⁵ ==
this#shop.Basket.items`<br>`∀bound⁶ bound⁶ == size(items⁵) && bound⁶ >=
0` | `∀this.items true`<br>`∀items⁵ items⁵ == this.items`<br>`∀bound⁶
bound⁶ == size(items⁵) && bound⁶ >= 0` |
| 2 after Substitution | (Simplified) `∀this#shop.Basket.items
true`<br>`∀bound⁶ bound⁶ == size(items) && bound⁶ >= 0` | `∀this.items
true`<br>`∀bound⁶ bound⁶ == size(this.items) && bound⁶ >= 0` |
| 3 after Binder | | (Simplified) `∀bound⁶ bound⁶ == size(this.items) &&
bound⁶ >= 0` |

The field display name is applied at every step, including Original,
because the server formats every step with `VariableFormatter.format`.
The internal names are untouched in the history itself.
`TestFoundBinders.steppingBackReachesTheOriginalWithTheDroppedRow`
checks that the original's binders are
`this#testSuite.classes.found_true_binders_error.Basket.items`,
`#items_…`, `#bound_…`. Showing the Original raw would be a one-line
change in `VCImplicationDTO` (skip `format` for the oldest step), but I
left that for the PM to decide.

### Source-like field names

`this#pkg.Class.field` is written `this.field` in the message, the Found
rows, the counterexample and the extension's context and translation
table. This holds for both `this.x` and bare `x`. A static field is
written `Class.field`. Instance counters stay (`this.interrupts¹¹³`),
nested classes and long package names reduce the same way, and the
**internal SMT name is unchanged**.

Static-ness is not in the name, so `Utils.qualifyFieldName` records
static fields as it builds their names, and `CommandLineLauncher.launch`
clears the record at the start of each run. Every error comes from code
verified in that run, which also built the names of the fields it shows,
so the record is complete for that run's errors. Verifying a static
`total`, then an instance `total` of the same class, then the static one
again in one JVM shows `C.total`, `this.total`, `C.total`. There is no
incremental verification that skips classes. If one is added, the record
would need to be filled from the field declarations instead.

I removed the earlier class-based disambiguation (`Basket.this.count`).
Real code could not reach it, it was not valid Java for inherited
fields, and it was not applied to binder rows or translation-table keys.
Two different fields with the same simple name in one expression (a
shadowed field) now both read `this.x`.

### Writes to another object's field (display only)

This PR does not change what the verifier accepts or rejects for any
write. A write to another object's field (`other.level = …`,
`other.level++`, `other.level--`, `other.level += …`) is still checked
and tracked exactly as on `main`, against the current object's field
variable.

Only its label changes. When `TypeChecker.checkVariableRefinements`
creates the new instance for a write that `Utils.accessesTrackedField`
says is not to the current object, it records the receiver's variable
name for that instance in `VariableFormatter` (a bare field name when
the receiver is not a variable). The instance is then written
`other.level¹` instead of `this.level¹`:

```
main:   level¹ == -1 is not a subtype of level¹ >= 0
now:    other.level¹ == -1 is not a subtype of other.level¹ >= 0
```

Because tracking is unchanged, a decrement shows what the verifier
actually uses as the old value: `other.level⁹ == this.level⁸ - 1`.
Writes through another object leak into `this.level`, and aliasing with
`this` is not handled. Both are left for their own issue.

Parity with `main`, checked on the reviewers' reproducers and
`ErrorOtherObjectFieldWrite.java`:
- `other.level++`, `other.level += 1` and `other.level = other.level +
1` verify.
- `other.level--` and `other.level = -1` are reported.
- The write through `W other = this` and `maybeSelf(this)` are reported.
- The `other.level = 5; int k = this.level` (`_ == 5`) case verifies as
on `main`.

### #375

This covers part of #375, not all of it. The `true` rows go, and in the
JabRef `EditAction` exercise all four are removed. The path conditions
over now-undeclared fresh variables (`∀#fresh¹²² !#fresh¹²¹`) are not
`true` rows and stay; they also tie in with #373. #375 stays open.

## Before / after (main vs this branch, every error)

I ran the harness that dumps what the IDE gets (message, rows,
counterexample, translation-table keys) over 321 test-suite errors and
117 errors from the 98 study exercises, with `main` and this branch on
identical inputs:

- The same errors are reported at the same lines on both sides (the
harness requires it), so nothing that `main` accepts or rejects changes.
- 58 test-suite errors and 57 exercise errors differ in what they show.
- The differences are renames (`this#…` to `this.x` or `Class.x`),
dropped `true` rows, the `Binder` reordering, and in refinement errors a
kept `true` row for an Expected variable. In those refinement errors
`main` showed only `true`; now the variable's counterexample value also
shows, e.g. `port == 65536`.
- `true` rows: 110 → 87 (test suite), 78 → 46 (exercises). Raw `this#`
names: 30 → 0 and 72 → 0.
- No state error gains a `true` row.
- **Instance numbers do not move**: 0 of the 438 messages change their
superscripts. I could not reproduce the `transactionCommitted²⁷→²⁸`
shift (A1_50 shows `²⁸` on both). I think it came from different inputs
between the two runs.

**Several fields** (`pickAny`)
```
before: ∀this#testSuite.classes.found_true_binders_error.Basket.items³⁷   true
        ∀first³⁸   first³⁸ == size(items³⁷) && first³⁸ >= 0
        ∀this#testSuite.classes.found_true_binders_error.Basket.extras⁴¹   true
        ∀second⁴²  second⁴² == size(extras⁴¹) && second⁴² >= 0
        ∀bound⁴⁵   bound⁴⁵ == first³⁸ + second⁴²
after:  ∀first³⁸   first³⁸ == size(this.items³⁷) && first³⁸ >= 0
        ∀second⁴²  second⁴² == size(this.extras⁴¹) && second⁴² >= 0
        ∀bound⁴⁵   bound⁴⁵ == first³⁸ + second⁴²
```

**Static field, linked to Expected** (`serve`)
```
before: count⁵⁴ == served + 1 is not a subtype of count⁵⁴ > 0
        ∀this#testSuite.classes.found_true_binders_error.Basket.served   true
        ∀count⁵⁴   count⁵⁴ == served + 1
after:  count⁵⁴ == Basket.served + 1 is not a subtype of count⁵⁴ > 0
        ∀Basket.served   true
        ∀count⁵⁴   count⁵⁴ == Basket.served + 1
        Counterexample: Basket.served == -1 && count⁵⁴ == 0
```

**Field holding a state kept, unrelated `true` parameter dropped**
(`classes/found_field_state_error`, after Jpcsp's `IntrManager`)
```
before: ∀intrNumber   true
        ∀#fresh¹⁶     !(intrNumber < 0 || intrNumber >= 67)
        ∀this#testSuite.classes.found_field_state_error.InterruptManager.interrupts¹³   empty(interrupts¹³)
after:  ∀#fresh¹⁶     !(intrNumber < 0 || intrNumber >= 67)
        ∀this.interrupts¹³   empty(this.interrupts¹³)
```

## Tests

- `TestFoundBinders` (19 tests) on the fixtures
`classes/found_true_binders_error`, `classes/found_field_state_error`,
`ErrorStateHintPathDependent.java` and the new
`ErrorOtherObjectFieldWrite.java`:
- dropped: the reproducer's field row; a `true` parameter, call result
and local; several fields; `port` behind an unrelated guard; `p`/`q`
behind one combined guard.
- kept: `x` linked through `y == x + 1`; an Expected variable in a
refinement error; `ready` in the path-dependent state error; the field
row holding `empty(...)`.
  - row order for a loop variable.
- names: static `Basket.served`; `this.amount` and bare `amount` written
alike; an inner-class field; `other.level` for writes and decrements on
another object, and `this.level` for an own write.
- parity with `main` for writes: `other.level++` and `other.level += 1`
verify; `other.level--` and the write through an alias of `this` are
reported.
- the original the panel steps back to keeps the dropped row and the raw
binder names, and the history includes a `Binder` step.
- `VCBinderSimplificationTest` (13 new, including a primitive ghost
argument that is kept):
  - linked through one or several rows;
  - an unlinked guard;
  - a split negated disjunction;
  - an Expected binder in refinement vs state errors;
  - linking through a ghost while keeping only value variables;
  - an object named only inside a ghost;
  - moving a kept binder before its first use;
  - the `NeededVariables` factories.
- `VCSimplificationUtilsTest` (4): splitting conjuncts and negated
disjunctions; transitive linking.
- `VariableFormatterTest` (6 new) and `ExpressionNameResolverTest` (2
new): instance, static, nested, long-package and other-object field
names; clearing the static record between runs; a field next to a local
of the same name; a field inside a ghost argument.

Without the fix (`main` sources, the new tests kept), `TestFoundBinders`
fails 15 of 19 and `ExpressionNameResolverTest` fails 2 of 5. The unit
tests on the new API do not compile on `main`.

`mvn test` (verifier): **583 tests, 0 failures** (`main`: 534).

**Changed existing expectations**
-
`VCBinderSimplificationTest.keepsTrueBinderWhenVariableIsUsedDownstream`
became `removesTrueBinderUsedDownstreamWhenNothingNeedsIt`: with nothing
to link to, the binder goes. That is the rule change itself.
-
`VCBinderSimplificationTest.skipsInapplicableTrueBinderAndSimplifiesLaterBinder`
now makes `x` an Expected variable, so its binder is still the
inapplicable one the test is about. The expected steps are unchanged.
- `VCTestUtils.parseImplication` splits a binder at the first `.` after
the `:`, so binder names can contain dots.

No `// Expect:` fixture, `TestCounterexamples` or `TestErrorCategories`
expectation changed.

## Not in this PR

- Raw names in the Original step (above).
- `random.nextInt(items.size() + extras.size())` fails on `main` with
`Sort mismatch … supplied sort is …Basket`, a separate translation bug.
The fixture uses two locals instead.
- The client's hover (`getOriginalVariableName`) strips only `this#`, so
it does not match fields, before or after this change. Stripping a
leading `this.` there would be a small follow-up in vscode-liquidjava.

Fixes #457

🤖 Generated with [Claude Code](https://claude.com/claude-code)

---------

Co-authored-by: Claude Opus 5.5 <[email protected]>