Re: [PATCH RFC bpf-next 0/4] bpf: replace min/max fields with struct cnum{32,64}

[shenghao yuan <shenghaoyuan0928@163.com>]

Hello Eduard,

On 2026/4/23 3:05, Eduard Zingerman wrote:
> On Wed, 2026-04-22 at 22:50 +0800, Yazhou Tang wrote:
>> Hi Eduard, Alexei, and everyone,
>>
>> On 4/21/26 6:28 PM, Eduard Zingerman wrote:
>>> This RFC replaces s64, u64, s32, u32 scalar range domains tracked by
>>> verifier by a pair of circular numbers (cnums): one for 64-bit domain
>>> and another for 32-bit domain. Each cnum represents a range as a
>>> single arc on the circular number line, from which signed and unsigned
>>> bounds are derived on demand. See also wrapped intervals
>>> representation as in [1].
>>>
>>> The use of such representation simplifies arithmetic and conditions
>>> handling in verifier.c and allows to express 32 <-> 64 bit deductions
>>> in a more mathematically rigorous way.
>>>
>>> [1] https://jorgenavas.github.io/papers/ACM-TOPLAS-wrapped.pdf
>> Thanks for the great RFC. Replacing the heuristic min/max bounds with
>> a rigorous cnum domain is a fantastic step forward for the verifier.
> 
> Hi Yazhou,
> 
> Thank you for the response! Collaboration is most definitely welcome.
> Alexei is positive about this RFC, so we have a way forward.
> 
>> We had previously considered proposing a similar replacement of
>> the range tracker with wrapped interval analysis (wint), based on
>> the same TOPLAS'15 paper. However, we held off, fearing the added
>> complexity might be rejected. That's why we are thrilled to see
>> this RFC and would love to contribute to this effort:
>>
>> 1. Implementation of division, modulo, and other missing ALU ops
>>
>> We noticed the discussion regarding the complexity of div/mod on cnum.
>> We have previously implemented [1] the full suite of abstract operations
>> for wint in Rust (including add/sub/mul/div/mod and bitwise ops).
>> This was built for potential integration into Solana BPF and is
>> heavily inspired by a recent paper [2].
>>
>> [1] https://github.com/OpenSourceVerif/Wrapped-Interval-for-Rust
>> [2] https://dl.acm.org/doi/pdf/10.1145/3728905
>>
>> The algorithms for div and mod are indeed complex but entirely viable.
>> We are very interested in collaborating to port these extended ALU
>> operations into the kernel C implementation.
> 
> Could you please elaborate which algorithms you have in mind.
> It appears that [2] is about sign-aware tnums not wrapped intervals.
> The Rust code for [sdiv] looks similar to the algorithm described in
> the TOPLAS'15 [1].
> 
> [sdiv] https://github.com/OpenSourceVerif/Wrapped-Interval-for-Rust/blob/master/src/wrapped_interval.rs#L985
> 
> 

