diff options
Diffstat (limited to 'proofs/signatures')
-rwxr-xr-x | proofs/signatures/ex_bv.plf | 112 | ||||
-rwxr-xr-x | proofs/signatures/th_bv.plf | 288 |
2 files changed, 200 insertions, 200 deletions
diff --git a/proofs/signatures/ex_bv.plf b/proofs/signatures/ex_bv.plf index 02cadaeab..ae585e455 100755 --- a/proofs/signatures/ex_bv.plf +++ b/proofs/signatures/ex_bv.plf @@ -1,57 +1,57 @@ -; 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 (\ 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 a 4) (\ v1 (\ a1
-(decl_atom (bblast b 4) (\ v2 (\ a2
-
-; 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
-(satlem _ _
-(asf _ _ _ a1 (\ l1
-(ast _ _ _ a2 (\ l2
-(clausify_false
- (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
-(satlem _ _
-(ast _ _ _ a1 (\ l1
-(clausify_false
- (impl_elim _ _ l1 (iff_elim_1 _ _ (and_elim_1 _ _ (impl_elim _ _ f2 bf2))))
-))) (\ C3
-
-; b.4
-(satlem _ _
-(asf _ _ _ a2 (\ l2
-(clausify_false
- (contra _ (impl_elim _ _ truth (iff_elim_2 _ _ (and_elim_1 _ _ (impl_elim _ _ f3 bf3)))) l2)
-))) (\ C6
-
-
-(satlem_simplify _ _ _
-(R _ _ (R _ _ C6 C2 v2) C3 v1) (\ x x))
-
+; 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 (\ 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 a 4) (\ v1 (\ a1 +(decl_atom (bblast b 4) (\ v2 (\ a2 + +; 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 +(satlem _ _ +(asf _ _ _ a1 (\ l1 +(ast _ _ _ a2 (\ l2 +(clausify_false + (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 +(satlem _ _ +(ast _ _ _ a1 (\ l1 +(clausify_false + (impl_elim _ _ l1 (iff_elim_1 _ _ (and_elim_1 _ _ (impl_elim _ _ f2 bf2)))) +))) (\ C3 + +; b.4 +(satlem _ _ +(asf _ _ _ a2 (\ l2 +(clausify_false + (contra _ (impl_elim _ _ truth (iff_elim_2 _ _ (and_elim_1 _ _ (impl_elim _ _ f3 bf3)))) l2) +))) (\ C6 + + +(satlem_simplify _ _ _ +(R _ _ (R _ _ C6 C2 v2) C3 v1) (\ x x)) + )))))))))))))))))))))))))))))))))))))))))))
\ No newline at end of file diff --git a/proofs/signatures/th_bv.plf b/proofs/signatures/th_bv.plf index 3fb9d1356..0fb50f8cf 100755 --- a/proofs/signatures/th_bv.plf +++ b/proofs/signatures/th_bv.plf @@ -1,145 +1,145 @@ -; "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)
-;....
-
-; all bit-vector terms are mapped with "bv_atom" to:
-; - a simply-typed term of type "var_bv", which is necessary for bit-blasting
-; - a integer size
-(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 (! 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 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 var_bv (! n mpz formula)))
-
-
-; 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
- (! v bv
- (! x var_bv
- (! f bblt
- (! u (bv_atom (a_bv v) x n)
- (! 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
-; 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)
- (! fx bblt
- (! fy bblt
- (! f formula
- (! 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' 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))))
- ((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)
+; "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) +;.... + +; all bit-vector terms are mapped with "bv_atom" to: +; - a simply-typed term of type "var_bv", which is necessary for bit-blasting +; - a integer size +(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 (! 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 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 var_bv (! n mpz formula))) + + +; 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 + (! v bv + (! x var_bv + (! f bblt + (! u (bv_atom (a_bv v) x n) + (! 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 +; 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) + (! fx bblt + (! fy bblt + (! f formula + (! 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' 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)))) + ((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 |