🐱 Is Widening Actually Necessary? (a provocative post)

Started by AbstractKitty · 247 replies · 18,432 views · 🔥 HOT THREAD

Posts: 247

Participants: 31

Last post: 2 hours ago by NarrowingEnjoyer

Status: ● Active

⚠️ Mod note (FixpointFelicia): Thread is being monitored for quality. Please keep discussion technically grounded. Do NOT post memes about Cousot without citing Cousot. Repeated violations will result in temporary ban from /static-analysis/.

Pages: 1 2 3 4 5 6 7 ... 25 Showing posts 41–50 of 247

· · · ✦ · · ·

Post #41 📅 March 14, 2024 02:47 AM

👻

SoundnessSpectre

Overapproximation Oracle

Posts: 4,891

Joined: Jan 2009

⭐ Veteran

Hibernating

I have been lurking this thread for four days from my cave. It finally dragged me out.

You are all arguing past each other because you're conflating two questions:
(1) Is widening necessary in general?
(2) Is widening necessary for specific program classes?

For (1): Yes. Trivially. The ascending chain condition fails for essentially all useful abstract domains over infinite-state programs. We've known this since Cousot & Cousot '77. I will not be relitigating this.

For (2): THIS IS WHERE IT GETS INTERESTING.

Dropped out of the net for two years but I kept tabs on the literature. I've been sitting on this link waiting for a thread worthy of it. Congratulations, you've earned it.

Let me be precise about what this says: for affine programs (loop bodies are affine assignments — think x := Ax + b with rational matrix A and vector b), Hrushovski et al. give an algorithm that computes all polynomial invariants of any degree. The strongest such invariant is their conjunction. The algorithm terminates in finite time. This is an exact fixpoint. No widening operator appears anywhere in the proof.

The key insight is algebraic: the set of polynomial invariants forms an ideal in the polynomial ring, and for affine maps this ideal is computable via techniques from algebraic geometry — specifically, the orbit of the affine map generates a variety whose defining ideal can be computed exactly.

So yes. For this class. Widening is not merely suboptimal. It is entirely unnecessary — you can do better, and "better" means exact.

I'll be going back into hibernation after this post. Discuss amongst yourselves.

— SoundnessSpectre | "The analysis that never terminates is the only truly sound one." | Last active: today (unfortunately)

Post #42 📅 March 14, 2024 02:53 AM

🐱

GaloisCat

Lattice Witch

Posts: 1,203

Joined: Aug 2019

🐾 Regular

OH MY GOODNESS.

SoundnessSpectre just woke from their slumber and immediately dropped a JACM paper. This is not a drill. This is not a drill.

SoundnessSpectre wrote:

the strongest algebraic invariant is computable. The algorithm terminates and produces an exact result. No widening required.

I read the Hrushovski et al. 2018 LICS version of this work a while back — the JACM 2023 version is the full journal paper with all the proofs. The core result is genuinely striking: they show that for an affine program (one whose loop body is a sequence of affine assignments), you can compute the ideal of all polynomial relations that hold as invariants.

The technique goes through the Zariski closure of the orbit of the linear part of the transition relation. Because we're dealing with affine maps, the orbit is contained in an algebraic variety, and that variety's ideal is finitely generated — so you can compute it! The algorithm essentially computes the Gröbner basis of this ideal.

This is the kind of result that makes me tear up a little, not gonna lie. 😭 An exact fixpoint for a nontrivial class of programs. Beautiful.

Now the obvious question for the thread: does this settle the original debate? I think it very significantly weakens the "widening is necessary" position for anyone whose programs of interest are affine. Which is... a lot of numerical programs!

— GaloisCat | Galois connections are just adjunctions for people who haven't discovered category theory yet

Post #43 📅 March 14, 2024 03:11 AM

😸

AbstractKitty

Domain Theorist

Posts: 867

Joined: Mar 2020

🐾 Regular

SoundnessSpectre wrote:

You are all arguing past each other because you're conflating two questions

...I mean. Yes. This is exactly what I was trying to say in the OP, but clearly I didn't say it nearly as clearly or authoritatively. 🙈

I want to be gracious here and not say "I told you so" — but. I told you so? Partially. My original claim was more modest: I said widening was a pragmatic crutch, not a fundamental necessity, and that for structured program classes better alternatives exist. I didn't have this specific paper in hand but the existence of such results wasn't surprising to me.

What is genuinely new to me from SoundnessSpectre's drop: the result is in the JACM, it's fully proven, and the keyword is "strongest algebraic program invariants" — meaning the algorithm doesn't just find some invariant, it finds the strongest possible polynomial invariant. That's much stronger than what I was claiming.

