diff options
Diffstat (limited to 'books/workshops/2004/sumners-ray/support')
| -rw-r--r-- | books/workshops/2004/sumners-ray/support/.gitignore | 5 | ||||
| -rw-r--r-- | books/workshops/2004/sumners-ray/support/Makefile | 49 | ||||
| -rw-r--r-- | books/workshops/2004/sumners-ray/support/basis.lisp | 295 | ||||
| -rw-r--r-- | books/workshops/2004/sumners-ray/support/cert_pl_exclude | 2 | ||||
| -rw-r--r-- | books/workshops/2004/sumners-ray/support/crit.lisp | 125 | ||||
| -rwxr-xr-x | books/workshops/2004/sumners-ray/support/invp.lsp | 1660 | ||||
| -rw-r--r-- | books/workshops/2004/sumners-ray/support/mesi.lisp | 227 | ||||
| -rw-r--r-- | books/workshops/2004/sumners-ray/support/records.lisp | 644 | ||||
| -rw-r--r-- | books/workshops/2004/sumners-ray/support/sets.lisp | 1220 | ||||
| -rw-r--r-- | books/workshops/2004/sumners-ray/support/total-order.lisp | 30 |
10 files changed, 4257 insertions, 0 deletions
diff --git a/books/workshops/2004/sumners-ray/support/.gitignore b/books/workshops/2004/sumners-ray/support/.gitignore new file mode 100644 index 0000000..844dd58 --- /dev/null +++ b/books/workshops/2004/sumners-ray/support/.gitignore @@ -0,0 +1,5 @@ +*.rpt +run.date +run.err +run.log +success.txt diff --git a/books/workshops/2004/sumners-ray/support/Makefile b/books/workshops/2004/sumners-ray/support/Makefile new file mode 100644 index 0000000..4c174c4 --- /dev/null +++ b/books/workshops/2004/sumners-ray/support/Makefile @@ -0,0 +1,49 @@ +# Instructions: + +# Before starting, see "Dependencies" below. + +# In the shell, execute +# make +# to certify all books. +# To clean up (removing files *.cert, *.o, *.fasl, etc.), in the shell execute +# make clean + +top1: + @echo "Using ACL2=$(ACL2)" + @$(MAKE) top + +top: success.txt + +success.txt: mesi.cert crit.cert invp.lsp + @echo "Making `pwd`/success.txt on `date`" + @rm -f success.txt workxxx + @date > run.date + @echo '(value :q)' > workxxx + @echo '(acl2::lp)' >> workxxx + @echo '(acl2::ld "invp.lsp")' >> workxxx + @echo '(value :q)' >> workxxx + @echo '(acl2::good-bye)' >> workxxx + @$(ACL2) < workxxx > run.log 2> run.err + @rm -f workxxx TMP* + @if [ ! -f success.txt ]; then \ + echo "**CERTIFICATION FAILED**"; \ + exit 1 ; \ + else \ + ls -al success.txt ; \ + fi + +include ../../../../Makefile-generic + +# Need to omit invp from BOOKS because targets like all-fas would try to +# include invp as a book: +BOOKS = basis crit mesi records sets total-order + + +clean: clean-more + +clean-more: + rm -f *.rpt + rm -f success.txt + rm -f run.date run.log run.err + +-include Makefile-deps diff --git a/books/workshops/2004/sumners-ray/support/basis.lisp b/books/workshops/2004/sumners-ray/support/basis.lisp new file mode 100644 index 0000000..b9ccacf --- /dev/null +++ b/books/workshops/2004/sumners-ray/support/basis.lisp @@ -0,0 +1,295 @@ +(in-package "ACL2") + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;;;;;;;;;; definitions and rules for time operators ;;;;;;;;;;;;;;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +;; Even though the invariant prover proves invariants by an induction over time +;; (where time is understood to be natural number), we prefer to use our own +;; operators t+, t-, t0, and tzp to define the behavior of the time +;; parameter. This avoids issues which may arise with the aliasing of ACL2 +;; arithmetic and allows us to define time in a manner which avoids the need to +;; introduce natp hypothesis. + +(encapsulate + (((t- *) => *) + ((t0) => *) + ((tzp *) => *) + ((tmsr *) => *)) + +(local (defun tzp (n) (or (atom n) (car n)))) +(local (defun t- (n) (if (tzp n) n (cdr n)))) +(local (defun t0 () nil)) +(local (defun tmsr (n) (if (tzp n) 0 (1+ (tmsr (cdr n)))))) + +(defthm tzp-t0redux (equal (tzp (t0)) t)) +(defthm tmsr-ordinal (o-p (tmsr n))) +(defthm tzp-tmsr-o< (implies (not (tzp n)) (o< (tmsr (t- n)) (tmsr n)))) + +;; The following definition and theorems are not exported because we do not +;; want any user functions which are defined in terms of t+, so it is built in +;; directly in the rewriter. We prove these theorems here to demonstrate that +;; the built-in rules in the rewriter are valid. + +(local (defun t+ (n) (cons nil n))) + +;; The following theorem is included to demonstrate that every object in the +;; ACL2 universe is either tzp or equal to (t+ n) for some n. This also means +;; that if a theorem is proven for (t0) and (t+ n) for every n, then it is true +;; for all n since the only property that we export about (t0) is (tzp (t0)). + +(local (defthm time-totality (implies (not (tzp n)) (equal (t+ (t- n)) n)))) +(local (defthm tzp-t+redux (equal (tzp (t+ n)) nil))) +(local (defthm t--t+-redux (equal (t- (t+ n)) n)))) + + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;;;;;;;;;;;;;;;;; auxiliary helper functions ;;;;;;;;;;;;;;;;;;;;;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(defmacro char-in-range (c x y) + `(let ((a (char-code ,c))) + (and (>= a (char-code ,x)) + (<= a (char-code ,y))))) + +(defun str-to-number1 (str i n acc) + (declare (xargs :measure (nfix n))) + (cond ((zp n) acc) + ((char-in-range (char str i) #\0 #\9) + (str-to-number1 str (1+ i) (1- n) + (+ (* acc 10) + (- (char-code (char str i)) + (char-code #\0))))) + (t (er hard 'str-to-number + "ill-formed token encountered: ~x0" + str)))) + +(defun str-to-number (str) + (str-to-number1 str 0 (length str) 0)) + +(defun digit-to-str (dig) + (string (code-char (+ dig (char-code #\0))))) + +(defun number-to-str1 (num d) + (declare (xargs :measure (nfix d))) + (cond ((zp d) + (er hard 'number-2-str + "attempt to print too large natural: ~x0" num)) + ((not (and (integerp num) (>= num 0))) + (er hard 'number-2-str + "attempt to print non-natural: ~x0" num)) + ((< num 10) (digit-to-str num)) + (t (string-append (number-to-str1 (floor num 10) (1- d)) + (digit-to-str (mod num 10)))))) + +(defun number-to-str (num) + (number-to-str1 num 1000000)) + +(defun pos-of-char1 (ch str i n) + (declare (xargs :measure (nfix n))) + (cond ((zp n) nil) + ((>= i (length str)) nil) + ((eql (char str i) ch) i) + + (t (pos-of-char1 ch str (1+ i) (1- n))))) + +(defun pos-of-char (ch str) + (pos-of-char1 ch str 0 (length str))) + +(defun to-string (obj) + (cond ((stringp obj) obj) + ((characterp obj) (string obj)) + ((symbolp obj) (string-downcase (symbol-name obj))) + ((natp obj) (number-to-str obj)) + (t (er hard 'to-string + "don't know how to convert to string: ~x0" obj)))) + +(defun snap-objs (objs) + (if (endp objs) "" + (string-append (to-string (first objs)) + (snap-objs (rest objs))))) + +(defmacro snap (&rest objs) + `(snap-objs (list ,@objs))) + +(defmacro snap-sym (&rest objs) + `(intern (string-upcase (snap ,@objs)) "ACL2")) + +(defmacro snap-key (&rest objs) + `(intern (string-upcase (snap ,@objs)) "KEYWORD")) + + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;;;;;;;;;; macro for generating if-lifting rules ;;;;;;;;;;;;;;;;;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(defun replace-arg (call arg term) + (cond ((endp call) + (er hard 'replace-arg "did not find arg")) + ((eq arg (first call)) + (cons term (rest call))) + (t + (cons (first call) + (replace-arg (rest call) arg term))))) + +(defun if-lift-call (arg call) + `(defthm ,(snap-sym 'if-lift- (first call) '- arg) + (equal ,(replace-arg call arg '(if tst tbr fbr)) + (if tst ,(replace-arg call arg 'tbr) ,(replace-arg call arg 'fbr))))) + +(defun if-lifts-call (args call) + (if (endp args) () + (cons (if-lift-call (first args) call) + (if-lifts-call (rest args) call)))) + +(defun if-lifts-calls (calls) + (if (endp calls) () + (append (if-lifts-call (rest (first calls)) (first calls)) + (if-lifts-calls (rest calls))))) + +(defmacro if-lift-rules (&rest calls) + (cons 'progn (if-lifts-calls calls))) + + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;;;;;;;;;; macro for generating abstraction rules ;;;;;;;;;;;;;;;;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(defun abs-termp (x) + (and (consp x) + (not (quotep x)) + (pseudo-termp x))) + +(defun abs-term-listp (x) + (or (null x) + (and (consp x) + (abs-termp (first x)) + (abs-term-listp (rest x))))) + +(defun make-abs-thm (trm n) + `(defthm ,(snap-sym 'abstract- (first trm) '- n) + (equal ,trm (hide ,trm)) + :hints (("Goal" :expand (hide ,trm))))) + +(defun make-abs-thms (trms n) + (if (endp trms) () + (cons (make-abs-thm (first trms) n) + (make-abs-thms (rest trms) (1+ n))))) + +(defmacro abstract-terms (&rest trms) + (declare (xargs :guard (abs-term-listp trms))) + `(progn ,@(make-abs-thms trms 0))) + + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;;;;;;;;;; macro for generating finite case-splits ;;;;;;;;;;;;;;;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(defun finite-case-term (tgt cases) + (if (endp cases) tgt + (let ((c (first cases))) + `(if (equal ,tgt ,c) ,c ,(finite-case-term tgt (rest cases)))))) + +(defmacro finite-cases (name class target cases) + (declare (xargs :guard (and (symbolp name) + (member class '(:state :input)) + (consp target) + (symbol-listp target) + (true-listp cases)))) + (let ((op! (snap-sym (first target) '!))) + `(encapsulate + () + (defun ,op! ,(rest target) ,target) + (defthm ,(snap-sym name '-finite-cases) + (implies (syntaxp (equal n (quote ,(if (eq class :input) '(t+ n) 'n)))) + (equal ,target ,(finite-case-term (cons op! (rest target)) cases)))) + ,@(and (eq class :state) + `((defthm ,(snap-sym name '-unwrap-cases) + (implies (syntaxp (or (equal n '(t0)) (equal n '(t+ n)))) + (equal ,(cons op! (rest target)) ,target))))) + (in-theory (disable ,op!))))) + + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;;;;;;;;;;;;;;;;; basic rules for equal and if ;;;;;;;;;;;;;;;;;;;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +;; We use if* here to avoid ACL2 restriction on if lhs rewrite rules. The +;; invariant prover will read any lhs if* rules as if rules and so the user is +;; encouraged to make use of this bypass around ACL2 when they wish to have +;; rules which have 'if as the outermost lhs operator. + +(defthm if-if-lift-rule + (equal (if* (if x y z) a b) + (if x (if y a b) (if z a b)))) + +(defthm equal-if-lift-lhs + (equal (equal (if x y z) a) + (if x (equal y a) (equal z a)))) + +(defthm equal-if-lift-rhs + (equal (equal a (if x y z)) + (if x (equal a y) (equal a z)))) + +(defthm equal-orient-rule + (implies (syntaxp (term-order x y)) + (equal (equal x y) (equal y x))) + ;; I have to add the following to keep ACL2 from adding + ;; a loop stopper by default :( + :rule-classes ((:rewrite :loop-stopper ()))) + + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;;;;;;;;;;;;;;;;;;;;;; define-system macro ;;;;;;;;;;;;;;;;;;;;;;;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(defun reg-declp (reg) + (and (true-listp reg) + (equal (length reg) 4) + (symbolp (first reg)) + (symbol-listp (second reg)))) + +(defun reg-declsp (regs) + (or (null regs) + (and (consp regs) + (reg-declp (first regs)) + (reg-declsp (rest regs))))) + +(defun reg-fn (reg) + (list `(defun ,(first reg) ,(second reg) + (declare (xargs :measure (tmsr n))) + (if (tzp n) ,(third reg) (let ((n- (t- n))) ,(fourth reg)))))) + +(defun reg-thm (reg) + (list `(if-lift-rules (,(first reg) ,@(second reg))) + `(defthm ,(snap-sym (first reg) '-tzp) + (implies (tzp n) + (equal (,(first reg) ,@(second reg)) + ,(third reg)))) + `(defthm ,(snap-sym (first reg) '-t+) + (implies (not (tzp n)) + (equal (,(first reg) ,@(second reg)) + (let ((n- (t- n))) ,(fourth reg))))))) + +(defun reg-fns (regs) + (if (endp regs) () + (append (reg-fn (first regs)) + (reg-fns (rest regs))))) + +(defun reg-thms (regs) + (if (endp regs) () + (append (reg-thm (first regs)) + (reg-thms (rest regs))))) + +(defmacro define-system (name &rest regs) + (declare (xargs :guard (and (symbolp name) (reg-declsp regs))) + (ignore name)) + (list* 'progn + (cons 'mutual-recursion (reg-fns regs)) + (reg-thms regs))) diff --git a/books/workshops/2004/sumners-ray/support/cert_pl_exclude b/books/workshops/2004/sumners-ray/support/cert_pl_exclude new file mode 100644 index 0000000..833501d --- /dev/null +++ b/books/workshops/2004/sumners-ray/support/cert_pl_exclude @@ -0,0 +1,2 @@ +This directory has a custom Makefile, so it is excluded from +certification based on cert.pl. diff --git a/books/workshops/2004/sumners-ray/support/crit.lisp b/books/workshops/2004/sumners-ray/support/crit.lisp new file mode 100644 index 0000000..03a1864 --- /dev/null +++ b/books/workshops/2004/sumners-ray/support/crit.lisp @@ -0,0 +1,125 @@ +(in-package "ACL2") +(include-book "basis") + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;;;;;;; definitions for example critical section system ;;;;;;;;;;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(encapsulate (((i *) => *)) (local (defun i (n) n))) + +(define-system critical + (in-critical (n) nil + (if (in-critical n-) + (/= (i n) (critical-id n-)) + (= (status (i n) n-) :try))) + + (critical-id (n) nil + (if (and (not (in-critical n-)) + (= (status (i n) n-) :try)) + (i n) + (critical-id n-))) + + (status (p n) :idle + (if (/= (i n) p) (status p n-) + (case (status p n-) + (:try (if (in-critical n-) :try :critical)) + (:critical :idle) + (t :try))))) + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;;;;;;; definitions for example critical section system ;;;;;;;;;;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(encapsulate (((a) => *) ((b) => *)) + (local (defun a () 1)) (local (defun b () 2)) + (defthm a-/=-b (not (equal (a) (b)))) + (defthm a-non-nil (not (equal (a) nil))) + (defthm b-non-nil (not (equal (b) nil)))) + +; Added after v7-2 by Matt K. since the define-system just below introduces a +; non-recursive definition with a measure. +(set-bogus-measure-ok t) + +(define-system critical-spec + (ok (n) t + (not (and (= (status (a) n-) :critical) + (= (status (b) n-) :critical))))) + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;;;;;;;; proof of invariant ok via inductive invariant ;;;;;;;;;;;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +; we have to use a different versions of the above functions which are +; defined on natural time rather than the abstracted t+,t-,tzp time +; defined in basis.lisp. + +(mutual-recursion + (defun in-critical* (n) + (declare (xargs :measure (nfix n))) + (if (zp n) nil + (let ((n- (1- n))) + (if (in-critical* n-) + (/= (i n) (critical-id* n-)) + (= (status* (i n) n-) :try))))) + + (defun critical-id* (n) + (declare (xargs :measure (nfix n))) + (if (zp n) nil + (let ((n- (1- n))) + (if (and (not (in-critical* n-)) + (= (status* (i n) n-) :try)) + (i n) + (critical-id* n-))))) + + (defun status* (p n) + (declare (xargs :measure (nfix n))) + (if (zp n) :idle + (let ((n- (1- n))) + (if (/= (i n) p) (status* p n-) + (case (status* p n-) + (:try (if (in-critical* n-) :try :critical)) + (:critical :idle) + (t :try)))))) + + (defun ok* (n) + (declare (xargs :measure (nfix n))) + (if (zp n) t + (let ((n- (1- n))) + (not (and (= (status* (a) n-) :critical) + (= (status* (b) n-) :critical))))))) + +(defun ii-ok-for1 (n i) + (iff (= (status* i n) :critical) + (and (in-critical* n) (= (critical-id* n) i)))) + +(defun ii-ok (n) + (and (ii-ok-for1 n (a)) (ii-ok-for1 n (b)))) + +(defthm bogus-linear + (implies (integerp n) + (equal (+ (- x) x n) n))) + +(defthm ok-is-invariant + (and (ii-ok 0) (ok* 0) + (implies (and (natp n) (ii-ok n)) + (and (ok* (1+ n)) (ii-ok (1+ n))))) + :hints (("Goal" :in-theory (disable (ii-ok) (ok*))))) + + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;;;;;;;; a few auxiliary rules for the invariant prover ;;;;;;;;;;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +; we will need if-lifting for equal rules in the invariant prover: +(if-lift-rules (equal x y)) + +; we also need to force a case-split on (i n) and (critical-id n) +; the need for a case-split on critical-id is unfortunate and is +; due to some weakness in the prover which needs to be resolved. +(finite-cases process-id :input (i n) ((a) (b))) +(finite-cases critical-id :state (critical-id n) ((a) (b))) + diff --git a/books/workshops/2004/sumners-ray/support/invp.lsp b/books/workshops/2004/sumners-ray/support/invp.lsp new file mode 100755 index 0000000..0254447 --- /dev/null +++ b/books/workshops/2004/sumners-ray/support/invp.lsp @@ -0,0 +1,1660 @@ +#| (ld "invp.lisp") |# + +(in-package "ACL2") + +#| + + invp.lisp + ~~~~~~~~~ + +CODE SECTIONS +------------- + +1. include the basis book which defines numerous operators +2. definition and initialization of ic$ stobj +3. inside-out conditional term rewriter +4. extended rewriting and propagating rep-step +5. invariant checker implementation +6. top-level algorithm and interface +7. some simple test examples + + +TODO LIST +--------- + +1. Add translation of model to Verilog and interface to VIS model checker. + +2. Add deep if-lifting to rewrite-step + +3. Add some tagging of terms to declare the term to be in normal-form to + avoid rewriting terms which are in normal-form. + + +NOTES/ISSUES +------------ + +1. Why do we need to set the translate-flg in the calls of simplify-term?? + +2. Need to write-up arguments for the correctness of all of the reductions + supported in this tool. + +|# + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +#| <SECTION> 1. include the basis book which defines numerous operators |# +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(include-book "basis") + +(defun zip-fms (chars lst) + (cond ((endp lst) ()) + ((endp chars) + (er hard 'zip-fms "too many args to detail!")) + (t (acons (car chars) (car lst) + (zip-fms (cdr chars) (cdr lst)))))) + +(defconst *fms-chars* + '(#\0 #\1 #\2 #\3 #\4 #\5 #\6 #\7 #\8 #\9)) + +(program) + +(defun detail-fn (fmt-str lst chan state) + (declare (xargs :stobjs state)) + (if (not chan) state + (fms fmt-str (zip-fms *fms-chars* lst) chan state nil))) + +(defmacro detail (&rest r) + `(let ((state (detail-fn ,(first r) + ,(cons 'list (rest (butlast r 1))) + (detail-channel ic$) state))) + ,(car (last r)))) + +(defmacro report (&rest r) + `(prog2$ (cw ,@(butlast r 1)) + (detail ,(string-append "REPORT:" (first r)) + ,@(rest r)))) + +(defmacro bozo (&rest r) + `(prog2$ (cw ,@(butlast r 1)) + ,(car (last r)))) + +(defmacro seq (&rest bind) + (cond ((endp bind) + (er hard 'seq + "no body/result expression in seq form")) + ((endp (cdr bind)) + (car bind)) + ((atom (caar bind)) + `(let ((,(caar bind) ,(cadar bind))) + (seq ,@(cdr bind)))) + (t + `(mv-let ,(caar bind) ,(cadar bind) + (seq ,@(cdr bind)))))) + +(defmacro die (&rest r) + `(prog2$ (er hard ,@(butlast r 1)) + ,(car (last r)))) + +(logic) + +(defabbrev bnil () 0) +(defabbrev bnth (i x) (logbitp i x)) + +(defun blist-length (x) + (cond ((atom x) + (er hard 'blist-length "ill-formed")) + ((eq (first x) 'bnil) 0) + ((eq (first x) 'bcons) + (1+ (blist-length (third x)))) + (t (er hard 'blist-length "ill-formed")))) + +(defmacro bcons (b x) + (let ((size (1+ (blist-length x)))) + `(the (unsigned-byte ,size) + (let ((b ,b) + (x (the (unsigned-byte ,size) (* ,x 2)))) + (declare (type (unsigned-byte ,size) x)) + (if b (the (unsigned-byte ,size) (1+ x)) x))))) + +(local ; ACL2 primitive + (defmacro 1+f (x) + `(the-fixnum (1+ (the-fixnum ,x))))) + +(local ; ACL2 primitive + (defmacro 1-f (x) + `(the-fixnum (1- (the-fixnum ,x))))) + +(defmacro modf (x y) + `(the-fixnum (mod (the-fixnum ,x) (the-fixnum ,y)))) + +(defmacro fzp (x) + `(let ((x ,x)) + (declare (type (signed-byte 29) x)) + (or (not (integerp x)) + (<= x 0)))) + +(in-theory (disable ash logbitp)) + +;; We need to get some properties of the functions we deal with from the +;; current ACL2 world. We define the macro fn-prop below for that purpose. +(defabbrev fn-prop (fn prop) + (getprop fn prop nil 'current-acl2-world (w state))) + +;; and more precisely, we will have the unnormalized-body and the formals. +(defabbrev get-formals (fn) + (fn-prop fn 'formals)) + +(defabbrev get-body (fn) + (fn-prop fn 'unnormalized-body)) + +(defabbrev get-normal-body (fn) + (fn-prop fn 'body)) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +#| <SECTION> 2. definition and initialization of ic$ stobj |# +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(program) + +;; we now define a stobj which we use to hold much of the state which +;; we use as a holding area for various parameters and variables which +;; are updated throughout the invariant proof +(defstobj ic$ + (reduce-contexts :type T) + (jump-bound :type T) + (check-bound :type T) + (refine-bound :type T) + (inputs-bound :type T) + (fast-search :type T) + (detail-channel :type T) + (always-check :type T) + (disable-exec :type T) + (num-rep-bits :type T) + (inv-check-result :type T) + ;; the following are merely in the stobj instead of being parameters to dfs + (search-bound :type (signed-byte 29) + :initially 0) + (num-states :type (signed-byte 29) + :initially 0) + (num-inputs :type (signed-byte 29) + :initially 0) + (input-vec :type (array T (0)) + :resizable T) + (inv-bit :type T) + (st-hashtbl :type (array T (0)) + :resizable T)) + +(defun is-prime-number (x y) + (cond ((or (zp x) (= x 1)) t) + ((eql (mod y x) 0) nil) + (t (is-prime-number (1- x) y)))) + +(defun prev-prime-number (x) + (cond ((zp x) 1) + ((is-prime-number x x) x) + (t (prev-prime-number (1- x))))) + +(defun clear-ic$-for-inv-check (ic$) + (declare (xargs :stobjs ic$)) + (seq + (ic$ (resize-st-hashtbl 0 ic$)) ;; this will clear the st-hashtbl + (ic$ (resize-st-hashtbl (prev-prime-number (check-bound ic$)) ic$)) + (ic$ (update-inv-check-result nil ic$)) + ic$)) + +;; we initialize the inv-checker stobj ic$ for the book-keeping we need. +(defun initialize-ic$ (jump-bound + check-bound + refine-bound + inputs-bound + fast-search + detail-file + always-check + disable-exec + reduce-contexts + ic$ + state) + (declare (xargs :stobjs (ic$ state))) + (seq + (ic$ (update-jump-bound jump-bound ic$)) + (ic$ (update-check-bound check-bound ic$)) + (ic$ (update-refine-bound refine-bound ic$)) + (ic$ (update-inputs-bound inputs-bound ic$)) + (ic$ (update-fast-search fast-search ic$)) + (ic$ (update-always-check always-check ic$)) + (ic$ (update-disable-exec disable-exec ic$)) + (ic$ (update-reduce-contexts reduce-contexts ic$)) + (ic$ (clear-ic$-for-inv-check ic$)) + ((channel state) + (if detail-file + (open-output-channel detail-file :character state) + (mv nil state))) + (ic$ (update-detail-channel channel ic$)) + (mv ic$ state))) + +(defun cleanup-ic$ (ic$ state) + (declare (xargs :stobjs (ic$ state))) + (seq + (state (close-output-channel (detail-channel ic$) state)) + (mv ic$ state))) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +#| <SECTION> 3. iterative inside-out conditional term rewriter |# +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(program) + +(defabbrev equiv-ops (a b) + (let ((op-a (if (atom a) a (car a))) + (op-b (if (atom b) b (car b)))) + (and (not (eq op-a 'lambda)) + (eq op-a op-b)))) + +(defabbrev hidep (x) + (and (consp x) (eq (first x) 'hide))) + +(defun equiv-terms1 (x y is-lst) + (cond ((and is-lst (endp x)) (endp y)) + (is-lst (and (equiv-terms1 (first x) (first y) nil) + (equiv-terms1 (rest x) (rest y) t))) + ((hidep x) (equiv-terms1 (second x) y nil)) + ((hidep y) (equiv-terms1 x (second y) nil)) + ((atom x) (eq x y)) + ((atom y) nil) + (t (and (equiv-ops (first x) (first y)) + (equiv-terms1 (rest x) (rest y) t))))) + +(defabbrev equiv-terms (x y) (equiv-terms1 x y nil)) + +(defun bind-args* (vars args rslt) + (if (endp vars) rslt + (bind-args* (rest vars) (rest args) + (cons (cons (first vars) + (first args)) + rslt)))) + +(defabbrev bind-args (vars args) + (bind-args* vars args ())) + +(defun subst-term* (trm alst is-lst in-synp ctx) + (cond + ((and is-lst (endp trm)) ()) + (is-lst (cons (subst-term* (first trm) alst nil in-synp ctx) + (subst-term* (rest trm) alst t in-synp ctx))) + ((atom trm) + (let* ((mtch (assoc-eq trm alst)) + (val (if mtch (cdr mtch) trm))) + (if (not in-synp) val + (list 'quote (if (and (not mtch) (eq trm 'ctx)) ctx val))))) + (t + (let ((op (first trm))) + (cond + ((eq op 'quote) trm) + ((eq op 'synp) (subst-term* (second (fourth trm)) alst nil t ctx)) + (t (cons (if (atom op) (list op) op) + (subst-term* (rest trm) alst t in-synp ctx)))))))) + +(defabbrev subst-term-ctx (trm alst ctx) + (subst-term* trm alst nil nil ctx)) + +(defabbrev subst-term (trm alst) + (subst-term* trm alst nil nil nil)) + +(defabbrev st-phase (st) (car st)) +(defabbrev st-wrld (st) (cadr st)) +(defabbrev st-ens (st) (caddr st)) +(defabbrev st-rew-ctx (st) (cadddr st)) +(defabbrev st-depth (st) (cddddr st)) + +(defun make-init-st (wrld ens rew-ctx depth) + (list* nil wrld ens rew-ctx depth)) + +(defabbrev in-hyps (st) + (if (st-phase st) st (cons t (cdr st)))) + +(defabbrev match-ctx-elem (trm ctx iff) + (cond + ((and iff (equiv-terms trm ctx)) ''t) + ((let ((op (first ctx))) + (or (eq op 'equal) + (and (eq op 'iff) iff))) + (and (equiv-terms trm (second ctx)) + (third ctx))))) + +(defun match-in-ctx* (trm ctx iff) + (and (not (endp ctx)) + (or (match-ctx-elem trm (first ctx) iff) + (match-in-ctx* trm (rest ctx) iff)))) + +(defun match-in-ctx (trm ctx iff) + (if (quotep trm) nil (match-in-ctx* trm ctx iff))) + +(defmacro gprop (name prop) + `(getprop ,name ,prop nil 'current-acl2-world wrld)) + +(defun quoted-args (args) + (or (endp args) + (and (quotep (first args)) + (quoted-args (rest args))))) + +(defun fncall-args (args) + (if (endp args) () + (cons (second (first args)) + (fncall-args (rest args))))) + +(defun merge-alsts (new alst) + (if (endp new) alst + (merge-alsts (cdr new) + (let ((mtch (assoc-eq (caar new) alst))) + (if mtch alst (cons (car new) alst)))))) + +(defun find-nume (pairs rune) + (cond ((endp pairs) nil) + ((equal rune (cdar pairs)) + (caar pairs)) + (t (find-nume (cdr pairs) rune)))) + +(defun rewrt-built-in (op args) + (cond + ((eq op 'if) + (let ((tst (first args)) + (tbr (second args)) + (fbr (third args))) + (cond + ((quotep tst) (if (second tst) tbr fbr)) + ((equal tbr fbr) tbr)))) + ((eq op 'equal) + (let ((lhs (first args)) + (rhs (second args))) + (cond + ((equal lhs rhs) ''t) + ((and (quotep lhs) (quotep rhs)) ''nil)))) + (t + (let ((n (first args))) + (cond + ((and (consp n) (eq (first n) 't+)) + (cond ((eq op 'tzp) ''nil) + ((eq op 't-) (second n))))))))) + +(defun all-vars-bound* (trm alst is-lst) + (cond + ((and is-lst (endp trm)) t) + (is-lst (and (all-vars-bound* (first trm) alst nil) + (all-vars-bound* (rest trm) alst t))) + ((atom trm) (assoc-eq trm alst)) + ((eq (first trm) 'quote) t) + (t (all-vars-bound* (rest trm) alst t)))) + +(defabbrev all-vars-bound (trm alst) + (all-vars-bound* trm alst nil)) + +(defun subtermp1 (x y is-lst) + (cond ((and is-lst (endp y)) nil) + (is-lst (or (subtermp1 x (first y) nil) + (subtermp1 x (rest y) t))) + ((equiv-terms x y) t) + ((atom y) nil) + ((eq (first y) 'quote) nil) + (t (subtermp1 x (rest y) t)))) + +(defun subtermp (x y) (subtermp1 x y nil)) + +(defun subterm-ctx (lhs ctx) + (and (not (endp ctx)) + (or (subtermp lhs (first ctx)) + (subterm-ctx lhs (rest ctx))))) + +(defabbrev func-symb (term) + (let ((op (car term))) (if (atom op) op (car op)))) + +(mutual-recursion +(defun unify-1way1 (pat term alist) + (cond + ((variablep pat) + (let ((pair (assoc-eq pat alist))) + (cond (pair (cond ((equiv-terms (cdr pair) term) + (mv t alist)) + (t (mv nil alist)))) + (t (mv t (cons (cons pat term) alist)))))) + ((fquotep pat) + (cond ((equal pat term) (mv t alist)) + (t (mv nil alist)))) + ((variablep term) (mv nil alist)) + ((fquotep term) + (let ((func-symb (func-symb pat))) + (cond + ((acl2-numberp (cadr term)) + (case func-symb + (binary-+ + (cond + ((quotep (fargn pat 1)) + (unify-1way1 (fargn pat 2) (kwote (- (cadr term) (fix (cadr (fargn pat 1))))) alist)) + ((quotep (fargn pat 2)) + (unify-1way1 (fargn pat 1) (kwote (- (cadr term) (fix (cadr (fargn pat 2))))) alist)) + (t (mv nil alist)))) + (binary-* + (cond + ((and (quotep (fargn pat 1)) + (integerp (cadr (fargn pat 1))) + (> (abs (cadr (fargn pat 1))) 1)) + (unify-1way1 (fargn pat 2) (kwote (/ (cadr term) (cadr (fargn pat 1)))) alist)) + ((and (quotep (fargn pat 2)) + (integerp (cadr (fargn pat 2))) + (> (abs (cadr (fargn pat 2))) 1)) + (unify-1way1 (fargn pat 1) (kwote (/ (cadr term) (cadr (fargn pat 2)))) alist)) + (t (mv nil alist)))) + (unary-- + (cond + ((>= (+ (realpart (cadr term)) (imagpart (cadr term))) 0) + (mv nil alist)) + (t (unify-1way1 (fargn pat 1) (kwote (- (cadr term))) alist)))) + (unary-/ + (cond + ((or (>= (* (cadr term) (conjugate (cadr term))) 1) (eql 0 (cadr term))) + (mv nil alist)) + (t (unify-1way1 (fargn pat 1) (kwote (/ (cadr term))) alist)))) + (otherwise (mv nil alist)))) + ((symbolp (cadr term)) + (cond + ((eq func-symb 'intern-in-package-of-symbol) + (let ((pkg (symbol-package-name (cadr term))) + (name (symbol-name (cadr term)))) + (mv-let (ans alist1) + (unify-1way1 (fargn pat 1) (kwote name) alist) + (if ans + (if (and (nvariablep (fargn pat 2)) + (fquotep (fargn pat 2))) + (if (not (symbolp (cadr (fargn pat 2)))) + (mv (if (equal term *nil*) ans nil) alist) + (if (equal pkg (symbol-package-name (cadr (fargn pat 2)))) + (mv ans alist1) + (mv nil alist))) + (mv-let (ans alist2) + (unify-1way1 (fargn pat 2) term alist1) + (if ans (mv ans alist2) (mv nil alist)))) + (mv nil alist))))) + (t (mv nil alist)))) + ((stringp (cadr term)) + (cond + ((and (eq func-symb 'coerce) (equal (fargn pat 2) ''string)) + (unify-1way1 (fargn pat 1) (kwote (coerce (cadr term) 'list)) alist)) + (t (mv nil alist)))) + ((consp (cadr term)) + (cond + ((eq func-symb 'cons) + (mv-let (ans alist1) + (unify-1way1 (fargn pat 1) (kwote (car (cadr term))) alist) + (if ans + (mv-let (ans alist2) + (unify-1way1 (fargn pat 2) (kwote (cdr (cadr term))) alist1) + (if ans (mv ans alist2) (mv nil alist))) + (mv nil alist)))) + (t (mv nil alist)))) + (t (mv nil alist))))) + (t + (let ((pat-fn (func-symb pat)) + (term-fn (func-symb term))) + (cond + ((or (not (eq pat-fn term-fn)) (eq pat-fn 'lambda)) + (mv nil alist)) + ((eq pat-fn 'equal) + (unify-1way1-equal (fargn pat 1) (fargn pat 2) + (fargn term 1) (fargn term 2) + alist)) + (t (mv-let (ans alist1) + (unify-1way1-lst (fargs pat) (fargs term) alist) + (if ans (mv ans alist1) (mv nil alist))))))))) + +(defun unify-1way1-lst (pl tl alist) + (if (endp pl) (mv t alist) + (mv-let (ans alist) + (unify-1way1 (car pl) (car tl) alist) + (if (not ans) (mv nil alist) + (unify-1way1-lst (cdr pl) (cdr tl) alist))))) + +(defun unify-1way1-equal1 (pat1 pat2 term1 term2 alist) + (mv-let (ans alist1) + (unify-1way1 pat1 term1 alist) + (if (not ans) (mv nil alist) + (mv-let (ans alist2) + (unify-1way1 pat2 term2 alist1) + (if ans (mv ans alist2) (mv nil alist)))))) + +(defun unify-1way1-equal (pat1 pat2 term1 term2 alist) + (mv-let (ans alist) + (unify-1way1-equal1 pat1 pat2 term1 term2 alist) + (if ans (mv ans alist) + (unify-1way1-equal1 pat2 pat1 term1 term2 alist)))) +) + +(defun unify-1way (pat term) (unify-1way1 pat term nil)) + +(defun ctx-lhs (trm) + (if (and (consp trm) (member-eq (first trm) '(equal iff))) (second trm) trm)) + +(defabbrev already-reduced (op op! go) + (or (eq op! 'quote) + (eq op! 'hide) + (and (eq op op!) (not go)))) + +(mutual-recursion +(defun prune-trm1 (trm) + (if (atom trm) trm + (let* ((op (first trm)) + (op! (if (atom op) op (first op)))) + (cond ((eq op op!) trm) + ((eq op! 'quote) (cons 'quote (rest trm))) + (t (cons op! (prune-args (rest trm)))))))) + +(defun prune-args (args) + (if (endp args) () + (cons (prune-trm1 (first args)) + (prune-args (rest args))))) +) + +(defabbrev prune-trm (op op! trm) + (cond ((eq op op!) trm) + ((eq op! 'hide) (prune-trm1 trm)) + (t (cons op! (rest trm))))) + +(mutual-recursion +(defun rewrt-hyp (hyp alst dp ctx st) + (if (not (all-vars-bound hyp alst)) :fail + (let ((rew (rewrt-trm (subst-term-ctx hyp alst ctx) + nil (1- dp) ctx t (in-hyps st)))) + (if (and (consp hyp) (eq (first hyp) 'synp)) + (cond + ((not (quotep rew)) + (er hard 'rewrt-hyp "illegal synp rewrite")) + ((eq (second rew) t) alst) + ((consp (second rew)) (merge-alsts rew alst)) + (t :fail)) + (if (equal rew ''t) alst :fail))))) + +(defun rewrt-hyps (hyps alst dp ctx st) + (if (endp hyps) alst + (let ((alst (rewrt-hyp (first hyps) alst dp ctx st))) + (if (eq alst :fail) alst + (rewrt-hyps (rest hyps) alst dp ctx st))))) + +(defun rewrt-rule (r recp ens trm dp ctx iff st) + (let ((subc (access rewrite-rule r :subclass)) + (lhs (access rewrite-rule r :lhs)) + (rhs (access rewrite-rule r :rhs)) + (hyps (access rewrite-rule r :hyps)) + (equiv (access rewrite-rule r :equiv)) + (hinfo (access rewrite-rule r :heuristic-info)) + (nume (access rewrite-rule r :nume))) + (and (not (and recp (eq subc 'definition))) + (member-eq subc '(definition abbreviation backchain)) + (enabled-numep nume ens) + (consp lhs) + (implies (eq subc 'backchain) (null hinfo)) + (or (eq equiv 'equal) (and iff (eq equiv 'iff))) + (consp trm) + (implies (eq (car trm) 'if*) (not (eq subc 'definition))) + (mv-let (mtch alst) (unify-1way lhs trm) + (and mtch + (let ((alst (if (st-phase st) (if hyps :fail alst) + (rewrt-hyps hyps alst dp ctx st)))) + (and (not (eq alst :fail)) + (subst-term rhs alst)))))))) + +(defun rewrt-rules (lemmas recp ens trm dp ctx iff st) + (and (not (endp lemmas)) + (or (rewrt-rule (first lemmas) recp ens trm dp ctx iff st) + (rewrt-rules (rest lemmas) recp ens trm dp ctx iff st)))) + +(defun rewrt-step (trm dp ctx iff st) + (let* ((wrld (st-wrld st)) + (ens (st-ens st)) + (op (first trm)) + (args (rest trm)) + (op* (if (eq op 'if) 'if* op)) + (op-ok (not (eq op 't+))) + (lemmas (and op-ok (gprop op* 'lemmas))) + (recp (and op-ok (gprop op* 'recursivep))) + (trm* (if (eq op 'if) (cons 'if* args) trm))) + (or (rewrt-built-in op args) + (rewrt-rules lemmas recp ens trm* dp ctx iff st) + (and op-ok (quoted-args args) + (or (eq (gprop op 'symbol-class) :program) ;; could only occur in synp + (let ((nume (find-nume (gprop op 'runic-mapping-pairs) + (list :executable-counterpart op)))) + (and nume (enabled-numep nume ens)))) + (mv-let (erp val) + (ev-fncall-w op (fncall-args args) wrld nil nil t nil nil) + (and (not erp) (list 'quote val)))) + trm))) + +(defun redux-ctx (lst ctx go dp st) + (cond + ((eq ctx :fail) :fail) + ((eq lst :fail) :fail) + ((endp lst) ctx) + (t + (let* ((trm (rewrt-trm (first lst) go dp ctx t st)) + (ctx+ (if (quotep trm) (if (second trm) ctx :fail) (cons trm ctx)))) + (redux-ctx (rest lst) ctx+ go dp st))))) + +(defun rewrt-ctx (ctx go dp st) + (let ((ctx+ (redux-ctx (redux-ctx ctx () go dp st) () go dp st))) + (if (or (eq ctx+ :fail) (equal ctx ctx+)) ctx (rewrt-ctx ctx+ go (1- dp) st)))) + +(defun extend-ctx (trm ctx go dp st) + (cond + ((quotep trm) + (if (second trm) () :fail)) + ((not (st-rew-ctx st)) + (cons trm ctx)) + ((subterm-ctx (ctx-lhs trm) ctx) + (rewrt-ctx (cons trm ctx) go dp st)) + (t (cons trm ctx)))) + +(defun rewrt-if-args (args go dp ctx iff st) + (let* ((tst (rewrt-trm (first args) go dp ctx t st)) + (tbr (second args)) + (fbr (third args)) + (t-ctx (extend-ctx tst ctx go dp st))) + (cond + ((eq t-ctx :fail) + (list ''nil tbr (rewrt-trm fbr go dp ctx iff st))) + ((endp t-ctx) + (list ''t (rewrt-trm tbr go dp ctx iff st) fbr)) + (t + (let ((f-ctx (extend-ctx (list 'equal tst ''nil) ctx go dp st))) + (cond + ((eq f-ctx :fail) + (list ''t (rewrt-trm tbr go dp ctx iff st) fbr)) + ((endp f-ctx) + (list ''nil tbr (rewrt-trm fbr go dp ctx iff st))) + (t + (list tst + (rewrt-trm tbr t dp t-ctx iff st) + (rewrt-trm fbr t dp f-ctx iff st))))))))) + +(defun rewrt-args* (args go dp ctx st) + (if (endp args) () + (cons (rewrt-trm (first args) go dp ctx nil st) + (rewrt-args* (rest args) go dp ctx st)))) + +(defun rewrt-args (args op go dp ctx iff st) + (if (eq op 'if) + (rewrt-if-args args go dp ctx iff st) + (rewrt-args* args go dp ctx st))) + +(defun rewrt-trm (trm go dp ctx iff st) + (if (zp dp) (list 'hide trm) + (let ((mtch (match-in-ctx trm ctx iff))) + (cond + (mtch (rewrt-trm mtch go (1- dp) ctx iff st)) + ((atom trm) trm) + (t + (let* ((op (first trm)) + (op! (if (atom op) op (car op)))) + (if (already-reduced op op! go) (prune-trm op op! trm) + (let ((args (rewrt-args (rest trm) op! go dp ctx iff st))) + (if (eq op! 'lambda) + (let ((trm+ (subst-term (third op) (bind-args (second op) args)))) + (rewrt-trm trm+ go dp ctx iff st)) + (let ((trm+ (rewrt-step (cons op! args) (1- dp) ctx iff st))) + (rewrt-trm trm+ nil (1- dp) ctx iff st))))))))))) +) + +(defconst *rewrt-trm-depth* 100) + +(defun rewrt-term (trm ctx iff rew-ctx state) + (declare (xargs :stobjs state)) + (let ((st (make-init-st (w state) (ens state) rew-ctx *rewrt-trm-depth*))) + (rewrt-trm trm t (st-depth st) ctx iff st))) + +(defabbrev rewrt-pure (trm) (rewrt-term trm () nil t state)) +(defabbrev rewrt-rep (trm rew-ctx) (rewrt-term trm () t rew-ctx state)) +(defabbrev rewrt-in-ctx (trm ctx) (rewrt-term trm ctx t nil state)) + +(mutual-recursion +(defun term-contains-force (trm) + (and (consp trm) + (or (eq (first trm) 'force) + (args-contain-force (rest trm))))) + +(defun args-contain-force (args) + (and (not (endp args)) + (or (term-contains-force (first args)) + (args-contain-force (rest args))))) +) + +(mutual-recursion +(defun strip-forces-term (trm hyps) + (if (atom trm) (mv trm hyps) + (case (first trm) + ((quote hide) (mv trm hyps)) + (force (mv ''t (cons trm hyps))) + (t (mv-let (args hyps) + (strip-forces-args (rest trm) hyps) + (mv (cons (first trm) args) hyps)))))) + +(defun strip-forces-args (args hyps) + (if (endp args) (mv () hyps) + (mv-let (fst hyps) + (strip-forces-term (first args) hyps) + (mv-let (rst hyps) + (strip-forces-args (rest args) hyps) + (mv (cons fst rst) hyps))))) +) + +(defun rewrt-rep-loop* (term hyps ic$ state) + (declare (xargs :stobjs (ic$ state))) + (let ((nterm (rewrt-rep term (reduce-contexts ic$)))) + (if (not (term-contains-force nterm)) (mv nterm hyps) + (mv-let (nterm nhyps) (strip-forces-term nterm ()) + (rewrt-rep-loop* nterm (append nhyps hyps) ic$ state))))) + +(defabbrev rewrt-rep-loop (term) + (rewrt-rep-loop* term () ic$ state)) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +#| <SECTION> 4. extended rewriting and propagating rep-step |# +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(defun rewrite-rep-step (rep ic$ state) + (declare (xargs :stobjs (ic$ state))) + (mv-let (term hyps) (rewrt-rep-loop `((lambda (n) ,rep) (t+ n))) + (detail "assuming rep hyps: ~p0 ~%" hyps (mv term hyps ic$ state)))) + +(mutual-recursion +(defun is-rep-term (term) + (if (atom term) (eq term 'n) + (let ((op (first term))) + (or (eq op 'quote) + (and (not (eq op 't+)) + (not (eq op 'hide)) + (are-rep-args (rest term))))))) + +(defun are-rep-args (args) + (or (endp args) + (and (is-rep-term (first args)) + (are-rep-args (rest args))))) +) + +(defmacro union-terms (x &rest y) + (if (endp y) x `(union-equal ,x (union-terms ,(car y) ,@(cdr y))))) + +(defun extract-rep-subterms (term) + (cond ((atom term) ()) + ((eq (first term) 'quote) ()) + ((eq (first term) 'if) + (union-terms (extract-rep-subterms (second term)) + (extract-rep-subterms (third term)) + (extract-rep-subterms (fourth term)))) + ((is-rep-term term) (list term)) + (t ()))) + +(defun extract-non-rep-subterms (term) + (cond ((atom term) (list term)) + ((eq (first term) 'quote) ()) + ((eq (first term) 'if) + (union-terms (extract-non-rep-subterms (second term)) + (extract-non-rep-subterms (third term)) + (extract-non-rep-subterms (fourth term)))) + ((is-rep-term term) ()) + (t (list term)))) + +(defun compute-rep-prime (reps step-alist ic$ state) + (declare (xargs :stobjs (ic$ state))) + (if (endp reps) + (mv nil nil step-alist nil ic$ state) + (seq + (current-rep (first reps)) + ((term fst-hyps ic$ state) + (rewrite-rep-step current-rep ic$ state)) + ((rst-reps rst-hyps step-alist rst-ins ic$ state) + (compute-rep-prime (rest reps) step-alist ic$ state)) + (fst-reps (extract-rep-subterms term)) + (reps (union-equal fst-reps rst-reps)) + (hyps (union-equal fst-hyps rst-hyps)) + (fst-ins (extract-non-rep-subterms term)) + (ins (union-equal fst-ins rst-ins)) + (step-alist (acons current-rep term step-alist)) + (mv reps hyps step-alist ins ic$ state)))) + +(defun compute-step-prime (reps step-alist ic$ state) + (declare (xargs :stobjs (ic$ state))) + (if (endp reps) + (mv (list 'bnil) ic$ state) + (seq + ((rest-step ic$ state) + (compute-step-prime (rest reps) step-alist ic$ state)) + (first-step + (cdr (assoc-equal (first reps) step-alist))) + (mv (list 'bcons first-step rest-step) ic$ state)))) + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +#| <SECTION> 5. invariant checker implementation |# +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(defun clear-st-hashtbl (ndx ic$) + (declare (xargs :stobjs ic$)) + (if (zp ndx) ic$ + (let* ((ndx (1- ndx)) + (ic$ (update-st-hashtbli ndx nil ic$))) + (clear-st-hashtbl ndx ic$)))) + +(defun clear-seen-states (ic$) + (declare (xargs :stobjs ic$)) + (clear-st-hashtbl (st-hashtbl-length ic$) ic$)) + +(defconst *hex-digits* + '("0" "1" "2" "3" "4" "5" "6" "7" "8" "9" "A" "B" "C" "D" "E" "F")) + +(defun st-str (n st) + (if (zp n) "" + (string-append (st-str (- n 1) (floor st 16)) + (nth (mod st 16) *hex-digits*)))) + +(defmacro the-max-fix-st () (expt 2 28)) + +(defmacro with-st-hash (st rslt) + `(let ((hash (let ((st ,st) + (len (the-fixnum (st-hashtbl-length ic$)))) + (declare (type (signed-byte 29) len)) + (the-fixnum (if (< st (the-max-fix-st)) + (the-fixnum (mod (the-fixnum st) len)) + (the-fixnum (mod st len))))))) + (declare (type (signed-byte 29) hash)) + ,rslt)) + +(defun legal-bnth (term) + (and (consp term) + (eq (first term) 'bnth) + (integerp (second term)) + (>= (second term) 0) + (member (third term) '(s i)))) + +(defun legal-singl (term) + (or (legal-bnth term) + (and (consp term) + (case (first term) + (quote t) + (if (and (legal-bnth (second term)) + (legal-singl (third term)) + (legal-singl (fourth term)))))))) + +(defun legal-step (term) + (and (consp term) + (case (first term) + (bcons (and (legal-singl (second term)) + (legal-step (third term)))) + (bnil t)))) + +(defmacro state-report-interval () 1000) + +(defun check-and-add-seen-state (st ic$) + (declare (xargs :stobjs ic$)) + (with-st-hash + st + (let* ((entry (st-hashtbli hash ic$)) + (seen (cond ((eq entry nil) nil) + ((eq entry t) t) + ((consp entry) (member st entry)) + (t (eql st entry))))) + (if seen + (mv t ic$) + (let ((num-states (num-states ic$))) + (declare (type (signed-byte 29) num-states)) + (prog2$ + (and (eql (modf num-states (state-report-interval)) 0) + (> num-states 0) + (cw "num. abstract states visited: ~x0 ~%" num-states)) + (let* ((ic$ (update-num-states (1+f num-states) ic$)) + (ic$ (update-search-bound (1-f (search-bound ic$)) ic$)) + (entry (cond ((eq entry nil) st) + ((fast-search ic$) t) + ((consp entry) (cons st entry)) + (t (list st entry)))) + (ic$ (update-st-hashtbli hash entry ic$))) + (mv nil ic$)))))))) + +(defun mk-not-term (x) + (cond ((atom x) (list 'not x)) + ((not (eq (first x) 'equal)) (list 'not x)) + ((equal (second x) ''nil) (third x)) + ((equal (third x) ''nil) (second x)) + (t (list 'not x)))) + +(defun map-rep-vector (mask reps st) + (if (endp mask) () + (let ((n (first mask))) + (cons (if (bnth n st) (nth n reps) (mk-not-term (nth n reps))) + (map-rep-vector (rest mask) reps st))))) + +(defun mk-and-term (lst) + (cond ((endp lst) t) + ((endp (rest lst)) (first lst)) + (t (cons 'and lst)))) + +(defun map-counter-example (reps inputs path mask) + (if (endp path) () + (cons (list (mk-and-term (map-rep-vector (caar mask) reps (caar path))) + (mk-and-term (map-rep-vector (cdar mask) inputs (cdar path)))) + (map-counter-example reps inputs (rest path) (rest mask))))) + +(defun get-mask-terms (step tgt n) + (if (atom step) + (er hard 'get-mask-terms "illegal step") + (case (first step) + (bnil ()) + (bcons + (if (member n tgt) + (cons (second step) + (get-mask-terms (third step) tgt (1+ n))) + (get-mask-terms (third step) tgt (1+ n)))) + (t (er hard 'get-mask-terms "illegal step"))))) + +(defun compute-ev (trm st in) + (if (atom trm) + (er hard 'compute-ev "illegal term") + (case (first trm) + (quote (second trm)) + (bnth (bnth (second trm) + (if (eq (third trm) 's) st in))) + (if (if (compute-ev (second trm) st in) + (compute-ev (third trm) st in) + (compute-ev (fourth trm) st in))) + (t (er hard 'compute-ev "illegal trm"))))) + +(defun compute-mask (term st in) + (if (atom term) + (er hard 'compute-mask "illegal term") + (case (first term) + (quote ()) + (bnth (list term)) + (if (let* ((tst (second term)) + (tbr (third term)) + (fbr (fourth term)) + (tst-v (compute-ev tst st in)) + (br (if tst-v tbr fbr)) + (rst (compute-mask br st in))) + (if (or (quotep tst) + (iff (compute-ev tbr st in) + (compute-ev fbr st in))) + rst + (cons tst rst)))) + (t (er hard 'compute-mask "illegal term"))))) + +(defun add-mask-bits (mask var rslt) + (if (endp mask) rslt + (add-mask-bits (rest mask) var + (if (eq var (third (first mask))) + (add-to-set-eql (second (first mask)) rslt) + rslt)))) + +(defun compute-masks (trms st in smsk imsk) + (if (endp trms) (mv smsk imsk) + (let ((mask (compute-mask (first trms) st in))) + (compute-masks (rest trms) st in + (add-mask-bits mask 's smsk) + (add-mask-bits mask 'i imsk))))) + +(defun compute-step-masks (step tgt st in) + (compute-masks (get-mask-terms step tgt 0) st in () ())) + +(defun compute-example-mask (path step tgt) + (if (endp path) () + (seq + ((st-mask in-mask) + (compute-step-masks step tgt (caar path) (cdar path))) + (acons st-mask in-mask + (compute-example-mask (cdr path) step st-mask))))) + +(defun transform-rslt-path (path) + (if (endp (cdr path)) () + (seq + (in (caar path)) + (st (cdadr path)) + (acons st in (transform-rslt-path (cdr path)))))) + +(defun load-input-vec (input-set ndx ic$) + (declare (xargs :stobjs ic$)) + (if (endp input-set) ic$ + (let ((ic$ (update-input-veci ndx (first input-set) ic$))) + (load-input-vec (rest input-set) (1+ ndx) ic$)))) + +(defun ivarp (x) + (and (consp x) + (eq (first x) 'if) + (natp (second x)) + (eq (third x) t) + (eq (fourth x) nil))) + +(defun input-set-template (term) + (if (atom term) + (er hard 'input-set-template "illegal atom term") + (case (first term) + (quote (if (second term) t nil)) + (bcons (list 'or + (input-set-template (second term)) + (input-set-template (third term)))) + (bnil :x) + (bnth (let ((ndx (second term)) + (var (third term))) + (cond ((not (and (natp ndx) + (member var '(s i)))) + (er hard 'input-set-template "illegal bnth term")) + ((eq var 'i) (list 'if ndx t nil)) + (t :x)))) + (if (let* ((tst (input-set-template (second term))) + (tbr (input-set-template (third term))) + (fbr (input-set-template (fourth term))) + (tst (if (ivarp tst) (second tst) tst))) + (cond ((natp tst) (list 'if tst tbr fbr)) + ((eq tst t) tbr) + ((eq tst nil) fbr) + ((eq tst :x) (list 'or tbr fbr)) + (t (er hard 'input-set-template "illegal if term"))))) + (t (er hard 'input-set-template "illegal op term"))))) + +(defun fully-defined (tmpl) + (cond ((eq tmpl :x) nil) + ((atom tmpl) t) + ((eq (first tmpl) 'or) + (and (fully-defined (second tmpl)) + (fully-defined (third tmpl)))) + (t + (and (fully-defined (third tmpl)) + (fully-defined (fourth tmpl)))))) + +(defun reduce-template (tmpl var valu) + (cond ((eql tmpl var) valu) + ((atom tmpl) tmpl) + ((eq (first tmpl) 'or) + (let ((a (reduce-template (second tmpl) var valu)) + (b (reduce-template (third tmpl) var valu))) + (cond ((equal a b) a) + ((and (atom a) (atom b)) :x) + (t (list 'or a b))))) + (t + (let ((tst (reduce-template (second tmpl) var valu))) + (cond ((eq tst t) + (reduce-template (third tmpl) var valu)) + ((eq tst nil) + (reduce-template (fourth tmpl) var valu)) + (t + (let ((tbr (reduce-template (third tmpl) var valu)) + (fbr (reduce-template (fourth tmpl) var valu))) + (cond ((and (equal tbr fbr) (fully-defined tbr)) tbr) + ((not (eq tst :x)) (list 'if tst tbr fbr)) + ((and (atom tbr) (atom fbr)) :x) + (t (list 'or tbr fbr)))))))))) + +(defun first-tmpl-var (tmpl) + (cond ((natp tmpl) tmpl) + ((atom tmpl) nil) + (t + (or (first-tmpl-var (second tmpl)) + (first-tmpl-var (third tmpl)) + (and (eq (first tmpl) 'if) + (first-tmpl-var (fourth tmpl))))))) + +(defabbrev set-bnth (i v x) + (if v (logior x (ash 1 i)) (logand x (lognot (ash 1 i))))) + +(defun add-input-set (tmpl in rslt) + (if (atom tmpl) (cons in rslt) + (let ((var (first-tmpl-var tmpl))) + (add-input-set (reduce-template tmpl var t) + (set-bnth var t in) + (add-input-set (reduce-template tmpl var nil) + (set-bnth var nil in) + rslt))))) + +(defun compute-input-set (step-term) + (add-input-set (input-set-template step-term) 0 ())) + +(defun construct-input-vec (step-term inputs state ic$) + (declare (xargs :stobjs (state ic$))) + (seq + (input-set (compute-input-set step-term)) + (num-inputs (length input-set)) + (ic$ (update-num-inputs num-inputs ic$)) + (ic$ (resize-input-vec num-inputs ic$)) + (ic$ (load-input-vec input-set 0 ic$)) + (report "number of input bits: ~p0 number of inputs: ~p1 ~%" + (length inputs) num-inputs + (detail "inputs: ~p0 ~%" inputs + (mv ic$ state))))) + +(defun format-counter-example1 (path n) + (if (endp path) () + (cons (list :step n + :state (first (first path)) + :input (second (first path))) + (format-counter-example1 (rest path) (1+ n))))) + +(defun format-counter-example (path) + (format-counter-example1 (reverse path) 1)) + +(defconst *invariant-checker-functions-and-compile* (quote ( +(defun visit-next-states (st in acc ic$) + (declare (xargs :stobjs ic$ + :mode :program) + (type (signed-byte 29) in)) + (if (fzp in) + (mv acc ic$) + (let ((in (1-f in))) + (declare (type (signed-byte 29) in)) + (seq + (next-in (input-veci in ic$)) + (next-st (step-prime st next-in)) + ((seen ic$) (check-and-add-seen-state next-st ic$)) + (acc (if seen acc (cons (cons next-in next-st) acc))) + (visit-next-states st in acc ic$))))) + +(defun bfs (visiting alst next-wave path ic$) + (declare (xargs :stobjs ic$ + :mode :program)) + (cond + ((endp visiting) + (cond + ((not (endp alst)) + (bfs (cdar alst) (cdr alst) next-wave (caar alst) ic$)) + ((endp next-wave) + (mv :passed ic$)) + (t + (bfs () next-wave () path ic$)))) + ((fzp (search-bound ic$)) + (mv :bound-fail ic$)) + (t + (seq + (pair (car visiting)) + (st (cdr pair)) + (path+ (cons pair path)) + (if (not (bnth (inv-bit ic$) st)) + (mv path+ ic$) + (seq + ((next ic$) (visit-next-states st (num-inputs ic$) () ic$)) + (next-wave (cons (cons path+ next) next-wave)) + (bfs (cdr visiting) alst next-wave path ic$))))))) + +(defun invariant-checker (reps inputs inv-term step-term ic$ state) + (declare (xargs :stobjs (ic$ state) + :mode :program)) + (if (not (legal-step step-term)) + (detail "illegal step term: ~p0 ~%" step-term + (seq + (ic$ (update-inv-check-result :bad-step ic$)) + (mv ic$ state))) + (seq + (term (rewrt-pure '(rep-prime (t0)))) + (if (not (quotep term)) + (detail "init term rewrote to: ~p0 ~%" term + (seq + (ic$ (update-inv-check-result :bad-init ic$)) + (mv ic$ state))) + (seq + (init-abs (second term)) + ((ic$ state) + (construct-input-vec step-term inputs state ic$)) + (ic$ (clear-seen-states ic$)) + (ic$ (update-inv-bit (position-equal inv-term reps) ic$)) + (ic$ (update-search-bound (check-bound ic$) ic$)) + (ic$ (update-num-states 0 ic$)) + (ic$ (update-num-rep-bits (length reps) ic$)) + ((rslt ic$) + (if (inv-bit ic$) + (bfs (list (cons 0 init-abs)) () () () ic$) + (die :model-check-inv + "unexpectedly did not find inv-term in list of reps" + (mv nil ic$)))) + (rslt (if (atom rslt) rslt + (seq + (rslt (transform-rslt-path rslt)) + (tgt (list (inv-bit ic$))) + (mask (compute-example-mask rslt step-term tgt)) + (rslt (map-counter-example reps inputs rslt mask)) + rslt))) + (ic$ (update-inv-check-result rslt ic$)) + (mv ic$ state)))))) + +(comp (quote (step-prime visit-next-states bfs invariant-checker))) +))) + +(defun bogus-function-denoting-invariant-checker-side-effect (ic$) + (declare (xargs :stobjs ic$)) + ic$) + +(defun check-invariant (step-body rep-body reps inputs inv ic$ state) + (declare (xargs :stobjs (ic$ state))) + (mv-let (erp val state) + (ld (append (list (list 'defun 'step-prime (list 's 'i) + '(declare (xargs :mode :program)) + step-body) + (list 'defun 'rep-prime (list 'n) + '(declare (xargs :mode :logic)) + rep-body)) + (and (disable-exec ic$) + (list (list 'in-theory (list 'disable (list 'rep-prime))))) + *invariant-checker-functions-and-compile* + (list (list 'invariant-checker + (list 'quote reps) + (list 'quote inputs) + (list 'quote inv) + (list 'quote step-body) + 'ic$ 'state) + (list 'ubt! (list 'quote 'step-prime))))) + (let ((ic$ (bogus-function-denoting-invariant-checker-side-effect ic$))) + (if erp (die :check-invariant + "Unexpected error ~p0" val + (mv nil ic$ state)) + (mv (inv-check-result ic$) ic$ state))))) + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +#| <SECTION> 6. top-level algorithm and interface |# +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(defun build-rep-body (reps) + (if (endp reps) + (list 'bnil) + (list 'bcons (first reps) + (build-rep-body (rest reps))))) + +(defun snoc (e x) + (if (endp x) (list e) + (cons (first x) (snoc e (rest x))))) + +(defun match-rep-or-input (term reps inputs) + (let ((pos (position-equal term reps))) + (if pos + (mv (list 'bnth pos 's) inputs) + (let ((pos (position-equal term inputs))) + (if pos + (mv (list 'bnth pos 'i) inputs) + (mv (list 'bnth (length inputs) 'i) + (snoc term inputs))))))) + +(defun final-step-redux (term) + (cond ((or (atom term) + (not (eq (car term) 'if))) + term) + ((quotep (second term)) + (if (second (second term)) + (third term) + (fourth term))) + ((equal (third term) (fourth term)) + (third term)) + ((and (equal (third term) ''t) + (equal (fourth term) ''nil)) + (second term)) + ((and (equal (third term) ''t) + (term-order (fourth term) (second term))) + (list 'if (fourth term) ''t (second term))) + ((and (equal (fourth term) ''nil) + (term-order (third term) (second term))) + (list 'if (third term) (second term) ''nil)) + (t term))) + +(defconst *step-prime-ops* + '(bcons bnil if)) + +(mutual-recursion +(defun build-step-body (term reps inputs ic$) + (declare (xargs :stobjs ic$)) + (cond ((atom term) + (match-rep-or-input term reps inputs)) + ((eq (car term) 'quote) + (mv (if (cadr term) ''t ''nil) inputs)) + ((member (car term) *step-prime-ops*) + (mv-let (args inputs) + (build-step-args (rest term) reps inputs ic$) + (mv (final-step-redux (cons (car term) args)) inputs))) + (t + (match-rep-or-input term reps inputs)))) + +(defun build-step-args (args reps inputs ic$) + (declare (xargs :stobjs ic$)) + (if (endp args) + (mv () inputs) + (mv-let (fst inputs) + (build-step-body (first args) reps inputs ic$) + (mv-let (rst inputs) + (build-step-args (rest args) reps inputs ic$) + (mv (cons fst rst) inputs))))) +) + +(defun compute-reps (bound new reps hyps step-alist ic$ state) + (declare (xargs :stobjs (ic$ state))) + (cond + ((endp new) + (report "converged on reps! ~%" + (mv t reps hyps step-alist ic$ state))) + ((zp bound) + (report "exceeded refine bound! ~%" + (mv nil reps hyps step-alist ic$ state))) + (t + (seq + ((new-new new-hyps step-alist new-ins ic$ state) + (compute-rep-prime new step-alist ic$ state)) + (bound (- bound (len new))) + (reps (union-equal new reps)) + (new (set-difference-equal new-new reps)) + (hyps (union-equal new-hyps hyps)) + (detail "new reps: ~p0 ~%" new + (detail "new ins: ~p0 ~%" new-ins + (compute-reps bound new reps hyps step-alist ic$ state))))))) + +(defun get-prods (term) + (cond ((eq term t) ()) + ((and (consp term) (eq (first term) 'and)) + (rest term)) + (t (list term)))) + +(defun drop-nots (terms) + (cond ((endp terms) ()) + ((and (consp (first terms)) + (eq (first (first terms)) 'not)) + (cons (second (first terms)) + (drop-nots (rest terms)))) + (t + (cons (first terms) + (drop-nots (rest terms)))))) + +(defun new-reps-in (prods) + (cond ((endp prods) ()) + ((is-rep-term (first prods)) (list (first prods))) + (t (new-reps-in (rest prods))))) + +(defun find-new-reps (path) + (and (consp path) + (or (new-reps-in (drop-nots (get-prods (second (first path))))) + (find-new-reps (rest path))))) + +(defun check-abstraction (reps step-alist inv ic$ state) + (declare (xargs :stobjs (ic$ state))) + (detail "check-reps: ~p0 ~%" reps + (seq + ((step-term ic$ state) + (compute-step-prime reps step-alist ic$ state)) + ((step-body inputs) + (build-step-body step-term reps () ic$)) + (rep-body (build-rep-body reps)) + (ic$ (clear-ic$-for-inv-check ic$)) + ((result ic$ state) + (detail "step-term: ~p0 ~%" step-term + (check-invariant step-body rep-body reps inputs inv ic$ state))) + (detail "number of abstract states visited: ~p0~%" (num-states ic$) + (cond + ((eq result :passed) + (mv t () ic$ state)) + ((eq result :bound-fail) + (report "exceeded bound on number of states!~%" + (mv nil () ic$ state))) + ((eq result :bad-init) + (report "could not rewrite (rep-prime (t0)) to constant!~%" + (mv nil () ic$ state))) + (t + (report "failed-inv-check!~%" + (detail "failed-path:~p0~%" (format-counter-example result) + (mv nil (find-new-reps result) ic$ state))))))))) + +(defun prove-inv-single (bound inv-term new-reps curr-reps curr-hyps curr-step ic$ state) + (declare (xargs :stobjs (ic$ state))) + (seq + ((ok reps hyps step-alist ic$ state) + (compute-reps (refine-bound ic$) new-reps curr-reps + curr-hyps curr-step ic$ state)) + (if (or ok (always-check ic$)) + (seq + ((ok new-reps ic$ state) + (check-abstraction reps step-alist inv-term ic$ state)) + (cond + (ok (mv t hyps ic$ state)) + ((or (endp new-reps) (zp bound)) (mv nil hyps ic$ state)) + (t (prove-inv-single (1- bound) inv-term new-reps + reps hyps step-alist ic$ state)))) + (mv nil hyps ic$ state)))) + +(defun prove-inv-loop (to-prove proven proofs-bound ic$ state) + (declare (xargs :stobjs (ic$ state))) + (cond + ((endp to-prove) + (mv t ic$ state)) + ((member-equal (first to-prove) proven) + (prove-inv-loop (rest to-prove) proven proofs-bound ic$ state)) + ((zp proofs-bound) + (report "exceeded bound on number of proofs!~%" + (mv nil ic$ state))) + (t + (seq + ((ok hyps ic$ state) + (prove-inv-single (jump-bound ic$) (first to-prove) (list (first to-prove)) + () () () ic$ state)) + (if (not ok) + (mv nil ic$ state) + (prove-inv-loop (append hyps (rest to-prove)) + (cons (first to-prove) proven) + (1- proofs-bound) ic$ state)))))) + +(defun definv-fn (inv-name + inv-form + jump-bound + check-bound + refine-bound + proofs-bound + inputs-bound + fast-search + detail-file + always-check + disable-exec + reduce-contexts + expected-result + ic$ + state) + (declare (xargs :stobjs (ic$ state))) + (seq + ((erp inv-term bindings state) + (translate1 inv-form :stobjs-out '((:stobjs-out . :stobjs-out)) + t 'top-level (w state) state)) + (state + (if (or erp + +; Change by Matt K., 10/17/2013: When testing a tentative fix for a soundness +; bug, I found a guard violation below because EQ was being called instead of +; EQUAL; so I changed EQ to EQUAL. (Implementation details: That bug involved +; doing extra guard-checking for certain :program mode functions in order to +; avoid violating stobj recognizers. In this case definv-fn was marked as such +; a function because it depended on ld-fn, which had been marked as such a +; function because it took state. The ultimate fix didn't give this special +; treatment for state, so the change from EQ to EQUAL below is no longer +; necessary. But it seems that since the call of EQ was ill-guarded, it is +; still good to fix.) + + (not (equal bindings bindings))) + (die :illegal-term + "Error in macro-expansion: ~p0" inv-form + state) + state)) + ((ic$ state) + (initialize-ic$ jump-bound + check-bound + refine-bound + inputs-bound + fast-search + detail-file + always-check + disable-exec + reduce-contexts + ic$ + state)) + (state + (detail "**************** begin ~s0 **************** ~%" detail-file + state)) + ((ok ic$ state) + (prove-inv-loop (list inv-term) () proofs-bound ic$ state)) + (result (if ok :qed :failed)) + (state + (report "~x0~%" (list result inv-name result) + (detail "**************** end ~s0 **************** ~%~%" detail-file + state))) + ((ic$ state) + (cleanup-ic$ ic$ state)) + (state + (if (implies expected-result (equal result expected-result)) + state + (die :unexpected-result-for-inv-proof + "encountered unexpected result for invariant proof~%" + state))) + (mv state ic$))) + +(defmacro definv (inv-name + inv-term + &key + (file '"invp.rpt") + (jump-bound '1) + (check-bound '4000) + (refine-bound '8) + (proofs-bound '10) + (inputs-bound '1000) + (fast-search 'nil) + (disable-exec 't) + (always-check 'nil) + (reduce-contexts 'nil) + (expected-result 'nil)) + (declare (xargs :guard (and (symbolp inv-name) + (integerp check-bound) + (>= check-bound 0) + (integerp inputs-bound) + (>= inputs-bound 0) + (integerp refine-bound) + (>= refine-bound 0) + (integerp proofs-bound) + (>= proofs-bound 0) + (or (stringp file) (not file)) + (booleanp fast-search) + (booleanp always-check) + (booleanp disable-exec) + (booleanp reduce-contexts) + (member-eq expected-result '(:qed :failed nil))))) + `(definv-fn + (quote ,inv-name) + (quote ,inv-term) + (quote ,jump-bound) + (quote ,check-bound) + (quote ,refine-bound) + (quote ,proofs-bound) + (quote ,inputs-bound) + (quote ,fast-search) + (quote ,file) + (quote ,always-check) + (quote ,disable-exec) + (quote ,reduce-contexts) + (quote ,expected-result) + ic$ + state)) + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +#| <SECTION> 7. various test examples |# +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +;; compile the invariant prover: +(comp t) + +(set-ignore-ok t) +(set-irrelevant-formals-ok t) +(set-match-free-error nil) + +(logic) + +;; Simple Example: A simple pair of integers +;; ----------------------------------------- + +(progn +(defun next (s i) + (cons (if (car i) (if (cdr s) 1 (ifix (cdr i))) (cdr s)) + (if (cdr i) (ifix (car i)) (cdr s)))) + +(defun init () + (cons 1 2)) + +(in-theory (disable natp)) + +;; environment input function +(encapsulate (((i *) => *)) (local (defun i (n) n))) + +(defun x (n) + (declare (xargs :measure (tmsr n))) + (if (tzp n) (init) (next (x (t- n)) (i n)))) + +(in-theory (disable (x))) + +(if-lift-rules + (integerp x) + (natp x) + (equal x y) + (car x) + (cdr x)) + +(defthm x-of-t+ + (implies (not (tzp n)) + (equal (x n) (next (x (t- n)) (i n)))) + :hints (("Goal" :in-theory (disable next)))) + +(defthm x-of-t0 + (equal (x (t0)) (init))) +) + +(definv simple-pass-inv + (integerp (car (x n))) + :file "simp1.rpt" + :expected-result :qed) + +(definv simple-fail-inv + (natp (car (x n))) + :file "simp2.rpt" + :expected-result :failed) + +(u) + +;; Another Simple Example: A mutual exclusion model +;; ------------------------------------------------- + +(include-book "crit") + +(definv crit-inv + (ok n) + :file "crit.rpt" + :expected-result :qed) + +(u) + +;; A slightly more complex example: A MESI cache model +;; ------------------------------------------------- + +(include-book "mesi") + +(definv mesi-inv + (ok n) + :file "mesi.rpt" + :expected-result :qed) + +(u) + +;; go ahead and write to success.txt in order to signal that we have succeeded +;; in proving all of the example invariants: + +(defun mark-successful-run (state) + (declare (xargs :stobjs state + :mode :program)) + (mv-let (channel state) + (open-output-channel "success.txt" :character state) + (let ((state (fms "invariant prover successfully completed proofs!!" () channel state nil))) + (let ((state (close-output-channel channel state))) + state)))) + +(mark-successful-run state) + + + + diff --git a/books/workshops/2004/sumners-ray/support/mesi.lisp b/books/workshops/2004/sumners-ray/support/mesi.lisp new file mode 100644 index 0000000..70583a0 --- /dev/null +++ b/books/workshops/2004/sumners-ray/support/mesi.lisp @@ -0,0 +1,227 @@ +(in-package "ACL2") +(include-book "basis") +(include-book "records") + +#| + +We define a cache-coherence memory-ordering protocol at a pretty high-level of +abstraction. This is loosely based on the MESI protocol. + +The property we want to prove is the following: + +Forall p,q,a,d: if (q completed the last write to address a with data d) and + p reads address a and gets value d. + +Well, it is easier to leave the specific q and d out of the equation and only +introduce p and a as skolem constants. We add appropriate auxiliary variables +to track this. + +|# + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;;;;;;;;;; definitions for example mesi cache system ;;;;;;;;;;;;;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(encapsulate (((proc *) => *) ((op *) => *) + ((addr *) => *) ((data *) => *)) + (local (defun proc (n) n)) (local (defun op (n) n)) + (local (defun addr (n) n)) (local (defun data (n) n))) + +(encapsulate (((c-l *) => *)) (local (defun c-l (a) a))) + +(define-system mesi-cache + (mem (c n) nil + (cond ((/= (c-l (addr n)) c) (mem c n-)) + ((and (= (op n) :flush) + (in (proc n) (excl c n-))) + (cache (proc n) c n-)) + (t (mem c n-)))) + + (cache (p c n) nil + (cond ((/= (c-l (addr n)) c) (cache p c n-)) + ((/= (proc n) p) (cache p c n-)) + ((or (and (= (op n) :fill) (not (excl c n-))) + (and (= (op n) :fille) (not (valid c n-)))) + (mem c n-)) + ((and (= (op n) :store) (in p (excl c n-))) + (s (addr n) (data n) (cache p c n-))) + (t (cache p c n-)))) + + (excl (c n) nil + (cond ((/= (c-l (addr n)) c) (excl c n-)) + ((and (= (op n) :flush) + (implies (excl c n-) + (in (proc n) (excl c n-)))) + (sdrop (proc n) (excl c n-))) + ((and (= (op n) :fille) (not (valid c n-))) + (sadd (proc n) (excl c n-))) + (t (excl c n-)))) + + (valid (c n) nil + (cond ((/= (c-l (addr n)) c) (valid c n-)) + ((and (= (op n) :flush) + (implies (excl c n-) + (in (proc n) (excl c n-)))) + (sdrop (proc n) (valid c n-))) + ((or (and (= (op n) :fill) (not (excl c n-))) + (and (= (op n) :fille) (not (valid c n-)))) + (sadd (proc n) (valid c n-))) + (t (valid c n-))))) + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;;;;;;;;;; definitions for mesi system specification ;;;;;;;;;;;;;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(encapsulate (((p) => *) ((a) => *)) + (local (defun p () t)) (local (defun a () t)) + (defthm a-not-nil (equal (equal (a) nil) nil)) + (defthm p-not-nil (equal (equal (p) nil) nil))) + +(define-system mesi-specification + (a-dat (n) nil + (if (and (equal (addr n) (a)) + (equal (op n) :store) + (in (proc n) (excl (c-l (addr n)) n-))) + (list (data n)) + (a-dat n-))) + + (ok (n) t + (if (and (a-dat n-) + (equal (proc n) (p)) + (equal (addr n) (a)) + (equal (op n) :load) + (in (p) (valid (c-l (addr n)) n-))) + (equal (g (a) (cache (p) (c-l (a)) n-)) + (car (a-dat n-))) + (ok n-)))) + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;;;;;;;;;;; various auxiliary rules and definitions ;;;;;;;;;;;;;;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + + +;; For the (proc n), (addr n), and (op n) inputs, we want to force +;; case-splits using the finite-cases macro from basis.lisp: + +(finite-cases process-id :input (proc n) ((p) (scar (excl (c-l (a)) (t- n))))) +(finite-cases address :input (addr n) ((a))) +(finite-cases operation :input (op n) (:store :fille :fill :flush :load)) + + +;; We do want the following rewrite rule from the records book enabled: + +(in-theory (enable g-of-s-redux)) + + +;; The following function is only used as shorthand in provide a precise +;; case-split in rewrite rules below: + +(defun <<s (e x) (implies x (<< e (scar x)))) + + +;; These could probably be moved into the sets and records books, but it is +;; easy enough to include all of the if-lifting rules in one form: + +(if-lift-rules + (<<s x y) + (car x) + (cons x y) + (g a r) + (s a v r) + (c1 r) + (equal x y) + (sdiff x y) + (isect x y) + (unite x y) + (in e x) + (subset x y) + (scar a) + (s1 a) + (c-l a)) + + +;; The following is an unfortunate rule that we need to add because the +;; rewriter does not handle equality reasoning across predicate +;; evaluations. This might be a worthwhile addition, but it could also be an +;; expensive proposition, so I need to continue working on this. + +(defthm bogus-equality1 + (implies (not (equal (proc! a) (p))) + (equal (equal (scar (excl (c-l (a)) n)) (proc! a)) + (if (equal (scar (excl (c-l (a)) n)) (p)) nil + (hide (equal (scar (excl (c-l (a)) n)) (proc! a)))))) + :hints (("Goal" :expand (hide (equal (scar (excl (c-l (a)) n)) (proc! a)))))) + + +;; The next set of rules are simply reorganized versions of rules from the sets +;; book which we need in order to introduce certain abstractions and/or force +;; certain case splits: + +(defthm c1-of-sdrop-hide + (equal (c1 (sdrop e x)) + (if (in e x) (if (c1 x) nil (hide (c1 (sdrop e x)))) (c1 x))) + :hints (("Goal" :expand (hide (c1 (sdrop e x)))))) + +(defthm scar-of-sdrop-hide + (equal (scar (sdrop e x)) + (if (in e x) (hide (scar (sdrop e x))) (scar x))) + :hints (("Goal" :expand (hide (scar (sdrop e x)))))) + +(defthm scar-of-sadd + (equal (scar (sadd e x)) + (if (<<s e x) e (scar x))) + :hints (("Goal" :cases (x (not x))))) + +(defthm drop-in-test-when-equal-scar + (implies (and s (equal (scar s) e)) + (in e s))) + +(defthm rename-of-wrap-up-s1 + (equal (equal s (s1 a)) + (and (c1 s) (equal (scar s) a)))) + + +;; We will only use the following predicate in syntaxp tests below... + +(defun st-predp (x) + (declare (xargs :mode :program)) + (not (intersectp-eq '(t+ hide) (all-fnnames x)))) + + +;; Ok, the key insight to this invariant proof is to case-split the test of a +;; node in an :excl set by testing if the :excl set is empty, a singleton of +;; the last guy to be added to the :excl set, or abstracted (we don't care +;; because we don't expect this case to ever occur -- or at least not +;; matter). We need the syntaxp test to make sure we only apply this in cases +;; where we are trying to case-split out a selected input, but also we must +;; ensure that the resulting tests and cases will in fact be rep terms. + +(defthm in-excl-rdx + (implies (syntaxp (not (st-predp e))) + (equal (in e (excl c n)) + (cond ((not (excl c n)) nil) + ((c1 (excl c n)) (equal e (scar (excl c n)))) + (t (hide (in e (excl c n))))))) + :hints (("Goal" :expand (hide (in e (excl c n)))))) + + +;; And now we abstract the terms which we do not wish to include in state +;; information for the MESI model: + +(abstract-terms (in 'nil (excl (c-l (a)) n)) + (equal (scar (excl (c-l (a)) n)) 'nil) + (equal (g (a) (cache 'nil (c-l (a)) n)) (car (a-dat n))) + (equal (scar (valid c n)) e) + (c1 (valid c n))) + + +;; This final theorem basically defines the only case of <<s we care about: + +(defthm <<s-of-nil + (equal (<<s e x) (if x (hide (<<s e x)) t)) + :hints (("Goal" :expand (hide (<<s e x))))) + +(in-theory (disable <<s)) + diff --git a/books/workshops/2004/sumners-ray/support/records.lisp b/books/workshops/2004/sumners-ray/support/records.lisp new file mode 100644 index 0000000..57b406d --- /dev/null +++ b/books/workshops/2004/sumners-ray/support/records.lisp @@ -0,0 +1,644 @@ +;; maps.lisp + +(in-package "ACL2") + +(set-match-free-default :all) + +#| + +We define properties of a generic map or record accessor function and updater +function. The basic functions are (g a r) and (s a v r) where a is an +address/key, v is a value, r is a record, and (g a r) returns the value set to +address a in record r, and (s a v r) returns a new record with address a set to +value v in record r. + +The following main lemmas are "exported" about record (g)et and (s)et: + +(defthm g-same-s + (equal (g a (s a v r)) + v)) + +(defthm g-diff-s + (implies (not (equal a b)) + (equal (g a (s b v r)) + (g a r)))) + +(defthm s-same-g + (equal (s a (g a r) r) + r)) + +(defthm s-same-s + (equal (s a y (s a x r)) + (s a y r))) + +(defthm s-diff-s + (implies (not (equal a b)) + (equal (s b y (s a x r)) + (s a x (s b y r)))) + :rule-classes ((:rewrite :loop-stopper ((b a s))))) + +We also include some auxiliary lemmas which have proven useful. + +(defthm access-of-nil-is-nil + (not (g a nil))) + +(defthm record-set-cannot-be-nil + (implies v (s a v r))) + +(defthm record-get-non-nil-cannot-be-nil + (implies (g a r) r)) + +We also include some additional functions and lemmas for defining functions +which recur through a record. The function 'dom takes a record and returns the +set of "keys" or "fields" in the record. We prove the following properties of +'dom with respect 's and 'g. + +(defthm dom-of-s + (equal (dom (s a v r)) + (if v + (sadd a (dom r)) + (sdrop a (dom r))))) + +(defthm in-dom-iff-g + (iff (in a (dom r)) + (g a r))) + +We normalize the record structures (which allows the 'equal-ity based rewrite +rules) as alists where the keys (cars) are ordered using the total-order added +to ACL2 and defined in the included book. We define a set of "-aux" functions +which assume well-formed records -- defined by rcdp -- and then prove the +desired properties using hypothesis assuming well-formed records. + +We then remove these well-formed record hypothesis by defining an invertible +mapping (acl2->rcd) taking any ACL2 object and returning a well-formed +record. We then prove the desired properties using the proper translations of +the -aux functions to the acl2 objects, and subsequently remove the +well-formed record hypothesis. + +|# + +(include-book "sets") + +;; BEGIN records definitions. + +(verify-guards <<) + +(defun ill-formed-key () + (declare (xargs :guard t)) + "unlikely-we-should-ever-encounter-this-particular-string-as-a-key!?!?!?!") + +(defun wf-keyp (x) + (declare (xargs :guard t)) + (not (equal x (ill-formed-key)))) + +(defun rcdp (x) + (declare (xargs :guard t)) + (or (null x) + (and (consp x) + (consp (car x)) + (rcdp (cdr x)) + (cdar x) + (or (null (cdr x)) + (<< (caar x) (caadr x)))))) + +(defthm rcdp-implies-alistp + (implies (rcdp x) (alistp x))) + +(defun ifrp (x) ;; ill-formed rcdp + (declare (xargs :guard t)) + (or (not (rcdp x)) + (and (consp x) + (null (cdr x)) + (consp (car x)) + (equal (caar x) (ill-formed-key)) + (ifrp (cdar x))))) + +(defun acl2->rcd (x) ;; function mapping acl2 objects to well-formed records. + (declare (xargs :guard t)) + (if (ifrp x) (list (cons (ill-formed-key) x)) x)) + +(defun rcd->acl2 (x) ;; inverse of acl2->rcd. + (declare (xargs :guard t)) + (if (ifrp x) (and (consp x) (consp (car x)) (cdar x)) x)) + +(defun g-aux (a x) ;; record g(et) when x is a well-formed record. + (declare (xargs :guard (rcdp x))) + (cond ((or (endp x) + (<< a (caar x))) + nil) + ((equal a (caar x)) + (cdar x)) + (t + (g-aux a (cdr x))))) + +(defun g (a x) ;; the generic record g(et) which works on any ACL2 object. + (declare (xargs :guard t)) + (g-aux a (acl2->rcd x))) + +(defabbrev acons-if (a v x) + (if v (cons (cons a v) x) x)) + +(defun s-aux (a v r) ;; record s(et) when x is a well-formed record. + (declare (xargs :guard (rcdp r))) + (cond ((or (endp r) + (<< a (caar r))) + (acons-if a v r)) + ((equal a (caar r)) + (acons-if a v (cdr r))) + (t + (cons (car r) (s-aux a v (cdr r)))))) + +(defun s (a v x) ;; the generic record s(et) which works on any ACL2 object. + (declare (xargs :guard t)) + (rcd->acl2 (s-aux a v (acl2->rcd x)))) + +(defun dom-aux (x) +;; (declare (xargs :guard (rcdp x))) + (if (endp x) () + (sadd (caar x) (dom-aux (cdr x))))) + +(defun dom (x) + (dom-aux (acl2->rcd x))) + + +;; We now provide "faster" versions of the above record operations. The bodies +;; of these "f" functions should rewrite immediately to the nicer logic +;; functions. + +(defun wf-rcdp (x) + (declare (xargs :guard t)) + (or (null x) + (and (consp x) + (consp (car x)) + (wf-rcdp (cdr x)) + (cdar x) + (wf-keyp (caar x)) + (or (null (cdr x)) + (<< (caar x) (caadr x)))))) + +(local +(defthm wf-rcdp-implies-rcdp + (implies (wf-rcdp x) + (rcdp x)))) + +(local +(defthm wf-rcdp-implies-not-ifrp + (implies (wf-rcdp x) + (not (ifrp x))))) + +(defun fast-g (a r) + (declare (xargs :guard (wf-rcdp r))) + (cond ((endp r) nil) + ((equal a (caar r)) (cdar r)) + (t (fast-g a (cdr r))))) + +(local +(defthm fast-g-equals-g-aux + (implies (wf-rcdp r) + (equal (fast-g a r) + (g-aux a r))))) + +(defun fg (a r) + (declare (xargs :guard (wf-rcdp r))) + (mbe :logic (g a r) + :exec (fast-g a r))) + +(local +(defthm s-aux-is-bounded + (implies (and (rcdp r) + (s-aux a v r) + (<< e a) + (<< e (caar r))) + (<< e (caar (s-aux a v r)))))) + +(local +(defthm s-aux-preserves-wf-rcdp + (implies (and (wf-rcdp r) + (wf-keyp a)) + (wf-rcdp (s-aux a v r))))) + +(defun fast-s (a v r) + (declare (xargs :guard (wf-rcdp r))) + (cond ((endp r) + (acons-if a v ())) + ((equal a (caar r)) + (acons-if a v (cdr r))) + ((<< a (caar r)) + (acons-if a v r)) + (t + (cons (car r) (fast-s a v (cdr r)))))) + +(local +(defthm fast-s-equals-s-aux + (implies (wf-rcdp r) + (equal (fast-s a v r) + (s-aux a v r))))) + +(defun fs (a v r) + (declare (xargs :guard (and (wf-keyp a) (wf-rcdp r)))) + (mbe :logic (s a v r) + :exec (fast-s a v r))) + +;; we will need the following theorem in order to prove guards in functions +;; which use fs: + +(defthm s-preserves-wf-rcdp + (implies (and (wf-rcdp r) + (wf-keyp a)) + (wf-rcdp (s a v r)))) + + +;;;; basic property of records ;;;; + +(local +(defthm rcdp-implies-true-listp + (implies (rcdp x) + (true-listp x)) + :rule-classes (:forward-chaining + :rewrite))) + + +;;;; initial properties of s-aux and g-aux ;;;; + +(local +(defthm s-aux-preserves-rcdp + (implies (rcdp r) + (rcdp (s-aux a v r))))) + +(local +(defthm g-aux-same-s-aux + (implies (rcdp r) + (equal (g-aux a (s-aux a v r)) + v)))) + +(local +(defthm g-aux-diff-s-aux + (implies (and (rcdp r) + (not (equal a b))) + (equal (g-aux a (s-aux b v r)) + (g-aux a r))))) + +(local +(defthm s-aux-same-g-aux + (implies (rcdp r) + (equal (s-aux a (g-aux a r) r) + r)))) + +(local +(defthm s-aux-same-s-aux + (implies (rcdp r) + (equal (s-aux a y (s-aux a x r)) + (s-aux a y r))))) + +(local +(defthm s-aux-diff-s-aux + (implies (and (rcdp r) + (not (equal a b))) + (equal (s-aux b y (s-aux a x r)) + (s-aux a x (s-aux b y r)))) + :rule-classes ((:rewrite :loop-stopper ((b a s)))))) + +(local +(defthm s-aux-non-nil-cannot-be-nil + (implies (and v (rcdp r)) + (s-aux a v r)))) + +(local +(defthm g-aux-is-nil-for-<< + (implies (and (rcdp r) + (<< a (caar r))) + (not (g-aux a r))))) + +(local +(defthm dom-aux-of-s-aux + (implies (rcdp r) + (equal (dom-aux (s-aux a v r)) + (if v + (sadd a (dom-aux r)) + (sdrop a (dom-aux r))))))) + +(local +(defthm in-dom-aux-iff-g-aux + (implies (rcdp r) + (iff (g-aux a r) + (in a (dom-aux r)))))) + +(defun induct-two-records (r1 r2) + (declare (xargs :measure (+ (len r1) (len r2)))) + (cond ((endp r1) r2) + ((endp r2) r1) + ((<< (caar r1) (caar r2)) + (induct-two-records (cdr r1) r2)) + ((<< (caar r2) (caar r1)) + (induct-two-records r1 (cdr r2))) + ((equal (caar r1) (caar r2)) + (induct-two-records (cdr r1) (cdr r2))) + (t nil))) + +;;;; The output from the following theorems is voluminous, +;;;; and it is pretty impressive that ACL2 can get through +;;;; this proof without any help other than the induction +;;;; scheme. Cool. + +(local +(defthm equal-s-aux-redux-1 + (implies (and (rcdp r1) + (rcdp r2) + (equal (s-aux a v1 r1) (s-aux a v2 r2))) + (equal (equal v1 v2) t)) + :hints (("Goal" :induct (induct-two-records r1 r2))))) + +(local +(defthm equal-s-aux-redux-2 + (implies (and (rcdp r1) + (rcdp r2) + (equal (s-aux a v1 r1) (s-aux a v2 r2))) + (equal (equal (s-aux a v r1) (s-aux a v r2)) + t)) + :hints (("Goal" :induct (induct-two-records r1 r2))))) + +;;;; properties of acl2->rcd and rcd->acl2 ;;;; + +(local +(defthm acl2->rcd-rcd->acl2-of-rcdp + (implies (rcdp x) + (equal (acl2->rcd (rcd->acl2 x)) + x)))) + +(local +(defthm acl2->rcd-returns-rcdp + (rcdp (acl2->rcd x)))) + +(local +(defthm acl2->rcd-preserves-equality + (iff (equal (acl2->rcd x) (acl2->rcd y)) + (equal x y)))) + +(local +(defthm rcd->acl2-acl2->rcd-inverse + (equal (rcd->acl2 (acl2->rcd x)) x))) + +(local +(defthm rcd->acl2-of-record-non-nil + (implies (and r (rcdp r)) + (rcd->acl2 r)))) + +(local +(defthm rcd->acl2-preserves-equality-on-rcds + (implies (and (rcdp x) (rcdp y)) + (iff (equal (rcd->acl2 x) (rcd->acl2 y)) + (equal x y))))) + +(in-theory (disable acl2->rcd rcd->acl2)) + + +;;;; final (exported) properties of record g(et) and s(et) ;;;; + +(defthm dom-of-s + (equal (dom (s a v r)) + (if v + (sadd a (dom r)) + (sdrop a (dom r))))) + +(defthm in-dom-iff-g + (iff (g a r) + (in a (dom r)))) + +;; We disable this rule because it may introduce "dom" into contexts where it +;; is not wanted. +(in-theory (disable in-dom-iff-g)) + +(local +(defthm dom-aux-empty-iff-empty + (implies (rcdp r) + (iff (dom-aux r) r)))) + +(defthm dom-empty-iff-empty + (iff (dom x) x)) + +;; NOTE that these theorems basically follow from the "equivalent" properties +;; for s-aux and g-aux with rcdp hypothesis, and the lemmas about the acl2->rcd +;; and its inverse rcd->acl2. If the user wanted to add to the following set of +;; exported theorems, they should add the corresponding lemma about s-aux and +;; g-aux using rcdp hypothesis and then add the theorem here about the generic +;; s(et) and g(et) they wish to export from the book. + +(defthm g-same-s + (equal (g a (s a v r)) + v)) + +(defthm g-diff-s + (implies (not (equal a b)) + (equal (g a (s b v r)) + (g a r)))) + +;;;; NOTE: The following can be used instead of the above rules to force ACL2 +;;;; to do a case-split. We disable this rule by default since it can lead to +;;;; an expensive case explosion, but in many cases, this rule may be more +;;;; effective than two rules above and should be enabled. + +(defthm g-of-s-redux + (equal (g a (s b v r)) + (if (equal a b) v (g a r)))) + +(in-theory (disable g-of-s-redux)) + +(defthm s-same-g + (equal (s a (g a r) r) + r)) + +(defthm s-same-s + (equal (s a y (s a x r)) + (s a y r))) + +(defthm s-diff-s + (implies (not (equal a b)) + (equal (s b y (s a x r)) + (s a x (s b y r)))) + :rule-classes ((:rewrite :loop-stopper ((b a s))))) + +;; the following theorems are less relevant but have been useful in dealing +;; with a default record of NIL. + +(defthm g-of-nil-is-nil + (not (g a nil))) + +(defthm s-non-nil-cannot-be-nil + (implies v (s a v r)) + :hints (("Goal" + :in-theory (disable rcd->acl2-of-record-non-nil) + :use (:instance rcd->acl2-of-record-non-nil + (r (s-aux a v (acl2->rcd r))))))) + +(defthm non-nil-if-g-non-nil + (implies (g a r) r) + :rule-classes :forward-chaining) + +(defthm equal-s-redux-1 + (implies (equal (s a v1 r1) (s a v2 r2)) + (equal (equal v1 v2) t)) + :hints (("Goal" + :use ((:instance equal-s-aux-redux-1 + (r1 (acl2->rcd r1)) + (r2 (acl2->rcd r2)))) + :in-theory (disable equal-s-aux-redux-1)))) + +(defthm equal-s-redux-2 + (implies (equal (s a v1 r1) (s a v2 r2)) + (equal (equal (s a v r1) (s a v r2)) t))) + +;; Finally, we prove some "constructive" properties about records. In +;; particular, we want to show the following property: +;; +;; (not (equal (g a x) x)) +;; +;; unfortunately, the above is not true when x is NIL, and may not be true when +;; a is NIL, so we will have a weaker form of the above property: +;; +;; (implies (and x a) (not (equal (g a x) x))) +;; +;; further, we would like to generalize this to any nesting of g(et)s Well, +;; what we can show is the following property: +;; +;; (implies (and x a) (< (rcd-count (g a x)) (rcd-count x))) +;; +;; where rcd-count is a natural number measure function. + +(defun rcount-msr (r) + (cond ((null r) 0) + ((endp r) 1) + (t (+ 1 + (rcount-msr (car r)) + (rcount-msr (cdr r)))))) + +(defun rcount (r) + (declare (xargs :measure (rcount-msr r))) + (if (null r) 0 + (+ 1 + (rcount (cdar r)) + (rcount (cdr r))))) + +(defthm rcount-g-aux-< + (implies r + (< (rcount (g-aux a r)) + (rcount r)))) + +(defthm rcount-g-< + (implies (and x (wf-keyp a)) + (< (rcount (g a x)) + (rcount x))) + :hints (("Goal" :in-theory (enable acl2->rcd)))) + +;; We disable s, g, and dom assuming the rules proven in this book are +;; sufficient to manipulate record terms which are encountered. + +(in-theory (disable s g dom)) + +;; in order to facilitate debugging of proofs which involve (equal (s .) (s .)) +;; terms, we include some additional definitions and rules in terms of s and g. + +(defun s-clr (a r) (s a nil r)) + +(defthm equal-s-destruct + (equal (equal (s a v1 r1) (s a v2 r2)) + (and (equal v1 v2) + (equal (s-clr a r1) (s-clr a r2))))) + +;; we no longer desire to have the parent theorems enabled +(in-theory (disable equal-s-redux-1 equal-s-redux-2)) + +(defthm g-same-s-clr + (equal (g a (s-clr a r)) + nil)) + +(defthm g-diff-s-clr + (implies (not (equal a b)) + (equal (g a (s-clr b r)) + (g a r)))) + +(defthm s-same-s-clr + (equal (s-clr a (s a v r)) + (s-clr a r))) + +(defthm s-diff-s-clr + (implies (not (equal a b)) + (equal (s-clr b (s a v r)) + (s a v (s-clr b r))))) + +(defthm dom-s-clr + (equal (dom (s-clr a r)) + (sdrop a (dom r)))) + +;; we add some rules for dealing with the case where records are collapsed as +;; quoted constants. Some normalization may not occur in this case unless one +;; "cleans" up the quoted constant records. + +(defun quoted-rcd-with-non-nil-field (a r) + (or (and (quotep r) + (g a (second r))) + (and (consp r) + (eq (first r) 's) + (quoted-rcd-with-non-nil-field a (fourth r))))) + +(defthm s-clean-up-rcd + (implies (syntaxp (and (quotep a) + (quoted-rcd-with-non-nil-field (second a) r))) + (equal (s a v r) + (s a v (s-clr a r))))) + +(in-theory (disable s-clr)) + +;; equal-s-destruct may be too aggressive and possibly, the following rules are +;; more appropriate candidates for use (maybe together): + +(defthm equal-s-key + (equal (equal (s a v1 r) (s a v2 r)) + (equal v1 v2))) + +(defthm equal-s-rcd + (equal (equal (s a v r1) (s a v r2)) + (equal (s-clr a r1) (s-clr a r2)))) + +(in-theory (disable equal-s-destruct equal-s-key equal-s-rcd)) + +;; we conclude with some useful macros for defining functions which recur +;; through records (for functions of this ilk, use (xargs :measure (rmsr r)) on +;; the record parameter) + +(defmacro rempty (r) + `(not (dom ,r))) + +(defmacro rcar (r) + `(scar (dom ,r))) + +(defmacro rcdr (r) + `(s-clr (rcar ,r) ,r)) + +(defmacro rmsr (r) + `(card (dom ,r))) + +(in-theory (disable s g)) + +(defun rts (n r) + (declare (xargs :guard (and (integerp n) (>= n 0) + (wf-rcdp r)))) + (if (zp n) r + (let ((k (- (nfix (g :b r)) + (nfix (g :b r))))) + (rts (1- n) (s :b (1+ k) r))))) + +(defun frts (n r) + (declare (xargs :guard (and (integerp n) (>= n 0) + (wf-rcdp r)))) + (if (zp n) r + (let ((k (- (nfix (fg :b r)) + (nfix (fg :b r))))) + (frts (1- n) (fs :b (1+ k) r))))) + +(defun arts (n r) + (declare (xargs :guard (and (integerp n) (>= n 0) + (alistp r)))) + (if (zp n) r + (let ((k (nfix (cdr (assoc-eq :a r))))) + (arts (1- n) (acons :a (1+ k) r))))) + diff --git a/books/workshops/2004/sumners-ray/support/sets.lisp b/books/workshops/2004/sumners-ray/support/sets.lisp new file mode 100644 index 0000000..951d261 --- /dev/null +++ b/books/workshops/2004/sumners-ray/support/sets.lisp @@ -0,0 +1,1220 @@ +;; sets.lisp + +(in-package "ACL2") + +(set-match-free-default :all) + +#| + +We define the common boolean operations (and a few other common useful notions) +on sets canonicalized as ordered lists using Pete's total ordering of all ACL2 +objects. Further, the functions have been defined with a normalization of all +ACL2 objects as appropriate sets (we define a 1-1 function which maps any ACL2 +object to a corresponding well-formed set) and using this normal (and its +inverse), we can prove properties about normalized set operations which use +equal-ity instead of set-equality and require no backtracking to relieve +well-formed set hypotheses. + +EXPORTED logic functions: + + (in e x) -- set membership predicate, is element e a member of set x + (subset x y) -- subset predicate, is set x a subset of set y + (isect x y) -- the set intersection of set x and set y + (unite x y) -- the set union of set x and set y + (sdiff x y) -- the set of elements in set x but not in set y + (card x) -- returns the number of objects in the set x + (s1 e) -- the singleton set consisting only of the element e + (scar x) -- the least (by <<) element in the set x, nil if x is empty + () -- NIL is unique representative value for empty set, + so use NULL or NOT to test a set for emptiness + (c1 x) -- test which returns true if x is a singleton set + +EXPORTED theorems provided at the end of this file. + +I have removed all of the subgoal hints except for those introduced by the +macro defthm-ternary-sets. These subgoal hints are reasonable since they are +introduced in the context of a provided induction scheme and they help speed +the proofs through considerably by avoiding the problem in ACL2 of +free-variable matching in the application of <<-transitive. + +|# + +(include-book "total-order") + +;; i needed to add the following forward-chaining rule to make better use +;; of <<-trichotomy from the included order book. + +(local +(defthm <<-trichotomy-forward-chain1 + (implies (and (not (<< x y)) + (not (equal x y))) + (<< y x)) + :rule-classes :forward-chaining)) + +(defun setp (x) + (or (null x) + (and (consp x) + (setp (rest x)) + (or (null (rest x)) + (<< (first x) (second x)))))) + +(defun ifsp (x) ;; ill-formed setp + (or (not (setp x)) + (and (consp x) + (null (cdr x)) + (ifsp (car x))))) + +(defun norm->set (x) + (if (ifsp x) (list x) x)) + +(defun set->norm (x) + (if (ifsp x) (first x) x)) + +(defun in-aux (e x) + (and (not (endp x)) + (or (equal e (first x)) + (and (<< (first x) e) + (in-aux e (rest x)))))) + +(defun in (e x) + (in-aux e (norm->set x))) + +(defun subset-aux (x y) + (or (endp x) + (and (not (endp y)) + (cond ((equal (first x) (first y)) + (subset-aux (rest x) (rest y))) + ((<< (first y) (first x)) + (subset-aux x (rest y))) + (t nil))))) + +(defun subset (x y) + (subset-aux (norm->set x) (norm->set y))) + +(defun isect-aux (x y) + (declare (xargs :measure (+ (acl2-count x) + (acl2-count y)))) + (cond ((endp x) ()) + ((endp y) ()) + ((equal (first x) (first y)) + (cons (first x) + (isect-aux (rest x) (rest y)))) + ((<< (first x) (first y)) + (isect-aux (rest x) y)) + (t + (isect-aux x (rest y))))) + +(defun isect (x y) + (set->norm (isect-aux (norm->set x) (norm->set y)))) + +(defun unite-aux (x y) + (declare (xargs :measure (+ (acl2-count x) + (acl2-count y)))) + (cond ((endp x) y) + ((endp y) x) + ((equal (first x) (first y)) + (cons (first x) + (unite-aux (rest x) (rest y)))) + ((<< (first x) (first y)) + (cons (first x) + (unite-aux (rest x) y))) + (t + (cons (first y) + (unite-aux x (rest y)))))) + +(defun unite (x y) + (set->norm (unite-aux (norm->set x) (norm->set y)))) + +(defun sdiff-aux (x y) + (declare (xargs :measure (+ (acl2-count x) + (acl2-count y)))) + (cond ((endp x) ()) + ((endp y) x) + ((equal (first x) (first y)) + (sdiff-aux (rest x) (rest y))) + ((<< (first x) (first y)) + (cons (first x) + (sdiff-aux (rest x) y))) + (t + (sdiff-aux x (rest y))))) + +(defun sdiff (x y) + (set->norm (sdiff-aux (norm->set x) (norm->set y)))) + +(defun s1 (e) + (set->norm (list e))) + +(defun card (x) + (len (norm->set x))) + +(defun scar (x) + (if (ifsp x) x (first x))) + +(defmacro empty-set () + `()) + +(defun c1 (x) + (let ((x (norm->set x))) (and (consp x) (not (cdr x))))) + + + +;;; some useful auxiliary macros which could be removed if +;;; needed (e.g. if the names conflict with existing fns) + +(defmacro sadd (e x) + `(unite (s1 ,e) ,x)) + +(defmacro sdrop (e x) + `(sdiff ,x (s1 ,e))) + +(defmacro scdr (x) + `(sdrop (scar ,x) ,x)) + +(defmacro satom (x) + `(not ,x)) + +(defmacro common (x y) + `(not (satom (isect ,x ,y)))) + + +;;;; properties of setp ;;;; + +(local +(defthm setp-implies-true-listp + (implies (setp x) + (true-listp x)) + :rule-classes (:forward-chaining + :rewrite))) + + +;;;; properties of norm->set and set->norm ;;;; + +(local +(defthm norm->set-set->norm-of-setp + (implies (setp x) + (equal (norm->set (set->norm x)) + x)))) + +(local +(defthm norm->set-of-wf-setp + (implies (not (ifsp x)) + (equal (norm->set x) x)))) + +(local +(defthm norm->set-of-if-setp + (implies (ifsp x) + (equal (norm->set x) (list x))))) + +(local +(defthm norm->set-returns-setp + (setp (norm->set x)))) + +(local +(defthm norm->set-preserves-equality + (iff (equal (norm->set x) (norm->set y)) + (equal x y)))) + +(local +(defthm set->norm-norm->set-inverse + (equal (set->norm (norm->set x)) x))) + +(local +(defthm set->norm-nil-iff-passed-nil + (implies (setp x) + (iff (set->norm x) x)))) + +(local +(defthm norm->set-of-x-is-consp-or-not-x + (iff (consp (norm->set x)) x) + :rule-classes nil)) + +(local +(defthm norm->set-is-true-listp + (true-listp (norm->set x)) + :rule-classes :type-prescription)) + +(in-theory (disable set->norm norm->set)) + + +;;;; bounded properties ;;;; + +(local +(defthm unite-aux-bounded-<< + (implies (and (<< a (first x)) + (<< a (first y))) + (<< a (first (unite-aux x y)))))) + +(local +(defthm isect-aux-bounded-<< + (implies (and (or (<< a (first x)) + (<< a (first y))) + (isect-aux x y)) + (<< a (first (isect-aux x y)))))) + +(local +(defthm sdiff-aux-bounded-<< + (implies (and (setp x) + (<< a (first x)) + (sdiff-aux x y)) + (<< a (first (sdiff-aux x y)))))) + + +;;;; type-correctness properties ;;;; + +(local +(defthm unite-aux-preserves-setp + (implies (and (setp x) (setp y)) + (setp (unite-aux x y))) + :rule-classes ((:forward-chaining + :trigger-terms ((unite-aux x y))) + :rewrite))) + +(local +(defthm isect-aux-preserves-setp + (implies (and (setp x) (setp y)) + (setp (isect-aux x y))) + :rule-classes ((:forward-chaining + :trigger-terms ((isect-aux x y))) + :rewrite))) + +(local +(defthm sdiff-aux-preserves-setp + (implies (setp x) + (setp (sdiff-aux x y))) + :rule-classes ((:forward-chaining + :trigger-terms ((sdiff-aux x y))) + :rewrite))) + + +;;;; properties of membership-aux ;;;; + +(local +(defthm in-aux-isect-aux-reduce + (equal (in-aux e (isect-aux x y)) + (and (in-aux e x) (in-aux e y))))) + +(local +(defthm in-aux-unite-aux-reduce + (equal (in-aux e (unite-aux x y)) + (or (in-aux e x) (in-aux e y))))) + +(local +(defthm in-aux-implies-bounded + (implies (and (setp x) + (<< a (first x))) + (not (in-aux a x))))) + +(local +(defthm in-aux-sdiff-aux-reduce + (implies (setp x) + (equal (in-aux e (sdiff-aux x y)) + (and (in-aux e x) (not (in-aux e y))))))) + +(local +(defthm in-aux-subset-aux-transits + (implies (and (in-aux e x) + (subset-aux x y)) + (in-aux e y)))) + + +;;;; ternary variable induction scheme and strategy ;;;; + +;; the following function defines an induction scheme used in theorems +;; involving three free variables (like associativity proofs). + +(local +(defun ternary-induct (x y z) + (declare (xargs :measure (+ (acl2-count x) + (acl2-count y) + (acl2-count z)))) + (if (or (endp x) + (endp y) + (endp z)) + ; The following was changed to avoid SBCL warning, "Asserted type NUMBER + ; conflicts with derived type (VALUES LIST &OPTIONAL)." + (list x y z) + (cond ((<< (first x) (first y)) + (cond ((<< (first x) (first z)) + (ternary-induct (rest x) y z)) + ((equal (first x) (first z)) + (ternary-induct (rest x) y (rest z))) + ((and (<< (first z) (first x)) + (<< (first z) (first y))) + (ternary-induct x y (rest z))))) + ((equal (first x) (first y)) + (cond ((<< (first x) (first z)) + (ternary-induct (rest x) (rest y) z)) + ((equal (first x) (first z)) + (ternary-induct (rest x) (rest y) (rest z))) + ((<< (first z) (first x)) + (ternary-induct x y (rest z))))) + ((<< (first y) (first x)) + (cond ((<< (first y) (first z)) + (ternary-induct x (rest y) z)) + ((equal (first y) (first z)) + (ternary-induct x (rest y) (rest z))) + ((and (<< (first z) (first y)) + (<< (first z) (first x))) + (ternary-induct x y (rest z))))))))) + +;; the following macro defines an effective strategy for inducting based on the +;; scheme ternary-induct. + +(defmacro defthm-ternary-sets (name body) + `(defthm ,name ,body + :hints (("Goal" + :induct (ternary-induct x y z) + :in-theory (disable <<-transitive)) + ("Subgoal *1/13" + :in-theory (enable <<-transitive)) + ("Subgoal *1/5" + :in-theory (enable <<-transitive))))) + + +;;;; properties of subset-aux ;;;; + +(local +(defthm unite-aux-x<y-expansion + (implies (and (consp x) + (consp y) + (<< (car x) (car y))) + (equal (unite-aux x y) + (cons (car x) + (unite-aux (cdr x) y)))))) + +(local +(defthm subset-aux-x<y-reduces-nil + (implies (and (consp x) + (consp y) + (<< (car x) (car y))) + (equal (subset-aux x y) + nil)))) + +(local +(defthm atom-unite-aux-implies-atom-params + (implies (not (consp (unite-aux x y))) + (and (not (consp x)) + (not (consp y)))))) + +(local +(defthm-ternary-sets subset-aux-unite-aux-reduction + (equal (subset-aux (unite-aux x y) z) + (and (subset-aux x z) + (subset-aux y z))))) + +(local +(in-theory (disable unite-aux-x<y-expansion))) + +(local +(defthm subset-aux-is-reflexive + (subset-aux x x))) + +(local +(defthm subset-aux-unite-aux-property + (implies (setp x) + (subset-aux x (unite-aux x y))))) + +(local +(defthm <<-irreflexive-rewrite + (implies (<< x y) + (not (equal x y))))) + +(local +(defthm-ternary-sets subset-aux-isect-aux-reduction + (equal (subset-aux x (isect-aux y z)) + (and (subset-aux x y) + (subset-aux x z))))) + +(local +(defthm subset-aux-isect-aux-property + (implies (setp x) + (subset-aux (isect-aux x y) x)))) + +(local +(defthm subset-aux-sdiff-aux-property + (implies (setp x) + (subset-aux (sdiff-aux x y) x)))) + +(local +(defthm-ternary-sets subset-aux-is-transitive + (implies (and (subset-aux x y) + (subset-aux y z)) + (subset-aux x z)))) + +(local +(defthm subset-aux-is-total-on-sets + (implies (and (setp x) (setp y) + (subset-aux x y)) + (equal (subset-aux y x) + (equal x y))))) + +(local +(defthm subset-length-property + (implies (and (setp x) + (setp y) + (subset-aux x y)) + (<= (len x) (len y))))) + +(local +(defthm len<-reduce-when-subset + (implies (and (setp x) + (setp y) + (subset-aux x y)) + (equal (< (len x) (len y)) + (not (equal x y)))))) + + +;;;; properties of unite-aux ;;;; + +(local +(defthm unite-aux-implied-by-and + (implies (and (setp x) + (setp y) + x y) + (unite-aux x y)))) + +(local +(defthm unite-aux-reflexes + (implies (setp x) + (equal (unite-aux x x) x)))) + +(local +(defthm unite-aux-commutes + (implies (and (setp x) (setp y)) + (equal (unite-aux x y) + (unite-aux y x))))) + +(local +(defthm unite-aux-x<y-expansion-flip + (implies (and (consp x) + (consp y) + (<< (car x) (car y))) + (equal (unite-aux y x) + (cons (car x) + (unite-aux y (cdr x))))))) + +(local +(in-theory (enable unite-aux-x<y-expansion))) + +(local +(defthm-ternary-sets unite-aux-associates + (implies (and (setp x) (setp y) (setp z)) + (equal (unite-aux (unite-aux x y) z) + (unite-aux x (unite-aux y z)))))) + +(local +(in-theory (disable unite-aux-x<y-expansion-flip + unite-aux-x<y-expansion))) + +(local +(defthm unite-aux-subset-aux-property + (equal (equal (unite-aux x y) y) + (subset-aux x y)))) + +(local +(defthm length-of-unite-aux-property + (implies (and (setp x) (setp y)) + (equal (len (unite-aux x y)) + (+ (len x) + (len (sdiff-aux y x))))))) + +(local +(defthm set-norm-equality-transfer + (implies (setp x) + (equal (equal (set->norm x) y) + (equal x (norm->set y)))))) + + +;;;; properties of isect-aux ;;;; + +(local +(defthm isect-aux-reflexes + (implies (setp x) + (equal (isect-aux x x) x)))) + +(local +(defthm isect-aux-commutes + (implies (and (setp x) (setp y)) + (equal (isect-aux x y) (isect-aux y x))))) + +(local +(defthm isect-aux-x<y-expansion + (implies (and (consp x) + (consp y) + (<< (car x) (car y))) + (equal (isect-aux y x) + (isect-aux y (cdr x)))))) + +(local +(defthm-ternary-sets isect-aux-associates + (implies (and (setp x) (setp y) (setp z)) + (equal (isect-aux (isect-aux x y) z) + (isect-aux x (isect-aux y z)))))) + +(local +(in-theory (disable isect-aux-commutes + unite-aux-commutes))) + +(local +(defthm isect-aux-bounded-then-not-equal + (implies (and (consp z) + (or (<< (car z) (car x)) + (<< (car z) (car y)))) + (not (equal (isect-aux x y) z))))) + +(local +(defthm isect-aux-subset-aux-property + (implies (and (setp x) (setp y)) + (equal (equal (isect-aux x y) x) + (subset-aux x y))))) + +(local +(defthm <<-irreflexive-rewrite-flip + (implies (<< x y) + (not (equal y x))))) + +(local +(defthm-ternary-sets isect-aux-unite-aux-distributes + (implies (and (setp x) (setp y) (setp z)) + (equal (isect-aux (unite-aux x y) z) + (unite-aux (isect-aux x z) + (isect-aux y z)))))) + +(local +(defthm-ternary-sets isect-aux-sdiff-aux-distributes + (implies (and (setp x) (setp y) (setp z)) + (equal (isect-aux (sdiff-aux x y) z) + (sdiff-aux (isect-aux x z) y))))) + + +;;;; properties of sdiff-aux ;;;; + +(local +(defthm sdiff-aux-subset-aux-property + (implies (and (setp x) (setp y)) + (iff (sdiff-aux x y) + (not (subset-aux x y)))))) + +(local +(defthm length-of-sdiff-aux-property + (implies (and (setp x) (setp y)) + (equal (len (sdiff-aux x y)) + (- (len x) + (len (isect-aux x y))))))) + +(local +(defthm-ternary-sets sdiff-aux-unite-aux-distributes + (implies (and (setp x) (setp y) (setp z)) + (equal (sdiff-aux (unite-aux x y) z) + (unite-aux (sdiff-aux x z) + (sdiff-aux y z)))))) + +(local +(defthm-ternary-sets sdiff-aux-unite-aux-reduction + (implies (and (setp x) (setp y) (setp z)) + (equal (sdiff-aux x (unite-aux y z)) + (sdiff-aux (sdiff-aux x y) z))))) + +(local +(defthm sdiff-aux-reduce-no-isect-aux + (implies (and (setp x) (setp y) (not (isect-aux x y))) + (equal (sdiff-aux x y) x)))) + + +;;;; properties of s1-aux -- i.e. list ;;;; + +(local +(defthm subset-aux-reduces-to-membership + (implies (setp x) + (equal (subset-aux (list e) x) + (in-aux e x))))) + +(local +(defthm subset-aux-of-singleton + (implies (and (setp x) x + (subset-aux x (list e))) + (equal (equal x (list e)) t)))) + +(local +(defthm isect-aux-of-singleton + (implies (setp x) + (equal (isect-aux (list e) x) + (if (in-aux e x) (list e) ()))))) + +(local +(defthm sdiff-aux-of-singleton + (implies (setp x) + (equal (sdiff-aux (list e) x) + (if (in-aux e x) () (list e)))))) + + +;;;; EXPORTED THEOREMS ;;;; +;; Note, the order of the these theorems below is relevant for the +;; order in which ACL2 applies them (later ones first). This is why +;; the associativity and commutativity theorems are first since +;; restructuring unite and isect can have the detrimental effect of +;; disabling the application of other rules. + +(local +(in-theory (enable unite-aux-commutes + isect-aux-commutes))) + + +;;;; EXPORTED associative and commutative properties ;;;; + +(defthm unite-implied-by-and + (implies (and x y) + (unite x y))) + +(defthm unite-reflexes + (equal (unite x x) x)) + +(defthm unite-commutes + (equal (unite x y) + (unite y x))) + +(defthm unite-associates + (equal (unite (unite x y) z) + (unite x (unite y z)))) + +(defthm unite-associate-2 + (equal (unite x (unite y z)) + (unite y (unite x z))) + :hints (("Goal" + :in-theory (disable unite-commutes) + :use ((:instance unite-commutes + (x x) (y (unite y z))) + (:instance unite-commutes + (x x) (y z)))))) + +(defthm isect-reflexes + (equal (isect x x) x)) + +(defthm isect-commutes + (equal (isect x y) + (isect y x))) + +(defthm isect-associates + (equal (isect (isect x y) z) + (isect x (isect y z)))) + +(defthm isect-associate-2 + (equal (isect x (isect y z)) + (isect y (isect x z))) + :hints (("Goal" + :in-theory (disable isect-commutes) + :use ((:instance isect-commutes + (x x) (y (isect y z))) + (:instance isect-commutes + (x x) (y z)))))) + +;;;; EXPORTED properties of membership ;;;; + +(defthm in-isect-reduce + (equal (in e (isect x y)) + (and (in e x) (in e y)))) + +(defthm in-unite-reduce + (equal (in e (unite x y)) + (or (in e x) (in e y)))) + +(defthm in-sdiff-reduce + (equal (in e (sdiff x y)) + (and (in e x) (not (in e y))))) + +(defthm in-subset-transits + (implies (and (in e x) + (subset x y)) + (in e y))) + + +;;;; EXPORTED properties of susbet ;;;; + +(defthm subset-unite-reduction + (equal (subset (unite x y) z) + (and (subset x z) + (subset y z)))) + +(defthm subset-unite-property + (subset x (unite x y))) + +(defthm subset-isect-reduction + (equal (subset x (isect y z)) + (and (subset x y) + (subset x z)))) + +(defthm subset-isect-property + (subset (isect x y) x)) + +(defthm subset-sdiff-property + (subset (sdiff x y) x)) + +(defthm subset-is-reflexive + (subset x x)) + +(defthm subset-is-transitive + (implies (and (subset x y) + (subset y z)) + (subset x z))) + +(defthm subset-is-total-order + (implies (subset x y) + (equal (subset y x) + (equal x y)))) + +(defthm subset-card-property + (implies (subset x y) + (<= (card x) (card y)))) + +(defthm card<-reduce-when-subset + (implies (subset x y) + (equal (< (card x) (card y)) + (not (equal x y))))) + + +;;;; EXPORTED reductions of unite ;;;; + +(defthm unite-subset-property + (equal (equal (unite x y) y) + (subset x y))) + +(defthm unite-subset-property-2 + (equal (equal (unite y x) y) + (subset x y))) + +(defthm unite-card-property + (equal (card (unite x y)) + (+ (card x) + (card (sdiff y x))))) + + +;;;; EXPORTED reductions of isect ;;;; + +(defthm isect-subset-property + (equal (equal (isect x y) x) + (subset x y))) + +(defthm isect-unite-distributes-1 + (equal (isect (unite x y) z) + (unite (isect x z) + (isect y z)))) + +(defthm isect-unite-distributes-2 + (equal (isect z (unite x y)) + (unite (isect x z) + (isect y z))) + :hints (("Goal" :in-theory (disable isect-aux-commutes) + :use (:instance isect-aux-commutes + (x (norm->set z)) + (y (unite-aux (norm->set x) + (norm->set y))))))) + +(defthm isect-sdiff-distributes-1 + (equal (isect (sdiff x y) z) + (sdiff (isect x z) y))) + +(defthm isect-sdiff-distributes-2 + (equal (isect z (sdiff x y)) + (sdiff (isect x z) y)) + :hints (("Goal" :in-theory (disable isect-aux-commutes) + :use (:instance isect-aux-commutes + (x (norm->set z)) + (y (sdiff-aux (norm->set x) + (norm->set y))))))) + + +;;;; EXPORTED reductions of sdiff ;;;; + +(defthm sdiff-subset-property + (iff (sdiff x y) + (not (subset x y)))) + +(defthm sdiff-card-property + (equal (card (sdiff x y)) + (- (card x) + (card (isect x y))))) + +(defthm sdiff-unite-distributes + (equal (sdiff (unite x y) z) + (unite (sdiff x z) + (sdiff y z)))) + +(defthm sdiff-unite-reduction + (equal (sdiff x (unite y z)) + (sdiff (sdiff x y) z))) + +(defthm sdiff-reduce-no-isect + (implies (not (isect x y)) + (equal (sdiff x y) x))) + + +;;;; EXPORTED reductions of s1 ;;;; + +(defthm s1-membership-property + (equal (in a (s1 b)) + (equal a b))) + +(defthm s1-subset-property-1 + (equal (subset (s1 e) x) + (in e x))) + +(defthm s1-subset-property-2 + (implies (and (subset x (s1 e)) x) + (equal x (s1 e))) + :hints (("Goal" :use + (:instance norm->set-of-x-is-consp-or-not-x))) + :rule-classes :forward-chaining) + +(defthm s1-isect-property-1 + (equal (isect (s1 e) x) + (if (in e x) (s1 e) ()))) + +(defthm s1-isect-property-2 + (equal (isect x (s1 e)) + (if (in e x) (s1 e) ())) + :hints (("Goal" :in-theory (disable isect-aux-commutes) + :use (:instance isect-aux-commutes + (x (norm->set x)) + (y (list e)))))) + +(defthm s1-sdiff-property + (equal (sdiff (s1 e) x) + (if (in e x) () (s1 e)))) + +(defthm s1-card-property + (equal (card (s1 e)) 1)) + +(defthm s1-iff-t (iff (s1 e) t)) + +(defthm s1-equal-nil + (equal (equal (s1 e) nil) nil)) + +(defthm subset-s1-redux + (equal (subset a (s1 e)) + (if a (equal a (s1 e)) t))) + + + +;;;; EXPORTED properties of empty-set ;;;; + +(defthm membership-empty-set + (not (in e (empty-set)))) + +(defthm empty-set-is-subset + (subset (empty-set) x)) + +(defthm empty-set-is-only-superset-self + (equal (subset x (empty-set)) + (not x))) + +(defthm unite-empty-set-property-1 + (equal (unite x (empty-set)) x)) + +(defthm unite-empty-set-property-2 + (equal (unite (empty-set) x) x)) + +(defthm isect-empty-set-property-1 + (equal (isect (empty-set) x) (empty-set))) + +(defthm isect-empty-set-property-2 + (equal (isect x (empty-set)) (empty-set))) + +(defthm sdiff-of-empty-set-1 + (equal (sdiff (empty-set) x) (empty-set))) + +(defthm sdiff-of-empty-set-2 + (equal (sdiff x (empty-set)) x)) + +(defthm s1-is-not-empty-set + (s1 e) + :hints (("Goal" :in-theory (enable set->norm))) + :rule-classes :type-prescription) + +(defthm card-of-empty-set + (iff (not x) + (equal (card x) 0)) + :hints (("Goal" :in-theory (enable norm->set))) + :rule-classes :type-prescription) + + +;;;; EXPORTED properties of scar ;;;; + +(defthm scar-membership-property + (iff (in (scar x) x) x)) + +(defthm scar-is-least-member + (implies (and (in e x) + (not (equal e (scar x)))) + (<< (scar x) e))) + +(defthm scar-returns-nil-for-empty-set + (equal (scar (empty-set)) nil)) + +(defthm scar-of-s1 + (equal (scar (s1 e)) e) + :hints (("Goal" :in-theory (enable set->norm)))) + +(defthm scar-of-unite + (implies (and x y) + (equal (scar (unite x y)) + (if (<< (scar x) (scar y)) (scar x) (scar y)))) + :hints (("Goal" :in-theory (enable norm->set set->norm)))) + +(defthm scar-of-sdiff + (implies (<< (scar x) (scar y)) + (equal (scar (sdiff x y)) (scar x))) + :hints (("Goal" :in-theory (enable norm->set set->norm)))) + + +;;;; EXPORTED properties of c1 ;;;; + +(defthm c1-of-s1 + (equal (c1 (s1 e)) t)) + +(defthm c1-of-nil + (equal (c1 ()) nil)) + +(defthm c1-of-unite + (equal (c1 (unite x y)) + (if (c1 x) (implies y (equal x y)) (and (not x) (c1 y)))) + :hints (("Goal" :in-theory (enable norm->set set->norm) + :expand ((unite-aux (list x) y) (unite-aux x y))))) + +(defthm isect-aux-sdiff-aux-prop1 + (implies (and (setp x) x + (not (isect-aux x y))) + (sdiff-aux x y))) + +(defthm isect-aux-sdiff-aux-prop2 + (implies (and (consp x) + (setp x) + (not (isect-aux x y)) + (not (cdr (sdiff-aux x y)))) + (not (cdr x)))) + +(defthm c1-of-sdiff + (implies (not (isect x y)) + (equal (c1 (sdiff x y)) (c1 x))) + :hints (("Goal" :in-theory (enable norm->set set->norm) + :expand ((:free (x) (sdiff-aux (list x) y)) + (:free (x z) (sdiff-aux (list x z) y)) + (:free (x a b) (sdiff-aux (list* x a b) y)))))) + +(defthm c1-not-sdiff + (implies (and (isect x y) (c1 x)) + (not (sdiff x y))) + :hints (("Goal" :in-theory (enable norm->set set->norm) + :expand (:free (x) (sdiff-aux (list x) y))))) + + +;; we now disable the top-level functions to keep their +;; definitions from being expanded + +(in-theory (disable in subset isect unite sdiff card s1 scar c1)) + +;; the following macro will enable/disable the executable-counterparts + +(defmacro ec-sets (x) + `(in-theory (,(if x 'enable 'disable) + (in) (subset) (isect) (unite) + (sdiff) (card) (s1) (scar) (c1)))) + +;; we will begin with the executable-counterparts disabled + +(ec-sets nil) + +;; the following macro is a convenient way to define constants, it is similar +;; to the 'list macro + +(defmacro make-set (&rest elems) + (if (endp elems) '(emptyset) + `(sadd ,(first elems) (make-set ,@(rest elems))))) + + + +;; we conclude with a few corollaries + +(defthm unite-iff-or + (iff (unite x y) (or x y)) + :hints (("Goal" :cases ((not x) (not y))))) + +(defthm unite-x-absorption + (equal (unite x (unite x y)) (unite x y))) + +(defthm c1-of-sadd + (equal (c1 (sadd e x)) (if (c1 x) (equal x (s1 e)) (not x)))) + +(defthm equal-s1-redux + (equal (equal (s1 a) (s1 b)) (equal a b)) + :hints (("Goal" :in-theory (enable s1)))) + +(defthm wrap-up-s1-equal-to-c1 + (equal (equal (s1 (scar s)) s) (c1 s)) + :hints (("Goal" :in-theory (enable s1 scar c1)))) + +(defthm c1-in-redux-scar + (implies (c1 s) (equal (in e s) (equal e (scar s)))) + :hints (("Goal" :in-theory (enable in c1 scar)))) + +(local +(defthm setp-cons-redux + (equal (setp (cons x y)) + (and (setp y) (implies y (<< x (car y))))))) + +(defthm equal-sadd-s1-redux + (equal (equal (sadd e x) (s1 a)) + (and (equal e a) (implies x (equal x (s1 e))))) + :hints (("Goal" :in-theory (enable s1 unite norm->set set->norm) + :expand ((unite-aux (list e) x))))) + + + + +#| + + + +> I propose the following additions to the sets book: +> +> (defthm sdiff-x-x +> (equal (sdiff x x) +> (empty-set))) + +The following rule subsumes yours and I think would be +a better addition: + +(defthm sdiff-superset + (implies (subset x y) + (equal (sdiff x y) + (empty-set)))) + +> ;(add similar lemmas about other functions than unite +> (e.g., isect)? +> (defthm unite-reflexes-2 +> (equal (unite x (unite x y)) +> (unite x y))) +> +> ;and can you prove this one for me? +> (defthm sdiff-sdiff +> (equal (sdiff (sdiff x y) y) +> (sdiff x y)) +> ) + +absorption rules for unite, isect, and sdiff (on the right) +would be good. I have no idea why I had not considered adding +these before. I will probably generalize them to have subset +hypothesis. + +> BTW, what's the status of the sets book? Will it be +> released with ACL2? + +It is in one of the workshops, although I am uncertain if it +is updated. I will probably get Matt to add it to the misc +directory (especially with some of the recent additions to +the records book which make use of the sets book). + +> I also need: +> +> (defthm unite-sdiff-hack +> (equal (unite x (sdiff y x)) +> (unite x y))) + +Hmmm. I am uncertain if this is a proper reduction. Intuitively, +while the lhs is a bigger term, it is smaller in terms of +cardinality. I will need to think about this case, but offhand, +I don't see this as an obviously good addition to the sets book. + +> (BTW, I'm assuming its okay to ask you to prove these +> since they'd make good additions to the sets book, +> which you are developing. If you'd rather not be +> bothered with this, let me know.) + +Please feel free to make suggestions (just don't expect that I +will always be quick in handling the suggestions). I like using +the sets book and would like to see others use it as well. (I am +generally an advocate of having books with rewrite rules which +are "context-free" -- well as context-free as possible). + + -Rob + + +> i talked with Matt (the other "old-timer") and we +> are +> in tacit agreement that we should change +> "records.lisp" +> to "maps.lisp" (the new version with all of the +> various +> improvements and which includes the sets book). But, +> I want to wait ask about this at the next ACL2 +> meeting +> to get an idea of how many people (if any) are using +> the +> records book. + +Excellent. + +My sense is that people aren't using the records/maps +book enough (and that, in general, people don't +appreciate the importance of the tricks done to make +the records book clean). Did anyone ever give a talk +on records/maps at the ACL2 seminar? + +I'm changing my copy of the "M5" JVM model to use +records, and I think this is clearly the way to go. +(There are some subtleties, but I now have a fairly +clean algebra for the heap.) If J's folks keep +hearing about this from enough people, maybe they'll +use records for M6. Hanbing seems to be in charge of +M6. + +> > BTW, are there easy proofs for either of the +> following +> > (which I've left as axioms in order to get on with +> my +> > JVM proofs)? I'm not terribly familiar with the +> sets +> > book, and I didn't find an easy proof for these. +> > +> > (defaxiom sdiff-sdiff +> > (equal (ACL2::SDIFF (ACL2::SDIFF Z X) X) +> > (ACL2::SDIFF Z X))) +> > +> > (defaxiom unite-hack +> > (equal (acl2::unite x (acl2::sdiff z x)) +> > (acl2::unite x z))) +> +> I believe these are provable, but not easily proven +> in +> terms of the existing rules. +> +> I am planning on doing some work with the records (I +> mean +> "maps") and sets books this weekend. The updates +> should +> cover these theorems (and many others). I will send +> them +> to you on Monday. + +That would be great! Thanks. I've been spending a +lot of time making changes to M5 and thinking about +sets, maps, and other implementation details, instead +of actually doing the proofs I'm supposed to be doing +(about java.util.linkedlist). Even so, Dill seems +satisfied with my progress. Once we get the JVM model +(and the sets and maps books) stabilized, I should be +much more productive and should be able to totally +impress him. + +Thanks, +-Eric + + +__________________________________________________ +Do you Yahoo!? +Yahoo! Tax Center - forms, calculators, tips, more +http://taxes.yahoo.com/ + + + + +|# diff --git a/books/workshops/2004/sumners-ray/support/total-order.lisp b/books/workshops/2004/sumners-ray/support/total-order.lisp new file mode 100644 index 0000000..519325a --- /dev/null +++ b/books/workshops/2004/sumners-ray/support/total-order.lisp @@ -0,0 +1,30 @@ +;; total-order.lisp + +(in-package "ACL2") + +(defun << (x y) + (and (lexorder x y) + (not (equal x y)))) + +(defthm <<-irreflexive + (not (<< x x))) + +(defthm <<-transitive + (implies (and (<< x y) + (<< y z)) + (<< x z))) + +(defthm <<-asymmetric + (implies (<< x y) + (not (<< y x)))) + +(defthm <<-trichotomy + (implies (and (not (<< y x)) + (not (equal x y))) + (<< x y))) + +(defthm <<-implies-lexorder + (implies (<< x y) + (lexorder x y))) + +(in-theory (disable <<)) |