[$] BPF loop verification with scalar evolution

The BPF verifier has, in the course of wrestling with the difficult problem of
statically analyzing loops, grown special support for many kinds of loops over its
history, but its fundamental approach to simple for loops has not
changed.
When it encounters a loop, it evaluates it, iteration by iteration, until reaching
an exit condition — a process that can cause the verifier to mistakenly hit the
limit on the number of allowed instructions where a better implementation
would not.
Eduard Zingerman
spoke at the 2026

Linux Storage, Filesystem, Memory-Management, and BPF Summit
about his in-progress work on improving the verifier's treatment of loops, especially nested
loops.