Abstract Interpretation — Brief ☧

"In whom are hid all the treasures of wisdom and knowledge."

— Colossians 2:3 (KJV)

Q: Suppose you are moving to a new city and want to know if traffic

is bad. You could track every single car on every road at every moment —

but that is impossible. Instead, you check a traffic report that says

"heavy on the highway, light downtown." You have lost the details of

individual cars, but you have gained a useful, actionable summary. Is

there a formal version of this idea for analyzing programs?

A: Yes — abstract interpretation. Instead of running a program on

exact, concrete values (every car), you run it on abstract values

(categories like "positive," "negative," "zero," or "heavy traffic,"

"light traffic"). You trade precision for guarantee: the analysis

always terminates and always gives you a safe answer — one that covers

all the real possibilities, even if it is a bit broad.

For example, if you know x is positive and y is positive, you can

conclude x + y is positive — without knowing the actual numbers.

Q: But how do you know the simplified answer is trustworthy? If you

throw away detail, how do you know you are not also throwing away a

bug?

A: Through a Galois connection — the formal bridge between the

concrete world and the abstract world. It consists of two functions:

alpha (abstraction): maps concrete values to abstract categories

gamma (concretization): maps abstract categories back to sets of concrete values

The key guarantee is soundness: if the abstract analysis says "this

is positive," then every concrete value it represents really is positive.

The abstract answer may be an over-approximation (it might include

some extra possibilities), but it will never miss a real case.
Concrete: {-3, -1, 0, 2, 5}
    ↓ alpha (abstract)
Abstract: {negative, zero, positive}
    ↓ gamma (concretize)
Concrete: {..., -3, -2, -1, 0, 1, 2, 3, ...}  (over-approximation — safe but broad)
Q: How does the analysis actually reach its conclusion?

A: By computing a fixpoint — it iterates

the abstract computation until the result stops changing. Think of

pouring water into a bowl: it sloshes around at first, but eventually

settles. A technique called widening ensures the iteration always

converges, even for loops that could run forever in the concrete world.

Key Concepts

Concept	Meaning	Our Project
Abstract domain	Simplified value space	BitVec64 (64 possible values represented as a bitmask)
Galois connection	Sound link between domains	Hierarchical4k ↔ Hierarchical256k
Fixpoint	Result of iterative analysis	Arc consistency fixpoint
Widening	Ensure termination	Limit domain hierarchy levels

Each concept in this table maps directly to a component of our system, and understanding these connections reveals that our FPGA constraint solver is, at its mathematical core, an abstract interpretation engine. The abstract domain is the bitmask: instead of tracking every possible concrete value, we track a set of possible values encoded as bits. The Galois connection is the hierarchical relationship between domain levels. The fixpoint is what arc consistency computes. And widening is what prevents the analysis from running forever -- by limiting the domain to a fixed number of hierarchy levels, we guarantee termination.

Connection to our system: Our hierarchical bitmask domains are an abstract

interpretation of finite sets. Each bit in a domain bitmask represents a concrete value; a 1 means "this value is still possible" and a 0 means "this value has been eliminated." This is the abstraction: we do not track which specific combination of values satisfies the constraints, only which individual values are still candidates. The L0/L1/L2 hierarchy is a Galois connection, with each level being a sound abstraction of the level below it:

L0 (64-bit summary) abstracts L1 (4K bits), which abstracts L2 (262K bits). The abstraction function (alpha) is the OR-reduction that computes summary bits; the concretization function (gamma) is the expansion that recovers the full domain from its summary. Arc

consistency propagation computes a fixpoint over these abstract domains — it iterates until no more values can be eliminated, which is precisely

the pattern abstract interpretation describes. The soundness guarantee holds: if our abstract analysis says a value is impossible (bit = 0), it truly is impossible in every concrete solution.

Learn more in the deep version

Related: Lattices | Fixpoints | Nelson-Oppen

Soli Deo Gloria