cc @bmkessler

This looks to be a limitation with prove results not being available to rewrite rules, since there are rewrite rules to handle this case:

(Div64 n (Const64 [c])) && isNonNegative(n) && isPowerOfTwo(c)            -> (Rsh64Ux64 n (Const64 <typ.UInt64> [log2(c)]))
(Mod64 <t> n (Const64 [c])) && isNonNegative(n) && isPowerOfTwo(c)            -> (And64 n (Const64 <t> [c-1]))

But the implementation of isNonNegative really only handles constants and a few special operations like len/cap.

// isNonNegative reports whether v is known to be greater or equal to zero.
func isNonNegative(v *Value) bool {
	switch v.Op {
	case OpConst64:
		return v.AuxInt >= 0

	case OpConst32:
		return int32(v.AuxInt) >= 0

	case OpStringLen, OpSliceLen, OpSliceCap,
		OpZeroExt8to64, OpZeroExt16to64, OpZeroExt32to64:
		return true

	case OpRsh64Ux64:
		by := v.Args[1]
		return by.Op == OpConst64 && by.AuxInt > 0

	case OpRsh64x64:
		return isNonNegative(v.Args[0])
	}
	return false
}

The division could be handled if the factsTable version of isNonNegative were available.

// isNonNegative reports whether v is known to be non-negative.
func (ft *factsTable) isNonNegative(v *Value) bool

Unfortunately, the first opt pass happens before prove even has a chance to deduce the numerator is non-negative, so the generic rule has already fired.

// Signed divide by power of 2.
// n / c =       n >> log(c) if n >= 0
//       = (n+c-1) >> log(c) if n < 0
// We conditionally add c-1 by adding n>>63>>(64-log(c)) (first shift signed, second shift unsigned).
(Div64 <t> n (Const64 [c])) && isPowerOfTwo(c) ->
  (Rsh64x64
    (Add64 <t> n (Rsh64Ux64 <t> (Rsh64x64 <t> n (Const64 <typ.UInt64> [63])) (Const64 <typ.UInt64> [64-log2(c)])))
    (Const64 <typ.UInt64> [log2(c)]))

Currently, the prove pass only removes redundant BlockIf branches, but I don't see any reason why it shouldn't be able to make other simplifications as well. In this case, it could use the knowledge that ft.isNonNegative(n) to simplify (Rsh64x64 <t> n (Const64 <typ.UInt64> [63])) -> 0 and equivalent for 32/16/8, that should eliminate all the unnecessary division fixups for constant division I believe after late opt does some further simplification. Note that there are other closely related rewrites that would be available to prove such as zeroing right shifts of known to be small numbers, (RshU64x64 n [c]) is 0 whenever 0 <= n < 1<<c.

Change https://golang.org/cl/212277 mentions this issue: cmd/compile: in prove, zero right shifts of positive int by #bits - 1

I beleive the CL above fixes this issue.

using ft.isNonNegative(n) to simplify (Rsh64x64 <t> n (Const64 <typ.UInt64> [63])) -> 0

(Rsh64x64 <t> n (Const64 <typ.UInt64> [63])) && ft.isNonNegative(n) -> 0
Is that just a specific instance of the more general calse you've listed later?

(RshU64x64 n [c]) && 0 <= n < 1<<c -> 0

Yes, that is just a special case where all positive int64 are automatically less than 1<<63, so the second condition is not needed.

Change https://golang.org/cl/232857 mentions this issue: cmd/compile: in prove, zero right shifts of positive int by #bits - 1