[PATCH bpf-next v2] bpf: Simplify tnum_step()

[PATCH bpf-next v2] bpf: Simplify tnum_step()

[Hao Sun]

Simplify tnum_step() from a 10-variable algorithm into a straight
line sequence of bitwise operations.

Problem Reduction:

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

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.

Algorithm:

The mask bits of `d` form a "counter" that we want to increment by one,
but the counter has gaps at the fixed-bit positions.  A normal +1 would
stop at the first 0-bit it meets; we need it to skip over fixed-bit
gaps and land on the next mask bit.

Step 1 -- plug the gaps:

    d | carry_mask | ~tmask

  - ~tmask fills all fixed-bit positions with 1.
  - carry_mask = (1 << fls64(d & ~tmask)) - 1 fills all positions
    (including mask positions) below the highest non-mask bit of d.

After this, the only remaining 0s are mask bits above the highest
non-mask bit of d where d is also 0 -- exactly the positions where
the carry can validly land.

Step 2 -- increment:

    (d | carry_mask | ~tmask) + 1

Adding 1 flips all trailing 1s to 0 and sets the first 0 to 1.  Since
every gap has been plugged, that first 0 is guaranteed to be a mask bit
above all non-mask bits of d.

Step 3 -- mask:

    ((d | carry_mask | ~tmask) + 1) & tmask

Strip the scaffolding, keeping only mask bits.  Call the result inc.

Step 4 -- result:

    tval | inc

Reattach the fixed bits.

A simple 8-bit example:
    tmask:        1  1  0  1  0  1  1  0
    d:            1  0  1  0  0  0  1  0     (d = 162)
                        ^
                        non-mask 1 at bit 5

With carry_mask = 0b00111111 (smeared from bit 5):

    d|carry|~tm   1  0  1  1  1  1  1  1
    + 1           1  1  0  0  0  0  0  0
    & tmask       1  1  0  0  0  0  0  0

The patch passes my local test: test_verifier, test_progs for
`-t verifier` and `-t reg_bounds`.

CBMC shows the new code is equiv to original one[1], and
a lean4 proof of correctness is available[2]:

theorem tnumStep_correct (tval tmask z : BitVec 64)
    -- Precondition: valid tnum and input z
    (h_consistent : (tval &&& tmask) = 0)
    (h_lo : tval ≤ z)
    (h_hi : z < (tval ||| tmask)) :
    -- Postcondition: r must be:
    --    (1) tnum member
    --    (2) z < r
    --    (3) for any other member w > z, r <= w
    let r := tnumStep tval tmask z
    satisfiesTnum64 r tval tmask ∧
    tval ≤ r ∧ r ≤ (tval ||| tmask) ∧
    z < r ∧
    ∀ w, satisfiesTnum64 w tval tmask → z < w → r ≤ w := by
  -- unfold definition
  unfold tnumStep satisfiesTnum64
  simp only []
  refine ⟨?_, ?_, ?_, ?_, ?_⟩
  -- the solver proves each conjunct
  · bv_decide
  · bv_decide
  · bv_decide
  · bv_decide
  · intro w hw1 hw2; bv_decide

[1] https://github.com/eddyz87/tnum-step-verif/blob/master/main.c
[2] https://pastebin.com/raw/czHKiyY0

Signed-off-by: Hao Sun <hao.sun@inf.ethz.ch>
Acked-by: Eduard Zingerman <eddyz87@gmail.com>
Acked-by: Shung-Hsi Yu <shung-hsi.yu@suse.com>

---
v1 -> v2: inline proof, add code comments, add a variable `filled`.

 kernel/bpf/tnum.c | 46 +++++++++++++++++++---------------------------
 1 file changed, 19 insertions(+), 27 deletions(-)

