BitVec Automata Tactic

There are two ways of expressing BitVec expressions. One is:

(x &&& y) ||| y + 0

the other way is:

Term.add (Term.or (Term.and (Term.var 0) (Term.var 1)) (Term.var 1)) Term.zero

The goal of this tactic is to convert expressions of the first kind into the second kind, because we have a decision procedure that decides equality on expressions of the second kind.

theorem eval_sub {x : Term} {y : Term} {vars : ℕ → BitStream} : (x.sub y).eval vars = x.eval vars - y.eval vars

theorem eval_add {x : Term} {y : Term} {vars : ℕ → BitStream} : (x.add y).eval vars = x.eval vars + y.eval vars

theorem eval_neg {x : Term} {vars : ℕ → BitStream} : x.neg.eval vars = -x.eval vars

theorem eval_not {x : Term} {vars : ℕ → BitStream} : x.not.eval vars = ~~~x.eval vars

theorem eval_and {x : Term} {y : Term} {vars : ℕ → BitStream} : (x.and y).eval vars = x.eval vars &&& y.eval vars

theorem eval_xor {x : Term} {y : Term} {vars : ℕ → BitStream} : (x.xor y).eval vars = x.eval vars ^^^ y.eval vars

theorem eval_or {x : Term} {y : Term} {vars : ℕ → BitStream} : (x.or y).eval vars = x.eval vars ||| y.eval vars

def quoteFVar (x : Lean.FVarId) : Q(ℕ)

Equations

• quoteFVar x = Lean.mkNatLit ↑(hash x).val

def termNat (n : ℕ) : Term

Equations

• termNat 0 = Term.zero
• termNat x.succ = (termNat x).incr

theorem termNat_correct (f : ℕ → BitStream) (w : ℕ) (n : ℕ) : BitStream.EqualUpTo w (BitStream.ofBitVec (BitVec.ofNat w n)) ((termNat n).eval f)

def quoteThm (qMapIndexToFVar : Q(ℕ → BitStream)) (w : Q(ℕ)) (nat : ℕ) : Q(BitStream.EqualUpTo «$w» (BitStream.ofBitVec (BitVec.ofNat «$w» «$nat»)) ((termNat «$nat»).eval «$qMapIndexToFVar»))

Equations

• quoteThm qMapIndexToFVar w nat = q(⋯)

partial def first_rep (w : Q(ℕ)) (e : Q(BitStream)) : Lean.Meta.SimpM ((x : Q(BitStream)) × Q(BitStream.EqualUpTo «$w» «$e» «$x»))

Given an Expr e, return a pair e', p where e' is an expression and p is a proof that e and e' are equal on the fist w bits

def reduce_bitvec2 : Lean.Meta.Simp.Simproc

Push all ofBitVecs down to the lowest level

def introduceMapIndexToFVar : Lean.Elab.Tactic.TacticM Unit

Introduce vars which maps variable ids to the variable values.

let vars (n : Nat) : BitStream := BitStream.ofBitVec (if n = 0 then v0 else if n = 1 then v1 else if n = 2 then v2 ......)

Term.var 0 -- represent the 0th variable Term.var 1 -- represent the 1st variable

def tacticIntroduceMapIndexToFVar : Lean.ParserDescr

Equations

• tacticIntroduceMapIndexToFVar = Lean.ParserDescr.node `tacticIntroduceMapIndexToFVar 1024 (Lean.ParserDescr.nonReservedSymbol "introduceMapIndexToFVar" false)

def tacticBv_automata : Lean.ParserDescr

Create bv_automata tactic which solves equalities on bitvectors.

Equations

• tacticBv_automata = Lean.ParserDescr.node `tacticBv_automata 1024 (Lean.ParserDescr.nonReservedSymbol "bv_automata" false)

Test Cases

def alive_1 {w : ℕ} (x : BitVec w) (x_1 : BitVec w) (x_2 : BitVec w) : (x_2 &&& x_1 ^^^ x_1) + 1#w + x = x - (x_2 ||| ~~~x_1)

Equations

• ⋯ = ⋯

def false_statement {w : ℕ} (x : BitVec w) (y : BitVec w) : x = y

Equations

• ⋯ = ⋯

def test_OfNat_ofNat (x : BitVec 1) : 1 + x = x + 1

Equations

• ⋯ = ⋯

def test_BitVec_ofNat (x : BitVec 1) : 1 + x = x + 1#1

Equations

• ⋯ = ⋯

def test0 {w : ℕ} (x : BitVec (w + 1)) (y : BitVec (w + 1)) : x + 0 = x

Equations

• ⋯ = ⋯

def test_simple2 {w : ℕ} (x : BitVec (w + 1)) (y : BitVec (w + 1)) : x = x

Equations

• ⋯ = ⋯

def test1 {w : ℕ} (x : BitVec (w + 1)) (y : BitVec (w + 1)) : (x ||| y) - (x ^^^ y) = x &&& y

Equations

• ⋯ = ⋯

def test2 (x : BitVec 300) (y : BitVec 300) : (x &&& y) + (x ||| y) = x + y

Equations

• ⋯ = ⋯

def test3 (x : BitVec 300) (y : BitVec 300) : (x ||| y) - (x ^^^ y) = x &&& y

Equations

• ⋯ = ⋯

def test4 (x : BitVec 2) (y : BitVec 2) : x + -y = x - y

Equations

• ⋯ = ⋯

def test5 (x : BitVec 2) (y : BitVec 2) (z : BitVec 2) : x + y + z = z + y + x

Equations

• ⋯ = ⋯

def test6 (x : BitVec 2) (y : BitVec 2) (z : BitVec 2) : x + (y + z) = x + y + z

Equations

• ⋯ = ⋯

def test11 (x : BitVec 2) (y : BitVec 2) : x + y = (x ||| y) + (x &&& y)

Equations

• ⋯ = ⋯

def test15 (x : BitVec 2) (y : BitVec 2) : x - y = (x &&& ~~~y) - (~~~x &&& y)

Equations

• ⋯ = ⋯

def test17 (x : BitVec 2) (y : BitVec 2) : x ^^^ y = (x ||| y) - (x &&& y)

Equations

• ⋯ = ⋯

def test18 (x : BitVec 2) (y : BitVec 2) : x &&& ~~~y = (x ||| y) - y

Equations

• ⋯ = ⋯

def test19 (x : BitVec 2) (y : BitVec 2) : x &&& ~~~y = x - (x &&& y)

Equations

• ⋯ = ⋯

def test21 (x : BitVec 2) (y : BitVec 2) : ~~~(x - y) = ~~~x + y

Equations

• ⋯ = ⋯

def test23 (x : BitVec 2) (y : BitVec 2) : ~~~(x ^^^ y) = (x &&& y) + ~~~(x ||| y)

Equations

• ⋯ = ⋯

def test24 (x : BitVec 2) (y : BitVec 2) : x ||| y = (x &&& ~~~y) + y

Equations

• ⋯ = ⋯

def test25 (x : BitVec 2) (y : BitVec 2) : x &&& y = (~~~x ||| y) - ~~~x

Equations

• ⋯ = ⋯

def test26 {w : ℕ} (x : BitVec (w + 1)) (y : BitVec (w + 1)) : 1 + x + 0 = 1 + x

Equations

• ⋯ = ⋯

def test27 (x : BitVec 5) (y : BitVec 5) : 2 + x = 1 + x + 1

Equations

• ⋯ = ⋯

def test28 {w : ℕ} (x : BitVec (w + 1)) (y : BitVec (w + 1)) : x &&& x &&& x &&& x &&& x &&& x = x

Equations

• ⋯ = ⋯