summaryrefslogtreecommitdiff
path: root/proofs
diff options
context:
space:
mode:
Diffstat (limited to 'proofs')
-rw-r--r--proofs/signatures/lrat.plf39
-rw-r--r--proofs/signatures/lrat_test.plf155
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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback