Skip to content

Add an expected-guided simplification step to state error derivations #297

New issue
New issue
Open
#495
Open
Add an expected-guided simplification step to state error derivations#297
#495
Labels
studyNeeded before the error-message user study

Description

@CatarinaGamboa
CatarinaGamboa
opened on Sep 24, 2026

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:
Image

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 study
    on Nov 6, 2026

  2. CatarinaGamboa commented on Nov 6, 2026

    @CatarinaGamboa
    CatarinaGamboa
    on Nov 6, 2026
    CollaboratorAuthor

    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
    CatarinaGamboa
    on Nov 6, 2026
    CollaboratorAuthor

    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.

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

Metadata

Metadata

Assignees

No one assigned

    Labels

    studyNeeded before the error-message user study

    Type

    No type

    Projects

    No projects

      Milestone

      No milestone

      Relationships

      None yet

      Development

      No branches or pull requests

      Issue actions