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

Author: uellenberg

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)
-		//}
 	}
 }