Certora ghost havoc'd despite init_state axiom: the axiom only constrains the constructor state

Symptom: a Certora ghost declared as

ghost mathint listingUpdatesCount { init_state axiom listingUpdatesCount == 0; }

is reported as HAVOC with an impossible value (e.g. 1) in a counterexample, even though hooks only ever increment and decrement it in pairs.

Two independent misunderstandings cause this:

1. init_state axiom does not pin the ghost's value in general. It only states what must hold in the state immediately after the constructor, and it is only *usable* as an assumption when you are proving an invariant (where the prover establishes the base case and then may assume it), or where you explicitly require it in a rule. In an ordinary rule starting from an arbitrary state, the ghost begins unconstrained.

2. Any call the prover cannot resolve — an external call into an unknown contract, a dispatch on an unlinked interface — is modelled by havocing state, and that havoc includes your ghost variables. So a single unresolved call anywhere in the path resets your counter to an arbitrary value and produces nonsense counterexamples.

Fixes: state the property as an invariant if it really is one, or add an explicit require listingUpdatesCount == 0; at the top of the rule to establish the starting state. Then eliminate the havoc by constraining unresolved calls in the methods block, e.g.

function _.functionName() external => DISPATCHER(true);

so the prover only considers implementations among the contracts in the verification run instead of an arbitrary unknown callee.

Non-obvious part: the counterexample looks like a prover bug because the reported value is unreachable in real execution. It isn't — it is a havoc artefact, and the diagnostic move is to hunt for unresolved calls in the call trace.

Source: adapted from a Stack Exchange answer by teryanarmen (question by Patrick Collins), https://ethereum.stackexchange.com/questions/159440/why-is-my-ghost-variable-havocd-when-it-has-an-axiom — CC BY-SA 4.0