Import acl2_7.4dfsg.orig.tar.gz

[dgit import orig acl2_7.4dfsg.orig.tar.gz]

13 files changed, 4811 insertions, 0 deletions

diff --git a/books/workshops/2000/manolios/pipeline/trivial/sawada-model/README b/books/workshops/2000/manolios/pipeline/trivial/sawada-model/README
new file mode 100644
index 0000000..efc9c72
--- /dev/null
+++ b/books/workshops/2000/manolios/pipeline/trivial/sawada-model/README
@@ -0,0 +1,43 @@
+The Verification Proof Script for the Three-Stage Pipelined Machine
+
+Author: Jun Sawada (sawada@cs.utexas.edu)
+
+1. Files in this Directory
+
+This directory contains the ACL2 books that define and verify the
+three-stage pipelined machine discussed in the book.
+There are three types of files: a makefile, files with the ".lisp"
+extension, and files with the ".acl2" extension.  The makefile is used 
+for the Unix make command.  The files with ".lisp" extension are ACL2
+books which includes the ACL2 functions and theorems.  The files with
+".acl2" extension are used during the certification process.
+
+
+Following is the list of files with the ".lisp" extension: 
+
+b-ops-aux-def.lisp:    Auxiliary definitions to the IHS library. 
+b-ops-aux.lisp:        Auxiliary theorems to the IHS library.
+basic-def.lisp:        The definitions of basic machine components.
+basic-lemmas.lisp:     Basic theorems about the pipelined machine.
+ihs.lisp:              Loads the IHS library and set the proper theory.
+model.lisp:            The definition of the three-stage pipelined machine.
+proof.lisp:            Proof of the commutative diagram. 
+table-def.lisp:        The definition of the intermediate abstraction MAETT.
+trivia.lisp:           Some trivial lemmas.
+utils.lisp:            Definitions of utility functions.
+
+
+How to re-certify the ACL2 book:
+
+1.  You may have to modify the paths to the ACL2 public libraries. At
+this moment, the ACL2 does not provide a uniform method to load ACL2
+public libraries whose absolute path names may vary.  For example, the
+IHS libraries are typically found in the "ihs" directory of the "book"
+directory of the root directory for the ACL2 source code, but the ACL2
+root directory is decided when it is installed.  If the load path to
+the public libraries are not set properly, the certification process
+fails.  You may have to change all the paths one-by-one.
+
+
+2 Run "make". 
+
diff --git a/books/workshops/2000/manolios/pipeline/trivial/sawada-model/b-ops-aux-def.lisp b/books/workshops/2000/manolios/pipeline/trivial/sawada-model/b-ops-aux-def.lisp
new file mode 100644
index 0000000..5f8a4ce
--- /dev/null
+++ b/books/workshops/2000/manolios/pipeline/trivial/sawada-model/b-ops-aux-def.lisp
@@ -0,0 +1,56 @@
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; b-ops-aux-def.lisp
+; This file contains definitions of auxiliary definition of bit operations.
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+(in-package "ACL2")
+
+;; [Jared] changed this book to just be an include of the identical book
+(include-book "workshops/1999/pipeline/b-ops-aux-def" :dir :system)
+
+;; (include-book "trivia")
+;; (include-book "ihs")
+
+;; (deflabel begin-b-ops-aux-def)
+
+;; ;; Bs-and takes arbitrary number of bits. It returns 1 if all
+;; ;; arguments are 1's, otherwise return 0.
+;; (defmacro bs-and (x y &rest rst)
+;;   (xxxjoin 'b-and (cons x (cons y rst))))
+
+;; ;; Bs-and takes arbitrary number of bits. It returns 1 if any
+;; ;; argument is 1, otherwise return 0.
+;; (defmacro bs-ior (x y &rest rst)
+;;   (xxxjoin 'b-ior (cons x (cons y rst))))
+
+;; ;; b1p returns T if x is 1, nil if x is 0.
+;; (defun b1p (x)
+;;   (declare (xargs :guard (bitp x)))
+;;   (not (zbp x)))
+
+;; ;; Bit if operation.
+;; (defmacro b-if (test a1 ax)
+;;   `(if (b1p ,test) ,a1 ,ax))
+
+;; ;; N-bit bit vector comparator.  If the least significant n-bit of
+;; ;; vectors x and y are equal, bv-eqv returns 1.
+;; (defun bv-eqv (n x y)
+;;   (declare (xargs :guard (and (integerp x) (integerp y)
+;; 			      (integerp n) (<= 0 n))))
+;;   (if (equal (loghead n x) (loghead n y)) 1 0))
+
+;; (defthm bitp-bv-eqv
+;;     (bitp (bv-eqv n x y)))
+
+;; (defthm bit-p-unsigned-byte-p-1
+;; 	     (implies (bitp x)
+;; 		      (unsigned-byte-p 1 x))
+;; 	   :hints (("Goal" :in-theory (enable unsigned-byte-p bitp))))
+
+;; ;; Note on disabled and enabled functions
+;; ;; All bit operations except for b-if are disabled.  We'd like to
+;; ;; deal with bit operations without opening them.  However, enabling
+;; ;; b-if allows the prover to examine cases automatically.
+
+;; (in-theory (disable b1p))
+;; (in-theory (disable bv-eqv))
diff --git a/books/workshops/2000/manolios/pipeline/trivial/sawada-model/b-ops-aux.lisp b/books/workshops/2000/manolios/pipeline/trivial/sawada-model/b-ops-aux.lisp
new file mode 100644
index 0000000..4854fdc
--- /dev/null
+++ b/books/workshops/2000/manolios/pipeline/trivial/sawada-model/b-ops-aux.lisp
@@ -0,0 +1,738 @@
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; b-ops-aux.lisp:
+;;  This file contains auxiliary lemmas to assist the IHS library
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+(in-package "ACL2")
+
+;; [Jared] changed this book to just be an include of the identical book
+(include-book "workshops/1999/pipeline/b-ops-aux" :dir :system)
+
+;; (include-book "b-ops-aux-def")
+
+;; (deflabel begin-b-ops-aux)
+
+;; ;; Type of b-if
+;; (defthm bitp-b-if
+;;     (implies (and (bitp y) (bitp z))
+;; 	     (bitp (b-if x y z)))
+;;   :hints (("goal" :in-theory (enable bitp))))
+
+;; (defthm integerp-b-if
+;;     (implies (and (integerp y) (integerp z))
+;; 	     (integerp (b-if x y z)))
+;;   :hints (("goal" :in-theory (enable bitp))))
+
+;; (defthm b-not-b-not
+;;     (equal (b-not (b-not i)) (bfix i))
+;;   :hints (("goal" :in-theory (enable b-not bfix zbp))))
+
+;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; ;; Here are several basic lemmas about bit operations.
+
+;; ;; If bit vector X is longer than (p+s), bits between the p'th and (p+s)'th
+;; ;; bits of the concatenation of x and y is equal to that of x.
+;; (defthm rdb-logapp-1
+;;     (implies (and (integerp x) (integerp y) (integerp i) (<= 0 i)
+;; 		  (integerp s) (<= 0 s) (integerp p) (<= 0 p)
+;; 		  (<= (+ s p) i))
+;; 	     (equal (rdb (cons s p) (logapp i x y))
+;; 		    (rdb (cons s p) x)))
+;;   :hints (("Goal" :in-theory (enable logapp* rdb bsp-size bsp-position))))
+
+;; ;; If bit vector X is shorter than p, bits from the p'th LSB to (p+s)'th
+;; ;; LSB of the concatenation of x and y is equal to that of y.
+;; (defthm rdb-logapp-2
+;;     (implies (and (integerp x) (integerp y)
+;; 		  (integerp s) (<= 0 s) (integerp p) (<= 0 p)
+;; 		  (integerp i) (<= 0 i)
+;; 		  (<= i p))
+;; 	     (equal (rdb (cons s p) (logapp i x y))
+;; 		    (rdb (cons s (- p i)) y)))
+;;   :hints (("Goal" :in-theory (enable logapp* rdb bsp-size bsp-position))))
+
+
+;; (defthm loghead-0
+;;     (equal (loghead x 0) 0)
+;;   :hints (("Goal" :in-theory (enable loghead))))
+
+;; (defthm loghead-1
+;;     (equal (loghead 1 vector) (logcar vector))
+;;   :hints (("Goal" :in-theory (enable logcar loghead))))
+
+;; (defthm logcar-bitp
+;;     (implies (bitp x)
+;; 	     (equal (logcar x) x))
+;;   :hints (("Goal" :in-theory (enable bitp logcar))))
+
+;; (defthm logbit-0-bitp
+;;     (implies (bitp x)
+;; 	     (equal (logbit 0 x) x))
+;;     :hints (("Goal" :in-theory (enable bitp logbit))))
+
+;; (defthm loghead-bitp
+;;     (implies (bitp x)
+;; 	     (equal (loghead 1 x) x))
+;;   :hints (("Goal" :in-theory (enable rdb))))
+
+
+;; (defthm logcons-0
+;;     (implies (bitp x)
+;; 	     (equal (logcons x 0) x))
+;;   :hints (("Goal" :in-theory (enable logcons))))
+
+;; (defthm rdb-bitp
+;;     (implies (bitp x)
+;; 	     (equal (rdb (cons 1 0) x) x))
+;;   :hints (("Goal" :in-theory (enable rdb))))
+
+;; (defthm rdb-0
+;;     (equal (rdb (cons 0 n) x) 0)
+;;   :hints (("Goal" :in-theory (enable rdb bsp-size))))
+
+;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; ;; Here begins a basic theory about lobops
+;; ; Recursive definition of Logbit*.
+;; (defthm logbit*
+;;     (implies (and (integerp pos)
+;; 		  (>= pos 0)
+;; 		  (integerp i))
+;; 	     (equal (logbit pos i)
+;; 		    (if (equal pos 0)
+;; 			(logcar i)
+;; 			(logbit (1- pos) (logcdr i)))))
+;;   :rule-classes :definition
+;;   :hints (("Goal" :in-theory (e/d (logbit logbitp*) (logbitp)))))
+
+;; (in-theory (disable logbit*))
+
+;; (local
+;; (defun logtail-induct (pos i)
+;;   (if (zp pos)
+;;       i
+;;       (logtail-induct (1- pos) (logcdr i)))))
+
+
+;; (defthm logcar-logtail
+;;     (implies (and (integerp n) (<= 0 n)
+;; 		  (integerp x))
+;; 	     (equal (logcar (logtail n x))
+;; 		    (logbit n x)))
+;;   :hints (("Goal" :in-theory (e/d (logtail* logbit logbitp*)
+;; 				  (logbitp))
+;; 		  :induct (logtail-induct n x))))
+
+;; (defthm logcdr-logtail
+;;     (implies (and (integerp n) (<= 0 n)
+;; 		  (integerp x))
+;; 	     (equal (logcdr (logtail n x))
+;; 		    (logtail (1+ n) x)))
+;;   :hints (("Goal" :in-theory (enable logtail*)
+;; 		    :induct (logtail-induct n x))))
+
+;; ;; The following two lemmas are for expansion before BDD
+;; (deflabel begin-bv-expand)
+;; (defthm rdb-expand
+;;    (implies (and (syntaxp (and (quoted-constant-p s) (quoted-constant-p n)))
+;; 		 (integerp s) (< 0 s)
+;; 		 (integerp n) (<= 0 n)
+;; 		 (integerp x))
+;; 	    (equal (rdb (cons s n) x)
+;; 		   (logcons (logbit n x) (rdb (cons (1- s) (1+ n)) x))))
+;;   :hints (("Goal" :in-theory (enable rdb bsp-position bsp-size loghead*
+;; 				     logtail*))))
+
+
+;; ;; logops supplement for logxxx operations. There are bunch of
+;; ;; definition rules logior* and so on, but they are definition rules.
+;; ;; We rewrite rules to forcibly open up the expressions before applying
+;; ;; BDD techniques.  We redefine the same lemma as a rewrite rule.
+;; (defthm open-logior-right-const
+;;     (implies (and (bitp i1)
+;; 		  (integerp i2)
+;; 		  (integerp j))
+;; 	     (equal (logior (logcons i1 i2) j)
+;; 		    (logcons (b-ior i1 (logcar j)) (logior i2 (logcdr j)))))
+;;   :hints (("Goal" :in-theory (enable logior*))))
+
+
+;; (defthm open-logior-left-const
+;;     (implies (and (bitp j1)
+;; 		  (integerp j2)
+;; 		  (integerp i))
+;; 	     (equal (logior i (logcons j1 j2))
+;; 		    (logcons (b-ior (logcar i) j1) (logior (logcdr i) j2))))
+;;   :hints (("Goal" :in-theory (enable logior*))))
+
+;; (defthm open-logior
+;;     (implies (and (bitp i1)
+;; 		  (bitp j1)
+;; 		  (integerp i2)
+;; 		  (integerp j2))
+;; 	     (equal (logior (logcons i1 i2) (logcons j1 j2))
+;; 		    (logcons (b-ior i1 j1) (logior i2 j2))))
+;;   :hints (("Goal" :in-theory (enable logior*))))
+
+;; (defthm open-logxor-right-const
+;;     (implies (and (bitp i1)
+;; 		  (integerp i2)
+;; 		  (integerp j))
+;; 	     (equal (logxor (logcons i1 i2) j)
+;; 		    (logcons (b-xor i1 (logcar j)) (logxor i2 (logcdr j)))))
+;;   :hints (("Goal" :in-theory (enable logxor*))))
+
+
+;; (defthm open-logxor-left-const
+;;     (implies (and (bitp j1)
+;; 		  (integerp j2)
+;; 		  (integerp i))
+;; 	     (equal (logxor i (logcons j1 j2))
+;; 		    (logcons (b-xor (logcar i) j1) (logxor (logcdr i) j2))))
+;;   :hints (("Goal" :in-theory (enable logxor*))))
+
+;; (defthm open-logxor
+;;     (implies (and (bitp i1)
+;; 		  (bitp j1)
+;; 		  (integerp i2)
+;; 		  (integerp j2))
+;; 	     (equal (logxor (logcons i1 i2) (logcons j1 j2))
+;; 		    (logcons (b-xor i1 j1) (logxor i2 j2))))
+;;   :hints (("Goal" :in-theory (enable logxor*))))
+
+
+
+
+;; (defthm open-logand-right-const
+;;     (implies (and (bitp i1)
+;; 		  (integerp i2)
+;; 		  (integerp j))
+;; 	     (equal (logand (logcons i1 i2) j)
+;; 		    (logcons (b-and i1 (logcar j)) (logand i2 (logcdr j)))))
+;;   :hints (("Goal" :in-theory (enable logand*))))
+
+
+;; (defthm open-logand-left-const
+;;     (implies (and (bitp j1)
+;; 		  (integerp j2)
+;; 		  (integerp i))
+;; 	     (equal (logand i (logcons j1 j2))
+;; 		    (logcons (b-and (logcar i) j1) (logand (logcdr i) j2))))
+;;   :hints (("Goal" :in-theory (enable logand*))))
+
+;; (defthm open-logand
+;;     (implies (and (bitp i1)
+;; 		  (bitp j1)
+;; 		  (integerp i2)
+;; 		  (integerp j2))
+;; 	     (equal (logand (logcons i1 i2) (logcons j1 j2))
+;; 		    (logcons (b-and i1 j1) (logand i2 j2))))
+;;   :hints (("Goal" :in-theory (enable logand*))))
+
+;; (defthm open-lognot
+;;     (implies (and (bitp i1)
+;; 		  (integerp i2))
+;; 	     (equal (lognot (logcons i1 i2))
+;; 		    (logcons (b-not i1) (lognot i2))))
+;;   :hints (("Goal" :in-theory (enable lognot*))))
+
+;; (defthm fold-logcdr-vector
+;;     (implies (and (integerp x)
+;; 		  (syntaxp (or (not (consp x))
+;; 			       (not (equal (car x) 'logcons$inline)))))
+;; 	     (equal (logcdr x) (logtail 1 x)))
+;;   :hints (("goal" :in-theory (enable logtail*))))
+;; (in-theory (disable fold-logcdr-vector))
+
+;; (defthm fold-logcar-vector
+;;     (implies (and (integerp x)
+;; 		  (syntaxp (or (not (consp x))
+;; 			       (not (equal (car x) 'logcons$inline)))))
+;; 	     (equal (logcar x) (logbit 0 x)))
+;;   :hints (("goal" :in-theory (enable logbit logbitp*))))
+;; (in-theory (disable fold-logcar-vector))
+;; (deflabel end-bv-expand)
+
+;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; ;; Bv-eqv rules
+;; (defthm bv-eqv*
+;;     (implies (and (integerp x)
+;; 		  (integerp y)
+;; 		  (integerp n)
+;; 		  (>= n 0))
+;; 	     (equal (bv-eqv n x y)
+;; 		    (if (zp n)
+;; 			1
+;; 			(b-and (b-eqv (logcar x) (logcar y))
+;; 			       (bv-eqv (1- n) (logcdr x) (logcdr y))))))
+;;   :hints (("goal" :in-theory (enable bv-eqv loghead*)))
+;;   :rule-classes :definition)
+
+;; (in-theory (disable bv-eqv*))
+
+;; ;; Following lemma is useful in converting a formula with 'bv-eqv' to one
+;; ;; with 'equal'.
+;; ;; This can cause BDD simplification to fail, especially if when the words
+;; ;; need to be open up.
+;; (defthm bv-eqv-iff-equal
+;;   (implies (and (unsigned-byte-p n x) (unsigned-byte-p n y))
+;; 	   (equal (b1p (bv-eqv n x y))
+;; 		  (equal x y)))
+;;   :hints (("Goal" :in-theory (enable bv-eqv b1p))))
+
+;; (defthm bv-eqv-0
+;;     (equal (bv-eqv 0 x y) 1)
+;;   :Hints (("Goal" :in-theory (enable bv-eqv))))
+
+;; (defthm bv-x-x
+;;     (equal (bv-eqv n x x) 1)
+;;   :hints (("goal" :in-theory (enable bv-eqv))))
+
+;; (defthm bv-eqv-assoc
+;;     (equal (bv-eqv n x y) (bv-eqv n y x))
+;;   :hints (("Goal" :in-theory (enable bv-eqv))))
+
+;; (defthm bv-eqv-bits
+;;     (implies (and (bitp x) (bitp y) (integerp n) (> n 0))
+;; 	     (equal (bv-eqv n x y) (b-eqv x y)))
+;;   :hints (("Goal" :in-theory (enable bv-eqv* bitp bv-eqv-iff-equal))))
+
+;; (defthm bv-eqv-expand
+;;     (implies (and (integerp x) (integerp y)
+;; 		  (integerp n) (> n 0)
+;; 		  (syntaxp (quoted-constant-p n)))
+;; 	     (equal (bv-eqv n x y)
+;; 		    (b-and (b-eqv (logcar x) (logcar y))
+;; 			   (bv-eqv (1- n) (logcdr x) (logcdr y)))))
+;;   :hints (("Goal" :in-theory (enable bv-eqv*))))
+
+;; ;; Following lemma is a schematic lemma which will be used in BDD proof.
+;; ;; We noticed that several lemmas is a tautology under the property that
+;; ;; (bv-eqv x y) and (bv-eqv x z) are not simultaneously asserted, if y and
+;; ;; z are not equal. We instantiate the following lemma and add it to BDD
+;; ;; proof as a hint.
+;; (defthm bv-eqv-transitivity
+;;     (implies (and (unsigned-byte-p n x)
+;; 		  (unsigned-byte-p n y)
+;; 		  (unsigned-byte-p n z)
+;; 		  (b1p (b-and (bv-eqv n x z) (bv-eqv n y z))))
+;; 	     (equal x y))
+;;   :hints (("Goal" :in-theory (enable bv-eqv )))
+;;   :rule-classes nil)
+
+;; ;; Bv-expander is the theory to be enabled to expand bit vectors before
+;; ;; applying bdd's.
+;; (deftheory bv-expander
+;;     '(rdb-expand
+;;       open-lognot
+;;       open-logand open-logand-right-const open-logand-left-const
+;;       open-logior open-logior-right-const open-logior-left-const
+;;       open-logxor open-logxor-right-const open-logxor-left-const
+;;       fold-logcar-vector fold-logcdr-vector
+;;       bv-eqv-bits
+;;       bv-eqv-0
+;;       bv-eqv-expand))
+
+;; (in-theory (disable bv-expander))
+
+;; (local (in-theory (enable b1p)))
+
+;; ;; Bit-boolean-converter converting expressions of form (equal x 1) to
+;; ;; expressions using bitp, lest BDD package assigns different boolean values
+;; ;; to (b1p x) and (equal x 1).  It also converts (equal x 0) to (not (b1p x)).
+;; (defthm equal-to-1-to-b1p
+;;     (implies (bitp x)
+;; 	     (equal (equal x 1)
+;; 		    (b1p x)))
+;;   :Hints (("Goal" :In-theory (enable bitp))))
+
+;; (defthm equal-to-0-to-not-b1p
+;;     (implies (bitp x)
+;; 	     (equal (equal x 0)
+;; 		    (not (b1p x))))
+;;   :Hints (("Goal" :In-theory (enable bitp))))
+
+;; (defthm equal-to-b1p-b-eqv
+;;     (implies (and (bitp x) (bitp y))
+;; 	     (equal (equal x y) (b1p (b-eqv x y))))
+;;   :hints (("Goal" :in-theory (enable b-eqv b1p zbp bitp))))
+
+;; (deftheory equal-b1p-converter
+;;     '(equal-to-1-to-b1p equal-to-0-to-not-b1p))
+
+;; (in-theory (disable equal-b1p-converter))
+;; (in-theory (disable  equal-to-b1p-b-eqv))
+
+;; ;; From here, we define bit-to-boolean converter, especially for BDD
+;; ;; operation.
+;; (deflabel begin-lift-b-ops)
+
+;; (defthm zbp-b-and
+;;     (equal (zbp (b-and x y))
+;; 	   (or (zbp x) (zbp y)))
+;;   :Hints (("Goal" :in-theory (enable b-and))))
+
+;; (defthm zbp-b-ior
+;;     (equal (zbp (b-ior x y))
+;; 	   (and (zbp x) (zbp y)))
+;;   :Hints (("Goal" :in-theory (enable b-ior))))
+
+;; (defthm zbp-b-xor
+;;     (equal (zbp (b-xor x y))
+;; 	   (or (and (zbp x) (zbp y))
+;; 	       (and (not (zbp x)) (not (zbp y)))))
+;;   :Hints (("Goal" :in-theory (enable b-xor))))
+
+;; (defthm zbp-b-not
+;;     (equal (zbp (b-not x))
+;; 	   (not (zbp x)))
+;;   :Hints (("Goal" :in-theory (enable b-not))))
+
+;; (defthm zbp-b-eqv
+;;     (equal (zbp (b-eqv x y))
+;; 	   (not (iff (zbp x) (zbp y))))
+;;   :Hints (("Goal" :in-theory (enable b-eqv))))
+
+
+
+;; (defthm b1p-b-and
+;;     (equal (b1p (b-and x y))
+;; 	   (and (b1p x) (b1p y)))
+;;   :Hints (("Goal" :in-theory (enable b-and))))
+
+;; (defthm b1p-b-ior
+;;     (equal (b1p (b-ior x y))
+;; 	   (or (b1p x) (b1p y)))
+;;   :Hints (("Goal" :in-theory (enable b-ior))))
+
+;; (defthm b1p-b-xor
+;;     (equal (b1p (b-xor x y))
+;; 	   (or (and (b1p x) (not (b1p y)))
+;; 	       (and (not (b1p x)) (b1p y))))
+;;   :Hints (("Goal" :in-theory (enable b-xor))))
+
+;; (defthm b1p-b-not
+;;     (equal (b1p (b-not x))
+;; 	   (not (b1p x)))
+;;   :Hints (("Goal" :in-theory (enable b-not))))
+
+;; (defthm b1p-b-eqv
+;;     (equal (b1p (b-eqv x y))
+;; 	   (iff (b1p x) (b1p y)))
+;;   :Hints (("Goal" :in-theory (enable b-eqv))))
+
+;; (defthm b1p-nand (equal (b1p (b-nand x y)) (not (and (b1p x) (b1p y))))
+;;   :hints (("Goal" :in-theory (enable b-nand))))
+
+;; (defthm b1p-nor (equal (b1p (b-nor x y)) (not (or (b1p x) (b1p y))))
+;;     :hints (("Goal" :in-theory (enable b-nor))))
+
+;; (defthm b1p-andc1 (equal (b1p (b-andc1 x y)) (and (not (b1p x)) (b1p y)))
+;;   :hints (("Goal" :in-theory (enable b-andc1))))
+
+;; (defthm b1p-andc2 (equal (b1p (b-andc2 x y)) (and (b1p x) (not (b1p y))))
+;;   :hints (("Goal" :in-theory (enable b-andc2))))
+
+;; (defthm b1p-orc1 (equal (b1p (b-orc1 x y)) (or (not (b1p x)) (b1p y)))
+;;   :hints (("Goal" :in-theory (enable b-orc1))))
+
+;; (defthm b1p-orc2 (equal (b1p (b-orc2 x y)) (or (b1p x) (not (b1p y))))
+;;   :hints (("Goal" :in-theory (enable b-orc2))))
+
+;; (defthm zbp-to-b1p
+;;     (equal (zbp x) (not (b1p x)))
+;;   :hints (("Goal" :in-theory (enable b1p))))
+
+;; (deflabel end-lift-b-ops)
+
+;; (deftheory lift-b-ops
+;;     (set-difference-theories (universal-theory 'end-lift-b-ops)
+;; 			     (universal-theory 'begin-lift-b-ops)))
+
+;; (in-theory (disable lift-b-ops))
+
+;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; ; New Simplifier
+;; ; This simplifier simplifies bit terms into 1 and 0's using information
+;; ; represented by b1p.
+;; ; Origianl Simplify-Bit-Functions can simplify expressions with bit-functions
+;; ; if its arguments are 0 or 1's.  For instance, it can reduce expressions
+;; ; with a rule like:
+;; ;  (EQUAL (B-AND 1 X) (BFIX X))
+;; ; In the new simplifier reduces the expressions if hypothesis satisfies
+;; ; certain conditions, like
+;; ;	 (implies (and (bitp x) (bitp y) (not (b1p y)))
+;; ;		  (equal (b-and x y) 0))
+;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; (deflabel begin-b1p-bit-rewriter)
+
+;; (defthm b1p-bit-forward
+;;     (implies (and (b1p b) (force (bitp b))) (equal b 1))
+;;   :hints (("goal" :in-theory (enable b1p bitp zbp)))
+;;   :rule-classes :forward-chaining)
+
+;; (defthm not-b1p-bit-forward
+;;     (implies (and (not (b1p b)) (force (bitp b))) (equal b 0))
+;;   :hints (("goal" :in-theory (enable b1p bitp zbp)))
+;;   :rule-classes :forward-chaining)
+
+;; (defthm simplify-bit-functions-2
+;;     (and (implies (and (bitp x) (bitp y) (not (b1p x)))
+;; 		  (equal (b-and x y) 0))
+;; 	 (implies (and (bitp x) (bitp y) (not (b1p y)))
+;; 		  (equal (b-and x y) 0))
+;; 	 (implies (and (bitp x) (bitp y) (b1p x))
+;; 		  (equal (b-and x y) y))
+;; 	 (implies (and (bitp x) (bitp y) (b1p y))
+;; 		  (equal (b-and x y) x))
+
+;; 	 (implies (and (bitp x) (bitp y) (not (b1p x)))
+;; 		  (equal (b-ior x y) y))
+;; 	 (implies (and (bitp x) (bitp y) (not (b1p y)))
+;; 		  (equal (b-ior x y) x))
+;; 	 (implies (and (bitp x) (bitp y) (b1p x))
+;; 		  (equal (b-ior x y) 1))
+;; 	 (implies (and (bitp x) (bitp y) (b1p y))
+;; 		  (equal (b-ior x y) 1))
+
+;; 	 (implies (and (bitp x) (bitp y) (not (b1p x)))
+;; 		  (equal (b-xor x y) y))
+;; 	 (implies (and (bitp x) (bitp y) (not (b1p y)))
+;; 		  (equal (b-xor x y) x))
+;; 	 (implies (and (bitp x) (bitp y) (b1p x))
+;; 		  (equal (b-xor x y) (b-not y)))
+;; 	 (implies (and (bitp x) (bitp y) (b1p y))
+;; 		  (equal (b-xor x y) (b-not x)))
+
+;; 	 (implies (and (bitp x) (bitp y) (not (b1p x)))
+;; 		  (equal (b-eqv x y) (b-not y)))
+;; 	 (implies (and (bitp x) (bitp y) (not (b1p y)))
+;; 		  (equal (b-eqv x y) (b-not x)))
+;; 	 (implies (and (bitp x) (bitp y) (b1p x))
+;; 		  (equal (b-eqv x y) y))
+;; 	 (implies (and (bitp x) (bitp y) (b1p y))
+;; 		  (equal (b-eqv x y) x))
+
+;; 	 (implies (and (bitp x) (bitp y) (not (b1p x)))
+;; 		  (equal (b-nand x y) 1))
+;; 	 (implies (and (bitp x) (bitp y) (not (b1p y)))
+;; 		  (equal (b-nand x y) 1))
+;; 	 (implies (and (bitp x) (bitp y) (b1p x))
+;; 		  (equal (b-nand x y) (b-not y)))
+;; 	 (implies (and (bitp x) (bitp y) (b1p y))
+;; 		  (equal (b-nand x y) (b-not x)))
+
+;; 	 (implies (and (bitp x) (bitp y) (not (b1p x)))
+;; 		  (equal (b-nor x y) (b-not y)))
+;; 	 (implies (and (bitp x) (bitp y) (not (b1p y)))
+;; 		  (equal (b-nor x y) (b-not x)))
+;; 	 (implies (and (bitp x) (bitp y) (b1p x))
+;; 		  (equal (b-nor x y) 0))
+;; 	 (implies (and (bitp x) (bitp y) (b1p y))
+;; 		  (equal (b-nor x y) 0))
+
+;; 	 (implies (and (bitp x) (bitp y) (not (b1p x)))
+;; 		  (equal (b-andc1 x y) y))
+;; 	 (implies (and (bitp x) (bitp y) (not (b1p y)))
+;; 		  (equal (b-andc1 x y) 0))
+;; 	 (implies (and (bitp x) (bitp y) (b1p x))
+;; 		  (equal (b-andc1 x y) 0))
+;; 	 (implies (and (bitp x) (bitp y) (b1p y))
+;; 		  (equal (b-andc1 x y) (b-not x)))
+
+;; 	 (implies (and (bitp x) (bitp y) (not (b1p x)))
+;; 		  (equal (b-andc2 x y) 0))
+;; 	 (implies (and (bitp x) (bitp y) (not (b1p y)))
+;; 		  (equal (b-andc2 x y) x))
+;; 	 (implies (and (bitp x) (bitp y) (b1p x))
+;; 		  (equal (b-andc2 x y) (b-not y)))
+;; 	 (implies (and (bitp x) (bitp y) (b1p y))
+;; 		  (equal (b-andc2 x y) 0))
+
+;; 	 (implies (and (bitp x) (bitp y) (not (b1p x)))
+;; 		  (equal (b-orc1 x y) 1))
+;; 	 (implies (and (bitp x) (bitp y) (not (b1p y)))
+;; 		  (equal (b-orc1 x y) (b-not x)))
+;; 	 (implies (and (bitp x) (bitp y) (b1p x))
+;; 		  (equal (b-orc1 x y) y))
+;; 	 (implies (and (bitp x) (bitp y) (b1p y))
+;; 		  (equal (b-orc1 x y) 1))
+
+;; 	 (implies (and (bitp x) (bitp y) (not (b1p x)))
+;; 		  (equal (b-orc2 x y) (b-not y)))
+;; 	 (implies (and (bitp x) (bitp y) (not (b1p y)))
+;; 		  (equal (b-orc2 x y) 1))
+;; 	 (implies (and (bitp x) (bitp y) (b1p x))
+;; 		  (equal (b-orc2 x y) 1))
+;; 	 (implies (and (bitp x) (bitp y) (b1p y))
+;; 		  (equal (b-orc2 x y) x)))
+;;   :hints (("Goal" :in-theory (enable b1p zbp b-and bitp))))
+
+;; (deflabel end-b1p-bit-rewriter)
+
+;; (deftheory b1p-bit-rewriter
+;;     (set-difference-theories (universal-theory 'end-b1p-bit-rewriter)
+;; 			     (universal-theory 'begin-b1p-bit-rewriter)))
+
+;; (in-theory (disable b1p-bit-rewriter))
+;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; ; BDD helps
+;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; (deftheory pre-bdd-disables
+;;     '(bv-eqv-iff-equal simplify-bit-functions))
+
+;; (deftheory bdd-disables
+;;     '(bv-eqv-iff-equal simplify-bit-functions))
+
+;; (theory-invariant (incompatible (:rewrite bv-eqv-iff-equal)
+;; 				(:rewrite rdb-expand)))
+
+;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; ; range of unsigned-byte-p
+;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; ; theories about the range of unsigned-byte-p
+;; (defthm plus-unsigned-byte-p-lt-2-*-expt-2-width
+;;     (implies (and (unsigned-byte-p width val1)
+;; 		  (unsigned-byte-p width val2))
+;; 	     (< (+ val1 val2) (* 2 (expt 2 width))))
+;;   :hints (("goal" :in-theory (enable unsigned-byte-p))))
+
+;; (defun logbit-induction (pos val)
+;;     (if (zp pos)
+;; 	val
+;; 	(logbit-induction (1- pos) (logcdr val))))
+
+;; ; If a value are in the range  0 <= val < 2^width
+;; ; then the width'th bit of val is not set.
+;; (defthm logbit-0-if-val-lt-expt-2-width
+;;     (implies (and (integerp width) (<= 0 width)
+;; 		  (integerp val)
+;; 		  (<= 0 val) (< val (expt 2 width)))
+;; 	     (equal (logbit width val) 0))
+;;   :hints (("goal" :in-theory (e/d (logbit* expt logcar logcdr)
+;; 				  (exponents-add))
+;; 		  :induct (logbit-induction width val)))
+;;   :rule-classes nil)
+
+
+;; (encapsulate nil
+;; (local
+;;  (defthm logbit-1-if-val-gt-expt-2-width-help1
+;;      (IMPLIES (AND (INTEGERP WIDTH)
+;; 		   (< 0 WIDTH)
+;; 		   (INTEGERP VAL)
+;; 		   (<= (* 2 (EXPT 2 (+ -1 WIDTH))) VAL)
+;; 		   (< (/ VAL 2) (* 2 (EXPT 2 (+ -1 WIDTH)))))
+;; 	      (> (* 2 (EXPT 2 (+ -1 WIDTH)))
+;; 		 (FLOOR VAL 2)))
+;;  :rule-classes nil))
+
+;; (local
+;;  (defthm logbit-1-if-val-gt-expt-2-width-help2
+;;      (implies  (and (integerp val)
+;; 		    (integerp width) (< 0 width)
+;; 		    (< VAL (* 2 2 (EXPT 2 (+ -1 WIDTH)))))
+;; 	       (< (/ VAL 2) (* 2 (EXPT 2 (+ -1 WIDTH)))))
+;;    :hints (("goal" :in-theory (e/d (expt) (exponents-add))))
+;;    :rule-classes nil))
+
+;; (local
+;; (defthm logbit-1-if-val-gt-expt-2-width-help
+;;     (IMPLIES (AND (INTEGERP WIDTH)
+;; 		  (INTEGERP VAL)
+;; 		  (< 0 WIDTH)
+;; 		  (<= (* 2 (EXPT 2 (+ -1 WIDTH))) (FLOOR VAL 2)))
+;; 	     (<= (* 2 2 (EXPT 2 (+ -1 WIDTH))) VAL))
+;;   :hints (("goal" :in-theory (e/d (exponents-add) (expt))
+;; 		  :use ((:instance logbit-1-if-val-gt-expt-2-width-help1)
+;; 			(:instance logbit-1-if-val-gt-expt-2-width-help2))))))
+
+
+;; ; If a value are in the range  2^width <= val < 2^width * 2,
+;; ; then the width'th bit of val is set.
+;; (defthm logbit-1-if-val-gt-expt-2-width
+;;     (implies (and (integerp width) (<= 0 width)
+;; 		  (integerp val)
+;; 		  (<= (expt 2 width) val)
+;; 		  (< val (* 2 (expt 2 width))))
+;; 	     (equal (logbit width val) 1))
+;;   :hints (("goal" :in-theory (e/d (logbit* expt logcar logcdr)
+;; 				  (exponents-add))
+;; 		  :induct (logbit-induction width val)))
+;;   :rule-classes nil)
+;; )
+
+;; ; Suppose val1 and val2 are unsigned-byte-p whose width is w.
+;; ; If w'th bit of the sum (+ val1 val2) is not set,
+;; ; (+ val1 val2) < 2^w.
+;; (defthm plus-unsigned-byte-lt-expt-2-width-if-logbit
+;;     (implies (and (unsigned-byte-p width val1)
+;; 		  (unsigned-byte-p width val2)
+;; 		  (not (b1p (logbit width (+ val1 val2)))))
+;; 	     (< (+ val1 val2) (expt 2 width)))
+;;   :hints (("goal" :in-theory (enable unsigned-byte-p)
+;; 		  :use (:instance logbit-1-if-val-gt-expt-2-width
+;; 				  (val (+ val1 val2))))))
+
+
+
+;; ; Suppose val1 and val2 are unsigned-byte-p whose width is w.
+;; ; If w'th bit of the sum (+ val1 val2) is set, then
+;; ;   2^w < (+ val1 val2).
+;; (defthm plus-unsigned-byte-gt-expt-2-width-if-logbit
+;;     (implies (and (unsigned-byte-p width val1)
+;; 		  (unsigned-byte-p width val2)
+;; 		  (b1p (logbit width (+ val1 val2))))
+;; 	     (<= (expt 2 width) (+ val1 val2)))
+;;   :hints (("goal" :in-theory (enable unsigned-byte-p)
+;; 		  :use (:instance logbit-0-if-val-lt-expt-2-width
+;; 				  (val (+ val1 val2))))))
+
+;; ; Suppose val1 and val2 are unsigned-byte-p whose width is w.
+;; ; If the sum of val1 and val2 does not carry out to w'th bit,
+;; ;  (loghead w (+ val1 val2)) = (+ val1 val2)
+;; (defthm loghead-unsigned-byte-+-if-not-carry
+;;     (implies (and (integerp width)
+;; 		  (<= 0 width)
+;; 		  (unsigned-byte-p width val1)
+;; 		  (unsigned-byte-p width val2)
+;; 		  (not (b1p (logbit width (+ val1 val2)))))
+;; 	     (equal (loghead width (+ val1 val2)) (+ val1 val2)))
+;;   :hints (("goal" :in-theory (enable loghead)
+;; 		  :do-not-induct t)))
+
+;; (encapsulate nil
+;; (local
+;; (defthm j*k-ge-2*k-if-j-gt-1
+;;     (implies (and (integerp j)
+;; 		  (< 1 j)
+;; 		  (integerp k)
+;; 		  (< 0 k))
+;; 	     (<= (* 2 k) (* j k)))
+;;   :hints (("Goal" :in-theory (enable <-*-right-cancel)))
+;;   :rule-classes :linear))
+
+;; ; A trivia theorem.
+;; ; If y < x < 2*y, then (x mod y) = x - y
+;; (defthm mod-x-y-=-minux-x-y
+;;  (implies (and (integerp x) (integerp y) (< 0 y)
+;; 	       (<= y x) (< x (* 2 y)))
+;; 	  (equal (mod x y) (- x y)))
+;;  :Hints (("goal" :in-theory (disable (:generalize floor-bounds)))
+;; 	 ("subgoal 1" :cases ((<= j 1)))))
+;; )
+
+;; (in-theory (disable mod-x-y-=-minux-x-y))
+
+;; ; Suppose val1 and val2 are unsigned-byte-p whose width is w.
+;; ; If the sum of val1 and val2 does not carry out to w'th bit,
+;; ;  (loghead w (+ val1 val2)) = (+ val1 val2)
+;; (defthm loghead-unsigned-byte-+-if-carry
+;;     (implies (and (integerp width)
+;; 		  (<= 0 width)
+;; 		  (unsigned-byte-p width val1)
+;; 		  (unsigned-byte-p width val2)
+;; 		  (b1p (logbit width (+ val1 val2))))
+;; 	     (equal (loghead width (+ val1 val2))
+;; 		    (- (+ val1 val2) (expt 2 width))))
+;;   :hints (("goal" :in-theory (enable loghead mod-x-y-=-minux-x-y)
+;; 		  :do-not-induct t)))
diff --git a/books/workshops/2000/manolios/pipeline/trivial/sawada-model/basic-def.acl2 b/books/workshops/2000/manolios/pipeline/trivial/sawada-model/basic-def.acl2
new file mode 100644
index 0000000..923cb2f
--- /dev/null
+++ b/books/workshops/2000/manolios/pipeline/trivial/sawada-model/basic-def.acl2
@@ -0,0 +1,4 @@
+(in-package "ACL2")
+(include-book "data-structures/portcullis" :dir :system)
+(certify-book "basic-def" ? t)
+
diff --git a/books/workshops/2000/manolios/pipeline/trivial/sawada-model/basic-def.lisp b/books/workshops/2000/manolios/pipeline/trivial/sawada-model/basic-def.lisp
new file mode 100644
index 0000000..347ddf7
--- /dev/null
+++ b/books/workshops/2000/manolios/pipeline/trivial/sawada-model/basic-def.lisp
@@ -0,0 +1,963 @@
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; Basic-def.lisp:
+; Copyright reserved by SRC
+; Author  Jun Sawada, University of Texas at Austin
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;'
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; This file includes various underlying definition for ISA and
+;; MA designs.
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+(in-package "ACL2")
+
+(include-book "../../../../../../data-structures/array1")
+(include-book "../../../../../../data-structures/deflist")
+(include-book "../../../../../../data-structures/list-defthms")
+(include-book "../../../../../../data-structures/structures")
+(include-book "ihs")
+
+(include-book "trivia")
+(include-book "b-ops-aux")
+
+(deflabel begin-basic-def)
+
+(defconst *addr-size* 16)
+(defconst *page-offset-size* 10)
+
+(defconst *rname-size* 4)
+(defconst *immediate-size* 8)
+(defconst *opcode-size* 4)
+(defconst *word-size* 16)
+(defconst *max-word-value* (expt 2 *word-size*))
+(defconst *num-regs* (expt 2 *rname-size*))
+(defconst *num-mem-words* (expt 2 *addr-size*))
+(defconst *num-page-words* (expt 2 *page-offset-size*))
+(defconst *num-pages* (expt 2 (- *addr-size* *page-offset-size*)))
+(defbytetype word *word-size* :unsigned)
+(defbytetype addr  *addr-size* :unsigned)
+(defbytetype rname *rname-size* :unsigned)
+(defbytetype immediate *immediate-size* :unsigned)
+(defbytetype opcd  *opcode-size* :unsigned)
+
+(defthm word-p-type
+    (implies (word-p word)
+	     (and (integerp word)
+		  (>= word 0)
+		  (< word *max-word-value*)))
+  :hints (("Goal" :in-theory (enable word-p)))
+  :rule-classes :forward-chaining)
+
+(defthm rname-p-type
+    (implies (rname-p rname)
+	     (and (integerp rname)
+		  (>= rname 0)
+		  (< rname *num-regs*)))
+  :hints (("Goal" :in-theory (enable rname-p)))
+  :rule-classes :forward-chaining)
+
+(defthm addr-p-type
+    (implies (addr-p ad)
+	     (and (integerp ad)
+		  (>= ad  0)
+		  (< ad *num-mem-words*)))
+ :hints (("Goal" :in-theory (enable addr-p)))
+  :rule-classes :forward-chaining)
+
+(defthm addr-word-double-casting
+    (equal (addr (word i)) (addr i))
+  :hints (("goal" :in-theory (enable addr word))))
+
+(defthm word-addr-double-casting
+    (equal (word (addr i)) (word i))
+  :hints (("goal" :in-theory (enable addr word))))
+
+
+(defthm word-addr-p
+    (implies (addr-p x) (equal (word x) x))
+  :hints (("goal" :in-theory (enable addr-p word))))
+
+(defthm addr-word-p
+    (implies (word-p x) (equal (addr x) x))
+  :hints (("goal" :in-theory (enable addr word-p))))
+
+(in-theory (disable word-addr-p addr-word-p))
+
+(defthm word-p-logand
+    (implies (and (word-p val1) (word-p val2))
+	     (word-p (logand val1 val2)))
+  :hints (("Goal" :in-theory (enable word-p))))
+
+(defthm word-p-logxor
+    (implies (and (word-p val1) (word-p val2))
+	     (word-p (logxor val1 val2)))
+  :hints (("Goal" :in-theory (enable word-p))))
+
+(defthm word-p-logior
+    (implies (and (word-p val1) (word-p val2))
+	     (word-p (logior val1 val2)))
+  :hints (("Goal" :in-theory (enable word-p))))
+
+(defthm word-p-bv-eqv-iff-equal
+    (implies (and (word-p wd0) (word-p wd1))
+	     (equal (b1p (bv-eqv *word-size* wd0 wd1)) (equal wd0 wd1)))
+  :hints (("Goal" :in-theory (enable word-p))))
+
+(defthm addr-p-bv-eqv-iff-equal
+    (implies (and (addr-p wd0) (addr-p wd1))
+	     (equal (b1p (bv-eqv *addr-size* wd0 wd1)) (equal wd0 wd1)))
+  :hints (("Goal" :in-theory (enable addr-p))))
+
+(defthm rname-p-bv-eqv-iff-equal
+    (implies (and (rname-p wd0) (rname-p wd1))
+	     (equal (b1p (bv-eqv *rname-size* wd0 wd1)) (equal wd0 wd1)))
+  :hints (("Goal" :in-theory (enable rname-p))))
+
+(defthm immediate-p-bv-eqv-iff-equal
+    (implies (and (immediate-p wd0) (immediate-p wd1))
+	     (equal (b1p (bv-eqv *immediate-size* wd0 wd1)) (equal wd0 wd1)))
+  :hints (("Goal" :in-theory (enable immediate-p))))
+
+(defthm opcd-p-bv-eqv-iff-equal
+    (implies (and (opcd-p wd0) (opcd-p wd1))
+	     (equal (b1p (bv-eqv *opcode-size* wd0 wd1)) (equal wd0 wd1)))
+  :hints (("Goal" :in-theory (enable opcd-p))))
+
+
+(deflist word-listp (l)
+  (declare (xargs :guard t))
+  word-p)
+
+(defun fixlen-word-listp (n lst)
+  "test if list is a array of n words."
+  (declare (xargs :guard (and (integerp n) (<= 0 n))))
+  (and (word-listp lst) (equal (len lst) n)))
+
+(defthm fixlen-word-true-listp
+    (implies (fixlen-word-listp n x)
+	     (true-listp x))
+  :rule-classes :forward-chaining)
+
+(in-theory (disable fixlen-word-listp))
+
+; Register file is a fixed lenghth true list of words.
+(defun regs-p (regs)
+  (declare (xargs :guard t))
+  (fixlen-word-listp *num-regs* regs))
+
+(defthm regs-p-true-listp
+    (implies (regs-p x)
+	     (true-listp x))
+  :rule-classes :forward-chaining)
+
+
+(defun read-reg (num regs)
+  (declare (xargs :guard (and (rname-p num) (regs-p regs))))
+  (nth num regs))
+
+(defun write-reg (val num regs)
+  (declare (xargs :guard (and (word-p val) (rname-p num) (regs-p regs))))
+  (update-nth num val regs))
+
+(defthm regs-p-write-reg
+    (implies (and (word-p word)
+		  (rname-p rname)
+		  (regs-p regs))
+	     (regs-p (write-reg word rname regs)))
+  :hints (("Goal" :in-theory (enable regs-p fixlen-word-listp
+				     rname-p UNSIGNED-BYTE-P
+				     len-update-nth))))
+
+(local
+(defthm nth-content-word-listp
+    (implies (and (integerp n)
+		  (<= 0 n)
+		  (word-listp lst)
+		  (< n (len lst)))
+	     (and (integerp (nth n lst))
+		  (acl2-numberp (nth n lst))))
+  :hints (("Goal" :use ((:instance word-listp-nth (n0 n) (l lst)))
+		  :in-theory (disable word-listp-nth)))))
+
+
+(defthm numberp-read-reg
+    (implies (and (regs-p regs)
+		  (rname-p rname))
+	     (and (integerp (read-reg rname regs))
+		  (acl2-numberp (read-reg rname regs))))
+  :hints (("Goal" :in-theory (enable rname-p regs-p fixlen-word-listp)))
+  :rule-classes
+  ((:type-prescription) (:rewrite)))
+
+(defthm word-p-read-reg
+    (implies (and (regs-p regs)
+		  (rname-p rname))
+	     (word-p (read-reg rname regs)))
+  :hints (("Goal" :in-theory (enable rname-p regs-p fixlen-word-listp)))
+  :rule-classes
+  ((:rewrite)
+   (:type-prescription :corollary
+	     (implies (and (regs-p regs) (rname-p rname))
+		      (integerp (read-reg rname regs)))
+	     :hints (("goal" :in-theory (enable word-p unsigned-byte-p))))))
+
+(defthm read-reg-write-reg
+    (implies (and (rname-p rn1)
+		  (rname-p rn2)
+		  (regs-p regs))
+	     (equal (read-reg rn1 (write-reg val rn2 regs))
+		    (if (equal rn1 rn2) val (read-reg rn1 regs))))
+  :hints (("Goal" :in-theory (enable read-reg write-reg regs-p
+				     nth-update-nth))))
+
+(in-theory (disable regs-p write-reg read-reg))
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; Here we define the memory system.
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+(defconst *no-access* 0)
+(defconst *read-only* 1)
+(defconst *read-write* 2)
+
+;;  Definition of Address Transformer
+;;  page-num Address --> Page number
+;;  page-offset Address --> Page Offset
+(defun page-num (addr)
+  (declare (xargs :guard (addr-p addr)))
+  (floor addr *num-page-words*))
+
+(defun page-offset (addr)
+  (declare (xargs :guard (addr-p addr)))
+  (mod addr *num-page-words*))
+
+(defthm page-num-type
+    (implies (addr-p addr)
+	     (and (integerp (page-num addr))
+		  (<= 0 (page-num addr))))
+  :rule-classes :type-prescription)
+
+(defthm page-num-bound
+    (implies (addr-p addr)
+	     (< (page-num addr) *num-pages*))
+  :hints (("Goal" :in-theory (enable addr-p unsigned-byte-p)))
+  :rule-classes :linear)
+
+(defthm page-offset-type
+    (implies (addr-p addr)
+	     (and (integerp (page-offset addr))
+		  (<= 0 (page-offset addr))))
+  :rule-classes :type-prescription)
+
+(defthm page-offset-bound
+    (implies (addr-p addr)
+	     (< (page-offset addr) *num-page-words*))
+  :rule-classes :linear)
+
+(in-theory (disable page-num page-offset))
+;;  End of Address Transformer
+
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; Definition of Memory Object
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; Check if page is an array representing a page.
+; Addr does not affect the value, but if the correct page tag is given,
+; execution is faster.
+(defun word-array-p (array)
+  (declare (xargs :guard (alistp array)
+		  :verify-guards nil))
+  (cond ((endp array) t)
+	((equal (caar array) ':header) (word-array-p (cdr array)))
+	(t (and (word-p (cdar array))
+		(word-array-p (cdr array))))))
+
+(verify-guards word-array-p
+	       :hints (("Goal" :in-theory (enable alistp))))
+
+(defun page-array-p (tag page-array)
+  (declare (xargs :guard t))
+  (and (array1p tag page-array)
+       (equal (car (dimensions tag page-array)) *num-page-words*)
+       (word-p (default tag page-array))
+       (word-array-p page-array)))
+
+(defstructure page
+  (tag (:assert (symbolp tag) :rewrite))
+  (mode (:assert (integerp mode) :rewrite))
+  (array (:assert (page-array-p tag array) :rewrite))
+  (:options :guards))
+
+(defun mem-array-p (array)
+  (declare (xargs :guard (alistp array)
+		  :verify-guards nil))
+  (cond ((endp array) t)
+	((equal (caar array) ':header) (mem-array-p (cdr array)))
+	(t (and (let ((page (cdar array)))
+		  (if (integerp page)
+		      (or (equal page *no-access*) (equal page *read-only*)
+			  (equal page *read-write*))
+		      (page-p page)))
+		(mem-array-p (cdr array))))))
+
+(verify-guards mem-array-p :hints (("Goal" :in-theory (enable alistp))))
+
+(defun mem-p (mem)
+  (declare (xargs :guard t))
+  (and (array1p 'mem mem)
+       (equal (car (dimensions 'mem mem)) *num-pages*)
+       (equal (default 'mem mem) *no-access*)
+       (mem-array-p mem)))
+
+(in-theory (disable word-array-p page-array-p mem-array-p mem-p))
+
+(defthm page-p-type
+    (implies (page-p p)
+	     (consp p))
+  :hints (("Goal" :in-theory (enable page-p)))
+  :rule-classes :compound-recognizer)
+
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;  Definition of Read-mem
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+(defmacro get-page (n mem)
+  `(aref1 'mem ,mem ,n))
+
+(defmacro set-page (page n mem)
+  `(aset1 'mem ,mem ,n ,page))
+
+(defun read-page (offset page)
+  (declare (xargs :guard (and (page-p page)
+			      (integerp offset) (<= 0 offset)
+			      (< offset *num-page-words*))
+		  :verify-guards nil))
+  (aref1 (page-tag page) (page-array page) offset))
+
+
+(defun read-mem (addr mem)
+  (declare (xargs :guard (and (addr-p addr) (mem-p mem))
+		  :verify-guards nil))
+  (let ((page (get-page (page-num addr) mem)))
+    (if (integerp page)
+	0
+	(read-page (page-offset addr) page))))
+
+;(verify-guards get-page
+; :hints (("Goal" :in-theory (enable mem-p))))
+
+(verify-guards read-page
+  :hints (("Goal" :in-theory (enable page-p page-array-p))))
+
+(encapsulate nil
+(local
+ (defthm page-p-assoc-mem-array
+     (implies (and (mem-array-p mem)
+		   (integerp pn)
+		   (assoc pn mem)
+		   (not (integerp (cdr (assoc pn mem)))))
+	      (page-p (cdr (assoc pn mem))))
+   :hints (("Goal" :in-theory (enable assoc mem-array-p)))))
+
+(local
+ (defthm integerp-default-in-mem-array
+     (implies (mem-p mem)
+	      (integerp (default 'mem mem)))
+   :hints (("Goal" :in-theory (enable mem-p)))))
+
+(defthm page-p-get-page
+    (implies (and (mem-p mem)
+		  (integerp pn)
+		  (not (integerp (get-page pn mem))))
+	     (page-p (get-page pn mem)))
+  :hints (("Goal" :in-theory (enable aref1 mem-p))))
+)
+
+(local
+ (defthm word-p-assoc-word-array
+     (implies (and (word-array-p wa)
+		   (integerp pn)
+		   (assoc pn wa))
+	      (word-p (cdr (assoc pn wa))))
+   :hints (("Goal" :in-theory (enable word-array-p assoc)))))
+
+(encapsulate nil
+(defthm word-p-read-page
+    (implies (and (page-p page)
+		  (integerp offset))
+	     (word-p (read-page offset page)))
+  :hints (("Goal" :in-theory (enable page-p aref1 page-array-p))))
+)
+
+(in-theory (disable read-page read-mem))
+(verify-guards read-mem
+	       :hints (("goal" :in-theory (enable mem-p))))
+
+(defthm word-p-read-mem
+    (implies (and (mem-p mem)
+		  (addr-p addr))
+	     (word-p (read-mem addr mem)))
+  :hints (("Goal" :in-theory (enable read-mem)))
+  :rule-classes
+  ((:rewrite)
+   (:type-prescription :corollary
+		       (implies (and (mem-p mem) (addr-p addr))
+				(and (integerp (read-mem addr mem))
+				     (>= (read-mem addr mem) 0))))
+   (:rewrite :corollary
+	     (implies (and (mem-p mem) (addr-p addr))
+		      (acl2-numberp (read-mem addr mem))))))
+
+
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; Definition of Write-Mem
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; Page tag is calculated for fast array access.
+; The tag for the <n>'th page is given by page<n>.
+(defun gen-page-tag (page-num)
+  (declare (xargs :guard (and (integerp page-num)
+			      (>= page-num 0))
+		  :verify-guards nil))
+  (pack-intern 'mem
+       (coerce (append (coerce (symbol-name 'page) 'list)
+		       (explode-nonnegative-integer page-num 10 nil))
+	       'string)))
+
+(encapsulate nil
+(local
+ (defthm character-listp-explode-nonnegative-integer-help
+     (implies (and (integerp n) (>= n 0)
+		   (character-listp x))
+	      (character-listp (explode-nonnegative-integer n print-base x)))
+   :hints (("goal" :in-theory (enable explode-nonnegative-integer
+				      character-listp)))))
+
+(local
+ (defthm character-listp-explode-nonnegative-integer
+     (implies (and (integerp n) (>= n 0))
+	      (character-listp (explode-nonnegative-integer n print-base nil)))))
+
+; Renamed by Matt K. after Version 4.3, since a similar :type-prescription
+; lemma is now provided by the ACL2 system.  Perhaps it could be deleted now.
+(local
+ (defthm true-listp-explode-nonnegative-integer-rewrite
+     (implies (true-listp x)
+	      (true-listp (explode-nonnegative-integer n print-base x)))))
+
+(verify-guards gen-page-tag
+     :hints (("goal" :in-theory (enable U::coerce-string-designator-list
+					U::STRING-DESIGNATOR-LISTP
+					character-listp
+					binary-append))))
+)
+
+(defun init-page (page-num mode)
+  (declare (xargs :guard (and (integerp page-num) (<= 0 page-num)
+			      (integerp mode))
+		  :verify-guards nil))
+  (let ((name (gen-page-tag page-num)))
+    (page name
+	  mode
+	  (compress1 name `((:header :name ,name
+			     :dimensions (,*num-page-words*)
+			     :default 0
+			     :maximum-length 4096))))))
+
+(verify-guards init-page
+ :hints (("Goal" :in-theory (enable array1p alistp
+				    keyword-value-listp
+				    assoc-eq
+				    assoc-keyword
+				    bounded-integer-alistp))))
+
+(defun write-page (val offset page)
+  (declare (xargs :guard (and (word-p val)
+			      (integerp offset) (<= 0 offset)
+			      (< offset *num-page-words*)
+			      (page-p page))
+		  :verify-guards nil))
+  (update-page page
+	       :array (aset1 (page-tag page) (page-array page) offset val)))
+
+(defun write-mem (val addr mem)
+  (declare (xargs :guard (and (word-p val) (addr-p addr) (mem-p mem))
+		  :verify-guards nil))
+  (let ((page (get-page (page-num addr) mem)))
+    (if (integerp page)
+	(let ((p (init-page (page-num addr) page)))
+	  (set-page (write-page val (page-offset addr) p)
+		    (page-num addr)
+		    mem))
+	(set-page (write-page val (page-offset addr) page)
+		  (page-num addr)
+		  mem))))
+
+(verify-guards write-page
+  :hints (("Goal" :in-theory (enable page-p page-array-p))))
+
+(in-theory (disable  write-mem init-page gen-page-tag write-page))
+
+
+(defthm page-p-init-page
+    (implies (integerp mode)
+	     (page-p (init-page pn mode)))
+  :hints (("goal" :in-theory (enable page-p init-page page-array-p
+				     default dimensions
+				     header array1p word-array-p))))
+
+(verify-guards write-mem
+  :hints (("Goal" :in-theory (enable mem-p ))))
+
+(local
+(defthm word-array-p-compress11
+    (implies (and (array1p tag array)
+		  (word-array-p array)
+		  (integerp i))
+	     (word-array-p (compress11 tag array i dim default)))
+  :hints (("Goal" :in-theory (enable word-array-p)))))
+
+
+; Added by Matt K. for Version 3.1, 7/1/06, to support proof of
+; compress1-assoc-property-0 in light of addition of reverse-sorted and
+; unsorted ACL2 arrays:
+(local
+ (defthm word-array-p-revappend
+   (equal (word-array-p (revappend x y))
+          (and (word-array-p x)
+               (word-array-p y)))
+   :hints (("Goal" :in-theory (enable word-array-p)
+            :induct (revappend x y)))))
+
+(defthm word-array-p-compress1
+    (implies (and (array1p tag array)
+		  (word-array-p array))
+	     (word-array-p (compress1 tag array)))
+  :hints (("Goal" :in-theory (enable compress1 word-array-p))))
+
+(defthm word-array-p-aset1
+    (implies (and (array1p tag page-array)
+		  (word-array-p page-array)
+		  (integerp index)
+		  (>= index 0)
+		  (> (car (dimensions tag page-array)) index)
+		  (word-p val))
+	     (word-array-p (aset1 tag page-array index val)))
+  :hints (("goal" :in-theory (enable aset1 word-array-p ARRAY1P-CONS))))
+
+(defthm page-array-p-aref1
+    (implies (and (page-array-p tag page-array)
+		  (word-p val)
+		  (integerp offset)
+		  (>= offset 0)
+		  (> *num-page-words* offset))
+	     (page-array-p tag (aset1 tag page-array offset val)))
+  :hints (("Goal" :in-theory (enable page-array-p))))
+
+
+(defthm page-p-write-page
+    (implies (and (word-p val)
+		  (integerp offset)
+		  (>= offset 0)
+		  (> *num-page-words* offset)
+		  (page-p page))
+	     (page-p (write-page val offset page)))
+  :hints (("Goal" :in-theory (enable write-page))))
+
+(local
+ (defthm valid-integer-assoc-mem-array
+     (implies (and (mem-array-p ma)
+		   (integerp pn)
+		   (assoc pn ma)
+		   (integerp (cdr (assoc pn ma)))
+		   (not (equal (cdr (assoc pn ma)) 0))
+		   (not (equal (cdr (assoc pn ma)) 1)))
+	      (equal (cdr (assoc pn ma)) 2))
+   :hints (("Goal" :in-theory (enable mem-array-p assoc)))))
+
+(local
+ (defthm page-p-assoc-mem-array
+     (implies (and (mem-array-p ma)
+		   (integerp pn)
+		   (assoc pn ma)
+		   (not (integerp (cdr (assoc pn ma)))))
+	      (page-p (cdr (assoc pn ma))))
+   :hints (("Goal" :in-theory (enable mem-array-p assoc)))))
+
+
+(local
+(defthm mem-array-p-compress11
+    (implies (and (array1p tag array)
+		  (mem-array-p array)
+		  (integerp i))
+	     (mem-array-p (compress11 tag array i dim default)))
+  :hints (("Goal" :in-theory (enable mem-array-p compress1)))))
+
+; Added by Matt K. for Version 3.1, 7/1/06, to support proof of
+; compress1-assoc-property-0 in light of addition of reverse-sorted and
+; unsorted ACL2 arrays:
+(local
+ (defthm mem-array-p-revappend
+   (equal (mem-array-p (revappend x y))
+          (and (mem-array-p x)
+               (mem-array-p y)))
+   :hints (("Goal" :in-theory (enable mem-array-p)
+            :induct (revappend x y)))))
+
+(defthm mem-array-p-compress1
+    (implies (and (array1p tag array)
+		  (mem-array-p array))
+	     (mem-array-p (compress1 tag array)))
+  :hints (("Goal" :in-theory (enable mem-array-p compress1))))
+
+
+
+(defthm mem-array-p-aset1
+    (implies (and (array1p tag mem-array)
+		  (mem-array-p mem-array)
+		  (or (page-p page)
+		      (equal page *no-access*)
+		      (equal page *read-only*)
+		      (equal page *read-write*))
+		  (integerp pn)
+		  (>= pn 0)
+		  (> (car (dimensions tag mem-array)) pn))
+	     (mem-array-p (aset1 tag mem-array pn page)))
+  :hints (("Goal" :in-theory (enable mem-array-p aset1))))
+
+
+(defthm mem-p-write-mem
+    (implies (and (word-p val)
+		  (addr-p addr)
+		  (mem-p mem))
+	     (mem-p (write-mem val addr mem)))
+  :hints (("goal" :in-theory (enable mem-p write-mem))))
+
+(defthm page-num-offset-extionsionality
+     (implies (and (addr-p addr1)
+		   (addr-p addr2)
+		   (equal (page-num addr1) (page-num addr2))
+		   (equal (page-offset addr1) (page-offset addr2)))
+	      (equal addr1 addr2))
+  :hints (("Goal" :in-theory (enable addr-p page-num page-offset)))
+   :rule-classes
+   ((:rewrite :corollary
+	      (implies (and (addr-p addr1)
+			    (addr-p addr2)
+			    (equal (page-num addr1) (page-num addr2))
+			    (not (equal addr1 addr2)))
+		       (equal (equal (page-offset addr1) (page-offset addr2))
+			      nil)))))
+
+(defthm read-page-init-page
+    (implies (integerp offset)
+	     (equal (read-page offset (init-page pn mode)) 0))
+  :hints (("Goal" :in-theory (enable init-page read-page aref1
+				     default header))))
+
+
+(defthm read-page-write-page
+    (implies (and (page-p page)
+		  (integerp offset1)
+		  (>= offset1 0)
+		  (> *num-page-words* offset1)
+		  (integerp offset2)
+		  (>= offset2 0)
+		  (> *num-page-words* offset2))
+	     (equal (read-page offset1 (write-page val offset2 page))
+		    (if (equal offset1 offset2)
+			val
+			(read-page offset1 page))))
+  :hints (("Goal" :in-theory (enable page-p read-page write-page
+				     page-array-p))))
+
+
+(defthm read-mem-write-mem
+    (implies (and (addr-p ad1)
+		  (addr-p ad2)
+		  (mem-p mem))
+	     (equal (read-mem ad1 (write-mem val ad2 mem))
+		    (if (equal ad1 ad2) val (read-mem ad1 mem))))
+  :hints (("Goal" :in-theory (enable read-mem write-mem
+				     mem-p))))
+
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; Definition of Protection Check.
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+(defun readable-addr-p (ad mem)
+  (declare (xargs :guard (and (addr-p ad) (mem-p mem))
+		  :verify-guards nil))
+  (let ((page (get-page (page-num ad) mem)))
+    (if (integerp page)
+	(or (equal page *read-only*)
+	    (equal page *read-write*))
+	(or (equal (page-mode page) *read-only*)
+	    (equal (page-mode page) *read-write*)))))
+
+(verify-guards  readable-addr-p
+ :hints (("Goal" :in-theory (enable mem-p))))
+
+(defun readable-addr? (ad mem)
+  (declare (xargs :guard (and (addr-p ad) (mem-p mem))))
+  (if (readable-addr-p ad mem) 1 0))
+
+(defthm bitp-readable-addr (bitp (readable-addr? ad mem)))
+
+(defun writable-addr-p (ad mem)
+  (declare (xargs :guard (and (addr-p ad) (mem-p mem))
+		  :verify-guards nil))
+  (let ((page (get-page (page-num ad) mem)))
+    (if (integerp page)
+	(equal page *read-write*)
+	(equal (page-mode page) *read-write*))))
+
+(verify-guards  writable-addr-p
+ :hints (("Goal" :in-theory (enable mem-p))))
+
+(defun writable-addr? (ad mem)
+  (declare (xargs :guard (and (addr-p ad) (mem-p mem))))
+  (if (writable-addr-p ad mem) 1 0))
+
+(defthm bitp-writable-addr (bitp (writable-addr? ad mem)))
+
+(defun set-page-mode (mode pn mem)
+  (declare (xargs :guard (and (integerp mode)
+			      (integerp pn) (<= 0 pn) (< pn *num-pages*)
+			      (mem-p mem))
+		  :verify-guards nil))
+  (let ((page (get-page pn mem)))
+    (if (integerp page)
+	(set-page mode pn mem)
+	(set-page (update-page page :mode mode) pn mem))))
+
+(verify-guards set-page-mode
+	:hints (("Goal" :in-theory (enable mem-p))))
+
+(defthm mem-p-set-page-mode
+    (implies (and (mem-p mem)
+		  (integerp mode)
+		  (or (equal mode *no-access*)
+		      (equal mode *read-only*)
+		      (equal mode *read-write*))
+		  (integerp pn) (<= 0 pn) (< pn *num-pages*))
+	     (mem-p (set-page-mode mode pn mem)))
+  :hints (("Goal" :in-theory (enable mem-p))))
+
+(defthm page-mode-init-page
+    (equal (page-mode (init-page page-num mode)) mode)
+  :hints (("Goal" :in-theory (enable init-page))))
+
+(defthm page-mode-write-page
+    (equal (page-mode (write-page val offset page))
+	   (page-mode page))
+  :hints (("Goal" :in-theory (enable write-page))))
+
+(defthm readable-addr-p-set-page-mode
+    (implies (and (integerp mode)
+		  (addr-p addr)
+		  (integerp pn1) (<= 0 pn1) (< pn1 *num-pages*)
+		  (mem-p mem))
+	     (equal (readable-addr-p addr (set-page-mode mode pn1 mem))
+		    (if (equal (page-num addr) pn1)
+			(or (equal mode *read-only*) (equal mode *read-write*))
+			(readable-addr-p addr mem))))
+  :hints (("Goal" :in-theory (enable set-page-mode mem-p
+				     readable-addr-p))))
+
+
+(defthm readable-addr-set-page-mode
+    (implies (and (integerp mode)
+		  (addr-p addr)
+		  (integerp pn1) (<= 0 pn1) (< pn1 *num-pages*)
+		  (mem-p mem))
+	     (equal (readable-addr? addr (set-page-mode mode pn1 mem))
+		    (if (equal (page-num addr) pn1)
+			(if (or (equal mode *read-only*)
+				(equal mode *read-write*))
+			    1 0)
+			(readable-addr? addr mem))))
+  :hints (("Goal" :in-theory (e/d (readable-addr?) (readable-addr-p
+						    SET-PAGE-MODE)))))
+
+(defthm writable-addr-p-set-page-mode
+    (implies (and (integerp mode)
+		  (addr-p addr)
+		  (integerp pn1) (<= 0 pn1) (< pn1 *num-pages*)
+		  (mem-p mem))
+	     (equal (writable-addr-p addr (set-page-mode mode pn1 mem))
+		    (if (equal (page-num addr) pn1)
+			(equal mode *read-write*)
+			(writable-addr-p addr mem))))
+  :hints (("Goal" :in-theory (enable set-page-mode mem-p
+				     writable-addr-p))))
+
+(defthm writable-addr-set-page-mode
+    (implies (and (integerp mode)
+		  (addr-p addr)
+		  (integerp pn1) (<= 0 pn1) (< pn1 *num-pages*)
+		  (mem-p mem))
+	     (equal (writable-addr? addr (set-page-mode mode pn1 mem))
+		    (if (equal (page-num addr) pn1)
+			(if (equal mode *read-write*) 1 0)
+			(writable-addr? addr mem))))
+  :hints (("Goal" :in-theory (e/d (writable-addr?)
+				  (writable-addr-p SET-PAGE-MODE)))))
+
+(defthm readable-addr-p-write-mem
+    (implies (and (addr-p addr) (addr-p addr2) (word-p val) (mem-p mem))
+	     (equal (readable-addr-p addr (write-mem val addr2 mem))
+		    (readable-addr-p addr mem)))
+  :hints (("Goal" :in-theory (enable readable-addr-p write-mem mem-p))))
+
+(defthm readable-addr-write-mem
+    (implies (and (addr-p addr) (addr-p addr2) (word-p val) (mem-p mem))
+	     (equal (readable-addr? addr (write-mem val addr2 mem))
+		    (readable-addr? addr mem)))
+  :hints (("Goal" :in-theory (enable readable-addr?))))
+
+(defthm writable-addr-p-write-mem
+    (implies (and (addr-p addr) (addr-p addr2) (word-p val) (mem-p mem))
+	     (equal (writable-addr-p addr (write-mem val addr2 mem))
+		    (writable-addr-p addr mem)))
+  :hints (("Goal" :in-theory (enable writable-addr-p write-mem mem-p))))
+
+(defthm writable-addr-write-mem
+    (implies (and (addr-p addr) (addr-p addr2) (word-p val) (mem-p mem))
+	     (equal (writable-addr? addr (write-mem val addr2 mem))
+		    (writable-addr? addr mem)))
+  :hints (("Goal" :in-theory (enable writable-addr?))))
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; Initialize Memory
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+(defconst *init-mem*
+    (compress1 'mem (list `(:header :name mem
+			    :dimensions (,*num-pages*)
+			    :default ,*no-access*
+			    :maximum-length 2048))))
+
+(defthm mem-p-init-mem
+    (mem-p *init-mem*))
+
+(deflist mem-alist-p (l)
+  (declare (xargs :guard t))
+  (lambda (l) (and (consp l) (addr-p (car l)) (word-p (cdr l)))))
+
+(defun load-mem-alist (alist mem)
+  (declare (xargs :guard (and (mem-alist-p alist) (mem-p mem))))
+  (if (endp alist)
+      mem
+      (load-mem-alist (cdr alist) (write-mem (cdar alist) (caar alist) mem))))
+
+(defthm mem-p-load-mem-alist
+    (implies (and (mem-alist-p alist)
+		  (mem-p mem))
+	     (mem-p (load-mem-alist alist mem))))
+
+(in-theory (disable page-p page-array-p word-array-p mem-p))
+(in-theory (disable read-reg))
+(in-theory (disable write-reg))
+(in-theory (disable read-mem))
+(in-theory (disable write-mem))
+(in-theory (disable writable-addr-p readable-addr-p
+		    writable-addr? readable-addr? set-page-mode))
+
+(defword* word-layout ((op-field 4 12)
+		      (rc-field *rname-size* 8)
+		      (ra-field *rname-size* 4)
+		      (rb-field *rname-size* 0)
+		      (im-field *immediate-size* 0))
+  :conc-name ||)
+
+
+(defthm opcd-p-opcode
+    (opcd-p (op-field inst))
+  :hints (("Goal" :in-theory (enable opcd-p))))
+
+(defthm rname-p-rc-field
+    (rname-p (rc-field inst))
+  :hints (("Goal" :in-theory (enable rname-p))))
+
+(defthm rname-p-ra-field
+    (rname-p (ra-field inst))
+  :hints (("Goal" :in-theory (enable rname-p))))
+
+(defthm rname-p-rb-field
+    (rname-p (rb-field inst))
+  :hints (("Goal" :in-theory (enable rname-p))))
+
+
+(defthm immediate-p-immediate-field
+    (immediate-p (im-field inst))
+  :hints (("Goal" :in-theory (enable immediate-p))))
+
+
+(defthm word-p-immediate-field
+    (word-p (im-field inst))
+  :hints (("Goal" :in-theory (enable word-p))))
+
+(defthm word-IM-field
+    (equal (word (IM-field i)) (IM-field i))
+  :hints (("goal" :in-theory (enable word))))
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;  Definition of Special registers
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+(defconst *num-sregs* 2)
+
+(defstructure sregs
+  (su (:assert (bitp su) :rewrite ))
+  (sr0 (:assert (word-p sr0) :rewrite))
+  (sr1 (:assert (word-p sr1) :rewrite))
+  (:options :guards))
+
+(defun srname-p (rname)
+  (declare (xargs :guard t))
+  (and (rname-p rname) (< rname *num-sregs*)))
+
+(defthm srname-p-type
+    (implies (srname-p rname)
+	     (and (integerp rname)
+		  (>= rname 0)
+		  (< rname *num-sregs*)))
+  :hints (("Goal" :in-theory (enable rname-p srname-p)))
+  :rule-classes :forward-chaining)
+
+(defun read-sreg (id sregs)
+  (declare (xargs :guard (and (rname-p id) (sregs-p sregs))))
+  (if (equal id 0) (sregs-sr0 sregs)
+      (if (equal id 1) (sregs-sr1 sregs)
+	  0)))
+
+(defun write-sreg (val id sregs)
+  (declare (xargs :guard (and (word-p val) (rname-p id) (sregs-p sregs))))
+  (if (equal id 0) (sregs (sregs-su sregs) val (sregs-sr1 sregs))
+      (if (equal id 1) (sregs (sregs-su sregs) (sregs-sr0 sregs) val)
+	  sregs)))
+
+(defthm word-p-read-sreg
+    (implies (and (rname-p id) (sregs-p sregs))
+	     (word-p (read-sreg id sregs))))
+
+(defthm numberp-read-sreg
+    (implies (and (sregs-p sregs)
+		  (rname-p rname))
+	     (and (integerp (read-sreg rname sregs))
+		  (acl2-numberp (read-sreg rname sregs))))
+  :hints (("Goal" :in-theory (enable rname-p sregs-p fixlen-word-listp)))
+  :rule-classes
+  ((:type-prescription) (:rewrite)))
+
+(defthm sregs-p-write-sreg
+    (implies (and (word-p val) (rname-p id) (sregs-p sregs))
+	     (sregs-p (write-sreg val id sregs))))
+
+(defthm read-sreg-write-sreg
+    (implies (and (srname-p rn1)
+		  (srname-p rn2)
+		  (sregs-p sregs))
+	     (equal (read-sreg rn1 (write-sreg val rn2 sregs))
+		    (if (equal rn1 rn2) val (read-sreg rn1 sregs))))
+  :hints (("Goal" :in-theory (enable read-sreg write-sreg sregs-p
+				     srname-p))))
+
+(in-theory (disable read-sreg write-sreg srname-p))
diff --git a/books/workshops/2000/manolios/pipeline/trivial/sawada-model/basic-lemmas.lisp b/books/workshops/2000/manolios/pipeline/trivial/sawada-model/basic-lemmas.lisp
new file mode 100644
index 0000000..973bd09
--- /dev/null
+++ b/books/workshops/2000/manolios/pipeline/trivial/sawada-model/basic-lemmas.lisp
@@ -0,0 +1,846 @@
+(in-package "ACL2")
+
+;(include-book "utils")
+(include-book "basic-def")
+(include-book "model")
+(include-book "table-def")
+
+(deflabel begin-basic-lemmas)
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;  Proof of misc lemmas
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; Lemmas about bv-eqv
+(defthm bv-eqv-opcode-p
+    (implies (and (opcd-p x) (opcd-p y))
+	     (equal (b1p (bv-eqv *opcode-size* x y)) (equal x y)))
+  :hints (("goal" :in-theory (enable opcd-p))))
+
+(defthm bv-eqv-rname-p
+    (implies (and (rname-p x) (rname-p y))
+	     (equal (b1p (bv-eqv *opcode-size* x y)) (equal x y)))
+  :hints (("goal" :in-theory (enable rname-p))))
+
+
+; Lemmas about the projection from an MA state to an ISA state.
+(defthm ISA-pc-proj
+    (equal (ISA-pc (proj MA)) (MA-pc MA))
+  :hints (("Goal" :in-theory (enable proj))))
+
+(defthm ISA-regs-proj
+    (equal (ISA-regs (proj MA)) (MA-regs MA))
+  :hints (("Goal" :in-theory (enable proj))))
+
+(defthm ISA-mem-proj
+    (equal (ISA-mem (proj MA)) (MA-mem MA))
+  :hints (("Goal" :in-theory (enable proj))))
+
+; (tail-p sublist list) is true if sublist is a terminating sub-list
+; of list.  For instance, (tail-p '(1 2 3 4) '(3 4)) is T, while
+; (tail-p '(1 2 3 4) '(2 3)) is nil.
+(defun tail-p (sublist list)
+  (declare (xargs :guard (and (true-listp sublist) (true-listp list))))
+  (if (equal sublist list)
+      T
+    (if (endp list)
+	nil
+      (tail-p sublist (cdr list)))))
+
+; Basic lemmas bout tail-p.
+(defthm tail-p-cdr-1
+    (implies (and (consp sub) (tail-p sub lst))
+	     (tail-p (cdr sub) lst)))
+
+(defthm tail-p-cdr-2
+    (implies (consp lst) (not (tail-p lst (cdr lst))))
+  :hints (("Goal" :induct (len lst))))
+
+; (INST-in i MT) is T, if MT contains i as an instruction entry.
+(defun INST-in (i MT)
+  (member-equal i (MT-trace MT)))
+
+; (subtrace-p trace MT) is T if trace is a terminating sub-list of
+; the list of instruction entries in MT.   Since MT stores
+; instruction entries in ISA execution order, trace is a list of
+; entries representing most recently fetched instructions.
+(defun subtrace-p (trace MT)
+  (declare (xargs :guard (and (INST-listp trace) (MAETT-p MT))))
+  (tail-p trace (MT-trace MT)))
+
+(in-theory (disable INST-in subtrace-p))
+
+(defthm subtrace-p-MT-trace
+    (subtrace-p (MT-trace MT) MT)
+  :hints (("Goal" :in-theory (enable subtrace-p))))
+
+(defthm subtrace-p-cdr
+    (implies (and (subtrace-p trace MT) (consp trace))
+	     (subtrace-p (cdr trace) MT))
+  :hints (("goal" :in-theory (enable subtrace-p))))
+
+(encapsulate nil
+(local
+(defthm inst-in-car-subtrace-induction
+    (implies (and (consp sub) (tail-p sub trace))
+	     (member-equal (car sub) trace))))
+
+(defthm inst-in-car-subtrace
+    (implies (and  (consp trace) (subtrace-p trace MT))
+	     (INST-in (car trace) MT))
+  :hints (("Goal" :in-theory (enable INST-in subtrace-p))))
+)
+
+; ISA-at-tail is used in the definition of ISA-before
+(defun ISA-at-tail (sub trace pre)
+  (declare (xargs :guard (and (INST-listp sub) (INST-listp trace)
+			      (ISA-state-p pre))))
+  (if (equal sub trace)
+      pre
+      (if (endp trace) pre
+	  (ISA-at-tail sub (cdr trace) (INST-post-ISA (car trace))))))
+
+(defthm ISA-state-p-ISA-at-tail
+    (implies (and (ISA-state-p pre)
+		  (INST-listp trace))
+	     (ISA-state-p (ISA-at-tail sub trace pre))))
+
+; (ISA-before sub MT) returns the ISA state before the execution of
+; the first instruction in sub.  For instance, MT represents
+; instructions I_1, I_2, I_3 and I_4.  If sub = (I_3 I_4), then
+; (ISA-before sub MT) returns ISA state before executing I_3.  If sub is nil,
+; (ISA-before sub MT) returns the ISA state after executing all instructions
+; represented in MT.
+(defun ISA-before (sub MT)
+  (declare (xargs :guard (and (INST-listp sub) (MAETT-p MT))))
+  (ISA-at-tail sub (MT-trace MT) (MT-init-ISA MT)))
+
+(in-theory (disable ISA-before))
+
+(defthm ISA-state-p-ISA-before
+    (implies (MAETT-p MT)
+	     (ISA-state-p (ISA-before sub MT)))
+  :hints (("goal" :in-theory (enable ISA-before))))
+
+(defthm ISA-before-MT-trace
+    (equal (ISA-before (MT-trace MT) MT)
+	   (MT-init-ISA MT))
+  :hints (("Goal" :in-theory (enable ISA-before))))
+
+(encapsulate nil
+(defthm ISA-before-cdr-induction
+    (implies (and (tail-p sub trace)
+		  (consp sub))
+	     (equal (ISA-at-tail (cdr sub) trace ISA)
+		    (INST-post-ISA (car sub)))))
+
+(defthm ISA-before-cdr
+    (implies (and (subtrace-p sub MT)
+		  (consp sub))
+	     (equal (ISA-before (cdr sub) MT)
+		    (INST-post-ISA (car sub))))
+  :hints (("Goal" :in-theory (enable ISA-before subtrace-p))))
+)
+
+(encapsulate nil
+(local
+(defthm INST-p-INST-at-induction
+    (implies (and (INST-listp trace) (trace-INST-at stg trace))
+	     (INST-p (trace-INST-at stg trace)))))
+
+; INST-p-INST-at asserts that (INST-at stg MT) is of type INST-p if
+; there exists an instruction at stage stg.  (INST-at stg MT) is
+; nil if MT does not contains an entry representing an instruction at
+; stage stg.
+(defthm INST-p-INST-at
+    (implies (and (MAETT-p MT) (INST-at stg MT))
+	     (INST-p (INST-at stg MT)))
+  :hints (("Goal" :in-theory (enable INST-p INST-at))))
+)
+
+(encapsulate nil
+(local
+(defthm INST-in-INST-at-induction
+    (implies (trace-INST-at stg trace)
+	     (member-equal (trace-INST-at stg trace) trace))))
+
+; (INST-at stg MT) is an instruction entry in MT, unless it is nil.
+(defthm INST-in-INST-at
+    (implies (INST-at stg MT)
+	     (INST-in (INST-at stg MT) MT))
+  :hints (("Goal" :in-theory (enable INST-at INST-in))))
+)
+
+
+(encapsulate nil
+(local
+(defthm INST-stg-INST-at-induction
+    (implies (trace-INST-at stg trace)
+	     (equal (INST-stg (trace-INST-at stg trace)) stg))))
+
+; Stage of (INST-at stg MT).
+(defthm INST-stg-INST-at
+    (implies (INST-at stg MT) (equal (INST-stg (INST-at stg MT)) stg))
+  :hints (("Goal" :in-theory (enable INST-at))))
+)
+
+; Memory is not updated by our machine.
+(defthm ISA-mem-ISA-step
+    (equal (ISA-mem (ISA-step ISA)) (ISA-mem ISA))
+  :hints (("Goal" :in-theory (enable ISA-step ISA-add ISA-sub ISA-default))))
+
+(defthm ISA-mem-ISA-stepn
+    (equal (ISA-mem (ISA-stepn ISA n)) (ISA-mem ISA)))
+
+; Various small lemmas about attributes of instructions.  I don't
+; comment each of them.  Most of them are trivial from the definition
+; of the instruction attributes and the definition of step-INST.
+(defthm INST-word-new-INST
+    (equal (INST-word (new-INST ISA))
+	   (read-mem (ISA-pc ISA) (ISA-mem ISA)))
+  :hints (("Goal" :in-theory (enable new-INST INST-word))))
+
+(defthm INST-stg-new-INST
+    (equal (INST-stg (new-INST ISA)) 'latch1)
+  :hints (("Goal" :in-theory (enable new-INST))))
+
+(defthm INST-pre-ISA-new-INST
+    (equal (INST-pre-ISA (new-INST ISA)) ISA)
+  :hints (("Goal" :in-theory (enable new-INST))))
+
+(defthm INST-post-ISA-new-INST
+    (equal (INST-post-ISA (new-INST ISA)) (ISA-step ISA))
+  :hints (("Goal" :in-theory (enable new-INST))))
+
+(defthm INST-word-step-INST
+    (implies (INST-p i)
+	     (equal (INST-word (step-INST i MA)) (INST-word i)))
+  :hints (("Goal" :in-theory (enable step-INST step-latch1-INST
+				     INST-word step-latch2-INST))))
+
+(defthm INST-op-step-INST
+    (implies (INST-p i)
+	     (equal (INST-op (step-INST i MA)) (INST-op i)))
+  :hints (("Goal" :in-theory (enable INST-op))))
+
+(defthm INST-rc-step-INST
+    (implies (INST-p i)
+	     (equal (INST-rc (step-INST i MA)) (INST-rc i)))
+  :hints (("Goal" :in-theory (enable INST-rc))))
+
+(defthm INST-ra-step-INST
+    (implies (INST-p i)
+	     (equal (INST-ra (step-INST i MA)) (INST-ra i)))
+  :hints (("Goal" :in-theory (enable INST-ra))))
+
+(defthm INST-rb-step-INST
+    (implies (INST-p i)
+	     (equal (INST-rb (step-INST i MA)) (INST-rb i)))
+  :hints (("Goal" :in-theory (enable INST-rb))))
+
+
+(defthm INST-pre-ISA-step-INST
+    (implies (INST-p i)
+	     (equal (INST-pre-ISA (step-INST i MA)) (INST-pre-ISA i)))
+  :hints (("Goal" :in-theory (enable step-INST step-latch1-INST
+				     step-latch2-INST))))
+
+(defthm INST-post-ISA-step-INST
+    (implies (INST-p i)
+	     (equal (INST-post-ISA (step-INST i MA)) (INST-post-ISA i)))
+  :hints (("Goal" :in-theory (enable step-INST step-latch1-INST
+				     step-latch2-INST))))
+(defthm INST-pre-ISA-car-MT-trace
+    (implies (and (invariant MT MA)
+		  (consp (MT-trace MT)))
+	     (equal (INST-pre-ISA (car (MT-trace MT))) (MT-init-ISA MT)))
+  :hints (("Goal" :in-theory (enable invariant ISA-chain-p))))
+
+
+(defthm MT-init-ISA-init-MT
+    (equal (MT-init-ISA (init-MT MA)) (proj MA))
+  :hints (("Goal" :in-theory (enable init-MT))))
+
+(defthm MT-init-ISA-MT-step
+    (equal (MT-init-ISA (MT-step MT MA sig))
+	   (MT-init-ISA MT))
+  :hints (("goal" :in-theory (enable MT-step))))
+
+(defthm MT-init-ISA-MT-stepn
+    (equal (MT-init-ISA (MT-stepn MT MA sig n))
+	   (MT-init-ISA MT)))
+
+
+; In order to understand following several lemmas, you need to understand
+; how INST-pre-ISA and INST-post-ISA make a chain of ISA states.
+; Intuitively, (INST-pre-ISA i) is the ISA state before executing the
+; instruction represented by i, and (INST-post-ISA i) is the ISA state
+; after the execution.  Suppose we execute instruction I_0, I_1 and I_2
+; in that order successively.  Equation
+; (INST-post-ISA I_0) = (INST-pre-ISA I_1)
+; holds because the resulting state of an instruction is a starting state
+; for the immediately following instruction.   This relation can be
+; described better with a picture shown below:
+;   (INST-pre-ISA i_0)
+;         |  execution of i_0
+;         v
+;   (INST-post-ISA i_0) = (INST-pre-ISA i_1)
+;         |  execution of i_1
+;         v
+;   (INST-post-ISA i_1) = (INST-pre-ISA i_2)
+;         ...
+; The transition relation can be written as
+;  (INST-post-ISA I_0) = (ISA-step (INST-pre-ISA I_0)).
+(encapsulate nil
+(local
+(defthm INST-post-ISA-INST-in-induction
+    (implies (and (member-equal i trace)
+		  (ISA-chain-trace-p trace ISA)
+		  (INST-p i))
+	     (equal (INST-post-ISA i)
+		    (ISA-step (INST-pre-ISA i))))))
+
+(defthm INST-post-ISA-INST-in
+    (implies (and (invariant MT MA)
+		  (MAETT-p MT)
+		  (INST-in i MT) (INST-p i))
+	     (equal (INST-post-ISA i)
+		    (ISA-step (INST-pre-ISA i))))
+  :hints (("Goal" :in-theory (enable INST-in invariant ISA-chain-p))))
+)
+
+
+(encapsulate nil
+(local
+(defthm INST-post-ISA-car-subtrace-help
+    (implies (and (ISA-chain-trace-p trace ISA)
+		  (tail-p sub trace)
+		  (consp sub)
+		  (INST-listp trace))
+	     (equal (INST-post-ISA (car sub))
+		    (ISA-step (INST-pre-ISA (car sub)))))))
+
+(defthm INST-post-ISA-car-subtrace
+    (implies (and (invariant MT MA)
+		  (subtrace-p trace MT)
+		  (MAETT-p MT)
+		  (consp trace)
+		  (INST-listp trace))
+	     (equal (INST-post-ISA (car trace))
+		    (ISA-step (INST-pre-ISA (car trace)))))
+  :hints (("goal" :in-theory (enable invariant subtrace-p
+				     ISA-chain-p))))
+)
+
+(encapsulate nil
+(local
+(defthm INST-pre-ISA-cadr-subtrace-induction
+    (implies (and (ISA-chain-trace-p trace ISA)
+		  (tail-p sub trace)
+		  (INST-listp trace)
+		  (consp sub)
+		  (consp (cdr sub)))
+	     (equal (INST-pre-ISA (cadr sub))
+		    (ISA-step (INST-pre-ISA (car sub)))))))
+
+(defthm INST-pre-ISA-cadr-subtrace
+    (implies (and (invariant MT MA)
+		  (subtrace-p trace MT)
+		  (MAETT-p MT)
+		  (INST-listp trace)
+		  (consp trace)
+		  (consp (cdr trace)))
+	     (equal (INST-pre-ISA (cadr trace))
+		    (ISA-step (INST-pre-ISA (car trace)))))
+  :hints (("goal" :in-theory (enable invariant ISA-chain-p subtrace-p))))
+)
+
+(encapsulate nil
+(local
+(defthm ISA-before-INST-pre-ISA-car-induction
+    (implies (and (invariant MT MA)
+		  (MAETT-p MT) (MA-state-p MA)
+		  (INST-listp trace)
+		  (subtrace-p trace MT)
+		  (tail-p sub trace)
+		  (consp sub))
+     (equal (ISA-at-tail sub trace (INST-pre-ISA (car trace)))
+	    (INST-pre-ISA (car sub))))
+  :hints (("Subgoal *1/3" :cases ((consp (cdr trace)))))
+  :rule-classes nil))
+
+; The relation between ISA-before and INST-pre-ISA is described by this
+; lemma.
+(defthm ISA-before-INST-pre-ISA-car
+    (implies (and (invariant MT MA)
+		  (MAETT-p MT) (MA-state-p MA)
+		  (subtrace-p trace MT)
+		  (consp trace))
+	     (equal (ISA-before trace MT)
+		    (INST-pre-ISA (car trace))))
+  :hints (("Goal" :in-theory (enable ISA-before subtrace-p)
+		  :use (:instance ISA-before-INST-pre-ISA-car-induction
+				  (sub trace)
+				  (trace (MT-trace MT))))
+	  ("Goal'" :cases ((consp (MT-trace MT))))))
+)
+(in-theory (disable ISA-before-INST-pre-ISA-car))
+
+(encapsulate nil
+(local
+(defthm ISA-pc-ISA-before-nil-help
+    (implies (and (equal (trace-pc trace ISA) (MA-pc MA))
+		  (MAETT-p MT) (MA-state-p MA))
+	     (equal (ISA-pc (ISA-at-tail nil trace ISA)) (MA-pc MA)))))
+
+; The program counter in an MA state points to the instruction which
+; will be fetched in the next machine cycle.  Since the MAETT records
+; all fetched instructions, the program counter of post-ISA of the
+; last instruction in the MAETT is equal to the  program counter in
+; the MA state.
+(defthm ISA-pc-ISA-before-nil
+    (implies (and (invariant MT MA)
+		  (MAETT-p MT) (MA-state-p MA))
+	     (equal (ISA-pc (ISA-before nil MT)) (MA-pc MA)))
+  :hints (("Goal" :in-theory (enable ISA-before invariant pc-match-p
+				     MT-pc))))
+)
+
+
+(encapsulate nil
+(local
+(defthm ISA-mem-ISA-before-nil-induction
+    (implies (and (MAETT-p MT) (MA-state-p MA)
+		  (ISA-chain-trace-p trace ISA))
+	     (equal (ISA-mem (ISA-at-tail nil trace ISA))
+		    (ISA-mem ISA)))))
+
+(local
+(defthm ISA-mem-ISA-before-nil-help
+    (implies (and (MAETT-p MT) (MA-state-p MA)
+		  (invariant MT MA))
+	     (equal (ISA-mem (ISA-before nil MT))
+		    (ISA-mem (MT-init-ISA MT))))
+  :hints (("Goal" :in-theory (enable ISA-before invariant ISA-chain-p)))))
+
+; Memory is not updated, therefore the memory state at any ISA state
+; is equal to any MA state.
+(defthm ISA-mem-ISA-before-nil
+    (implies (and (invariant MT MA)
+		  (MAETT-p MT) (MA-state-p MA))
+	     (equal (ISA-mem (ISA-before nil MT)) (MA-mem MA)))
+  :hints (("Goal" :in-theory (enable invariant mem-match-p))))
+)
+
+; There are only two states in this pipeline latch1 and latch2.  We also
+; count retire as another stage.  The stage of an instruction entry
+; should be one of them.
+(defthm stages-of-INST
+    (implies (INST-p i)
+	     (or (equal (INST-stg i) 'latch1) (equal (INST-stg i) 'latch2)
+		 (equal (INST-stg i) 'retire)))
+  :hints (("goal" :in-theory (enable INST-p stage-p)))
+  :rule-classes nil)
+
+; Following several lemmas are about how the stages of an instruction
+; changes.
+(defthm INST-stg-step-latch1-INST
+    (implies (equal (INST-stg i) 'latch1)
+	     (equal (INST-stg (step-INST i MA))
+		    (if (b1p (stall-cond? MA)) 'latch1 'latch2)))
+  :hints (("Goal" :in-theory (enable step-INST step-latch1-INST))))
+
+
+(defthm retire-step-INST-if-latch2
+    (implies (equal (INST-stg i) 'latch2)
+	     (equal (INST-stg (step-INST i MA)) 'retire))
+  :hints (("Goal" :in-theory (enable step-INST step-latch1-INST
+				     step-latch2-INST))))
+
+(defthm retire-step-INST-if-retire
+    (implies (equal (INST-stg i) 'retire)
+	     (equal (INST-stg (step-INST i MA)) 'retire))
+  :hints (("Goal" :in-theory (enable step-INST step-latch1-INST
+				     step-latch2-INST))))
+
+(defthm not-retire-step-INST-if-not-retire-latch2
+    (implies (and (INST-p i)
+		  (not (equal (INST-stg i) 'retire))
+		  (not (equal (INST-stg i) 'latch2)))
+	     (not (equal (INST-stg (step-INST i MT)) 'retire)))
+  :hints (("Goal" :in-theory (enable INST-p stage-p step-INST
+				     step-latch1-INST))))
+
+(encapsulate nil
+(local
+(defthm no-inst-after-INST-latch1-induction
+    (implies (and (trace-in-order-p trace)
+		  (tail-p sub trace)
+		  (INST-listp trace)
+		  (consp sub)
+		  (equal (INST-stg (car sub)) 'latch1))
+	     (endp (cdr sub)))
+  :rule-classes nil))
+
+; Instruction at latch1 is the most recently fetched instruction.  A
+; MAETT records instructions in program order, so the instruction at latch1
+; is always represented by the last entry of a MAETT.
+(defthm no-inst-after-INST-latch1
+    (implies (and (invariant MT MA)
+		  (MAETT-p MT) (MA-state-p MA)
+		  (subtrace-p trace MT)
+		  (INST-listp trace)
+		  (consp trace)
+		  (equal (INST-stg (car trace)) 'latch1))
+	     (endp (cdr trace)))
+  :hints (("Goal" :in-theory (enable subtrace-p invariant MT-in-order-p)
+		  :use (:instance no-inst-after-INST-latch1-induction
+				  (sub trace) (trace (MT-trace MT)))))
+  :rule-classes nil)
+)
+
+; A corollary of no-inst-after-INST-latch1.
+(defthm INST-latch1-last-inst-in-MT
+    (implies (and (invariant MT MA)
+		  (MAETT-p MT) (MA-state-p MA)
+		  (subtrace-p trace MT)
+		  (INST-listp trace)
+		  (consp trace)
+		  (equal (INST-stg (car trace)) 'latch1))
+	     (not (member-equal i (cdr trace))))
+  :hints (("Goal" :use (:instance no-inst-after-INST-latch1))))
+
+; The instruction at stage latch2 is older than the instruction at latch1.
+(defthm no-inst-at-latch2-after-latch1
+    (implies (and (invariant MT MA)
+		  (MAETT-p MT) (MA-state-p MA)
+		  (subtrace-p trace MT)
+		  (INST-listp trace)
+		  (consp trace)
+		  (equal (INST-stg (car trace)) 'latch1))
+	     (not (trace-INST-at 'latch2 (cdr trace))))
+  :hints (("Goal" :use (:instance no-inst-after-INST-latch1))))
+
+
+(encapsulate nil
+(local
+(defthm no-inst-at-latch2-after-latch2-help
+    (implies (and (trace-in-order-p trace)
+		  (tail-p sub trace)
+		  (INST-listp trace)
+		  (consp sub)
+		  (equal (INST-stg (car sub)) 'latch2))
+	     (not (trace-INST-at 'latch2 (cdr sub))))))
+
+; There are no two instructions at latch2.
+(defthm no-inst-at-latch2-after-latch2
+    (implies (and (invariant MT MA)
+		  (MAETT-p MT) (MA-state-p MA)
+		  (subtrace-p trace MT)
+		  (INST-listp trace)
+		  (consp trace)
+		  (equal (INST-stg (car trace)) 'latch2))
+	     (not (trace-INST-at 'latch2 (cdr trace))))
+  :hints (("Goal" :in-theory (enable subtrace-p invariant MT-in-order-p))))
+)
+
+(encapsulate nil
+(local
+(defthm no-inst-at-retire-after-latch2-help
+    (implies (and (trace-in-order-p trace)
+		  (tail-p sub trace)
+		  (INST-listp trace)
+		  (consp sub)
+		  (equal (INST-stg (car sub)) 'latch2))
+	     (not (trace-INST-at 'retire (cdr sub))))))
+
+; No retired instruction is younger than instruction at latch2.
+; Instructions are retired in program order.
+(defthm no-inst-at-retire-after-latch2
+    (implies (and (invariant MT MA)
+		  (MAETT-p MT) (MA-state-p MA)
+		  (subtrace-p trace MT)
+		  (INST-listp trace)
+		  (consp trace)
+		  (equal (INST-stg (car trace)) 'latch2))
+	     (not (trace-INST-at 'retire (cdr trace))))
+  :hints (("Goal" :in-theory (enable subtrace-p invariant MT-in-order-p))))
+)
+
+; An instruction at latch2 is immediately followed by an instruction
+; at latch1.
+(defthm INST-latch1-follows-INST-latch2
+    (implies (and (invariant MT MA)
+		  (MAETT-p MT) (MA-state-p MA)
+		  (subtrace-p trace MT)
+		  (INST-listp trace)
+		  (consp trace) (consp (cdr trace))
+		  (equal (INST-stg (car trace)) 'latch2))
+	     (equal (INST-stg (cadr trace)) 'latch1))
+  :hints (("Goal" :use ((:instance stages-of-inst (i (cadr trace)))
+			(:instance no-inst-at-latch2-after-latch2)
+			(:instance no-inst-at-retire-after-latch2))
+		  :in-theory (disable no-inst-at-latch2-after-latch2
+				      no-inst-at-retire-after-latch2))))
+
+
+; Predicate inst-invariant is an invariant condition that every
+; instruction in a MAETT should satisfy.  Following two lemmas shows
+; that in two different formulation.
+(encapsulate nil
+(local
+(defthm inst-invariant-INST-at-help
+    (implies (and (trace-INST-invariant trace MA)
+		  (trace-INST-at stg trace))
+	     (inst-invariant (trace-INST-at stg trace) MA))))
+
+(defthm inst-invariant-INST-at
+    (implies (and (invariant MT MA)
+		  (INST-at stg MT))
+	     (inst-invariant (INST-at stg MT) MA))
+  :hints (("Goal" :in-theory (enable INST-at invariant MT-inst-invariant))))
+)
+
+(encapsulate nil
+(local
+ (defthm INST-invariant-INST-in-induction
+     (implies (and (trace-inst-invariant trace MA)
+		   (member-equal i trace))
+	      (inst-invariant i MA))))
+
+
+(defthm INST-invariant-INST-in
+    (implies (and (invariant MT MA)
+		  (INST-in i MT))
+	     (inst-invariant i MA))
+  :hints (("Goal" :in-theory (enable invariant INST-in MT-inst-invariant
+				     trace-INST-invariant)))
+  :rule-classes nil)
+)
+
+; There must be an instruction at latch1 if flag latch1-valid? in an
+; MA state is on.  This lemma shows that a MAETT contains an entry
+; representing the instruction at latch1 if latch1-valid? is on in
+; the corresponding MA state.
+(defthm INST-at-latch1-if-latch1-valid
+    (implies (and (invariant MT MA)
+		  (b1p (latch1-valid? (MA-latch1 MA))))
+	     (INST-at 'latch1 MT))
+  :hints (("Goal" :in-theory (enable invariant MT-contains-all-insts))))
+
+; If latch1-valid? is off, no instruction is at latch1.
+(defthm not-INST-at-latch1-if-not-latch1-valid
+    (implies (and (invariant MT MA)
+		  (not (b1p (latch1-valid? (MA-latch1 MA)))))
+	     (not (INST-at 'latch1 MT)))
+  :hints (("Goal" :use (:instance INST-invariant-INST-at (stg 'latch1))
+		  :in-theory (e/d (INST-invariant INST-latch1-inv)
+				  (INST-invariant-INST-at)))))
+
+; If instruction i is at latch1, latch1-valid? should be on.
+(defthm latch1-valid-if-INST-in
+    (implies (and (invariant MT MA)
+		  (INST-in i MT) (INST-p i)
+		  (equal (INST-stg i) 'latch1))
+	     (b1p (latch1-valid? (MA-latch1 MA))))
+  :hints (("Goal" :use (:instance INST-invariant-INST-in)
+		  :in-theory (e/d (INST-invariant INST-latch1-inv)
+				  ()))))
+
+; Same for latch2.
+(defthm INST-at-latch2-if-latch2-valid
+    (implies (and (invariant MT MA)
+		  (b1p (latch2-valid? (MA-latch2 MA))))
+	     (INST-at 'latch2 MT))
+  :hints (("Goal" :in-theory (enable invariant MT-contains-all-insts))))
+
+(defthm not-INST-at-latch2-if-not-latch2-valid
+    (implies (and (invariant MT MA)
+		  (not (b1p (latch2-valid? (MA-latch2 MA)))))
+	     (not (INST-at 'latch2 MT)))
+  :hints (("Goal" :use (:instance INST-invariant-INST-at (stg 'latch2))
+		  :in-theory (e/d (INST-invariant INST-latch2-inv)
+				  (INST-invariant-INST-at)))))
+
+(defthm latch2-valid-if-INST-in
+    (implies (and (invariant MT MA)
+		  (INST-in i MT) (INST-p i)
+		  (equal (INST-stg i) 'latch2))
+	     (b1p (latch2-valid? (MA-latch2 MA))))
+  :hints (("Goal" :use (:instance INST-invariant-INST-in)
+		  :in-theory (e/d (INST-invariant INST-latch2-inv)
+				  ()))))
+
+; Correct intermediate values of instruction execution can be specified
+; using the instruction entry in a MAETT.  For
+; instance, if instruction I is in latch1, then the latch1-op should
+; hold the operand of instruction I, which can be specified as
+; (INST-op i). This is shown by Lemma latch1-op-INST-op-if-INST-in.
+; In the rest of this file, we give a list of similar lemmas.
+
+;
+; Note: First, we give all lemmas in the same style as
+; latch1-op-INST-op-if-INST-in.  Then we re-state all the lemmas in a
+; different style, starting from latch1-op-INST-op.  In the latter
+; style, we use function INST-at to specify the instruction at a
+; specific latch.
+(defthm latch1-op-INST-op-if-INST-in
+    (implies (and (invariant MT MA)
+		  (MAETT-p MT) (MA-state-p MA)
+		  (INST-in i MT) (INST-p i)
+		  (equal (INST-stg i) 'latch1))
+	     (equal (latch1-op (MA-latch1 MA)) (INST-op i)))
+  :hints (("goal" :in-theory (e/d (INST-INVARIANT INST-LATCH1-INV)
+				  (inst-invariant-INST-at))
+		  :use (:instance inst-invariant-INST-in))))
+
+(defthm latch1-rc-INST-rc-if-INST-in
+    (implies (and (invariant MT MA)
+		  (MAETT-p MT) (MA-state-p MA)
+		  (INST-in i MT) (INST-p i)
+		  (equal (INST-stg i) 'latch1))
+	     (equal (latch1-rc (MA-latch1 MA)) (INST-rc i)))
+  :hints (("goal" :in-theory (e/d (INST-INVARIANT INST-LATCH1-INV)
+				  (inst-invariant-INST-at))
+		  :use (:instance inst-invariant-INST-in))))
+
+(defthm latch1-ra-INST-ra-if-INST-in
+    (implies (and (invariant MT MA)
+		  (MAETT-p MT) (MA-state-p MA)
+		  (INST-in i MT) (INST-p i)
+		  (equal (INST-stg i) 'latch1))
+	     (equal (latch1-ra (MA-latch1 MA)) (INST-ra i)))
+  :hints (("goal" :in-theory (e/d (INST-INVARIANT INST-LATCH1-INV)
+				  (inst-invariant-INST-at))
+		  :use (:instance inst-invariant-INST-in))))
+
+(defthm latch1-rb-INST-rb-if-INST-in
+    (implies (and (invariant MT MA)
+		  (MAETT-p MT) (MA-state-p MA)
+		  (INST-in i MT) (INST-p i)
+		  (equal (INST-stg i) 'latch1))
+	     (equal (latch1-rb (MA-latch1 MA)) (INST-rb i)))
+  :hints (("goal" :in-theory (e/d (INST-INVARIANT INST-LATCH1-INV)
+				  (inst-invariant-INST-at))
+		  :use (:instance inst-invariant-INST-in))))
+
+(defthm latch2-op-INST-op-if-INST-in
+    (implies (and (invariant MT MA)
+		  (MAETT-p MT) (MA-state-p MA)
+		  (INST-in i MT) (INST-p i)
+		  (equal (INST-stg i) 'latch2))
+	     (equal (latch2-op (MA-latch2 MA)) (INST-op i)))
+  :hints (("goal" :in-theory (e/d (INST-INVARIANT INST-LATCH2-INV)
+				  (inst-invariant-INST-at))
+		  :use (:instance inst-invariant-INST-in))))
+
+(defthm latch2-rc-INST-rc-if-INST-in
+    (implies (and (invariant MT MA)
+		  (MAETT-p MT) (MA-state-p MA)
+		  (INST-in i MT) (INST-p i)
+		  (equal (INST-stg i) 'latch2))
+	     (equal (latch2-rc (MA-latch2 MA)) (INST-rc i)))
+  :hints (("goal" :in-theory (e/d (INST-INVARIANT INST-LATCH2-INV)
+				  (inst-invariant-INST-at))
+		  :use (:instance inst-invariant-INST-in))))
+
+(defthm latch2-val1-INST-val1-if-INST-in
+    (implies (and (invariant MT MA)
+		  (MAETT-p MT) (MA-state-p MA)
+		  (INST-in i MT) (INST-p i)
+		  (equal (INST-stg i) 'latch2))
+	     (equal (latch2-ra-val (MA-latch2 MA)) (INST-ra-val i)))
+  :hints (("goal" :in-theory (e/d (INST-INVARIANT INST-LATCH2-INV)
+				  (inst-invariant-INST-at))
+		  :use (:instance inst-invariant-INST-in))))
+
+(defthm latch2-rb-val-INST-rb-val-if-INST-in
+    (implies (and (invariant MT MA)
+		  (MAETT-p MT) (MA-state-p MA)
+		  (INST-in i MT) (INST-p i)
+		  (equal (INST-stg i) 'latch2))
+	     (equal (latch2-rb-val (MA-latch2 MA)) (INST-rb-val i)))
+  :hints (("goal" :in-theory (e/d (INST-INVARIANT INST-LATCH2-INV)
+				  (inst-invariant-INST-at))
+		  :use (:instance inst-invariant-INST-in))))
+
+
+(defthm latch1-op-INST-op
+    (implies (and (invariant MT MA)
+		  (MAETT-p MT) (MA-state-p MA)
+		  (INST-at 'latch1 MT))
+	     (equal (latch1-op (MA-latch1 MA))
+		    (INST-op (INST-at 'latch1 MT))))
+  :hints (("goal" :in-theory (e/d (INST-INVARIANT INST-LATCH1-INV)
+				  (inst-invariant-INST-at))
+		  :use (:instance inst-invariant-INST-at (stg 'latch1)))))
+
+(defthm latch1-rc-INST-rc
+    (implies (and (invariant MT MA)
+		  (MAETT-p MT) (MA-state-p MA)
+		  (INST-at 'latch1 MT))
+	     (equal (latch1-rc (MA-latch1 MA))
+		    (INST-rc (INST-at 'latch1 MT))))
+  :hints (("goal" :in-theory (e/d (INST-INVARIANT INST-LATCH1-INV)
+				  (inst-invariant-INST-at))
+		  :use (:instance inst-invariant-INST-at (stg 'latch1)))))
+
+(defthm latch1-ra-INST-ra
+    (implies (and (invariant MT MA)
+		  (MAETT-p MT) (MA-state-p MA)
+		  (INST-at 'latch1 MT))
+	     (equal (latch1-ra (MA-latch1 MA))
+		    (INST-ra (INST-at 'latch1 MT))))
+  :hints (("goal" :in-theory (e/d (INST-INVARIANT INST-LATCH1-INV)
+				  (inst-invariant-INST-at))
+		  :use (:instance inst-invariant-INST-at (stg 'latch1)))))
+
+(defthm latch1-rb-INST-rb
+    (implies (and (invariant MT MA)
+		  (MAETT-p MT) (MA-state-p MA)
+		  (INST-at 'latch1 MT))
+	     (equal (latch1-rb (MA-latch1 MA))
+		    (INST-rb (INST-at 'latch1 MT))))
+  :hints (("goal" :in-theory (e/d (INST-INVARIANT INST-LATCH1-INV)
+				  (inst-invariant-INST-at))
+		  :use (:instance inst-invariant-INST-at (stg 'latch1)))))
+
+(defthm latch2-op-INST-op
+    (implies (and (invariant MT MA)
+		  (MAETT-p MT) (MA-state-p MA)
+		  (INST-at 'latch2 MT))
+	     (equal (latch2-op (MA-latch2 MA))
+		    (INST-op (INST-at 'latch2 MT))))
+  :hints (("goal" :in-theory (e/d (INST-INVARIANT INST-LATCH2-INV)
+				  (inst-invariant-INST-at))
+		  :use (:instance inst-invariant-INST-at (stg 'latch2)))))
+
+(defthm latch2-rc-INST-rc
+    (implies (and (invariant MT MA)
+		  (MAETT-p MT) (MA-state-p MA)
+		  (INST-at 'latch2 MT))
+	     (equal (latch2-rc (MA-latch2 MA))
+		    (INST-rc (INST-at 'latch2 MT))))
+  :hints (("goal" :in-theory (e/d (INST-INVARIANT INST-LATCH2-INV)
+				  (inst-invariant-INST-at))
+		  :use (:instance inst-invariant-INST-at (stg 'latch2)))))
+
+(defthm latch2-ra-val-INST-ra-val
+    (implies (and (invariant MT MA)
+		  (MAETT-p MT) (MA-state-p MA)
+		  (INST-at 'latch2 MT))
+	     (equal (latch2-ra-val (MA-latch2 MA))
+		    (INST-ra-val (INST-at 'latch2 MT))))
+  :hints (("goal" :in-theory (e/d (INST-INVARIANT INST-LATCH2-INV)
+				  (inst-invariant-INST-at))
+		  :use (:instance inst-invariant-INST-at (stg 'latch2)))))
+
+(defthm latch2-rb-val-INST-rb-val
+    (implies (and (invariant MT MA)
+		  (MAETT-p MT) (MA-state-p MA)
+		  (INST-at 'latch2 MT))
+	     (equal (latch2-rb-val (MA-latch2 MA))
+		    (INST-rb-val (INST-at 'latch2 MT))))
+  :hints (("goal" :in-theory (e/d (INST-INVARIANT INST-LATCH2-INV)
+				  (inst-invariant-INST-at))
+		  :use (:instance inst-invariant-INST-at (stg 'latch2)))))
+
+
diff --git a/books/workshops/2000/manolios/pipeline/trivial/sawada-model/ihs.lisp b/books/workshops/2000/manolios/pipeline/trivial/sawada-model/ihs.lisp
new file mode 100644
index 0000000..1117cbc
--- /dev/null
+++ b/books/workshops/2000/manolios/pipeline/trivial/sawada-model/ihs.lisp
@@ -0,0 +1,155 @@
+(in-package "ACL2")
+
+;; [Jared] turning this book into an include-book since it is identical to
+;; 1999/pipeline/ihs
+
+(include-book "workshops/1999/pipeline/ihs" :dir :system)
+
+;; (deflabel before-loading-ihs)
+;; (include-book "../../../../../../ihs/ihs-definitions")
+;; (include-book "../../../../../../ihs/ihs-lemmas")
+;; (deflabel after-loading-ihs)
+
+;; (deftheory default-IHS-incompatibles
+;;     '(oddp evenp floor mod rem truncate expt
+;;       loghead logtail logior lognot logand logand
+;;       logeqv logorc1 logorc2 logandc1 logandc2 logcount
+;;       lognand lognor logxor))
+
+;; (in-theory
+;;  (set-difference-theories (current-theory :here)
+;; 	  (set-difference-theories  (universal-theory 'after-loading-IHS)
+;; 				    (universal-theory 'before-loading-IHS))))
+
+;; (in-theory (disable default-ihs-incompatibles))
+;; (in-theory
+;;  (enable
+;;   ihs-math				; From "math-lemmas"
+;;   quotient-remainder-rules		; From "quotient-remainder-lemmas"
+;;   logops-lemmas-theory))		; From "logops-lemmas"
+
+;; (in-theory (disable (force)))
+
+;; (in-theory (disable
+;; 	    (:generalize MOD-X-Y-=-X+Y-for-rationals)
+;; 	    (:generalize MOD-X-Y-=-X-for-rationals)
+;; 	    (:generalize MOD-=-0)
+;; 	    (:generalize FLOOR-TYPE-4)
+;; 	    (:generalize FLOOR-TYPE-3)
+;; 	    (:generalize FLOOR-TYPE-2)
+;; 	    (:generalize FLOOR-TYPE-1)
+;; 	    (:generalize FLOOR-BOUNDED-BY-/)
+;; 	    (:generalize FLOOR-=-X/Y)))
+
+
+;; (defun weak-defword-tuple-p (tuple)
+;;   (or (and (true-listp tuple)
+;; 	   (or (equal (length tuple) 3)
+;; 	       (equal (length tuple) 4))
+;; 	   (symbolp (first tuple)))
+;;       (er hard 'defword
+;; 	  "A field designator for DEFWORD must be a list, the first ~
+;;              element of which is a symbol, the second a positive integer, ~
+;;              and the third a non-negative integer.  If a fouth element is ~
+;;              provided it must be a string.  This object violates these ~
+;;              constraints: ~p0" tuple)))
+
+;; (defun weak-defword-tuple-p-listp (struct)
+;;   (cond
+;;    ((null struct) t)
+;;    (t (and (weak-defword-tuple-p (car struct))
+;; 	   (weak-defword-tuple-p-listp (cdr struct))))))
+
+;; (defun weak-defword-struct-p (struct)
+;;   (cond
+;;    ((true-listp struct) (weak-defword-tuple-p-listp struct))
+;;    (t (er hard 'defword
+;; 	  "The second argument of DEFWORD must be a true list. ~
+;;            This object is not a true list: ~p0" struct))))
+
+;; (defun weak-defword-guards (struct)
+;;   (weak-defword-struct-p struct))
+
+;; (defun defword-tuple-typecheck-thms (tuple)
+;;   (let ((tuple-thm-name
+;; 	 (pack-intern (first tuple) "DEFWORD-TUPLE-" (first tuple))))
+;;     `(local (defthm ,tuple-thm-name
+;; 		(and
+;; 		 (integerp ,(second tuple))
+;; 		 (> ,(second tuple) 0)
+;; 		 (integerp ,(third tuple))
+;; 		 (>= ,(third tuple) 0)
+;; 		 (implies ,(fourth tuple) (stringp ,(fourth tuple))))
+;; 	      :rule-classes nil))))
+
+
+;; (defun defword-struct-typecheck-thms (struct)
+;;   (if (endp struct) nil
+;;       (cons (defword-tuple-typecheck-thms (car struct))
+;; 	    (defword-struct-typecheck-thms (cdr struct)))))
+
+;; (defun type-check-thms
+;;     (name struct conc-name set-conc-name keyword-updater doc)
+;;   (append
+;;    (list
+;;     `(local (defthm defword-symbolp-name (symbolp ',name)
+;; 	      :rule-classes nil
+;; 	      :doc "Defword name should be a symbol."))
+;;     `(local (defthm defword-symbolp-conc-name (symbolp ',conc-name)
+;; 	      :rule-classes nil
+;; 	      :doc "Defword conc-name should be a symbol."))
+;;     `(local (defthm defword-symbolp-set-conc-name (symbolp ',set-conc-name)
+;; 	      :rule-classes nil
+;; 	      :doc "Defword set-conc-name should be a symbol."))
+;;     `(local
+;;       (defthm defword-symbolp-keyword-updater (symbolp ',keyword-updater)
+;; 	:rule-classes nil
+;; 	:doc "Defword keyword-updater should be a symbol."))
+;;     `(local (defthm defword-stringp-doc
+;; 		(implies ',doc (stringp ',doc))
+;; 	      :rule-classes nil
+;; 	      :doc "Defword doc should be a string.")))
+;;    (defword-struct-typecheck-thms struct)))
+
+
+;; ;; This version of defword postpones the type checking of arguments until
+;; ;; macro expansion is completed.  Because the original deword checks
+;; ;; types of arguments before expanding macro, some defword expressions
+;; ;; are rejected even if it can be considered as a legitimate defword
+;; ;; expression. For instance,
+;; ;; (defword new-word ((field1 *field1-pos* *field1-width*)
+;; ;;                    (field2 *field2-pos* *field2-width*)))
+;; ;; is rejected because *field1-pos* and other constants are not
+;; ;; integers.
+;; (defmacro defword* (name struct &key conc-name set-conc-name keyword-updater
+;; 			 doc)
+;;   (cond
+;;    ((not (weak-defword-guards struct)))
+;;    (t
+;;     (let*
+;;       ((conc-name (if conc-name
+;;                       conc-name
+;;                     (pack-intern name name "-")))
+;;        (set-conc-name (if set-conc-name
+;;                           set-conc-name
+;;                         (pack-intern name "SET-" name "-")))
+;;        (keyword-updater (if keyword-updater
+;; 			    keyword-updater
+;; 			  (pack-intern name "UPDATE-" name)))
+;;        (type-check-thms
+;; 	(type-check-thms name struct conc-name set-conc-name
+;; 			 keyword-updater doc))
+;;        (accessor-definitions
+;;         (defword-accessor-definitions 'RDB name conc-name struct))
+;;        (updater-definitions
+;;         (defword-updater-definitions 'WRB name set-conc-name struct))
+;;        (field-names (strip-cars struct)))
+
+;;       `(ENCAPSULATE ()                  ;Only to make macroexpansion pretty.
+;;          (DEFLABEL ,name ,@(if doc `(:DOC ,doc) nil))
+;; 	 ,@type-check-thms
+;;          ,@accessor-definitions
+;;          ,@updater-definitions
+;;          ,(defword-keyword-updater
+;; 	    name keyword-updater set-conc-name field-names))))))
+
diff --git a/books/workshops/2000/manolios/pipeline/trivial/sawada-model/model.lisp b/books/workshops/2000/manolios/pipeline/trivial/sawada-model/model.lisp
new file mode 100644
index 0000000..c9ea05d
--- /dev/null
+++ b/books/workshops/2000/manolios/pipeline/trivial/sawada-model/model.lisp
@@ -0,0 +1,374 @@
+(in-package "ACL2")
+
+(include-book "basic-def")
+
+(deflabel begin-model)
+
+; Basic Pipeline Design
+; Our example machine is very simple.  It consists of a program counter,
+; a register file, the memory, pipeline latches latch1 and latch2.
+; The programmer visible components are the program counter, the register
+; file and the memory.  It can execute two types of instructions, ADD
+; and SUB.  The format of an instruction is as shown here:
+;           --------------------------------
+;          | op    |  RC   |  RA   |   RB  |
+;           --------------------------------
+;           15    12 11    8 7     4 3     0
+;
+; where RC, RA and RB are operand register specifiers.  There are only
+; two valid opcodes 0 (ADD) and 1 (SUB).  An instruction without a
+; valid opcode is considered as a NOP.  The ADD instruction reads
+; registers specified by RA and RB, adds the values and writes the
+; result back into the register specified by RC.  The SUB subtracts RB
+; from RA.  Every machine cycle the program counter is incremented by
+; 1.  No exceptions and no interrupts occur.  There is one external
+; input to the machine.  If this input signal is on, the machine may
+; fetch a new instruction from the memory.  Pipeline flushing can be
+; done by running the machine with 0's as its inputs.
+;
+; We define this machine at two levels: instruction-set architecture
+; and micro-architecture.
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; ISA Definition
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; Description of ISA
+; The ISA state consists of only programmer visible states, that is,
+; the program counter, register file and the memory.
+; ISA behavior is specified by ISA-step.  Depending on the operand,
+; it executes ADD or SUB operation.
+
+; Definition of the ISA state.
+;
+; Note: For the detail of the definition with defstructure, please
+; refer to the public ACL2 book data-structures/structures.lisp.
+; Briefly speaking, an expression (ISA-state PC REGS MEM) returns
+; an ISA state whose program counter, register file and memory are PC,
+; REGS and MEM, respectively.  The pc value of an ISA state, ISA, can
+; be obtained by (ISA-pc ISA).
+(defstructure ISA-state
+  (pc   (:assert (addr-p pc)   :rewrite))
+  (regs (:assert (regs-p regs) :rewrite))
+  (mem  (:assert (mem-p mem)   :rewrite))
+  (:options :guards  (:conc-name ISA-)))
+
+(deflabel begin-ISA-def)
+
+; Definition of the effect of an ADD instruction.
+(defun ISA-add (rc ra rb ISA)
+  (declare (xargs :guard (and (rname-p rc) (rname-p ra) (rname-p rb)
+			      (ISA-state-p ISA))))
+  (ISA-state (addr (1+ (ISA-pc ISA)))
+	     (write-reg (word (+ (read-reg ra (ISA-regs ISA))
+				 (read-reg rb (ISA-regs ISA))))
+			rc (ISA-regs ISA))
+	     (ISA-mem ISA)))
+
+; Definition of the effect of an SUB instruction.
+(defun ISA-sub (rc ra rb ISA)
+  (declare (xargs :guard (and (rname-p rc) (rname-p ra) (rname-p rb)
+			      (ISA-state-p ISA))))
+  (ISA-state (addr (1+ (ISA-pc ISA)))
+	     (write-reg (word (- (read-reg ra (ISA-regs ISA))
+				 (read-reg rb (ISA-regs ISA))))
+			rc (ISA-regs ISA))
+	     (ISA-mem ISA)))
+
+; Definition of NOP. It only increments the program counter.
+(defun ISA-default (ISA)
+  (declare (xargs :guard (ISA-state-p ISA)))
+  (ISA-state (addr (1+ (ISA-pc ISA)))
+	     (ISA-regs ISA)
+	     (ISA-mem ISA)))
+
+; Next ISA state function.  It takes the current ISA state and returns
+; the ISA state after executing one instruction.  This function is a
+; simple dispatcher of corresponding functions depending on the
+; instruction type.
+(defun ISA-step (ISA)
+  (declare (xargs :guard (ISA-state-p ISA)))
+  (let ((inst (read-mem (ISA-pc ISA) (ISA-mem ISA))))
+    (let ((op (op-field inst))
+	  (rc (rc-field inst))
+	  (ra (ra-field inst))
+	  (rb (rb-field inst)))
+      (case op
+	(0 (ISA-add rc ra rb ISA)) ; add
+	(1 (ISA-sub rc ra rb ISA)) ; sub
+	(otherwise (ISA-default ISA))))))
+
+; N step ISA function.  It returns the ISA state after executing n
+; instructions from the initial state, ISA.
+(defun ISA-stepn (ISA n)
+  (declare (xargs :guard (and (ISA-state-p ISA) (integerp n) (<= 0 n))))
+  (if (zp n) ISA (ISA-stepn (ISA-step ISA) (1- n))))
+
+(deflabel end-ISA-def)
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; MA Definition
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; Definition of MA states
+;
+; Definition of pipeline latch latch1.
+(defstructure latch1
+  (valid? (:assert (bitp valid?) :rewrite))
+  (op     (:assert (opcd-p op)   :rewrite))
+  (rc     (:assert (rname-p rc)  :rewrite))
+  (ra     (:assert (rname-p ra)  :rewrite))
+  (rb     (:assert (rname-p rb)  :rewrite))
+  (:options :guards))
+
+; Definition of pipeline latch latch2.
+(defstructure latch2
+  (valid?  (:assert (bitp valid?)   :rewrite))
+  (op      (:assert (opcd-p op)     :rewrite))
+  (rc      (:assert (rname-p rc)    :rewrite))
+  (ra-val  (:assert (word-p ra-val) :rewrite))
+  (rb-val  (:assert (word-p rb-val) :rewrite))
+  (:options :guards))
+
+; Definition of pipelined micro-architecture.
+(defstructure MA-state
+  (pc     (:assert (addr-p pc)       :rewrite (:rewrite (acl2-numberp pc))))
+  (regs   (:assert (regs-p regs)     :rewrite))
+  (mem    (:assert (mem-p mem)       :rewrite))
+  (latch1 (:assert (latch1-p latch1) :rewrite))
+  (latch2 (:assert (latch2-p latch2) :rewrite))
+  (:options :guards  (:conc-name MA-)))
+
+; Defines the signal supplied to the micro-architectural behavioral
+; function.  We assume that the micro-architecture takes one bit
+; input, which turn on and off instruction fetching.
+(defun MA-sig-p (sig)
+  (declare (xargs :guard t))
+  (bitp sig))
+
+; List of sig
+(deflist MA-sig-listp (l)
+  (declare (xargs :guard t))
+  MA-sig-p)
+
+(deflabel begin-MA-def)
+; The definition of ALU.  The ALU takes opcode and two operands,
+; and outputs the result.
+(defun ALU-output (op val1 val2)
+  (declare (xargs :guard (and (opcd-p op) (word-p val1) (word-p val2))))
+  (cond ((equal op 0) (word (+ val1 val2)))
+	((equal op 1) (word (- val1 val2)))
+	(t 0)))
+
+; The behavior of the register file.  If the latch2 contains an ADD or
+; SUB instruction, the register specified by latch2-rc is updated by
+; the output from the ALU.  Otherwise, the register file is unchanged.
+(defun step-regs (MA)
+  (declare (xargs :guard (MA-state-p MA)))
+  (let ((latch2 (MA-latch2 MA)))
+    (b-if (b-and (latch2-valid? latch2)
+		 (b-ior (bv-eqv *opcode-size* (latch2-op latch2) 0)
+			(bv-eqv *opcode-size* (latch2-op latch2) 1)))
+	  (write-reg (ALU-output (latch2-op latch2)
+				 (latch2-ra-val latch2)
+				 (latch2-rb-val latch2))
+		     (latch2-rc latch2)
+		     (MA-regs MA))
+	  (MA-regs MA))))
+
+; The dependency check.  If there is a true (RAW) dependency
+; between the instructions at latch1 and latch2, the instruction at
+; latch1 should stall until the instruction at latch2 completes.  We
+; check whether the destination register of the instruction at latch2
+; is one of the source registers of the instruction at latch1.
+(defun dependency? (MA)
+  (declare (xargs :guard (MA-state-p MA)))
+  (let ((latch1 (MA-latch1 MA))
+	(latch2 (MA-latch2 MA)))
+    (b-ior (bv-eqv *rname-size* (latch1-ra latch1) (latch2-rc latch2))
+	   (bv-eqv *rname-size* (latch1-rb latch1) (latch2-rc latch2)))))
+
+(defthm bitp-dependency
+    (bitp (dependency? MA)))
+
+; The stall condition.  If both latch1 and latch2 contain valid
+; instructions, and there are dependencies between the two
+; instructions, the instruction at latch1 is stalled.
+(defun stall-cond? (MA)
+  (declare (xargs :guard (MA-state-p MA)))
+  (b-and (latch1-valid? (MA-latch1 MA))
+	 (b-and (latch2-valid? (MA-latch2 MA))
+		(dependency? MA))))
+
+(defthm bitp-stall-cond
+    (bitp (stall-cond? MA)))
+
+; Next state function for pipeline latch latch2.  The instruction at
+; latch1 advances to latch2, only if stall-cond? is off.  Note that
+; the rest of the fields of latch2 are updated anyway. Is it okay?
+; The answer is yes.  The instruction at latch2 always complete, and
+; the instruction at latch1 may or may not advance to latch2.  If
+; instruction at latch1 stalls, latch2 will hold a bubble in the next
+; cycle.  In this case, we don't care the values the fields of latch2
+; except for latch2-valid?, which indicates whether the content of
+; latch2 is a bubble or not.
+(defun step-latch2 (MA)
+  (declare (xargs :guard (MA-state-p MA)))
+  (let ((latch1 (MA-latch1 MA))
+	(latch2 (MA-latch2 MA)))
+    (latch2 (b-and (latch1-valid? latch1)
+		   (b-nand (dependency? MA) (latch2-valid? latch2)))
+	    (latch1-op latch1)
+	    (latch1-rc latch1)
+	    (read-reg (latch1-ra latch1) (MA-regs MA))
+	    (read-reg (latch1-rb latch1) (MA-regs MA)))))
+
+
+; This function defines how latch1 is updated. If the stall condition
+; is true, latch1 is not updated.  If latch1 is currently empty or the
+; stall condition is false, and if the given sig is true, we fetch an
+; instruction.  Sig is an external input that directs the processor to
+; fetch a new instruction.
+(defun step-latch1 (MA sig)
+  (declare (xargs :guard (and (MA-state-p MA) (MA-sig-p sig))))
+  (let ((latch1 (MA-latch1 MA))
+	(inst (read-mem (MA-pc MA) (MA-mem MA))))
+    (latch1 (b-ior sig (stall-cond? MA))
+	    (b-if (stall-cond? MA) (latch1-op latch1) (op-field inst))
+	    (b-if (stall-cond? MA) (latch1-rc latch1) (rc-field inst))
+	    (b-if (stall-cond? MA) (latch1-ra latch1) (ra-field inst))
+	    (b-if (stall-cond? MA) (latch1-rb latch1) (rb-field inst)))))
+
+
+; The condition whether a new instruction is fetched.
+(defun fetch-inst? (MA sig)
+  (declare (xargs :guard (and (MA-state-p MA) (MA-sig-p sig))))
+  (b-and sig
+	 (b-nand (latch1-valid? (MA-latch1 MA))
+		 (b-and (latch2-valid? (MA-latch2 MA))
+			(dependency? MA)))))
+
+(defthm bitp-fetch-inst?
+    (bitp (fetch-inst? MA sig)))
+
+; Function step-pc defines how the program counter is updated.
+(defun step-pc (MA sig)
+  (declare (xargs :guard (and (MA-state-p MA) (MA-sig-p sig))))
+  (b-if (fetch-inst? MA sig)
+	(addr (1+ (MA-pc MA)))
+	(MA-pc MA)))
+
+; MA-step defines how the MA state is updated every clock cycle.  The
+; memory does not change in our model.  The behavior of other
+; components is specified by the corresponding step functions.
+(defun MA-step (MA sig)
+  (declare (xargs :guard (and (MA-state-p MA) (MA-sig-p sig))))
+  (MA-state (step-pc MA sig)
+	    (step-regs MA)
+	    (MA-mem MA)
+	    (step-latch1 MA sig)
+	    (step-latch2 MA)))
+
+; MA-stepn returns the MA state after n clock cycles of MA execution.
+; The argument MA is the initial state, and sig-list specifies the
+; series of inputs.
+(defun MA-stepn (MA sig-list n)
+  (declare (xargs :guard (and (MA-state-p MA) (MA-sig-listp sig-list)
+			      (integerp n) (<= 0 n)
+			      (<= n (len sig-list)))))
+  (if (zp n)
+      MA
+      (MA-stepn (MA-step MA (car sig-list)) (cdr sig-list) (1- n))))
+
+(deflabel end-MA-def)
+
+(deftheory ISA-def
+    (set-difference-theories
+     (set-difference-theories (function-theory 'end-ISA-def)
+			      (function-theory 'begin-ISA-def))
+     '(ISA-stepn)))
+
+(deftheory MA-def
+    (set-difference-theories
+     (set-difference-theories (function-theory 'end-MA-def)
+			      (function-theory 'begin-MA-def))
+     '(MA-stepn)))
+
+(in-theory (disable ISA-def MA-def MA-sig-p))
+
+;;;;;;;; Type proofs ;;;;;;;;
+(defthm ISA-state-p-ISA-step
+    (implies (ISA-state-p ISA) (ISA-state-p (ISA-step ISA)))
+  :hints (("Goal" :in-theory (enable ISA-step ISA-add ISA-sub ISA-default))))
+
+(defthm ISA-state-p-ISA-stepn
+    (implies (ISA-state-p ISA) (ISA-state-p (ISA-stepn ISA n))))
+
+(defthm addr-p-step-pc
+    (implies (MA-state-p MA) (addr-p (step-pc MA sig)))
+  :hints (("Goal" :in-theory (enable step-pc))))
+
+(defthm word-p-ALU-output
+    (implies (and (opcd-p op) (word-p val1) (word-p val2))
+	     (word-p (ALU-output op val1 val2)))
+  :hints (("Goal" :in-theory (enable ALU-output))))
+
+(defthm regs-p-step-regs
+    (implies (MA-state-p MA) (regs-p (step-regs MA)))
+  :hints (("Goal" :in-theory (enable step-regs))))
+
+(defthm latch1-p-step-latch1
+    (implies (and (MA-state-p MA) (MA-sig-p sig))
+	     (latch1-p (step-latch1 MA sig)))
+  :hints (("Goal" :in-theory (enable step-latch1 MA-sig-p))))
+
+(defthm latch1-p-step-latch2
+    (implies (and (MA-state-p MA) (MA-sig-p sig))
+	     (latch2-p (step-latch2 MA)))
+  :hints (("Goal" :in-theory (enable step-latch2 MA-sig-p))))
+
+(defthm MA-state-p-MA-step
+    (implies (and (MA-state-p MA) (MA-sig-p sig))
+	     (MA-state-p (MA-step MA sig)))
+  :hints (("Goal" :in-theory (enable MA-step))))
+
+(defthm MA-state-p-MA-stepn
+    (implies (and (MA-state-p MA) (MA-sig-listp sig-list)
+		  (<= n (len sig-list)))
+	     (MA-state-p (MA-stepn MA sig-list n))))
+
+;;;  Predicates for correctness
+
+; The projection function from an MA state to the corresponding ISA
+; state. Function proj strips off pipeline latches from the MA state.
+(defun proj (MA)
+  (declare (xargs :guard (MA-state-p MA)))
+  (ISA-state (MA-pc MA) (MA-regs MA) (MA-mem MA)))
+
+; (flushed? MA) is true if the pipeline of MA is flushed.
+(defun flushed? (MA)
+  (b-nor (latch1-valid? (MA-latch1 MA))
+	 (latch2-valid? (MA-latch2 MA))))
+
+
+#|
+We will prove a following lemma for operational correctness:
+(defthm correctness
+    (implies (and (MA-state-p MA)
+		  (MA-sig-listp sig-list)
+		  (<= n (len sig-list))
+		  (b1p (flushed? MA))
+		  (b1p (flushed? (MA-stepn MA sig-list n))))
+	     (equal (proj (MA-stepn MA sig-list n))
+		    (ISA-stepn (proj MA)
+			       (num-insts MA sig-list n)))))
+
+where num-insts calculates the nunber of instructions executed in the
+n cycles of MA execution.  We also prove the liveness property with:
+
+(defthm liveness
+    (implies (MA-state-p MA)
+	     (b1p (flushed? (MA-stepn MA
+				      (zeros (flush-cycles MA))
+				      (flush-cycles MA)))))).
+
+Function flush-cycles calculates the number of cycles to flush the pipeline.
+|#
diff --git a/books/workshops/2000/manolios/pipeline/trivial/sawada-model/proof.lisp b/books/workshops/2000/manolios/pipeline/trivial/sawada-model/proof.lisp
new file mode 100644
index 0000000..1ef1071
--- /dev/null
+++ b/books/workshops/2000/manolios/pipeline/trivial/sawada-model/proof.lisp
@@ -0,0 +1,938 @@
+(in-package "ACL2")
+
+
+;(include-book "utils")
+(include-book "basic-def")
+(include-book "model")
+(include-book "table-def")
+(include-book "basic-lemmas")
+
+(deflabel begin-proof)
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; In this file, we prove our correctness criterion. First we prove that
+; our invariant conditions hold for all micro-architectural states
+; reachable from initial states.  Then we prove the correctness of
+; the criterion using the invariant.
+;
+; We verify two lemmas about invariant conditions: invariant-init-MT
+; and invariant-step.  Lemma invariant-init-MT shows that invariant
+; conditions are true for all initial states, while lemma
+; invariant-step shows that conditions are invariantly held during
+; the micro-architecture machine transitions.
+;
+; Predicate invariant is a conjunction of seven conditions,
+; pc-match-p, regs-match-p, mem-match-p, ISA-chain-p,
+; MT-inst-invariant, MT-contains-all-insts, and MT-in-order-p.  We
+; prove that individual conditions are held at the initial states, and
+; that they are preserved over the machine state transition.  For instance,
+; pc-match-p-init-MT shows that condition pc-match-p is true for
+; initial states.  And lemma pc-match-p-MT-step shows that pc-match-p
+; is preserved during machine transitions.
+;
+
+;
+;;;;;;; Proof of pc-match-p ;;;
+; PC-match-p is true for initial states.
+(defthm pc-match-p-init-MT
+    (pc-match-p (init-MT MA) MA)
+  :hints (("Goal" :in-theory (enable pc-match-p init-MT MT-pc))))
+
+(encapsulate nil
+(local
+(defthm pc-match-p-MT-step-induction
+    (implies (and (equal (trace-pc trace ISA) (MA-pc MA))
+		  (INST-listp trace)
+		  (MAETT-p MT) (MA-state-p MA))
+	     (equal (trace-pc (step-trace trace MA sig ISA) ISA)
+		    (step-pc MA sig)))
+  :hints (("Goal" :in-theory (enable STEP-PC ISA-STEP
+				     ISA-add ISA-sub ISA-default)
+		  :expand (TRACE-PC (LIST (NEW-INST ISA))
+					    ISA)))))
+; PC-match-p is preserved during MA state transitions.
+(defthm pc-match-p-MT-step
+    (implies (and (invariant MT MA)
+		  (MAETT-p MT) (MA-state-p MA))
+	     (pc-match-p (MT-step MT MA sig) (MA-step MA sig)))
+  :hints (("Goal" :in-theory (enable pc-match-p MT-step MA-step
+				     invariant MT-pc))))
+)
+
+;;;;;;; Proof of regs-match-p
+; Register file is in the correct state in the initial states.
+(defthm regs-match-p-init-MT
+    (regs-match-p (init-MT MA) MA)
+  :hints (("Goal" :in-theory (enable init-MT regs-match-p MT-regs))))
+
+(encapsulate nil
+(local
+(defthm INST-pre-ISA-INST-at-latch2-induction
+    (implies (and (invariant MT MA)
+		  (MAETT-p MT) (MA-state-p MA)
+		  (subtrace-p trace MT) (INST-listp trace)
+		  (trace-INST-at 'latch2 trace))
+	     (equal (ISA-regs (INST-pre-ISA (trace-INST-at 'latch2 trace)))
+		    (trace-regs trace (INST-pre-ISA (car trace)))))
+  :hints (("subgoal *1/3" :cases ((consp (cdr trace))))
+	  ("subgoal *1/2" :use (:instance stages-of-inst (i (car trace)))))))
+
+
+(local
+(defthm INST-pre-ISA-INST-at-latch2-help
+    (implies (and (invariant MT MA)
+		  (MAETT-p MT) (MA-state-p MA)
+		  (INST-at 'latch2 MT))
+	     (equal (ISA-regs (INST-pre-ISA (INST-at 'latch2 MT)))
+		    (MT-regs MT)))
+  :hints (("Goal" :in-theory (enable MT-regs INST-at)
+		  :cases ((consp (MT-trace MT)))))
+  :rule-classes nil))
+
+
+; If an instruction I is in stage latch2, the register file of the MA
+; state looks like the register file in the pre-ISA state  I.  This is
+; because the register file reflects the result of all
+; retired instructions, while the result of partially executed
+; instructions are not written in the register file.
+(defthm INST-pre-ISA-INST-at-latch2
+    (implies (and (invariant MT MA)
+		  (MAETT-p MT) (MA-state-p MA)
+		  (INST-at 'latch2 MT))
+	     (equal (ISA-regs (INST-pre-ISA (INST-at 'latch2 MT)))
+		    (MA-regs MA)))
+  :hints (("Goal" :in-theory (enable invariant regs-match-p)
+		  :use (:instance INST-pre-ISA-INST-at-latch2-help))))
+)
+
+(encapsulate nil
+(local
+(defthm MT-regs-MT-step-if-latch2-valid-help-help
+    (implies (and (INST-listp trace)
+		  (not (trace-INST-at 'latch2 trace))
+		  (not (trace-INST-at 'retire trace)))
+	     (equal (trace-regs (step-trace trace MA sig ISA) ISA)
+		    (ISA-regs ISA)))
+  :hints (("Goal" :cases ((consp trace))))))
+
+
+(local
+(defthm MT-regs-MT-step-if-latch2-valid-help
+    (implies (and (invariant MT MA)
+		  (MAETT-p MT) (MA-state-p MA)
+		  (subtrace-p trace MT)
+		  (INST-listp trace)
+		  (trace-INST-at 'latch2 trace))
+	     (equal (trace-regs (step-trace trace MA sig ISA) ISA)
+		    (ISA-regs (INST-post-ISA (trace-INST-at 'latch2 trace)))))
+  :hints (("Subgoal *1/6" :use (:instance stages-of-inst (i (car trace)))))))
+
+
+; The correct register file state for the next cycle is defined here.
+; If instruction I is at latch2, I retires in this cycle and the
+; effect of I appears in the register file.
+(defthm MT-regs-MT-step-if-latch2-valid
+    (implies (and (invariant MT MA)
+		  (MAETT-p MT) (MA-state-p MA)
+		  (INST-at 'latch2 MT))
+	     (equal (MT-regs (MT-step MT MA sig))
+		    (ISA-regs (INST-post-ISA (INST-at 'latch2 MT)))))
+  :hints (("Goal" :in-theory (enable MT-regs INST-at MT-step))))
+)
+
+; The effect of ISA execution of instruction I is described by this
+; lemma.  If instruction is add (0) or sub (1), the destination register
+; will contain the result of the instruction.  If the instruction
+; is a NOP, the register file is unchanged.
+(defthm ISA-regs-INST-post-ISA
+    (implies (and (invariant MT MA)
+		  (MAETT-p MT) (MA-state-p MA)
+		  (INST-in i MT) (INST-p i))
+	     (equal (ISA-regs (ISA-step (INST-pre-ISA i)))
+		    (if (or (equal (INST-op i) 0) (equal (INST-op i) 1))
+			(write-reg (INST-result i) (INST-rc i)
+				   (ISA-regs (INST-pre-ISA i)))
+			(ISA-regs (INST-pre-ISA i)))))
+  :hints (("Goal" :in-theory (enable ISA-step ISA-add ISA-sub ISA-default
+				     INST-attrb ALU-output))))
+(in-theory (disable ISA-regs-INST-post-ISA))
+
+
+(encapsulate nil
+(local
+(defthm MT-regs-MT-step-induction
+    (implies (and (INST-listp trace) (not (trace-INST-at 'latch2 trace)))
+	     (equal (trace-regs (step-trace trace MA sig ISA) ISA)
+		    (trace-regs trace ISA)))
+  :hints (("Goal" :expand (TRACE-REGS (CONS (STEP-INST (CAR TRACE) MA)
+                            (STEP-TRACE (CDR TRACE)
+                                        MA SIG (INST-POST-ISA (CAR TRACE))))
+                      ISA)))))
+
+
+; If there is no instruction at latch2, the register file in MA is not
+; updated in this cycle.  Correct register file states calculated from the
+; MAETT does not change.
+(defthm MT-regs-MT-step
+    (implies (and (MAETT-p MT) (not (INST-at 'latch2 MT)))
+	     (equal (MT-regs (MT-step MT MA sig))
+		    (MT-regs MT)))
+  :hints (("Goal" :in-theory (enable MT-regs MT-step
+				     INST-at))))
+)
+
+(encapsulate nil
+; This is a help lemma.
+(local
+(defthm MT-regs-MA-regs
+    (implies (and (invariant MT MA)
+		  (MAETT-p MT) (MA-state-p MA))
+	     (equal (equal (MT-regs MT) (MA-regs MA)) t))
+  :hints (("Goal" :in-theory (enable invariant regs-match-p)))))
+
+
+; Finally, we prove that predicate regs-match-p is preserved during MA
+; machine cycles.  Predicate regs-match-p holds after one MA  machine cycle
+; of execution.
+(defthm regs-match-p-MT-step
+    (implies (and (invariant MT MA)
+		  (MAETT-p MT) (MA-state-p MA))
+	     (regs-match-p (MT-step MT MA sig) (MA-step MA sig)))
+  :hints (("Goal" :in-theory (enable regs-match-p MA-step step-regs
+				     ISA-regs-INST-post-ISA
+				     lift-b-ops bv-eqv-iff-equal
+				     INST-result)
+		  :cases ((b1p (latch2-valid? (MA-latch2 MA)))))))
+)
+
+;;;;;;; Proof of mem-match-p
+; Predicate mem-match-p is true for the initial states.
+(defthm mem-match-p-init-MT
+    (mem-match-p (init-MT MA) MA)
+  :hints (("Goal" :in-theory (enable mem-match-p))))
+
+; Predicate mem-match-p is preserved during MA machines state transitions.
+(defthm mem-match-p-MT-step
+    (implies (and (invariant MT MA)
+		  (MAETT-p MT) (MA-state-p MA))
+	     (mem-match-p (MT-step MT MA sig) (MA-step MA sig)))
+  :hints (("Goal" :in-theory (enable mem-match-p MA-STEP
+				     invariant))))
+
+;;;;;;; Proof of ISA-chain-p
+; ISA-chain-p is true for initial tables.
+(defthm ISA-chain-p-init-MT
+    (ISA-chain-p (init-MT MA))
+  :hints (("Goal" :in-theory (enable ISA-chain-p init-MT))))
+
+(encapsulate nil
+(local
+(defthm ISA-chain-p-step-MT-induction
+    (implies (and (INST-listp trace) (ISA-chain-trace-p trace ISA))
+	     (ISA-chain-trace-p (step-trace trace MA sig ISA) ISA))))
+
+; And it is also preserved during MAETT updates.
+(defthm ISA-chain-p-step-MT
+    (implies (and (invariant MT MA)
+		  (MAETT-p MT))
+	     (ISA-chain-p (MT-step MT MA sig)))
+  :hints (("Goal" :in-theory (enable ISA-chain-p MT-step invariant
+				     MAETT-p))))
+)
+
+;;;;;; MT-inst-invariant
+
+; MT-inst-invariant are true for initial states.
+(defthm MT-inst-invariant-init-MT
+    (MT-inst-invariant (init-MT MA) MA)
+  :hints (("Goal" :in-theory (enable MT-inst-invariant init-MT
+				     trace-INST-invariant))))
+
+
+; Proof of MT-inst-invariant-MT-step.
+;
+; MT-inst-invariant checks recursively every instruction in the MAETT
+; satisfies predicate inst-invariant.  Predicate inst-invariant
+; represents the conditions that each instructions should satisfy,
+; depending on the current stage.
+; We prove that every instruction invariantly satisfy inst-invariant,
+; and then prove the lemma MT-inst-invariant-MT-step using induction.
+;
+; The check for individual instructions needs to consider two cases:
+; the case in which the instruction is a newly fetched instruction,
+; and the case in which the instruction is in the current MAETT.  The
+; first case is proven as lemma inst-invariant-new-INST, and the
+; second case as INST-invariant-step-INST.
+;
+
+; Inst-invariant-new-INST shows that inst-invariant is true for
+; the instruction entry (new-INST (ISA-before nil MT)), which
+; represents the newly fetched instruction.
+(defthm inst-invariant-new-INST
+    (implies (and (invariant MT MA)
+		  (MAETT-p MT) (MA-state-p MA)
+		  (b1p (fetch-inst? MA sig)))
+	     (inst-invariant (new-INST (ISA-before nil MT))
+			      (MA-step MA sig)))
+  :hints (("Goal" :in-theory (enable new-INST inst-invariant
+				     INST-LATCH1-INV fetch-inst?
+				     stall-cond?
+				     MA-STEP step-latch1 lift-b-ops
+				     INST-attrb))))
+
+
+; From here, we prove lemma INST-invariant-step-INST, which asserts
+; that an instruction satisfies inst-invariant at the next machine
+; cycle.
+
+; Read-reg-ISA-step-if-target-reg-differs proves the fact that
+; the value of register is not updated by an instruction whose destination
+; register is different.
+; (INST-rc i) represents the destination register for the instruction
+; i. Suppose register (INST-rc i) differs from register rix.  Then
+; ISA execution of instruction i does not update register rix, and the
+; value of register rix is unchanged.
+(defthm read-reg-ISA-step-if-target-reg-differs
+    (implies (and (INST-p i) (rname-p rix) (not (equal (INST-rc i) rix)))
+	     (equal (read-reg rix (ISA-regs (ISA-step (INST-pre-ISA i))))
+		    (read-reg rix (ISA-regs (INST-pre-ISA i)))))
+  :hints (("Goal" :in-theory (enable ISA-step ISA-add ISA-sub ISA-default
+				     INST-attrb))))
+
+; This lemmas assures that the pipeline interlock is working
+; correctly.
+; Briefly speaking, the fact that (dependency? MA) is off implies that
+; instruction i at latch1 and instruction (car trace) at latch2 have
+; no true (RAW) dependencies.  Therefore, execution of instruction
+; (car trace) does not change the register (INST-ra i), which is a
+; source register of instruction i.  As a result, we don't have to
+; stall the instruction i.
+;
+; Note: trace is a subtrace of the current MAETT MT.  We consider the
+; interlocks between instructions represented by (car trace) and i.
+; This is one of the easiest ways to represent the lemma
+; without a fully developed supporting theory, although the resulting
+; lemma is not beautifully formulated.
+(defthm read-regs-latch1-INST-ra-special-case
+    (implies (and (invariant MT MA)
+		  (MAETT-p MT) (MA-state-p MA)
+		  (subtrace-p trace MT)
+		  (INST-listp trace)
+		  (consp trace)
+		  (equal (INST-stg (car trace)) 'latch2)
+		  (member-equal i (cdr trace))
+		  (equal (INST-stg i) 'latch1)
+		  (not (b1p (dependency? MA))))
+	     (equal (read-reg (INST-ra i)
+			      (ISA-regs (INST-pre-ISA (car trace))))
+		    (read-reg (INST-ra i)
+			      (ISA-regs (INST-pre-ISA i)))))
+  :hints (("Goal" :cases ((consp (cdr trace))))
+	  ("Subgoal 1" :cases ((equal (cadr trace) i)))
+	  ("Subgoal 1.1" :in-theory (enable dependency? lift-b-ops)
+			 :restrict
+			 ((latch2-rc-INST-rc-if-INST-in ((i (car trace))))
+			  (latch1-ra-INST-ra-if-INST-in ((i (cadr trace))))))))
+
+; Similar lemma for source register (INST-rb i).
+(defthm read-regs-latch1-INST-rb-special-case
+    (implies (and (invariant MT MA)
+		  (MAETT-p MT) (MA-state-p MA)
+		  (subtrace-p trace MT)
+		  (INST-listp trace)
+		  (consp trace)
+		  (equal (INST-stg (car trace)) 'latch2)
+		  (member-equal i (cdr trace))
+		  (equal (INST-stg i) 'latch1)
+		  (not (b1p (dependency? MA))))
+	     (equal (read-reg (INST-rb i)
+			      (ISA-regs (INST-pre-ISA (car trace))))
+		    (read-reg (INST-rb i)
+			      (ISA-regs (INST-pre-ISA i)))))
+  :hints (("Goal" :cases ((consp (cdr trace))))
+	  ("Subgoal 1" :cases ((equal (cadr trace) i)))
+	  ("Subgoal 1.1" :in-theory (enable DEPENDENCY? lift-b-ops)
+			 :restrict
+			 ((latch2-rc-INST-rc-if-INST-in ((i (car trace))))
+			  (latch1-rb-INST-rb-if-INST-in ((i (cadr trace))))))))
+
+(encapsulate nil
+(local
+(defthm read-regs-latch1-INST-ra-if-not-stall-cond-help
+   (implies (and (invariant MT MA)
+		 (MAETT-p MT) (MA-state-p MA)
+		 (subtrace-p trace MT)
+		 (INST-listp trace)
+		 (member-equal i trace) (INST-p i)
+		 (equal (INST-stg i) 'latch1)
+		 (not (b1p (dependency? MA))))
+	    (equal (read-reg (INST-ra I)
+			     (trace-regs trace (ISA-before trace MT)))
+		   (read-reg (INST-ra I) (ISA-regs (INST-pre-ISA I)))))
+  :hints (("Goal" :in-theory (enable ISA-before-INST-pre-ISA-car))
+	  ("subgoal *1/2" :use (:instance stages-of-INST (i (car trace)))))
+  :rule-classes nil))
+
+; Suppose instruction i is at latch1, and (dependency? MA) is off.  It
+; means there is no instruction at latch2 which updates i's source register
+; (INST-ra i).  This lemma proves that the register (INST-ra i) in the MA
+; state contains the correct source value for instruction i.
+(defthm read-regs-latch1-INST-ra-if-not-stall-cond
+    (implies (and (invariant MT MA)
+		  (MAETT-p MT) (MA-state-p MA)
+		  (INST-in i MT) (INST-p i)
+		  (equal (INST-stg i) 'latch1)
+		  (not (b1p (dependency? MA))))
+	     (equal (read-reg (INST-ra I) (MA-regs MA))
+		    (read-reg (INST-ra I) (ISA-regs (INST-pre-ISA I)))))
+  :hints (("Goal"
+	   :use
+	   (:instance read-regs-latch1-INST-ra-if-not-stall-cond-help
+		      (trace (MT-trace MT)))
+	   :in-theory (enable invariant regs-match-p INST-in
+			      MT-REGS))))
+)
+
+(encapsulate nil
+(local
+(defthm read-regs-latch1-INST-rb-if-not-stall-cond-help
+   (implies (and (invariant MT MA)
+		 (MAETT-p MT) (MA-state-p MA)
+		 (subtrace-p trace MT)
+		 (INST-listp trace)
+		 (member-equal i trace) (INST-p i)
+		 (equal (INST-stg i) 'latch1)
+		 (not (b1p (dependency? MA))))
+	    (equal (read-reg (INST-rb I)
+			     (trace-regs trace (ISA-before trace MT)))
+		   (read-reg (INST-rb I) (ISA-regs (INST-pre-ISA I)))))
+  :hints (("Goal" :in-theory (enable ISA-before-INST-pre-ISA-car))
+	  ("subgoal *1/2" :use (:instance stages-of-INST (i (car trace)))))
+  :rule-classes nil))
+
+; Similar lemma for RB.
+(defthm read-regs-latch1-INST-rb-if-not-stall-cond
+    (implies (and (invariant MT MA)
+		  (MAETT-p MT) (MA-state-p MA)
+		  (INST-in i MT) (INST-p i)
+		  (equal (INST-stg i) 'latch1)
+		  (not (b1p (dependency? MA))))
+	     (equal (read-reg (INST-rb I) (MA-regs MA))
+		    (read-reg (INST-rb I) (ISA-regs (INST-pre-ISA I)))))
+    :hints (("Goal"
+	   :use
+	   (:instance read-regs-latch1-INST-rb-if-not-stall-cond-help
+		      (trace (MT-trace MT)))
+	   :in-theory (enable invariant regs-match-p INST-in
+			      MT-REGS))))
+)
+
+(encapsulate nil
+(local
+(defthm ISA-regs-MA-regs-if-not-latch2-valid-induction
+    (implies (and (invariant MT MA)
+		  (MAETT-p MT) (MA-state-p MA)
+		  (subtrace-p trace MT) (INST-listp trace)
+		  (member-equal i trace)
+		  (equal (INST-stg i) 'latch1)
+		  (not (b1p (latch2-valid? (MA-latch2 MA)))))
+	     (equal (ISA-regs (INST-pre-ISA I))
+		    (trace-regs trace (ISA-before trace MT))))
+  :hints (("goal" :in-theory (enable ISA-BEFORE-INST-PRE-ISA-CAR)
+		  :restrict ((LATCH2-VALID-IF-INST-IN ((i (car trace))))))
+	  ("subgoal *1/2" :use ((:instance stages-of-inst (I (car trace))))))
+  :rule-classes nil))
+
+;
+; If instruction i is at latch1 and no instruction is at latch2, i is the
+; only instruction in the pipeline, and i has not updated the register file
+; in the MA. So, the register file in the MA state is the same as in pre-ISA
+; of i.
+(defthm ISA-regs-MA-regs-if-not-latch2-valid
+    (implies (and (invariant MT MA)
+		  (MAETT-p MT) (MA-state-p MA)
+		  (INST-in i MT) (INST-p i)
+		  (equal (INST-stg i) 'latch1)
+		  (not (b1p (latch2-valid? (MA-latch2 MA)))))
+	     (equal (ISA-regs (INST-pre-ISA I)) (MA-regs MA)))
+  :hints (("goal" :in-theory (enable invariant regs-match-p
+				     MT-REGS INST-in)
+		  :use (:instance
+			ISA-regs-MA-regs-if-not-latch2-valid-induction
+			(trace (MT-trace MT))))))
+)
+
+(encapsulate nil
+(local
+(defthm INST-latch1-inv-step-INST-help
+    (implies (and (invariant MT MA)
+		  (MAETT-p MT) (MA-state-p MA)
+		  (INST-in i MT) (INST-p i)
+		  (equal (INST-stg i) 'latch1)
+		  (equal (INST-stg (step-INST i MA)) 'latch1))
+	     (inst-latch1-inv (step-INST i MA) (MA-step MA sig)))
+  :hints (("Goal" :use (:instance INST-invariant-INST-in)
+		  :in-theory (enable INST-invariant INST-latch1-inv
+				     MA-step step-latch1 lift-b-ops
+				     STEP-INST step-latch1-inst)))))
+
+
+; Instruction i will satisfy predicate inst-latch1-inv in the next
+; machine cycle, if its stage will be latch1.
+(defthm INST-latch1-inv-step-INST
+    (implies (and (invariant MT MA)
+		  (MAETT-p MT) (MA-state-p MA)
+		  (INST-in i MT) (INST-p i)
+		  (equal (INST-stg (step-INST i MA)) 'latch1))
+	     (inst-latch1-inv (step-INST i MA) (MA-step MA sig)))
+  :hints (("Goal" :use ((:instance stages-of-inst)))))
+)
+
+
+(encapsulate nil
+(local
+(defthm INST-latch2-inv-step-INST-help
+    (implies (and (invariant MT MA)
+		  (MAETT-p MT) (MA-state-p MA)
+		  (INST-in i MT) (INST-p i)
+		  (equal (INST-stg i) 'latch1)
+		  (equal (INST-stg (step-INST i MA)) 'latch2))
+	     (inst-latch2-inv (step-INST i MA) (MA-step MA sig)))
+  :hints (("Goal" :use (:instance INST-invariant-INST-in)
+		  :in-theory (enable INST-invariant INST-latch2-inv
+				     STALL-COND?
+				     INST-latch1-inv INST-RA-VAL INST-RB-VAL
+				     MA-step step-latch2 lift-b-ops)))))
+
+; Similarly, instruction i satisfies inst-latch2-inv in the next
+; machine cycle if it will be in the stage latch2.
+(defthm INST-latch2-inv-step-INST
+    (implies (and (invariant MT MA)
+		  (MAETT-p MT) (MA-state-p MA)
+		  (INST-in i MT) (INST-p i)
+		  (equal (INST-stg (step-INST i MA)) 'latch2))
+	     (inst-latch2-inv (step-INST i MA) (MA-step MA sig)))
+  :hints (("Goal" :use ((:instance stages-of-inst)))))
+)
+
+
+; Instruction i will satisfy predicate INST-invariant in the next
+; machine cycle.
+(defthm INST-invariant-step-INST
+    (implies (and (invariant MT MA)
+		  (MAETT-p MT) (MA-state-p MA)
+		  (INST-in i MT) (INST-p i))
+	     (inst-invariant (step-INST i MA) (MA-step MA sig)))
+  :hints (("Goal" :in-theory (enable inst-invariant))))
+
+
+(encapsulate nil
+(local
+(defthm MT-init-invariant-MT-step-induction
+    (implies (and (invariant MT MA)
+		  (MAETT-p MT) (MA-state-p MA)
+		  (subtrace-p trace MT) (INST-listp trace))
+	     (trace-inst-invariant (step-trace trace MA sig
+						(ISA-before trace MT))
+				    (MA-step MA sig)))
+  :rule-classes nil))
+
+; MT-init-invariant is true for the next machine state.
+; With induction, we prove that MT-inst-invariant is true for the
+; next MA state and the update table.
+(defthm MT-init-invariant-MT-step
+    (implies (and (invariant MT MA)
+		  (MAETT-p MT) (MA-state-p MA))
+	     (MT-inst-invariant (MT-step MT MA sig)
+				 (MA-step MA sig)))
+  :hints (("Goal" :in-theory (enable MT-inst-invariant MT-step)
+		  :use (:instance MT-init-invariant-MT-step-induction
+				  (trace (MT-trace MT))))))
+)
+
+; MT-contains-all-insts is correct for initial states.
+(defthm MT-contains-all-insts-init-MT
+    (implies (b1p (flushed? MA))
+	     (MT-contains-all-insts (init-MT MA) MA))
+  :hints (("Goal" :in-theory (enable MT-contains-all-insts flushed?
+				     lift-b-ops))))
+
+; Proof of MT-contains-all-insts-MT-step.
+; A MAETT represents all instructions currently in the pipeline, as
+; well as those retired.  If flag latch1-valid? is on, there must be
+; an instruction at latch1.  Similarly, there must be an instruction
+; at latch2 if latch2-valid? is on.  We prove them one by one.
+(encapsulate nil
+(local
+(defthm INST-at-latch1-MT-step-if-fetch-inst-induction
+    (implies (and (invariant MT MA)
+		  (MAETT-p MT) (MA-state-p MA)
+		  (b1p (fetch-inst? MA sig)))
+	     (trace-INST-at 'latch1 (step-trace trace MA sig ISA)))))
+
+
+; INST-at-latch1-MT-step is proven by case analysis.  In one case,
+; fetch-inst? is on.  In other case, dependency? is on.  (They are
+; exclusive.)  INST-at-latch1-MT-step-if-fetch-inst and
+; INST-at-latch1-MT-step-if-stall-cond covers the two cases, respectively.
+(defthm INST-at-latch1-MT-step-if-fetch-inst
+    (implies (and (invariant MT MA)
+		  (MAETT-p MT) (MA-state-p MA)
+		  (b1p (fetch-inst? MA sig)))
+	     (INST-at 'latch1 (MT-step MT MA sig)))
+  :hints (("Goal" :in-theory (enable MT-step INST-at))))
+)
+
+(encapsulate nil
+(local
+(defthm INST-at-latch1-MT-step-if-stall-cond-induction
+    (implies (and (invariant MT MA)
+		  (MAETT-p MT) (MA-state-p MA)
+		  (b1p (stall-cond? MA))
+		  (trace-INST-at 'latch1 trace))
+	     (trace-INST-at 'latch1 (step-trace trace MA sig ISA)))))
+
+(defthm INST-at-latch1-MT-step-if-stall-cond
+    (implies (and (invariant MT MA)
+		  (MAETT-p MT) (MA-state-p MA)
+		  (b1p (stall-cond? MA))
+		  (b1p (latch1-valid? (MA-latch1 MA))))
+	     (INST-at 'latch1 (MT-step MT MA sig)))
+  :hints (("Goal" :in-theory (e/d (INST-at MT-step)
+				  (INST-AT-LATCH1-IF-LATCH1-VALID))
+		  :use (:instance INST-AT-LATCH1-IF-LATCH1-VALID))))
+)
+
+; If latch1-valid? is on for the next MA state, the updated MAETT
+; contains an entry representing the instruction at latch1.
+(defthm INST-at-latch1-MT-step
+    (implies (and (invariant MT MA)
+		  (MAETT-p MT) (MA-state-p MA)
+		  (b1p (latch1-valid? (step-latch1 MA sig))))
+	     (INST-at 'latch1 (MT-step MT MA sig)))
+  :hints (("Goal" :cases ((b1p (fetch-inst? MA sig))))
+	  ("subgoal 2" :in-theory (enable step-latch1 lift-b-ops
+					  stall-cond? fetch-inst?))))
+
+(encapsulate nil
+(local
+(defthm INST-at-latch2-MT-step-induction
+    (implies (and (invariant MT MA)
+		  (MAETT-p MT) (MA-state-p MA)
+		  (or (not (b1p (dependency? MA)))
+		      (not (b1p (latch2-valid? (MA-latch2 MA)))))
+		  (trace-INST-at 'latch1 trace))
+	     (trace-INST-at 'latch2 (step-trace trace MA sig ISA)))
+  :hints (("Goal" :in-theory (enable step-latch2 lift-b-ops STALL-COND?)))))
+
+; Similarly for latch2.
+(defthm INST-at-latch2-MT-step
+    (implies (and (invariant MT MA)
+		  (MAETT-p MT) (MA-state-p MA)
+		  (b1p (latch2-valid? (step-latch2 MA))))
+	     (INST-at 'latch2 (MT-step MT MA sig)))
+  :hints (("Goal" :in-theory (e/d (step-latch2 lift-b-ops INST-at MT-step
+)
+				  (INST-AT-LATCH1-IF-LATCH1-VALID))
+		  :use (:instance INST-AT-LATCH1-IF-LATCH1-VALID))))
+)
+
+; MT-contains-all-insts is true for the next machine state.
+(defthm MT-contains-all-insts-MT-step
+    (implies (and (invariant MT MA)
+		  (MAETT-p MT) (MA-state-p MA))
+	     (MT-contains-all-insts (MT-step MT MA sig)
+				    (MA-step MA sig)))
+  :hints (("Goal" :in-theory (enable MT-contains-all-insts MA-step))))
+
+;;;;;; Proof of MT-in-order-p
+;
+; MT-in-order-p is true for initial case.
+(defthm MT-in-order-p-init-MT
+    (MT-in-order-p (init-MT MA))
+  :hints (("Goal" :in-theory (enable init-MT MT-in-order-p))))
+
+
+; Instruction at latch1 is the last fetched instruction in the
+; pipeline.  MAETT records fetched and executed instructions in ISA
+; execution order, so the entry representing the instruction at latch1
+; is the last in a MAETT.
+(defthm endp-step-trace-cdr-if-step-INST-latch1
+    (implies (and (invariant MT MA)
+		  (MAETT-p MT) (MA-state-p MA)
+		  (subtrace-p trace MT)
+		  (INST-listp trace)
+		  (consp trace)
+		  (equal (INST-stg (step-INST (car trace) MA)) 'latch1))
+	     (not (consp (step-trace (cdr trace) MA sig ISA))))
+  :hints (("Goal" :use ((:instance stages-of-inst (i (car trace)))
+			(:instance no-inst-after-INST-latch1)
+			(:instance latch1-valid-if-INST-in (i (car trace))))
+		  :in-theory (enable fetch-inst? stall-cond? lift-b-ops))))
+
+
+; There cannot be more than two entries of MAETT representing an
+; instruction at latch2.
+(defthm not-trace-INST-at-latch2-step-trace
+    (implies (and (invariant MT MA)
+		  (MAETT-p MT) (MA-state-p MA)
+		  (subtrace-p trace MT)
+		  (consp trace)
+		  (INST-listp trace)
+		  (equal (INST-stg (step-INST (car trace) MA)) 'latch2))
+	     (not (trace-INST-at 'latch2 (step-trace (cdr trace) MA sig ISA))))
+  :hints (("Goal" :use ((:instance stages-of-inst (i (car trace)))
+			(:instance no-inst-after-INST-latch1)))))
+
+
+; Instructions retire in order.  So no retired instruction follows
+; an instruction at latch2.
+(defthm not-trace-INST-at-retire-step-trace
+    (implies (and (invariant MT MA)
+		  (MAETT-p MT) (MA-state-p MA)
+		  (subtrace-p trace MT)
+		  (consp trace)
+		  (INST-listp trace)
+		  (equal (INST-stg (step-INST (car trace) MA)) 'latch2))
+	     (not (trace-INST-at 'retire (step-trace (cdr trace) MA sig ISA))))
+  :hints (("Goal" :use ((:instance stages-of-inst (i (car trace)))
+			(:instance no-inst-after-INST-latch1)))))
+
+
+(encapsulate nil
+(local
+(defthm MT-in-order-p-MT-step-induction
+    (implies (and (invariant MT MA)
+		  (MAETT-p MT) (MA-state-p MA)
+		  (subtrace-p trace MT)
+		  (INST-listp trace))
+	     (trace-in-order-p (step-trace trace MA sig ISA)))))
+
+; MT-in-order-p is true for the next machine state.
+(defthm MT-in-order-p-MT-step
+    (implies (and (invariant MT MA)
+		  (MAETT-p MT) (MA-state-p MA))
+	     (MT-in-order-p (MT-step MT MA sig)))
+  :hints (("Goal" :in-theory (enable MT-step MT-in-order-p))))
+)
+
+;;;;;;;; Proof of invariant
+; Invariant are true for the initial MA state and its MAETT.
+(defthm invariant-init-MT
+    (implies (and (MA-state-p MA) (b1p (flushed? MA)))
+	     (invariant (init-MT MA) MA))
+  :hints (("Goal" :in-theory (enable invariant))))
+
+; Predicate Invariant is actually an invariant condition.
+(defthm invariant-step
+    (implies (and (invariant MT MA) (MAETT-p MT) (MA-state-p MA)
+		  (MA-sig-p sig))
+	     (invariant (MT-step MT MA sig)
+			 (MA-step MA sig)))
+  :Hints (("Goal" :in-theory (enable invariant))))
+
+; By induction, invariant is correct after n cycles of MA
+; execution.
+(defthm invariant-stepn
+    (implies (and (invariant MT MA) (MAETT-p MT) (MA-state-p MA)
+		  (MA-sig-listp sig-list)
+		  (<= n (len sig-list)))
+	     (invariant (MT-stepn MT MA sig-list n)
+			 (MA-stepn MA sig-list n))))
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; Proof of the correctness criterion.
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; The number of instructions recorded in the MAETT.  This is the
+; number of fetched instructions since the initial machine state.
+(defun MT-num-insts (MT) (len (MT-trace MT)))
+
+; The number of instructions fetched and executed during the n cycles
+; of machine execution from the initial state MA with input signal list
+; sig-list.
+(defun num-insts (MA sig-list n)
+  (MT-num-insts (MT-stepn (init-MT MA) MA sig-list n)))
+
+(defthm integerp-MT-num-insts (integerp (MT-num-insts MT)))
+
+(defthm integerp-num-insts (integerp (num-insts MA sig-list n)))
+
+(in-theory (disable MT-num-insts num-insts))
+
+(defun trace-all-retired (trace)
+  (if (endp trace)
+      t
+      (and (equal (INST-stg (car trace)) 'retire)
+	   (trace-all-retired (cdr trace)))))
+
+; (MT-all-retires MT) is true if all instructions recorded by MT is
+; retired.
+(defun MT-all-retired (MT)
+    (trace-all-retired (MT-trace MT)))
+
+(encapsulate nil
+(local
+(defthm flushed-implies-MT-all-retired-help
+    (implies (and (INST-listp trace)
+		  (trace-inst-invariant trace MA)
+		  (b1p (flushed? MA)))
+	     (trace-all-retired trace))
+  :hints (("goal" :in-theory (enable flushed? lift-b-ops INST-p stage-p
+				     inst-invariant INST-latch1-inv
+				     INST-latch2-inv)))))
+
+; If a MA state, MA, is flushed, the corresponding MAETT, MT, contains
+; only retired instructions.
+(defthm flushed-implies-MT-all-retired
+    (implies (and (invariant MT MA)
+		  (MAETT-p MT)
+		  (b1p (flushed? MA)))
+	     (MT-all-retired MT))
+  :hints (("goal" :in-theory (enable MT-all-retired invariant
+				     MT-inst-invariant))))
+)
+
+; ; A help lemma
+(defthm ISA-extensionality
+    (implies (and (ISA-state-p ISA1)
+		  (ISA-state-p ISA2)
+		  (equal (ISA-pc ISA1) (ISA-pc ISA2))
+		  (equal (ISA-regs ISA1) (ISA-regs ISA2))
+		  (equal (ISA-mem ISA1) (ISA-mem ISA2)))
+	     (equal ISA1 ISA2))
+  :rule-classes nil)
+
+; Lemma flushed-MA-=-MT-final-ISA is proven by showing the equivalence
+; of LHS and RHS with respect to each programmer visible components such
+; as program counter, register file and memory.
+(encapsulate nil
+(local
+(defthm ISA-pc-ISA-stepn-if-flushed-induction
+    (implies (ISA-chain-trace-p trace ISA)
+	     (equal (ISA-pc (ISA-stepn ISA (len trace)))
+		    (trace-pc trace ISA)))))
+
+(local
+(defthm ISA-pc-ISA-stepn-if-flushed-help
+    (implies (invariant MT MA)
+	     (equal (ISA-pc (ISA-stepn (MT-init-ISA MT) (MT-num-insts MT)))
+		    (MT-pc MT)))
+  :hints (("Goal" :in-theory (enable MT-pc MT-num-insts
+				     invariant ISA-chain-p)))))
+
+
+; Equivalence with respect to PC.
+(defthm ISA-pc-ISA-stepn-if-flushed
+    (implies (and (invariant MT MA)
+		  (MT-all-retired MT))
+	     (equal (ISA-pc (ISA-stepn (MT-init-ISA MT) (MT-num-insts MT)))
+		    (MA-pc MA)))
+  :hints (("Goal" :in-theory (enable invariant pc-match-p)
+		  :restrict ((ISA-pc-ISA-stepn-if-flushed-help
+			      ((MT MT) (MA MA)))))))
+)
+
+(encapsulate nil
+(local
+ (defthm ISA-regs-ISA-stepn-if-flushed-induction
+     (implies (and (ISA-chain-trace-p trace ISA)
+		   (trace-all-retired trace))
+	      (equal (ISA-regs (ISA-stepn ISA (len trace)))
+		     (trace-regs trace ISA)))))
+(local
+(defthm ISA-regs-ISA-stepn-if-flushed-help
+    (implies (and (invariant MT MA) (MT-all-retired MT))
+	     (equal (ISA-regs (ISA-stepn (MT-init-ISA MT) (MT-num-insts MT)))
+		    (MT-regs MT)))
+  :hints (("goal" :in-theory (enable MT-init-ISA MT-all-retired
+				     MT-num-insts MT-regs
+				     invariant ISA-chain-p)))))
+
+; Equivalence with respect to the register file.
+(defthm ISA-regs-ISA-stepn-if-flushed
+    (implies (and (invariant MT MA)
+		  (MT-all-retired MT))
+	     (equal (ISA-regs (ISA-stepn (MT-init-ISA MT) (MT-num-insts MT)))
+		    (MA-regs MA)))
+  :hints (("Goal" :in-theory (enable invariant regs-match-p)
+		  :restrict ((ISA-regs-ISA-stepn-if-flushed-help
+			      ((MT MT) (MA MA)))))))
+)
+
+; Equivalence with respect to the memory.
+(defthm ISA-mem-MT-init-ISA-=-MA-mem
+    (implies (and (invariant MT MA)
+		  (MAETT-p MT) (MA-state-p MA))
+	     (equal (ISA-mem (MT-init-ISA MT)) (MA-mem MA)))
+  :hints (("Goal" :in-theory (enable invariant mem-match-p))))
+
+; One step before the final lemma.  Consider a flushed micro-state MA
+; and its MAETT.  MAETT contains (MT-num-INST MT) instruction
+; entries.  (MT-init-ISA MT) is the initial ISA state before executing
+; the first instruction recorded in MAETT.  Therefore,
+; (ISA-stepn (MT-init-ISA MT) (MT-num-insts MT)) is the final ISA state
+; after executing all instructions recorded in MT.  Our invariant
+; guarantees that the projection of MA to an ISA state is equal to
+; this final ISA state.
+(defthm flushed-MA-=-MT-final-ISA
+    (implies (and (invariant MT MA)
+		  (MAETT-p MT) (MA-state-p MA)
+		  (b1p (flushed? MA)))
+	     (equal (ISA-stepn (MT-init-ISA MT) (MT-num-insts MT))
+		    (proj MA)))
+  :hints (("Goal" :in-theory (enable proj)
+		  :use
+		  (:instance ISA-extensionality
+		     (ISA1 (ISA-stepn (MT-init-ISA MT) (MT-num-insts MT)))
+		     (ISA2 (proj MA)))))
+  :rule-classes nil)
+
+;  Correctness diagram.
+(defthm commutative-diagram
+    (implies (and (MA-state-p MA)
+		  (MA-sig-listp sig-list)
+		  (<= n (len sig-list))
+		  (b1p (flushed? MA))
+		  (b1p (flushed? (MA-stepn MA sig-list n))))
+	     (equal (proj (MA-stepn MA sig-list n))
+		    (ISA-stepn (proj MA)
+			       (num-insts MA sig-list n))))
+  :hints (("Goal" :use (:instance flushed-MA-=-MT-final-ISA
+				  (MT (MT-stepn (init-MT MA) MA sig-list n))
+				  (MA (MA-stepn MA sig-list n)))
+		  :in-theory (enable num-insts))))
+
+; Define the weight of an MA state.
+(defun MA-weight (MA)
+  (+ (if (b1p (latch1-valid? (MA-latch1 MA))) 2 0)
+     (if (b1p (latch2-valid? (MA-latch2 MA))) 1 0)))
+
+; The weight decreases unless MA is flushed.
+(defthm MA-weight-MT-step
+    (implies (not (b1p (flushed? MA)))
+	     (< (MA-weight (MA-step MA 0)) (MA-weight MA)))
+  :hints (("Goal" :in-theory (enable flushed? lift-b-ops b1p-b-and
+				     MA-step step-latch1 b-and b-nand
+				     step-latch2
+				     stall-cond?))))
+
+(in-theory (disable MA-weight))
+
+; The number of the cycles to flush the pipeline.
+(defun flush-cycles (MA)
+  (declare (xargs :measure (MA-weight MA)))
+  (if (b1p (flushed? MA))
+      0
+      (1+ (flush-cycles (MA-step MA 0)))))
+
+; Generate a list of 0 with length n.
+(defun zeros (n)
+  (if (zp n) nil (cons 0 (zeros (1- n)))))
+
+; The MA state after (flush-cycles MA) cycles of MA execution with
+; sig-list 0's is flushed.
+(defthm liveness
+    (implies (MA-state-p MA)
+	     (b1p (flushed? (MA-stepn MA
+				      (zeros (flush-cycles MA))
+				      (flush-cycles MA))))))
diff --git a/books/workshops/2000/manolios/pipeline/trivial/sawada-model/table-def.lisp b/books/workshops/2000/manolios/pipeline/trivial/sawada-model/table-def.lisp
new file mode 100644
index 0000000..a705802
--- /dev/null
+++ b/books/workshops/2000/manolios/pipeline/trivial/sawada-model/table-def.lisp
@@ -0,0 +1,487 @@
+(in-package "ACL2")
+
+(include-book "utils")
+(include-book "basic-def")
+(include-book "model")
+
+(deflabel begin-table-def)
+
+; The valid pipeline stages in this machine are latch1, latch2 and
+; retire.
+(defun stage-p (stg)
+  (declare (xargs :guard t))
+  (or (equal stg 'latch1) (equal stg 'latch2) (equal stg 'retire)))
+
+(in-theory (disable proj flushed? stage-p))
+
+; The definition of MAETT entry which represents an instruction.
+; Only a few fields are required for this example.
+;  Field	Description
+;  stg		The current stage of the represented instruction.
+;  pre-ISA	The ISA state before the execution of this instruction.
+;  post-ISA	The ISA state after the execution of this instruction.
+(defstructure INST
+  (stg  (:assert (stage-p stg) :rewrite))
+  (pre-ISA (:assert (ISA-state-p pre-ISA) :rewrite))
+  (post-ISA (:assert (ISA-state-p post-ISA) :rewrite))
+  (:options :guards))
+
+(deflist INST-listp (l)
+  (declare (xargs :guard t))
+  INST-p)
+
+; Definition of MAETT.  It stores the initial ISA state, init-ISA, and
+; a list of MAETT entries, trace.  Each entry of trace represents
+; a fetched and executed instruction.   Trace stores the entries in
+; the order that the ISA executes the represented instructions.  ISA
+; state init-ISA is the ISA state before executing the first
+; instruction in trace.
+(defstructure MAETT
+  (init-ISA (:assert (ISA-state-p init-ISA) :rewrite))
+  (trace (:assert (INST-listp trace) :rewrite))
+  (:options :guards (:conc-name MT-)))
+
+(deflabel begin-MAETT-def)
+
+; Function init-MT constructs the initial  MAETT table for an
+; flushed initial MA state.  Since no instructions are fetched yet,
+; trace field contains an empty list.
+(defun init-MT (MA)
+  (declare (xargs :guard (MA-state-p MA)))
+  (MAETT (proj MA) nil))
+
+; The MAETT entry representing a newly fetched instruction.  Argument
+; ISA is the pre-ISA state of the newly fetched instruction.  In other
+; words, it is the correct ISA state before executing the newly
+; fetched instruction.
+(defun new-inst (ISA)
+  (declare (xargs :guard (ISA-state-p ISA)))
+  (INST 'latch1
+	ISA
+	(ISA-step ISA)))
+
+(defun step-latch1-INST (i MA)
+  (declare (xargs :guard (and (INST-p i) (MA-state-p MA))))
+  (if (b1p (stall-cond? MA))
+      i
+      (update-INST i :stg 'latch2)))
+
+(defun step-latch2-INST (i)
+  (declare (xargs :guard (INST-p i)))
+  (update-INST i :stg 'retire))
+
+; Function step-INST updates the MAETT entry to reflect the change of
+; the state of the represented instruction.  In this example, we only
+; have to update the stage field as the instruction advances through the
+; pipeline.
+(defun step-INST (i MA)
+  (declare (xargs :guard (and (INST-p i) (MA-state-p MA))))
+  (cond ((equal (INST-stg i) 'latch1)
+	 (step-latch1-INST i MA))
+	((equal (INST-stg i) 'latch2)
+	 (step-latch2-INST i))
+	(t i)))
+
+; Function step-trace updates the field, trace, of a MAETT.  If a new
+; instruction is fetched, an entry corresponding to the new
+; instruction is added at the end of the trace.  The rest of the
+; entries are updated with function step-INST.
+(defun step-trace (trace MA sig last-ISA)
+  (declare (xargs :guard (and (INST-listp trace) (MA-state-p MA)
+			      (MA-sig-p sig)
+			      (ISA-state-p last-ISA))))
+  (if (endp trace)
+      (if (b1p (fetch-inst? MA sig))
+	  (list (new-inst last-ISA))
+	  nil)
+      (cons (step-INST (car trace) MA)
+	    (step-trace (cdr trace) MA sig (INST-post-ISA (car trace))))))
+
+; Function to update an MAETT.  MT-step takes arguments MA and MT,
+; which are the current MA state and the corresponding MAETT, and it
+; returns the updated MAETT.  The new MAETT represents the next MA
+; state (MA-step MA sig).
+(defun MT-step (MT MA sig)
+  (declare (xargs :guard (and (MAETT-p MT) (MA-state-p MA)
+			      (MA-sig-p sig))))
+  (MAETT (MT-init-ISA MT)
+	 (step-trace (MT-trace MT) MA sig (MT-init-ISA MT))))
+
+(deflabel end-MAETT-def)
+
+
+; Function to iteratively update a MAETT, MT, for n cycles.  Argument
+; MA and MT are the initial MA state and the corresponding MAETT.
+(defun MT-stepn (MT MA sig-list n)
+  (declare (xargs :guard (and (MAETT-p MT) (MA-state-p MA)
+			      (MA-sig-listp sig-list)
+			      (integerp n) (<= 0 n))
+		  :verify-guards nil))
+  (if (zp n) MT
+      (if (endp sig-list) MT
+	  (MT-stepn (MT-step MT MA (car sig-list))
+		    (MA-step MA (car sig-list))
+		    (cdr sig-list)
+		    (1- n)))))
+
+(deftheory MAETT-def
+    (non-rec-functions
+     (set-difference-theories (function-theory 'end-MAETT-def)
+			      (function-theory 'begin-MAETT-def))
+     world))
+
+(in-theory (disable MAETT-def))
+
+;; Type proofs
+(defthm ISA-state-p-proj
+    (implies (MA-state-p MA) (ISA-state-p (proj MA)))
+  :hints (("Goal" :in-theory (enable proj))))
+
+(defthm MAETT-p-init-MT
+    (implies (MA-state-p MA) (MAETT-p (init-MT MA)))
+  :hints (("Goal" :in-theory (enable init-MT))))
+
+(defthm inst-p-new-inst
+    (implies (ISA-state-p ISA) (INST-p (new-inst ISA)))
+  :hints (("Goal" :in-theory (enable new-inst))))
+
+(defthm INST-p-step-INST
+    (implies (INST-p i) (INST-p (step-INST i MA)))
+  :Hints (("Goal" :in-theory (enable step-inst step-latch1-inst
+				     step-latch2-inst))))
+
+(defthm INST-listp-step-trace
+    (implies (and (INST-listp trace) (ISA-state-p ISA))
+	     (INST-listp (step-trace trace MA sig ISA))))
+
+(defthm MAETT-p-MT-step
+    (implies (and (MAETT-p MT) (MA-state-p MA) (MA-sig-p sig))
+	     (MAETT-p (MT-step MT MA sig)))
+  :hints (("Goal" :in-theory (enable MT-step))))
+
+(verify-guards MT-step)
+
+(defthm MAETT-p-MT-stepn
+    (implies (and (MAETT-p MT) (MA-state-p MA) (MA-sig-listp sig-list)
+		  (<= n (len sig-list)))
+	     (MAETT-p (MT-stepn MT MA sig-list n))))
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; Definition of Instruction Attributes
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; Various attributes of an instruction are defined as functions which
+; take the MAETT entry representing the instruction.  For instance,
+; the opcode of an instruction represented by MAETT entry I is defined
+; as (INST-op I).  In the following definitions, we define many
+; attributes such as instruction word, operand registers, source
+; values and result value.
+(deflabel begin-INST-attrb)
+(defun INST-word (i)
+  (declare (xargs :guard (INST-p i)))
+  (read-mem (ISA-pc (INST-pre-ISA i)) (ISA-mem (INST-pre-ISA i))))
+
+(defun INST-op (i)
+  (declare (xargs :guard (INST-p i)))
+  (op-field (INST-word i)))
+
+(defun INST-rc (i)
+  (declare (xargs :guard (INST-p i)))
+  (rc-field (INST-word i)))
+
+(defun INST-ra (i)
+  (declare (xargs :guard (INST-p i)))
+  (ra-field (INST-word i)))
+
+(defun INST-rb (i)
+  (declare (xargs :guard (INST-p i)))
+  (rb-field (INST-word i)))
+
+(defun INST-ra-val (i)
+  (declare (xargs :guard (INST-p i)))
+  (read-reg (INST-ra i) (ISA-regs (INST-pre-ISA i))))
+
+(defun INST-rb-val (i)
+  (declare (xargs :guard (INST-p i)))
+  (read-reg (INST-rb i) (ISA-regs (INST-pre-ISA i))))
+
+(defun INST-result (i)
+  (declare (xargs :guard (INST-p i)))
+  (ALU-output (INST-op i) (INST-ra-val i) (INST-rb-val i)))
+
+(deflabel end-INST-attrb)
+(deftheory INST-attrb
+    (set-difference-theories (function-theory 'end-INST-attrb)
+			     (function-theory 'begin-INST-attrb)))
+(in-theory (disable INST-attrb))
+
+(defthm word-p-INST-word
+    (implies (INST-p i) (word-p (INST-word i)))
+  :hints (("Goal" :in-theory (enable INST-word))))
+
+(defthm opcd-p-INST-op
+    (implies (INST-p i) (opcd-p (INST-op i)))
+  :hints (("Goal" :in-theory (enable INST-op))))
+
+(defthm rname-p-INST-rc
+    (implies (INST-p i) (rname-p (INST-rc i)))
+  :hints (("Goal" :in-theory (enable INST-rc))))
+
+(defthm rname-p-INST-ra
+    (implies (INST-p i) (rname-p (INST-ra i)))
+  :hints (("Goal" :in-theory (enable INST-ra))))
+
+(defthm rname-p-INST-rb
+    (implies (INST-p i) (rname-p (INST-rb i)))
+  :hints (("Goal" :in-theory (enable INST-rb))))
+
+(defthm word-p-INST-ra-val
+    (implies (INST-p i) (word-p (INST-ra-val i)))
+  :hints (("Goal" :in-theory (enable INST-ra-val))))
+
+(defthm word-p-INST-rb-val
+    (implies (INST-p i) (word-p (INST-rb-val i)))
+  :hints (("Goal" :in-theory (enable INST-rb-val))))
+
+(defthm word-p-INST-result
+    (implies (INST-p i) (word-p (INST-result i)))
+  :hints (("Goal" :in-theory (enable INST-result ALU-output))))
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; Defintion of INST-at
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; INST-at returns the MAETT entry whose represented instruction is at
+; a particular stage.
+;
+; (INST-at stg MT) is nil if there is no instruction at stage stg in
+; MAETT MT.  If there is one, it returns the corresponding MAETT entry
+; representing the instruction.
+
+(defun trace-inst-at (stg trace)
+  (declare (xargs :guard (and (stage-p stg) (INST-listp trace))))
+  (if (endp trace) nil
+      (if (equal (INST-stg (car trace)) stg)
+	  (car trace)
+	  (trace-inst-at stg (cdr trace)))))
+
+(defun INST-at (stg MT)
+  (declare (xargs :guard (and (stage-p stg) (MAETT-p MT))))
+  (trace-inst-at stg (MT-trace MT)))
+
+(in-theory (disable INST-at))
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; Definition of invariant conditions
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; Invariant conditions required for the proof of correctness diagram
+; are defined here.  We needed seven invariant conditions.
+;
+;       (pc-match-p MT MA)
+;          The program counter holds the correct value.
+;       (regs-match-p MT MA)
+;          The register file contains correct values.
+;       (mem-match-p MT MA)
+;          The memory is in the correct state.
+;       (ISA-chain-p MT)
+;          MAETT records correct ISA execution of instructions.
+;       (MT-inst-invariant MT MA)
+;          Each instruction in the pipeline satisfies "instruction invariant".
+;       (MT-contains-all-insts MT MA)
+;          MT contains all instructions currently in the pipeline of MA.
+;       (MT-in-order-p MT)))
+;          MA pipeline executes instructions in program order.
+(deflabel begin-invariant-def)
+
+; Predicate pc-match-p checks whether the program counter in the MA
+; holds the correct value.  The reader may ask what the correct value is.
+; The answer is that the program counter should point to the
+; instruction to be fetched in the next cycle.  MT-pc calculates
+; it from a MAETT, by first looking for the most recently fetched
+; instruction I, and find the program counter value of (INST-post-ISA I).
+; (INST-post-ISA I) is the ISA state after the execution of I,
+; and before fetching the next instruction.
+(defun trace-pc (trace ISA)
+  (declare (xargs :guard (and (INST-listp trace) (ISA-state-p ISA))))
+  (if (endp trace)
+      (ISA-pc ISA)
+      (trace-pc (cdr trace) (INST-post-ISA (car trace)))))
+
+(defun MT-pc (MT)
+  (declare (xargs :guard (MAETT-p MT)))
+  (trace-pc (MT-trace MT) (MT-init-ISA MT)))
+
+(defun pc-match-p (MT MA)
+  (declare (xargs :guard (and (MAETT-p MT) (MA-state-p MA))))
+  (equal (MT-pc MT) (MA-pc MA)))
+
+; Predicate regs-match-p checks whether the register file contains the
+; correct values.  MT-regs calculate the correct register file
+; state from a MAETT.  It first looks for the earliest non-retired
+; instruction I, and returns the register file of (INST-pre-ISA I).
+; The register is updated when an instruction retires.  So the
+; register file in the MA holds the results of all retired
+; instruction, but none of the partially executed instructions,
+; including I.
+(defun trace-regs (trace ISA)
+  (declare (xargs :guard (and (INST-listp trace) (ISA-state-p ISA))))
+  (if (endp trace)
+      (ISA-regs ISA)
+      (if (not (equal (INST-stg (car trace)) 'retire))
+	  (ISA-regs ISA)
+	  (trace-regs (cdr trace) (INST-post-ISA (car trace))))))
+
+(defun MT-regs (MT)
+  (declare (xargs :guard (MAETT-p MT)))
+  (trace-regs (MT-trace MT) (MT-init-ISA MT)))
+
+(defun regs-match-p (MT MA)
+  (declare (xargs :guard (and (MAETT-p MT) (MA-state-p MA))))
+  (equal (MT-regs MT) (MA-regs MA)))
+
+; Memory state does not change in this model.  The memory of the MA state
+; should be equal to that of the initial ISA state.
+(defun mem-match-p (MT MA)
+  (declare (xargs :guard (and (MAETT-p MT) (MA-state-p MA))))
+  (equal (MA-mem MA) (ISA-mem (MT-init-ISA MT))))
+
+; MAETT represents the sequence of instructions as a list, where each
+; element of the list represents an instruction.  Each entry
+; has pre-ISA and post-ISA fields, which store the ISA state before
+; and after executing the represented instruction.  This ISA
+; states form a sort of chain.  Suppose MT has a list of instruction
+; entries (I_0 I_1 I_2 ...).  I_0 represents the first instruction to be
+; executed, I_1 represents the second and so on.  Then following
+; equations hold:
+; (ISA-step (INST-pre-ISA I_0)) = (INST-post-ISA I_0)
+; (INST-post-ISA I_0) = (INST-pre-ISA I_1)
+; (ISA-step (INST-pre-ISA I_1)) = (INST-post-ISA I_1)
+; (INST-post-ISA I_1) = (INST-pre-ISA I_2)
+;   ....
+; This relations are checked by the predicate ISA-chain-p.  In other
+; words, ISA-chain-p checks whether the correct sequence of ISA states
+; are stored in the MAETT.  Following picture may help the reader to
+; understand the relations of pre-ISA and post-ISA.
+;
+;   (INST-pre-ISA i_0)
+;         |  execution of i_0
+;         v
+;   (INST-post-ISA i_0) = (INST-pre-ISA i_1)
+;         |  execution of i_1
+;         v
+;   (INST-post-ISA i_1) = (INST-pre-ISA i_2)
+;         ...
+(defun ISA-chain-trace-p (trace ISA)
+  (declare (xargs :guard (and (INST-listp trace) (ISA-state-p ISA))))
+  (if (endp trace)
+      T
+      (and (equal (INST-pre-ISA (car trace)) ISA)
+	   (equal (ISA-step ISA)
+		  (INST-post-ISA (car trace)))
+	   (ISA-chain-trace-p (cdr trace) (ISA-step ISA)))))
+
+(defun ISA-chain-p (MT)
+  (declare (xargs :guard (MAETT-p MT)))
+  (ISA-chain-trace-p (MT-trace MT) (MT-init-ISA MT)))
+
+; Each instruction should satisfy some invariant conditions at each
+; stage of the pipeline.  Mostly, these conditions are about the
+; intermediate values stored in the pipeline latches.
+;
+; For instance, field latch1-op of latch latch1 in the MA state hould
+; hold the operand of instruction at stage latch1.  If you see the
+; definition of inst-latch1-inv, you can find the corresponding
+; equation as the second conjunct of the body of the definition.
+;
+; Predicate inst-invariant checks whether instruction entry i and the
+; corresponding MA state satisfies these stage-dependent invariant.
+; MT-inst-invariant checks all instructions in the MAETT satisfies
+; inst-invariant.
+
+; The condition that instruction should satisfy at state latch1.
+(defun inst-latch1-inv (i MA)
+  (declare (xargs :guard (and (INST-p i) (MA-state-p MA))))
+  (and (b1p (latch1-valid? (MA-latch1 MA)))
+       (equal (latch1-op (MA-latch1 MA)) (INST-op i))
+       (equal (latch1-rc (MA-latch1 MA)) (INST-rc i))
+       (equal (latch1-ra (MA-latch1 MA)) (INST-ra i))
+       (equal (latch1-rb (MA-latch1 MA)) (INST-rb i))))
+
+; The condition that instruction should satisfy at state latch2.
+(defun inst-latch2-inv (i MA)
+  (declare (xargs :guard (and (INST-p i) (MA-state-p MA))))
+  (and (b1p (latch2-valid? (MA-latch2 MA)))
+       (equal (latch2-op (MA-latch2 MA))     (INST-op i))
+       (equal (latch2-rc (MA-latch2 MA))     (INST-rc i))
+       (equal (latch2-ra-val (MA-latch2 MA)) (INST-ra-val i))
+       (equal (latch2-rb-val (MA-latch2 MA)) (INST-rb-val i))))
+
+; Instruction invariant that i should satisfy regardless of its stage.
+(defun inst-invariant (i MA)
+  (declare (xargs :guard (and (INST-p i) (MA-state-p MA))))
+  (cond ((equal (INST-stg i) 'latch1)
+	 (inst-latch1-inv i MA))
+	((equal (INST-stg i) 'latch2)
+	 (inst-latch2-inv i MA))
+	(t t)))
+
+(defun trace-inst-invariant (trace MA)
+  (declare (xargs :guard (and (INST-listp trace) (MA-state-p MA))))
+  (if (endp trace) t
+      (and (inst-invariant (car trace) MA)
+	   (trace-inst-invariant (cdr trace) MA))))
+
+(defun MT-inst-invariant (MT MA)
+  (declare (xargs :guard (and (MAETT-p MT) (MA-state-p MA))))
+  (trace-inst-invariant (MT-trace MT) MA))
+
+; If field latch1-valid? of an MA state is on, the corresponding MAETT
+; contains an entry representing the instruction at latch1.  Similarly
+; for latch2.
+(defun MT-contains-all-insts (MT MA)
+  (declare (xargs :guard (and (MAETT-p MT) (MA-state-p MA))))
+  (and (implies (b1p (latch1-valid? (MA-latch1 MA)))
+		(inst-at 'latch1 MT))
+       (implies (b1p (latch2-valid? (MA-latch2 MA)))
+		(inst-at 'latch2 MT))))
+
+; This pipelined machine executes instructions in program order.
+; The instruction at latch1 is younger than the instruction at latch2,
+; and the instruction at latch2 is younger than any retired
+; instructions.  This fact is checked by MT-in-order-p, assuming that
+; instructions are recorded in program order in a MAETT.
+(defun trace-in-order-p (trace)
+  (declare (xargs :guard (INST-listp trace)))
+  (if (endp trace)
+      t
+      (if (equal (INST-stg (car trace)) 'latch1)
+	  (endp (cdr trace))
+	  (if (equal (INST-stg (car trace)) 'latch2)
+	      (and (not (trace-inst-at 'latch2 (cdr trace)))
+		   (not (trace-inst-at 'retire (cdr trace)))
+		   (trace-in-order-p (cdr trace)))
+	      (trace-in-order-p (cdr trace))))))
+
+(defun MT-in-order-p (MT)
+  (declare (xargs :guard (MAETT-p MT)))
+  (trace-in-order-p (MT-trace MT)))
+
+; The definition of invariant.
+(defun invariant (MT MA)
+  (declare (xargs :guard (and (MAETT-p MT) (MA-state-p MA))))
+  (and (pc-match-p MT MA)
+       (regs-match-p MT MA)
+       (mem-match-p MT MA)
+       (ISA-chain-p MT)
+       (MT-inst-invariant MT MA)
+       (MT-contains-all-insts MT MA)
+       (MT-in-order-p MT)))
+
+(deflabel end-invariant-def)
+(deftheory invariant-def
+    (set-difference-theories (function-theory 'end-invariant-def)
+			     (function-theory 'begin-invariant-def)))
+
+(deftheory non-rec-invariant-def
+    (non-rec-functions (theory 'invariant-def) world))
+
+(in-theory (disable non-rec-invariant-def))
+
diff --git a/books/workshops/2000/manolios/pipeline/trivial/sawada-model/trivia.lisp b/books/workshops/2000/manolios/pipeline/trivial/sawada-model/trivia.lisp
new file mode 100644
index 0000000..a930142
--- /dev/null
+++ b/books/workshops/2000/manolios/pipeline/trivial/sawada-model/trivia.lisp
@@ -0,0 +1,99 @@
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; Trivia.lisp
+; Copyright reserved by SRC
+; Author  Jun Sawada, University of Texas at Austin
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;'
+(in-package "ACL2")
+
+;; Jared: changing this to an include of an identical book
+(include-book "workshops/1999/pipeline/trivia" :dir :system)
+
+;; (include-book "../../../../../../data-structures/array1")
+;; (include-book "../../../../../../arithmetic/top")
+
+;; (deflabel begin-trivia)
+
+;; (defmacro quoted-constant-p (x)
+;;   `(and (consp ,x) (equal (car ,x) 'quote)))
+
+;; (defthm append-nil
+;;     (implies (true-listp x)
+;; 	      (equal (append x nil) x))
+;;   :hints (("Goal" :in-theory (enable binary-append))))
+
+;; (defun natural-induction (i)
+;;     (if (zp i) t
+;; 	(natural-induction (1- i))))
+
+;; ;; in data-structures/list-defthms
+;; ;; (defthm car-nthcdr
+;; ;;     (equal (car (nthcdr idx lst)) (nth idx lst)))
+
+;; (defthm cdr-nthcdr
+;;     (implies (and (integerp idx) (<= 0 idx))
+;; 	     (equal (cdr (nthcdr idx lst)) (nthcdr (+ 1 idx) lst))))
+
+
+;; (in-theory (disable length))
+
+;; (in-theory (disable array1p compress1 default dimensions header
+;; 		    aref1 aset1 maximum-length))
+
+;; (defthm array1p-module-type
+;;   (implies
+;;    (array1p name l)
+;;    (and (symbolp name)
+;; 	(alistp l)
+;; 	(consp (header name l))
+;; 	(consp (dimensions name l))
+;; 	(true-listp (dimensions name l))
+;; 	(integerp (car (dimensions name l)))
+;; 	(<= 0 (car (dimensions name l)))
+;; 	(integerp (maximum-length name l))
+;; 	(<= 0 (maximum-length name l))))
+;;   :hints (("Goal" :in-theory (enable array1p header default dimensions
+;; 				     maximum-length)))
+;;   :rule-classes
+;;   ((:type-prescription :corollary
+;; 	         (implies
+;; 		  (array1p name l)
+;; 		  (and (consp (header name l)))))
+;;    (:type-prescription :corollary
+;; 	         (implies
+;; 		  (array1p name l)
+;; 		  (and (consp (dimensions name l))
+;; 		       (true-listp (dimensions name l)))))
+;;    (:type-prescription :corollary
+;; 	         (implies
+;; 		  (array1p name l)
+;; 		  (and (integerp (car (dimensions name l)))
+;; 		       (<= 0 (car (dimensions name l))))))
+;;    (:type-prescription :corollary
+;; 	         (implies
+;; 		  (array1p name l)
+;; 		  (and (integerp (maximum-length name l))
+;; 		       (<= 0 (maximum-length name l)))))))
+
+
+;; (local
+;; (defthm compress11-empty-array
+;;     (implies (and (integerp n) (>= n 0))
+;; 	     (equal (compress11 name (list (cons :header info)) n dim default)
+;; 		    nil))
+;;   :hints (("Goal" :In-theory (enable compress11)))))
+
+
+;; (defthm compress1-empty-array
+;;      (equal (compress1 tag (list (cons :header x)))
+;; 	    (list (cons :header x)))
+;;    :hints (("Goal" :in-theory (enable compress1 compress11
+;; 				      header default))))
+
+;; (defthm array1p-cons-with-dimensions
+;;     (implies (and (array1p tag array)
+;; 		  (integerp index)
+;; 		  (>= index 0)
+;; 		  (> (car (dimensions tag array)) index))
+;; 	     (array1p tag (cons (cons index val) array)))
+;;   :hints (("goal" :in-theory (enable dimensions header))))
+
diff --git a/books/workshops/2000/manolios/pipeline/trivial/sawada-model/utils.acl2 b/books/workshops/2000/manolios/pipeline/trivial/sawada-model/utils.acl2
new file mode 100644
index 0000000..fee05b6
--- /dev/null
+++ b/books/workshops/2000/manolios/pipeline/trivial/sawada-model/utils.acl2
@@ -0,0 +1,4 @@
+(in-package "ACL2")
+(include-book "data-structures/portcullis" :dir :system)
+(certify-book "utils" ? t)
+
diff --git a/books/workshops/2000/manolios/pipeline/trivial/sawada-model/utils.lisp b/books/workshops/2000/manolios/pipeline/trivial/sawada-model/utils.lisp
new file mode 100644
index 0000000..5c59580
--- /dev/null
+++ b/books/workshops/2000/manolios/pipeline/trivial/sawada-model/utils.lisp
@@ -0,0 +1,104 @@
+(in-package "ACL2")
+
+(include-book "../../../../../../data-structures/utilities")
+
+(u::import-as-macros
+ U::A-UNIQUE-SYMBOL-IN-THE-U-PACKAGE
+ defloop)
+
+(defloop non-rec-functions (runes world)
+  (for ((rune in runes))
+       (unless (fgetprop (cadr rune) 'induction-machine nil world)
+	 (collect rune))))
+
+(defloop rec-functions (runes world)
+  (for ((rune in runes))
+       (when (fgetprop (cadr rune) 'induction-machine nil world)
+	 (collect rune))))
+
+
+(defmacro ww (form)
+  "With (W state) ..."
+  `(LET ((WORLD (W STATE))) ,form))
+
+;Example
+;(ww (non-rec-functions (definition-theory (current-theory :here)) world))
+
+;Example
+; (deftheory test (non-rec-functions (theory 'table-def) world))
+
+
+;
+; Macro ld-up-to fast loads ACL2 events in a file to a specified point.
+;  (ld-up-to "<filename>" <event_name>  {:speed <speed> })
+; This command loads ACL2 file <filename> to the point where
+; <event_name> is first defined.
+
+; Since ld-up-to skips proofs of the theorems in a loaded file by
+; default, a user can quickly reach the state where he or she wants
+; to work in.  <even_name> can be any symbol newly defined by the
+; event at the desired breaking point.  For instance, a label
+; defined by deflabel can be used as well.  Keyword :all can be
+; specified when the user want to load the whole file.
+
+;
+; The user can specify loading speed using keyword :speed
+;  :speed 0  Does not skip proofs. The slowest way to load a file.
+;  :speed 1  Skips proofs, but performs other checks on theorems.
+;            Ld-up-to loads files at this speed by default.
+;  :speed 2  Skips proofs and other checks on theorems.  Warning
+;            will not be printed out.  It also skips events local to
+;            the ACL2 file.
+
+; Example
+;  (ld-up-to "invariants-def.lisp" invariants)
+;   This command loads ACL2 file invariant-def.lisp until it finds the
+;   definition of function invariants.
+;
+;  (ld-up-to "invariants-def.lisp" :all :speed 2)
+;   this command load the all events in invariants-def.lisp except
+;   events local to the ACL2 book.
+(defmacro ld-up-to (file event &key (speed '1))
+  (let ((skip-proofs-flag (if (equal speed 0) nil
+			      (if (equal speed 1) t ''include-book))))
+      `(ld ,file :ld-pre-eval-filter ',event :ld-skip-proofsp ,skip-proofs-flag)))
+
+
+; Macro refresh rolls back ACL2 history and reloads ACL2 events fast.
+;
+; (refresh <filename> {:back-to <event1>} {:up-to <event2>} {:speed <speed>})
+;
+
+; Refresh first undoes events back to the point where <event1> was
+; defined, then it loads ACL2 file <filename> up to the point where
+; <event2> is newly defined.  When previously executed ACL2 events
+; like definition and theorems are modified, the current world of ACL2
+; is corrupted and a user may want to restart the ACL2 from scratch.
+; However, restarting ACL2 takes a long time especially if many books
+; are loaded.  Refresh helps to reload modified files and get the
+; newest state of ACL2 world quickly.  It only undoes to the point
+; where symbol <event1> is defined, and then loads file <filename>,
+; skipping proofs by default.  Since refresh loads ACL2 books included
+; by <filename>, usually the user only has to specify the top ACL2 book.
+; <event1> can be a symbol defined in an included book, and refresh
+; undoes the include-book of the included book.  If :back-to
+; keyword is not supplied, refresh undoes all user defined events.  If
+; :up-to keyword is not given, it load all events in <filename>.  So
+; (refresh <filename>) is equivalent to (refresh <filename> :back-to 1
+; :up-to :all).  <event1> can be a number designating an event.
+;
+; The user can also specify loading speed using keyword :speed
+;  :speed 0  Does not skip proofs. The slowest way to load a file.
+;  :speed 1  Skips proofs, but performs other checks on theorems.
+;            Ld-up-to loads files at this speed by default.
+;  :speed 2  Skips proofs and other checks on theorems.  Warning
+;            will not be printed out.  It also skips events local to
+;            the ACL2 file.
+
+(defmacro refresh (file &key (back-to '1) (up-to ':all) (speed '1))
+  (let ((skip-proofs-flag (if (equal speed 0) nil
+			      (if (equal speed 1) t ''include-book))))
+    `(ld '((ubt! ',back-to) (ld ,file :ld-pre-eval-filter ',up-to
+			     :ld-skip-proofsp ,skip-proofs-flag)))))
+
+