search

leanprover / lean4

Lean 4 programming language and theorem prover
https://lean-lang.org
Apache License 2.0
4.65k stars 418 forks source link

bv_decide does not normalize bitvector widths #5575

Closed bollu closed 5 days ago

bollu commented 4 weeks ago

Consider the MWE:

import Lean

/-- Succeeds. -/
theorem success (x : BitVec 64) (y : BitVec 64) (hxy : x.ult y) (hyx : y.ult x) : x = y := by
  bv_decide

/-- Fails. -/
theorem failure (x : BitVec (8 * 8)) (y : BitVec 64) (hxy : x.ult y) (hyx : y.ult x) : x = y := by
  /-
  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.
  -/
  bv_decide

Changing the type of (x : BitVec (8 * 8)) to (x : BitVec 64) allows bv_decide to see that the values are indeed equivalent. Intuitively, one might expect bv_decide to index bitvectors upto defeq of their widths, since those are the equalities that Lean itself allows.

It would be nice if bv_decide ran normalizations on the width, so that cases like these are automatically proven. It may need to be a somewhat carefully engineered normalization, that does not spend too long evaluating / unfolding, but it should probably perform constant folding and rewrite upto associativity/commutativity.

A larger issue with this as the MWE was discovered by @pennyannn, and was reduced by @alexkeizer .

CC @hargoniX

hargoniX commented 4 weeks ago

Given that bv_decide is only supposed to work on fixed width things anyways, why would there need to be normalization up to associativity and commutativity? Just running the equivalent of simp only [seval] at <BitVec fvars> should be enough right?

Kha commented 5 days ago

Closing as everyone seems to agree this is as designed

alexkeizer commented 5 days ago

I'm not sure I stand behind with that conclusion: I read @hargoniX comment as "it should be enough to have bv_decide do constant folding in the normalization pass", which I agree with, rather than as "the current status-quo is fine, seeing as it should be enough to rely on the user to do constant folding via simp only [seval] at ...".

It'd be nice for bv_decide to do this automatically!