Top definition is unsound

[ymand]

When BoolValues were refactored so to split out Formulas, Top was redefined. In the new definition, a given Top instance has a specific fixed Atom, which violates the invariant that all Top are equivalent, which is crucial for soundness. Indeed, the only reason we didn't implement Top with a singleton was a technical constraint in the SAT solver.

In the old version, when Top is unpacked, it generates a fresh atom. In the new version, an atom is chosen when Top is created. Here's the comment:

/// A TopBoolValue represents a boolean that is explicitly unconstrained.
///
/// This is equivalent to an AtomicBoolValue that does not appear anywhere
/// else in a system of formula.
/// Knowing the value is unconstrained is useful when e.g. reasoning about
/// convergence.

Unfortunately, this is incorrect. Once Top is used, the atom can leak into the environment and become constrained. This leads to unsoundness, for example:

// Key:
// x -> Top(V1) means "x maps to a Top value with atom V1".
// FC means "flow condition"
bool x = ...
bool cond();
bool foo();
// x -> Top(V1)
bool b = ...;
if (b) { ... }
else {
  if (!x) return;
  // x -> V1 and FC = V1
  while(cond())
    x = foo();
  // x -> Top(V2)
}
// FC = !b implies V1
// x -> Top(V1), because comparison equates all Tops and we take the left one
// (the then branch), on which `x` is unchanged.
if (!b) {
  bool wrong = x;
  // x -> V1, unpacked from Top(V1)
  // wrong -> V1
  // From FC, we incorrectly conclude V1 is true from which anything follows...
}