From 499aa5641e2b830f60159c2ce1c791bf4d45aac1 Mon Sep 17 00:00:00 2001 From: Alex Ozdemir Date: Fri, 6 Dec 2019 07:51:54 -0800 Subject: [proof] Eliminate side-condition from ER signature (#3230) * [proof] Eliminate the side condition in er.plf By tweaking the axioms a bit, I got rid of the lone SC in the Extended Resolution signature. * [proof] Changed er_proof.cpp in line with signature The new signature requires slightly different proof printing. * [proof] clang-format er_proof.cpp * Fix tests * [proof] Actually delete the SC * Apply suggestions from code review Co-Authored-By: yoni206 * Add LFSC-checking unit test for ER proof * Gate the lfsc invocation on the build system * Properly gate the lfsc check on the build system * gate the plf_signatures forward def on the build system --- proofs/signatures/er.plf | 65 +++++++++++++++++++++++-------------------- proofs/signatures/er_test.plf | 39 ++++---------------------- 2 files changed, 41 insertions(+), 63 deletions(-) (limited to 'proofs') diff --git a/proofs/signatures/er.plf b/proofs/signatures/er.plf index 8b559671e..9fcc9d4e8 100644 --- a/proofs/signatures/er.plf +++ b/proofs/signatures/er.plf @@ -64,13 +64,17 @@ (holds cln))) (holds cln))))) -; Takes a `list` of literals and a clause, `suffix`, adds the suffix to each -; literal and returns a list of clauses as a `cnf`. -(program clause_add_suffix_all ((list clause) (suffix clause)) cnf - (match list - (cln cnfn) - ((clc l rest) (cnfc (clc l suffix) - (clause_add_suffix_all rest suffix))))) +; Represents multiple conjoined clauses. +; There is a list, `heads` of literals, each of which is suffixed by the +; same `tail`. +(declare common_tail_cnf_t type) +(declare common_tail_cnf + (! heads clause + (! tail clause common_tail_cnf_t))) + +; A member of this type is a proof of a common_tail_cnf. +(declare common_tail_cnf_holds + (! cnf common_tail_cnf_t type)) ; This translates a definition witness value for the def: ; @@ -89,10 +93,6 @@ (! def (definition new old others) (! negOld lit (! mkNegOld (^ (lit_flip old) negOld) - (! provenCnf cnf - (! mkProvenCnf (^ (clause_add_suffix_all - others - (clc (neg new) (clc old cln))) provenCnf) ; If you can prove bottom from its clausal representation (! pf_continuation ; new v l_1 v l_2 v ... v l_n @@ -100,26 +100,31 @@ ; new v ~old (! pf_c2 (holds (clc (pos new) (clc negOld cln))) ; for each i <= n: l_i v ~new v old - (! pf_cs (cnf_holds provenCnf) + (! pf_cs (common_tail_cnf_holds + (common_tail_cnf + others + (clc (neg new) (clc old cln)))) (holds cln)))) ; Then you've proven bottom - (holds cln))))))))))) + (holds cln))))))))) -; This axiom is useful for converting a proof of some CNF formula (a value of -; type (cnf_holds ...)) into proofs of the constituent clauses (many values of -; type (holds ...)). +; These axioms are useful for converting a proof of some CNF formula represented +; using the `common_tail_cnf` type (a value of type `common_tail_cnf_holds`), +; into proofs of its constituent clauses (many values of type `holds`). ; Given -; 1. a proof of some cnf, first ^ rest, and -; 2. a proof continuation that -; a. takes in proofs of -; i. first and -; ii. rest and -; b. proceeds to prove bottom, -; proves bottom. -(declare cnfc_unroll_towards_bottom - (! first clause - (! rest cnf - (! pf (cnf_holds (cnfc first rest)) - (! pf_continuation (! r1 (holds first) (! r2 (cnf_holds rest) (holds cln))) - (holds cln)))))) - +; 1. a proof of some `common_tail_cnf` +; Then +; 1. the first axiom gives you a proof of the first `clause` therein and +; 2. the second gives you a proof of the rest of the `common_tail_cnf`. +(declare common_tail_cnf_prove_head + (! first lit + (! rest clause + (! tail clause + (! pf (common_tail_cnf_holds (common_tail_cnf (clc first rest) tail)) + (holds (clc first tail))))))) +(declare common_tail_cnf_prove_tail + (! first lit + (! rest clause + (! tail clause + (! pf (common_tail_cnf_holds (common_tail_cnf (clc first rest) tail)) + (common_tail_cnf_holds (common_tail_cnf rest tail))))))) diff --git a/proofs/signatures/er_test.plf b/proofs/signatures/er_test.plf index 27c61de1f..1b5117a70 100644 --- a/proofs/signatures/er_test.plf +++ b/proofs/signatures/er_test.plf @@ -1,30 +1,5 @@ ; Depends on er.plf -; Type for representing success when testing a side-condition -(declare TestSuccess type) - -; Test for clause_add_suffix_all -(declare test_clause_add_suffix_all - (! list clause - (! suffix clause - (! result cnf - (! (^ (clause_add_suffix_all list suffix) result) - TestSuccess))))) - -(check - (% a lit - (% b lit - (% c lit - (test_clause_add_suffix_all - (clc a (clc b cln)) - (clc c cln) - (cnfc (clc a (clc c cln)) - (cnfc (clc b (clc c cln)) - cnfn)) - ) - ))) -) - ; This is a circuitous proof that uses the definition introduction and ; unrolling rules (check @@ -40,13 +15,11 @@ (clc (neg v2) cln) (\ v3 (\ def3 - (clausify_definition _ _ _ def3 _ _ + (clausify_definition _ _ _ def3 _ (\ pf_c5 ; type: (holds (clc (pos v3) (clc (neg v2) cln))) (\ pf_c6 ; type: (holds (clc (pos v3) (clc (pos v1) cln))) - (\ pf_cnf3 ; type: (cnf_holds (cnfc (clc (neg v2) (clc (neg v3) (clc (neg v1) cln))) cnfn)) - (cnfc_unroll_towards_bottom _ _ pf_cnf3 - (\ pf_c7 ; type: (clc (neg v2) (clc (neg v3) (clc (neg v1) cln))) - (\ pf_cnfn + (\ pf_cnf ; type: (common_tail_cnf (clc (neg v2) cln) (clc (neg v3) (clc (neg v1) cln))) + (@ pf_c7 (common_tail_cnf_prove_head _ _ _ pf_cnf) ; Clauses (satlem_simplify _ _ _ (R _ _ pf_c1 pf_c2 v1) (\ pf_c8 ; v2 (satlem_simplify _ _ _ (R _ _ pf_c8 pf_c5 v2) (\ pf_c9 ; v3 @@ -61,7 +34,7 @@ )) )) )) - ))) + ) ))) ) )) @@ -92,10 +65,10 @@ cln (\ v5 (\ def1 - (clausify_definition _ _ _ def1 _ _ + (clausify_definition _ _ _ def1 _ (\ pf_c9 ; type: (holds (clc (pos def1v) cln)) (\ pf_c10 ; type: (holds (clc (pos def1v) (clc (pos v1) cln))) - (\ idc0 ; type: (cnf_holds cnfn) + (\ idc0 ; type: (common_tail_cnf cln _) (satlem_simplify _ _ _ (R _ _ pf_c10 pf_c7 v1) (\ pf_c11 (satlem_simplify _ _ _ (R _ _ pf_c10 pf_c5 v1) (\ pf_c12 (satlem_simplify _ _ _ (R _ _ pf_c10 pf_c2 v1) (\ pf_c13 -- cgit v1.2.3