Update bv proof signature and example, after discussions with Liana.

diff --git a/proofs/signatures/ex_bv.plf b/proofs/signatures/ex_bv.plf
index 86e094efee836ff87d0d91867f74bea54a72e1c1..02cadaeab43b79cf42a52dfef0890db37935e8ed 100755 (executable)
--- 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))))))))\r
 (: (holds cln)\r
 \r
-(decl_bv_atom_var 5 a (\ bv1 (\ ba1\r
-(decl_bv_atom_var 5 b (\ bv2 (\ ba2\r
-(decl_bv_atom_const _ (bvc b0 (bvc b0 (bvc b0 (bvc b0 (bvc b0 bvn))))) (\ bv3 (\ ba3\r
-(decl_bv_atom_const _ (bvc b1 (bvc b1 (bvc b1 (bvc b1 (bvc b1 bvn))))) (\ bv4 (\ ba4\r
+(decl_bv_atom_var 5 a (\ ba1\r
+(decl_bv_atom_var 5 b (\ ba2\r
+(decl_bv_atom_const _ (bvc b0 (bvc b0 (bvc b0 (bvc b0 (bvc b0 bvn))))) (\ c (\ ba3\r
+(decl_bv_atom_const _ (bvc b1 (bvc b1 (bvc b1 (bvc b1 (bvc b1 bvn))))) (\ d (\ ba4\r
 \r
-(decl_atom (bblast bv1 4) (\ v1 (\ a1\r
-(decl_atom (bblast bv2 4) (\ v2 (\ a2\r
-(decl_atom (bblast bv3 4) (\ v3 (\ a3\r
-(decl_atom (bblast bv4 4) (\ v4 (\ a4\r
+(decl_atom (bblast a 4) (\ v1 (\ a1\r
+(decl_atom (bblast b 4) (\ v2 (\ a2\r
 \r
-; bitblasting\r
-(th_let_pf _ (bv_bbl_eq _ _ _ _ _ _ ba1 ba2 f1) (\ bf1\r
-(th_let_pf _ (bv_bbl_eq _ _ _ _ _ _ ba1 ba3 f2) (\ bf2\r
-(th_let_pf _ (bv_bbl_eq _ _ _ _ _ _ ba2 ba4 f3) (\ bf3\r
-(th_let_pf _ (bv_bbl_const _ _ _ _ ba3) (\ bf4\r
-(th_let_pf _ (bv_bbl_const _ _ _ _ ba4) (\ bf5\r
+; bitblasting terms\r
+(th_let_pf _ (bv_bbl_var _ _ _ ba1) (\ bt1\r
+(th_let_pf _ (bv_bbl_var _ _ _ ba2) (\ bt2\r
+(th_let_pf _ (bv_bbl_const _ _ _ _ ba3) (\ bt3\r
+(th_let_pf _ (bv_bbl_const _ _ _ _ ba4) (\ bt4\r
+\r
+; bitblasting formulas\r
+(th_let_pf _ (bv_bbl_eq _ _ _ _ _ bt1 bt2) (\ bf1\r
+(th_let_pf _ (bv_bbl_eq _ _ _ _ _ bt1 bt3) (\ bf2\r
+(th_let_pf _ (bv_bbl_eq _ _ _ _ _ bt2 bt4) (\ bf3\r
 \r
 ; CNFication\r
 ; a.4 V ~b.4\r
@@ -31,43 +33,25 @@
 (asf _ _ _ a1 (\ l1\r
 (ast _ _ _ a2 (\ l2\r
 (clausify_false\r
-  (contra _ (impl_elim _ _ l2 (iff_elim_2 _ _ (and_elim_1 _ _ bf1))) l1)\r
+  (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\r
 ))))) (\ C2\r
 \r
-; ~a.4 V 00000.4 \r
+; ~a.4\r
 (satlem _ _\r
 (ast _ _ _ a1 (\ l1\r
-(asf _ _ _ a3 (\ l3\r
 (clausify_false\r
-  (contra _ (impl_elim _ _ l1 (iff_elim_1 _ _ (and_elim_1 _ _ bf2))) l3)\r
-))))) (\ C3\r
+  (impl_elim _ _ l1 (iff_elim_1 _ _ (and_elim_1 _ _ (impl_elim _ _ f2 bf2))))\r
+))) (\ C3\r
 \r
-; b.4 V ~11111.4 \r
+; b.4 \r
 (satlem _ _\r
 (asf _ _ _ a2 (\ l2\r
-(ast _ _ _ a4 (\ l4\r
-(clausify_false\r
-  (contra _ (impl_elim _ _ l4 (iff_elim_2 _ _ (and_elim_1 _ _ bf3))) l2)\r
-))))) (\ C6\r
-\r
-; ~00000.4\r
-(satlem _ _\r
-(ast _ _ _ a3 (\ l3\r
-(clausify_false\r
-  (contra _ l3 (and_elim_1 _ _ bf4))\r
-))) (\ C7\r
-\r
-; 11111.4\r
-(satlem _ _\r
-(asf _ _ _ a4 (\ l4\r
 (clausify_false\r
-  (contra _ (and_elim_1 _ _ bf5) l4)\r
-))) (\ C8\r
+  (contra _ (impl_elim _ _ truth (iff_elim_2 _ _ (and_elim_1 _ _ (impl_elim _ _ f3 bf3)))) l2)\r
+))) (\ C6\r
 \r
 \r
 (satlem_simplify _ _ _ \r
-(R _ _ \r
-  (R _ _ (R _ _ C8 C6 v4) C2 v2)\r
-  (R _ _ C3 C7 v3) v1) (\ x x))\r
+(R _ _ (R _ _ C6 C2 v2) C3 v1) (\ x x))\r
 \r
-)))))))))))))))))))))))))))))))))))))))))))))))))))
\ 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 bbee2d49bca2685102b077fe270b9053aa4cc5a1..942e17df0d8447b935babf44e1033329797d487e 100755 (executable)
--- 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 8c972accfd0f7feb8f64bb8e3b98bf9b09bb1277..3fb9d13563a7b3afdfee7814ac06f7fe558f5336 100755 (executable)
--- a/proofs/signatures/th_bv.plf
+++ b/proofs/signatures/th_bv.plf
@@ -1,5 +1,3 @@
-;a = b ^ a = 0 ^ b = 1\r
-\r
 ; "bitvec" is a term of type "sort"\r
 (declare BitVec sort)\r
 \r
@@ -27,7 +25,6 @@
 (declare a_var_bv (! v var_bv (term BitVec)))\r
 \r
 \r
-\r
 ; bit vector operators\r
 (define bvoper (! x (term BitVec) \r
                (! y (term BitVec) \r
@@ -36,79 +33,102 @@
 (declare bvadd bvoper)\r
 ;....\r
 \r
-; variable used for bit-blasting (must be simply-typed)\r
-(declare bbl_var type)\r
-\r
 ; all bit-vector terms are mapped with "bv_atom" to:\r
-;  - a simply-typed term of type "bbl_var", which is used for bit-blasting\r
+;  - a simply-typed term of type "var_bv", which is necessary for bit-blasting\r
 ;  - a integer size\r
-(declare bv_atom (! x (term BitVec) (! y bbl_var (! n mpz type))))\r
+(declare bv_atom (! x (term BitVec) (! y var_bv (! n mpz type))))\r
 \r
 (declare decl_bv_atom_var (! n mpz    ; must be specified\r
                           (! x var_bv\r
-                          (! p (! w bbl_var\r
-                               (! u (bv_atom (a_var_bv x) w n)\r
-                                 (holds cln)))\r
+                          (! p (! u (bv_atom (a_var_bv x) x n)\r
+                                 (holds cln))\r
                              (holds cln)))))\r
 \r
 (declare decl_bv_atom_const (! n mpz\r
                             (! v bv\r
                             (! s (^ (bv_len v) n)\r
-                            (! p (! w bbl_var\r
+                            (! p (! w var_bv\r
                                  (! u (bv_atom (a_bv v) w n)\r
                                    (holds cln)))\r
                              (holds cln))))))\r
 \r
 \r
+; other terms here?\r
+\r
+\r
+; bit blasted terms\r
+(declare bblt type)\r
+(declare bbltn bblt)\r
+(declare bbltc (! f formula (! v bblt bblt)))\r
+\r
+; (bblast_term x y) means term x corresponds to bit level interpretation y\r
+(declare bblast_term (! x (term BitVec) (! y bblt formula)))\r
+\r
 ; a predicate to represent the n^th bit of a bitvector term\r
-(declare bblast (! x bbl_var (! n mpz formula)))\r
+(declare bblast (! x var_bv (! n mpz formula)))\r
 \r
-; bit blast  constant\r
-(program bblast_const ((x bbl_var) (v bv) (n mpz)) formula\r
-  (match v\r
-    (bvn (mp_ifneg n true (fail formula)))\r
-    ((bvc b v') (let n' (mp_add n (~ 1))\r
-                (let f (match b (b0 (not (bblast x n))) (b1 (bblast x n)))\r
-                  (mp_ifzero n' f (and f (bblast_const x v' n'))))))))\r
 \r
+; bit blast  constant\r
+(program bblast_const ((v bv) (n mpz)) bblt\r
+  (mp_ifneg n (match v (bvn bbltn) \r
+                       (default (fail bblt)))\r
+              (match v ((bvc b v') (bbltc (match b (b0 false) (b1 true)) (bblast_const v' (mp_add n (~ 1)))))\r
+                       (default (fail bblt)))))\r
+              \r
 (declare bv_bbl_const (! n mpz\r
-                      (! f formula\r
                       (! v bv\r
-                      (! x bbl_var\r
+                      (! x var_bv\r
+                      (! f bblt\r
                       (! u (bv_atom (a_bv v) x n)\r
-                      (! c (^ (bblast_const x v (mp_add n (~ 1))) f)\r
-                         (th_holds f))))))))\r
+                      (! c (^ (bblast_const v (mp_add n (~ 1))) f)\r
+                         (th_holds (bblast_term (a_bv v) f)))))))))\r
+\r
+; bit blast  variable\r
+(program bblast_var ((x var_bv) (n mpz)) bblt\r
+  (mp_ifneg n bbltn \r
+              (bbltc (bblast x n) (bblast_var x (mp_add n (~ 1))))))\r
+\r
+(declare bv_bbl_var (! n mpz\r
+                    (! x var_bv\r
+                    (! f bblt                    \r
+                    (! u (bv_atom (a_var_bv x) x n)\r
+                    (! c (^ (bblast_var x (mp_add n (~ 1))) f)\r
+                       (th_holds (bblast_term (a_var_bv x) f))))))))\r
 \r
 ; bit blast  x = y\r
-(program bblast_eq ((x bbl_var) (y bbl_var) (n mpz)) formula\r
-  (let n' (mp_add n (~ 1))\r
-  (let f (iff (bblast x n) (bblast y n))\r
-  (mp_ifzero n' f (and f (bblast_eq x y n'))))))\r
+;  for x,y of size n, it will return a conjuction (x.{n-1} = y.{n-1} ^ ( ... ^ (x.0 = y.0 ^ true)))\r
+(program bblast_eq ((x bblt) (y bblt)) formula\r
+  (match x \r
+    (bbltn (match y (bbltn true) (default (fail formula))))\r
+    ((bbltc fx x') (match y \r
+                      (bbltn (fail formula))\r
+                      ((bbltc fy y') (and (iff fx fy) (bblast_eq x' y')))))))\r
 \r
 (declare bv_bbl_eq (! x (term BitVec)\r
                    (! y (term BitVec)\r
-                   (! n mpz\r
+                   (! fx bblt\r
+                   (! fy bblt\r
                    (! f formula\r
-                   (! x' bbl_var\r
-                   (! y' bbl_var\r
-                   (! ux' (bv_atom x x' n)\r
-                   (! uy' (bv_atom y y' n)\r
-                   (! u (th_holds (= BitVec x y))\r
-                   (! c (^ (bblast_eq x' y' (mp_add n (~ 1))) f)\r
-                      (th_holds f))))))))))))\r
+                   (! ux (th_holds (bblast_term x fx))\r
+                   (! uy (th_holds (bblast_term y fy))\r
+                   (! c (^ (bblast_eq fx fy) f)\r
+                      (th_holds (impl (= BitVec x y) f)))))))))))\r
 \r
 \r
 ; rewrite rule :\r
 ; x + y = y + x\r
 (declare bvadd_symm (! x (term BitVec)\r
                     (! y (term BitVec)\r
-                    (! x' bbl_var\r
-                    (! y' bbl_var\r
+                    (! x' var_bv\r
+                    (! y' var_bv\r
                     (! n mpz\r
                     (! ux (bv_atom x x' n)\r
                     (! uy (bv_atom y y' n)\r
                        (th_holds (= BitVec (bvadd x y) (bvadd y x)))))))))))\r
 \r
+\r
+\r
+; necessary? \r
 (program calc_bvand ((a bv) (b bv)) bv\r
   (match a\r
     (bvn (match b (bvn bvn) (default (fail bv))))\r