I think Yazhou meant that we could translate the Rust implementation (reproducing
the TOPLAS'15 algorithm) to C for the cnum domain. But we could try to implement
a simplified vesion of [sdiv] in the TOPLAS'15 paper to better suit the
real-world production scenarios.

>> 2. Machine-checked proofs via theorem prover(s)
>>
>> While CBMC is excellent for checking bounded C-level implementation
>> details and catching integer bugs, model checking is inherently
>> constrained by its bounds.
>>
>> To complement this, we have used the Rocq theorem prover to provide
>> deductive, algebraic proofs for the soundness and completeness of
>> wint's operations over int64. This is still a work in progress;
>> currently, we have completed the proofs for:
>> - the soundness and completeness of wint's add and sub operation
>> - the soundness of wint's join operation
>>
>> We believe this can strengthen the theoretical foundation of cnum.
>>
>> We are also exploring the use of Z3 to automate the soundness proofs
>> for these abstract operations. Furthermore, we are actively researching
>> the soundness of the reduced product between tnum and wint (cnum),
>> which we hope will eventually serve as the theoretical guarantee
>> for the safe collaboration between tnum and cnum in the verifier.
> 
> That's a bit of a mess on my side at the moment.
> Not married to CBMC-based proofs, just happen to understand the
> notation and it was easy to write CBMC proofs for basic cnum
> operations. I did not try to prove anything about precision, only
> soundness, here is what I have:
> - https://github.com/eddyz87/cnum-verif/blob/master/cbmc_cnum32.c
>    This were easy for CBMC to prove
>    - from_{u,s}range()     32-bit domain
>    - {u,s}{min,max}()      32-bit domain
>    - intersect()           32-bit domain
>    - cnum32_from_cnum64()
>    - cnum64_cnum32_intersect()
> - https://github.com/eddyz87/cnum-verif/blob/arithm-ops-2/cbmc_helpers8.c
>    I tried to verify full mul operation using cbmc and hoped that use of the
>    8-bit domain would make it faster to converge. Some of the operations
>    below can be moved to 32/64-bit domains w/o risking solver timing out.
>    - add
>    - union
>    - cut
>    - check_mul_chunk
> - https://github.com/eddyz87/cnum-verif/blob/arithm-ops/cbmc_helpers8.c
>    - negate
> - https://github.com/eddyz87/cnum-verif/blob/arithm-ops-2/main.c
>    - mul -- in the function's current form CBMC is not able to process
>      it quickly even in 8-bit domain. Idk if I can make it work by
>      adding more contracts or moving the sorting phase to a separate
>      function with additional contract.  So far, I just have a
>      brute-force verification for all possible combinations of 8-bit
>      intervals.  It finishes in a couple of minutes on a 192 core
>      machine :)
> 
> Tldr, CBMC proved to be easy to use for primitive operations on cnums
> (probably generalizes to other SMT based checkers, but CBMC consumes
> unmodified C code which is extremely convenient).
> The combination of primitive operations, such as `mul` turned out to
> be harder to prove. (But I am by no means an expert when it comes to
> these tools).
> 

Thanks for sharing the details of your current verification setup.

Let me clarify a few points:
1) CBMC-based proofs – These are very good are useful.
2) Our verification approach - We (Yazhou, Tianci, me and other members in our term)
    will use Z3 and Rocq to prove the soundness of (the existing and future)
    cnum operations before the code is merged upstream.
    The proofs will be open-sourced at [3], and the primary purpose is to
    build greater confidence that the cnum implementation is safe.
    We will maintain these proofs continously, and no extra maintenance burden
    are added to the Linux eBPF community (like learn or use Z3/Rocq).

[3] https://github.com/OpenSourceVerif/open-verified-artifacts

Brief comparison of the three techniques for clarity:
- CBMC: Very user-friendly and allows quick checks. However,
   it cannot guarantee full soundness for cnum because it is bounded and
   cannot explore all possible cases (hence "bounded" verification).
   I am also very interested in CBMC for cnum, especially given
   the timeout issues you experienced.

- Z3 solver: Less user-friendly, but it can explore all possible cases
   using mathematical theories when the search space is not too large.
   For cnum, I believe operations like  cnum64-add/union/negate/etc could be proven in Z3.
   Not sure for the current cnum64-mul operations which looks complicated,
   maybe Z3 timeout on it. For example, in our recent experiments on the
   tnum_sdiv/smod (the algorithm from [2]), Z3 easily solved the 8-bit version
   but timed out after 24 hours on a 256-core server (1.5TB memory)
   for the 64-bit version.

- Rocq prover: Quite difficult to use and requires significant manual effort,
   but it is the most powerful tool.
   We can use it to prove the remaining cases that Z3 cannot handle.

> Thanks,
> Eduard


Looking forward to your thoughts.
ps: Could we send PRs to [4] firstly once we have new cnum implementations?

[4] https://github.com/eddyz87/bpf/

Best wishes,
Shenghao