diff --git a/kernel/bpf/tnum.c b/kernel/bpf/tnum.c
index 4abc359b3db0..ec9c310cf5d7 100644
--- a/kernel/bpf/tnum.c
+++ b/kernel/bpf/tnum.c
@@ -286,8 +286,7 @@ struct tnum tnum_bswap64(struct tnum a)
  */
 u64 tnum_step(struct tnum t, u64 z)
 {
-	u64 tmax, j, p, q, r, s, v, u, w, res;
-	u8 k;
+	u64 tmax, d, carry_mask, filled, inc;
 
 	tmax = t.value | t.mask;
 
@@ -299,29 +298,22 @@ u64 tnum_step(struct tnum t, u64 z)
 	if (z < t.value)
 		return t.value;
 
-	/* keep t's known bits, and match all unknown bits to z */
-	j = t.value | (z & t.mask);
-
-	if (j > z) {
-		p = ~z & t.value & ~t.mask;
-		k = fls64(p); /* k is the most-significant 0-to-1 flip */
-		q = U64_MAX << k;
-		r = q & z; /* positions > k matched to z */
-		s = ~q & t.value; /* positions <= k matched to t.value */
-		v = r | s;
-		res = v;
-	} else {
-		p = z & ~t.value & ~t.mask;
-		k = fls64(p); /* k is the most-significant 1-to-0 flip */
-		q = U64_MAX << k;
-		r = q & t.mask & z; /* unknown positions > k, matched to z */
-		s = q & ~t.mask; /* known positions > k, set to 1 */
-		v = r | s;
-		/* add 1 to unknown positions > k to make value greater than z */
-		u = v + (1ULL << k);
-		/* extract bits in unknown positions > k from u, rest from t.value */
-		w = (u & t.mask) | t.value;
-		res = w;
-	}
-	return res;
+	/*
+	 * Let r be the result tnum member, z = t.value + d.
+	 * Every tnum member is t.value | s for some submask s of t.mask,
+	 * and since t.value & t.mask == 0, t.value | s == t.value + s.
+	 * So r > z becomes s > d where d = z - t.value.
+	 *
+	 * Find the smallest submask s of t.mask greater than d by
+	 * "incrementing d within the mask": fill every non-mask
+	 * position with 1 (`filled`) so +1 ripples through the gaps,
+	 * then keep only mask bits. `carry_mask` additionally fills
+	 * positions below the highest non-mask 1 in d, preventing
+	 * it from trapping the carry.
+	 */
+	d = z - t.value;
+	carry_mask = (1ULL << fls64(d & ~t.mask)) - 1;
+	filled = d | carry_mask | ~t.mask;
+	inc = (filled + 1) & t.mask;
+	return t.value | inc;
 }
-- 
2.34.1

Re: [PATCH bpf-next v2] bpf: Simplify tnum_step()

[Harishankar Vishwanathan]

On Fri, Mar 20, 2026 at 12:23 PM Hao Sun <sunhao.th@gmail.com> wrote:

Thanks for the patch. This is a neat simplification to make the algorithm become
straight line. I really liked the idea of working with d = z - tmin,
instead of the original
where we were working with j.  The core idea of adding 1 to
masked bits with fixed bits in place seems the same.

I checked this new algorithm for soundness in z3 using bitvector
theory, and it is
indeed sound and equivalent to the old algorithm.

Some comments below, mainly regarding explanation and maintainability.

> Simplify tnum_step() from a 10-variable algorithm into a straight
> line sequence of bitwise operations.

The original algorithm was purposefully verbose for the sake of
explanation. I feel it is better
use temporaries that explain relatively complex ideas. The compiler
will optimize
the subexpressions anyway.

> Problem Reduction:
>
> 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

I'd start with explaining what "subset of tmask" means and perhaps
define it as "submask"
early on. Currently, the term submask isn't explained anywhere but used in
the code comments.

Also, "disjoint" can be unclear to the reader. I'd explicity state
that tval and tmask can never
share 1 in the same bit position.

We should either call it "s" or "inc" everywhere.

> 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.

To be precise regarding minimality: we have to find a submask of t that
is minimally greater than d.

> Algorithm:
>
> The mask bits of `d` form a "counter" that we want to increment by one,
> but the counter has gaps at the fixed-bit positions.  A normal +1 would
> stop at the first 0-bit it meets; we need it to skip over fixed-bit
> gaps and land on the next mask bit.

I think it will be useful to illustrate right away with an example to
make it easier
to follow.

This part of the algorithm shares its idea with the previous algorithm
and a lot of the
previous commit message explained the reasoning for doing what we are
doing, but that
explanation has been dropped.

You are first trying to identify the highest bit position k which is 1
in d, and known/fixed
in t. This is important because when constructing s (or inc), setting
to 1 any masked bit
lower than k will not result in a number > d. Only positions > k are
candidates for
being set to 1. For example

z = 1010100100
t = 10xx0x1xx1
d = 0010011011
          ^
          k

Borrowing wording from the previous commit: We must set masked
positions of significance
higher than k. Specifically, we look for the next larger combination
of 1s to place in
the masked positions, relative to the combination that exists in d. We
can achieve this
by concatenating bits at unknown positions of t into an integer,
adding 1, and writing
the bits of that result back into the corresponding bit positions
previously extracted
from d.

