[LRAT] signature robust against duplicate literals (#2743)

* [LRAT] signature robust against duplicate literals

The LRAT signature previously had complex, surprising, and occasionally
incorrect behavior when given clauses with duplicate literals.

Now it does not. Now clauses have true set semantics, and clauses with
duplicate literals are treated identically to those without.

* Test with logically = but structurally != clauses.

2 files changed, 163 insertions, 31 deletions

diff --git a/proofs/signatures/lrat.plf b/proofs/signatures/lrat.plf
index f5af891bc..96cdd83b3 100644
--- a/proofs/signatures/lrat.plf
+++ b/proofs/signatures/lrat.plf
@@ -129,6 +129,28 @@
                                     (ff (clause_contains_lit c' l))))
                 (cln ff)))
 
+; Returns a copy of `c` with any duplicate literals removed.
+; Never fails.
+; Uses marks 3 & 4. Expects them to be clear before hand, and leaves them clear
+; afterwards.
+(program clause_dedup ((c clause)) clause
+         (match c
+                (cln cln)
+                ((clc l rest)
+                 (match l
+                        ((pos v) (ifmarked3
+                                   v
+                                   (clause_dedup rest)
+                                   (do (markvar3 v)
+                                     (let result (clc (pos v) (clause_dedup rest))
+                                       (do (markvar3 v) result)))))
+                        ((neg v) (ifmarked4
+                                   v
+                                   (clause_dedup rest)
+                                   (do (markvar4 v)
+                                     (let result (clc (neg v) (clause_dedup rest))
+                                       (do (markvar4 v) result)))))))))
+
 ; Append two traces
 (program Trace_concat ((t1 Trace) (t2 Trace)) Trace
          (match t1
@@ -473,9 +495,9 @@
                 (RATHintsn CTPn)
                 ((RATHintsc i ht hints')
                  (CTPc
-                   (clause_append c
+                   (clause_dedup (clause_append c
                                   (clause_remove_all (lit_flip (clause_head c))
-                                                     (CMap_get i cs)))
+                                                     (CMap_get i cs))))
                    (Trace_concat t ht)
                    (construct_ct_pairs cs c t hints')))))
 
@@ -534,17 +556,22 @@
                 (LRATProofn ff))
          )
 
+
 ; Proof of a CMap from clause proofs.
 ; The idx is unelidable b/c it is unspecified.
+;  Robust against clauses with duplicat literals, but not against tautological
+;  clauses.
 (declare CMap_holds (! c CMap type))
 (declare CMapn_proof (CMap_holds CMapn))
 (declare CMapc_proof
          (! idx mpz ; Not elidable!
             (! c clause
-               (! rest CMap
-                  (! proof_c (holds c)
-                     ( ! proof_rest (CMap_holds rest)
-                         (CMap_holds (CMapc idx c rest))))))))
+               (! deduped_c clause
+                  (! rest CMap
+                     (! proof_c (holds c)
+                        (! proof_rest (CMap_holds rest)
+                            (! sc (^ (clause_dedup c) deduped_c)
+                               (CMap_holds (CMapc idx deduped_c rest))))))))))
 
 (define bottom (holds cln))
 (declare lrat_proof_of_bottom
diff --git a/proofs/signatures/lrat_test.plf b/proofs/signatures/lrat_test.plf
index 3ba785507..0663a08f7 100644
--- a/proofs/signatures/lrat_test.plf
+++ b/proofs/signatures/lrat_test.plf
@@ -637,14 +637,66 @@
     (% pf_c7 (holds (clc (neg v1) (clc (pos v2) (clc (pos v4) cln))))
     (% pf_c8 (holds (clc (pos v1) (clc (neg v2) (clc (neg v4) cln))))
       (@ pf_cmap
-         (CMapc_proof 1 _ _ pf_c1
-         (CMapc_proof 2 _ _ pf_c2
-         (CMapc_proof 3 _ _ pf_c3
-         (CMapc_proof 4 _ _ pf_c4
-         (CMapc_proof 5 _ _ pf_c5
-         (CMapc_proof 6 _ _ pf_c6
-         (CMapc_proof 7 _ _ pf_c7
-         (CMapc_proof 8 _ _ pf_c8
+         (CMapc_proof 1 _ _ _ pf_c1
+         (CMapc_proof 2 _ _ _ pf_c2
+         (CMapc_proof 3 _ _ _ pf_c3
+         (CMapc_proof 4 _ _ _ pf_c4
+         (CMapc_proof 5 _ _ _ pf_c5
+         (CMapc_proof 6 _ _ _ pf_c6
+         (CMapc_proof 7 _ _ _ pf_c7
+         (CMapc_proof 8 _ _ _ pf_c8
+                      CMapn_proof))))))))
+      (@ lrat_proof_witness
+            (LRATProofa 9
+                        (clc (pos v1) cln)
+                        Tracen
+                        (RATHintsc 2 (Tracec 6 (Tracec 8 Tracen))
+                          (RATHintsc 5 (Tracec 1 (Tracec 8 Tracen))
+                          (RATHintsc 7 (Tracec 6 (Tracec 1 Tracen))
+                                     RATHintsn)))
+            (LRATProofd (CIListc 1 (CIListc 6 (CIListc 8 CIListn)))
+            (LRATProofa 10
+                        (clc (pos v2) cln)
+                        (Tracec 9 (Tracec 7 (Tracec 5 (Tracec 3 Tracen))))
+                        RATHintsn
+            (LRATProofd (CIListc 3 (CIListc 7 CIListn))
+            (LRATProofa 11
+                        cln
+                        (Tracec 9 (Tracec 10 (Tracec 2 (Tracec 4 (Tracec 5 Tracen)))))
+                        RATHintsn
+            LRATProofn)))))
+            (:
+              (holds cln)
+              (lrat_proof_of_bottom _ pf_cmap lrat_proof_witness))
+      ))
+    ))))))))
+  ))))
+)
+
+; Proof from Figure 2 of "Efficient Certified RAT Verification"
+; With duplicates
+(check
+  (% v1 var
+  (% v2 var
+  (% v3 var
+  (% v4 var
+    (% pf_c1 (holds (clc (pos v1) (clc (pos v1) (clc (pos v2) (clc (neg v3) cln)))))
+    (% pf_c2 (holds (clc (neg v1) (clc (neg v2) (clc (pos v3) cln))))
+    (% pf_c3 (holds (clc (pos v2) (clc (pos v3) (clc (pos v3) (clc (pos v3) (clc (neg v4) cln))))))
+    (% pf_c4 (holds (clc (neg v2) (clc (neg v3) (clc (pos v4) cln))))
+    (% pf_c5 (holds (clc (neg v1) (clc (neg v3) (clc (neg v4) (clc (neg v4) cln)))))
+    (% pf_c6 (holds (clc (pos v1) (clc (pos v3) (clc (pos v3) (clc (pos v4) cln)))))
+    (% pf_c7 (holds (clc (neg v1) (clc (pos v2) (clc (pos v4) cln))))
+    (% pf_c8 (holds (clc (pos v1) (clc (neg v2) (clc (neg v2) (clc (neg v4) cln)))))
+      (@ pf_cmap
+         (CMapc_proof 1 _ _ _ pf_c1
+         (CMapc_proof 2 _ _ _ pf_c2
+         (CMapc_proof 3 _ _ _ pf_c3
+         (CMapc_proof 4 _ _ _ pf_c4
+         (CMapc_proof 5 _ _ _ pf_c5
+         (CMapc_proof 6 _ _ _ pf_c6
+         (CMapc_proof 7 _ _ _ pf_c7
+         (CMapc_proof 8 _ _ _ pf_c8
                       CMapn_proof))))))))
       (@ lrat_proof_witness
             (LRATProofa 9
@@ -689,15 +741,68 @@
     (% pf_c8 (holds (clc (pos v1) (clc (neg v2) (clc (neg v4) cln))))
     (% pf_c9 (holds (clc (pos v1) (clc (pos v2) (clc (neg v3) cln))))
       (@ pf_cmap
-         (CMapc_proof 1 _ _ pf_c1
-         (CMapc_proof 2 _ _ pf_c2
-         (CMapc_proof 3 _ _ pf_c3
-         (CMapc_proof 4 _ _ pf_c4
-         (CMapc_proof 5 _ _ pf_c5
-         (CMapc_proof 6 _ _ pf_c6
-         (CMapc_proof 7 _ _ pf_c7
-         (CMapc_proof 8 _ _ pf_c8
-         (CMapc_proof 9 _ _ pf_c9
+         (CMapc_proof 1 _ _ _ pf_c1
+         (CMapc_proof 2 _ _ _ pf_c2
+         (CMapc_proof 3 _ _ _ pf_c3
+         (CMapc_proof 4 _ _ _ pf_c4
+         (CMapc_proof 5 _ _ _ pf_c5
+         (CMapc_proof 6 _ _ _ pf_c6
+         (CMapc_proof 7 _ _ _ pf_c7
+         (CMapc_proof 8 _ _ _ pf_c8
+         (CMapc_proof 9 _ _ _ pf_c9
+                      CMapn_proof)))))))))
+      (@ lrat_proof_witness
+            (LRATProofa 10
+                        (clc (pos v1) cln)
+                        Tracen
+                        (RATHintsc 2 (Tracec 6 (Tracec 8 Tracen))
+                          (RATHintsc 5 (Tracec 1 (Tracec 8 Tracen))
+                          (RATHintsc 7 (Tracec 6 (Tracec 9 Tracen))
+                                     RATHintsn)))
+            (LRATProofd (CIListc 1 (CIListc 6 (CIListc 8 (CIListc 9 CIListn))))
+            (LRATProofa 11
+                        (clc (pos v2) cln)
+                        (Tracec 10 (Tracec 7 (Tracec 5 (Tracec 3 Tracen))))
+                        RATHintsn
+            (LRATProofd (CIListc 3 (CIListc 7 CIListn))
+            (LRATProofa 12
+                        cln
+                        (Tracec 10 (Tracec 11 (Tracec 2 (Tracec 4 (Tracec 5 Tracen)))))
+                        RATHintsn
+            LRATProofn)))))
+            (:
+              (holds cln)
+              (lrat_proof_of_bottom _ pf_cmap lrat_proof_witness))
+      ))
+    )))))))))
+  ))))
+)
+
+; Clauses 1 and 9 are logically identical, but the literals have been reordered.
+(check
+  (% v1 var
+  (% v2 var
+  (% v3 var
+  (% v4 var
+    (% pf_c1 (holds (clc (pos v1) (clc (pos v2) (clc (neg v3) cln))))
+    (% pf_c2 (holds (clc (neg v1) (clc (neg v2) (clc (pos v3) cln))))
+    (% pf_c3 (holds (clc (pos v2) (clc (pos v3) (clc (neg v4) cln))))
+    (% pf_c4 (holds (clc (neg v2) (clc (neg v3) (clc (pos v4) cln))))
+    (% pf_c5 (holds (clc (neg v1) (clc (neg v3) (clc (neg v4) cln))))
+    (% pf_c6 (holds (clc (pos v1) (clc (pos v3) (clc (pos v4) cln))))
+    (% pf_c7 (holds (clc (neg v1) (clc (pos v2) (clc (pos v4) cln))))
+    (% pf_c8 (holds (clc (pos v1) (clc (neg v2) (clc (neg v4) cln))))
+    (% pf_c9 (holds (clc (neg v3) (clc (pos v2) (clc (pos v1) cln))))
+      (@ pf_cmap
+         (CMapc_proof 1 _ _ _ pf_c1
+         (CMapc_proof 2 _ _ _ pf_c2
+         (CMapc_proof 3 _ _ _ pf_c3
+         (CMapc_proof 4 _ _ _ pf_c4
+         (CMapc_proof 5 _ _ _ pf_c5
+         (CMapc_proof 6 _ _ _ pf_c6
+         (CMapc_proof 7 _ _ _ pf_c7
+         (CMapc_proof 8 _ _ _ pf_c8
+         (CMapc_proof 9 _ _ _ pf_c9
                       CMapn_proof)))))))))
       (@ lrat_proof_witness
             (LRATProofa 10
@@ -741,14 +846,14 @@
     (% pf_c7 (holds (clc (neg v1) (clc (pos v2) (clc (pos v4) cln))))
     (% pf_c8 (holds (clc (pos v1) (clc (neg v2) (clc (neg v4) cln))))
       (@ pf_cmap
-         (CMapc_proof 1 _ _ pf_c1
-         (CMapc_proof 2 _ _ pf_c2
-         (CMapc_proof 3 _ _ pf_c3
-         (CMapc_proof 4 _ _ pf_c4
-         (CMapc_proof 5 _ _ pf_c5
-         (CMapc_proof 6 _ _ pf_c6
-         (CMapc_proof 7 _ _ pf_c7
-         (CMapc_proof 8 _ _ pf_c8
+         (CMapc_proof 1 _ _ _ pf_c1
+         (CMapc_proof 2 _ _ _ pf_c2
+         (CMapc_proof 3 _ _ _ pf_c3
+         (CMapc_proof 4 _ _ _ pf_c4
+         (CMapc_proof 5 _ _ _ pf_c5
+         (CMapc_proof 6 _ _ _ pf_c6
+         (CMapc_proof 7 _ _ _ pf_c7
+         (CMapc_proof 8 _ _ _ pf_c8
                       CMapn_proof))))))))
       (@ lrat_proof_witness
             (LRATProofa 9