Using bv_decide

Stream: lean4

[Wrenna Robson]

The following proof looks primed for using bv_decide i.e. this is something I just want to throw at a SMT solver! But it doesn't seem to work. Regular decide does, though - it is true.

def mulTwo (x : BitVec 8) : BitVec 8 :=
  let b7 := x[7]
  let x := x <<< 1
  if b7 then x ^^^ 0x1B else x

def mulTwo' (x : BitVec 8) : BitVec 8 :=
  let b7 := x[7]
  BitVec.ofFnBE ![x[6], x[5], x[4], x[3].xor b7, x[2].xor b7, x[1], x[0].xor b7, b7]

theorem mulTwo_eq_mulTwo' : ∀ x, mulTwo x = mulTwo' x := sorry

What am I doing wrong?

[Henrik Böving]

bv_decide canot have knowledge of BitVec.ofFnBE its in batteries

[Wrenna Robson]

Right. Is there a way I can specify that bit vector in a way it will understand or do I have to built it from scratch? What is allowed?

[Henrik Böving]

bv_decide is supposed to work with all operations on bitvectors that core defines, if your simp set is powerful enough to dumb down BitVec.ofFnBE to that it will be fine

[Wrenna Robson]

Hmm

[Wrenna Robson]

def mulTwo (x : BitVec 8) : BitVec 8 :=
  let b7 := x[7]
  let x := x <<< 1
  if b7 then x ^^^ 0x1B else x

open BitVec in
def mulTwo' (x : BitVec 8) : BitVec 8 :=
  let b7 := x[7]
  shiftConcat (shiftConcat (shiftConcat (shiftConcat
    (shiftConcat (shiftConcat (shiftConcat (shiftConcat 0 x[6]) x[5]) x[4]) (x[3].xor b7))
    (x[2].xor b7)) x[1]) (x[0].xor b7)) b7

theorem mulTwo_eq_mulTwo' : ∀ x : BitVec 8, mulTwo x = mulTwo' x := by
  unfold mulTwo mulTwo'
  bv_decide -- nope

theorem mulTwo_eq_mulTwo'_decide : ∀ x : BitVec 8, mulTwo x = mulTwo' x := by
  unfold mulTwo mulTwo'
  decide -- yep

[Wrenna Robson]

shiftConcat is in core, I think.

[Wrenna Robson]

So what is forbidden here

[Henrik Böving]

That's an oversight in the coverage of bv_decide, feel free to open an issue about the fact that I missed shiftConcat and concat.

[Henrik Böving]

theorem mulTwo_eq_mulTwo' : ∀ x : BitVec 8, mulTwo x = mulTwo' x := by
  unfold mulTwo mulTwo'
  simp only [BitVec.shiftConcat, BitVec.concat]
  bv_decide

works

[Wrenna Robson]

Aha!

[Wrenna Robson]

Thank you :)

[Wrenna Robson]

I open an issue in core's repo?

[Henrik Böving]

Yes

[Wrenna Robson]

I'll get on that.

[Henrik Böving]

You could even fix it yourself i you're interested in that?

[Henrik Böving]

You'd have to prove a lemma such as docs#BitVec.twoPow_eq for shiftConcat and concat and then tag it here https://github.com/leanprover/lean4/blob/master/src/Std/Tactic/BVDecide/Normalize/BitVec.lean#L153 with bv_normalize + add your thing as a test.

[Wrenna Robson]

I will try to figure out how to do that. For BitVec.ofFnBE which I used originally, the issue seems to be that Fin.foldr is too crunchy for it to reason about.

[Henrik Böving]

Yes Fin.foldr requires higher order reasoning, that's not doable. However when applied to a constant Fin.foldr should be sufficiently symbolically evaluatable using the simp set to make it vanish

[Wrenna Robson]

It looks like BitVec.cons might also be missing.

[Wrenna Robson]

def mulTwo'' (x : BitVec 8) : BitVec 8 :=
  let b7 := x[7]
  BitVec.ofBoolListBE [x[6], x[5], x[4], x[3].xor b7, x[2].xor b7, x[1], x[0].xor b7, b7]

theorem mulTwo_eq_mulTwo'' : ∀ x : BitVec 8, mulTwo x = mulTwo'' x := by
  unfold mulTwo mulTwo''
  simp only [BitVec.ofBoolListBE, BitVec.cons]
  bv_decide

[Henrik Böving]

Could be, I mostly focused on the operations that are present in SMT-LIB as those are the ones people most commonly use and all the other ones can usually be expressed in terms of them.

[Wrenna Robson]

Yeah that is fair. I could look up an AES implementation and see how people normally do this operation anyway.

[Henrik Böving]

Oh they most likely extend and then shift + or

[Henrik Böving]

just how you would do it in C

[Wrenna Robson]

Makes sense.

[Wrenna Robson]

BitVec.fill as well I think.

[Henrik Böving]

Didn't even know we had that one lol

[Wrenna Robson]

Have managed to proof via bitsmashing that muliplication over Galois-256 is commutative so that is nice though.

[François G. Dorais]

If there's a way to improve BitVec.ofFnBE etc in Batteries so that it fits better with bv_decide, I would be happy to hear! I've been doing a little GF work and GF2 linear algebra for myself, which is why I added these functions but I never had time to tune the API.

[Wrenna Robson]

Oh cool, yeah pretty much me too.

[Wrenna Robson]

Would be good to compare notes...

[Wrenna Robson]

Actually proving it obeys the field axioms seems quite challenging and I was hoping maybe I could just bit blast my way through the problem.

[Henrik Böving]

@Wrenna Robson do you still plan on submitting an issue and/or PR?

[Wrenna Robson]

Yes, I just haven't yet!

[Wrenna Robson]

I finished at 7PM yesterday so slow start this morning