Intblasting for mixed bitvector-integer goals?

Stream: Is there code for X?

[Andres Erbsen]

Is there an implementation of the intblasting strategy for reasoning about arithmetic involving both Uint64 and Int, ideally with grind? The idea is that operations on Uint64 would be seen as integer operations involving div/mod with constant denominators, which would be translated to LIA. I don't need the and/or cases that need a number of equations proportionally to the number of bits.

[Kim Morrison]

Could you please provide some examples (ideally even arranged from easy to hard)?

[Andres Erbsen]

Here are some very easy examples:

example (x : UInt8) : 0 <= x.toNat := by grind -- this one already works!
example (x : Int8) (H : x.toInt > 256) : 0 = 1 := by grind -- LIA counterexample x:=257
example (x : UInt8) : x.toNat <= 2^8 := by grind -- x:=257
example (x : UInt8) : x.toNat <= 256 := by grind -- x:=257
example (x : Int8) : -256 <= x.toInt := by grind -- x:=-256
example (x y : UInt8) : x < 2 -> y < 2 -> (x + y).toNat = x.toNat+ y.toNat := by grind -- x := 0, y := 0
example (x y : UInt8) : x < 2 -> y < 2 -> (x + y).toNat = x.toNat+ y.toNat := by simp; grind -- x := 0, y := 0
example (x y : Int8) : 0 <= x /\ x < 2 -> 0 <= y /\ y < 2 -> (x + y).toInt = x.toInt+ y.toInt := by grind -- x := 0, y := 0
example (x : UInt8) : x.toNat != 0 -> (x - 1).toNat < x.toNat := by grind
example (b e i : UInt8) (l : Nat) : (e - b).toNat = l -> i.toNat < l -> (b + i - b).toNat < l := by grind
example (b e i l : UInt8) : (e - b) = l -> i < l -> (b + i - b) < l := by grind
example (x : UInt8) : x.shiftLeft 7 != 0 -> x != 0 := by grind
example (x : UInt8) : x.shiftRight 7 != 0 -> x > 100 := by grind

If more challenging examples would be helpful, I could extract some from bedrock2 tests, LiveVerif tests, and examples (bsearch, lightbulb) in Rocq.

[Andres Erbsen]

Here's a more advanced example from bsearch above; hopefully I translated it correctly:

example (left right : UInt32) (n : Nat)
(na : (right - left).toNat = 8 * n)
(nz : (right - left).toNat != 0) :
let mid := left + (((right - left) >>> 4) <<< 3);
(mid - left).toNat < 8 * n
:= by grind

[Andres Erbsen]

I started to hack something together using grind patterns and got most of the ones shown here to pass. There are some failing examples in there that I don't know how to make progress on right now, including one where running subst before grind seems to help.

[Kim Morrison]

@Henrik Böving, are any of these in your fragment? :-)

[Henrik Böving]

bv_decide cannot deal with anything toNat or toInt. The ones that dont are perfectly doable. It would work partially for toInt/toNat if there was a preprocessor to try and remove them but that is not really in the spirit of what Andres is asking for here.