Improved Tristate Multiplication With Formalization in Rocq

• The new multiplication algorithm is simpler to describe and has running time comparable to the previous state-of-the-art algorithm.Source: §1 · p. 2
• At 31-bit width, the algorithm was more precise in 95.6% of cases; at 8 bits, it was optimal in 76% of cases versus 22% for the previous algorithm.Source: §1 · p. 2
• Improved precision at higher bit positions is desirable for bounds checking and enables the Linux kernel eBPF verifier to accept more valid programs.Source: §1 · p. 2
• The Rocq work also proves soundness and optimality for tnum addition and soundness and optimality for the newly added union operation.Source: §1 · p. 2
• The multiplication soundness proof works for all bit widths, unlike the previous SAT/SMT-based proof, which could not scale beyond 8 bits.Source: §1 · p. 2

2 Background

• Tnums are sequences of trits that represent n-bit numbers with uncertain positions; each trit can match 0, 1, or either bit.A tnum matches a number when each corresponding bit belongs to the set represented by its trit.Source: §2 · p. 3

2.1 The Abstract Domain of Tnums

• Tnums form an abstract domain for nonempty sets of natural numbers, with abstraction and concretization functions relating the two domains.Abstraction can lose precision: concretizing an abstraction may produce a superset of the original set.Source: §2.1 · pp. 3–4
• An arithmetic approximation is sound when it safely covers concrete results, while an optimal approximation is the least sound approximation under the inclusion order.Soundness alone may be uninformative: mapping every input pair to a tnum of entirely uncertain bits is also sound.Source: §2.1 · pp. 4–5

2.2 Tnum Arithmetic in the Linux Kernel

• Linux represents each tnum with value and mask bit vectors; mask bits mark uncertainty, and inputs are assumed well-formed.Well-formedness requires value bits to be zero wherever the mask is one.Source: §2.2 · pp. 5–6
• The authors formalized the Linux tnum addition algorithm in Rocq and proved its soundness and optimality for unbounded bit widths.The soundness proof is also used for their multiplication algorithm, which calls addition as a subroutine.Source: §2.2 · p. 6

3 Our Algorithm for Tnum Multiplication

• An uncertain multiplier bit can create correlated unknown bits across partial products, and ignoring that correlation loses precision.For P = 11 and Q = µ1, the two µ trits in the shifted partial product arise from the same uncertain bit.Source: §3 · p. 7
• For each uncertain multiplier bit, the algorithm computes partial products for both bit values and unions them into the accumulator.It repeats shift-and-add until both the multiplier's value and mask are zero.Source: §3 · p. 7

Union Operation.

• Tnum union abstracts the union of the concrete sets represented by its inputs, and its efficient algorithm avoids computing those sets directly.The paper gives soundness and optimality proofs for the union algorithm.Source: Union Operation · p. 7

Time Complexity.

• O(n) word operations are used by tnum_mul, similar to the previous work, while tnum_union adds O(1) word operations.For arbitrary-precision operands, each word operation is itself O(n), so both algorithms are O(n^2) in Turing Machine complexity.Source: Time Complexity · p. 7

Example.

• For multiplicand 11, the example shows the new algorithm considering both possible additions for an uncertain multiplier bit, while the previous algorithm adds µµ.The two cases use additions of 00 and 11, with appropriate shifts.Source: Example · p. 8

4 Formalization in Rocq

• The Rocq formalization proves multiplication soundness and also establishes soundness and optimality for union and addition.The supporting operations’ optimality contributes to the multiplication algorithm’s overall precision.Source: §4 · p. 8
• Because the tnum arithmetic encoding is manual, the proofs establish properties of the Rocq implementations.The authors state that the Rocq embedding reflects the C code as far as possible.Source: §4 · pp. 8, 10

4.1 Modeling Tnum

• Tnums are modeled as fixed-length value and mask bit vectors, with membership requiring known bits to match the value field.The proofs take well-formed operands as a precondition.Source: §4.1 · pp. 10–11

4.2 Modeling Soundness

