Converting goals to be bitblasted like BVDecide

Stream: general

[l1mey]

I've been experimenting for a while on how to enable entirely automated proofs for this LLVM rewrites formalisation project I've been working on. I have been working with definitions of LLVM integers as so:

inductive iN (bits : Nat) : Type where
  | bitvec : BitVec bits → iN bits
  | poison : iN bits

export iN (poison bitvec)

/--
`Rewrite x y` means the value `x` can be rewritten into the value `y`.
-/
inductive Rewrite {n} : iN n → iN n → Prop where
  /-- A value rewrites to itself. -/
  | refl (x : iN n) : Rewrite x x
  /-- Poison can be rewritten into any concrete value. -/
  | poison_forge (v : BitVec n) : Rewrite poison (bitvec v)

These are easily amenable to proof, and easy to read. The Rewrite relation encodes the semantics of valid coercions.

However, it is impossible to be used with bv_decide, as the constructors poison and bitvec need to be removed from the expression:

theorem addNsw_assoc {n} (x y : iN n)
    : iN.addNsw x y ~> iN.addNsw y x := by

  -- this simp would be automated
  simp [iN.addNsw, iN.poisonWrapper, iN.addNswBV, iN.poisonPreconditions]
  /-
  n : Nat
  x y : iN n
  ⊢ (match x, y with
    | poison, x => poison
    | x, poison => poison
    | bitvec a, bitvec b => if a.saddOverflow b = true then poison else bitvec (a + b)) ~>
    match y, x with
    | poison, x => poison
    | x, poison => poison
    | bitvec a, bitvec b => if a.saddOverflow b = true then poison else bitvec (a + b)
  -/
  bv_decide
  -- None of the hypotheses are in the supported
  -- BitVec fragment after applying preprocessing.

Even if I were to introduce simplifiers that would take away all these match cases and leave only BitVec operations, which I have, it still wouldn't be able to bitblast, because the goal contains iN from the inputs and hence needs to be matched anyway. So in all cases, I'm always left with the inputs being unable to simplify down. Either I change my definitions (1), or find some way to transform the goal and have it replaced (2).

(Below at the end of the post, I have attached MWEs for the pattern match definition of iN, and the bitwise version of iN.)

So I thought to myself that I should change my definitions (1), to allow it to be easily bitblasted, I did so and ended up with:

structure iN (bits : Nat) : Type where
  protected bitvec : BitVec bits
  protected poison : Bool

def poison {n : Nat} : iN n := ⟨0, true⟩
def bitvec {n : Nat} (value : BitVec n) : iN n := ⟨value, false⟩

/--
`Rewrite x y` means the value `x` can be rewritten into the value `y`.
-/
def Rewrite {n : Nat} (x y : iN n) : Prop :=
  /- A value rewrites to itself. -/
  (¬x.poison ∧ ¬y.poison ∧ x.bitvec = y.bitvec) ∨

  /- (or) Poison can be rewritten into anything. -/
  (x.poison)

The Rewrite relation is entirely encoded in propositional logic, and is equivalent. There wasn't much code that needed to be adjusted, other than the match expressions, and so this definition fit in nicely.

However, I quickly ended up with an unprovable result, due to the fact that I define poison as ⟨0, true⟩. This definition doesn't actually encode that a value being poison means that it's concrete value is inaccessible:

theorem unprovable {n} (x : iN n) {h : x.poison = true}
    : x = poison := by

  unfold poison at *
  simp
  /-
  n : Nat
  x : iN n
  h : x.poison = true
  ⊢ x = { bitvec := 0#n, poison := true }
  -/
  sorry

So, I'm back at at (2). I want to know how to convert the goals in terms of iN, to equivalent goals in terms of propositional logic, that would encode poison states faithfully. This would be essentially be "bitblasting" these goals, even though there isn't much to change.

I am quite new to metaprogramming, but know enough to write some basic tactics. I have a general understanding of how you'd want to do this, a proof by reflection taking the goal and reifying it and then having some lemmas about equality of denoted expressions. So far my knowledge is from the article Proof by Reflection (and why not to use it) by @Timothy Mou. I have done a cursory read about how bv_decide works and I know it does a similar proof by reflection, but that's all I know. I wanted to ask first to see where people could lead me.

Could someone offer their experience? I know this is possibly out of the range of what most Lean users do.

This file is an MWE for the inductive type definition of iN: mwe.lean. This MWE contains the bitwise definition of iN: mwe2.lean.

[l1mey]

Is there at least any material on how to write tactics that transform the goal from one that isn't amenable to automated proof, into one that can? How would you even structure a tactic like that? I've been reading the bv_decide code, and while it isn't exactly related, it is helping me at a slow pace.

The ability to construct the theorem x ~> y ↔ $(convert x y), where convert converts the expressions x and y into something that works only on bitvectors would be a big win for me. Then it would allow me to replace the goal with something easier to work on.