abstract-invariant-generator
Installation
SKILL.md
Abstract Invariant Generator
When → invariant-inference (which works from concrete traces) can't find the invariant, abstract interpretation can. It over-approximates: instead of tracking exact values, track which region of a chosen domain the values are in.
Abstract domains — pick by invariant shape
| Domain | Can express | Example invariant | Cost |
|---|---|---|---|
| Sign | x > 0, x = 0, x < 0 |
n > 0 |
Trivial |
| Interval | lo ≤ x ≤ hi |
0 ≤ i ≤ n |
Cheap |
| Octagon | ±x ± y ≤ c (two-var bounds) |
i ≤ j, j - i ≤ n |
Moderate |
| Polyhedra | Arbitrary linear inequalities | 2i + 3j ≤ n + 5 |
Expensive |
| Congruence | x ≡ k (mod m) |
i is even |
Cheap |
Start cheap. Intervals catch 80% of array-bounds invariants. Octagons catch most two-pointer patterns. Polyhedra are for when you actually need a weird linear relationship.