[CatarinaGamboa]

Stacked on #531 (base feat/found-fold-decided-ternary). Part of #523: the last step of folding A1_09's Found.

What

After #531 folds A1_09's ternary under newMode == BORDERLESS, the ternary no longer mentions newMode, yet Found still shows newMode == BORDERLESS. The cause is in Relevant to Expected (VCRelevantFacts.addSymbols, VCRelevantFacts.java:125 on #531): every Var is a symbol, and an enum constant read in code is a Var named DisplayMode.BORDERLESS. So newMode == BORDERLESS and the folded ternary stay linked through the constant. (An enum constant written in a refinement is an Enum node, which already linked nothing.)

A constant is a fixed value: two facts that only compare values with the same constant share no unknown. The relevance pass now ignores enum constants as symbols, except when a function or alias takes the constant, or a value one takes is compared with it. There, equality through the constant does relate facts (x == A && state(A) == shown gives state(x) == shown). This exception comes from Codex's round-1 counterexample.

• VCRelevantFacts takes the enum constants of the chain. VCKnownEnumValues.enumConstants exposes the set Fold ternaries that a fact of Found decides on an enum value #531 already builds.
• There is still one relevance run and no new pass. The step order is unchanged: Substitution, Function Substitution, Binder, Known Enum Values, Folding, Arithmetic, Logical, Constraint to a fixed point, then Relevant to Expected once, then ErrorMessage's fact selection.

Soundness

Display only; the verdict is unchanged. The relevance pass drops only facts D whose unknowns are disjoint from Expected's and from the kept facts S. Enum constants are distinct EnumSort values. When no function takes a value equal to a shared constant, a model of S and a model of D combine. So the premises imply S, and S fails Expected exactly when the premises do. static final constants are not in the set.

A1_09 (the only study task that changes)

#531:  found newMode == BORDERLESS && (previousMode != BORDERLESS ? display(host) == notDisplayable : display(host) == displayable) but expected display(host) == notDisplayable
this:  found previousMode != BORDERLESS ? display(host) == notDisplayable : display(host) == displayable but expected display(host) == notDisplayable

The other seven study tasks have the same output as on #531, byte for byte, with one error each on reportedLine. All 287 testSuite fixtures have the same headlines as on #531.

The formatter writes a Found that is a single ternary without parentheses, as in #531's FULLSCREEN case. That is outside this PR.

Tests

• VCSimplificationTest#relevantStepDoesNotLinkFactsThroughAConstant (fails without the change).
• VCSimplificationTest#relevantStepLinksFactsThroughAConstantAnObjectEquals (Codex's counterexample; fails with the naive "drop every constant" version).
• mvn test: 735 tests, 0 failures.

🤖 Generated with Claude Code

[CatarinaGamboa]

Codex design review

Sent the comparison of #529 and #531, the cause, the change and its soundness argument, and asked Codex to break it.

Round 1: DISAGREE

(The first draft dropped every enum constant from the symbols. Codex read the file while a temporary // X from my fail-without-the-fix check was in it. Its counterexample is valid regardless.)

The intended change has a blocking counterexample. Let Mode.A be an enum constant, and let state be a ghost function over Mode:

Found:    x == Mode.A && state(Mode.A) == shown
Expected: state(x) == hidden

The premises establish state(x) == shown. With Mode.A removed from every symbol set, VCRelevantFacts keeps x == Mode.A because it links to state(x), but drops state(Mode.A) == shown: its application is reduced to the removed constant symbol. StateRefinementError.java then rejects the remaining fact as having no ghost application, producing “expected state(x) == hidden but could not prove it.” The fact explaining the failure has disappeared. The same problem occurs for an unknown function applied to Mode.A. Equality with a fixed constant can connect applications at x and at that constant, so the proposed disjoint-symbol argument does not hold.

As checked out, the diff does not implement the removal: VCRelevantFacts.java still has // X. The focused test fails: it expected the first fact to be dropped but still got n == Photo.

For the other cases: a resolved-literal Enum node already contributes no variable name; an enum absent from the chain’s binders is left untouched; and x == y retains both variable symbols. Simple-name collisions deserve a separate test because the collected names use EnumSimpleName.CONST, even across packages. None removes the function-application counterexample.

I would keep ErrorMessage’s linkedToExpected from globally ignoring enum constants for the same reason. A smaller fix is to remove a specific redundant enum path equality from the headline after folding, only when its variable and constant have no remaining application or equality dependency. PR 529’s guarded, later display fold is worth retaining as a model for that decision; the reported literal probes do not establish a benefit from adding literal folding now.

DISAGREE — removing enum constants from all relevance symbols can hide the ghost-function fact that explains a state error.

Fixed: a constant stays a symbol when a function or alias takes it, or when a value one takes is compared with it. Its counterexample is now the test relevantStepLinksFactsThroughAConstantAnObjectEquals.

Round 2: AGREE

No new blocking objection to the revised change. I reviewed the uncommitted diff without editing the checkout or running Maven.

The cases you named behave as intended under the revised rule:

• Variables inside alias arguments enter objects, including constants represented as Var nodes. Comparisons with those objects keep the relevant constant symbol.
• For mode(o) == A and mode(p) == A, a Var-represented A remains a symbol because each comparison contains a function argument. This can retain an unrelated fact, but it is conservative and was possible before this revision.
• In x == (c ? A : B), the equality walk sees variables in both branches and the condition. Negation does not hide x == A, because the walk descends through !.
• notDisplayable is a Var when shown as a state-set value, but it is absent from the enum-constant set, so this change does not remove it. A tracked field path is likewise a variable name distinct from an enum constant.
• The “every fact or none relevant” guard leaves the chain unchanged. appliesGhost can still choose “could not prove it” when the facts selected for the headline contain no function invocation.

There is a pre-existing limitation worth recording. For a two-value enum {A, B}, x != A and state(B) == shown imply state(x) == shown, since Z3 uses a finite enum sort. The relevance graph does not link A to B, so it can omit the state fact and produce a less informative headline for an error expecting a different state. The revised constant removal does not cause that omission: the old graph also had no link between the two distinct constants.

A Found that is a single ternary reading found a ? b : c but expected d is a framing/formatter issue outside this change.

AGREE

[CatarinaGamboa]

Clean-code review

I audited this PR's diff against the clean-code principles (SOLID, DRY, KISS, YAGNI, naming).

Fixed

• core-dry: VCRelevantFacts needs the enum constants that VCKnownEnumValues already collects. I extracted enumTypesOf and exposed VCKnownEnumValues.enumConstants, so the set is built in one place. The field became final and is assigned once.
• name-meaningful: the set of constants that relate no facts is named valueConstants, to set it apart from all constants, and symbolsOf says that it leaves them out.

Declined

• func-few-arguments: symbolsOf now takes three parameters. valueConstants depends on the facts of each apply call, so it is passed in rather than stored in a field, which keeps the pass stateless.
• core-dry: addArguments has two near-identical branches, for FunctionInvocation and AliasInvocation. They share no interface for getArgs(), and adding one would grow this PR.
• core-kiss: removeComparedWithObjects is conservative. It keeps every constant of a comparison that mentions an object anywhere, for example mode(o) == A. That can keep an unrelated fact, as before this PR, but it never drops a needed one.

[CatarinaGamboa]

Codex review, round 1

codex exec review --base origin/feat/found-fold-decided-ternary:

No actionable regression was found in the changed code. The targeted VCSimplificationTest suite passes.

Nothing to fix, so no further rounds.