Can you please post a complete snippet that actually compiles?

package main

func test1(foo []byte) {
	// _ = foo[0]
	rem := len(foo) % 64
	_ = foo[:rem]  // I originally put _ = foo[rem] which is wrong as rem==len(foo) is possible
}

func test2(foo []byte) {
	_ = foo[63]
	rem := len(foo) % 64
	_ = foo[rem] 
}

func main(){}

Running go build -gcflags="-d=ssa/check_bce/debug=1" gives

./test.go:4:9: Found IsInBounds
./test.go:6:9: Found IsInBounds
./test.go:10:9: Found IsInBounds
./test.go:12:9: Found IsInBounds

The checks on line 4 and 10 are expected, but line 6 and 12 should be eliminated

@cbeuw if len(foo) == 0, then rem is 0, so _ = foo[rem] should not be proved.

@cuonglm That's correct, which is why _ = foo[0] needs a bounds check. When it is known len(foo) > 0, then _ = foo[rem] is always safe.

@cuonglm Actually there is a +-1 error in the first case, because it's possible rem == len(foo). But the second case still stands since rem is strictly less than m

The complication with the general case of proving that

r := x%m && m > 0 --> 0 <= r < m

Is that by the time prove runs, the modulus for constant m will have been strength reduced in general to a form that doesn't involve the modulus operator anymore.

x%C => x-(x/C*C)

However, for the specific case above where m is a power of 2 (x%64 above), then the modulus will be rewritten as x&(64-1) by the compiler. So the relation that needs to be inferred in that case is:

r := x&m && m >= 0 --> 0 <= r <= m

AND of a non-negative number is bounded by zero and that non-negative number. I think adding that fact to prove may be fairly straightforward. @zdjones may have more insight.

I think this may not quite be a duplicate, but requires the same or similar solution as #29872.

We talked there of delaying div reduction to only the lateopt pass. This would leave the mods in place for the prove pass to see.