✅ AbstractKitty's original thesis, partially vindicated: For affine programs with rational coefficients, exact fixpoints are indeed computable without widening. The price is computational cost (Gröbner basis computations can be expensive), but correctness is not sacrificed.

I'll also note: the distinction SoundnessSpectre drew matters enormously for what "widening is necessary" means. If it means "for Turing-complete programs in general, no finite-time convergence guarantee without widening," sure. But if it means "for all practical purposes, widening is the only game in town" — that's false, and this paper is one of several counterexamples.

— AbstractKitty | Started this thread. Regrets nothing. Well, maybe the title.

Post #44 📅 March 14, 2024 03:29 AM

🔍

LatticeTabby

Tarski's Familiar

Posts: 2,441

Joined: Nov 2015

⭐ Senior

Okay. I have now read the paper. Or rather, I have re-read the 2018 LICS version and skimmed the JACM version's new sections. Let me actually interrogate this claim properly, because GaloisCat and AbstractKitty are getting excited and I want to make sure we understand exactly what's being claimed and what isn't.

What the paper actually says (precisely):

Hrushovski et al. 2023, Theorem 1.1 (paraphrased):
For an affine program P over the rationals — a program whose loop body consists solely of assignments of the form x_i := Σ a_{ij} x_j + b_i (with rational a_{ij}, b_i) — the strongest polynomial invariant of P is computable. The algorithm terminates.

What "affine program" means here: The loop body is a single affine map (or a non-deterministic choice between affine maps). No conditional branches that depend on variable values. No multiplication of variables by each other. Coefficients are rationals.

What "strongest polynomial invariant" means: The conjunction of all polynomial equalities that hold as loop invariants. Note this is about polynomial equalities, not inequalities. The paper does not claim to compute the strongest invariant for the full polyhedral domain (which includes linear inequalities).

My concerns / open questions:

1. Computational cost: The algorithm goes through algebraic geometry machinery — specifically computing the ideal of the Zariski closure of an orbit. In practice, this involves Gröbner basis computation, which is doubly exponential in the worst case. Is this tractable for real programs?

2. Inequalities vs. equalities: Most program analysis domains we care about (intervals, octagons, polyhedra) are about inequalities, not polynomial equalities. The Hrushovski et al. result gives you the algebraic variety — the zero set. How does this translate to the kinds of range information interval analysis gives you?

3. Non-deterministic conditionals: Their model handles non-determinism by taking the union of affine maps. But real programs have guards! while (x < 100) { x := x + 1 } — the guard x < 100 is not captured in the affine map model. Their result abstracts this away.

I'm not saying the result isn't beautiful and important — it clearly is. I'm saying we should be precise about the gap between "exact fixpoints computable for affine programs" and "widening is unnecessary for programs you actually want to analyze."

SoundnessSpectre — if you're still awake — can you comment on point 2?

— LatticeTabby | "A beautiful theorem is not automatically a useful one" — me, constantly, at every reading group

Post #45 📅 March 14, 2024 03:44 AM

🦶

PolyhedralPaws

Constraint Kitten

Posts: 312

Joined: Feb 2022

🐾 Member

This is all incredibly exciting! Quick question — does this generalize to nonlinear programs? Like, what if my loop body has a product of two variables? x := x * y + 1 kind of thing? We have lots of embedded numerical code with polynomial updates. Would the result extend to polynomial (not just affine) loop bodies?

If you can compute exact invariants for affine loops, surely the same algebraic geometry machinery could be pushed to polynomial loops? The variety would just be... more complicated?

Post #46 📅 March 14, 2024 03:52 AM

🔍

LatticeTabby

Tarski's Familiar

Posts: 2,441

Joined: Nov 2015

⭐ Senior

PolyhedralPaws wrote:

does this generalize to nonlinear programs? [...] surely the same algebraic geometry machinery could be pushed to polynomial loops?

No. And the paper itself addresses this explicitly. I'll quote the relevant observation:

For affine programs, the key property exploited is that the orbit of an affine map is well-behaved algebraically — the Zariski closure of the orbit is computable. For polynomial maps (nonlinear loop bodies), the situation is dramatically different. Computing invariant ideals is undecidable for general loops, and the paper makes clear that the affine case is special precisely because affine maps generate a group whose orbit has a nicely structured algebraic closure.

The moment you introduce a term like x * y in the loop body, you lose the algebraic structure that makes the orbit computation tractable. The set of polynomial invariants for a general polynomial loop is not even recursively enumerable in general.

