This is already fixed on master by my prove CLs. I will add a specific testcase.

Change https://golang.org/cl/107355 mentions this issue: cmd/compile: add testcase for #24876

Sweet! Sorry I didn't check against tip. I forgot about filing this issue and Austin's comments made it sound like it was unlikely to be done anytime soon.

Sorry, forgot to update this issue. The specific case in dgryski/go-metro@1308eab is unfortunately not fixed yet.

IOW, this still has bound checks:

        for len(data) >= 32 {
		x += binary.BigEndian.Uint64(data)
		data = data[8:]
		x += binary.BigEndian.Uint64(data) // ERROR "Found IsInBounds$"
		data = data[8:]
		x += binary.BigEndian.Uint64(data) // ERROR "Found IsInBounds$"
		data = data[8:]
		x += binary.BigEndian.Uint64(data) // ERROR "Found IsInBounds$"
		data = data[8:]
	}

while this doesn't:

        for len(data) >= 32 {
		x += binary.BigEndian.Uint64(data[:8])
		x += binary.BigEndian.Uint64(data[8:16])
		x += binary.BigEndian.Uint64(data[16:24])
		x += binary.BigEndian.Uint64(data[24:32])
		data = data[32:]
	}

I'll notice that, even if you remove bound checks from the first snippet, you still get a lot of overhead compared to the second one because the additional 3 slice updates that require a writebarrier and computation of len/cap which are not optimized away.

Change https://golang.org/cl/190657 mentions this issue: cmd/compile: introduce recursive, on-demand inference in prove

Change https://golang.org/cl/193839 mentions this issue: cmd/compile: make prove trace OpIsSliceInBounds:

Change https://golang.org/cl/193838 mentions this issue: cmd/compile: make prove trace OpAdd64 and OpMakeSlice:

And interesing thing I noticed when looking to fix this. Maybe it was obvious, but not to me. The bounds checks in question are not actually from the slicing operations, they are from the inlined encoding/binary methods. Within prove, the bounds check in the inlined method is actually doing some work in helping to pass information along about the length of the slice. For illustration, despite removing the bounds checks in the example for this issue, my CL above doesnt remove the IsSliceInBounds from this:

for len(data) >= 32 {
	data = data[8:]
	x = data
	data = data[8:]
	x = data
	data = data[8:]
	x = data
	data = data[8:]
	x = data
}

The next CL in the chain will get these though.

Related #28941.