[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

2 files changed, 41 insertions, 63 deletions

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