$ go version
go version devel go1.20-0a4a57de4d Thu Aug 18 21:54:52 2022 +0000 linux/amd64

sort.Search, and its inlined copy in go/token.searchInts, both have code like:

func searchInts(a []int, x int) int {
    i, j := 0, len(a)    
    for i < j {
        h := int(uint(i+j) >> 1) // avoid overflow when computing h
        // i ≤ h < j  
        if a[h] <= x { // Found IsInBounds
            i = h + 1
        } else {
            j = h
        }
    }
    return i - 1   
}

Note that a[h] causes a bounds check, as the compiler doesn't know that 0 <= h < len(a). We intuitively know that, because h is the middle point between i and j, thus i <= h <= j. i and j themselves start as 0 and len(a) and move closer towards h.

It would be nice if the prove pass could be smart enough to tell that a[h] here does not need a bounds check. I can force its hand via if h >= 0 && h < len(a) && a[h] <= x {, but that doesn't result in a noticeable improvement:

name           old time/op  new time/op  delta
SearchInts-16  16.2ns ± 2%  16.5ns ± 1%  +1.50%  (p=0.001 n=8+10)

I realize that this request is fairly specific to binary searches, but I reckon that's a common enough occurrence that we should teach prove about it.

cc @egonelbre @golang/compiler