An example like in the previous commit might also help:

t = 10xx0x
d = ..10.1
+        1
----------
    ..11.0

> Step 1 -- plug the gaps:
>
>     d | carry_mask | ~tmask
>
>   - ~tmask fills all fixed-bit positions with 1.
>   - carry_mask = (1 << fls64(d & ~tmask)) - 1 fills all positions
>     (including mask positions) below the highest non-mask bit of d.
>
> After this, the only remaining 0s are mask bits above the highest
> non-mask bit of d where d is also 0 -- exactly the positions where
> the carry can validly land.
>
> Step 2 -- increment:
>
>     (d | carry_mask | ~tmask) + 1
>
> Adding 1 flips all trailing 1s to 0 and sets the first 0 to 1.  Since
> every gap has been plugged, that first 0 is guaranteed to be a mask bit
> above all non-mask bits of d.
>
> Step 3 -- mask:
>
>     ((d | carry_mask | ~tmask) + 1) & tmask
>
> Strip the scaffolding, keeping only mask bits.  Call the result inc.
>
> Step 4 -- result:
>
>     tval | inc
>
> Reattach the fixed bits.
>
> A simple 8-bit example:

What are z and tval here in this example? It would be helpful to provide them.

>     tmask:        1  1  0  1  0  1  1  0
>     d:            1  0  1  0  0  0  1  0     (d = 162)
>                         ^
>                         non-mask 1 at bit 5
>
> With carry_mask = 0b00111111 (smeared from bit 5):
>
>     d|carry|~tm   1  0  1  1  1  1  1  1
>     + 1           1  1  0  0  0  0  0  0
>     & tmask       1  1  0  0  0  0  0  0
>
> The patch passes my local test: test_verifier, test_progs for
> `-t verifier` and `-t reg_bounds`.
>
> CBMC shows the new code is equiv to original one[1], and
> a lean4 proof of correctness is available[2]:
>
> theorem tnumStep_correct (tval tmask z : BitVec 64)
>     -- Precondition: valid tnum and input z
>     (h_consistent : (tval &&& tmask) = 0)
>     (h_lo : tval ≤ z)
>     (h_hi : z < (tval ||| tmask)) :
>     -- Postcondition: r must be:
>     --    (1) tnum member
>     --    (2) z < r
>     --    (3) for any other member w > z, r <= w
>     let r := tnumStep tval tmask z
>     satisfiesTnum64 r tval tmask ∧
>     tval ≤ r ∧ r ≤ (tval ||| tmask) ∧
>     z < r ∧
>     ∀ w, satisfiesTnum64 w tval tmask → z < w → r ≤ w := by
>   -- unfold definition
>   unfold tnumStep satisfiesTnum64
>   simp only []
>   refine ⟨?_, ?_, ?_, ?_, ?_⟩
>   -- the solver proves each conjunct
>   · bv_decide
>   · bv_decide
>   · bv_decide
>   · bv_decide
>   · intro w hw1 hw2; bv_decide
>
> [1] https://github.com/eddyz87/tnum-step-verif/blob/master/main.c
> [2] https://pastebin.com/raw/czHKiyY0
>
> Signed-off-by: Hao Sun <hao.sun@inf.ethz.ch>
> Acked-by: Eduard Zingerman <eddyz87@gmail.com>
> Acked-by: Shung-Hsi Yu <shung-hsi.yu@suse.com>

Reviewed-by: Harishankar Vishwanathan <harishankar.vishwanathan@gmail.com>

