Description

CatarinaGamboa

opened on Sep 24, 2026

Issue body actions

Problem

The final Found step in a state error can contain facts from state sets unrelated to Expected. The user must identify the relevant fact and trace version equalities manually.

Current example

The last simplification step for preview.setTiling(...) is:

Expected concerns the tiling state of preview³⁰⁴. The relevant startTiling(preview²⁹⁹) fact and the version link are present, but compression facts remain in the final explanation.

Desired behavior

Append a step labeled “Relevant to this requirement” after the existing simplification steps when the verifier can safely produce one. In this example, it should retain startTiling(preview²⁹⁹) and the equality needed to relate its tiling state to preview³⁰⁴. It should omit compression facts only if their independence from this requirement has been established. The back arrow should return to the full step shown above.

This is a simplification step in the error display. It must not change the verification condition checked by the solver or the verification result.

Implementation direction

1. Give the new pass both Expected and the simplified Found expression. VCChecker.throwStateRefinementError has both when it constructs the error.
2. Use expression and state set information to identify the receiver, relevant state set, and necessary version equalities.
3. Remove a clause only when its independence has been established. Keep clauses whose role is uncertain.
4. Append the result to the derivation history with the metadata needed for source links and backward navigation. Do not infer dependencies from rendered names.

Acceptance criteria

• The scanner error gains a final “Relevant to this requirement” step showing the startTiling fact and every necessary version link.
• Proven independent compression facts are omitted; uncertain facts remain.
• The existing full step remains available through the back arrow.
• No step is added when safe cleanup cannot be established.
• Verification results do not change.

Activity

1. CatarinaGamboa

   added

   studyNeeded before the error-message user studyNeeded before the error-message user study

   on Nov 6, 2026
2. CatarinaGamboa commented on Nov 6, 2026

   

   CatarinaGamboa

   on Nov 6, 2026

   CollaboratorAuthor

   More actions

   Two more examples from the error-message study, run on current main (ae278d2).

   A1_56 after a partial fix (only redo() guarded)

   CountingUndoManager undoManager = frame.getUndoManager();
   switch (action) {
       ...
       case REDO -> {
           if (undoManager.canRedo()) undoManager.redo();
       }
       case UNDO -> undoManager.undo();   // error here

   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) && limit(undoManager) == limit(undoManager@70) : (#canRedo_result ? redoable(undoManager) : notRedoable(undoManager)) && state1(undoManager) == state1(#getUndoManager_result) && state2(undoManager) == state2(#getUndoManager_result) && limit(undoManager) == limit(#getUndoManager_result)) but expected undoable(undoManager)
   

   Expected concerns only the undo state set (state1), but Found keeps the frame equalities for the redo state set (state2(...) == state2(...)) and for limit(...). It also shows internal names for call results, #canRedo_result and #getUndoManager_result, which the message does not explain.

   Part of this example is caused by a different problem: switch cases are not modelled separately. The REDO case's effects reach the UNDO case, which is where #canRedo_result and undoManager@70 come from (a separate issue is being filed for this). These facts all depend on the same #canRedo_result condition, so this issue's pass cannot drop the state2/limit facts on its own. For that reason, the main target is the scanner example below.

   E_A3_07 (the scanner/preview example from this issue)

   State Refinement Error: found startTiling(preview@53) && state2(preview@53) == state2(preview@52) && compressionSet(preview) && state1(preview) == state1(preview@53) but expected tilingExplicit(preview) || tilingSet(preview)
   

   Here no switch or condition is involved: state2/compressionSet belong to the compression state set and share no term with the tiling state set that Expected names. The relevant step should be startTiling(preview@53) && state1(preview) == state1(preview@53).

   Internal #<method>_result names

   Advisor rule: if users are not told what something means and it does not make sense to them, do not show it. Proposal: write a refined call result as the call itself (undoManager.canRedo(), frame.getUndoManager()) wherever it reaches the shown Found. This changes how names are displayed (DisplayNames/translation table), and it applies to refinement errors too, not only to this state-error step. So I am leaving it out of this issue and suggest it as a follow-up. The same rule applies to the state1/state2 names of frame equalities, which are also never explained.
3. CatarinaGamboa commented on Nov 6, 2026

   

   CatarinaGamboa

   on Nov 6, 2026

   CollaboratorAuthor

   More actions

   Following PM feedback, the step is now labelled Relevant to Expected instead of "Relevant to this requirement" (#495). The label is the step's simplification name, which the server already sends to vscode.
4. CatarinaGamboa

   closed this as completedin #495on Nov 9, 2026

Issue actions