Skip to content

Fold a state error's Found under the constants its path conditions state - #529

Closed
CatarinaGamboa wants to merge 2 commits into
mainfrom
fold-state-found
Closed

Fold a state error's Found under the constants its path conditions state#529
CatarinaGamboa wants to merge 2 commits into
mainfrom
fold-state-found

Conversation

@CatarinaGamboa

@CatarinaGamboa CatarinaGamboa commented Nov 10, 2026 •
edited
Loading

Copy link
Copy Markdown
Collaborator

Closes #522, part 5 of 5: A1_09's nested if-then-else Found, folded under the shown path condition. Design: #522 (comment)

What it does

A new pass, VCPathFolding, runs once on the shown Found of a state error, after VCRelevantFacts:

  1. It collects the facts x == c that the chain states. c is a literal (int, long, real, boolean, char), an Enum node, or a Java enum constant. A Java enum constant enters the VC as a variable named Type.CONST; it counts as a constant only when the unsimplified chain binds it with an enum type that declares that constant.

  2. In the conditions of the chain's if-then-else facts, it writes c for x. It then folds the condition with the existing VCFolding/VCLogicalSimplification, plus A == B/A != B between two such enum constants (distinct values of a datatype).

  3. A branch is dropped only when its condition folds to true or false. Otherwise the ITE stays, with its simplified condition. No SMT check is used.

  4. VCChecker keeps the fold only if every fact of the unfolded shown Found that has no if-then-else is still shown. Otherwise, when a settled branch would make the headline drop the path fact that chose it (mode == A), it shows the unfolded Found.

Why it is sound: every fact of the premise chain holds wherever the others are checked. Writing c for x where x == c is a premise keeps Found equivalent, and the fact x == c itself stays. The chain the pass gets has no Expected node (joinPredicates clones it before appending Expected), so nothing is assumed from Expected.

The pass is a normal simplification step ("Path Folding"), so the panel's steps can show it.

A1_09, before and after

-State Refinement Error: found newMode == BORDERLESS && (previousMode == BORDERLESS && newMode != BORDERLESS ? display(host) == notDisplayable : (previousMode != BORDERLESS && newMode == BORDERLESS ? display(host) == notDisplayable : display(host) == displayable)) but expected display(host) == notDisplayable
+State Refinement Error: found newMode == BORDERLESS && (previousMode != BORDERLESS ? display(host) == notDisplayable : display(host) == displayable) but expected display(host) == notDisplayable
  • This is the review's mock-up, with otherwise left to the panel rows (extension side).
  • The other seven tasks are byte-identical. Each still gives exactly one error, on its reportedLine.
  • Every state-error fixture of the suite gives the same headline as before.

Test

TestFoundBinders.stateFoundFoldsTheBranchesItsPathConditionRulesOut, on a new fixture shaped like A1_09: ErrorStatePathFolding.java, an enum mode with a two-arm if/else-if and a switch case. No existing fixture has a path-condition constant inside an ITE. The test fails without the change.

mvn test: 730 run, 0 failures.

Conflicts

🤖 Generated with Claude Code

@CatarinaGamboa @claude
Fold a state error's Found under the constants its path conditions state
35f7c0a 
The conditions of the conditional facts of a state error's Found are
written with c for x wherever Found states x == c, for a literal or an
enum constant, and folded; a branch is dropped only when its condition
folds to a constant that rules it out. Found stays equivalent, and the
fact x == c stays. A1_09's nested if-then-else becomes
newMode == BORDERLESS && (previousMode != BORDERLESS ? ... : ...).

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
@CatarinaGamboa

CatarinaGamboa commented Nov 10, 2026

Copy link
Copy Markdown
Collaborator Author

Clean-code review

I audited the diff with the clean-code-principles checklist.

Fixed, while writing it:

  • [core-dry] Folding reuses VCFolding and VCLogicalSimplification, run to a fixed point on the condition, instead of a second set of folding rules. The only new rule compares two enum constants that enter the VC as variables, which neither pass can know about.
  • [core-fail-fast] The enum constants come from the chain before binder simplification. My first version looked at the simplified chain, where the DisplayMode.BORDERLESS binder was already dropped, so it silently did nothing. A1_09 showed that before I pushed.
  • [solid-ocp] It is a separate VCSimplificationPass. The existing passes are unchanged, and only state errors run it.

Declined:

  • [func-few-arguments] foldConditions(expression, constants, enumConstants) passes the enum set down the recursion. A field would do the same (the constructor already keeps it), but constants is per chain, so both stay parameters, alike.
  • [solid-srp] Constant collection, substitution and folding are in one 150-line class. Each step is one private method, and splitting them across classes would scatter a single rule.

@CatarinaGamboa @claude
Keep a state Found unfolded when folding would hide a fact it showed
3a963d4 
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
@CatarinaGamboa

