diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2014-08-08 14:13:49 +0200 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2014-08-08 14:13:49 +0200 |
| commit | 90217b1d4662c536ba5b3e05f28b1ae636c54342 (patch) | |
| tree | e44f84cea789174bc4f864d94fee9fb3721d8a39 | |
| parent | 78dd401e00978ae5f76558965d9c536fc6fe63a2 (diff) | |
Add draft of BV proof signature (incomplete) and example proof.
| -rwxr-xr-x | proofs/signatures/ex_bv.plf | 73 | ||||
| -rwxr-xr-x | proofs/signatures/th_bv.plf | 125 |
2 files changed, 198 insertions, 0 deletions
diff --git a/proofs/signatures/ex_bv.plf b/proofs/signatures/ex_bv.plf new file mode 100755 index 000000000..86e094efe --- /dev/null +++ b/proofs/signatures/ex_bv.plf @@ -0,0 +1,73 @@ +; a = b ^ a = 00000 ^ b = 11111 is UNSAT
+
+(check
+(% a var_bv
+(% b var_bv
+(% f1 (th_holds (= BitVec (a_var_bv a) (a_var_bv b)))
+(% f2 (th_holds (= BitVec (a_var_bv a) (a_bv (bvc b0 (bvc b0 (bvc b0 (bvc b0 (bvc b0 bvn))))))))
+(% 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_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
+
+; 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
+
+; CNFication
+; a.4 V ~b.4
+(satlem _ _
+(asf _ _ _ a1 (\ l1
+(ast _ _ _ a2 (\ l2
+(clausify_false
+ (contra _ (impl_elim _ _ l2 (iff_elim_2 _ _ (and_elim_1 _ _ bf1))) l1)
+))))) (\ C2
+
+; ~a.4 V 00000.4
+(satlem _ _
+(ast _ _ _ a1 (\ l1
+(asf _ _ _ a3 (\ l3
+(clausify_false
+ (contra _ (impl_elim _ _ l1 (iff_elim_1 _ _ (and_elim_1 _ _ bf2))) l3)
+))))) (\ C3
+
+; b.4 V ~11111.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
+
+
+(satlem_simplify _ _ _
+(R _ _
+ (R _ _ (R _ _ C8 C6 v4) C2 v2)
+ (R _ _ C3 C7 v3) v1) (\ x x))
+
+)))))))))))))))))))))))))))))))))))))))))))))))))))
\ No newline at end of file diff --git a/proofs/signatures/th_bv.plf b/proofs/signatures/th_bv.plf new file mode 100755 index 000000000..8c972accf --- /dev/null +++ b/proofs/signatures/th_bv.plf @@ -0,0 +1,125 @@ +;a = b ^ a = 0 ^ b = 1
+
+; "bitvec" is a term of type "sort"
+(declare BitVec sort)
+
+; bit type
+(declare bit type)
+(declare b0 bit)
+(declare b1 bit)
+
+; bit vector type
+(declare bv type)
+(declare bvn bv)
+(declare bvc (! b bit (! v bv bv)))
+; a bv constant term
+(declare a_bv (! v bv (term BitVec)))
+
+; calculate the length of a bitvector
+(program bv_len ((v bv)) mpz
+ (match v
+ (bvn 0)
+ ((bvc b v') (mp_add (bv_len v') 1))))
+
+; a bv variable
+(declare var_bv type)
+; a bv variable term
+(declare a_var_bv (! v var_bv (term BitVec)))
+
+
+
+; bit vector operators
+(define bvoper (! x (term BitVec)
+ (! y (term BitVec)
+ (term BitVec))))
+(declare bvand bvoper)
+(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 integer size
+(declare bv_atom (! x (term BitVec) (! y bbl_var (! 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)))
+ (holds cln)))))
+
+(declare decl_bv_atom_const (! n mpz
+ (! v bv
+ (! s (^ (bv_len v) n)
+ (! p (! w bbl_var
+ (! u (bv_atom (a_bv v) w n)
+ (holds cln)))
+ (holds cln))))))
+
+
+; a predicate to represent the n^th bit of a bitvector term
+(declare bblast (! x bbl_var (! 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'))))))))
+
+(declare bv_bbl_const (! n mpz
+ (! f formula
+ (! v bv
+ (! x bbl_var
+ (! u (bv_atom (a_bv v) x n)
+ (! c (^ (bblast_const x v (mp_add n (~ 1))) f)
+ (th_holds 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'))))))
+
+(declare bv_bbl_eq (! x (term BitVec)
+ (! y (term BitVec)
+ (! n mpz
+ (! 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))))))))))))
+
+
+; rewrite rule :
+; x + y = y + x
+(declare bvadd_symm (! x (term BitVec)
+ (! y (term BitVec)
+ (! x' bbl_var
+ (! y' bbl_var
+ (! n mpz
+ (! ux (bv_atom x x' n)
+ (! uy (bv_atom y y' n)
+ (th_holds (= BitVec (bvadd x y) (bvadd y x)))))))))))
+
+(program calc_bvand ((a bv) (b bv)) bv
+ (match a
+ (bvn (match b (bvn bvn) (default (fail bv))))
+ ((bvc ba a') (match b
+ ((bvc bb b') (bvc (match ba (b0 b0) (b1 bb)) (calc_bvand a' b')))
+ (default (fail bv))))))
+
+; rewrite rule (w constants) :
+; a & b = c
+(declare bvand_const (! c bv
+ (! a bv
+ (! b bv
+ (! u (^ (calc_bvand a b) c)
+ (th_holds (= BitVec (bvand (a_bv a) (a_bv b)) (a_bv c))))))))
\ No newline at end of file |