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

[Eduard Zingerman <eddyz87@gmail.com>]

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


> 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,
Eduard