Re: [PATCH] bpf: Simplify tnum_step()

[Eduard Zingerman <eddyz87@gmail.com>]

On Thu, 2026-03-19 at 10:06 +0100, Hao Sun wrote:
> On Thu, Mar 19, 2026 at 9:18 AM Kumar Kartikeya Dwivedi
> <memxor@gmail.com> wrote:
> > 
> > On Wed, 18 Mar 2026 at 19:21, Hao Sun <sunhao.th@gmail.com> wrote:
> > > [...]
> > > in case anyone is interested:
> > >         [1] https://pastebin.com/raw/czHKiyY0
> > 
> > IMO it is worth it to include this proof inline in the commit log,
> > since links are fragile.
> > It's not that big, and I think it's more useful to have it inline than not.
> > 
> 
> The only concern is that the proof mainly uses `bv_decide`, which does not
> provide much insight. But it's not big, I will inline it.

I agree with you, not sure it would provide much signal, tbh.
As far as I understand `bv_decide` means: SAT-solver, please do the magic :)

A more interesting discussion would be to have some model-checker
based tests in the selftests, but Alexei was not excited last time we
talked about that.

If we have enough interested people, we can pick a checker and
maintain a "shadow copy" of relevant functions and data structures in
some repo e.g. on github + current proofs/tests. To have a starting
point for future changes.