This patch improves the precison of the scalar(32)_min_max_add and
scalar(32)_min_max_sub functions, which update the u(32)min/u(32)_max
ranges for the BPF_ADD and BPF_SUB instructions. We discovered this more
precise operator using a technique we are developing for automatically
synthesizing functions for updating tnums and ranges.

According to the BPF ISA [1], "Underflow and overflow are allowed during
arithmetic operations, meaning the 64-bit or 32-bit value will wrap".
Our patch leverages the wrap-around semantics of unsigned overflow and
underflow to improve precision.

Below is an example of our patch for scalar_min_max_add; the idea is
analogous for all four functions.

There are three cases to consider when adding two u64 ranges [dst_umin,
dst_umax] and [src_umin, src_umax]. Consider a value x in the range
[dst_umin, dst_umax] and another value y in the range [src_umin,
src_umax].

(a) No overflow: No addition x + y overflows. This occurs when even the
largest possible sum, i.e., dst_umax + src_umax <= U64_MAX.

(b) Partial overflow: Some additions x + y overflow. This occurs when
the largest possible sum overflows (dst_umax + src_umax > U64_MAX), but
the smallest possible sum does not overflow (dst_umin + src_umin <=
U64_MAX).

(c) Full overflow: All additions x + y overflow. This occurs when both
the smallest possible sum and the largest possible sum overflow, i.e.,
both (dst_umin + src_umin) and (dst_umax + src_umax) are > U64_MAX.

The current implementation conservatively sets the output bounds to
unbounded, i.e, [umin=0, umax=U64_MAX], whenever there is *any*
possibility of overflow, i.e, in cases (b) and (c). Otherwise it
computes tight bounds as [dst_umin + src_umin, dst_umax + src_umax]:

if (check_add_overflow(*dst_umin, src_reg->umin_value, dst_umin) ||
    check_add_overflow(*dst_umax, src_reg->umax_value, dst_umax)) {
	*dst_umin = 0;
	*dst_umax = U64_MAX;
}

Our synthesis-based technique discovered a more precise operator.
Particularly, in case (c), all possible additions x + y overflow and
wrap around according to eBPF semantics, and the computation of the
output range as [dst_umin + src_umin, dst_umax + src_umax] continues to
work. Only in case (b), do we need to set the output bounds to
unbounded, i.e., [0, U64_MAX].

Case (b) can be checked by seeing if the minimum possible sum does *not*
overflow and the maximum possible sum *does* overflow, and when that
happens, we set the output to unbounded:

min_overflow = check_add_overflow(*dst_umin, src_reg->umin_value, dst_umin);
max_overflow = check_add_overflow(*dst_umax, src_reg->umax_value, dst_umax);

if (!min_overflow && max_overflow) {
	*dst_umin = 0;
	*dst_umax = U64_MAX;
}

Below is an example eBPF program and the corresponding log from the
verifier. At instruction 7: (0f) r5 += r3, due to conservative overflow
handling, the current implementation of scalar_min_max_add() sets r5's
bounds to [0, U64_MAX], which is then updated by reg_bounds_sync() to
[0x3d67e960f7d, U64_MAX].

0: R1=ctx() R10=fp0
0: (85) call bpf_get_prandom_u32#7    ; R0_w=scalar()
1: (bf) r3 = r0                       ; R0_w=scalar(id=1) R3_w=scalar(id=1)
2: (18) r4 = 0x950a43d67e960f7d       ; R4_w=0x950a43d67e960f7d
4: (4f) r3 |= r4                      ; R3_w=scalar(smin=0x950a43d67e960f7d,smax=-1,umin=0x950a43d67e960f7d,smin32=0xfe960f7d,umin32=0x7e960f7d,var_off=(0x950a43d67e960f7d; 0x6af5bc298169f082)) R4_w=0x950a43d67e960f7d
5: (18) r5 = 0xc014a00000000000       ; R5_w=0xc014a00000000000
7: (0f) r5 += r3                      ; R3_w=scalar(smin=0x950a43d67e960f7d,smax=-1,umin=0x950a43d67e960f7d,smin32=0xfe960f7d,umin32=0x7e960f7d,var_off=(0x950a43d67e960f7d; 0x6af5bc298169f082)) R5_w=scalar(smin=0x800003d67e960f7d,umin=0x3d67e960f7d,smin32=0xfe960f7d,umin32=0x7e960f7d,var_off=(0x3d67e960f7d; 0xfffffc298169f082))
8: (b7) r0 = 0                        ; R0_w=0
9: (95) exit

