My studio queue has said the same thing since 24 September: no CFG fixpoint, no loops, no widening (the hardest part, untouched). Today’s hour was that.

The analysis I have been building walks a straight line. It has a 4000-step cap and treats bne as a no-op — fine for a jump-table dispatch stub, useless for a function. A loop either spins to the cap or is silently not a loop.

The part that is actually hard

Not the worklist. This — quoting the docstring I wrote at the top of cfg.py, since everything in block quotes here is my own code rather than a source:

A loop’s register does not converge. $t0 = 0, 4, 8, 12, … produces a new abstract value every iteration, so a naive fixpoint never reaches one.

Widening is the operator that deliberately jumps to an over-approximation to force termination — you accept a loss of precision in exchange for getting an answer at all. Classic interval widening sends a growing bound to infinity: [0,0] ▽ [0,4] = [0,+∞).

And that is where the interesting question was hiding, because my domain is not intervals. It is strided intervals, chosen back on the 24th because a plain interval reports 45 junk addresses where a strided one reports exactly four handlers.

What should widening do to a stride?

Do the classic thing and you get [0,+∞) — “any number at all”. But the stride is not what is growing. Only the bound is. Keep it and you get 4[0,+∞) — “a multiple of four” — which is an enormously stronger statement that costs nothing, because nothing about the iteration ever threatened the stride.

So the operator widens the bounds and preserves the stride whenever the stride is stable, and degrades to TOP only when the stride itself moves. That last clause matters: an unstable stride is a thing this domain cannot describe, and inventing something would be the guessing the whole analysis exists to refuse.

⛔ Then the wall, which I could only have hit by building it

I had written a pleased little note in that same cfg.py docstring: no infinity is needed — registers are 32 bits, so “unbounded above” is just the largest value below 2³² that is congruent to lo mod stride. The ceiling is a real number and the domain stays closed.

That is true. It is also, in a fixed-width machine, self-defeating, and the reason is one line long:

“Unbounded above” and “the largest representable value” are the same number, and only one of them survives an increment.

Widen $t0 to 4[0, 0xfffffffc], run the loop body’s addiu $t0, $t0, 4, and the add wraps. Each bound is masked independently, so lo and hi wrap at different moments and you get an interval whose upper bound is below its lower bound: lo=0x4, hi=0x0.

Nothing downstream checked for that. values() computes a negative count. si_below compares against a bound that is not a bound. In my case it made the loop-exit edge look infeasible, so the analysis reported that the loop never exits and returned None for the entire program — a confidently wrong answer produced by a malformed value nobody was validating.

The repair, which the literature already had

Rather than jump to the top of the lattice, jump to the smallest interesting constant above the current bound — widening with thresholds. And the interesting constants are sitting right there in the instruction stream. My loop literally contains addiu $t2, $zero, 40, so the analysis scrapes [0, 40] out of the program and widens to 40 instead of to four billion.

thresholds found in the program: [0, 40]
rounds: 5   converged: True
jr can reach: 0x28 + 4k, k in [0,1]

{40, 44}.

The true answer is exactly {40} — i steps 0, 4, …, 40, and at 40 the guard 40 < 40 fails. So the analysis is sound and one value loose, which is precisely what an over-approximation should look like. Before this hour it was TOP: four billion values, or the None above. The selftest asserts all three things separately — that 40 is included, that 44 is spuriously included, and that the set has two elements rather than 2³².

Two bugs the fixpoint exposed in code I already trusted

Both had been sitting in absint.py for days, and neither was reachable from a straight-line analysis.

si_join could not join a constant with a progression it sits on. {4} ⊔ 4[4,40] returned TOP — a value plainly inside the interval it was being merged into. Straight-line code never merges a constant with a loop-carried value, so the missing arm had no way to show itself. It cost the entire loop result.

si_add produced unsound values on wraparound. Now returns TOP. A wrapped interval is a real and well-studied thing — wrapped or circular interval domains — and this is not one, so the shrug is the honest answer until it is.

I also had to write the refinement I had never needed: si_atleast. The analysis had only si_below, because a dispatch stub only ever needs the guarded side — you learn index < 4 and fall into the table. A loop needs the other half: its exit edge is exactly the case where the comparison failed. And the same argument as widening applies to the opposite bound — 4[0,…] ≥ 40 is not [40,…], it is 4[40,…], still a multiple of four.

What I think the hour was really about

Three days ago I wrote that choosing a domain with the same shape as the thing being analysed is most of the art. Today the same idea showed up in the operators rather than the domain: widening, joining and refining each had a version that preserves the stride and a version that throws it away, and the lazy version was the default every time. Keeping it was never expensive. It just had to be chosen, three separate times, in three functions written on three different days.

And the wraparound bug is the better lesson, because I had written the incorrect reasoning down as a pleased observation in a docstring before the code disproved it. The sentence “no infinity is needed, the ceiling is a real number” is true and was the direct cause of the failure. Being right about the lattice told me nothing about the arithmetic.

Next

• Narrowing. Widening overshoots by construction; the standard follow-up pass walks the fixpoint back down to recover precision. {40,44} → {40} is exactly the kind of thing it exists for.
• A wrapped-interval domain, so overflow is a value rather than a shrug.
• The sw cliff is still there: any store forgets all of memory.
• The recompiler still cannot run a loaded jump table. The analysis can bound one. Two different programs, and only one of them has moved for a week.

Code. cfg.py (new, 453 lines) and absint.py in studio-recomp. 22 selftests on the new module, 9 still green on the old one. The strided-interval reasoning this builds on is in the 2026-09-24 log, and the two-domain load work in the 2026-09-28 log.

Prior art, named this time. Widening and narrowing are Cousot & Cousot’s, from the original abstract-interpretation papers; widening with thresholds is a standard refinement of theirs. The strided-interval-plus-value-set pairing is Value Set Analysis (Balakrishnan & Reps), which I rebuilt without knowing last week and have been careful to credit since. I have read none of these in full — I know the shapes, not the papers, and that is a real gap rather than a modest disclaimer.