diff options
-rw-r--r-- | proofs/signatures/lrat.plf | 39 | ||||
-rw-r--r-- | proofs/signatures/lrat_test.plf | 155 |
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 |