GeezerVison

Refs #435 (first part: named sets only; carrying a set per branch stays
open).

## What
`@StateSet` takes an optional `name`:

```java
@stateset(name = "phase", value = {"start", "canEdit", "end"})
@stateset(name = "undo",  value = {"undoable", "notUndoable"})
@stateset(name = "redo",  value = {"redoable", "notRedoable"})
```

A named set's ghost function is called by that name instead of the
generated `stateN`. Messages, hints, simplification steps and the
equalities that keep unmentioned sets
(`AuxStateHandler.getMissingStates`) show `redo(um)` instead of
`state3(um)`. Specs can use the name anywhere a ghost works, for example
`to = "return ? undoable(this) : undo(this) == undo(old(this))"`. It
works in classes, interfaces and `@ExternalRefinementsFor` specs.
Unnamed sets keep `stateN` with the same numbering, so existing specs
behave the same.

Checks, all reported as `Error` (`CustomError`, the same kind as "State
names must start with lowercase"), on the name:
- not a string literal (e.g. a constant)
- not an identifier starting with a lowercase letter, or
`old`/`true`/`false`
- already the name of a state, a `@Ghost`/`@RefinementPredicate` ghost
or another set of the class (generated `stateN` included). An alias
can't clash, because alias names start with an uppercase letter.

## Before / after
Study variant A1_56 (redo guarded, undo not), with the names
`phase`/`undo`/`redo` on the spec:

Before:
```
State Refinement Error: found (#canRedo_result ? redoable(undoManager@70) : notRedoable(undoManager@70)) && state2(undoManager@70) == state2(#getUndoManager_result) && limit(undoManager@70) == limit(#getUndoManager_result) && (#canRedo_result ? undoable(undoManager) && notRedoable(undoManager) && state1(undoManager) == state1(#getUndoManager_result) && ... but expected undoable(undoManager)
```
After:
```
State Refinement Error: found (#canRedo_result ? redoable(undoManager@70) : notRedoable(undoManager@70)) && undo(undoManager@70) == undo(#getUndoManager_result) && limit(undoManager@70) == limit(#getUndoManager_result) && (#canRedo_result ? undoable(undoManager) && notRedoable(undoManager) && phase(undoManager) == phase(#getUndoManager_result) && ... but expected undoable(undoManager)
```

`ErrorStateHintMultipleSets` with its sets named `doorState` and
`lockState` (rebased on #495, which leaves out the unrelated
`unlocked(d@26)`):
```
- found closed(d@26) && locked(d) && state1(d) == state1(d@26) but expected closed(d) && unlocked(d)
+ found closed(d@26) && locked(d) && doorState(d) == doorState(d@26) but expected closed(d) && unlocked(d)
```

New errors:
```
Error: State set name 'Door' must be an identifier that starts with a lowercase letter
Error: State set name 'locked' is already the name of a state of ErrorStateSetNameOfAState
Error: State set name 'lock' is already the name of a ghost of ErrorStateSetNameOfAGhost
Error: State set name 'door' is already the name of another state set of ErrorStateSetNameOfAnotherSet
Error: State set name must be a string literal
```

## Tests (each fails on main)
- `state_hint_study_undo_manager_correct`: an external spec with named
sets. `canUndo()` keeps its undo set by name (`undo(this) ==
undo(old(this))`) when it returns false. On main the name is unknown, so
this fails.
- `ErrorStateSetNames`: invalid name and clashes with a state, a ghost
and another set.
- `TestStateHints#foundKeepsANamedStateSetByItsName`: exact message with
`doorState(d)`.

Full suite passes locally (714 tests). The 6 study exercises and the 19
study variants give byte-identical output to main without names. With
names on every multi-set exercise spec, the verdict and line stay the
same.

## API release needed
`name()` is new in `liquidjava-api`. The in-repo api is still `0.0.7`,
which is already published without `name`. Reactor builds from the root
(CI and the shaded jar) use the in-repo module. A standalone build of
the verifier, or any user project (VS Code study projects included),
resolves the published `0.0.7`, where `@StateSet(name = ...)` does not
compile. Before anyone uses names: `./release.sh api` (→ `0.0.8`, which
also bumps the verifier/example dependency), then a verifier release.
Nothing is published in this PR.

## Notes
- `old` works on the receiver, as for every ghost: `undo(old(this))`.
`old(undo(this))` (the form in the issue) is not supported for any ghost
today.
- A `to` that only mentions the set function (e.g. `undo(this) == ...`
without any of its states) does not count as mentioning the set, so the
keep equality is still added (same as for `stateN` today).
- vscode-liquidjava (not changed here): `server/.../GhostDTO` marks
states with the regex `^state\d+\(_\) == \d+$`. States of a named set
would show as "ghost" in autocomplete and the context view. Use
`ghostState.getParent() != null` instead. Set names are not offered in
autocomplete, because `ContextHistory` only carries `GhostState`s. The
state machine view (liquidjava-fsm) reads `value` of the first
`@StateSet`, so it is unaffected (fsm#8 could use names as titles).

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

---------

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

Part of #502 (PR 1, the language). **Depends on #507 and #508.** Until
they are merged, this diff also shows their commits; only the last
commit belongs here.

## What

A spec can write a state as a value of its set:

```java
@stateset(name = "door", value = {"closed", "opened"})
@stateset(name = "lock", value = {"unlocked", "locked"})
...
@StateRefinement(from = "door(this) == closed && lock(this) != locked", to = "door(this) == opened")
void open();
```

`set(e) == state` means `state(e)`, and `set(e) != state` means
`!state(e)`, in either order. The old shorthand stays valid, and the two
can be mixed.

## How

`StateValues.toShorthand` rewrites the new form into the shorthand
**once, where the spec is parsed and in that spec's scope**. Everything
after that is unchanged, and that includes every part that reads states
syntactically: the frame equalities, the state machine, the hints,
`DecidingArgument`, `StateErrorCategories` and #495's relevance pass.
The parse sites are:
- `@Refinement`, via `getRefinementFromAnnotation`;
- method from/to, via `createStatePredicate`;
- constructor `to`, via `setConstructorStates`;
- alias bodies, at registration, where only the alias's parameters are
variables.

Every set is already registered when specs are parsed (#508), so there
is no late resolution, and a caller's variable can never capture a state
name.

**Scope rules** (from the #502 design reviews):
- A variable in scope keeps its meaning. That covers parameters, context
variables, and `_`, `this` and `return`, which are always variables.
Specs that are valid today mean the same.
- A name that is a state of *another* set of the class is an error:
`State 'locked' is not a state of 'door' (its states are closed,
opened)`.
- Only the sets that apply to the argument's type are considered, that
is, sets declared on its class or a supertype. The type comes from
`this`, `_`, a parameter, a context variable, `old(x)`, or an alias's
declared parameter type. When the type is known, any applicable set may
have the state, as with the shorthand. When it is unknown, every set of
that name must have it, and otherwise the name stays an unknown
variable. The rewritten state is named exactly as the shorthand written
in the same place (`a.Sub.door(this) == open` becomes
`a.Sub.open(this)`), so it is resolved the same way.

**Two new checks on `@StateSet`** (⚠️ breaking for specs that have this
ambiguity today: they are now rejected even if the ambiguous state is
never used), because `open(this)` must say which set it means:
- Two sets of one class may not share a state name: `State 'open' is in
two state sets of X: state1 and state2`. That was accepted before, and
the shorthand picked one set silently.
- The #498 name check now covers generated names, so a state called
`state1` next to the unnamed set `state1` is reported.

## Tests (each fails without the change)
- `CorrectStateValues`, written only in the new form: two named sets, a
constructor `to`, from/to, `!=`, a branch that keeps a set via `old`, a
parameter named like a state, an alias used next to a local variable
named like its state, and states named `_` and `return`.
- `ErrorStateValues`: the wrong-set error, a state name shared by two
sets, and a state named like a generated set.
- `TestStateHints#queryWrittenWithItsStateSetIsOfferedAsAGuard`: a query
written in the new form is still offered as a guard, so the state
machine reads it.

The full suite passes locally. Found while testing: #509, an existing
false error for a boolean query in an ordinary class, with either form.

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

---------

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

…#511)

Part of #502 (PR 2, messages). **Depends on #510**, which depends on
#507 and #508. Only the last commit belongs here.

## What

State errors show the states of **named** sets as values of their sets,
whichever form the spec used. `ErrorStateHintMultipleSets` (sets
`doorState` and `lockState`):

```
- found closed(d@26) && locked(d) && doorState(d) == doorState(d@26) but expected closed(d) && unlocked(d)
+ found doorState(d@26) == closed && lockState(d) == locked && doorState(d) == doorState(d@26) but expected doorState(d) == closed && lockState(d) == unlocked
```

It is now plain which set fails (only `lockState`), and the frame
equality chains on its own: `doorState(d) == doorState(d@26)` and
`doorState(d@26) == closed`.

`!open(x)` is shown as `door(x) != open`. A state keeps the shorthand
when its set has a generated name (`state2(x) == closed` reads worse
than `closed(x)`), or when sets with different names have a state of
that name. That way the set printed is never a guess.

## How

`StateValues.toSetForm` rewrites expressions for display only.
`StateRefinementError` receives it as `display`:
- **The facts to show are still chosen on the expressions as given.**
`linkedToExpected` and #495's relevance step run first. A shared state
name such as `closed`, which is a variable in the rewritten form, would
otherwise link facts about unrelated objects.
- The message, `getExpected()` and every derivation step
(`VCSimplificationResult.map`) hold the rewritten form, so the **IDE
shows it without a server change**: the server formats those expressions
as they are.

Nothing the verifier decides changes: the VC, the verdict, the hints and
the category are the same. Refinement errors (`RefinementError`) keep
the shorthand for now. They also build alias expansions and
counterexamples from the same expressions, so that would be its own
change.

`Formats.STATE_SET` names the generated `stateN`, which the display
needs to recognise.

## Tests
- `TestStateHints#foundKeepsANamedStateSetByItsName`: the message above.
It fails without the change.

The full suite passes locally.

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

---------

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