Re: [PATCH] bpf: Simplify tnum_step()

[Paul Chaignon <paul.chaignon@gmail.com>]

On Thu, Mar 19, 2026 at 02:12:54PM +0100, Hao Sun wrote:
> On Thu, Mar 19, 2026 at 10:35 AM Paul Chaignon <paul.chaignon@gmail.com> 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.

Seems I thought one word and wrote another :/ I meant the code, the
tnum_step function.

> 
> [...]