For polynomial programs, researchers have developed template-based approaches (fix the degree, search for coefficients) and SOS (sum-of-squares) relaxations — but these are approximations, not exact computations. See the Rodríguez-Carbonell & Kapur line of work, or more recently the algebro-geometric synthesis work by Goharshady et al. (2023, OOPSLA) — but again, those are about program synthesis, not analysis exactness.

The affine case is genuinely special. Do not generalize it.

⚠️ LatticeTabby's Razor: If you think a decidability result for a restricted class "obviously" extends to a more general class, you have not been doing program analysis long enough.

— LatticeTabby | I have been burned by this exact mistake twice in my research career

Post #47 📅 March 14, 2024 04:18 AM

🐈

MeownadTransformer

Functor Enthusiast

Posts: 578

Joined: Jul 2021

🐾 Regular

okay I got extremely nerd-sniped and started trying to sketch what a Haskell implementation of the basic structure would look like. it's 4am but I'm going with it. here's what I have so far for representing affine programs and computing invariant ideals (partial, definitely doesn't compile yet):

-- AffineInvariant.hs
-- Sketch of Hrushovski-style strongest algebraic invariant computation
-- WARNING: this is a 4am sketch, not production code
-- TODO: actually implement Gröbner basis (currently placeholder)

module AffineInvariant where

import Data.Matrix (Matrix, (!), fromLists, multStd, identity)
import Data.Ratio (Rational, (%))
import qualified Data.Set as Set
import Data.List (nub, transpose)

-- | An affine map: x ↦ Ax + b
-- A is n×n rational matrix, b is n-vector
data AffineMap = AffineMap
  { linearPart  :: Matrix Rational   -- ^ the A matrix
  , constPart   :: [Rational]         -- ^ the b vector
  } deriving (Show, Eq)

-- | An affine program: initial point + loop body (affine map)
-- In the non-det case, a list of possible loop bodies
data AffineProgram = AffineProgram
  { initPoint   :: [Rational]
  , loopBodies  :: [AffineMap]     -- ^ non-det choice
  } deriving (Show)

-- | Compose two affine maps: (A2, b2) ∘ (A1, b1) = (A2·A1, A2·b1 + b2)
composeAffine :: AffineMap -> AffineMap -> AffineMap
composeAffine (AffineMap a2 b2) (AffineMap a1 b1) =
  AffineMap (a2 `multStd` a1) newB
  where
    newB = -- A2 * b1 + b2  (TODO: implement properly)
           zipWith (+) b2 (applyLinear a2 b1)

applyLinear :: Matrix Rational -> [Rational] -> [Rational]
applyLinear m v = -- matrix-vector multiply
  [ sum [ m ! (i, j) * (v !! (j-1)) | j <- [1..length v] ]
  | i <- [1..length v]
  ]

-- | Compute the first k iterates of the affine map from the initial point
-- The orbit is { f^0(x0), f^1(x0), f^2(x0), ... }
orbit :: AffineMap -> [Rational] -> Int -> [[Rational]]
orbit f x0 k = take k $ iterate (applyAffine f) x0

applyAffine :: AffineMap -> [Rational] -> [Rational]
applyAffine (AffineMap a b) x =
  zipWith (+) (applyLinear a x) b

-- TODO: 
--   groebnerBasis :: [Polynomial] -> [Polynomial]
--   zariski closure computation via orbit ideal
--   this is the hard part and I'm going to bed

The TODO comment at the bottom basically represents where the entire difficulty of this project lives lol. The Gröbner basis computation is the core of the algorithm and it's deeply nontrivial to implement efficiently. There are Haskell packages (algebra, computational-algebra) but I haven't figured out how to wire them in yet.

The orbit computation part is trivial — that's just iterating the map. The hard part is computing the ideal of the Zariski closure of that orbit, which requires finding all polynomials that vanish on the (possibly infinite) orbit. In practice you compute up to some degree bound and hope the ideal stabilizes.

Will continue tomorrow. Or in an hour. We'll see.

— MeownadTransformer | "It's not a bug, it's an under-approximation"

Post #48 📅 March 14, 2024 04:31 AM

🐾

NarrowingEnjoyer

Descending Chain Gang

Posts: 1,994

Joined: May 2017

⬇️ Narrower

told you widening bad

— NarrowingEnjoyer

Post #49 📅 March 14, 2024 04:58 AM

🐱

GaloisCat

Lattice Witch

Posts: 1,203

Joined: Aug 2019

🐾 Regular

Can we talk about the Presburger arithmetic angle for a second? Because I think it's relevant to LatticeTabby's point 2 about inequalities vs equalities.