• Soundness requires every concrete result from represented inputs to belong to the output tnum, while preserving output well-formedness.The Rocq predicate specializes this condition to binary functions.Source: §4.2 · p. 11

4.3 Soundness of the New Tnum Multiplication

• The multiplication proof separates correctness of shift-and-add bit-vector multiplication against Rocq natural-number multiplication from soundness of tnum multiplication.The tnum theorem is parameterized by bit width.Source: §4.3 · pp. 11–12

Proof Overview.

• The recursive loop proof proceeds by induction on the multiplier length, using shift soundness and the separately proved soundness of tnum addition and union.The accumulator update is the difficult step because it branches on the multiplier’s low mask bit and uses union.Source: Proof Overview · p. 12

4.4 Soundness and Optimality of Tnum Union

• Tnum union is computed with bitwise operations, and its optimality proof shows every uncertain output bit is needed to represent the concrete union.Its soundness lemma also establishes that both input tnums are subsets of the union result.Source: §4.4 · pp. 12–13

4.5 Soundness and Optimality of Tnum Addition

• The Rocq treatment proves tnum addition soundness and optimality separately, using direct lemmas rather than the prior work’s combined reasoning.The optimality argument shows an uncertain output bit corresponds to concrete sums that differ at that bit.Source: §4.5 · p. 14, Soundness of tnum_add · p. 14

5.1 Optimality

• The new algorithm performs better at all tested bit widths on optimality, although testing was computationally infeasible beyond 8 bits.Both algorithms become less optimal as width increases, but the new algorithm's optimality declines more slowly.Source: §5.1 · p. 15, Table 1 · p. 16

5.2 Relative Precision

• The new algorithm yields more precise results than the previous one at every tested bit width.The comparison used all tnum pairs through 8 bits and 10 million random pairs at higher widths.Source: §5.2 · p. 16

Precision Anomaly Beyond 31 Bits.

• The new algorithm's relative precision advantage grows through 31 bits, then drops because multiplication can overflow 64-bit integers.A similar anomaly appears at 16 bits when the implementation uses 32-bit integers.Source: Precision Anomaly Beyond 31 Bits · pp. 16–17, Table 3 · p. 17

5.3 Precision at Higher Bits

• Comparisons of numerically smaller masks confirm that the new algorithm improves precision at higher bits.The evaluation compares all pairs through 8 bits and 10 million random pairs at higher widths.Source: §5.3 · p. 17

5.4 Multiplication in Real-world eBPF Programs

• Across 251 eBPF object files, researchers found 8,854 multiplication instances: 2,167 64-bit and 6,687 32-bit.At 32 bits, the new algorithm is more precise in 43.41% of cases despite the precision anomaly.Source: §5.4 · p. 17

5.5 Performance

• For 10 million random pairs, the previous algorithm averaged 4.52 seconds and the new one 5.19 seconds, indicating performance overhead.Callgrind estimated 875 cycles per call for the previous algorithm and 1,352 for the new one.Source: §5.5 · p. 18

6 Related Work

• Formal methods have also been applied to Linux eBPF verifier range analysis and the kernel JIT compiler.The cited work includes efforts to rectify identified range-analysis bugs.Source: §6 · p. 18
• Vishwanathan et al. gave bounded-bitwidth machine-checked proofs and unbounded-bitwidth pen-and-paper proofs for tnum addition and subtraction, plus a soundness proof for multiplication.Their multiplication implementation remained in the kernel until the authors' patch replaced it in Linux 6.18.Source: §6 · pp. 18–19
• LLVM KnownBits tracks known-zero and known-one positions, resembling Linux tnums and Miné's bitfield domain D♯b.Unlike tnums' mask-and-value representation, KnownBits uses separate Zero and One fields.Source: §6 · p. 19

7 Conclusion

• The new tnum multiplication algorithm is more precise and equally efficient compared with the previous one, and is upstreamed to Linux.The paper reports that tnum is used in the Linux kernel eBPF verifier.Source: §7 · p. 19
• The paper proves soundness of the new multiplication algorithm and soundness and optimality of tnum addition and union.The union operation was newly added to the Linux kernel.Source: §7 · p. 19
• The paper presents its unbounded machine-checked proofs as the first for tnum arithmetic.Source: §7 · p. 19

