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

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))))