From 9055dc86552b63779ed74590252294a07bb980f8 Mon Sep 17 00:00:00 2001 From: Siddharth Bhat Date: Thu, 26 Sep 2024 11:26:13 -0500 Subject: [PATCH 1/4] chore: add WIP to remind myself that I owe kim --- src/Init/Data/BitVec/Bitblast.lean | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/src/Init/Data/BitVec/Bitblast.lean b/src/Init/Data/BitVec/Bitblast.lean index a8ce5b31dd3c..1c4a572d89d1 100644 --- a/src/Init/Data/BitVec/Bitblast.lean +++ b/src/Init/Data/BitVec/Bitblast.lean @@ -26,6 +26,11 @@ expressions into expressions about individual bits in each vector. All other operations are to be PR'ed later and are already proved in https://github.com/mhk119/lean-smt/blob/bitvec/Smt/Data/Bitwise.lean. +### Example: How bitblasting work for multiplication + +- `succ` +- `zero` + -/ set_option linter.missingDocs true From 8378285fe6c79a1315205881b323a24cb1e2edb3 Mon Sep 17 00:00:00 2001 From: Siddharth Bhat Date: Fri, 4 Oct 2024 09:22:54 -0500 Subject: [PATCH 2/4] chore: tune text --- src/Init/Data/BitVec/Bitblast.lean | 80 +++++++++++++++++++++++++++--- 1 file changed, 73 insertions(+), 7 deletions(-) diff --git a/src/Init/Data/BitVec/Bitblast.lean b/src/Init/Data/BitVec/Bitblast.lean index 1c4a572d89d1..825e8ed1dffd 100644 --- a/src/Init/Data/BitVec/Bitblast.lean +++ b/src/Init/Data/BitVec/Bitblast.lean @@ -15,8 +15,79 @@ the `Fin 2^n` representation and Boolean vectors. It is still under development intended to provide a path for converting SAT and SMT solver proofs about BitVectors as vectors of bits into proofs about Lean `BitVec` values. -The module is named for the bit-blasting operation in an SMT solver that converts bitvector -expressions into expressions about individual bits in each vector. +### Example: How bitblasting works for multiplication + +We explain how the lemmas here are used for bitblasting, +by using multiplication as a prototypical example. +Other bitblasters for other operations follow the same pattern. +To bitblast a multiplication of the form `x * y`, +we must unfold the above into a form that the SAT solver understands. + +We assume that the solver already knows how to bitblast addition. +This is known to `bv_decide`, by exploiting the lemma `add_eq_adc`, +which says that `x + y : BitVec w` equals `(adc x y false).2`, +where `adc` builds an add-carry circuit in terms of the primitive operations +(bitwise and, bitwise or, bitwise xor) that bv_decide already understands. +In this way, we layer bitblasters on top of each other, +by reducing the multiplication bitblaster to an addition operation. + +The core lemma is given by `getLsbD_mul`: + +```lean + x y : BitVec w ⊢ (x * y).getLsbD i = (mulRec x y w).getLsbD i +``` + +Which says that the `i`th bit of `x * y` can be obtained by +evaluating the `i`th bit of `(mulRec x y w)`. +Once again, we assume that `bv_decide` knows how to implement `getLsbD`, +given that `mulRec` can be understood by `bv_decide`. + +We write two lemmas to enable `bv_decide` to unfold `(mulRec x y w)` +into a complete circuit, **when `w` is a known constant**`. +This is given by two recurrence lemmas, `mulRec_zero_eq` and `mulRec_succ_eq`, +which are applied repeatedly when the width is `0` and when the width is `w' + 1`: + +```lean +mulRec_zero_eq : + mulRec x y 0 = + if y.getLsbD 0 then x else 0 + +mulRec_succ_eq + mulRec x y (s + 1) = + mulRec x y s + + if y.getLsbD (s + 1) then (x <<< (s + 1)) else 0 := rfl +``` + +By repeatedly applying the lemmas `mulRec_zero_eq` and `mulRec_succ_eq`, +one obtains a circuit for multiplication. +Note that this circuit uses `BitVec.add`, `BitVec.getLsbD`, `BitVec.shiftLeft`. +Here, `BitVec.add` and `BitVec.shiftLeft` are (recursively) bitblasted by `bv_decide`, +using the lemmas `add_eq_adc` and `shiftLeft_eq_shiftLeftRec`, +and `BitVec.getLsbD` is a primitive that `bv_decide` knows how to reduce to SAT. + +The two lemmas, `mulRec_zero_eq`, and `mulRec_succ_eq`, +are used in `Std.Tactic.BVDecide.BVExpr.bitblast.blastMul` +to prove the correctness of the circuit that is built by `bv_decide`. + +```lean +def blastMul (aig : AIG BVBit) (input : AIG.BinaryRefVec aig w) : AIG.RefVecEntry BVBit w +theorem denote_blastMul (aig : AIG BVBit) (lhs rhs : BitVec w) (assign : Assignment) : + ... + ⟦(blastMul aig input).aig, (blastMul aig input).vec.get idx hidx, assign.toAIGAssignment⟧ + = + (lhs * rhs).getLsbD idx +``` + +The definition and theorem above are internal to `bv_decide`, +and use `mulRec_{zero,succ}_eq` to prove that the circuit built by `bv_decide` +computes the correct value for multiplication. + +To zoom out, therefore, we follow two steps: +First, we prove bitvector lemmas to unfold a high-level operation (such as multiplication) +into already bitblstable operations (such as addition and left shift). +We then use these lemmas to prove the correctness of the circuit that `bv_decide` builds. + +We use this workflow to implement bitblasting for all SMT-LIB2 operations. ## Main results * `x + y : BitVec w` is `(adc x y false).2`. @@ -26,11 +97,6 @@ expressions into expressions about individual bits in each vector. All other operations are to be PR'ed later and are already proved in https://github.com/mhk119/lean-smt/blob/bitvec/Smt/Data/Bitwise.lean. -### Example: How bitblasting work for multiplication - -- `succ` -- `zero` - -/ set_option linter.missingDocs true From 3843e10421cd424bfe43c45e1d25f6b515c4340b Mon Sep 17 00:00:00 2001 From: Siddharth Bhat Date: Fri, 4 Oct 2024 09:23:41 -0500 Subject: [PATCH 3/4] chore: bring back deleted text --- src/Init/Data/BitVec/Bitblast.lean | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/Init/Data/BitVec/Bitblast.lean b/src/Init/Data/BitVec/Bitblast.lean index 825e8ed1dffd..4b75b8ec87d7 100644 --- a/src/Init/Data/BitVec/Bitblast.lean +++ b/src/Init/Data/BitVec/Bitblast.lean @@ -15,6 +15,9 @@ the `Fin 2^n` representation and Boolean vectors. It is still under development intended to provide a path for converting SAT and SMT solver proofs about BitVectors as vectors of bits into proofs about Lean `BitVec` values. +The module is named for the bit-blasting operation in an SMT solver that converts bitvector +expressions into expressions about individual bits in each vector. + ### Example: How bitblasting works for multiplication We explain how the lemmas here are used for bitblasting, From 929d961b25c12ae4f0f91303d06135792cdfceec Mon Sep 17 00:00:00 2001 From: Siddharth Bhat Date: Fri, 4 Oct 2024 15:50:33 -0500 Subject: [PATCH 4/4] chore: fix typo --- src/Init/Data/BitVec/Bitblast.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Init/Data/BitVec/Bitblast.lean b/src/Init/Data/BitVec/Bitblast.lean index 4b75b8ec87d7..4934b3b07385 100644 --- a/src/Init/Data/BitVec/Bitblast.lean +++ b/src/Init/Data/BitVec/Bitblast.lean @@ -87,7 +87,7 @@ computes the correct value for multiplication. To zoom out, therefore, we follow two steps: First, we prove bitvector lemmas to unfold a high-level operation (such as multiplication) -into already bitblstable operations (such as addition and left shift). +into already bitblastable operations (such as addition and left shift). We then use these lemmas to prove the correctness of the circuit that `bv_decide` builds. We use this workflow to implement bitblasting for all SMT-LIB2 operations.