With our patch, r5's bounds after instruction 7 are set to a much more
precise [0x551ee3d67e960f7d, 0xc0149fffffffffff] by
scalar_min_max_add().

...
7: (0f) r5 += r3                      ; R3_w=scalar(smin=0x950a43d67e960f7d,smax=-1,umin=0x950a43d67e960f7d,smin32=0xfe960f7d,umin32=0x7e960f7d,var_off=(0x950a43d67e960f7d; 0x6af5bc298169f082)) R5_w=scalar(smin=0x800003d67e960f7d,umin=0x551ee3d67e960f7d,umax=0xc0149fffffffffff,smin32=0xfe960f7d,umin32=0x7e960f7d,var_off=(0x3d67e960f7d; 0xfffffc298169f082))
8: (b7) r0 = 0                        ; R0_w=0
9: (95) exit

The logic for scalar32_min_max_add is analogous. For the
scalar(32)_min_max_sub functions, the reasoning is similar but applied
to detecting underflow instead of overflow.

We verified the correctness of the new implementations using Agni [3,4].

We since also discovered that a similar technique has been used to
calculate output ranges for unsigned interval addition and subtraction
in Hacker's Delight [2].

[1] https://docs.kernel.org/bpf/standardization/instruction-set.html
[2] Hacker's Delight Ch.4-2, Propagating Bounds through Add’s and Subtract’s
[3] https://github.com/bpfverif/agni
[4] https://people.cs.rutgers.edu/~sn349/papers/sas24-preprint.pdf

Co-developed-by: Matan Shachnai <m.shachnai@rutgers.edu>
Signed-off-by: Matan Shachnai <m.shachnai@rutgers.edu>
Co-developed-by: Srinivas Narayana <srinivas.narayana@rutgers.edu>
Signed-off-by: Srinivas Narayana <srinivas.narayana@rutgers.edu>
Co-developed-by: Santosh Nagarakatte <santosh.nagarakatte@rutgers.edu>
Signed-off-by: Santosh Nagarakatte <santosh.nagarakatte@rutgers.edu>
Signed-off-by: Harishankar Vishwanathan <harishankar.vishwanathan@gmail.com>
---
 kernel/bpf/verifier.c | 76 +++++++++++++++++++++++++++++++------------
 1 file changed, 56 insertions(+), 20 deletions(-)

