From f342e03da57a73c2261ed2ca06c651cc4153df8a Mon Sep 17 00:00:00 2001 From: ajreynol Date: Wed, 20 Aug 2014 22:43:22 +0200 Subject: [PATCH] Update bv proof signature and example, after discussions with Liana. --- proofs/signatures/ex_bv.plf | 66 ++++++++++--------------- proofs/signatures/smt.plf | 3 ++ proofs/signatures/th_bv.plf | 96 ++++++++++++++++++++++--------------- 3 files changed, 86 insertions(+), 79 deletions(-) diff --git a/proofs/signatures/ex_bv.plf b/proofs/signatures/ex_bv.plf index 86e094efe..02cadaeab 100755 --- a/proofs/signatures/ex_bv.plf +++ b/proofs/signatures/ex_bv.plf @@ -8,22 +8,24 @@ (% f3 (th_holds (= BitVec (a_var_bv b) (a_bv (bvc b1 (bvc b1 (bvc b1 (bvc b1 (bvc b1 bvn)))))))) (: (holds cln) -(decl_bv_atom_var 5 a (\ bv1 (\ ba1 -(decl_bv_atom_var 5 b (\ bv2 (\ ba2 -(decl_bv_atom_const _ (bvc b0 (bvc b0 (bvc b0 (bvc b0 (bvc b0 bvn))))) (\ bv3 (\ ba3 -(decl_bv_atom_const _ (bvc b1 (bvc b1 (bvc b1 (bvc b1 (bvc b1 bvn))))) (\ bv4 (\ ba4 +(decl_bv_atom_var 5 a (\ ba1 +(decl_bv_atom_var 5 b (\ ba2 +(decl_bv_atom_const _ (bvc b0 (bvc b0 (bvc b0 (bvc b0 (bvc b0 bvn))))) (\ c (\ ba3 +(decl_bv_atom_const _ (bvc b1 (bvc b1 (bvc b1 (bvc b1 (bvc b1 bvn))))) (\ d (\ ba4 -(decl_atom (bblast bv1 4) (\ v1 (\ a1 -(decl_atom (bblast bv2 4) (\ v2 (\ a2 -(decl_atom (bblast bv3 4) (\ v3 (\ a3 -(decl_atom (bblast bv4 4) (\ v4 (\ a4 +(decl_atom (bblast a 4) (\ v1 (\ a1 +(decl_atom (bblast b 4) (\ v2 (\ a2 -; bitblasting -(th_let_pf _ (bv_bbl_eq _ _ _ _ _ _ ba1 ba2 f1) (\ bf1 -(th_let_pf _ (bv_bbl_eq _ _ _ _ _ _ ba1 ba3 f2) (\ bf2 -(th_let_pf _ (bv_bbl_eq _ _ _ _ _ _ ba2 ba4 f3) (\ bf3 -(th_let_pf _ (bv_bbl_const _ _ _ _ ba3) (\ bf4 -(th_let_pf _ (bv_bbl_const _ _ _ _ ba4) (\ bf5 +; bitblasting terms +(th_let_pf _ (bv_bbl_var _ _ _ ba1) (\ bt1 +(th_let_pf _ (bv_bbl_var _ _ _ ba2) (\ bt2 +(th_let_pf _ (bv_bbl_const _ _ _ _ ba3) (\ bt3 +(th_let_pf _ (bv_bbl_const _ _ _ _ ba4) (\ bt4 + +; bitblasting formulas +(th_let_pf _ (bv_bbl_eq _ _ _ _ _ bt1 bt2) (\ bf1 +(th_let_pf _ (bv_bbl_eq _ _ _ _ _ bt1 bt3) (\ bf2 +(th_let_pf _ (bv_bbl_eq _ _ _ _ _ bt2 bt4) (\ bf3 ; CNFication ; a.4 V ~b.4 @@ -31,43 +33,25 @@ (asf _ _ _ a1 (\ l1 (ast _ _ _ a2 (\ l2 (clausify_false - (contra _ (impl_elim _ _ l2 (iff_elim_2 _ _ (and_elim_1 _ _ bf1))) l1) + (contra _ (impl_elim _ _ l2 (iff_elim_2 _ _ (and_elim_1 _ _ (impl_elim _ _ f1 bf1)))) l1) ; notice at the intermost we impl_elim, which converts from atom to bit-blasting representation ))))) (\ C2 -; ~a.4 V 00000.4 +; ~a.4 (satlem _ _ (ast _ _ _ a1 (\ l1 -(asf _ _ _ a3 (\ l3 (clausify_false - (contra _ (impl_elim _ _ l1 (iff_elim_1 _ _ (and_elim_1 _ _ bf2))) l3) -))))) (\ C3 + (impl_elim _ _ l1 (iff_elim_1 _ _ (and_elim_1 _ _ (impl_elim _ _ f2 bf2)))) +))) (\ C3 -; b.4 V ~11111.4 +; b.4 (satlem _ _ (asf _ _ _ a2 (\ l2 -(ast _ _ _ a4 (\ l4 -(clausify_false - (contra _ (impl_elim _ _ l4 (iff_elim_2 _ _ (and_elim_1 _ _ bf3))) l2) -))))) (\ C6 - -; ~00000.4 -(satlem _ _ -(ast _ _ _ a3 (\ l3 -(clausify_false - (contra _ l3 (and_elim_1 _ _ bf4)) -))) (\ C7 - -; 11111.4 -(satlem _ _ -(asf _ _ _ a4 (\ l4 (clausify_false - (contra _ (and_elim_1 _ _ bf5) l4) -))) (\ C8 + (contra _ (impl_elim _ _ truth (iff_elim_2 _ _ (and_elim_1 _ _ (impl_elim _ _ f3 bf3)))) l2) +))) (\ C6 (satlem_simplify _ _ _ -(R _ _ - (R _ _ (R _ _ C8 C6 v4) C2 v2) - (R _ _ C3 C7 v3) v1) (\ x x)) +(R _ _ (R _ _ C6 C2 v2) C3 v1) (\ x x)) -))))))))))))))))))))))))))))))))))))))))))))))))))) \ No newline at end of file +))))))))))))))))))))))))))))))))))))))))))) \ No newline at end of file diff --git a/proofs/signatures/smt.plf b/proofs/signatures/smt.plf index bbee2d49b..942e17df0 100755 --- a/proofs/signatures/smt.plf +++ b/proofs/signatures/smt.plf @@ -104,6 +104,9 @@ (! r2 (th_holds (not f)) (th_holds false))))) +; truth +(declare truth (th_holds true)) + ;; not not (declare not_not_intro diff --git a/proofs/signatures/th_bv.plf b/proofs/signatures/th_bv.plf index 8c972accf..3fb9d1356 100755 --- a/proofs/signatures/th_bv.plf +++ b/proofs/signatures/th_bv.plf @@ -1,5 +1,3 @@ -;a = b ^ a = 0 ^ b = 1 - ; "bitvec" is a term of type "sort" (declare BitVec sort) @@ -27,7 +25,6 @@ (declare a_var_bv (! v var_bv (term BitVec))) - ; bit vector operators (define bvoper (! x (term BitVec) (! y (term BitVec) @@ -36,79 +33,102 @@ (declare bvadd bvoper) ;.... -; variable used for bit-blasting (must be simply-typed) -(declare bbl_var type) - ; all bit-vector terms are mapped with "bv_atom" to: -; - a simply-typed term of type "bbl_var", which is used for bit-blasting +; - a simply-typed term of type "var_bv", which is necessary for bit-blasting ; - a integer size -(declare bv_atom (! x (term BitVec) (! y bbl_var (! n mpz type)))) +(declare bv_atom (! x (term BitVec) (! y var_bv (! n mpz type)))) (declare decl_bv_atom_var (! n mpz ; must be specified (! x var_bv - (! p (! w bbl_var - (! u (bv_atom (a_var_bv x) w n) - (holds cln))) + (! p (! u (bv_atom (a_var_bv x) x n) + (holds cln)) (holds cln))))) (declare decl_bv_atom_const (! n mpz (! v bv (! s (^ (bv_len v) n) - (! p (! w bbl_var + (! p (! w var_bv (! u (bv_atom (a_bv v) w n) (holds cln))) (holds cln)))))) +; other terms here? + + +; bit blasted terms +(declare bblt type) +(declare bbltn bblt) +(declare bbltc (! f formula (! v bblt bblt))) + +; (bblast_term x y) means term x corresponds to bit level interpretation y +(declare bblast_term (! x (term BitVec) (! y bblt formula))) + ; a predicate to represent the n^th bit of a bitvector term -(declare bblast (! x bbl_var (! n mpz formula))) +(declare bblast (! x var_bv (! n mpz formula))) -; bit blast constant -(program bblast_const ((x bbl_var) (v bv) (n mpz)) formula - (match v - (bvn (mp_ifneg n true (fail formula))) - ((bvc b v') (let n' (mp_add n (~ 1)) - (let f (match b (b0 (not (bblast x n))) (b1 (bblast x n))) - (mp_ifzero n' f (and f (bblast_const x v' n')))))))) +; bit blast constant +(program bblast_const ((v bv) (n mpz)) bblt + (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 formula (! v bv - (! x bbl_var + (! x var_bv + (! f bblt (! u (bv_atom (a_bv v) x n) - (! c (^ (bblast_const x v (mp_add n (~ 1))) f) - (th_holds f)))))))) + (! c (^ (bblast_const v (mp_add n (~ 1))) f) + (th_holds (bblast_term (a_bv v) f))))))))) + +; bit blast variable +(program bblast_var ((x var_bv) (n mpz)) bblt + (mp_ifneg n bbltn + (bbltc (bblast x n) (bblast_var x (mp_add n (~ 1)))))) + +(declare bv_bbl_var (! n mpz + (! x var_bv + (! f bblt + (! u (bv_atom (a_var_bv x) x n) + (! c (^ (bblast_var x (mp_add n (~ 1))) f) + (th_holds (bblast_term (a_var_bv x) f)))))))) ; bit blast x = y -(program bblast_eq ((x bbl_var) (y bbl_var) (n mpz)) formula - (let n' (mp_add n (~ 1)) - (let f (iff (bblast x n) (bblast y n)) - (mp_ifzero n' f (and f (bblast_eq x y n')))))) +; for x,y of size n, it will return a conjuction (x.{n-1} = y.{n-1} ^ ( ... ^ (x.0 = y.0 ^ true))) +(program bblast_eq ((x bblt) (y bblt)) formula + (match x + (bbltn (match y (bbltn true) (default (fail formula)))) + ((bbltc fx x') (match y + (bbltn (fail formula)) + ((bbltc fy y') (and (iff fx fy) (bblast_eq x' y'))))))) (declare bv_bbl_eq (! x (term BitVec) (! y (term BitVec) - (! n mpz + (! fx bblt + (! fy bblt (! f formula - (! x' bbl_var - (! y' bbl_var - (! ux' (bv_atom x x' n) - (! uy' (bv_atom y y' n) - (! u (th_holds (= BitVec x y)) - (! c (^ (bblast_eq x' y' (mp_add n (~ 1))) f) - (th_holds f)))))))))))) + (! ux (th_holds (bblast_term x fx)) + (! uy (th_holds (bblast_term y fy)) + (! c (^ (bblast_eq fx fy) f) + (th_holds (impl (= BitVec x y) f))))))))))) ; rewrite rule : ; x + y = y + x (declare bvadd_symm (! x (term BitVec) (! y (term BitVec) - (! x' bbl_var - (! y' bbl_var + (! x' var_bv + (! y' var_bv (! n mpz (! ux (bv_atom x x' n) (! uy (bv_atom y y' n) (th_holds (= BitVec (bvadd x y) (bvadd y x))))))))))) + + +; necessary? (program calc_bvand ((a bv) (b bv)) bv (match a (bvn (match b (bvn bvn) (default (fail bv)))) -- 2.30.2