8b5443eb22
This is the first step towards fixing the issue of not having mutual recursion between the `Bool` and `BitVec` fragment of `QF_BV` in `bv_decide`. This PR adds support for `BitVec.ofBool` by doing the following: 1. Introduce a new mechanism into the reification engine that allows us to add additional lemmas to the top level on the fly as we are traversing the expression tree. 2. If we encounter an expression `BitVec.ofBool boolExpr` we reify `boolExpr` and then abstract `BitVec.ofBool boolExpr` as some atom `a` 3. We add two lemmas `boolExpr = true -> a = 1#1` and `boolExpr = false -> a = 0#1`. This mirrors the full behavior of `BitVec.ofBool` and thus makes our atom `a` correctly interpreted again. In order to do the reification in step 2 mutual recursion in the reification engine is required. For this reason I started pulling out logic from the, now rather large, mutual block into other files and document the invariants that they assume explicitly.
40 lines
1.1 KiB
Text
40 lines
1.1 KiB
Text
import Std.Tactic.BVDecide
|
|
|
|
open BitVec
|
|
|
|
set_option bv.ac_nf false
|
|
|
|
theorem bitwise_unit_1 {x y : BitVec 64} : ~~~(x &&& y) = (~~~x ||| ~~~y) := by
|
|
bv_decide
|
|
|
|
theorem bitwise_unit_1' {x y : BitVec 64} : ~~~(BitVec.and x y) = ((BitVec.not x) ||| ~~~y) := by
|
|
bv_decide
|
|
|
|
theorem bitwise_unit_2 {x : BitVec 64} : x ^^^ x = 0 := by
|
|
bv_decide
|
|
|
|
theorem bitwise_unit_2' {x : BitVec 64} : (BitVec.xor x x) = 0 := by
|
|
bv_decide
|
|
|
|
theorem bitwise_unit_3 {x : BitVec 64} : (x ^^^ x).getLsbD 32 = false := by
|
|
bv_decide
|
|
|
|
theorem bitwise_unit_4 {x : BitVec 64} : (x ^^^ ~~~x).getLsbD 32 = true := by
|
|
bv_decide
|
|
|
|
theorem bitwise_unit_5 {x : BitVec 64} : (x ^^^ ~~~x).getLsbD 128 = false := by
|
|
bv_decide
|
|
|
|
theorem bitwise_unit_6 {x : BitVec 64} : (x ^^^ ~~~x).getLsbD 63 = (x ^^^ ~~~x).msb := by
|
|
bv_decide
|
|
|
|
theorem bitwise_unit_7 (x : BitVec 32) : x ^^^ 123#32 = 123#'(by decide) ^^^ x := by
|
|
bv_decide
|
|
|
|
theorem bitwise_unit_8 (x : BitVec 32) : BitVec.ofBool (x.getLsbD 0) = x.extractLsb' 0 1 := by
|
|
bv_decide
|
|
|
|
theorem bitwise_unit_9 (x y : BitVec 32) :
|
|
BitVec.ofBool (x.getLsbD 0 ^^ y.getLsbD 0) = BitVec.ofBool ((x ^^^ y).getLsbD 0) := by
|
|
bv_decide
|
|
|