CatarinaGamboa commented Nov 10, 2026 •
edited
Loading

Copy link
Copy Markdown
Collaborator Author

Codex review, round 1

codex exec review: "I found no actionable bugs in the diff."

Soundness prompt. It found a real gap. Once a fold removes the last condition that mentions x, the headline's relevance filter (linkedToExpected) also drops the fact x == c that chose the branch:

Program This PR (before the fix) main
DroppedEnumGuard found phase(cell) == b but expected phase(cell) == a found mode == A && (mode == A ? phase(cell) == b : phase(cell) == a) but …
DroppedIntGuard found phase(cell) == b … found n == 1 && (n == 1 ? … : …) …
DroppedBooleanGuard found phase(cell) == b … found flag == true && (flag == true ? … : …) …
NestedEnum found flag ? phase(cell) == b : phase(cell) == a … found mode == A && (flag ? (mode == A ? …) : (mode == B ? …)) …

The shorter headline is still a fact the verifier knew (S1), but the path condition that explains the branch disappears. That is not "folded under the shown path condition".

Fixed in "Keep a state Found unfolded when folding would hide a fact it showed". VCChecker keeps the fold only if every fact of the unfolded shown Found that has no if-then-else is still shown after folding. Otherwise it shows the unfolded Found.

  • All four programs now print main's headline.
  • A1_09 and the new fixture still fold. There the path condition newMode == BORDERLESS stays shown after the fold.

Tests: 730 run, 0 failures.

@CatarinaGamboa

CatarinaGamboa commented Nov 10, 2026 •
edited
Loading

Copy link
Copy Markdown
Collaborator Author

Codex review, round 2

Soundness prompt. Eight new programs, built and compared with origin/main: ints, chars, longs, booleans, static final constants, switch, nested ifs, loops, an enum from another file, and an equality inside Expected. It found no incorrect Found headline and no dropped reachable branch.

  • One program folds further than main, correctly: second == ONE rules out a first == ONE && second == TWO arm.
  • The Expected equality is not used to fold, as intended.

codex exec review:

[P2] Preserve path facts when folding the last conditional. When a path equality settles every conditional on its variable, the folded fact no longer mentions it, linkedToExpected drops the equality, and keepsShownFacts falls back to the unfolded Found (e.g. mode == ON && (mode == ON ? … : …)).

Declined for this PR. It is the round 1 fix working as designed: when keeping a fold would hide the path fact, we show the unfolded Found, which is sound and complete. Keeping a settled path fact visible needs ErrorMessage's fact selection (linkedToExpected) to treat facts used by a fold as linked. That is shared by every error message and touched by #520. A1_09, the case this PR is for, still folds: its newMode == BORDERLESS stays shown after the fold. I'll list it as a follow-up.

This ends the Codex loop for this PR: nothing relevant is left.

