Extended DRAT signature to operational DRAT (#2815)

* Extended DRAT signature to operational DRAT

The DRAT signature now supports both operational and specified DRAT.
That is, either kind of proof will be accepted.

The goal of this implementation of operational DRAT was to re-use as
much of the specified DRAT machinery as possible. However, by writing a
separate operational signature, we could make it much more efficient
(after all, operational DRAT came about because of a push for efficient
cheking).

You can run the new AND old DRAT tests by running

```
lfscc sat.plf smt.plf lrat.plf drat.plf drat_test.plf
```

* Apply suggestions from code review (Yoni)

Co-Authored-By: alex-ozdemir <aozdemir@hmc.edu>

2 files changed, 293 insertions, 4 deletions

diff --git a/proofs/signatures/drat.plf b/proofs/signatures/drat.plf
index d777a143a..d0f647452 100644
--- a/proofs/signatures/drat.plf
+++ b/proofs/signatures/drat.plf
@@ -229,21 +229,158 @@
                                  (collect_pseudo_resolvents cs c)))))))
 
 ; Is this proof a valid DRAT proof of bottom?
-(program is_drat_proof_of_bottom ((f cnf) (proof DRATProof)) bool
+(program is_specified_drat_proof ((f cnf) (proof DRATProof)) bool
          (match proof
                 (DRATProofn (cnf_has_bottom f))
                 ((DRATProofa c p) (match
                                     (is_rat f c)
-                                    (tt (is_drat_proof_of_bottom (cnfc c f) p))
+                                    (tt (is_specified_drat_proof (cnfc c f) p))
                                     (ff ff)))
                 ((DRATProofd c p)
-                 (is_drat_proof_of_bottom (cnf_remove_clause c f) p))))
+                 (is_specified_drat_proof (cnf_remove_clause c f) p))))
 
 
+; =============================== ;
+; Operational DRAT implementation ;
+; =============================== ;
+
+; Operation DRAT is defined in the paper "Two Flavors of DRAT".
+; Below is an extension of the DRAT signature to handle it.
+
+; Notes on types.
+; For operational DRAT it is useful to manifest partial assignments in values
+; (although we still use the global assignment in some places). To this end,
+; literals are used to represent single-variable assignments ((pos v) denotes
+; {v maps to true}) and clauses are partial assignments by way of being
+; literal lists.
+
+; Copy the partial assignment represented by a clause into the global
+; assignment. Fails if that clause represents an inconsistent partial
+; assignment (e.g. v is both true and false)
+(program clause_into_global ((a clause)) Unit
+         (match a
+                (cln unit)
+                ((clc l rest)
+                 (do (lit_mk_sat l) (clause_into_global rest)))))
+
+; Remove the partial assignment represented by c from the global assignment
+(program clause_undo_into_global ((a clause)) Unit
+         (match a
+                (cln unit)
+                ((clc l rest)
+                 (do (lit_un_mk_sat l) (clause_undo_into_global rest)))))
+
+; Does this clause have no floating literals w.r.t. the global assignment?
+(program clause_no_floating ((c clause)) bool
+         (match c
+                (cln tt)
+                ((clc l rest) (match (lit_is_floating l)
+                                    (tt ff)
+                                    (ff (clause_no_floating rest))))))
+
+; Does this clause have no sat literals w.r.t. the global assignment?
+(program clause_no_sat ((c clause)) bool
+         (match c
+                (cln tt)
+                ((clc l rest) (match (lit_is_sat l)
+                                    (tt ff)
+                                    (ff (clause_no_sat rest))))))
+
+; Does this clause have one sat literal w.r.t. the global assignment?
+(program clause_one_sat ((c clause)) bool
+         (match c
+                (cln ff)
+                ((clc l rest) (match (lit_is_sat l)
+                                    (tt (clause_no_sat rest))
+                                    (ff (clause_one_sat rest))))))
+
+; Is this clause a unit clause w.r.t. the global assignment?
+; This notion is defined as:
+;    * A clause where no literals are floating, and exactly one is sat.
+(program clause_is_unit_wrt_up_model ((c clause) (up_model clause)) bool
+         (let c' (clause_dedup c)
+         (do (clause_into_global up_model)
+           (let result (match (clause_no_floating c')
+                              (tt (clause_one_sat c'))
+                              (ff ff))
+             (do (clause_undo_into_global up_model)
+               result)))))
+
+; Result from constructing a UP model (defined in "Two Flavors of DRAT")
+; Technically, we're constructing the shared UP model -- the intersection of all
+; UP models.
+; Informally, this is just the partial assignment implied by UP.
+;
+; This type is necessary, because constructing a UP model can reveal an
+; inconsistent UP model -- one which assigns some variable to true and false.
+; This would break our machinery, so we special case it.
+(declare UPConstructionResult type)
+; An actual model
+(declare UPCRModel (! up_model clause UPConstructionResult))
+; Bottom is implied!
+(declare UPCRBottom UPConstructionResult)
+
+
+; Do unit propagation on `f`, constructing a UP model for it.
+(program build_up_model ((f cnf)) clause
+         (match (unit_search f)
+                (USRBottom UPCRBottom)
+                (USRNoUnit (UPCRModel cln))
+                ((USRUnit l f')
+                 (let result (build_up_model f')
+                   (do (lit_un_mk_sat l)
+                     (match result
+                            (UPCRBottom UPCRBottom)
+                            ((UPCRModel model) (UPCRModel (clc l model)))))))))
+
+; Given some starting assignment (`up_model`), continue UP to construct a larger
+; model.
+(program extend_up_model ((f cnf) (up_model clause)) clause
+         (do (clause_into_global up_model)
+           (let result (build_up_model f)
+             (do (clause_undo_into_global up_model)
+               (match result
+                      (UPCRBottom UPCRBottom)
+                      ((UPCRModel up_model')
+                       (UPCRModel (clause_append up_model up_model'))))))))
+
+; Helper for `is_operational_drat_proof` which takes a UP model for the working
+; formula. The UP model is important for determining which clause deletions
+; actually are executed in operational DRAT. Passing the UP model along
+; prevents it from being fully recomputed everytime.
+(program is_operational_drat_proof_h ((f cnf) (up_model clause) (pf DRATProof)) bool
+         (match pf
+                (DRATProofn (cnf_has_bottom f))
+                ((DRATProofd c pf')
+                 (match (clause_is_unit_wrt_up_model c up_model)
+                        (tt (is_operational_drat_proof_h f up_model pf'))
+                        (ff (is_operational_drat_proof_h
+                              (cnf_remove_clause c f) up_model pf'))))
+                ((DRATProofa c pf')
+                 (let f' (cnfc c f)
+                   (match (is_rat f c)
+                          (tt (match (extend_up_model f' up_model)
+                                     (UPCRBottom tt)
+                                     ((UPCRModel up_model')
+                                      (is_operational_drat_proof_h f' up_model' pf'))))
+                          (ff ff))))))
+
+; Is this an operational DRAT proof of bottom for this formula?
+(program is_operational_drat_proof ((f cnf) (pf DRATProof)) bool
+         (match (build_up_model f)
+                (UPCRBottom tt)
+                ((UPCRModel model) (is_operational_drat_proof_h f model pf))))
+
+; Is this a specified or operational DRAT proof of bottom for this formula?
+(program is_drat_proof ((f cnf) (pf DRATProof)) bool
+         (match (is_specified_drat_proof f pf)
+                (tt tt)
+                (ff (is_operational_drat_proof f pf))))
+
 (declare drat_proof_of_bottom
          (! f cnf
             (! proof_of_formula (cnf_holds f)
                (! proof DRATProof
-                  (! sc (^ (is_drat_proof_of_bottom f proof) tt)
+                  (! sc (^ (is_drat_proof f proof) tt)
                      bottom)))))
 
diff --git a/proofs/signatures/drat_test.plf b/proofs/signatures/drat_test.plf
index 57de39111..2ede6df34 100644
--- a/proofs/signatures/drat_test.plf
+++ b/proofs/signatures/drat_test.plf
@@ -280,3 +280,155 @@
                (DRATProofd (clc (pos v2) (clc (pos v3) (clc (neg v4) cln)))
                (DRATProofa cln
                 DRATProofn)))))))))))))))
+
+; ===================================== ;
+; Test Suite from "Two Flavors of DRAT" ;
+; ===================================== ;
+
+; The paper includes a number of proofs which explore specified and operational
+; DRAT validity.
+
+; Our test predicate for asserting the specified and operational validity of
+; DRAT proofs
+(declare spec_oper_test
+         (! f cnf
+         (! proof DRATProof
+         (! spec_validity bool
+         (! oper_validity bool
+            (! sc (^ (bool_and
+                       (bool_eq (is_specified_drat_proof f proof) spec_validity)
+                       (bool_eq (is_operational_drat_proof f proof) oper_validity)
+                     ) tt)
+         TestSuccess))))))
+
+
+(declare x var)
+(declare y var)
+(declare z var)
+(declare w var)
+(define ex_1_formula
+  (cnfc (clc (pos x) (clc (pos y) (clc (pos z) cln)))
+  (cnfc (clc (neg x) (clc (pos y) (clc (pos z) cln)))
+  (cnfc (clc (pos x) (clc (neg y) (clc (pos z) cln)))
+  (cnfc (clc (neg x) (clc (neg y) (clc (pos z) cln)))
+  (cnfc (clc (pos x) (clc (pos y) (clc (neg z) cln)))
+  (cnfc (clc (neg x) (clc (pos y) (clc (neg z) cln)))
+  (cnfc (clc (pos x) (clc (neg y) (clc (neg z) cln)))
+  (cnfc (clc (neg x) (clc (neg y) (clc (neg z) cln)))
+        cnfn)))))))))
+
+; Spec-valid, operationally-invalid
+(define ex_1_pf_pi
+  (DRATProofa (clc (pos x) (clc (pos y) cln))
+  (DRATProofa (clc (pos x) cln)
+  (DRATProofa (clc (pos w) (clc (neg x) cln))
+  (DRATProofd (clc (pos w) (clc (neg x) cln))
+  (DRATProofa (clc (neg w) (clc (neg x) cln))
+  (DRATProofa (clc (pos w) (clc (pos x) cln))
+  (DRATProofa (clc (pos y) (clc (pos w) cln))
+  (DRATProofa cln
+              DRATProofn)))))))))
+
+(check
+  (: TestSuccess
+     (spec_oper_test ex_1_formula ex_1_pf_pi tt ff)))
+
+; Spec-invalid, operationally valid
+(define ex_1_pf_sigma
+  (DRATProofa (clc (pos x) (clc (pos y) cln))
+  (DRATProofa (clc (pos x) cln)
+  (DRATProofd (clc (pos x) cln)
+  (DRATProofa (clc (pos w) (clc (neg y) cln))
+  (DRATProofa (clc (neg w) (clc (neg y) cln))
+  (DRATProofa (clc (pos w) cln)
+  (DRATProofa cln
+              DRATProofn))))))))
+
+(check
+  (: TestSuccess
+     (spec_oper_test ex_1_formula ex_1_pf_sigma ff tt)))
+
+(declare x1 var)
+(declare x2 var)
+(declare x3 var)
+(declare x4 var)
+(declare x5 var)
+(declare x6 var)
+(declare x7 var)
+(declare x8 var)
+(declare x9 var)
+(declare x10 var)
+
+(define ex_2_formula
+  (cnfc (clc (pos x1) cln)
+  (cnfc (clc (neg x1) (clc (pos x2) cln))
+  (cnfc (clc (neg x1) (clc (neg x2) (clc (pos x3) cln)))
+  (cnfc (clc (neg x1) (clc (neg x3) (clc (pos x4) cln)))
+  (cnfc (clc (pos x5) (clc (pos x6) cln))
+  (cnfc (clc (neg x2) (clc (neg x5) (clc (pos x7) cln)))
+  (cnfc (clc (neg x1) (clc (neg x5) (clc (pos x6) cln)))
+  (cnfc (clc (neg x5) (clc (neg x6) (clc (pos x4) cln)))
+  (cnfc (clc (neg x3) (clc (neg x6) (clc (pos x8) cln)))
+  (cnfc (clc (neg x6) (clc (neg x4) (clc (pos x3) cln)))
+  (cnfc (clc (neg x8) (clc (pos x5) cln))
+  (cnfc (clc (neg x3) (clc (pos x9) (clc (pos x10) cln)))
+  (cnfc (clc (neg x4) (clc (neg x9) (clc (pos x10) cln)))
+  (cnfc (clc (neg x10) (clc (pos x9) cln))
+  (cnfc (clc (neg x9) (clc (pos x7) cln))
+  (cnfc (clc (neg x7) (clc (neg x8) (clc (neg x9) (clc (neg x10) cln))))
+        cnfn)))))))))))))))))
+
+; Spec-valid, operationally-valid
+(define ex_2_pf_tau
+  (DRATProofa (clc (pos x5) cln)
+  (DRATProofa (clc (pos x4) cln)
+  (DRATProofa (clc (pos x9) cln)
+  (DRATProofa cln
+              DRATProofn)))))
+
+(check
+  (: TestSuccess
+     (spec_oper_test ex_2_formula ex_2_pf_tau tt tt)))
+
+; Spec-valid, operationally unspecified in the paper, but its operationally valid.
+(define ex_3_pf_tau_prime
+  (DRATProofa (clc (pos x5) cln)
+  (DRATProofd (clc (neg x1) (clc (pos x2) cln))
+  (DRATProofa (clc (pos x9) cln)
+  (DRATProofa cln
+              DRATProofn)))))
+
+(check
+  (: TestSuccess
+     (spec_oper_test ex_2_formula ex_3_pf_tau_prime tt tt)))
+
+; Spec-invalid, operationally-invalid
+(define ex_4_pf_pi_prime
+  (DRATProofa (clc (pos x) (clc (pos y) cln))
+  (DRATProofa (clc (pos x) cln)
+  (DRATProofa (clc (pos w) (clc (neg x) cln))
+  (DRATProofa (clc (neg w) (clc (neg x) cln))
+  (DRATProofa (clc (pos w) (clc (pos x) cln))
+  (DRATProofa (clc (pos y) (clc (pos w) cln))
+  (DRATProofa cln
+              DRATProofn))))))))
+
+(check
+  (: TestSuccess
+     (spec_oper_test ex_1_formula ex_4_pf_pi_prime ff ff)))
+
+
+; Spec-valid, operationally valid
+(define ex_5_pf_sigma_prime
+  (DRATProofa (clc (pos x) (clc (pos y) cln))
+  (DRATProofa (clc (pos x) cln)
+  (DRATProofa (clc (pos w) (clc (neg y) cln))
+  (DRATProofa (clc (neg w) (clc (neg y) cln))
+  (DRATProofa (clc (pos w) cln)
+  (DRATProofa cln
+              DRATProofn)))))))
+
+(check
+  (: TestSuccess
+     (spec_oper_test ex_1_formula ex_5_pf_sigma_prime tt tt)))
+