Recall: Presburger arithmetic is the first-order theory of the integers with addition (but not multiplication). It is decidable — Presburger himself proved this in 1929 via quantifier elimination. This is crucially different from Peano arithmetic (which adds multiplication and is undecidable by Gödel).

Relevance to the thread: Presburger arithmetic can express linear arithmetic constraints — exactly the kind of thing you'd find in interval/octagon/polyhedral analyses. And because Presburger arithmetic is decidable, we can in principle decide all first-order properties expressible in linear arithmetic over integer variables.

The connection to widening is: if your program's semantics can be expressed in Presburger arithmetic (i.e., the loop body and invariant candidates are all linear arithmetic), then in principle you don't need widening for convergence — you can use a decision procedure. The catch is that Presburger arithmetic decision procedures have doubly exponential complexity in the worst case (Fischer & Rabin 1974). So "in principle decidable" doesn't mean "practically usable."

This is the real tradeoff: widening trades precision for scalability. The exact algebraic invariant methods trade scalability for precision. Both are valid engineering choices depending on your context.

But crucially: the existence of the exact methods means widening is a pragmatic choice, not a theoretical necessity. AbstractKitty was right about that framing.

— GaloisCat | Presburger arithmetic is the only arithmetic that's ever loved me back

Post #50 📅 March 14, 2024 05:22 AM

👻

SoundnessSpectre

Overapproximation Oracle

Posts: 4,892

Joined: Jan 2009

⭐ Veteran

🔥 Active

(I said I was going back to sleep. LatticeTabby asked a good question. I cannot let a good question go unanswered. This is my curse.)

LatticeTabby wrote:

inequalities vs. equalities: Most program analysis domains we care about are about inequalities. The Hrushovski et al. result gives you the algebraic variety — the zero set. How does this translate to range information?

This is the correct and important objection. Let me address it precisely.

You are right that the Hrushovski result gives you polynomial equalities, not inequalities. The strongest polynomial invariant is a conjunction of polynomial equations — it describes an algebraic variety. If you want to know "x ≤ 100 after the loop," that's a semialgebraic condition, not an algebraic one (it's a sign condition, not a vanishing condition).

However, a few observations:

1. Equalities are often more powerful than you think. The strongest polynomial invariant can capture nontrivial relationships. For example, for the loop x := x+1; y := y+x, the strongest invariant might capture the quadratic relationship between x and y that lets you precisely bound y in terms of x. From the equality, you can sometimes derive useful bounds.

2. The Presburger angle (thanks GaloisCat). For integer affine programs, if we restrict to linear invariants (not polynomial), then we're in the territory of Presburger arithmetic. The Karr algorithm (1976) already handles the linear equality case — it computes the strongest linear equality invariant (the affine hull) exactly in polynomial time. No widening. This is old news but still underappreciated.

3. For linear inequalities + affine programs: The situation is more subtle. The work of Kincaid et al. on "closed forms of loops" (they call it "loop summarization") computes a symbolic closed form for an affine loop — essentially x^n = f(n, x^0) as a formula in Presburger arithmetic extended with some exponential terms. This is decidable for the rational case and gives you exact loop behavior, from which invariants (including inequality invariants) can be extracted.

Bottom line: The paper I cited handles polynomial equalities exactly. For linear inequalities over affine programs, related work gives you exact or near-exact results via different techniques. The gap between "equalities" and "the full polyhedral domain" is real but is actively being closed by the research community.

Now I really am going to sleep. Do not quote me for at least six hours.

— SoundnessSpectre | post count: one more than I intended | "every finite descending chain terminates, unlike me apparently"

· · · ✦ · · ·

Pages: 1 2 3 4 5 6 7 ... 25 « Prev Next »

💬 Quick Reply

Full reply editor →

Currently viewing this thread: LatticeTabby, MeownadTransformer, GaloisCat, PolyhedralPaws, 5 guests | SoundnessSpectre last seen: 2 minutes ago

📂 Related Threads

🧵 The Karr Algorithm is Criminally Underappreciated (affine hull computation) · 89 replies

🧵 Gröbner Bases in Program Analysis: A Practical Introduction · 44 replies

🧵 Presburger Arithmetic and Loop Invariants: What Every Analyst Should Know · 127 replies

🧵 Polyhedra vs Octagons: When Does Precision Actually Matter? · 203 replies

🧵 Survey: Every Widening Operator I Know Of (community wiki) · 318 replies · 📌 Pinned

🧵 Narrowing After Widening: Is It Worth The Effort? · 71 replies