A framework for verified use of an external AIG+SAT solver with ACL2 Matt Kaufmann April 13, 2011 ============================================================ === Outline ============================================================ Please feel free to ask questions. I don't expect to cover all of these topics; we may skip the last three almost entirely. * Abstract * Introduction * Notation and definitions * An introductory example of proof-checking * The checker * A small introductory example of proof generation * Two certification runs: (1) ZZ proof generation (2) ZZ proof checking * Some remarks on the use of GL * Maybe-skip-proofs * Interface with ZZ (during proof generation) ============================================================ === Abstract ============================================================ Abstract. We provide a framework for proving ACL2 theorems with the help of an external SAT solver, but without dependence on the correctness of that solver. The solver is the ZZ tool of Niklas Een, a C program based on MiniSAT that proves unsatisfiability of and-inverter graphs (AIGs). Our talk focuses on the proof-checker as well as the use of two certification runs in order to avoid trust tags (this will be explained). As time permits (which it probably won't, really), I'll mention a connection with the GL framework of Sol Swords. The talk (but not necessarily the notes without the talk) is intended to be self-contained for anyone familiar with ACL2. My goal, in addition to presenting our framework, is to illustrate several features of ACL2 developed in recent years. ============================================================ === Introduction ============================================================ Our framework for checking external proof objects was initially developed for connecting with the GL framework developed by Sol Swords. During preparation of this talk, we learned how Anna Slobodova uses our framework without GL, and we focus today primarily on that simpler approach. Acknowledgements etc.: I'm grateful to Sol Swords and Niklas Een for helping me to get started on this project. This work depends on the AIG+SAT solver ZZ, based on MiniSAT, written in C by Niklas Een. It also ties into AIG stuff developed at Centaur, even when not connected to the GL framework developed by Sol Swords. My thanks to Warren Hunt for proposing this work, so that ZZ can assist in proving ACL2 theorems without having to trust ZZ. I also thank Anna Slobodova for showing me how she uses my SAT proof-checker without GL. For the talk, I'll follow these notes. I plan to put them on the web, together with a log. The relevant ACL2 books and other input files are not yet all released from Centaur, and it's up to Niklas Een to decide about releasing ZZ. History: I completed a first cut of this work in January, 2011. It has been used at Centaur since that time, and I can see some changes. This talk is based on the code from Centaur that I have as of April 11, 2011. Major ideas presented: - An external AIG+SAT solver to verify ACL2 conjectures (NOTE: already being done at Centaur before I got involved) - Verified AIG+SAT proof-checker - "Two-runs" certification so that correctness does not depend on the external solver (hence, does not need a trust tag) Auxiliary ideas touched on (my intention is to give a sense of how these work; you may wish to read associated documentation for details): - Make-event - ACL2 state globals - The use of hons for efficient ground resolution - The use of memoization for efficient normalization (aig-norm) - Set-enforce-redundancy - Defattach - As time permits, a bit about the GL framework of Sol Swords, and (less likely) also: set-evisc-tuple and iprinting; CCL foreign function interface ============================================================ === Notation and definitions ============================================================ - In this talk, all pathnames are relative to the Centaur directory "e/cbooks". - We refer below to a "fast-alist", which can be created using (make-fal alist name). This is essentially an alist, but in the HONS version of ACL2 it is associated with a hash table so that lookup is fast. - "SAT" refers to the class of problems of the form: Is a given Boolean formula satisfiable? - An AIG, or And-Inverter Graph, is a tree with arbitrary atoms at the leaves, whose cons nodes are of the form (x) or (x . y), where the former represents the negation of x and the latter (with y non-nil) represents the conjunction of x and y. Thus every ACL2 object can be interpreted as an AIG. The following definition is equivalent to the one in the book aig/base.lisp. (defun aig-eval (x al) (cond ((eq x t) t) ((eq x nil) nil) ((atom x) (and (aig-env-lookup x al) t)) ((eq (cdr x) nil) (not (aig-eval (car x) al))) (t (and (aig-eval (car x) al) (aig-eval (cdr x) al))))) ; Example: (aig-eval (aig-or (aig-and 'x 'y) (aig-not 'z)) (make-fal '((x . t) (y . nil) (z . t)) nil)) - The external tool uses "normalized" AIGs: for an AND node (u . v), u is "smaller" than v. We thus normalize too (the full story is a bit tricky and omitted here), using this function, which in turn uses an order hons< that is based closely on lexorder. (defn aig-norm (x) (cond ((atom x) x) ((null (cdr x)) (aig-not (aig-norm (car x)))) (t (let ((a (aig-norm (car x))) (b (aig-norm (cdr x)))) (if (hons< a b) (aig-and a b) (aig-and b a)))))) We actually memoize this function. (memoize 'aig-norm :condition '(and (consp x) (cdr x))) - For us, a "clause" is a list of AIGs, viewed as their disjunction. As usual, it is often convenient to think of a disjunction as an implication as follows: If all but one of the literals (clause elements) is false, then the other must be true. So for example, the clause (A \/ B \/ C) is equivalent to: (~A & ~B) => C. - The "Tseiten clauses" for an AND-node of an AIG, say (u . v), are as follows (i.e., we can treat them as axiom clauses). (u . v) => u, i.e., {~(u . v), u} (u . v) => v, i.e., {~(u . v), v} (u & v) => (u . v), i.e., {~u, ~v, (u . v)} - "Resolution" is a procedure for deriving a clause (the "resolvent") from two given clauses and a literal, by taking their union after deleting the literal from one clause and its negation from the other. For example: Resolving {u,v,w} and {r,~v,w}, on literal v, yields the clause {u,w,r}. ============================================================ === An introductory example of proof-checking ============================================================ We'll look at intro.lisp. Then we'll see what's going on.... (include-book "intro") Let's look at the result of "running" the proof. It should produce a clause at each step, and the final clause (in the CAR) should contain just the negation of the input aig (up to normalization). (mv-let (erp val) (zzchk-run-proof *proof* nil) (assert$ (null erp) val)) (mv-let (erp val) (zzchk-run-proof *proof* nil) (assert$ (null erp) (let* ((last-step (car val)) (last-cl (cdr last-step))) (assert$ (eql (len last-cl) 1) (hons-equal (aig-norm *aig*) (aig-not (aig-norm (car last-cl)))))))) (include-book "print-proof") (print-proof *proof*) Included in the output is this: (14 CHAIN 7 (8 (AND (NOT Y) (NOT X))) (9 (NOT Z)) (10 (NOT Y)) (11 (AND (NOT Y) (NOT Z))) (12 (NOT X)) (13 (AND (NOT X) (NOT Y) (NOT Z)))) Let's see how that works. The starting clause shown above in (14 CHAIN 7 ...) is clause number 7: (7 ROOT (Z (AND (NOT Z) (NOT Y) (NOT X)) (NOT (AND (NOT Y) (NOT X))))) Think of the negations of the first and third literals as implying the second: ( (NOT Z) & (AND (NOT Y) (NOT X))) => (AND (NOT Z) (and (NOT Y) (NOT X))) We recognize the above clause as valid because it is one of the "Tseiten" clauses corresponding to the AIG and-node shown in the conclusion of the => above. The first step in the CHAIN above is as follows. (8 (AND (NOT Y) (NOT X))) Here's where we get clause 8: (8 ROOT (X Y (AND (NOT Y) (NOT X)))) Let's resolve clauses 7 and 8 on the indicated literal. ; Clause 7: (Z (AND (NOT Z) (NOT Y) (NOT X)) (NOT (AND (NOT Y) (NOT X)))) ; Clause 8: (X Y (AND (NOT Y) (NOT X))) ; Literal: (AND (NOT Y) (NOT X)) ; Resolvent: (Z (AND (NOT Z) (NOT Y) (NOT X)) X Y) Now we execute the next step in the chain: (9 (NOT Z)) Clause 9 from *proof* is given by: (9 ROOT ((NOT (AND (NOT Y) (NOT Z))) (NOT Z))) Resolve this against previous resolvent using literal (NOT Z) to obtain: ((AND (NOT Z) (NOT Y) (NOT X)) X Y (NOT (AND (NOT Y) (NOT Z)))) ... and so on. We've illustrated how zzchk-run-proof works, ultimately to produce a clause consisting of just the negation of the input AIG. ============================================================ === The checker ============================================================ Next we discuss the checker function, zzchk-check. Here is the key correctness theorem that we used in intro.lisp, from aig/zz-check.lisp. Time does not permit discussing the proof of this theorem, which is a routine ACL2 proof. (defthm zzchk-check-correct (implies (zzchk-check (aig-norm aig) proof) (not (aig-eval aig env))) :hints ...) Here is a slightly simplified definition of function zzchk-check from aig/zz-check.lisp. (defun zzchk-check (aig proof) (declare (xargs :guard (or (null aig) (zzchk-run-proof-guard proof)))) (cond ((null aig) t) (t (let ((proof-length (len proof))) (mv-let (ctx val) (zzchk-run-proof proof (1+ proof-length)) (cond (ctx (prog2$ (cw ...) nil)) ; failed ((not (consp val)) nil) ; failed (shouldn't occur) ((let* ((last-step (car val)) (last-cl (and (consp last-step) (cdr last-step)))) (cond ((not (and (consp last-cl) (null (cdr last-cl)))) (prog2$ (cw ...) nil)) ; failed (shouldn't occur) ((hons-equal aig (aig-not (aig-norm (car last-cl)))) t) (t ; failed (proved the wrong thing!) (prog2$ (cw ...) nil))))))))))) The key function called above is zzchk-run-proof. Here is the definition. (defun zzchk-run-proof (proof alist) ; We return an alist that extends the given alist, associating ids with ; generated clauses. Note that the second argument is initially a fast alist, ; and we maintain that property as we recur. (declare (xargs :guard (zzchk-run-proof-guard proof) :guard-hints (("Goal" :expand ((zzchk-run-proof-guard proof)))))) (cond ((endp proof) (mv nil alist)) (t (let* ((step (car proof)) (id (car step)) (typ (cadr step)) (data (cddr step))) (er-let*-cmp ((cl (case typ (root (zzchk-root data id)) ; cl = data if no error (chain (zzchk-chain data id alist)) (t (er-cmp 'zzchk-run-proof "Unexpected type, ~x0" typ))))) (zzchk-run-proof (cdr proof) (hons-acons id cl alist))))))) The two key functions called above are zzchk-root and zzchk-chain. The function (zzchk-root cl id) checks that cl is a Tseiten clause. It ignores id except for error reporting. For zzchk-chain we take a look, top-down, simplifying the definitions a bit. Recall that a chain is of the form: ; (id0 ; (lit1 . id1) (lit2 . id2) (lit3 . id3) ... (litk . idk)) So we look up id0 for our starting clause, and then recur on the above alist, (lit1 . id1) (lit2 . id2) (lit3 . id3) ... (litk . idk)). Notice that as we recur in zzchk-chain1, we cl+ is a fast-alist form of the current clause; literals mapped to t are in the clause. (defun zzchk-chain (chain id cl-alist) (er-let*-cmp ((cl (lookup-cl (car chain) cl-alist 'zzchk-chain))) (zzchk-chain1 (cdr chain) (hons-put-list cl t 'cl+-final-cdr) cl-alist))) (defun zzchk-chain1 (chain cl+ cl-alist) (cond ((endp chain) (mv nil (cl+2cl cl+))) (t (er-let*-cmp ((cl2 (lookup-cl (cdar chain) cl-alist 'zzchk-chain1))) (zzchk-chain1 (cdr chain) (zzchk-resolve cl+ cl2 (caar chain)) cl-alist))))) (defun cl+2cl (cl+) (declare (xargs :guard t)) (let ((alist (hons-shrink-alist cl+ 'cl+-final-cdr))) (strip-nonnil-cars (fast-alist-free alist) nil))) (defun zzchk-resolve (cl1+ cl2 lit) (zzchk-resolve1 (hons-acons (zzchk-negate-lit lit) nil cl1+) cl2 lit)) (defmacro zzchk-negate-lit (lit) `(aig-not ,lit)) (defun zzchk-resolve1 (cl1+ cl2 lit) (declare (xargs :guard t)) (cond ((atom cl2) cl1+) ((hons-equal (car cl2) lit) (zzchk-resolve1 cl1+ (cdr cl2) nil)) (t (zzchk-resolve1 (hons-acons (car cl2) t cl1+) (cdr cl2) lit)))) ============================================================ === A small introductory example of proof generation ============================================================ DEMO: (add-include-book-dir :cbooks "/Users/kaufmann/fh/e/current/e/cbooks") (set-inhibit-warnings "theory") ; avoid some annoying warnings (include-book "aig/zz-check" :dir :cbooks) (set-zzchk-debug-level 2) ; optional (defconst *aig* (aig-not (aig-iff (aig-or 'x (aig-or 'y 'z)) (aig-or 'z (aig-or 'y 'x))))) (include-book "g-logic/gl-extras" :dir :cbooks) (assign zz-proof-alist 'zz-proof-alist) ; turn on proof generation (zz-sat *aig*) ; Call external solver, ZZ (more below) (cdr (hons-get *aig* (@ zz-proof-alist))) (defconst *proof* ) ; paste in result of previous evaluation (defthm aig-is-unsat (not (aig-eval *aig* env)) :hints (("Goal" :use ((:instance zzchk-check-correct (aig *aig*) (proof *proof*))) :in-theory '((zzchk-check) (aig-norm))))) (pe 'zz-sat) (pe 'zz-sat-exec) (fmx "Search for include-raw in file zz.lisp printed out above.~%~ Then search for zz-sat-exec in the resulting file zz-raw.lsp.~%~ Note the use there of zz-proof-alist.~%") (zz-sat ; can also be used to generate counterexamples (aig-not (aig-iff (aig-or 'x 'y) (aig-or 'z (aig-or 'y 'x))))) ============================================================ === Two certification runs: === (1) ZZ proof generation === (2) ZZ proof checking ============================================================ We do two runs of book certification. (See :doc set-write-acl2x for details of how that works.) - The first run of certify-book causes ZZ to generate proofs, and hence requires a trust tag so that we can include call that external tool. The ZZ proofs are stored in generated file two-runs.acl2x, where a fast-alist associates AIGs with representations of their proofs. - The second certify-book reads a so-called "expansion-alist" from file two-runs.acl2x, which avoids calling ZZ and hence avoids the need for a trust tag. Here's how that works. These two steps are actually orchestrated automatically by the Makefile: make clean time make two-runs.cert # To do them all: time make -j 4 acl2h (include-book "two-runs") ; no trust tags or other warnings! === (1) ZZ proof generation First certify-book run: Write out a .acl2x file. .......... ; acl2h (set-write-acl2x t state) ; enable .acl2x file generation (ld "two-runs.acl2") ; certify ; Look at the contents of the resulting .acl2x file: (read-acl2x-file "two-runs.acl2x" "two-runs.lisp" 100 t 'top state) (quit) .......... === (2) ZZ proof checking Second certify-book run: Certify based on contents of the .acl2x file. So we proceed as above, but without the set-write-acl2x command. It's as though we pasted the defconst for for *proof* into two-runs.lisp in place of the make-event form, before certifying. .......... ; acl2h ; Now certify, replacing into two-runs.lisp using two-runs.acl2x: (ld "two-runs.acl2") :pe *proof* .......... ============================================================ === Some remarks on the use of GL ============================================================ Let's take a look at book gl-example.lisp. ..... Here's something I'll run. We'll find the output useful in understanding what follows. (I'll explain a bit about the uses of defattach but not about the fancy computed hints and clause processors provided by the GL system.) (include-book "gl-example") :trans1 (GL-AIG-MODE) :trans1 (GL::GL-AIG-PROOF-CHECKING-MODE) Our running example will now be the first top-level form having the shape (gl::with-recorded-proofs (def-gl-thm ...)). Let's look at the single-step macroexpansion of that form. Here it is, after a bit of harmless editing. (MAKE-EVENT (PROGN (DEFTTAG GL::CHECK-UNSAT-PROOF) (INCLUDE-BOOK "/g-logic/gl-extras") (PROGN! :STATE-GLOBAL-BINDINGS ((ZZ-PROOF-ALIST 'ZZ-PROOF-ALIST)) (SKIP-PROOFS (GL-AIG-MODE)) ; Evaluation of the following form generates proofs, because state ; global 'ZZ-PROOF-ALIST is bound during the resulting call of ; gl::bfr-sat-zz (the current attachment to gl::bfr-sat). That call ; saves the proofs in a new value of 'ZZ-PROOF-ALIST, which is a fast ; alist, where each pair associates an AIG with its proof. (LET ((BODY `(WITH-OUTPUT :OFF (EVENT SUMMARY) (ENCAPSULATE NIL (LOCAL (MAKE-EVENT '(PROGN (DEFCONST GL::*UNSAT-PROOFS-TEMP* (MAKE-FAL ',(F-GET-GLOBAL 'ZZ-PROOF-ALIST STATE) 'ZZ-PROOF-ALIST)) (DEFUN GL::UNSAT-PROOFS-TEMP NIL (DECLARE (XARGS :GUARD T)) GL::*UNSAT-PROOFS-TEMP*) (DEFATTACH GL::UNSAT-PROOFS GL::UNSAT-PROOFS-TEMP) ; The following event generates a defattach event that attaches ; bfr-sat-check-proof to bfr-sat, which is justified by the theorem ; bfr-sat-check-proof-unsat discussed above. (GL::GL-AIG-PROOF-CHECKING-MODE)))) )))) (VALUE-TRIPLE (LIST 'MAYBE-SKIP-PROOFS BODY) :ON-SKIP-PROOFS T))))) Let's consider the above BODY returned by make-event expansion, ignoring the MAYBE-SKIP-PROOFS wrapper for the moment. It includes a call of Sol's fancy def-gl-thm macro, which ultimately calls gl::bfr-sat. (GL::GL-AIG-PROOF-CHECKING-MODE) expands to forms that include this one: (DEFATTACH (GL::BFR-SAT GL::BFR-SAT-CHECK-PROOF) ...) ; from g-logic/bfr-proof-check.lisp, in package GL (defun bfr-sat-check-proof (prop) (declare (xargs :guard t)) (bfr-case :bdd (mv nil nil nil) :aig (cond ((check-unsat-proof prop (cdr (hons-get prop (unsat-proofs)))) (mv nil t nil)) (t (mv nil nil nil))))) ; from g-logic/bfr-proof-check.lisp: (defun gl::check-unsat-proof (gl::prop gl::proof) (declare (xargs :guard t)) (and (zzchk-run-proof-guard gl::proof) (zzchk-check (aig-norm gl::prop) gl::proof))) ; Above, where (GL::UNSAT-PROOFS-TEMP) = value of 'ZZ-PROOF-ALIST: (DEFATTACH GL::UNSAT-PROOFS GL::UNSAT-PROOFS-TEMP) ============================================================ === Maybe-skip-proofs ============================================================ Use of (include-book "make-event/acl2x-help" :dir :system) defines the maybe-skip-proofs macro as follows, using a more general mechanism developed by Sol Swords than what I developed originally. (defmacro maybe-skip-proofs (form) `(acl2x-replace (skip-proofs ,form) ,form :single-pass ,form ;; Is this what we want? :outside-certification (skip-proofs ,form))) From the comments: ;; (ACL2X-REPLACE PASS1 PASS2) runs the event PASS2 unless we are in the first ;; pass of a two-pass certification. If we are in that first pass, it runs ;; PASS1, but leaves it in a specially-formed wrapper so that in ;; postprocessing, the recorded version in the produced .acl2x file will ;; actually be PASS2. ;; Note that a certain function must be attached to acl2x-expansion-alist in ;; order for this to work. We perform this attachment in this book, but it may ;; be undone. You may use (use-acl2x-replace) to ensure that this attachment ;; is in place locally, or (use-acl2x-replace!) to put it in place globally. ;; (no-acl2x-replace) removes this attachment. The file concludes as follows. (use-acl2x-replace!) which actually expands to: (defattach acl2x-expansion-alist acl2x-expansion-alist-replacement) where acl2x-expansion-alist-replacement is defined in the above book. The function acl2x-expansion-alist is what is called to write out the .acl2x file. ============================================================ === Interface with ZZ (during proof generation) ============================================================ I doubt we'll have any time to go over this section, which is just as well because it's been awhile since it's been cached into my head. But I include some key pieces of the story for reference, sufficient to get a sense of the interface. In g-logic/g-sat.lisp we find the following definition of the function gl::bfr-sat-zz mentioned above (ultimately invoked by the computed hint). (defun bfr-sat-zz (prop) (declare (xargs :guard t)) (bfr-case :bdd (mv nil nil nil) ;; fail :aig (b* ((- (cw "Running ZZ-SAT... ")) (res (time$ (acl2::zz-sat prop) :msg "done; cpu: ~sc real: ~st mem: ~sa~%"))) (case (car res) (acl2::sat (mv t t (cdr res))) (acl2::unsat (mv nil t nil)) (t (mv nil nil nil)))))) The original definition of acl2::zz-sat is smashed by a load (using a trust tag) of file ../../ZZ/Centaur/zz-raw.lsp, where we find this call in its definition. (zz-aig-container (and (boundp-global 'zz-proof-alist *the-live-state*) (f-get-global 'zz-proof-alist *the-live-state*))) The argument of zz-aig-container indicates whether proof-logging is to be turned on in ZZ: (defun zz-aig-container (&optional with-proof-logging) (let ((aig (ccl:external-call "AIG_create" :unsigned (if with-proof-logging 1 0) :address))) (ccl:external-call "AIG_setCB" :address aig :address *zz-callback* :address) (ccl:external-call "AIG_setTimeout" :address aig (:unsigned 64) 1000000 :address) aig)) Similar external calls are made under zz-sat, in particular a call of this function: (defun zz-aig-solve (aig-container assumps var-ht) (let ((res (ccl:external-call "c_AIG_solve" :address aig-container :address assumps :unsigned))) (case res (0 '(failed)) (2 '(unsat)) (3 (cons 'sat (zz-read-model aig-container var-ht)))))) Ultimately, zz-sat calls check-zz-sat-ans: (defun check-zz-sat-ans (aig zz-aig inv-node-ht ans &aux (state *the-live-state*)) (case (car ans) (sat ) (unsat (when (and aig (boundp-global 'zz-proof-alist state) (f-get-global 'zz-proof-alist state) (not (hons-get aig (f-get-global 'zz-proof-alist state)))) (zz-add-proof-pair aig (zz-create-proof zz-aig inv-node-ht))) ans) (t ans))) Here is the definition of the key function called above: (defun zz-create-proof (zz-aig inv-node-ht &key (verbose *zz-create-proof-verbose*) (array-size *zz-create-proof-array-size*)) (assert zz-aig) (assert inv-node-ht) (unwind-protect (progn (when (> verbose 0) (cw "~%Note: Starting C proof extraction....~|")) (zz-pfl-log-proof zz-aig verbose array-size) (when (> verbose 0) (cw "Note: Completed C proof extraction.~|") (cw "Note: Generating Lisp-level proof....~|")) (let ((proof (zz-proof inv-node-ht))) (when (> verbose 0) (cw "Note: Generated Lisp-level proof of length ~x0:~|" (length proof)) (let ((roots 0) (chains 0) (steps 0)) (loop for x in proof do (case (cadr x) (root (incf roots)) (chain (incf chains) (setq steps (+ (length (cddr x)) steps))))) (cw "~t0~x1 root clauses,~|~t0~x2 chain steps, and~t0~x3 ~ total resolutions to perform.~|" 6 roots chains steps))) proof)) (zz-pflArray-finalize))) And here is the definition of the key function called just above. (defun zz-proof (inv-node-ht) (zz-pflArray-prepare-to-read) (let (proof) (loop (let ((step-type (zz-pflArray-read))) (case step-type ; type of step (2 ; end (return)) (t (push (let ((count (zz-pflArray-read))) (cons (zz-pflArray-read) ; clause-id (case step-type (0 (cons 'root (loop for i from 2 to count collect (lit-to-aig (zz-pflArray-read) inv-node-ht)))) (1 (assert (<= 3 count)) (assert (evenp count)) (list* 'chain (zz-pflArray-read) ; initial clause id ; Now collect literal-clause pairs to create successive resolvents. (loop for i from 1 to (floor (- count 2) 2) collect (cons (lit-to-aig (zz-pflArray-read) inv-node-ht) (zz-pflArray-read))))) (t (error "Unexpected step-type in zz-proof (file ~ zz-raw.lsp), ~s." step-type))))) proof))))) (nreverse proof))) ============================================================