[CatarinaGamboa]

Closes #488

Where the name was lost

Both paths in the issue already kept the name up to VC simplification:

• the spec side (Predicate.resolveStaticFinalConstants) and the client side (RefinementTypeChecker.tryStaticFinalConstantRefinement, for a field read such as int mode = ImageWriteParam.MODE_EXPLICIT; or a call argument) both build an Enum node named ImageWriteParam.MODE_EXPLICIT that carries the value as its resolvedLiteral;
• the SMT translator encodes that node as a constant plus the axiom ImageWriteParam.MODE_EXPLICIT == 2.

The name was dropped by the folding pass of the simplification (VCFolding), which rewrote every resolved constant to its literal (// enum constant -> literal), whatever was around it. So Found, which is the simplified VC, showed mode == 2, while Expected, which is not simplified, kept the name.

Design

The AST already has a node that holds both name and value, so no new node or context equality is needed. The only change is when folding uses the value:

• VCFolding reads a constant's value only to fold the expression around it: a binary or unary expression whose operands are all literals or constants (MODE_EXPLICIT + 1 → 3, Integer.MIN_VALUE < 0 → true, -LIMIT), or a ternary whose condition is a boolean constant. In every other case the constant keeps its name (mode == ImageWriteParam.MODE_EXPLICIT). The constant is never rewritten to a bare literal on its own, so a derivation step never shows the value in place of a name the code wrote.
• Two constants are still compared by their values (before, they had already been turned into literals), so A.X == A.Y with both equal to 2 folds to true; the name-based rule Format.JPG != Format.PNG keeps applying to enums only.
• RefinementError.states (the counterexample filter) compares a constant in Found with its value in the model, so mode == ImageWriteParam.MODE_EXPLICIT does not also print Counterexample: mode == 2. This is a 3-line change in RefinementError; Restore alias expansion in refinement diagnostic history #295 (fix/295-alias-expansion) also touches this file, in other methods, so the two should merge cleanly.

Names come only from where the source wrote them: the node is built from the field read or the spec text, never from a value. Literals the code wrote stay numbers (requireKnownMode(2)), computed values become numbers, and the solver's counterexample values stay numbers. The SMT encoding is unchanged.

Before / after (CLI, java -jar liquidjava-verifier/target/liquidjava-verifier-0.0.36.jar <dir>)

Issue reproducer (direct() and throughLocal()):

before: Refinement Error: mode⁰ == 2 is not a subtype of mode⁰ != ImageWriteParam.MODE_EXPLICIT
        Refinement Error: mode¹ == 2 is not a subtype of mode¹ != ImageWriteParam.MODE_EXPLICIT
after:  Refinement Error: mode⁰ == ImageWriteParam.MODE_EXPLICIT is not a subtype of mode⁰ != ImageWriteParam.MODE_EXPLICIT
        Refinement Error: mode¹ == ImageWriteParam.MODE_EXPLICIT is not a subtype of mode¹ != ImageWriteParam.MODE_EXPLICIT

dcm4che study task (x_e_oss_a1_01_sliderecoder, package line stripped, so lines are one less than in the exercise) with wParam.setProgressiveMode(ImageWriteParam.MODE_EXPLICIT); after getDefaultWriteParam():

before: Refinement Error: mode³⁰⁶ == 2 is not a subtype of ImageWriteMode(mode³⁰⁶) && mode³⁰⁶ != ImageWriteParam.MODE_EXPLICIT
after:  Refinement Error: mode³⁰⁶ == ImageWriteParam.MODE_EXPLICIT is not a subtype of ImageWriteMode(mode³⁰⁶) && mode³⁰⁶ != ImageWriteParam.MODE_EXPLICIT

Unmodified task: unchanged before and after, State Refinement Error: found tilingNotExplicit(wParam³⁰⁵) && compressionNotExplicit(wParam³⁰⁵) but expected compressionExplicit(wParam³⁰⁵) || compressionTypeSet(wParam³⁰⁵) at line 131 of the exercise. With wParam.setCompressionMode(ImageWriteParam.MODE_EXPLICIT); added: Correct! Passed Verification. before and after.

Computed value, small(ImageWriteParam.MODE_EXPLICIT + 1) with @Refinement("_ < 3"), unchanged (the value is computed, so it is a number); small(ImageWriteParam.MODE_EXPLICIT - 1) passes:

before/after: Refinement Error: mode⁰ == 3 is not a subtype of mode⁰ < 3

Negative constant, the existing ErrorStaticFinalConstant (requirePositive(Integer.MIN_VALUE)):

before: Refinement Error: x⁰ == -2147483648 is not a subtype of x⁰ > 0
after:  Refinement Error: x⁰ == Integer.MIN_VALUE is not a subtype of x⁰ > 0

Tests

• TestStaticConstantNames + fixture ErrorStaticFinalConstantName: the issue's two shapes, asserting the message and that there is no counterexample. Both fail on main.
• VCFoldingTest: new keepsResolvedEnumNameWhenNothingFolds (fails on main); the two tests of resolved constants now expect the fold in one step (Config.LIMIT == 3 → true, Config.LIMIT + 2 == 5 → 5 == 5 → true) instead of an intermediate step showing the value.
• The existing constant tests (Add Constant Propagation And Folding To Predicates #58 folding, Verifier crashes when an enum (or class) constant is compared in an if #302, Constant accessed through a subclass gives "Sorts Int and Bool are incompatible" #305, Soundness: a local variable with a constant's name shadows the constant (Format.JPG read as local JPG) #321, Verifier crashes on a field or enum constant whose declaring class cannot be resolved #390, the *StaticFinal* fixtures, TestCounterexamples#staticFinalConstantHasNoCounterexampleBecauseValueIsAlreadyKnown) pass unchanged.

Full verifier suite locally: 702 tests, 0 failures.

🤖 Generated with Claude Code

[CatarinaGamboa]

Codex review, round 1

The changes preserve static constant names in unfolded expressions while still using their resolved values for folding and counterexample filtering. The targeted tests passed, and I found no actionable regression.

No findings, so nothing to fix; the review loop stops here.