From 8c6a579516a731ddbf305482822939440be82454 Mon Sep 17 00:00:00 2001
From: Jonah Uellenberg <JonahUellenberg@gmail.com>
Date: Thu, 27 Nov 2025 18:31:12 -0800
Subject: [PATCH] cmd/compile: make prove use non-equality in subtraction for a
 stronger bound

Given:
  s := /* slice */
  k := /* proved valid index in s (0 <= k < len(s)) */
  v := s[k:]

len(v) >= 1, so v[0] needs no bounds check. However, for
len(v) = len(s) - k, we only checked if len(s) >= k and so could only
prove len(v) >= 0, thus the bounds check wasn't removed.

As far as I can tell these checks were commented out for performance,
but after benchmarking prove I see no difference.

Fixes: #76429
---
 src/cmd/compile/internal/ssa/prove.go | 24 +++++++++++-------------
 test/loopbce.go                       |  6 +++---
 test/prove.go                         | 10 +++++++++-
 3 files changed, 23 insertions(+), 17 deletions(-)

diff --git a/src/cmd/compile/internal/ssa/prove.go b/src/cmd/compile/internal/ssa/prove.go
index 1aab7e3eb775e9..c4f491f13ddc2a 100644
--- a/src/cmd/compile/internal/ssa/prove.go
+++ b/src/cmd/compile/internal/ssa/prove.go
@@ -2162,24 +2162,22 @@ func (ft *factsTable) detectSubRelations(v *Value) {
 		return // x-y might overflow
 	}
 
-	// Subtracting a positive number only makes
-	// things smaller.
-	if yLim.min >= 0 {
+	// Subtracting a positive non-zero number only makes
+	// things smaller. If it's positive or zero, it might
+	// also do nothing (x-0 == v).
+	if yLim.min > 0 {
+		ft.update(v.Block, v, x, signed, lt)
+	} else if yLim.min == 0 {
 		ft.update(v.Block, v, x, signed, lt|eq)
-		// TODO: is this worth it?
-		//if yLim.min > 0 {
-		//	ft.update(v.Block, v, x, signed, lt)
-		//}
 	}
 
 	// Subtracting a number from a bigger one
-	// can't go below 0.
-	if ft.orderS.OrderedOrEqual(y, x) {
+	// can't go below 1. If the numbers might be
+	// equal, then it can't go below 0.
+	if ft.orderS.Ordered(y, x) {
+		ft.signedMin(v, 1)
+	} else if ft.orderS.OrderedOrEqual(y, x) {
 		ft.setNonNegative(v)
-		// TODO: is this worth it?
-		//if ft.orderS.Ordered(y, x) {
-		//	ft.signedMin(v, 1)
-		//}
 	}
 }
 
diff --git a/test/loopbce.go b/test/loopbce.go
index aabd56c682b878..ca09e7e7f70e6b 100644
--- a/test/loopbce.go
+++ b/test/loopbce.go
@@ -17,8 +17,8 @@ func f0a(a []int) int {
 func f0b(a []int) int {
 	x := 0
 	for i := range a { // ERROR "Induction variable: limits \[0,\?\), increment 1$"
-		b := a[i:] // ERROR "Proved IsSliceInBounds$"
-		x += b[0]
+		b := a[i:] // ERROR "Proved IsSliceInBounds$" "Proved slicemask not needed \(by limit\)$"
+		x += b[0]  // ERROR "Proved IsInBounds$"
 	}
 	return x
 }
@@ -417,7 +417,7 @@ func bce1() {
 
 func nobce2(a string) {
 	for i := int64(0); i < int64(len(a)); i++ { // ERROR "Induction variable: limits \[0,\?\), increment 1$"
-		useString(a[i:]) // ERROR "Proved IsSliceInBounds$"
+		useString(a[i:]) // ERROR "Proved IsSliceInBounds$" "Proved slicemask not needed \(by limit\)$"
 	}
 	for i := int64(0); i < int64(len(a))-31337; i++ { // ERROR "Induction variable: limits \[0,\?\), increment 1$"
 		useString(a[i:]) // ERROR "Proved IsSliceInBounds$" "Proved slicemask not needed"
diff --git a/test/prove.go b/test/prove.go
index 1b50317fe3ea4e..00e5581841a184 100644
--- a/test/prove.go
+++ b/test/prove.go
@@ -2552,7 +2552,7 @@ func swapbound(v []int) {
 	for i := 0; i < len(v)/2; i++ { // ERROR "Proved Div64 is unsigned|Induction variable"
 		v[i], // ERROR "Proved IsInBounds"
 			v[len(v)-1-i] = // ERROR "Proved IsInBounds"
-			v[len(v)-1-i],
+			v[len(v)-1-i],  // ERROR "Proved IsInBounds"
 			v[i] // ERROR "Proved IsInBounds"
 	}
 }
@@ -2718,6 +2718,14 @@ func detectStringLenRelation(s string) bool {
 	return false
 }
 
+func issue76429(s []byte, k int) byte {
+	if k < 0 || k >= len(s) {
+		return 0
+	}
+	s = s[k:]   // ERROR "Proved IsSliceInBounds" "Proved slicemask not needed"
+	return s[0] // ERROR "Proved IsInBounds"
+}
+
 //go:noinline
 func prove(x int) {
 }