diff --git a/kernel/bpf/verifier.c b/kernel/bpf/verifier.c
index 279a64933262..f403524bd215 100644
--- a/kernel/bpf/verifier.c
+++ b/kernel/bpf/verifier.c
@@ -14605,14 +14605,25 @@ static void scalar32_min_max_add(struct bpf_reg_state *dst_reg,
 	s32 *dst_smax = &dst_reg->s32_max_value;
 	u32 *dst_umin = &dst_reg->u32_min_value;
 	u32 *dst_umax = &dst_reg->u32_max_value;
+	u32 umin_val = src_reg->u32_min_value;
+	u32 umax_val = src_reg->u32_max_value;
+	bool min_overflow, max_overflow;
 
 	if (check_add_overflow(*dst_smin, src_reg->s32_min_value, dst_smin) ||
 	    check_add_overflow(*dst_smax, src_reg->s32_max_value, dst_smax)) {
 		*dst_smin = S32_MIN;
 		*dst_smax = S32_MAX;
 	}
-	if (check_add_overflow(*dst_umin, src_reg->u32_min_value, dst_umin) ||
-	    check_add_overflow(*dst_umax, src_reg->u32_max_value, dst_umax)) {
+
+	/* If either all additions overflow or no additions overflow, then
+	 * it is okay to set: dst_umin = dst_umin + src_umin, dst_umax =
+	 * dst_umax + src_umax. Otherwise (some additions overflow), set
+	 * the output bounds to unbounded.
+	 */
+	min_overflow = check_add_overflow(*dst_umin, umin_val, dst_umin);
+	max_overflow = check_add_overflow(*dst_umax, umax_val, dst_umax);
+
+	if (!min_overflow && max_overflow) {
 		*dst_umin = 0;
 		*dst_umax = U32_MAX;
 	}
@@ -14625,14 +14636,25 @@ static void scalar_min_max_add(struct bpf_reg_state *dst_reg,
 	s64 *dst_smax = &dst_reg->smax_value;
 	u64 *dst_umin = &dst_reg->umin_value;
 	u64 *dst_umax = &dst_reg->umax_value;
+	u64 umin_val = src_reg->umin_value;
+	u64 umax_val = src_reg->umax_value;
+	bool min_overflow, max_overflow;
 
 	if (check_add_overflow(*dst_smin, src_reg->smin_value, dst_smin) ||
 	    check_add_overflow(*dst_smax, src_reg->smax_value, dst_smax)) {
 		*dst_smin = S64_MIN;
 		*dst_smax = S64_MAX;
 	}
-	if (check_add_overflow(*dst_umin, src_reg->umin_value, dst_umin) ||
-	    check_add_overflow(*dst_umax, src_reg->umax_value, dst_umax)) {
+
+	/* If either all additions overflow or no additions overflow, then
+	 * it is okay to set: dst_umin = dst_umin + src_umin, dst_umax =
+	 * dst_umax + src_umax. Otherwise (some additions overflow), set
+	 * the output bounds to unbounded.
+	 */
+	min_overflow = check_add_overflow(*dst_umin, umin_val, dst_umin);
+	max_overflow = check_add_overflow(*dst_umax, umax_val, dst_umax);
+
+	if (!min_overflow && max_overflow) {
 		*dst_umin = 0;
 		*dst_umax = U64_MAX;
 	}
@@ -14643,8 +14665,11 @@ static void scalar32_min_max_sub(struct bpf_reg_state *dst_reg,
 {
 	s32 *dst_smin = &dst_reg->s32_min_value;
 	s32 *dst_smax = &dst_reg->s32_max_value;
+	u32 *dst_umin = &dst_reg->u32_min_value;
+	u32 *dst_umax = &dst_reg->u32_max_value;
 	u32 umin_val = src_reg->u32_min_value;
 	u32 umax_val = src_reg->u32_max_value;
+	bool min_underflow, max_underflow;
 
 	if (check_sub_overflow(*dst_smin, src_reg->s32_max_value, dst_smin) ||
 	    check_sub_overflow(*dst_smax, src_reg->s32_min_value, dst_smax)) {
@@ -14652,14 +14677,18 @@ static void scalar32_min_max_sub(struct bpf_reg_state *dst_reg,
 		*dst_smin = S32_MIN;
 		*dst_smax = S32_MAX;
 	}
-	if (dst_reg->u32_min_value < umax_val) {
-		/* Overflow possible, we know nothing */
-		dst_reg->u32_min_value = 0;
-		dst_reg->u32_max_value = U32_MAX;
-	} else {
-		/* Cannot overflow (as long as bounds are consistent) */
-		dst_reg->u32_min_value -= umax_val;
-		dst_reg->u32_max_value -= umin_val;
+
+	/* If either all subtractions underflow or no subtractions
+	 * underflow, it is okay to set: dst_umin = dst_umin - src_umax,
+	 * dst_umax = dst_umax - src_umin. Otherwise (some subtractions
+	 * underflow), set the output bounds to unbounded.
+	 */
+	min_underflow = check_sub_overflow(*dst_umin, umax_val, dst_umin);
+	max_underflow = check_sub_overflow(*dst_umax, umin_val, dst_umax);
+
+	if (min_underflow && !max_underflow) {
+		*dst_umin = 0;
+		*dst_umax = U32_MAX;
 	}
 }
 
@@ -14668,8 +14697,11 @@ static void scalar_min_max_sub(struct bpf_reg_state *dst_reg,
 {
 	s64 *dst_smin = &dst_reg->smin_value;
 	s64 *dst_smax = &dst_reg->smax_value;
+	u64 *dst_umin = &dst_reg->umin_value;
+	u64 *dst_umax = &dst_reg->umax_value;
 	u64 umin_val = src_reg->umin_value;
 	u64 umax_val = src_reg->umax_value;
+	bool min_underflow, max_underflow;
 
 	if (check_sub_overflow(*dst_smin, src_reg->smax_value, dst_smin) ||
 	    check_sub_overflow(*dst_smax, src_reg->smin_value, dst_smax)) {
@@ -14677,14 +14709,18 @@ static void scalar_min_max_sub(struct bpf_reg_state *dst_reg,
 		*dst_smin = S64_MIN;
 		*dst_smax = S64_MAX;
 	}
-	if (dst_reg->umin_value < umax_val) {
-		/* Overflow possible, we know nothing */
-		dst_reg->umin_value = 0;
-		dst_reg->umax_value = U64_MAX;
-	} else {
-		/* Cannot overflow (as long as bounds are consistent) */
-		dst_reg->umin_value -= umax_val;
-		dst_reg->umax_value -= umin_val;
+
+	/* If either all subtractions underflow or no subtractions
+	 * underflow, it is okay to set: dst_umin = dst_umin - src_umax,
+	 * dst_umax = dst_umax - src_umin. Otherwise (some subtractions
+	 * underflow), set the output bounds to unbounded.
+	 */
+	min_underflow = check_sub_overflow(*dst_umin, umax_val, dst_umin);
+	max_underflow = check_sub_overflow(*dst_umax, umin_val, dst_umax);
+
+	if (min_underflow && !max_underflow) {
+		*dst_umin = 0;
+		*dst_umax = U64_MAX;
 	}
 }
 
-- 
2.45.2

On Tue, 2025-06-17 at 19:17 -0400, Harishankar Vishwanathan wrote:
> This patch improves the precison of the scalar(32)_min_max_add and
> scalar(32)_min_max_sub functions, which update the u(32)min/u(32)_max
> ranges for the BPF_ADD and BPF_SUB instructions. We discovered this more
> precise operator using a technique we are developing for automatically
> synthesizing functions for updating tnums and ranges.
> 
> According to the BPF ISA [1], "Underflow and overflow are allowed during
> arithmetic operations, meaning the 64-bit or 32-bit value will wrap".
> Our patch leverages the wrap-around semantics of unsigned overflow and
> underflow to improve precision.
> 
> Below is an example of our patch for scalar_min_max_add; the idea is
> analogous for all four functions.
> 
> There are three cases to consider when adding two u64 ranges [dst_umin,
> dst_umax] and [src_umin, src_umax]. Consider a value x in the range
> [dst_umin, dst_umax] and another value y in the range [src_umin,
> src_umax].
> 
> (a) No overflow: No addition x + y overflows. This occurs when even the
> largest possible sum, i.e., dst_umax + src_umax <= U64_MAX.
> 
> (b) Partial overflow: Some additions x + y overflow. This occurs when
> the largest possible sum overflows (dst_umax + src_umax > U64_MAX), but
> the smallest possible sum does not overflow (dst_umin + src_umin <=
> U64_MAX).
> 
> (c) Full overflow: All additions x + y overflow. This occurs when both
> the smallest possible sum and the largest possible sum overflow, i.e.,
> both (dst_umin + src_umin) and (dst_umax + src_umax) are > U64_MAX.
> 
> The current implementation conservatively sets the output bounds to
> unbounded, i.e, [umin=0, umax=U64_MAX], whenever there is *any*
> possibility of overflow, i.e, in cases (b) and (c). Otherwise it
> computes tight bounds as [dst_umin + src_umin, dst_umax + src_umax]:
> 
> if (check_add_overflow(*dst_umin, src_reg->umin_value, dst_umin) ||
>     check_add_overflow(*dst_umax, src_reg->umax_value, dst_umax)) {
> 	*dst_umin = 0;
> 	*dst_umax = U64_MAX;
> }
> 
> Our synthesis-based technique discovered a more precise operator.
> Particularly, in case (c), all possible additions x + y overflow and
> wrap around according to eBPF semantics, and the computation of the
> output range as [dst_umin + src_umin, dst_umax + src_umax] continues to
> work. Only in case (b), do we need to set the output bounds to
> unbounded, i.e., [0, U64_MAX].
> 
> Case (b) can be checked by seeing if the minimum possible sum does *not*
> overflow and the maximum possible sum *does* overflow, and when that
> happens, we set the output to unbounded:
> 
> min_overflow = check_add_overflow(*dst_umin, src_reg->umin_value, dst_umin);
> max_overflow = check_add_overflow(*dst_umax, src_reg->umax_value, dst_umax);
> 
> if (!min_overflow && max_overflow) {
> 	*dst_umin = 0;
> 	*dst_umax = U64_MAX;
> }
> 
> Below is an example eBPF program and the corresponding log from the
> verifier. At instruction 7: (0f) r5 += r3, due to conservative overflow
> handling, the current implementation of scalar_min_max_add() sets r5's
> bounds to [0, U64_MAX], which is then updated by reg_bounds_sync() to
> [0x3d67e960f7d, U64_MAX].
> 
> 0: R1=ctx() R10=fp0
> 0: (85) call bpf_get_prandom_u32#7    ; R0_w=scalar()
> 1: (bf) r3 = r0                       ; R0_w=scalar(id=1) R3_w=scalar(id=1)
> 2: (18) r4 = 0x950a43d67e960f7d       ; R4_w=0x950a43d67e960f7d
> 4: (4f) r3 |= r4                      ; R3_w=scalar(smin=0x950a43d67e960f7d,smax=-1,umin=0x950a43d67e960f7d,smin32=0xfe960f7d,umin32=0x7e960f7d,var_off=(0x950a43d67e960f7d; 0x6af5bc298169f082)) R4_w=0x950a43d67e960f7d
> 5: (18) r5 = 0xc014a00000000000       ; R5_w=0xc014a00000000000
> 7: (0f) r5 += r3                      ; R3_w=scalar(smin=0x950a43d67e960f7d,smax=-1,umin=0x950a43d67e960f7d,smin32=0xfe960f7d,umin32=0x7e960f7d,var_off=(0x950a43d67e960f7d; 0x6af5bc298169f082)) R5_w=scalar(smin=0x800003d67e960f7d,umin=0x3d67e960f7d,smin32=0xfe960f7d,umin32=0x7e960f7d,var_off=(0x3d67e960f7d; 0xfffffc298169f082))
> 8: (b7) r0 = 0                        ; R0_w=0
> 9: (95) exit
> 
> With our patch, r5's bounds after instruction 7 are set to a much more
> precise [0x551ee3d67e960f7d, 0xc0149fffffffffff] by
> scalar_min_max_add().
> 
> ...
> 7: (0f) r5 += r3                      ; R3_w=scalar(smin=0x950a43d67e960f7d,smax=-1,umin=0x950a43d67e960f7d,smin32=0xfe960f7d,umin32=0x7e960f7d,var_off=(0x950a43d67e960f7d; 0x6af5bc298169f082)) R5_w=scalar(smin=0x800003d67e960f7d,umin=0x551ee3d67e960f7d,umax=0xc0149fffffffffff,smin32=0xfe960f7d,umin32=0x7e960f7d,var_off=(0x3d67e960f7d; 0xfffffc298169f082))
> 8: (b7) r0 = 0                        ; R0_w=0
> 9: (95) exit
> 
> The logic for scalar32_min_max_add is analogous. For the
> scalar(32)_min_max_sub functions, the reasoning is similar but applied
> to detecting underflow instead of overflow.
> 
> We verified the correctness of the new implementations using Agni [3,4].
> 
> We since also discovered that a similar technique has been used to
> calculate output ranges for unsigned interval addition and subtraction
> in Hacker's Delight [2].
> 
> [1] https://docs.kernel.org/bpf/standardization/instruction-set.html
> [2] Hacker's Delight Ch.4-2, Propagating Bounds through Add’s and Subtract’s
> [3] https://github.com/bpfverif/agni
> [4] https://people.cs.rutgers.edu/~sn349/papers/sas24-preprint.pdf
> 
> Co-developed-by: Matan Shachnai <m.shachnai@rutgers.edu>
> Signed-off-by: Matan Shachnai <m.shachnai@rutgers.edu>
> Co-developed-by: Srinivas Narayana <srinivas.narayana@rutgers.edu>
> Signed-off-by: Srinivas Narayana <srinivas.narayana@rutgers.edu>
> Co-developed-by: Santosh Nagarakatte <santosh.nagarakatte@rutgers.edu>
> Signed-off-by: Santosh Nagarakatte <santosh.nagarakatte@rutgers.edu>
> Signed-off-by: Harishankar Vishwanathan <harishankar.vishwanathan@gmail.com>
> ---

Acked-by: Eduard Zingerman <eddyz87@gmail.com>

[...]

On Tue, Jun 17, 2025 at 07:17:31PM -0400, Harishankar Vishwanathan wrote:
[...]
> 
> There are three cases to consider when adding two u64 ranges [dst_umin,
> dst_umax] and [src_umin, src_umax]. Consider a value x in the range
> [dst_umin, dst_umax] and another value y in the range [src_umin,
> src_umax].
> 
> (a) No overflow: No addition x + y overflows. This occurs when even the
> largest possible sum, i.e., dst_umax + src_umax <= U64_MAX.
> 
> (b) Partial overflow: Some additions x + y overflow. This occurs when
> the largest possible sum overflows (dst_umax + src_umax > U64_MAX), but
> the smallest possible sum does not overflow (dst_umin + src_umin <=
> U64_MAX).
> 
> (c) Full overflow: All additions x + y overflow. This occurs when both
> the smallest possible sum and the largest possible sum overflow, i.e.,
> both (dst_umin + src_umin) and (dst_umax + src_umax) are > U64_MAX.
> 
> The current implementation conservatively sets the output bounds to
> unbounded, i.e, [umin=0, umax=U64_MAX], whenever there is *any*
> possibility of overflow, i.e, in cases (b) and (c). Otherwise it
> computes tight bounds as [dst_umin + src_umin, dst_umax + src_umax]:
> 
> if (check_add_overflow(*dst_umin, src_reg->umin_value, dst_umin) ||
>     check_add_overflow(*dst_umax, src_reg->umax_value, dst_umax)) {
> 	*dst_umin = 0;
> 	*dst_umax = U64_MAX;
> }
> 
> Our synthesis-based technique discovered a more precise operator.
> Particularly, in case (c), all possible additions x + y overflow and
> wrap around according to eBPF semantics, and the computation of the
> output range as [dst_umin + src_umin, dst_umax + src_umax] continues to
> work. Only in case (b), do we need to set the output bounds to
> unbounded, i.e., [0, U64_MAX].
> 
 
In case anyone is interested, the above (case c) can also be proved by
the following SMT formula directly, which may ease the reasoning here:

```
; ================================================================
;  Unsigned 32- and 64-bit interval addition & subtraction
;  with wrap-around semantics and endpoint overflow / underflow.
; ================================================================
(set-logic ALL)

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ----------  u32  (32-bit)  ----------
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(declare-const l0_32 (_ BitVec 32))
(declare-const h0_32 (_ BitVec 32))
(declare-const l1_32 (_ BitVec 32))
(declare-const h1_32 (_ BitVec 32))

; Well-formed input ranges
(assert (bvule l0_32 h0_32))
(assert (bvule l1_32 h1_32))

; ----- Addition -----
(define-fun lowSum32  () (_ BitVec 32) (bvadd l0_32 l1_32))
(define-fun highSum32 () (_ BitVec 32) (bvadd h0_32 h1_32))

; Both endpoint sums overflow (wrap) ⇒ result < first addend
(assert (bvult lowSum32  l0_32))
(assert (bvult highSum32 h0_32))

; Soundness of addition
(assert
  (forall ((x (_ BitVec 32)) (y (_ BitVec 32)))
    (=> (and (bvule l0_32 x) (bvule x h0_32)
             (bvule l1_32 y) (bvule y h1_32))
        (and (bvule lowSum32  (bvadd x y))
             (bvule (bvadd x y) highSum32)))))

; ----- Subtraction -----
(define-fun lowDiff32  () (_ BitVec 32) (bvsub l0_32 h1_32))
(define-fun highDiff32 () (_ BitVec 32) (bvsub h0_32 l1_32))

; Both endpoint differences underflow ⇒ result > minuend
(assert (bvugt lowDiff32  l0_32))
(assert (bvugt highDiff32 h0_32))

; Soundness of subtraction
(assert
  (forall ((x (_ BitVec 32)) (y (_ BitVec 32)))
    (=> (and (bvule l0_32 x) (bvule x h0_32)
             (bvule l1_32 y) (bvule y h1_32))
        (and (bvule lowDiff32  (bvsub x y))
             (bvule (bvsub x y) highDiff32)))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ----------  u64  (64-bit)  ----------
;; Basically the same as above but for u64
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(declare-const l0_64 (_ BitVec 64))
(declare-const h0_64 (_ BitVec 64))
(declare-const l1_64 (_ BitVec 64))
(declare-const h1_64 (_ BitVec 64))

; Well-formed input ranges
(assert (bvule l0_64 h0_64))
(assert (bvule l1_64 h1_64))

; ----- Addition -----
(define-fun lowSum64  () (_ BitVec 64) (bvadd l0_64 l1_64))
(define-fun highSum64 () (_ BitVec 64) (bvadd h0_64 h1_64))

(assert (bvult lowSum64  l0_64))
(assert (bvult highSum64 h0_64))

(assert
  (forall ((x (_ BitVec 64)) (y (_ BitVec 64)))
    (=> (and (bvule l0_64 x) (bvule x h0_64)
             (bvule l1_64 y) (bvule y h1_64))
        (and (bvule lowSum64  (bvadd x y))
             (bvule (bvadd x y) highSum64)))))

; ----- Subtraction -----
(define-fun lowDiff64  () (_ BitVec 64) (bvsub l0_64 h1_64))
(define-fun highDiff64 () (_ BitVec 64) (bvsub h0_64 l1_64))

(assert (bvugt lowDiff64  l0_64))
(assert (bvugt highDiff64 h0_64))

(assert
  (forall ((x (_ BitVec 64)) (y (_ BitVec 64)))
    (=> (and (bvule l0_64 x) (bvule x h0_64)
             (bvule l1_64 y) (bvule y h1_64))
        (and (bvule lowDiff64  (bvsub x y))
             (bvule (bvsub x y) highDiff64)))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(check-sat)
(exit)
```

Both cvc5 and z3 can prove the above, and one can try this and expect
it producing SAT on:
https://cvc5.github.io/app/#temp_a95e25c4-88c5-4257-96c8-0bd74125b179

In addition, the unsoundness of partial case-b can also be proved by
the following formula, and the counter examples generated may be used
as test cases if needed:
https://pastebin.com/raw/qrT7rC1P

Regards
Hao

On Wed, Jun 18, 2025 at 7:24 AM Hao Sun <sunhao.th@gmail.com> wrote:
>
> On Tue, Jun 17, 2025 at 07:17:31PM -0400, Harishankar Vishwanathan wrote:
[...]
>
> Both cvc5 and z3 can prove the above, and one can try this and expect
> it producing SAT on:
> https://cvc5.github.io/app/#temp_a95e25c4-88c5-4257-96c8-0bd74125b179

Thanks for verifying this! As mentioned, we tested the new operators
using Agni, which extracts SMT encodings automatically from the C
source code and
verifies them with Z3, and found the operators to be sound. It is nice
to see that your
testing also concluded that the new operators are sound.

If you’re comfortable, feel free to reply to the patch with a
Tested-by: tag. I’d be happy
to include it in v3 of the patch.

> In addition, the unsoundness of partial case-b can also be proved by
> the following formula, and the counter examples generated may be used
> as test cases if needed:
> https://pastebin.com/raw/qrT7rC1P

We have found that using counterexamples directly for writing test cases is not
straightforward. For instance, consider constructing a test case for the partial
overflow case B. A counterexample might return specific range inputs
([umin, umax]) to
scalar_min_max_add(), which should cause the output to be unbounded
([0, U64_MAX]) due
to the partial overflow. However, these specific range inputs suggested by the
counterexample might not be reachable at all during real verifier
execution. In other
cases, the *tnum* may later refine the result in reg_bounds_sync(),
making the final
output not actually unbounded (when seen in the verifier log).

As such, we adapted Agni's enumerative synthesis procedure with
additional constraints
to generate the test cases.