> ---
> v1 -> v2: inline proof, add code comments, add a variable `filled`.
>
>  kernel/bpf/tnum.c | 46 +++++++++++++++++++---------------------------
>  1 file changed, 19 insertions(+), 27 deletions(-)
>
> diff --git a/kernel/bpf/tnum.c b/kernel/bpf/tnum.c
> index 4abc359b3db0..ec9c310cf5d7 100644
> --- a/kernel/bpf/tnum.c
> +++ b/kernel/bpf/tnum.c
> @@ -286,8 +286,7 @@ struct tnum tnum_bswap64(struct tnum a)
>   */
>  u64 tnum_step(struct tnum t, u64 z)
>  {
> -       u64 tmax, j, p, q, r, s, v, u, w, res;
> -       u8 k;
> +       u64 tmax, d, carry_mask, filled, inc;
>
>         tmax = t.value | t.mask;
>
> @@ -299,29 +298,22 @@ u64 tnum_step(struct tnum t, u64 z)
>         if (z < t.value)
>                 return t.value;
>
> -       /* keep t's known bits, and match all unknown bits to z */
> -       j = t.value | (z & t.mask);
> -
> -       if (j > z) {
> -               p = ~z & t.value & ~t.mask;
> -               k = fls64(p); /* k is the most-significant 0-to-1 flip */
> -               q = U64_MAX << k;
> -               r = q & z; /* positions > k matched to z */
> -               s = ~q & t.value; /* positions <= k matched to t.value */
> -               v = r | s;
> -               res = v;
> -       } else {
> -               p = z & ~t.value & ~t.mask;
> -               k = fls64(p); /* k is the most-significant 1-to-0 flip */
> -               q = U64_MAX << k;
> -               r = q & t.mask & z; /* unknown positions > k, matched to z */
> -               s = q & ~t.mask; /* known positions > k, set to 1 */
> -               v = r | s;
> -               /* add 1 to unknown positions > k to make value greater than z */
> -               u = v + (1ULL << k);
> -               /* extract bits in unknown positions > k from u, rest from t.value */
> -               w = (u & t.mask) | t.value;
> -               res = w;
> -       }
> -       return res;
> +       /*
> +        * Let r be the result tnum member, z = t.value + d.
> +        * Every tnum member is t.value | s for some submask s of t.mask,
> +        * and since t.value & t.mask == 0, t.value | s == t.value + s.
> +        * So r > z becomes s > d where d = z - t.value.
> +        *
> +        * Find the smallest submask s of t.mask greater than d by
> +        * "incrementing d within the mask": fill every non-mask
> +        * position with 1 (`filled`) so +1 ripples through the gaps,
> +        * then keep only mask bits. `carry_mask` additionally fills
> +        * positions below the highest non-mask 1 in d, preventing
> +        * it from trapping the carry.
> +        */
> +       d = z - t.value;
> +       carry_mask = (1ULL << fls64(d & ~t.mask)) - 1;
> +       filled = d | carry_mask | ~t.mask;
> +       inc = (filled + 1) & t.mask;
> +       return t.value | inc;
>  }
> --
> 2.34.1
>

Re: [PATCH bpf-next v2] bpf: Simplify tnum_step()

[patchwork-bot+netdevbpf]

Hello:

This patch was applied to bpf/bpf-next.git (master)
by Alexei Starovoitov <ast@kernel.org>:

On Fri, 20 Mar 2026 17:23:36 +0100 you wrote:
> Simplify tnum_step() from a 10-variable algorithm into a straight
> line sequence of bitwise operations.
> 
> Problem Reduction:
> 
> 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`.
> 
> [...]

Here is the summary with links:
  - [bpf-next,v2] bpf: Simplify tnum_step()
    https://git.kernel.org/bpf/bpf-next/c/833ef4a954e1

You are awesome, thank you!
-- 
Deet-doot-dot, I am a bot.
https://korg.docs.kernel.org/patchwork/pwbot.html

Re: [PATCH bpf-next v2] bpf: Simplify tnum_step()

[Harishankar Vishwanathan]

On Tue, Mar 24, 2026 at 11:50 AM <patchwork-bot+netdevbpf@kernel.org> wrote:
>
> Hello:
>
> This patch was applied to bpf/bpf-next.git (master)
> by Alexei Starovoitov <ast@kernel.org>:

Hello, I see this was applied. Just a heads up that I still had a few
concerns regarding the
commit message and code style in my last reply. I think it was my
mistake to include
the Reviewed-by while still requesting changes.

Hao, would you like to send a follow-up for those, or should I put one together?

Or Alexei, do you think it is okay as is? If yes, we can just leave it be.


> On Fri, 20 Mar 2026 17:23:36 +0100 you wrote:
> > Simplify tnum_step() from a 10-variable algorithm into a straight
> > line sequence of bitwise operations.
> >
> > Problem Reduction:
> >
> > 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`.
> >
> > [...]
>
> Here is the summary with links:
>   - [bpf-next,v2] bpf: Simplify tnum_step()
>     https://git.kernel.org/bpf/bpf-next/c/833ef4a954e1
>
> You are awesome, thank you!
> --
> Deet-doot-dot, I am a bot.
> https://korg.docs.kernel.org/patchwork/pwbot.html
>
>

Re: [PATCH bpf-next v2] bpf: Simplify tnum_step()

[Alexei Starovoitov]

