Repository navigation
Found: rewrite facts through ghost equalities g(x) == g(x@k) so they are stated about x #501
Description
Problem
A state error's Found keeps every call's frame equality, g(x) == g(x@k), next to the facts about the older instance x@k. The reader has to chain them in their head to see what x is now:
found closed(d@26) && locked(d) && doorState(d) == doorState(d@26) but expected closed(d) && unlocked(d)
says "d is closed" in two steps. Written directly about d, the clash with Expected is plain:
found closed(d) && locked(d) but expected closed(d) && unlocked(d)
VCFunctionSubstitution already propagates f(...) == e, but only into later rows and only for an exact syntactic match. A state is written closed(d@26), not doorState(d@26) == 0, so it never matches and the equality stays.
Proposal: a general display step, rewrite through ghost equalities
Source equality. g(x) == g(y) where g is a ghost function (a state set, named or stateN, or any @Ghost such as size or r) with the same argument tuple shape, and either:
- the equality is a top-level conjunct of Found, in which case it rewrites across all of Found; or
- it sits inside a branch of
c ? … : …, in which case it rewrites only within that branch, and the guard stays. The equality is dropped only ifg(y)occurs nowhere outside that branch. Otherwise it stays: rewriting under an equality that holds is still exact, but eliminatingg(y)is not.
An equality under ||, !, or on the left of --> is never used.
Conditions on the eliminated term g(y):
-
Expected does not mention
g(y). -
Let the fresh variables be the argument variables of
g(y)that do not occur anywhere in the arguments ofg(x). Occurrence is by variable identity across the whole tuple, so a variable moved to another position is not fresh. There must be at least one fresh variable (sog(a,b) == g(b,a)is never eliminated). Every fresh variable has a class type, which Z3 encodes as an uninterpreted sort, and is never constrained as a value in Found or in Expected. No other application of the same SMT-resolved ghost in Found or Expected uses a fresh variable:g(y,b)next tog(x,a) == g(y,a)blocks it, becausea == bwould make the two the same application. The conditions are checked again before each step of a chain. That means noy == z, noyas an argument of an alias or of a non-ghost function, and noyin a ghost application whose arguments are not plain variables. This is the same guard as Add a Relevant to Expected step to state errors #495. Ghosts overboolean, enums,intor other interpreted or finite sorts are never eliminated. Facts about other ghosts ofy(h(y) == 1) may stay. -
Under 1 and 2, replacing every
g(y)(that exact application) byg(x)and dropping the equality is exact:Found' ⇒ Expectedis valid iffFound ⇒ Expectedis valid.- From a model of
Found' ∧ ¬Expected, build a model ofFound ∧ ¬Expected. Map each fresh variable to a fresh element of its sort. Give every ghost application involving those elements the value its original version had, and giveg(y)the value ofg(x). This is consistent because the tuple ofg(y)now contains a fresh element, so it differs from every other tuple ofg,g(x)'s included. That holds because no other application ofguses a fresh variable. Every fact keeps its truth value, because by condition 2 the fresh variables occur only as ghost arguments. The equality now holds, and Expected is unchanged. - The converse direction is substitution under the equality.
- A fresh element always exists for an uninterpreted sort. For a finite sort it may not: with
x == false,h(x) == 0 && h(y) == 1forcesy == truewithout ever comparingy. That is why condition 2 restricts the type.
When either condition fails, the equality and the facts stay as they are.
- From a model of
Rewrite. Replace every occurrence of the exact application g(y) (same qualified ghost, same full argument tuple) by g(x), including inside other equalities. So g(x) == g(y) && g(z) == g(y) && g(z) == 0 becomes g(z) == g(x) && g(z) == 0, and then g(x) == 0.
A state counts as an occurrence only if its refinement is exactly g(v) == k for this g, which is the form @StateSet gives (TypeChecker builds it). So closed(d@26) becomes closed(d). A state or alias with any other refinement is an argument of a non-ghost function, which condition 2 already excludes.
Direction. The kept term is the endpoint Expected mentions. Normally that is the newest instance, which keeps the target variable visible (#374). If Expected mentions both endpoints, the equality joins two terms it sees, so it stays. If Expected mentions neither, keep the newer instance (x over x@k; a variable over a generated #…_result).
Rows. The display chain scopes variables by row. Each rewritten fact goes in the latest of its original row and the rows binding each of its variables, so x and any other variable it mentions are in scope. A fact whose row already binds all of them stays where it is.
Interaction with VCFunctionSubstitution. That pass consumes g(x) == g(y) in the opposite direction: it rewrites later rows from g(x) to g(y) and drops the equality. Running this pass first is not enough, because an equality this pass declines (for example g(x) == g(y) && y != z) would still be consumed there. Main can then already print y != z && g(y) == 1 for an Expected g(x) == 1, which no longer shows the link. So for state errors, VCFunctionSubstitution skips every equality between two ghost applications, and this pass is the only one that rewrites through them. Guards are checked against the ghost application that actually resolves in SMT (resolveFunctionDecl falls back to the simple name).
Termination. Each step removes the term g(y) from Found, so the steps stop.
Like the other steps, this only affects what is displayed: the solver's VC is unchanged and the original Found stays as the previous step. State errors only, until it is checked against the counterexamples of refinement errors.
A side effect: a frame equality whose g(y) has no other fact, and whose y meets condition 2, disappears outright. In ErrorTrafficLightRGB, r(tl) == r(tl@48) && g(tl) == g(tl@48) && b(tl) == b(tl@48) only says "the colour values were kept" and goes away.
Where it shows
ErrorStateHintMultipleSets: as above.- Study A1_56 (undo manager):
undo(undoManager@70) == undo(#getUndoManager_result),limit(...) == limit(...),phase(...) == phase(...)chains through every call. E_A3_07scanner,ErrorArgumentPicksTheStateEarlier:state1(param) == state1(param@25)next totilingOff(param@25).
Relation to other work
- Add an expected-guided simplification step to state error derivations #297 / Add a Relevant to Expected step to state errors #495 (Relevant to Expected): the two are complementary. Run this rewrite first, then the relevance step on its result.
- Named state sets, so a spec can refer to a whole set (e.g. old(phase(this))) #435 / Named state sets: optional name on @StateSet #498 (named sets): makes the equalities readable, and this step removes most of them.
- The state-to-set lookup is the one Add a Relevant to Expected step to state errors #495 adds (
ghostFunctionsOf), so it can be shared.
Tests (lean), each failing without its rule:
- a message test on
ErrorStateHintMultipleSets; - unit tests for a two-step chain; a declined equality that
VCFunctionSubstitutionmust keep; an equality inside one branch that must not rewrite outside it;y == zblocking the elimination; and a ghost over abooleanargument that is not eliminated; a permuted tupleg(a,b) == g(b,a)that is kept; andg(x,a) == g(y,a) && a == b && g(y,b) == 1that is kept.
Activity
CatarinaGamboa commentedon Nov 6, 2026
Codex review of the design, round 1 (soundness)
Codex found that the rule as first written was unsound. All five findings were real, and the issue body is now amended:
(c ? g(x) == g(y) : true) && g(y) == 1, Expectedg(x) == 1g(y)occurs nowhere else. Never use equalities under||,!or-->.yhas value factsg(x) == g(y) && y == z, Expectedg(x) == g(z)yis never constrained as a value (the same guard as #495). Under it, dropping is existential elimination ofg(y)and is exact.g(x) == g(y) && g(z) == g(y) && g(z) == 0S(v) = g(v) == 0 && h(v) == 1g(v) == k.g(y)into a row beforex's binder;VCFunctionSubstitutionconsuming the equality in the opposite directionVCFunctionSubstitution, or that pass skips ghost-to-ghost equalities.Codex: "The design is sound once amended". Next round checks the amended text.
CatarinaGamboa commentedon Nov 6, 2026
Codex review of the design, round 2 (soundness): one real gap, amended
Codex found that the round 1 argument was wrong. It treated
g(y)as an independent value, but Z3 sees a function applied toy. Over a finite sort, other facts can fixywithout ever comparing it as a value:x == false && z == true && h(x) == 0 && h(y) == 1 && g(x) == g(y), Expectedg(x) == g(z). Withbooleanarguments,h(y) != h(x)forcesy == z, so the original proves Expected. Dropping the equality loses that.x == false && z == true && g(false,false) == 0 && g(true,true) == 0 && g(x,z) == g(y,y), Expectedg(x,z) == 0. A repeatedbooleanargument does the same.Amended (condition 2 and the proof in condition 3). Every argument of
g(y)not shared withg(x)must have a class type, which Z3 encodes as an uninterpreted sort. Ghosts overboolean, enums,intand other interpreted or finite sorts are never eliminated.The proof: from a model of
Found' ∧ ¬Expected, moveyto a fresh element, copy its ghost values, and setg(y) := g(x). That gives a model ofFound ∧ ¬Expected. This construction is exactly what fails for a finite sort, where a fresh element need not exist. State sets and object ghosts, the use case of this issue, all take a class-typed object. Abooleantest was added to the test list.CatarinaGamboa commentedon Nov 6, 2026
Codex review of the design, round 3 (soundness): proof holds, two fixes to the display chain
Codex found no counterexample to the fresh-element proof for class-typed arguments. It checked the uninterpreted sort per class, the type views of one reference (it found the axioms that keep them in sync, and they can be given fresh elements together), static constants and enum sorts. It found no cardinality or range axiom on state sets.
Two gaps in how the rewrite fits the display chain, both amended:
g(x) == g(y) && y != z, theng(x) == 1in a later row, with Expectedg(x) == 1. This pass declines (yis compared as a value), butVCFunctionSubstitutiondrops the equality anyway and printsy != z && g(y) == 1. That is an existing display problem on main. Amended: in state errors,VCFunctionSubstitutionskips equalities between two ghost applications, and this pass is the only one that rewrites through them.g(y) == h(z)tog(x) == h(z)and moving it into the equality's row can put it beforez's binder. Amended: each rewritten fact goes in the latest of its own row and the binder rows of all its variables.Codex: "The design is sound once both amendments above are made". Next round checks the amended text.
CatarinaGamboa commentedon Nov 6, 2026
Codex review of the design, round 4 (soundness): permuted tuples, amended
Codex confirmed that the round 3 amendments (
VCFunctionSubstitutionskipping ghost-to-ghost equalities, and the row placement) fix their problems. It found one more case:g(a,b) == g(b,a) && a == c && b == d && g(d,c) == 1, Expectedg(a,b) == 1, all class typed. Every argument ofg(b,a)also occurs ing(a,b), so no variable could be moved to a fresh element and condition 2 guarded nothing. Dropping the equality loses the step fromg(d,c)tog(a,b).Amended (condition 2 and the proof in condition 3). The fresh variables are the argument variables of
g(y)that occur nowhere ing(x)'s arguments, compared by identity across the whole tuple. There must be at least one, and each must be class typed and never constrained as a value. The proof moves them to fresh elements, so the tuple ofg(y)differs from every other tuple. A permuted-tuple test was added to the list.For the single-argument state sets and object ghosts this issue targets,
yitself is the fresh variable, so nothing changes for them.CatarinaGamboa commentedon Nov 6, 2026
Codex review of the design, round 5 (soundness): another multi-argument case, amended
g(x,a) == g(y,a) && a == b && g(y,b) == 1, Expectedg(x,a) == 1, all class typed.yis fresh, buta == bmakesg(y,a)andg(y,b)the same application. Movingyto a fresh element does not separate them, so dropping the equality loses Expected.Amended (condition 2). No other application of the same SMT-resolved ghost may use a fresh variable, and the conditions are checked again before each step of a chain. This guard is conservative. For the single-argument state sets and object ghosts this issue targets it never blocks anything, since the only application of
goveryisg(y)itself.Codex: "With this additional guard, I found no further counterexample to successive elimination, branch scoping, or row placement." One confirming round follows.
CatarinaGamboa commentedon Nov 6, 2026
Codex review of the design, round 6 (confirming): no new findings
Codex: "The amended display rewrite is sound and sufficiently specified to implement against the current code."
It wrote out the model construction for the general multi-argument case and confirmed:
g(y)as the only tuple that needs a new value, namely that ofg(x).g(y)occurs outside the branch. Row placement keeps every variable in scope.It also confirmed that skipping ghost-to-ghost equalities in
VCFunctionSubstitutionfor state errors is necessary.Six rounds in total; the design is settled. Implementation notes: guards are checked against the SMT-resolved ghost, and the tests are the lean list in the issue body.