cmd/compile: fix mis-infer bounds in slice len/cap calculations

CL 704875 enhanced prove to infer bounds when index have a relationship
with len(A) - K. However, the change incorrectly infer "K - len(A)" case,
causing wrong bounds information.

Fixing this by matching exactly "len(A) - K" case.

Fixes #76709

Change-Id: Ibeedff55520658401af5bd3aa7e98cc1bcf38fd6
Reviewed-on: https://go-review.googlesource.com/c/go/+/727180
Reviewed-by: Cherry Mui <cherryyz@google.com>
Auto-Submit: Cuong Manh Le <cuong.manhle.vn@gmail.com>
LUCI-TryBot-Result: Go LUCI <golang-scoped@luci-project-accounts.iam.gserviceaccount.com>
Reviewed-by: Jakub Ciolek <jakub@ciolek.dev>
Reviewed-by: David Chase <drchase@google.com>

src/cmd/compile/internal/ssa/prove.go

@@ -2119,7 +2119,10 @@ func (ft *factsTable) detectSliceLenRelation(v *Value) {
 		if bound := ow.Args[0]; (bound.Op == OpSliceLen || bound.Op == OpStringLen) && bound.Args[0] == slice {
 			lenOffset = ow.Args[1]
 		} else if bound := ow.Args[1]; (bound.Op == OpSliceLen || bound.Op == OpStringLen) && bound.Args[0] == slice {
-			lenOffset = ow.Args[0]
+			// Do not infer K - slicelen, see issue #76709.
+			if ow.Op == OpAdd64 {
+				lenOffset = ow.Args[0]
+			}
 		}
 		if lenOffset == nil || lenOffset.Op != OpConst64 {
 			continue

test/fixedbugs/issue76709.go

@@ -0,0 +1,42 @@
+// run
+
+// Copyright 2025 The Go Authors. All rights reserved.
+// Use of this source code is governed by a BSD-style
+// license that can be found in the LICENSE file.
+
+package main
+
+import "fmt"
+
+//go:noinline
+func bug1(a []int, i int) int {
+	if i < 0 || i > 20-len(a) {
+		return 0
+	}
+	diff := len(a) - i
+	if diff < 10 {
+		return 1
+	}
+	return 2
+}
+
+//go:noinline
+func bug2(s []int, i int) int {
+	if i < 0 {
+		return 0
+	}
+	if i <= 10-len(s) {
+		x := len(s) - i
+		return x / 2
+	}
+	return 0
+}
+
+func main() {
+	if got := bug1(make([]int, 5), 15); got != 1 {
+		panic(fmt.Sprintf("bug1: got %d, want 1", got))
+	}
+	if got := bug2(make([]int, 3), 7); got != -2 {
+		panic(fmt.Sprintf("bug2: got %d, want -2", got))
+	}
+}