On Tue, Mar 24, 2026 at 2:33 PM Harishankar Vishwanathan
<harishankar.vishwanathan@gmail.com> wrote:
>
> On Tue, Mar 24, 2026 at 11:50 AM <patchwork-bot+netdevbpf@kernel.org> wrote:
> >
> > Hello:
> >
> > This patch was applied to bpf/bpf-next.git (master)
> > by Alexei Starovoitov <ast@kernel.org>:
>
> Hello, I see this was applied. Just a heads up that I still had a few
> concerns regarding the
> commit message and code style in my last reply. I think it was my
> mistake to include
> the Reviewed-by while still requesting changes.
>
> Hao, would you like to send a follow-up for those, or should I put one together?
>
> Or Alexei, do you think it is okay as is? If yes, we can just leave it be.

They read like nits to me.
New code is definitely cleaner.
As a follow up better craft a targeted selftest and explain
your points in selftest comments.

Re: [PATCH bpf-next v2] bpf: Simplify tnum_step()

[Harishankar Vishwanathan]

On Tue, Mar 24, 2026 at 5:36 PM Alexei Starovoitov
<alexei.starovoitov@gmail.com> wrote:
>
> On Tue, Mar 24, 2026 at 2:33 PM Harishankar Vishwanathan
> <harishankar.vishwanathan@gmail.com> wrote:
> >
> > On Tue, Mar 24, 2026 at 11:50 AM <patchwork-bot+netdevbpf@kernel.org> wrote:
> > >
> > > Hello:
> > >
> > > This patch was applied to bpf/bpf-next.git (master)
> > > by Alexei Starovoitov <ast@kernel.org>:
> >
> > Hello, I see this was applied. Just a heads up that I still had a few
> > concerns regarding the
> > commit message and code style in my last reply. I think it was my
> > mistake to include
> > the Reviewed-by while still requesting changes.
> >
> > Hao, would you like to send a follow-up for those, or should I put one together?
> >
> > Or Alexei, do you think it is okay as is? If yes, we can just leave it be.
>
> They read like nits to me.
> New code is definitely cleaner.
> As a follow up better craft a targeted selftest and explain
> your points in selftest comments.

Yes they were definitely nits. Makes sense to keep the
code clean.

The logic is sound and verified, so I'm happy to leave it as-is.
If I find the time to put together a targeted selftest down the road,
I'll send a separate patch!

Re: [PATCH bpf-next v2] bpf: Simplify tnum_step()

[Hao Sun]

On Tue, Mar 24, 2026 at 10:57 PM Harishankar Vishwanathan
<harishankar.vishwanathan@gmail.com> wrote:
>
> On Tue, Mar 24, 2026 at 5:36 PM Alexei Starovoitov
> <alexei.starovoitov@gmail.com> wrote:
> >
> > On Tue, Mar 24, 2026 at 2:33 PM Harishankar Vishwanathan
> > <harishankar.vishwanathan@gmail.com> wrote:
> > >
> > > On Tue, Mar 24, 2026 at 11:50 AM <patchwork-bot+netdevbpf@kernel.org> wrote:
> > > >
> > > > Hello:
> > > >
> > > > This patch was applied to bpf/bpf-next.git (master)
> > > > by Alexei Starovoitov <ast@kernel.org>:
> > >
> > > Hello, I see this was applied. Just a heads up that I still had a few
> > > concerns regarding the
> > > commit message and code style in my last reply. I think it was my
> > > mistake to include
> > > the Reviewed-by while still requesting changes.
> > >
> > > Hao, would you like to send a follow-up for those, or should I put one together?
> > >
> > > Or Alexei, do you think it is okay as is? If yes, we can just leave it be.
> >
> > They read like nits to me.
> > New code is definitely cleaner.
> > As a follow up better craft a targeted selftest and explain
> > your points in selftest comments.
>
> Yes they were definitely nits. Makes sense to keep the
> code clean.
>
> The logic is sound and verified, so I'm happy to leave it as-is.
> If I find the time to put together a targeted selftest down the road,
> I'll send a separate patch!

Hi Harishankar,

Thank you for reviewing the code and verifying its correctness, which
gives additional confidence.

I kept the commit message concise, as I felt it was sufficient to describe:
simplifying the problem to finding the submask and treating d’s mask bits
as a counter that we increment by one. Once this perspective is clear,
the rest of the logic should be relatively easy to follow.

That said, please feel free to refine the message further, e.g., adding a
selftest and referencing it from the code.