leanprover
`bv_decide`: support for shifting by a natural number
The following example is not currently supported by bv_decide
import Std.Tactic.BVDecide
theorem ushiftRight_symbolic_shift (x : BitVec 64) (n : Nat) (h : n < 64) :
x >>> n = (BitVec.extractLsb 63 n x).zeroExtend 64 := by
bv_decide
It produces the error message.
error: None of the hypotheses are in the supported BitVec fragment.
There are two potential fixes for this:
1. If you are using custom BitVec constructs simplify them to built-in ones.
2. If your problem is using only built-in ones it might currently be out of reach.
Consider expressing it in terms of different operations that are better supported.
@shilgoel brought this up in conversation today, and I will think a bit on how to add support for this use-case.
A proposal was to take into account the fact that larger values of the Nat shift amount will shift out the operand completely, effectively putting a bound on the shift amount to consider.
I don't think we can nicely handle this apart from the non trivial cases. As soon as you have any other constraints on your Nat or the Nat occurs in multiple locations inside of the BitVec term this naive case splitting won't lead to satisfactory results. @bollu also told me that this issue was mostly caused by you using x >>> y.toNat instead of x >>> y? In that case the issue here doesn't sound really critical to me?
