Re: [PATCH] bpf: Simplify tnum_step()

[Shung-Hsi Yu]

Cc Harishankar and Paul since they've sent the original patchset that
added tnum_step().

On Wed, Mar 18, 2026 at 06:19:06PM +0100, Hao Sun wrote:
> Simplify tnum_step() from a 10-variable algorithm into a straight
> line sequence of bitwise operations.

Nit: my brain is a bit fried trying to go through current implementation
and this new one in parallel. Would be nice to get a short tldr;
something like

  The trick is realizing the problem can be simplified to finding a
  submask of t.mask that is greater than (z - t.value).

> tnum_step(): Given a tnum `(tval, tmask)` where `tval & tmask == 0`,
> and a value `z` with `tval ≤ z < (tval | tmask)`, find the smallest
> `r > z`, a tnum-satisfying value, i.e., `r & ~tmask == tval`.
> 
> Every tnum-satisfying value has the form tval | s where s is a subset
> of tmask bits (s & ~tmask == 0).  Since tval and tmask are disjoint:
> 
>     tval | s  =  tval + s

This seems the key to simplification, quite interested at how you came
across this.

> Similarly z = tval + d where d = z - tval, so r > z becomes:
> 
>     tval + s  >  tval + d
>     s > d
> 
> The problem reduces to: find the smallest s, a subset of tmask, such
> that s > d.
> 
> Notice that `s` must be a subset of tmask, the problem now is simplified.
...
> A Lean4 proof for the correctness of the algorithm is also available
> in case anyone is interested:
> 	[1] https://pastebin.com/raw/czHKiyY0

Cool! First time Lean4 proof showing up BPF mailing list.

...
> -		res = w;
> -	}
> -	return res;
> +	d = z - t.value;

A bit of comment explaining would be nice.

> +	carry_mask = (1ULL << fls64(d & ~t.mask)) - 1;
> +	inc = ((d | carry_mask | ~t.mask) + 1) & t.mask;

Maybe break out the calculation of inc, give it a name (next_submask?),
and have it as preceding patch? It seems generic enough that I thought
would have been implemented already, but bitmap_scatter() was the
closest I could find.

Perhaps could be submitted to include/linux/bitops.h in the future.

...