[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 <yoni206@users.noreply.github.com>

* 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

1 files changed, 6 insertions, 33 deletions

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