The expression simplifier’s analyzer is unable to prove:
k + (bx * 2048 + tx * 16) % 7168 < 7168
even though this is mathematically provable given known variable bounds.
Variable Bounds
- k:
[0, 16) - tx:
[0, 128) - bx:
[0, 3584)
Two different analysis methods give inconsistent bound information for the sub‑expression:
(bx * 2048 + tx * 16) % 7168
-
const_int_boundanalysis
Returns the range[0, 7167] -
modular_setanalysis
Reveals a coefficient of16, meaning the actual reachable values are multiples of 16 in the range[0, 7168).
Therefore, the effective max is7168 - 16 = 7152, giving a tighter bound[0, 7152].
Reproduction Code
from tvm.arith import Analyzer, ProofStrength
import tvm
analyzer = Analyzer()
k = tvm.te.var("k", dtype="int32")
tx = tvm.te.var("tx", dtype="int32")
bx = tvm.te.var("bx", dtype="int32")
analyzer.bind(k, tvm.ir.Range(0, 16))
analyzer.bind(tx, tvm.ir.Range(0, 128))
analyzer.bind(bx, tvm.ir.Range(0, 3584))
expr = k + (bx * 2048 + tx * 16) % 7168 < 7168
print("can_prove(expr):", analyzer.can_prove(expr, ProofStrength.SYMBOLIC_BOUND))
print("can_prove((...) % 7168 < 7168):", analyzer.can_prove((bx * 2048 + tx * 16) % 7168 < 7168, ProofStrength.SYMBOLIC_BOUND))
print("can_prove((...) % 7168 <= 7152):", analyzer.can_prove((bx * 2048 + tx * 16) % 7168 <= 7152, ProofStrength.SYMBOLIC_BOUND))
print("can_prove(k + (...) % 7168 <= 7168):", analyzer.can_prove((k + (bx * 2048 + tx * 16) % 7168) <= 7168, ProofStrength.SYMBOLIC_BOUND))
print("const_int_bound(...) % 7168:", analyzer.const_int_bound((bx * 2048 + tx * 16) % 7168))
print("modular_set(...) % 7168:", analyzer.modular_set((bx * 2048 + tx * 16) % 7168))
Possible Direction for Solution
wanna discuss if we might consider enhancing const_int_bound analysis to incorporate stride/coeff information from modular_set.
That way, tighter bounds (e.g. [0, 7152] instead of [0, 7167]) would allow can_prove to succeed for such cases.