Re: [PATCH] bpf: Simplify tnum_step()

[Hao Sun]

On Thu, Mar 19, 2026 at 10:35 AM Paul Chaignon <paul.chaignon@xxxxxxxxx> wrote:
>
> On Thu, Mar 19, 2026 at 10:01:31AM +0100, Hao Sun wrote:
>
> Thanks for the cc Shung-Hsi. We were discussing it with Hari who's
> planning to double check soundness.

Great, let me know the result when the verification is done; I will then
send the v2.

>
> > [...]
> > > > -             res = w;
> > > > -     }
> > > > -     return res;
> > > > +     d = z - t.value;
> > >
> > > A bit of comment explaining would be nice.
> > >
> >
> > The commit message is self-contained; anyone interested can git blame.
> > But I am unsure. If a detailed description is preferred, I can add a
> > comment to v2.
>
> Not disagreeing about the role of git blame, but it's not a replacement
> for code comments either. Having just the intuition in comments can help
> a lot; as you mention below, it's one less indirection ;)
>
> In its current form, I find the proof harder to follow than the
> previous, very verbose version. Maybe there's a good middle ground?
>

By `proof`, you are referring to the description/commit message,  not
the Lean4 proof, right? I was a bit confused here.

[...]