[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.

diff --git a/proofs/signatures/lrat.plf b/proofs/signatures/lrat.plf
index f5af891bc8bee5aeaabe019b9f9f1f0f17dd5496..96cdd83b3c15c30793766656a1ac8a3f14420dbb 100644 (file)
--- 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 3ba78550708cc8254033e7db7183e0796e99e452..0663a08f7debaf30d7dd04c6e1e7478dae443fbd 100644 (file)
--- 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