diff options
Diffstat (limited to 'proofs/signatures/th_bv_bitblast.plf')
-rw-r--r-- | proofs/signatures/th_bv_bitblast.plf | 220 |
1 files changed, 131 insertions, 89 deletions
diff --git a/proofs/signatures/th_bv_bitblast.plf b/proofs/signatures/th_bv_bitblast.plf index 8e8c51857..3cc1ec296 100644 --- a/proofs/signatures/th_bv_bitblast.plf +++ b/proofs/signatures/th_bv_bitblast.plf @@ -4,7 +4,7 @@ (declare bbltc (! f formula (! v bblt bblt))) ; calculate the length of a bit-blasted term -(program bblt_len ((v bblt)) mpz +(program bblt_len ((v bblt)) mpz (match v (bbltn 0) ((bbltc b v') (mp_add (bblt_len v') 1)))) @@ -25,6 +25,7 @@ (bblast_term n x y))))) +; Binds a symbol to the bblast_term to be used later on. (declare decl_bblast (! n mpz (! b bblt @@ -34,6 +35,16 @@ (! u (! v (bblast_term n t b) (holds cln)) (holds cln)))))))) +(declare decl_bblast_with_alias + (! n mpz + (! b bblt + (! t (term (BitVec n)) + (! a (term (BitVec n)) + (! bb (bblast_term n t b) + (! e (th_holds (= _ t a)) + (! s (^ (bblt_len b) n) + (! u (! v (bblast_term n a b) (holds cln)) + (holds cln)))))))))) ; a predicate to represent the n^th bit of a bitvector term (declare bitof @@ -46,31 +57,31 @@ ;; BITBLASTING RULES ;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; BITBLAST CONSTANT ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; (program bblast_const ((v bv) (n mpz)) bblt - (mp_ifneg n (match v (bvn bbltn) + (mp_ifneg n (match v (bvn bbltn) (default (fail bblt))) (match v ((bvc b v') (bbltc (match b (b0 false) (b1 true)) (bblast_const v' (mp_add n (~ 1))))) (default (fail bblt))))) - + (declare bv_bbl_const (! n mpz (! f bblt (! v bv (! c (^ (bblast_const v (mp_add n (~ 1))) f) (bblast_term n (a_bv n v) f)))))) - + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; BITBLAST VARIABLE ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; (program bblast_var ((x var_bv) (n mpz)) bblt - (mp_ifneg n bbltn + (mp_ifneg n bbltn (bbltc (bitof x n) (bblast_var x (mp_add n (~ 1)))))) (declare bv_bbl_var (! n mpz @@ -79,18 +90,16 @@ (! c (^ (bblast_var x (mp_add n (~ 1))) f) (bblast_term n (a_var_bv n x) f)))))) - ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; BITBLAST CONCAT ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; (program bblast_concat ((x bblt) (y bblt)) bblt - (match x + (match x (bbltn (match y ((bbltc by y') (bbltc by (bblast_concat x y'))) (bbltn bbltn))) ((bbltc bx x') (bbltc bx (bblast_concat x' y))))) - - + (declare bv_bbl_concat (! n mpz (! m mpz (! m1 mpz @@ -104,36 +113,34 @@ (! c (^ (bblast_concat xb yb ) rb) (bblast_term n (concat n m m1 x y) rb))))))))))))) - ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; BITBLAST EXTRACT ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; (program bblast_extract_rec ((x bblt) (i mpz) (j mpz) (n mpz)) bblt - (match x + (match x ((bbltc bx x') (mp_ifneg (mpz_sub (mpz_sub j n) 1) (mp_ifneg (mpz_sub (mpz_sub n i) 1) (bbltc bx (bblast_extract_rec x' i j (mpz_sub n 1))) (bblast_extract_rec x' i j (mpz_sub n 1))) - + bbltn)) (bbltn bbltn))) (program bblast_extract ((x bblt) (i mpz) (j mpz) (n mpz)) bblt - (bblast_extract_rec x i j (mpz_sub n 1))) + (bblast_extract_rec x i j (mpz_sub n 1))) (declare bv_bbl_extract (! n mpz (! i mpz (! j mpz (! m mpz - (! x (term (BitVec m)) + (! x (term (BitVec m)) (! xb bblt (! rb bblt (! xbb (bblast_term m x xb) (! c ( ^ (bblast_extract xb i j m) rb) (bblast_term n (extract n i j m x) rb))))))))))) - ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; BITBLAST ZERO/SIGN EXTEND ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; @@ -148,42 +155,38 @@ (declare bv_bbl_zero_extend (! n mpz (! k mpz (! m mpz - (! x (term (BitVec m)) + (! x (term (BitVec m)) (! xb bblt (! rb bblt (! xbb (bblast_term m x xb) (! c ( ^ (bblast_zextend xb k m) rb) (bblast_term n (zero_extend n k m x) rb)))))))))) - (program bblast_sextend ((x bblt) (i mpz)) bblt (match x (bbltn (fail bblt)) - ((bbltc xb x') (extend_rec x (mpz_sub i 1) xb)))) + ((bbltc xb x') (extend_rec x (mpz_sub i 1) xb)))) (declare bv_bbl_sign_extend (! n mpz (! k mpz (! m mpz - (! x (term (BitVec m)) + (! x (term (BitVec m)) (! xb bblt (! rb bblt (! xbb (bblast_term m x xb) (! c ( ^ (bblast_sextend xb k m) rb) (bblast_term n (sign_extend n k m x) rb)))))))))) - - - + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; BITBLAST BVAND ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - + (program bblast_bvand ((x bblt) (y bblt)) bblt - (match x + (match x (bbltn (match y (bbltn bbltn) (default (fail bblt)))) - ((bbltc bx x') (match y + ((bbltc bx x') (match y (bbltn (fail bblt)) ((bbltc by y') (bbltc (and bx by) (bblast_bvand x' y'))))))) - - + (declare bv_bbl_bvand (! n mpz (! x (term (BitVec n)) (! y (term (BitVec n)) @@ -199,11 +202,10 @@ ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; (program bblast_bvnot ((x bblt)) bblt - (match x - (bbltn bbltn) + (match x + (bbltn bbltn) ((bbltc bx x') (bbltc (not bx) (bblast_bvnot x'))))) - - + (declare bv_bbl_bvnot (! n mpz (! x (term (BitVec n)) (! xb bblt @@ -215,15 +217,14 @@ ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; BITBLAST BVOR ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - + (program bblast_bvor ((x bblt) (y bblt)) bblt - (match x + (match x (bbltn (match y (bbltn bbltn) (default (fail bblt)))) - ((bbltc bx x') (match y + ((bbltc bx x') (match y (bbltn (fail bblt)) ((bbltc by y') (bbltc (or bx by) (bblast_bvor x' y'))))))) - - + (declare bv_bbl_bvor (! n mpz (! x (term (BitVec n)) (! y (term (BitVec n)) @@ -238,15 +239,14 @@ ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; BITBLAST BVXOR ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - + (program bblast_bvxor ((x bblt) (y bblt)) bblt - (match x + (match x (bbltn (match y (bbltn bbltn) (default (fail bblt)))) - ((bbltc bx x') (match y + ((bbltc bx x') (match y (bbltn (fail bblt)) ((bbltc by y') (bbltc (xor bx by) (bblast_bvxor x' y'))))))) - - + (declare bv_bbl_bvxor (! n mpz (! x (term (BitVec n)) (! y (term (BitVec n)) @@ -262,8 +262,8 @@ ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; BITBLAST BVADD ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - -;; return the carry bit after adding x y + +;; return the carry bit after adding x y ;; FIXME: not the most efficient thing in the world (program bblast_bvadd_carry ((a bblt) (b bblt) (carry formula)) formula (match a @@ -272,7 +272,7 @@ (bbltn (fail formula)) ((bbltc bi b') (or (and ai bi) (and (xor ai bi) (bblast_bvadd_carry a' b' carry)))))))) -;; ripple carry adder where carry is the initial carry bit +;; ripple carry adder where carry is the initial carry bit (program bblast_bvadd ((a bblt) (b bblt) (carry formula)) bblt (match a ( bbltn (match b (bbltn bbltn) (default (fail bblt)))) @@ -280,8 +280,35 @@ (bbltn (fail bblt)) ((bbltc bi b') (bbltc (xor (xor ai bi) (bblast_bvadd_carry a' b' carry)) (bblast_bvadd a' b' carry))))))) - - + + +(program reverse_help ((x bblt) (acc bblt)) bblt +(match x + (bbltn acc) + ((bbltc xi x') (reverse_help x' (bbltc xi acc))))) + + +(program reverseb ((x bblt)) bblt + (reverse_help x bbltn)) + + +; AJR: use this version? +;(program bblast_bvadd_2h ((a bblt) (b bblt) (carry formula)) bblt +;(match a +; ( bbltn (match b (bbltn bbltn) (default (fail bblt)))) +; ((bbltc ai a') (match b +; (bbltn (fail bblt)) +; ((bbltc bi b') +; (let carry' (or (and ai bi) (and (xor ai bi) carry)) +; (bbltc (xor (xor ai bi) carry) +; (bblast_bvadd_2h a' b' carry')))))))) + +;(program bblast_bvadd_2 ((a bblt) (b bblt) (carry formula)) bblt +;(let ar (reverseb a) ;; reverse a and b so that we can build the circuit +;(let br (reverseb b) ;; from the least significant bit up +;(let ret (bblast_bvadd_2h ar br carry) +; (reverseb ret))))) + (declare bv_bbl_bvadd (! n mpz (! x (term (BitVec n)) (! y (term (BitVec n)) @@ -293,7 +320,6 @@ (! c (^ (bblast_bvadd xb yb false) rb) (bblast_term n (bvadd n x y) rb))))))))))) - ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; BITBLAST BVNEG ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; @@ -304,8 +330,8 @@ (program bblast_bvneg ((x bblt) (n mpz)) bblt (bblast_bvadd (bblast_bvnot x) (bblast_zero n) true)) - - + + (declare bv_bbl_bvneg (! n mpz (! x (term (BitVec n)) (! xb bblt @@ -319,23 +345,14 @@ ;; BITBLAST BVMUL ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - -;; shift add multiplier - -(program reverse_help ((x bblt) (acc bblt)) bblt -(match x - (bbltn acc) - ((bbltc xi x') (reverse_help x' (bbltc xi acc))))) - -(program reverseb ((x bblt)) bblt - (reverse_help x bbltn)) +;; shift add multiplier ;; (program concat ((a bblt) (b bblt)) bblt ;; (match a (bbltn b) ;; ((bbltc ai a') (bbltc ai (concat a' b))))) - + (program top_k_bits ((a bblt) (k mpz)) bblt (mp_ifzero k bbltn (match a (bbltn (fail bblt)) @@ -344,7 +361,7 @@ (program bottom_k_bits ((a bblt) (k mpz)) bblt (reverseb (top_k_bits (reverseb a) k))) -;; assumes the least signigicant bit is at the beginning of the list +;; assumes the least signigicant bit is at the beginning of the list (program k_bit ((a bblt) (k mpz)) formula (mp_ifneg k (fail formula) (match a (bbltn (fail formula)) @@ -353,7 +370,7 @@ (program and_with_bit ((a bblt) (bt formula)) bblt (match a (bbltn bbltn) ((bbltc ai a') (bbltc (and bt ai) (and_with_bit a' bt))))) - + ;; a is going to be the current result ;; carry is going to be false initially ;; b is the and of a and b[k] @@ -377,19 +394,19 @@ (let ak (top_k_bits a k') (let b' (and_with_bit ak (k_bit b k)) (mp_ifzero (mpz_sub k' 1) - (mult_step_k_h res b' bbltn false k) + (mult_step_k_h res b' bbltn false k) (let res' (mult_step_k_h res b' bbltn false k) (mult_step a b (reverseb res') n (mp_add k 1)))))))) (program bblast_bvmul ((a bblt) (b bblt) (n mpz)) bblt -(let ar (reverseb a) ;; reverse a and b so that we can build the circuit +(let ar (reverseb a) ;; reverse a and b so that we can build the circuit (let br (reverseb b) ;; from the least significant bit up (let res (and_with_bit ar (k_bit br 0)) - (mp_ifzero (mpz_sub n 1) ;; if multiplying 1 bit numbers no need to call mult_step + (mp_ifzero (mpz_sub n 1) ;; if multiplying 1 bit numbers no need to call mult_step res (mult_step ar br res n 1)))))) - + (declare bv_bbl_bvmul (! n mpz (! x (term (BitVec n)) (! y (term (BitVec n)) @@ -402,18 +419,18 @@ (bblast_term n (bvmul n x y) rb))))))))))) - + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; BITBLAST EQUALS ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - + ; bit blast x = y ; for x,y of size n, it will return a conjuction (x.0 = y.0 ^ ( ... ^ (x.{n-1} = y.{n-1}))) ; f is the accumulator formula that builds the equality in the right order (program bblast_eq_rec ((x bblt) (y bblt) (f formula)) formula - (match x + (match x (bbltn (match y (bbltn f) (default (fail formula)))) - ((bbltc fx x') (match y + ((bbltc fx x') (match y (bbltn (fail formula)) ((bbltc fy y') (bblast_eq_rec x' y' (and (iff fx fy) f))))) (default (fail formula)))) @@ -423,7 +440,23 @@ ((bbltc bx x') (match y ((bbltc by y') (bblast_eq_rec x' y' (iff bx by))) (default (fail formula)))) (default (fail formula)))) - + + +;; TODO: a temporary bypass for rewrites that we don't support yet. As soon +;; as we do, remove this rule. + +(declare bv_bbl_=_false + (! n mpz + (! x (term (BitVec n)) + (! y (term (BitVec n)) + (! bx bblt + (! by bblt + (! f formula + (! bbx (bblast_term n x bx) + (! bby (bblast_term n y by) + (! c (^ (bblast_eq bx by) f) + (th_holds (iff (= (BitVec n) x y) false)))))))))))) + (declare bv_bbl_= (! n mpz (! x (term (BitVec n)) @@ -436,11 +469,22 @@ (! c (^ (bblast_eq bx by) f) (th_holds (iff (= (BitVec n) x y) f)))))))))))) - +(declare bv_bbl_=_swap + (! n mpz + (! x (term (BitVec n)) + (! y (term (BitVec n)) + (! bx bblt + (! by bblt + (! f formula + (! bbx (bblast_term n x bx) + (! bby (bblast_term n y by) + (! c (^ (bblast_eq by bx) f) + (th_holds (iff (= (BitVec n) x y) f)))))))))))) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; BITBLAST BVULT ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - + (program bblast_bvult ((x bblt) (y bblt) (n mpz)) formula (match x ( bbltn (fail formula)) @@ -465,7 +509,7 @@ ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; BITBLAST BVSLT ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - + (program bblast_bvslt ((x bblt) (y bblt) (n mpz)) formula (match x ( bbltn (fail formula)) @@ -488,7 +532,6 @@ (! bby (bblast_term n y by) (! c (^ (bblast_bvslt bx by n) f) (th_holds (iff (bvslt n x y) f)))))))))))) - ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; @@ -525,8 +568,8 @@ ;; REWRITE RULES ;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - - + + ; rewrite rule : ; x + y = y + x (declare bvadd_symm @@ -534,7 +577,7 @@ (! x (term (BitVec n)) (! y (term (BitVec n)) (th_holds (= (BitVec n) (bvadd _ x y) (bvadd _ y x))))))) - + ;; (declare bvcrazy_rewrite ;; (! n mpz ;; (! x (term (BitVec n)) @@ -546,12 +589,12 @@ ;; (! s (^ (rewrite_scc xn yn) true) ;; (! u (! x (term (BitVec n)) (holds cln)) ;; (holds cln))))))))))) - + ;; (th_holds (= (BitVec n) (bvadd x y) (bvadd y x))))))) - - -; necessary? + + +; necessary? ;; (program calc_bvand ((a bv) (b bv)) bv ;; (match a ;; (bvn (match b (bvn bvn) (default (fail bv)))) @@ -560,7 +603,7 @@ ;; (default (fail bv)))))) ;; ; rewrite rule (w constants) : -;; ; a & b = c +;; ; a & b = c ;; (declare bvand_const (! c bv ;; (! a bv ;; (! b bv @@ -568,7 +611,7 @@ ;; (th_holds (= BitVec (bvand (a_bv a) (a_bv b)) (a_bv c)))))))) -;; making constant bit-vectors +;; making constant bit-vectors (program mk_ones ((n mpz)) bv (mp_ifzero n bvn (bvc b1 (mk_ones (mpz_sub n 1))))) @@ -576,7 +619,7 @@ (mp_ifzero n bvn (bvc b0 (mk_ones (mpz_sub n 1))))) - + ;; (bvxnor a b) => (bvnot (bvxor a b)) ;; (declare bvxnor_elim ;; (! n mpz @@ -603,7 +646,7 @@ ;; (! rwb (rw_term _ b (a_bv _ zero_bits)) ;; (rw_term _ (bvxor _ a b) ;; a')))))))))) - + ;; ;; (bvxor a 11) => (bvnot a) ;; (declare bvxor_one ;; (! n mpz @@ -617,7 +660,7 @@ ;; (rw_term _ (bvxor _ a b) ;; (bvnot _ a'))))))))))) - + ;; ;; (bvnot (bvnot a)) => a ;; (declare bvnot_idemp ;; (! n mpz @@ -626,4 +669,3 @@ ;; (! rwa (rw_term _ a a') ;; (rw_term _ (bvnot _ (bvnot _ a)) ;; a')))))) - |