This was referenced Nov 10, 2026
Closed
Merged
Merged
CatarinaGamboa added a commit that referenced this pull request Nov 11, 2026
@CatarinaGamboa @claude
Mark code in every message with backticks, and name the lines they re…
cfe9405 
…fer to (#533)

Closes #532. **Stacked on #530** (→ #528 → `main`). Retarget it to
`main` before #530 is merged with `--delete-branch`.

Every message that shows code now marks it with backticks, inside the
message string:
- headlines (`found … but expected …`, `expected … but could not prove
it`);
- hints;
- origin notes;
- the declared-here gloss (`where … means …`);
- alias `where` lines;
- counterexamples.

## How each client sees it
- **Plain text** (`getMessage()`, `getMessageNotes()`, `Hint.message()`,
`getCounterexampleStr()`, `getDeclarationNotes()`, and so the Problems
tab and the hover): the string with backticks, as rustc writes its
messages.
- **CLI:** each span in blue (the existing `Colors.BLUE`), without
backticks. The backticks stay when colour is off: `NO_COLOR` set
(https://no-color.org) or no console (output piped or redirected). The
colour switch applies to code spans only; the CLI's other colours are
unchanged.
- **IDE:** the same backticked strings, plus
`LJDiagnostic.getReferences()`, a `List<SourceReference>` with one entry
per line reference. See below.

**Escaping:** `Code.of` fences code that holds backticks with a longer
run, and pads it with one space on each side when it holds a backtick or
starts or ends with a space: ``` `` c == '`' `` ```. `Code.render`
strips exactly that padding, so it shows any non-empty code exactly as
marked.

## Source references (for vscode-liquidjava#192)
`record SourceReference(String message, String text, int start, String
file, int line, int column)`:
- `message`: the whole message line it belongs to, exactly as
`getMessageNotes()` or `Hint.message()` gives it;
- `text`: the words of `message` that name the place, e.g. `line 134` or
`ArrayListRefinements.java:162`;
- `start`: where `text` starts in `message`, as a UTF-16 index (a
Java/JS string index), so `message.substring(start, start +
text.length())` is `text`. Use it instead of searching, because the code
of a call can hold the same words (`d.lock("line 18")` on line 18);
- `file`: the absolute path; `line`, `column`: 1-based, from Spoon.

Who carries one:
- every origin note: the call, parameter, constructor or
return-refinement declaration it names;
- the deciding-argument hint (`… on line 20 decides …`), through the new
`Hint.reference()`, which is null for other hints.

`getReferences()` returns the notes' references first, then the hints'.

## Before → after (CLI piped, so backticks shown)
```text
A1_38  State Refinement Error: found `stream(buffered) == open && markState(buffered) == unmarked` but expected `markState(buffered) == marked && stream(buffered) == open`
         Origin: line 134, `new BufferedInputStream(stream)` makes `markState(buffered) == unmarked`
         - Call `buffered.mark(int)` before this call; afterwards `markState(buffered) == marked`
         where `marked(this)` means `markState(this) == marked`, `open(this)` means `stream(this) == open`
A1_01    Origin: line 130, `writer.getDefaultWriteParam()` returns `compression(wParam) == compressionNotExplicit`
         - Call `wParam.setCompressionMode(ImageWriteParam.MODE_EXPLICIT)` before this call; afterwards `compression(wParam) == compressionExplicit`
A2_04  Refinement Error: expected `timeout >= 0` but could not prove it
         Origin: line 94, `timeout` is a parameter of `checkCimReachable(String, int)` with no refinement
          --> Counterexample: `timeout == -1`
A1_56    Origin: line 69, `frame.getUndoManager()` says nothing about `redoState(undoManager)`
         - Guard this call with `if (undoManager.canRedo())`; inside it, `redoState(undoManager) == redoable`
A2_10  Refinement Error: found `failures.size() == size(this.failures) && failures.size() >= 0` but expected `failures.size() > 0`
         Origin: ArrayListRefinements.java:162, `failures.size()` guarantees only `failures.size() >= 0`
```
For all eight tasks (six study tasks and both practice tasks), the
output with backticks removed is byte-identical to #530's. Each task
still gives exactly one error, on its `reportedLine`. On a terminal the
spans are blue and the backticks are gone. With `NO_COLOR=1` the
backticks stay.

## Changes
- `Code` (`of`, `render`), `SourceReference`, and `Colors.enabled()`.
- `LJDiagnostic`:
  - `addMessageNote(SourceReference)` and `getReferences()`;
- `toString` renders the message, notes, counterexample, hints and
declaration notes.
- Marked at the leaves where messages are built:
  - `ErrorMessage` (both headline frames);
  - `RefinementError` (counterexample, alias lines);
  - `AuxStateHandler.addMeanings` (gloss);
- `StateHints`: each state name, call, receiver and constructor, with
the prose words `or`, `and`, `then`, `with` left unmarked;
  - `OriginNotes`/`StateOrigin`, whose notes are now `SourceReference`s.
- `NotFoundError` marks the missing name and the suggestion (``Alias
`Positiv` could not be found``, ``Did you mean `Positive`?``).
- Not marked: the other error kinds (state conflicts, syntax errors) and
warnings, which the issue does not list. They are a follow-up if wanted.

## Tests
- 59 existing expectations gained backticks. Each change was made by a
script that accepts a new string only if removing its backticks gives
exactly the old one.
- `TestStateHints.assertHints` compares kind and message.
- New tests, each failing without the change:
  - `CodeTest` (fence, colour on and off);
  - `TestOriginNotes.noteNamesTheLineOfTheCallForClientsToLinkTo`;
  - a reference check in the deciding-argument hint test.

`mvn test`: 740 run, 0 failures.

## Conflicts
- **#524 and #525 are merged**, and this branch sits on top of them (via
#528's rebase), so it does not conflict with them. The lines of their
code it changes are:
- `StateHints.java`, on main: the hint templates at 116–119, 131–132,
182–184, 234, 239–240, 249, 252, 258, 260, 269, 295–297, 301, 303–305,
349, and `stateName` at 387–389;
- `RefinementError.java`, on main: 71 (counterexample) and 123 (alias
`where` lines);
  - `ErrorMessage.java` 39–41 (headline);
  - `AuxStateHandler.java` 865–866 (gloss).
- With the #529 agent's work: both may touch
`VCChecker.throwStateRefinementError`. This PR changes only the notes'
parameter type there.

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

---------

Co-authored-by: Claude Opus 5.5 <noreply@anthropic.com>
@CatarinaGamboa

CatarinaGamboa commented Nov 11, 2026

Copy link
Copy Markdown
Collaborator Author

Fixed in another stack

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

Say where the wrong state or value comes from (From note), and counterexamples for state errors

1 participant

@CatarinaGamboa