A New Algorithm and the eBPF Verifier

• The example's new multiplication result, µ0µ1, is more precise than the previous result, µµµ1.Source: A New Algorithm and the eBPF Verifier · p. 22
• The verifier begins with uncertainty about r0 after a random-value operation, representing it as 00µ1 before multiplication.Source: A New Algorithm and the eBPF Verifier · p. 22
• The tighter product lets the verifier determine that the branch is never taken, avoiding a false positive for the program.The branch would violate the requirement that every eBPF program terminate with r0 set to 0.Source: A New Algorithm and the eBPF Verifier · pp. 21–22

B.1 Convention

• In the value-mask representation, P.v and P.m give value and mask bits, with least significant bits numbered from 1.Vn denotes well-formed n-bit tnums, and set(x, i) sets bit i.Source: §B.1 · p. 22

B.2 Background

• A concrete bit vector belongs to P when every unmasked position matches P.v.The membership condition is P.m[i] = 0 implies p[i] = P.v[i].Source: §B.2 · p. 22, §B.1 · p. 22
• A masked position can vary while preserving membership, and well-formed tnum addition decomposes to bitwise OR when adding such inputs.The appendix shows that setting a masked bit in P.v still yields a member of γ(P).Source: §B.2 · p. 23

B.3 Optimality of tnum_add

• Whenever tnum_add(P, Q).m[i] = 1, concrete sums from P and Q can differ at bit i, establishing tnum_add's optimality.The section describes optimality as having no more uncertainty than the concrete result set.Source: §B.3 · p. 23
• The proof divides an uncertain output bit into cases where P.m[i], Q.m[i], or the carry-related χ.m[i] is 1.For input-mask cases, it varies the corresponding concrete operand at bit i while holding the other operand fixed.Source: §B.3 · p. 23
• For χ.m[i] = 1, the proof considers two possible bit configurations and uses concrete operand bounds to construct differing sums.χ is defined from the value and mask sums; the cited case uses P.v | P.m and Q.v | Q.m as concrete operands.Source: §B.3 · pp. 23–24

B.4 Optimality of tnum_union

• If tnum_union(P, Q).m[i] = 1, two values in concrete_union(P, Q) differ at bit i.Concrete union is γ(P) ∪ γ(Q).Source: §B.4 · p. 24
• When both input mask bits are zero, the uncertain union bit means P.v[i] and Q.v[i] differ, so their value vectors witness the claim.Source: §B.4 · p. 24
• When either input bit is masked, two values within that operand's concretization disagree at the position, including when both bits are masked.The proof uses the value vector and value-or-mask vector as witnesses.Source: §B.4 · p. 24

B.5 Soundness of tnum_mul

• The proof models the loop as tnum_mul_loop(A, B, C), with C as the partial accumulator, and defines tnum_mul by starting from TNUM(0, 0).A has length m ≥ 0, while B and C have length n > 0.Source: §B.5 · pp. 24–25
• The recursive model uses an unpadded right shift to shorten A; truncation and the accumulator support an inductive soundness proof.The unpadded shift preserves A's value relative to the algorithm's zero-padded right shift.Source: §B.5 · p. 25
• The proof proceeds by induction on A's length, with the zero-length case returning the accumulator as the product.This satisfies the proof goal because the concrete accumulator belongs to γ(C).Source: §B.5 · p. 25
• After proving membership for the shifted operands and updated accumulator, the induction hypothesis yields the original goal.The argument uses soundness of tnum shifts for the shifted operands; the multiplication proof is checked against Rocq's natural-number multiplication.Source: §B.5 · p. 25
• For a set low value bit of A, the algorithm adds B to C; for a masked low bit, it unions C with that sum.The two possible concrete low-bit choices are covered by soundness of tnum_add and tnum_union.Source: §B.5 · p. 25