diff options
| author | Camm Maguire <camm@debian.org> | 2017-05-08 12:58:52 -0400 |
|---|---|---|
| committer | Camm Maguire <camm@debian.org> | 2017-05-08 12:58:52 -0400 |
| commit | 092176848cbfd27b96c323cc30c54dff4c4a6872 (patch) | |
| tree | 91b91b4db76805fd2a09de0745b22080a9ebd335 /books/workshops/2004/matthews-vroon | |
Import acl2_7.4dfsg.orig.tar.gz
[dgit import orig acl2_7.4dfsg.orig.tar.gz]
Diffstat (limited to 'books/workshops/2004/matthews-vroon')
10 files changed, 3593 insertions, 0 deletions
diff --git a/books/workshops/2004/matthews-vroon/partial-clock-functions.pdf.gz b/books/workshops/2004/matthews-vroon/partial-clock-functions.pdf.gz Binary files differnew file mode 100644 index 0000000..4a49e6b --- /dev/null +++ b/books/workshops/2004/matthews-vroon/partial-clock-functions.pdf.gz diff --git a/books/workshops/2004/matthews-vroon/slides.pdf.gz b/books/workshops/2004/matthews-vroon/slides.pdf.gz Binary files differnew file mode 100644 index 0000000..f91ee2b --- /dev/null +++ b/books/workshops/2004/matthews-vroon/slides.pdf.gz diff --git a/books/workshops/2004/matthews-vroon/support/partial-clock-functions/efficient-simulator.lisp b/books/workshops/2004/matthews-vroon/support/partial-clock-functions/efficient-simulator.lisp new file mode 100644 index 0000000..fae5fb9 --- /dev/null +++ b/books/workshops/2004/matthews-vroon/support/partial-clock-functions/efficient-simulator.lisp @@ -0,0 +1,109 @@ +(in-package "ACL2") +(include-book "partial-clock-functions") + +(verify-guards omega) + +; note that this is admitted as an executable function. this is possible because: +; 1) we never change the original copy of mstate, so it fits with the rules of stobjs +; 2) acl2 allows functions that call partial functions to be declared executable. +; but because we do call a partial function inside steps-to-cutpoint-exec, any attempt +; to actually execute it result in an error; +(defun steps-to-cutpoint-exec (mstate) + (declare (xargs :stobjs (mstate))) + (let ((steps (steps-to-cutpoint-tail 0 (copy-from-mstate mstate)))) + (if (and (natp steps) ;the number of steps is a natural number. + (with-copy-of-stobj ;running a copy of our machine state forward steps steps + mstate ;gives us a cutpoint. + (mv-let (result mstate) + (let ((mstate (run steps mstate))) + (mv (at-cutpoint mstate) mstate)) + result))) + steps + (omega)))) + +(defthm o-p-steps-to-cutpoint-exec + (o-p (steps-to-cutpoint-exec mstate)) + :hints (("goal" :in-theory (enable steps-to-cutpoint-exec)))) + +(defthm steps-to-cutpoint-exec-steps-to-cutpoint + (implies (mstatep mstate) + (equal (steps-to-cutpoint-exec mstate) + (steps-to-cutpoint mstate))) + :hints (("goal" :in-theory (enable steps-to-cutpoint)))) + +(in-theory (disable steps-to-cutpoint-exec)) + +(defun dummy-mstate (mstate) + (declare (xargs :stobjs (mstate))) + (update-progc -1 mstate)) + +(defun next-cutpoint-exec (mstate) + (declare (xargs :stobjs (mstate) + :measure (steps-to-cutpoint-exec mstate) + :guard (and (mstatep mstate) + (natp (steps-to-cutpoint-exec mstate))))) + (if (mbt (and (mstatep mstate) + (natp (steps-to-cutpoint-exec mstate)))) + (if (at-cutpoint mstate) + mstate + (let ((mstate (next mstate))) + (next-cutpoint-exec mstate))) + (dummy-mstate mstate))) + + +; (defexec next-cutpoint-exec (mstate) +; (declare (xargs :stobjs (mstate) +; :measure (steps-to-cutpoint-exec mstate) +; :guard (and (mstatep mstate) +; (natp (steps-to-cutpoint-exec mstate)))) +; (exec-xargs :default-value (dummy-mstate mstate))) +; (mbe :exec (if (at-cutpoint mstate) +; mstate +; (let ((mstate (next mstate))) +; (next-cutpoint-exec mstate))) +; :logic (cond ((at-cutpoint mstate) mstate) +; ((or (not (natp (steps-to-cutpoint-exec mstate))) +; (not (mstatep mstate))) +; (dummy-mstate mstate)) +; (t (let ((mstate (next mstate))) +; (next-cutpoint-exec mstate)))))) + +(defthm next-cutpoint-exec-cutpoint-exec + (implies (and (mstatep mstate) + (natp (steps-to-cutpoint-exec mstate))) + (equal (next-cutpoint-exec mstate) + (next-cutpoint mstate))) + :hints (("goal" :in-theory (e/d (next-cutpoint run) + (next-cutpoint-intro-next))))) + +(in-theory (disable next-cutpoint-exec)) + +(defun cutpoint-to-cutpoint-exec (mstate) + (declare (xargs :stobjs (mstate) + :guard (and (at-cutpoint mstate) + (not (at-exitpoint mstate))))) + (let ((mstate (next mstate))) + (next-cutpoint-exec mstate))) + +(defthm cutpoint-to-cutpoint-exec-cutpoint-to-cutpoint + (implies (and (mstatep mstate) + (at-cutpoint mstate) + (not (at-exitpoint mstate))) + (equal (cutpoint-to-cutpoint-exec mstate) + (cutpoint-to-cutpoint mstate))) + :hints (("goal" :in-theory (enable cutpoint-to-cutpoint)))) + +(in-theory (disable cutpoint-to-cutpoint-exec)) + +(defun fast-cutpoint-to-cutpoint (mstate) + (declare (xargs :stobjs (mstate) + :measure (cutpoint-measure mstate) + :guard (at-cutpoint mstate))) + (if (mbt (at-cutpoint mstate)) + (if (at-exitpoint mstate) + mstate + (let ((mstate (cutpoint-to-cutpoint-exec mstate))) + (fast-cutpoint-to-cutpoint mstate))) + (dummy-mstate mstate))) + +#|==================================================================|#
\ No newline at end of file diff --git a/books/workshops/2004/matthews-vroon/support/partial-clock-functions/partial-clock-functions.lisp b/books/workshops/2004/matthews-vroon/support/partial-clock-functions/partial-clock-functions.lisp new file mode 100644 index 0000000..ac28931 --- /dev/null +++ b/books/workshops/2004/matthews-vroon/support/partial-clock-functions/partial-clock-functions.lisp @@ -0,0 +1,628 @@ +#|==================================================================|# + +#| + A template for using inductive assertions to prove + that a program eventually reaches an exit state. + Using this proof an efficient simulator can be + written that doesn't require step-counter parameters. + + However, ACL2 2.8 cannot execute these simulators + as they are written, because some of the guards + associated with function calls internal to the + simulators are not executable. Nevertheless, ACL2 + is able to prove that the guards hold for all + arguments the internal functions will be called on. + + Thus this restriction will hopefully be relaxed + in future versions of ACL2. +|# + +;(in-package "partial-clock-functions") +(in-package "ACL2") +(include-book "../tiny-fib-example/defstobj+") + +#|================ Generic arithmetic lemmas and books ===================|# + +(encapsulate + () + +; (Matt K., 10/2013: Changed rel8 to rel9.) + (local (include-book "rtl/rel9/arithmetic/top" :dir :system)) + (local (in-theory (enable mod-sum-cases mod-force-chosen-a-neg))) + + (defthm mod-zero-subtract-remainder + (implies (and (equal (mod m k) 0) + (natp m) + (posp k) + (integerp c) + (< c 0) + (<= (- k) c)) + (equal (mod (+ c m) k) + (+ k c)))) + + (defthm mod-zero-subtract-modulus-natp + (implies (and (equal (mod m k) 0) + (posp m) + (posp k) + (equal c (- k))) + (natp (+ c m)))) + + (defthm mod-zero-simplify-less + (implies (and (equal (mod n k) 0) + (integerp n) + (posp k) + (< n k)) + (<= n 0)) + :rule-classes :forward-chaining)) + +(include-book "arithmetic/top-with-meta" :dir :system) + + +#|========================== MSTATE theory =========================|# + +;;A very simple machine model with a next-state function, +;; called NEXT. The machine model itself is called MSTATE, +;; after the name of the stobj it is using. + +;A machine-state. For this example the state +; only contains a program counter. +(defstobj+ mstate + (progc :type integer :initially 0)) + +(defthm mstatep-type + (implies (mstatep mstate) + (consp mstate)) + :rule-classes :compound-recognizer) + +(defthm mstatep-cons + (iff (mstatep (cons pc rest)) + (and (integerp pc) + (equal rest nil)))) + +(defthm progc-integerp + (implies (mstatep mstate) + (integerp (progc mstate))) + :rule-classes :type-prescription) + +(defthm true-listp-len-zero + (implies (and (true-listp xs) + (equal (len xs) 0)) + (not xs)) + :rule-classes :forward-chaining) + +(defthm make-mstate + (implies (mstatep mstate) + (equal (list (progc mstate)) + mstate))) + +(defthm update-progc-type + (implies (and (mstatep mstate) + (integerp pc)) + (mstatep (update-progc pc mstate))) + :rule-classes (:type-prescription :rewrite)) + +(defthm update-progc-list + (implies (integerp pc) + (equal (update-progc pc (list pc)) + (list pc)))) + +(defthm update-progc-mstatep + (implies (mstatep mstate) + (equal (update-progc (progc mstate) mstate) + mstate))) + +(defthm progc-update-progc + (equal (progc (update-progc pc mstate)) + pc)) + +(defthm update-progc-twice + (equal (update-progc pc2 + (update-progc pc1 mstate)) + (update-progc pc2 mstate))) + +(in-theory (disable progc update-progc mstatep)) + +;A next-state function that simulates one step of a machine. +; For this example we just decrement the program counter. +(defund next (mstate) + (declare (xargs :stobjs (mstate))) + (update-progc (1- (progc mstate)) mstate)) + +;;A common form of induction used for +;; reasoning about runs of the machine. +(defun run-induction (n mstate) + (declare (xargs :stobjs (mstate))) + (cond + ((not (posp n)) mstate) + (t (let ((mstate (next mstate))) + (run-induction (1- n) mstate))))) + +(defthm negative-progc-implies-next-negative-progc + (implies (< (progc mstate) 0) + (< (progc (next mstate)) 0)) + :hints (("Goal" :in-theory (enable next))) + :rule-classes (:forward-chaining)) + +;; For this example we arbitrarily choose +;; a cutpoint state to be any valid mstate where +;; the program counter is nonnegative and evenly +;; divisible by 10. +(defund at-cutpoint (mstate) + (declare (xargs :stobjs (mstate))) + (and (mstatep mstate) + (natp (progc mstate)) + (equal (mod (progc mstate) 10) + 0))) + +(in-theory (disable mod)) + +(defthm prove-nil-not-cutpoint + (not (at-cutpoint nil)) + :hints (("Goal" :in-theory (enable at-cutpoint)))) + +;;NEXT preserves the structure of MSTATEs. +(defthm next-mstatep + (implies (mstatep mstate) + (mstatep (next mstate))) + :hints (("Goal" :in-theory (enable next)))) + +#|====== Partial clock functions and symbolic simulation ======|# + +(include-book "misc/defpun" :dir :system) +(include-book "ordinals/ordinals" :dir :system) + +(defthm nil-not-cutpoint + (not (at-cutpoint nil))) + +;A simulator that runs for N steps. +; N is a step-counter parameter. +(defun run (n mstate) + (declare (xargs :stobjs (mstate) + :guard (natp n))) + (if (zp n) + mstate + (let ((mstate (next mstate))) + (run (1- n) mstate)))) + +;A tail-recursive partial function that returns the +; number of steps until mstate reaches a cutpoint state, +; if in fact mstate can eventually reach a cutpoint state. +; The parameter N is an accumulator, which clients +; should initially set to zero. +(defpun steps-to-cutpoint-tail (n mstate) + (if (at-cutpoint mstate) + n + (steps-to-cutpoint-tail (1+ n) (run 1 mstate)))) + +;The number of steps until mstate reaches the next +; cutpoint state, if there is one. If there isn't, +; then this function returns zero. +(defun-nx steps-to-cutpoint (mstate) + (let ((steps (steps-to-cutpoint-tail 0 mstate))) + (if (at-cutpoint (run steps mstate)) + steps + (omega)))) + +;Simulate mstate until it reaches a cutpoint state, +; assuming it does. +(defun-nx run-to-cutpoint (mstate) + (run (steps-to-cutpoint mstate) mstate)) + +#| +;;This version of RUN-TO-CUTPOINT looks nicer, but +;; then (AT-CUTPOINT (RUN-TO-CUTPOINT MSTATE)) does +;; not imply that MSTATE eventually reaches a cutpoint +;; state. The problem is that if MSTATE never reaches +;; a cutpoint state then (RUN-TO-CUTPOINT MSTATE) can return anything, +;; including a cutpoint state. +(defpun run-to-cutpoint (mstate) + (if (at-cutpoint mstate) + mstate + (run-to-cutpoint (next mstate)))) +|# + +(defthm steps-to-cutpoint-tail-at-cutpoint + (implies (at-cutpoint mstate) + (equal (steps-to-cutpoint-tail n mstate) + n))) + +(defthm steps-to-cutpoint-tail-not-cutpoint + (implies (and (integerp n) + (not (at-cutpoint mstate))) + (equal (steps-to-cutpoint-tail n (run 1 mstate)) + (steps-to-cutpoint-tail (- n 1) mstate)))) + +(in-theory (disable steps-to-cutpoint-tail-def)) + +(defthm run-zero + (implies (zp n) + (equal (run n mstate) + mstate))) + +(defthm run-1 + (equal (next mstate) + (run 1 mstate))) + +(defthm run-plus + (let ((steps (cond + ((zp m) + n) + ((zp n) + m) + (t + (+ m n))))) + (equal (run m (run n mstate)) + (run steps mstate)))) + +(in-theory (disable run)) + +(defun-nx steps-to-cutpoint-induction (k mstate steps) + (declare (xargs :verify-guards nil + :guard (and (equal mstate mstate) + (equal steps steps)))) + (or (zp k) + (steps-to-cutpoint-induction (1- k) (next mstate) (1+ steps)))) + +(defthmd steps-to-cutpoint-tail-inv + (implies (and (at-cutpoint (run k mstate)) + (integerp steps)) + (let* ((result (steps-to-cutpoint-tail steps mstate)) + (cutpoint-steps (- result steps))) + (and (integerp result) + (natp cutpoint-steps) + (implies (natp k) + (<= cutpoint-steps k)) + (at-cutpoint (run cutpoint-steps mstate))))) + :hints (("Goal" :induct (steps-to-cutpoint-induction k mstate steps) + :do-not-induct t) + ("Subgoal *1/2" :cases ((at-cutpoint mstate))))) + +(defthm steps-to-cutpoint-tail-at-cutpoint-simp + (implies (at-cutpoint (run k mstate)) + (at-cutpoint (run (steps-to-cutpoint-tail 0 mstate) + mstate))) + :hints (("Goal" :use (:instance steps-to-cutpoint-tail-inv + (steps 0)))) + :rule-classes (:forward-chaining :rewrite)) + +(defthm steps-to-cutpoint-at-cutpoint + (implies (at-cutpoint (run k mstate)) + (at-cutpoint (run (steps-to-cutpoint mstate) + mstate))) + :rule-classes (:rewrite :forward-chaining)) + +(defthm steps-to-cutpoint-tail-diff + (implies (and (at-cutpoint (run k mstate)) + (syntaxp (not (equal n ''0))) + (integerp n)) + (equal (steps-to-cutpoint-tail n mstate) + (+ n (steps-to-cutpoint-tail 0 mstate)))) + :hints (("Goal" :use ((:instance steps-to-cutpoint-tail-inv + (k (- (steps-to-cutpoint-tail n mstate) + n)) + (steps 0)) + (:instance steps-to-cutpoint-tail-inv + (k (steps-to-cutpoint mstate)) + (steps n)) + (:instance steps-to-cutpoint-tail-inv + (steps 0)))))) + +(defthm not-at-cutpoint-implies-steps-to-cutpoint-tail-nonzero + (implies (and (at-cutpoint (run (steps-to-cutpoint-tail 0 mstate) + mstate)) + (not (at-cutpoint mstate))) + (posp (steps-to-cutpoint-tail 0 mstate))) + :rule-classes (:rewrite)) + +(defthm not-at-cutpoint-implies-steps-to-cutpoint-tail-nonzero-fwd-chain + (implies (and (at-cutpoint (run k mstate)) + (not (at-cutpoint mstate))) + (posp (steps-to-cutpoint-tail 0 mstate))) + :rule-classes (:forward-chaining)) + +(defthm natp-steps-to-cutpoint-tail + (implies (at-cutpoint (run (steps-to-cutpoint-tail 0 mstate) mstate)) + (natp (steps-to-cutpoint-tail 0 mstate))) + :hints (("Goal" :use (:instance steps-to-cutpoint-tail-inv))) + :rule-classes (:rewrite :forward-chaining)) + +(defthm natp-steps-to-cutpoint + (iff (at-cutpoint (run (steps-to-cutpoint mstate) mstate)) + (natp (steps-to-cutpoint mstate))) + :hints (("Goal" :use (:instance steps-to-cutpoint-tail-inv))) + :rule-classes (:rewrite)) + +(defthm steps-to-cutpoint-equals-omega-simp + (iff (equal (steps-to-cutpoint mstate) + (omega)) + (not (natp (steps-to-cutpoint mstate))))) + +(defthm o-p-steps-to-cutpoint + (o-p (steps-to-cutpoint mstate)) + :hints (("Goal" :cases ((natp (steps-to-cutpoint mstate)))))) + +(defthm steps-to-cutpoint-zero + (implies (at-cutpoint mstate) + (equal (steps-to-cutpoint mstate) 0))) + +(defthm integerp-add + (iff (integerp (+ -1 n)) + (or (integerp n) + (not (acl2-numberp n))))) + +(defthmd steps-to-cutpoint-nonzero-intro + (implies (not (at-cutpoint mstate)) + (equal (steps-to-cutpoint mstate) + (o+ 1 (steps-to-cutpoint (next mstate))))) + :hints (("Subgoal 1'" :cases ((equal (steps-to-cutpoint-tail 0 mstate) + 0))))) + +(defthm integerp-ord-decrement + (implies (natp n) + (equal (o- n 1) + (max 0 (- n 1)))) + :hints (("Goal" :in-theory (enable o-)))) + +(defthm natp-steps-to-cutpoint-increment + (iff (natp (o+ 1 (steps-to-cutpoint mstate))) + (natp (steps-to-cutpoint mstate))) + :hints (("Goal" :in-theory (enable o+)))) + +(defthm natp-steps-to-cutpoint-decrement + (iff (natp (o- (steps-to-cutpoint mstate) 1)) + (natp (steps-to-cutpoint mstate))) + :hints (("Goal" :in-theory (enable o-)))) + +(defthm omega-minus-one-equals-omega + (equal (o- (omega) 1) + (omega)) + :hints (("Goal" :in-theory (enable o-)))) + +(defthmd natp-ord-decrement + (iff (natp (o- n 1)) + (or (and (o-finp n) + (or (<= n 1) + (posp n))) + (< (o-first-expt n) 0))) + :hints (("Goal" :in-theory (enable o- o< o-finp)))) + +(defthm o-finp-steps-to-cutpoint-iff-natp + (iff (o-finp (steps-to-cutpoint mstate)) + (natp (steps-to-cutpoint mstate)))) + +(defthmd convert-at-cutpoint-to-steps-to-cutpoint + (iff (at-cutpoint mstate) + (equal (steps-to-cutpoint mstate) + 0))) + +(defthm at-cutpoint-implies-steps-to-cutpoint-zero + (implies (at-cutpoint mstate) + (equal (steps-to-cutpoint mstate) + 0)) + :rule-classes :forward-chaining) + +(defthm not-at-cutpoint-implies-steps-to-cutpoint-nonzero + (implies (not (at-cutpoint mstate)) + (not (equal (steps-to-cutpoint mstate) + 0))) + :rule-classes :forward-chaining) + +(defthmd steps-to-cutpoint-nonzero-elim + (implies (not (at-cutpoint mstate)) + (equal (steps-to-cutpoint (next mstate)) + (o- (steps-to-cutpoint mstate) 1))) + :hints (("Goal" :in-theory (enable steps-to-cutpoint-nonzero-intro)))) + +(defthm natp-steps-to-cutpoint-run + (implies (natp (steps-to-cutpoint (run k mstate))) + (natp (steps-to-cutpoint mstate)))) + +(in-theory (disable steps-to-cutpoint)) + +(defthm steps-to-cutpoint-run-1-elim + (implies (not (at-cutpoint mstate)) + (equal (steps-to-cutpoint (run 1 mstate)) + (o- (steps-to-cutpoint mstate) 1))) + :hints (("Goal" :in-theory (e/d (steps-to-cutpoint-nonzero-elim run) + (run-1))))) + +;Simulate MSTATE until it reaches the next +; cutpoint state, if there is one. If there isn't, +; then return NIL. +; This function allows simpler rewrite rules +; than RUN-TO-CUTPOINT does. + +(defun-nx next-cutpoint (mstate) + (let ((steps (steps-to-cutpoint mstate))) + (if (natp steps) + (run steps mstate) + nil))) + +;;A derived induction scheme, useful for reasoning +;; about NEXT-CUTPOINT +(defun-nx next-cutpoint-induction (k mstate) + (cond + ((at-cutpoint mstate) + t) + ((zp k) + t) + (t + (next-cutpoint-induction (+ -1 k) (next mstate))))) + +(defthm next-cutpoint-at-cutpoint + (implies (at-cutpoint mstate) + (equal (next-cutpoint mstate) + mstate))) + +(defthmd next-cutpoint-elim-next + (implies (not (at-cutpoint mstate)) + (equal (next-cutpoint (next mstate)) + (next-cutpoint mstate)))) + +(defthm next-cutpoint-intro-next + (implies (not (at-cutpoint mstate)) + (equal (next-cutpoint mstate) + (next-cutpoint (next mstate))))) + +(defthm next-cutpoint-reaches-cutpoint + (iff (at-cutpoint (next-cutpoint mstate)) + (natp (steps-to-cutpoint mstate)))) + +(in-theory (e/d (steps-to-cutpoint-nonzero-intro) (next-cutpoint))) + +(defun-nx cutpoint-to-cutpoint (mstate) + (next-cutpoint (next mstate))) + +(defthm cutpoint-to-cutpoint-returns-cutpoint-state + (implies (natp (steps-to-cutpoint (next mstate))) + (at-cutpoint (cutpoint-to-cutpoint mstate)))) + +(defthmd convert-cutpoint-to-cutpoint-to-run + (let ((steps (steps-to-cutpoint (next mstate)))) + (implies (natp steps) + (equal (cutpoint-to-cutpoint mstate) + (run (+ 1 steps) mstate)))) + :hints (("Goal" :in-theory (enable next-cutpoint)))) + +(in-theory (disable cutpoint-to-cutpoint run-1)) + +(defthm run-cutpoint-to-cutpoint + (let ((steps (steps-to-cutpoint (next mstate)))) + (implies (and (natp steps) + (natp k)) + (equal (run k (cutpoint-to-cutpoint mstate)) + (run (+ 1 k steps) mstate)))) + :hints (("Goal" :in-theory (enable convert-cutpoint-to-cutpoint-to-run)))) + + +#|================== Program exit points =================|# + +;;For this example we arbitrarily define the program to +;; have exited when the program counter has reached zero. +(defund at-exitpoint (mstate) + (declare (xargs :stobjs (mstate))) + (and (mstatep mstate) + (equal (progc mstate) + 0))) + +(defthm not-at-exitpoint-implies-not-progc-zero + (implies (and (mstatep mstate) + (not (at-exitpoint mstate)) + (natp (progc mstate))) + (posp (progc mstate))) + :hints (("Goal" :in-theory (enable at-exitpoint)))) + +(defthm at-exitpoint-implies-at-cutpoint + (implies (at-exitpoint mstate) + (at-cutpoint mstate)) + :hints (("Goal" :in-theory (enable at-exitpoint at-cutpoint)))) + +(defthm prove-steps-to-next-cutpoint-natp + (implies (and (at-cutpoint mstate) + (not (at-exitpoint mstate))) + (natp (steps-to-cutpoint (next mstate)))) + :hints (("Goal" :in-theory (enable at-cutpoint next)))) + +;; This is an ordinal measure function that should +;; decrease from cutpoint to cutpoint, until an +;; exit point has been reached. In this example we +;; just use the value of the program counter. +(defun cutpoint-measure (mstate) + (declare (xargs :stobjs (mstate))) + (nfix (progc mstate))) + +(defthm prove-cutpoint-measure-is-ordinal + (o-p (cutpoint-measure mstate))) + +(defthm prove-cutpoint-measure-decreases + (implies (and (at-cutpoint mstate) + (not (at-exitpoint mstate))) + (o< (cutpoint-measure (cutpoint-to-cutpoint mstate)) + (cutpoint-measure mstate))) + :hints (("Goal" :in-theory (enable cutpoint-to-cutpoint next + at-cutpoint at-exitpoint)))) + +(in-theory (disable cutpoint-measure cutpoint-to-cutpoint)) + + +#|================= The termination proof ===============|# + +;;Proves that every cutpoint state eventually +;; leads to an exitpoint state. + +(defthm steps-to-next-cutpoint-natp + (implies (and (at-cutpoint mstate) + (not (at-exitpoint mstate))) + (natp (steps-to-cutpoint (next mstate))))) + +(defthm cutpoint-measure-is-ordinal + (o-p (cutpoint-measure mstate))) + +(defthm cutpoint-measure-decreases + (implies (and (at-cutpoint mstate) + (not (at-exitpoint mstate))) + (o< (cutpoint-measure (cutpoint-to-cutpoint mstate)) + (cutpoint-measure mstate)))) + +;;Number of machine steps until we exit, assuming +;; we start at a cutpoint state. +(defun-nx steps-to-exitpoint (mstate) + (declare (xargs :measure (cutpoint-measure mstate))) + (cond + ((not (at-cutpoint mstate)) 0) + ((at-exitpoint mstate) 0) + (t (+ 1 (steps-to-cutpoint (next mstate)) + (steps-to-exitpoint (cutpoint-to-cutpoint mstate)))))) + +(defthmd adding-natp-args-implies-natp + (implies (and (natp m) + (natp n)) + (natp (binary-+ m n)))) + +(defthm steps-to-exitpoint-natp + (natp (steps-to-exitpoint mstate)) + :rule-classes :type-prescription + :hints (("Goal" :in-theory (enable cutpoint-to-cutpoint + adding-natp-args-implies-natp)))) + +(defun-nx next-exitpoint (mstate) + (declare (xargs :measure (cutpoint-measure mstate))) + (cond + ((not (at-cutpoint mstate)) + mstate) + ((at-exitpoint mstate) + mstate) + (t + (next-exitpoint (cutpoint-to-cutpoint mstate))))) + +;;This is the guard verification condition for +;; a more efficient guarded version of NEXT-EXITPOINT +;; that assumes it starts in a cutpoint state. However, +;; CUTPOINT-TO-CUTPOINT is still non-executable. +(defthmd next-exitpoint-mbe + (implies (and (at-cutpoint mstate) + (not (at-exitpoint mstate))) + (equal (next-exitpoint (cutpoint-to-cutpoint mstate)) + (next-exitpoint mstate)))) + +;;The following two theorems show that any cutpoint +;; state eventually leads to an exitpoint state. + +(defthmd next-exitpoint-correct + (implies (at-cutpoint mstate) + (equal (run (steps-to-exitpoint mstate) mstate) + (next-exitpoint mstate))) + :hints (("Goal" :induct (steps-to-exitpoint mstate) + :do-not-induct t))) + +(defthm at-cutpoint-implies-reaches-exitpoint + (implies (at-cutpoint mstate) + (at-exitpoint (next-exitpoint mstate))) + :hints (("Goal" :induct (next-exitpoint mstate)))) + +(defthm cutpoint-implies-mstatep + (implies (at-cutpoint mstate) + (mstatep mstate)) + :hints (("Goal" :in-theory (enable at-cutpoint)))) + +#|==================================================================|# diff --git a/books/workshops/2004/matthews-vroon/support/tiny-fib-example/defstobj+.lisp b/books/workshops/2004/matthews-vroon/support/tiny-fib-example/defstobj+.lisp new file mode 100644 index 0000000..0104b5c --- /dev/null +++ b/books/workshops/2004/matthews-vroon/support/tiny-fib-example/defstobj+.lisp @@ -0,0 +1,756 @@ +(in-package "ACL2") + +;This book was created by Daron Vroon on August 10, 2004 + +;The purpose of this book is to define a macro, defstobj+, which +;defines a defstobj, functions that copy to and from the defstobj from +;and to a non-stobj of similar shape, and theorems that these functions +;are logically the identity. + +;This gets challenging if the stobj has arrays in it. These must be +;copied element by element using the element accessor defined by the +;defstobj. For example, consider the following stobj from the tiny +;machine (developed at Rockwell Collins, and published in the ACL2 case +;studies book): + +;(defstobj tiny-state +; (progc :type (unsigned-byte 10) +; :initially 0) +; (mem :type (array (signed-byte 32) (1024)) +; :initially 0) +; (dtos :type (unsigned-byte 10) +; :initially 0) +; (ctos :type (unsigned-byte 10) +; :initially 0) +; :inline t) + +;Copying the non-array elements is simple, using the update-progc and +;progc functions. The mem field only has accessors for its elements, so +;it must be copied one element at a time: + +;(defun copy-to-tiny-state-mem +; (n mem tiny-state) +; (declare (xargs :stobjs (tiny-state) +; :measure (acl2-count (1+ n)) +; :guard +; (and (memp mem) +; (equal (length mem) 1024) +; (natp n) +; (<= n 1024)))) +; (if (or (zp n) (< 1024 n)) +; tiny-state +; (let* ((n (1- n)) +; (tiny-state (update-memi n (nth n mem) tiny-state))) +; (copy-to-tiny-state-mem n mem tiny-state)))) + +;and + +;(defun copy-from-tiny-state-mem (n tiny-state) +; (declare (xargs :stobjs (tiny-state) +; :guard (and (natp n) (<= n 1024)))) +; (if (zp n) +; nil +; (cons (memi (- 1024 n) tiny-state) +; (copy-from-tiny-state-mem (1- n) +; tiny-state)))) + +;Proving that each of these behaves correctly requires a 2 step +;process. First we need to prove a more general theorem proven by +;induction over n. Then we can prove the overall theorem that the +;functions work correctly when n = (len (nth *memi* tiny-state)). +;Rather than do this two step process for every array field of every +;stobj defined using defstobj+, we define generic versions of array +;copying functions that are very similar to the ones defined +;above. These are called copy-to-stobj-array and +;copy-from-stobj-array. See their definitions below. Once they are +;defined, we prove that they do what we want (basically, that they are +;noops). The defstobj+ macro then simply defines array copy functions +;such as the ones above, and proves that they are logically equivalent +;to the generic functions. + +;The only other difficulty of this macro is the guard proofs for the +;functions it generates (such as the ones above). In order to prove +;these, we need to prove that each array field is a true-list and that +;every element of those arrays is of the appropriate type. However, +;these are useful theorems in general, so we export them from defstobj+ +;as well. Another "bonus" of this macro is a function that is logically +;identical to the stobj recognizer predicate, but works on +;non-stobjs. In our running example, the defstobj above creates a +;function called tiny-statep that is a recognizer predicate for the +;stobj. Our macro also includes a function called logical-tiny-statep +;which is logically equivalent to tiny-statep, but works on +;non-stobjs. We then immediately prove this fact and turn off the +;definition. + +;USAGE + +;Simply call defstobj+ like you would defstobj. It should work in any +;package. The only problem we have found is if you define the stobj to +;have a name in a package different than the current package. For +;example + +;(defstobj+ FOO::tiny-state +; (progc :type (unsigned-byte 10) +; :initially 0) +; (mem :type (array (signed-byte 32) (1024)) +; :initially 0) +; (dtos :type (unsigned-byte 10) +; :initially 0) +; (ctos :type (unsigned-byte 10) +; :initially 0) +; :inline t) + +;will break if you are in package BAR. This is due to the fact that +;defstobj (which is called by this macro) puts all of the functions +;it generates into the current package instead of the package of the +;stobj name. Since we haven't found a way of getting at the current +;package in a macro, we cannot follow suit. When we try to use +;functions generated by the defstobj, we call them in the package of +;the name of the stobj, and everything breaks. + +;When you have successfully run defstobj+, you get everything that a +;defstobj generates. In addition, you get the following: + +;(DEFUN COPY-TO-c (COPY c) ...) ;puts all the data in COPY into the stobj c. + +;(DEFTHM COPY-TO-c-NOOP +; (IMPLIES (AND (cP X) +; (cP Y)) +; (EQUAL (COPY-TO-c X Y) +; X))) + +;(DEFTHM COPY-TO-c-IGNORES-SECOND-ARG +; (IMPLIES (AND (cP X) +; (CP Y)) +; (EQUAL (EQUAL (COPY-TO-c COPY X) +; (COPY-TO-c COPY Y)) +; T))) + +;(DEFUN COPY-FROM-c (c) ...) ;creates a non-stobj that is logically identical to c. + +;(DEFTHM COPY-FROM-c-NOOP +; (IMPLIES (cP c) +; (EQUAL (COPY-FROM-c c) c))) + +;(DEFUN LOGICAL-cP (X) ...) ;logically equivalent to cP, but x doesn't need to +; ;be a stobj. +;(DEFTHM LOGICAL-cP-cP +; (EQUAL (LOGICAL-cP X) +; (cP X))) + +;where c is the name of your stobj. In addition, for each array field, +;a of c, you get the following: + +;(DEFTHM aP-TRUE-LISTP +; (IMPLIES (aP X) (TRUE-LISTP X))) + +;(DEFTHM aP-NTH-TYPE +; (IMPLIES (AND (aP X) (NATP N) (< N (LEN X))) +; (typep(NTH N X)))) + +;(DEFUN COPY-TO-c-a (N a c) ...) ;called by COPY-TO-c +;(DEFUN COPY-FROM-c-a (N c) ...) ;called by COPY-FROM-c + +;where typep is the predicate associated with the type of elements in +;a. To see what the predicate is for a given type, see the ACL2 +;documentation topic type-spec. + +;Including this book also provides some useful theorems about +;update-nth, nth, and a couple other functions. To turn these off, +;simply run the form: + +;(in-theory (disable defstobj+-theory)) + +;Don't worry about the macro, it turns on everything it needs locally. + +;MODIFIED by Daron Vroon on October 18, 2004: + +;I've added a with-copy-of-stobj macro. The usage is identical to that +;of with-local-stobj (see ACL2 documentation). However, instead of +;creating a blank copy of the stobj for the form, it creates a copy of +;the current version of the stobj. + +;For our purposes, this is useful since we can take the current state +;of our machine and run it forward to see what happens without +;actually changing the state of the machine. + +;Basically, the macro uses copy-from- and copy-to- functions as +;follows. First, the macro creates a non-stobj copy of the stobj. Then +;it calls with-local-stobj to create a local copy of the stobj. Before +;computing anything, it puts the contents of the non-stobj copy into +;the local stobj. Finally, it performs the computation given by the +;user using the local copy. + +(local + ;; [Jared] changed this to use arithmetic-3 instead of 2 + (include-book "arithmetic-3/bind-free/top" :dir :system)) + + +;we only want the stuff in this book + ground-zero theory for our +;proofs. so we have defstobj+-before and defstobj+-after. +(deflabel defstobj+-before) + +;;;firstn + +(local + (defun firstn (n l) + (declare (xargs :guard (and (true-listp l) + (integerp n) + (<= 0 n)))) + (cond ((endp l) nil) + ((zp n) nil) + (t (cons (car l) + (firstn (1- n) (cdr l))))))) + +;;;lastn + +(local + (defun lastn (n a) + (declare (xargs :guard (and (natp n)))) + (if (or (atom a) (zp n)) + a (lastn (1- n) (cdr a))))) + + +(local + (defthm car-lastn + (equal (car (lastn n x)) + (nth n x)) + :hints (("Goal" :in-theory (enable nth))))) + +(local + (defthm cdr-lastn + (implies (and (natp n) + (true-listp x)) + (equal (cdr (lastn n x)) + (lastn (1+ n) x))))) + +(local + (defthm consp-lastn + (implies (and (< n (len x)) + (<= 0 n)) + (consp (lastn n x))))) + +(local + (defthm lastn-alt-def + (implies (and (natp n) + (true-listp x) + (< n (len x))) + (equal (lastn n x) + (cons (nth n x) + (lastn (1+ n) x)))) + :hints (("goal" + :in-theory (disable car-lastn cdr-lastn lastn) + :use (car-lastn cdr-lastn))))) + +(local + (defthm lastn-nil + (implies (and (true-listp x) + (<= (len x) n) + (natp n)) + (equal (lastn n x) + nil)))) + +(local + (defthm lastn-0 + (equal (lastn 0 x) x))) + +(local (in-theory (disable lastn))) + +;;;;;;;;;;;;;;;update-nth/nth stuff;;;;;;;;;;;;;;;;;;;;;;; +;i'm not sure exactly how much of this is necessary. i just grabbed +;these theorems from tiny.lisp + +(defthm nth-update-nth2 + (equal + (nth n1 (update-nth n2 v l)) + (if (equal (nfix n1) (nfix n2)) + v + (nth n1 l))) + :hints (("goal" :in-theory (enable update-nth nth)))) + +(defthm nth-update-nth-1 + (implies + (not (equal (nfix n1) (nfix n2))) + (equal + (nth n1 (update-nth n2 v l)) + (nth n1 l)))) + +(defthm nth-update-nth-2 + (implies + (equal (nfix n1) (nfix n2)) + (equal + (nth n1 (update-nth n2 v l)) + v))) + +(defun repeat (n v) + (if (zp n) + nil + (cons v (repeat (1- n) v)))) + +(defthm update-nth-nil + (equal (update-nth i v nil) + (append (repeat i nil) (list v))) + :hints (("goal" :in-theory (enable update-nth)))) + +(defthm update-nth-nth-noop-helper + (implies + (and (<= 0 n) (< n (len l))) + (equal (update-nth n (nth n l) l) l)) + :hints (("goal" :in-theory (enable nth update-nth)))) + +(defthm update-nth-nth-noop + (implies + (and (<= 0 n) (< n (len l1)) (equal (nth n l1) (nth n l2))) + (equal (update-nth n (nth n l2) l1) l1))) + +;; order update-nth terms based on update field value +(defthm update-nth-update-nth-diff + (implies + (not (equal (nfix i1) (nfix i2))) + (equal (update-nth i1 v1 (update-nth i2 v2 l)) + (update-nth i2 v2 (update-nth i1 v1 l)))) + :hints (("goal" :in-theory (enable update-nth nfix))) + :rule-classes ((:rewrite :loop-stopper ((i1 i2))))) + +(defthm update-nth-update-nth-same + (equal (update-nth i v1 (update-nth i v2 l)) + (update-nth i v1 l)) + :hints (("goal" :in-theory (enable update-nth)))) + +(defthm len-repeat + (equal (len (repeat i v)) (nfix i)) + :hints (("goal" :in-theory (enable nfix)))) + +(defthm len-update-nth-better + (equal (len (update-nth i v l)) (max (1+ (nfix i)) (len l))) + :hints (("goal" :in-theory (enable update-nth max)))) + +(defthm car-update-nth + (equal (car (update-nth i v l)) (if (zp i) v (car l))) + :hints (("goal" :in-theory (enable update-nth)))) + +(defthm cdr-update-nth + (equal (cdr (update-nth n x y)) + (if (zp n) (cdr y) (update-nth (1- n) x (cdr y))))) + +;;;copy-from-stobj stuff + +(defun copy-from-stobj-array (n array) + (if (zp n) + nil + (cons (nth (- (len array) n) array) + (copy-from-stobj-array (1- n) array)))) + +(local + (defthm copy-from-stobj-array-noop-l1 + (implies (and (natp n) + (true-listp array) + (<= n (len array))) + (equal (copy-from-stobj-array n array) + (lastn (- (len array) n) array))))) + +(in-theory (disable copy-from-stobj-array)) + +(defthm copy-from-stobj-array-noop + (implies (and (equal n (len array)) + (true-listp array)) + (equal (copy-from-stobj-array n array) + array)) + :hints (("goal" :use ((:instance copy-from-stobj-array-noop-l1 + (n (len array))))))) + +;;;copy-to-stobj stuff;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(defun copy-to-stobj-array (n mem1 mem2) + (if (or (zp n) + (< (len mem2) n)) + mem2 + (let* ((n (1- n)) + (mem2 (update-nth n (nth n mem1) mem2))) + (copy-to-stobj-array n mem1 mem2)))) + +(local + (defthm cdr-copy-to-stobj-array + (implies (and (consp mem2) + (<= n (len mem2)) + (natp n)) + (equal (cdr (copy-to-stobj-array n mem1 mem2)) + (copy-to-stobj-array (1- n) (cdr mem1) (cdr mem2)))) + :hints (("Goal" :in-theory (enable update-nth nth))))) + +(local + (defthm car-copy-to-stobj-array + (implies (and (consp mem2) + (<= n (len mem2)) + (posp n)) + (equal (car (copy-to-stobj-array n mem1 mem2)) + (car mem1))) + :hints (("Goal" :in-theory (enable update-nth nth))))) + +(in-theory (disable copy-to-stobj-array)) + +(local + (defun sub1-cdr-cdr-induction (n x1 x2) + (if (zp n) + (cons x1 x2) + (sub1-cdr-cdr-induction (1- n) (cdr x1) (cdr x2))))) + +(local + (defthm copy-to-stobj-array-firstn + (implies (and (consp mem1) + (consp mem2) + (equal (len mem1) + (len mem2)) + (<= n (len mem1)) + (natp n)) + (equal (firstn n (copy-to-stobj-array n mem1 mem2)) + (firstn n mem1))) + :hints (("Goal" :in-theory (enable update-nth nth) + :induct (sub1-cdr-cdr-induction n mem1 mem2))))) + +(local + (defthm firstn-with-large-index + (implies (and (<= (len l) (nfix n)) + (true-listp l)) + (equal (firstn n l) l)) + :hints (("goal" :in-theory (enable nfix))))) + +(local + (defthm true-listp-copy-to-stobj-array + (implies (true-listp x) + (true-listp (copy-to-stobj-array n y x))) + :hints (("Goal" :in-theory (enable copy-to-stobj-array))))) + +(local + (defthm len-copy-to-stobj-array + (implies (<= n (len x)) + (equal (len (copy-to-stobj-array n y x)) + (len x))) + :hints (("Goal" :in-theory (enable copy-to-stobj-array))))) + +(defthm copy-to-stobj-array-noop + (implies (and (equal n (len mem1)) + (equal n (len mem2)) + (consp mem1) + (consp mem2) + (true-listp mem1) + (true-listp mem2)) + (equal (copy-to-stobj-array n mem1 mem2) + mem1)) + :hints (("goal" :use copy-to-stobj-array-firstn))) + +;;;copy-to-stobj-array ignores 2nd argument. + +(local + (defun sub1-cdr-cdr-cdr-induction (n x1 x2 x3) + (if (zp n) + (list x1 x2 x3) + (sub1-cdr-cdr-cdr-induction (1- n) (cdr x1) (cdr x2) (cdr x3))))) + +(local + (defthm copy-to-stobj-array-ignores-second-arg-l1 + (implies (and (natp n) + (<= n (len mem2)) + (equal (len mem2) (len mem3))) + (equal (equal (firstn n (copy-to-stobj-array n mem1 mem2)) + (firstn n (copy-to-stobj-array n mem1 mem3))) + t)) + :hints (("Goal" :induct (sub1-cdr-cdr-cdr-induction n mem1 mem2 mem3))))) + +(defthm copy-to-stobj-array-ignores-second-arg + (implies (and (true-listp mem2) + (true-listp mem3) + (equal n (len mem2)) + (equal n (len mem3))) + (equal (equal (copy-to-stobj-array n mem1 mem2) + (copy-to-stobj-array n mem1 mem3)) + t)) + :hints (("Goal" :use copy-to-stobj-array-ignores-second-arg-l1))) + +;;;other helpful theorems: + +(defthm len-0-atom + (equal (equal 0 (len x)) + (atom x))) + +;(defthmd nth-constant-open +; (implies (and (syntaxp (quotep n)) +; (natp n)) +; (equal (nth n x) +; (if (equal n 0) (car x) (nth (1- n) (cdr x)))))) + +(defthmd cons-equal-car + (equal (equal x (cons (car x) rest)) + (and (consp x) + (equal (cdr x) rest)))) + +(defthm len>0-consp + (implies (< 0 (len x)) + (consp x))) + +(defthm add-cancel + (implies (and (syntaxp (quotep x)) + (syntaxp (quotep z)) + (rationalp y) + (rationalp z)) + (equal (equal (+ x y) z) + (equal y (+ (- x) z))))) + +(deflabel defstobj+-after) + +(deftheory defstobj+-theory + (set-difference-theories (current-theory 'defstobj+-after) + (current-theory 'defstobj+-before))) + +;and now, the macro: + +;snagged this from Dave Greve's work. It turns a list of symbols into +;a single string that is the concatination of the names of those symobols +(defun symbol-list-to-string (list) + (declare (xargs :guard (symbol-listp list))) + (if (consp list) + (concatenate 'string + (symbol-name (car list)) + (symbol-list-to-string (cdr list))) + "")) + +;again, snagged from Dave Greve. This concatinates symbols. The +;resulting symbol is put in the same package as the witness. +(defmacro join-symbols (witness &rest rst) + `(intern-in-package-of-symbol (symbol-list-to-string (list ,@rst)) + ,witness)) + +;this generates all the stuff necessary for each array field +(defun generate-array-theorems (stobj-name field-name elt-type len) + (declare (xargs :mode :program)) + (let* ((x (join-symbols stobj-name 'x)) + (n (join-symbols stobj-name 'n)) + (field-predicate (join-symbols stobj-name field-name 'p)) + (field-get (join-symbols stobj-name field-name 'i)) + (field-update (join-symbols stobj-name 'update- field-get)) + (field-index (join-symbols stobj-name '* field-name 'i*)) + (stobj-predicate (join-symbols stobj-name stobj-name 'p)) + (thm1name (join-symbols stobj-name + field-predicate + '-true-listp)) + (thm2name (join-symbols stobj-name + field-predicate + '-nth-type)) + (copy-to-name (join-symbols stobj-name + 'copy-to- + stobj-name + '- + field-name)) + (thm3name (join-symbols stobj-name + copy-to-name + '-copy-to-stobj-array)) + (copy-from-name (join-symbols stobj-name + 'copy-from- + stobj-name + '- + field-name)) + (thm4name (join-symbols stobj-name + copy-from-name + '-copy-from-stobj-array))) + (list + `(defthm ,thm1name + (implies (,field-predicate ,x) + (true-listp ,x))) + `(defthm ,thm2name + (implies (and (,field-predicate ,x) + (natp ,n) + (< ,n (len ,x))) + ,(translate-declaration-to-guard elt-type `(nth ,n ,x) nil))) + `(defun ,copy-to-name (,n ,field-name ,stobj-name) + (declare (xargs :stobjs (,stobj-name) + :measure (acl2-count (1+ ,n)) ;needed? + :guard (and (,field-predicate ,field-name) + (equal (length ,field-name) ,len) + (natp ,n) + (<= ,n ,len)))) + (if (or (zp ,n) + (< ,len ,n)) + ,stobj-name + (let* ((,n (1- ,n)) + (,stobj-name (,field-update ,n (nth ,n ,field-name) ,stobj-name))) + (,copy-to-name ,n ,field-name ,stobj-name)))) + `(local + (defthm ,thm3name + (implies (and (< ,field-index (len ,stobj-name)) + (equal (len (nth ,field-index ,stobj-name)) ,len)) + (equal (,copy-to-name ,n ,field-name ,stobj-name) + (update-nth + ,field-index + (copy-to-stobj-array ,n + ,field-name + (nth ,field-index ,stobj-name)) + ,stobj-name))) + :hints (("goal" :in-theory (enable copy-to-stobj-array))))) + `(in-theory (disable ,copy-to-name)) + `(defun ,copy-from-name (,n ,stobj-name) + (declare (xargs :stobjs (,stobj-name) + :guard (and (natp ,n) + (<= ,n ,len)))) + (if (zp ,n) + nil + (cons (,field-get (- ,len ,n) ,stobj-name) + (,copy-from-name (1- ,n) ,stobj-name)))) + `(local + (defthm ,thm4name + (implies (,stobj-predicate ,stobj-name) + (equal (,copy-from-name ,n ,stobj-name) + (copy-from-stobj-array ,n + (nth ,field-index + ,stobj-name)))) + :hints (("goal" :in-theory (enable copy-from-stobj-array)))))))) + +;this gets the type of a field from its definition. +(defun get-type-from-field-declaration (fd) + (cond ((endp fd) t) + ((equal (car fd) :type) (cadr fd)) + (t (get-type-from-field-declaration (cdr fd))))) + +;this generates all the theorems and defuns necessary. +;stobj-name is the name of the stobj (duh) +;field-defs is the list of field definitions left to be processed +;lsp is the list of predicates for the logical stobj predicate (aka lsp) +;ct keeps track of the actions necessary to copy to a stobj +;cf keeps track of the actions necessary to copy from a stobj +;array-thms keeps track of all the events generated for all the array fields +;len keeps track of the number of field-defs processed so far. at the end, it gives +; us the length of the stobj. +(defun generate-defstobj+-aux (stobj-name field-defs lsp ct cf array-thms len) + (declare (xargs :mode :program)) + (let ((x (join-symbols stobj-name 'x)) + (y (join-symbols stobj-name 'y)) + (copy (join-symbols stobj-name 'copy))) + (if (endp field-defs) ;when we are done, put everything together. + (let* ((stobj-predicate (join-symbols stobj-name stobj-name 'p)) + (lsp-name (join-symbols stobj-name 'logical- stobj-predicate)) + (thm1name (join-symbols stobj-name lsp-name '- stobj-predicate)) + (copy-to-name (join-symbols stobj-name 'copy-to- stobj-name)) + (copy-from-name (join-symbols stobj-name 'copy-from- stobj-name)) + (thm2name (join-symbols stobj-name copy-to-name '-noop)) + (thm3name (join-symbols stobj-name + copy-to-name + '-ignores-second-arg)) + (thm4name (join-symbols stobj-name copy-from-name '-noop))) + `((defun ,lsp-name (,x) + (declare (xargs :guard t)) + (and (true-listp ,x) + (equal (len ,x) ,len) + ,@lsp)) + (defthm ,thm1name + (equal (,lsp-name ,x) + (,stobj-predicate ,x))) + (in-theory (disable ,lsp-name)) + ,@array-thms + (defun ,copy-to-name (,copy ,stobj-name) + (declare (xargs :stobjs (,stobj-name) + :guard (,lsp-name ,copy))) + (let* ,ct ,stobj-name)) + (defthm ,thm2name + (implies (and (,stobj-predicate ,x) + (,stobj-predicate ,y)) + (equal (,copy-to-name ,x ,y) + ,x)) + :hints (("goal" :in-theory (enable cons-equal-car)))) + (defthm ,thm3name + (implies (and (,stobj-predicate ,x) + (,stobj-predicate ,y)) + (equal (equal (,copy-to-name ,copy ,x) + (,copy-to-name ,copy ,y)) + t))) + (defun ,copy-from-name (,stobj-name) + (declare (xargs :stobjs (,stobj-name))) + (list ,@(reverse cf))) + (defthm ,thm4name + (implies (,stobj-predicate ,stobj-name) + (equal (,copy-from-name ,stobj-name) + ,stobj-name)) + :hints (("goal" :in-theory (enable cons-equal-car)))) + (in-theory (disable ,copy-to-name ,copy-from-name)))) + (if (not (consp (car field-defs))) ;if the item is :inline, t, or nil, just continue. + (generate-defstobj+-aux stobj-name (cdr field-defs) lsp ct cf array-thms len) + (let* ((fd (car field-defs)) + (fname (car fd)) + (type (get-type-from-field-declaration (cdr fd))) + (field-predicate (join-symbols stobj-name fname 'p))) + (if (and (consp type) + (eq (car type) 'array)) + (let ((flen (caaddr type)) + (elt-type (cadr type)) + (field-index (join-symbols stobj-name '* fname 'i*)) + (copy-to-name (join-symbols stobj-name + 'copy-to- + stobj-name + '- + fname)) + (copy-from-name (join-symbols stobj-name + 'copy-from- + stobj-name + '- + fname))) + (generate-defstobj+-aux + stobj-name + (cdr field-defs) + (cons `(,field-predicate (nth ,field-index ,x)) + (cons `(equal (len (nth ,field-index ,x)) ,flen) + lsp)) + (cons `(,stobj-name (,copy-to-name ,flen (nth ,field-index ,copy) ,stobj-name)) + ct) + (cons `(,copy-from-name ,flen ,stobj-name) cf) + (append (generate-array-theorems stobj-name fname elt-type flen) + array-thms) + (1+ len))) + (let ((field-index (join-symbols stobj-name '* fname '*)) + (field-update (join-symbols stobj-name 'update- fname))) + (generate-defstobj+-aux + stobj-name + (cdr field-defs) + (cons `(,field-predicate (nth ,field-index ,x)) + lsp) + (cons `(,stobj-name (,field-update (nth ,field-index ,copy) ,stobj-name)) + ct) + (cons `(,fname ,stobj-name) cf) + array-thms + (1+ len))))))))) + +;(generate-defstobj+-aux 'tiny-state +; '((progc :type (unsigned-byte 10) :initially 0) +; (mem :type (array (signed-byte 32) (1024)) :initially 0) +; (dtos :type (unsigned-byte 10) :initially 0) +; (ctos :type (unsigned-byte 10) :initially 0) +; :inline t) +; nil +; nil +; nil +; nil +; 0) + +;makes the encapsulate, and seperates everything for generate-defstobj+-aux +(defun generate-defstobj+ (dlist) + (declare (xargs :mode :program)) + `(encapsulate + () + (local (in-theory (union-theories (theory 'ground-zero) + (theory 'defstobj+-theory)))) + (defstobj ,@dlist) + ,@(generate-defstobj+-aux (car dlist) (cdr dlist) nil nil nil nil 0))) + +;the final product: +(defmacro defstobj+ (name &rest args) + (generate-defstobj+ (cons name args))) + +;added October 18, 2004 by Daron Vroon: + +(defmacro with-copy-of-stobj (stobj mv-let-form) + (let ((copy-from-stobj (join-symbols stobj 'copy-from- stobj)) + (copy-to-stobj (join-symbols stobj 'copy-to- stobj))) + `(let ((stobj (,copy-from-stobj ,stobj))) + (with-local-stobj + ,stobj + (mv-let ,(nth 1 mv-let-form) + (let ((,stobj (,copy-to-stobj stobj ,stobj))) + ,(nth 2 mv-let-form)) + ,(nth 3 mv-let-form)))))) diff --git a/books/workshops/2004/matthews-vroon/support/tiny-fib-example/fib-def.lisp b/books/workshops/2004/matthews-vroon/support/tiny-fib-example/fib-def.lisp new file mode 100644 index 0000000..9232543 --- /dev/null +++ b/books/workshops/2004/matthews-vroon/support/tiny-fib-example/fib-def.lisp @@ -0,0 +1,163 @@ +(in-package "ACL2") +;; A proof that an implementation of the Fibonacci function +;; on Tiny, a small stack-machine, is correct. + +(include-book "tiny") +;(include-book "tiny-rewrites") +;(include-book "stream-fib") + +(set-verify-guards-eagerness 0) + +(defun tiny-loaded () t) + +;; Addresses of fib's temporary variables +(defconst *fib-adr* 20) +(defconst *fib-1-adr* (1+ *fib-adr*)) + +;; The start-of-program address +(defconst *prog-start-address* 100) + +;; Replaces label placeholders in a program fragment with +;; their final computed values. Label placeholders should +;; be negative integers, to prevent conflicts with opcodes +;; and address references in the program being patched. +(defun patch-prog-labels (prog label-map) + (cond ((endp prog) + prog) + ((assoc-equal (car prog) label-map) + (cons (cdr (assoc-equal (car prog) label-map)) + (patch-prog-labels (cdr prog) label-map))) + (t + (cons (car prog) + (patch-prog-labels (cdr prog) label-map))))) + +#| +NOTE: I am using Hoare triples to document the pre- and post-conditions + of basic blocks. To describe the contents of the stack I am overloading + the predicate symbol (<=) to compare stacks. Given stacks xs and ys, + xs <= ys holds when xs is a prefix of ys. I write the contents of + a stack using Haskell notation, so that [1,2,3] represents a three + element stack with 1 as the top element. I use the special constant + 'stack' to represent tiny's current value stack. + + I also define an operator on memory that takes a stack of addresses + and returns a stack of values consisting of the current contents of + memory at those addresses. So if the contents of memory at address + 1 is 3 and the contents of memory at address 5 is 12, then + mem[1,3] = [5,12]. +|# + +;; {[N] <= stack} +;; *init-block* +;; {[N-1] <= stack /\ mem[*fib-adr*,*fib-adr-1*] = [1,1]} +(defconst *init-block* + (assemble `(pushsi 1 + dup + dup + pop ,*fib-adr* + pop ,*fib-1-adr* + sub))) + + +;; {[N] <= stack /\ mem[*fib-adr*,*fib-adr-1*] = [M,K]} +;; *loop-block* +;; { (N=0 /\ [0] <= stack /\ mem[*fib-adr*] = M) +;; \/ ([N-1] <= stack /\ mem[*fib-adr*,*fib-adr-1*] = [M+K,M])} +(defconst *loop-label-hole* -2) +(defconst *done-label-hole* -3) +(defconst *unpatched-loop-block* + (assemble `(; loop-label-hole: + dup + jumpz ,*done-label-hole* + pushs ,*fib-adr* + dup + pushs ,*fib-1-adr* + add + pop ,*fib-adr* + pop ,*fib-1-adr* + pushsi 1 + sub + jump ,*loop-label-hole* + ; done-label-hole: + ))) + +; Calculate the actual program labels to patch +(defconst *loop-label* (+ *prog-start-address* + (len *init-block*))) +(defconst *done-label* (+ *loop-label* + (len *unpatched-loop-block*))) + +(defconst *label-patches* + `((,*loop-label-hole* . ,*loop-label*) + (,*done-label-hole* . ,*done-label*))) + +(defconst *loop-block* + (patch-prog-labels *unpatched-loop-block* *label-patches*)) + +;; {[0] <= stack /\ mem[*fib-adr*] = M) +;; *done-block* +;; {[M] <= stack} +(defconst *done-block* + (assemble `(pushs ,*fib-adr* + add + halt))) + +(defconst *prog-halt-address* (+ *done-label* + (1- (len *done-block*)))) + +;; The Fibonacci program +(defconst *fib-prog* + (append *init-block* + *loop-block* + *done-block*)) + + +;;; ;;========== Test harness for evaluating *fib-prog* on tiny ============= + +;; ;; Initialize the state of the tiny interpreter so +;; ;; that it will calculate the n'th Fibonacci number. +;; ;; The variable 'tiny-state' is a stobj defined in tiny.lisp. +;; (defun init-tiny-fib (tiny-state n) +;; (declare (xargs :stobjs (tiny-state))) +;; (load-tiny *prog-start-address* +;; `((,*prog-start-address* . ,*fib-prog*) ; Load program into memory +;; (901 . (,n))) ; Initialize TOS with n +;; tiny-state)) + +;; ;; Initialize the current tiny machine state +;; (defconst *fib-input* 4) +;; (init-tiny-fib tiny-state *fib-input*) + +;; ;;Execute exactly enough TINY steps to have the +;; ;; fib program halt. +;; (tiny tiny-state (+ (len *init-block*) +;; (* (1- *fib-input*) (len *loop-block*)) +;; (len *done-block*))) + +;; ; Examine the returned Fibonacci number +;; (dtos-val tiny-state 0) + +;; ; Check that the returned number matches +;; ; the Fibonacci specification. +;; (equal (dtos-val tiny-state 0) (fib-spec *fib-input*)) + +;; ; Check that the program has halted. +;; (equal (memi (progc tiny-state) tiny-state) (encode 'halt)) + +;; ;;Execute these commands in ACL2's repl-loop to probe +;; ;; the contents of the TINY machine state. +;; *prog-start-address* +;; (memi *prog-start-address* tiny-state) +;; (dtos-val tiny-state 0) ; data TOS +;; (progc tiny-state) ; program counter +;; (ctos tiny-state) ; return value TOS + +(defconst *fib-cutpoints* + `(,*prog-start-address* + ,*loop-label* + ,*done-label* + ,*prog-halt-address*)) + +;;The initial top-of-stack address. Note that the stack already +;; contains a single input value, namely the parameter to fib. +(defconst *init-dtos* 899) diff --git a/books/workshops/2004/matthews-vroon/support/tiny-fib-example/partial-clock-functions.lisp b/books/workshops/2004/matthews-vroon/support/tiny-fib-example/partial-clock-functions.lisp new file mode 100644 index 0000000..f41d994 --- /dev/null +++ b/books/workshops/2004/matthews-vroon/support/tiny-fib-example/partial-clock-functions.lisp @@ -0,0 +1,514 @@ +#|==================================================================|# + +#| +An application of the techniques of our paper to a program to calculate +the nth number in the fibonacci sequence written for the tiny machine. +|# + +;(in-package "partial-clock-functions") + +(in-package "ACL2") + +(include-book "tiny-rewrites") +(include-book "fib-def") +(include-book "misc/defpun" :dir :system) +(include-book "ordinals/ordinals" :dir :system) + +(defun at-cutpoint (tiny-state) + (declare (xargs :stobjs (tiny-state))) + (and (member (progc tiny-state) *fib-cutpoints*) + (program-loaded tiny-state *fib-prog* *prog-start-address*) + (tiny-statep tiny-state) + (equal (dtos tiny-state) *init-dtos*) + (cond ((equal (progc tiny-state) *prog-start-address*) + (< 0 (dtos-val tiny-state 0))) + ((equal (progc tiny-state) *loop-label*) + (<= 0 (dtos-val tiny-state 0))) + ((equal (progc tiny-state) *done-label*) + (= 0 (dtos-val tiny-state 0))) + (t t)))) + +(defthm cutpoint-implies-tiny-statep + (implies (at-cutpoint tiny-state) + (tiny-statep tiny-state)) + :hints (("Goal" :in-theory (enable at-cutpoint))) + :rule-classes :forward-chaining) + +#|====== Partial clock functions and symbolic simulation ======|# + +;A simulator that runs for N steps. +; N is a step-counter parameter. +(defun run (n tiny-state) + (declare (xargs :stobjs (tiny-state) + :guard (natp n))) + (if (zp n) + tiny-state + (let ((tiny-state (next tiny-state))) + (run (1- n) tiny-state)))) + +;A tail-recursive partial function that returns the +; number of steps until tiny-state reaches a cutpoint state, +; if in fact tiny-state can eventually reach a cutpoint state. +; The parameter N is an accumulator, which clients +; should initially set to zero. +(defpun steps-to-cutpoint-tail (n tiny-state) + (if (at-cutpoint tiny-state) + n + (steps-to-cutpoint-tail (1+ n) (run 1 tiny-state)))) + +(verify-guards omega) + +(defthm tiny-statep-create-tiny-state + (tiny-statep (create-tiny-state)) + :rule-classes :type-prescription) + +(in-theory (disable create-tiny-state)) + +(defun steps-to-cutpoint (tiny-state) + (declare (xargs :stobjs (tiny-state))) + (let ((steps (steps-to-cutpoint-tail 0 (copy-from-tiny-state tiny-state)))) + (if (and (natp steps) ;the number of steps is a natural number + (with-copy-of-stobj ;running a copy of tiny-state forward steps steps + tiny-state ;gives us a cutpoint. + (mv-let (result tiny-state) + (let ((tiny-state (run steps tiny-state))) + (mv (at-cutpoint tiny-state) tiny-state)) + result))) + steps + (omega)))) + +;Simulate tiny-state until it reaches a cutpoint state, +; assuming it does. +(defun-nx run-to-cutpoint (tiny-state) + (run (steps-to-cutpoint tiny-state) tiny-state)) + +(in-theory (disable at-cutpoint tiny-statep)) + +(defthm steps-to-cutpoint-tail-at-cutpoint + (implies (at-cutpoint tiny-state) + (equal (steps-to-cutpoint-tail n tiny-state) + n))) + +(defthm steps-to-cutpoint-tail-not-cutpoint + (implies (and (integerp n) + (not (at-cutpoint tiny-state))) + (equal (steps-to-cutpoint-tail n (run 1 tiny-state)) + (steps-to-cutpoint-tail (- n 1) tiny-state)))) + +(in-theory (disable steps-to-cutpoint-tail-def)) + +(defthm tiny-statep-run + (implies (tiny-statep tiny-state) + (tiny-statep (run n tiny-state))) + :rule-classes ((:rewrite) + (:forward-chaining :trigger-terms ((run n tiny-state))))) + +(defthm run-zero + (implies (zp n) + (equal (run n tiny-state) + tiny-state))) + +(defthm run-1 + (equal (next tiny-state) + (run 1 tiny-state))) + +(defthm run-plus + (equal (run m (run n tiny-state)) + (run (+ (nfix m) (nfix n)) tiny-state))) + +(in-theory (disable run)) + +(local + (defun-nx steps-to-cutpoint-induction (k tiny-state steps) + (declare (xargs :verify-guards nil + :guard (and (equal tiny-state tiny-state) + (equal steps steps)))) + (or (zp k) + (steps-to-cutpoint-induction (1- k) (next tiny-state) (1+ steps))))) + +(defthmd steps-to-cutpoint-tail-inv + (implies (and (at-cutpoint (run k tiny-state)) + (integerp steps)) + (let* ((result (steps-to-cutpoint-tail steps tiny-state)) + (cutpoint-steps (- result steps))) + (and (integerp result) + (natp cutpoint-steps) + (implies (natp k) + (<= cutpoint-steps k)) + (at-cutpoint (run cutpoint-steps tiny-state))))) + :hints (("Goal" :induct (steps-to-cutpoint-induction k tiny-state steps) + :do-not-induct t) + ("Subgoal *1/2" :cases ((at-cutpoint tiny-state))))) + +(defthm steps-to-cutpoint-tail-at-cutpoint-simp + (implies (at-cutpoint (run k tiny-state)) + (at-cutpoint (run (steps-to-cutpoint-tail 0 tiny-state) + tiny-state))) + :hints (("Goal" :use (:instance steps-to-cutpoint-tail-inv + (steps 0)))) + :rule-classes (:forward-chaining :rewrite)) + +(defthm steps-to-cutpoint-at-cutpoint + (implies (and (at-cutpoint (run k tiny-state)) + (tiny-statep tiny-state)) + (at-cutpoint (run (steps-to-cutpoint tiny-state) + tiny-state))) + :hints (("Goal" :use (:instance steps-to-cutpoint-tail-inv + (steps 0)))) + :rule-classes (:rewrite :forward-chaining)) + +(defthm steps-to-cutpoint-tail-diff + (implies (and (at-cutpoint (run k tiny-state)) + (syntaxp (not (equal n ''0))) + (integerp n) + (tiny-statep tiny-state)) + (equal (steps-to-cutpoint-tail n tiny-state) + (+ n (steps-to-cutpoint-tail 0 tiny-state)))) + :hints (("Goal" :use ((:instance steps-to-cutpoint-tail-inv + (k (- (steps-to-cutpoint-tail n tiny-state) + n)) + (steps 0)) + (:instance steps-to-cutpoint-tail-inv + (k (steps-to-cutpoint tiny-state)) + (steps n)) + (:instance steps-to-cutpoint-tail-inv + (steps 0)))))) + +(defthm not-at-cutpoint-implies-steps-to-cutpoint-tail-nonzero + (implies (and (at-cutpoint (run (steps-to-cutpoint-tail 0 tiny-state) + tiny-state)) + (not (at-cutpoint tiny-state))) + (posp (steps-to-cutpoint-tail 0 tiny-state))) + :rule-classes (:rewrite)) + +(defthm not-at-cutpoint-implies-steps-to-cutpoint-tail-nonzero-fwd-chain + (implies (and (at-cutpoint (run k tiny-state)) + (not (at-cutpoint tiny-state))) + (posp (steps-to-cutpoint-tail 0 tiny-state))) + :rule-classes (:forward-chaining)) + +(defthm natp-steps-to-cutpoint-tail + (implies (at-cutpoint (run (steps-to-cutpoint-tail 0 tiny-state) tiny-state)) + (natp (steps-to-cutpoint-tail 0 tiny-state))) + :hints (("Goal" :use (:instance steps-to-cutpoint-tail-inv))) + :rule-classes (:rewrite :forward-chaining)) + +(defthm natp-steps-to-cutpoint + (implies (tiny-statep tiny-state) + (equal (at-cutpoint (run (steps-to-cutpoint tiny-state) tiny-state)) + (natp (steps-to-cutpoint tiny-state)))) + :hints (("Goal" :use (:instance steps-to-cutpoint-tail-inv))) + :rule-classes (:rewrite)) + +(defthm steps-to-cutpoint-equals-omega-simp + (iff (equal (steps-to-cutpoint tiny-state) + (omega)) + (not (natp (steps-to-cutpoint tiny-state))))) + +(defthm o-p-steps-to-cutpoint + (o-p (steps-to-cutpoint tiny-state)) + :hints (("Goal" :cases ((natp (steps-to-cutpoint tiny-state)))))) + +(defthm steps-to-cutpoint-zero + (implies (and (at-cutpoint tiny-state) + (tiny-statep tiny-state)) + (equal (steps-to-cutpoint tiny-state) 0))) + +(defthm integerp-add + (equal (integerp (+ -1 n)) + (or (integerp n) + (not (acl2-numberp n))))) + +(defthmd steps-to-cutpoint-nonzero-intro + (implies (and (not (at-cutpoint tiny-state)) + (tiny-statep tiny-state)) + (equal (steps-to-cutpoint tiny-state) + (o+ 1 (steps-to-cutpoint (next tiny-state)))))) + +(defthm integerp-ord-decrement + (implies (natp n) + (equal (o- n 1) + (max 0 (- n 1)))) + :hints (("Goal" :in-theory (enable o-)))) + +(defthm natp-steps-to-cutpoint-increment + (equal (natp (o+ 1 (steps-to-cutpoint tiny-state))) + (natp (steps-to-cutpoint tiny-state))) + :hints (("Goal" :in-theory (enable o+)))) + +(defthm natp-steps-to-cutpoint-decrement + (equal (natp (o- (steps-to-cutpoint tiny-state) 1)) + (natp (steps-to-cutpoint tiny-state))) + :hints (("Goal" :in-theory (enable o-)))) + +(defthm omega-minus-one-equals-omega + (equal (o- (omega) 1) + (omega)) + :hints (("Goal" :in-theory (enable o-)))) + +(defthmd natp-ord-decrement + (equal (natp (o- n 1)) + (or (and (o-finp n) + (or (<= n 1) + (posp n))) + (< (o-first-expt n) 0))) + :hints (("Goal" :in-theory (enable o- o< o-finp)))) + +(defthm o-finp-steps-to-cutpoint-iff-natp + (equal (o-finp (steps-to-cutpoint tiny-state)) + (natp (steps-to-cutpoint tiny-state)))) + +(defthmd convert-at-cutpoint-to-steps-to-cutpoint + (implies (tiny-statep tiny-state) + (equal (at-cutpoint tiny-state) + (equal (steps-to-cutpoint tiny-state) + 0)))) + +(defthm at-cutpoint-implies-steps-to-cutpoint-zero + (implies (and (at-cutpoint tiny-state) + (tiny-statep tiny-state)) + (equal (steps-to-cutpoint tiny-state) + 0)) + :rule-classes :forward-chaining) + +(defthm not-at-cutpoint-implies-steps-to-cutpoint-nonzero + (implies (and (not (at-cutpoint tiny-state)) + (tiny-statep tiny-state)) + (not (equal (steps-to-cutpoint tiny-state) + 0))) + :rule-classes :forward-chaining) + +(defthmd steps-to-cutpoint-nonzero-elim + (implies (and (not (at-cutpoint tiny-state)) + (tiny-statep tiny-state)) + (equal (steps-to-cutpoint (next tiny-state)) + (o- (steps-to-cutpoint tiny-state) 1))) + :hints (("Goal" :in-theory (enable steps-to-cutpoint-nonzero-intro)))) + +(defthm natp-steps-to-cutpoint-run + (implies (and (natp (steps-to-cutpoint (run k tiny-state))) + (tiny-statep tiny-state)) + (natp (steps-to-cutpoint tiny-state)))) + +(in-theory (disable steps-to-cutpoint)) + +(defthm steps-to-cutpoint-run-1-elim + (implies (and (not (at-cutpoint tiny-state)) + (tiny-statep tiny-state)) + (equal (steps-to-cutpoint (run 1 tiny-state)) + (o- (steps-to-cutpoint tiny-state) 1))) + :hints (("Goal" :in-theory (e/d (steps-to-cutpoint-nonzero-elim run) + (run-1))))) + +;Simulate TINY-STATE until it reaches the next +; cutpoint state, if there is one. If there isn't, +; then return NIL. +; This function allows simpler rewrite rules +; than RUN-TO-CUTPOINT does. +(defun dummy-state (tiny-state) + (declare (xargs :stobjs (tiny-state))) + (let ((ts (with-local-stobj + tiny-state + (mv-let (result tiny-state) + (mv (copy-from-tiny-state tiny-state) tiny-state) + result)))) + (copy-to-tiny-state ts tiny-state))) + +(defthm dummy-state-create-tiny-state + (implies (tiny-statep tiny-state) + (equal (dummy-state tiny-state) + (create-tiny-state)))) + +(defthm not-at-cutpoint-create-tiny-state + (not (at-cutpoint (create-tiny-state))) + :hints (("goal" :in-theory (enable create-tiny-state)))) + +(defun next-cutpoint (tiny-state) + (declare (xargs :stobjs (tiny-state) + :measure (steps-to-cutpoint tiny-state) + :guard (and (tiny-statep tiny-state) + (natp (steps-to-cutpoint tiny-state))))) + (if (mbt (and (tiny-statep tiny-state) + (natp (steps-to-cutpoint tiny-state)))) + (if (at-cutpoint tiny-state) + tiny-state + (let ((tiny-state (next tiny-state))) + (next-cutpoint tiny-state))) + (dummy-state tiny-state))) + +(defthm tiny-statep-next-cutpoint + (implies (tiny-statep tiny-state) + (tiny-statep (next-cutpoint tiny-state))) + :rule-classes ((:type-prescription) (:rewrite))) + +(defthm next-cutpoint-at-cutpoint + (implies (at-cutpoint tiny-state) + (equal (next-cutpoint tiny-state) + tiny-state))) + +(defthmd next-cutpoint-elim-next + (implies (and (not (at-cutpoint tiny-state)) + (tiny-statep tiny-state)) + (equal (next-cutpoint (next tiny-state)) + (next-cutpoint tiny-state)))) + +(defthm next-cutpoint-intro-next + (implies (and (not (at-cutpoint tiny-state)) + (tiny-statep tiny-state)) + (equal (next-cutpoint tiny-state) + (next-cutpoint (next tiny-state))))) + +(defthm next-cutpoint-reaches-cutpoint + (implies (tiny-statep tiny-state) + (equal (at-cutpoint (next-cutpoint tiny-state)) + (natp (steps-to-cutpoint tiny-state))))) + +(in-theory (e/d (steps-to-cutpoint-nonzero-intro) (next-cutpoint run-1))) + +#|================== Program exit points and cutpoint-to-cutpoint =================|# + +(defun at-exitpoint (tiny-state) + (declare (xargs :stobjs (tiny-state))) + (and (equal (progc tiny-state) *prog-halt-address*) + (program-loaded tiny-state *fib-prog* *prog-start-address*) + (tiny-statep tiny-state) + (equal (dtos tiny-state) *init-dtos*))) + +(defthm at-exitpoint-implies-at-cutpoint + (implies (at-exitpoint tiny-state) + (at-cutpoint tiny-state)) + :hints (("Goal" :in-theory (enable at-exitpoint at-cutpoint)))) + +(defthm prove-steps-to-next-cutpoint-natp + (implies (and (at-cutpoint tiny-state) + (not (at-exitpoint tiny-state))) + (natp (steps-to-cutpoint (next tiny-state)))) + :hints (("Goal" :in-theory (enable at-cutpoint steps-to-cutpoint-nonzero-intro tiny-statep)))) + +(defun cutpoint-to-cutpoint (tiny-state) + (declare (xargs :stobjs (tiny-state) + :guard (and (at-cutpoint tiny-state) + (not (at-exitpoint tiny-state))) + :guard-hints (("goal" + :in-theory (disable steps-to-cutpoint-run-1-elim))))) + (let ((tiny-state (next tiny-state))) + (next-cutpoint tiny-state))) + +(defthm tiny-statep-cutpoint-to-cutpoint + (implies (tiny-statep tiny-state) + (tiny-statep (cutpoint-to-cutpoint tiny-state))) + :rule-classes ((:type-prescription) (:rewrite))) + +(defthm cutpoint-to-cutpoint-returns-cutpoint-state + (implies (and (natp (steps-to-cutpoint (next tiny-state))) + (tiny-statep tiny-state)) + (at-cutpoint (cutpoint-to-cutpoint tiny-state)))) + +;had to add this one. +(defthmd next-cutpoint-to-run + (let ((steps (steps-to-cutpoint tiny-state))) + (implies (and (natp steps) + (tiny-statep tiny-state)) + (equal (next-cutpoint tiny-state) + (run steps tiny-state)))) + :hints (("goal" :in-theory (e/d (next-cutpoint run) + (run-1 run-zero))))) + +(defthmd convert-cutpoint-to-cutpoint-to-run + (let ((steps (steps-to-cutpoint (next tiny-state)))) + (implies (and (natp steps) + (tiny-statep tiny-state)) + (equal (cutpoint-to-cutpoint tiny-state) + (run (1+ steps) tiny-state)))) + :hints (("Goal" + :in-theory (enable run-1) + :use ((:instance next-cutpoint-to-run (tiny-state + (next tiny-state))))))) + +(in-theory (disable cutpoint-to-cutpoint)) + +(defthm run-cutpoint-to-cutpoint + (let ((steps (steps-to-cutpoint (next tiny-state)))) + (implies (and (natp steps) + (tiny-statep tiny-state) + (natp k)) + (equal (run k (cutpoint-to-cutpoint tiny-state)) + (run (+ 1 k steps) tiny-state)))) + :hints (("Goal" :in-theory (enable convert-cutpoint-to-cutpoint-to-run)))) + +(defconst *max-prog-address* (1- (+ *prog-start-address* + (len *fib-prog*)))) + +;; This is an ordinal measure function that should +;; decrease from cutpoint to cutpoint, until an +;; exit point has been reached. In this example we +;; just use the value of the program counter. +(defun-nx cutpoint-measure (tiny-state) + (if (at-exitpoint tiny-state) + 0 + (o+ (o* (omega) (nfix (dtos-val tiny-state 0))) + (nfix (- *max-prog-address* (progc tiny-state)))))) + +(defthm prove-cutpoint-measure-is-ordinal + (o-p (cutpoint-measure tiny-state))) + +(local + (defthm l1 + (implies (and (natp a) + (natp b) + (natp c) + (natp d) + (< a b)) + (o< (o+ (o* (omega) a) c) + (o+ (o* (omega) b) d))) + :hints (("goal" :cases ((equal a 0)))))) + +(defthm prove-cutpoint-measure-decreases + (implies (and (at-cutpoint tiny-state) + (not (at-exitpoint tiny-state))) + (o< (cutpoint-measure (cutpoint-to-cutpoint tiny-state)) + (cutpoint-measure tiny-state))) + :hints (("Goal" + :do-not-induct t + :in-theory (enable cutpoint-to-cutpoint next + at-cutpoint at-exitpoint tiny-statep)))) + +(in-theory (disable cutpoint-measure cutpoint-to-cutpoint)) + + +#|================= The termination proof ===============|# + +#|====== Application: An efficient simulator ======|# +#|====== FAST-CUTPOINT-TO-CUTPOINT with non-executable ======|# +#|====== guards in the function's body ======|# + +(in-theory (disable at-exitpoint)) + +;here's the defexec version. but the mbt version below is equivalent, +;still guaranteed to terminate, and more succinct. +;(defexec fast-cutpoint-to-cutpoint (tiny-state) +; (declare (xargs :stobjs (tiny-state) +; :measure (cutpoint-measure tiny-state) +; :guard (at-cutpoint tiny-state)) +; (exec-xargs :default-value (dummy-state tiny-state))) +; (mbe :logic (cond ((not (at-cutpoint tiny-state)) (dummy-state tiny-state)) +; ((at-exitpoint tiny-state) tiny-state) +; (t (let ((tiny-state (cutpoint-to-cutpoint tiny-state))) +; (fast-cutpoint-to-cutpoint tiny-state)))) +; :exec (if (at-exitpoint tiny-state) +; tiny-state +; (let ((tiny-state (cutpoint-to-cutpoint tiny-state))) +; (fast-cutpoint-to-cutpoint tiny-state))))) + +(defun fast-cutpoint-to-cutpoint (tiny-state) + (declare (xargs :stobjs (tiny-state) + :measure (cutpoint-measure tiny-state) + :guard (at-cutpoint tiny-state))) + (if (mbt (at-cutpoint tiny-state)) + (if (at-exitpoint tiny-state) + tiny-state + (let ((tiny-state (cutpoint-to-cutpoint tiny-state))) + (fast-cutpoint-to-cutpoint tiny-state))) + (dummy-state tiny-state))) + +#|==================================================================|#
\ No newline at end of file diff --git a/books/workshops/2004/matthews-vroon/support/tiny-fib-example/tiny-rewrites.lisp b/books/workshops/2004/matthews-vroon/support/tiny-fib-example/tiny-rewrites.lisp new file mode 100644 index 0000000..415cb10 --- /dev/null +++ b/books/workshops/2004/matthews-vroon/support/tiny-fib-example/tiny-rewrites.lisp @@ -0,0 +1,367 @@ +(in-package "ACL2") + +(include-book "tiny") +(local (include-book "arithmetic/top-with-meta" :dir :system)) + +; Helper function to lookup values from the top +; of the TINY data stack. +(defun dtos-val (tiny-state n) + (declare (xargs :stobjs (tiny-state) + :guard (and (natp n) + (< (+ (dtos tiny-state) n 1) + (mem-length tiny-state)) + (acl2-numberp (dtos tiny-state))))) + (memi (+ (dtos tiny-state) n 1) tiny-state)) + +;Return the instruction pointed to by tiny's program counter +(defun instr-val (tiny-state) + (declare (xargs :stobjs (tiny-state))) + (memi (progc tiny-state) tiny-state)) + + +#|==== Rewrite rules for symbolically simulating tiny ====|# + +;REVISIT: The RHS of each rewrite rule was taken directly +; from the definition of 'next'. However, the RHS +; could probably be simplified, if we added to the hypotheses +; of each rewrite the condition (tiny-statep tiny-state). +; Try the command +; :pr +; to see the rewrite rule generated from each theorem. + +(defthm next-instr-pop + (let* ((progc (progc tiny-state)) + (ins (memi progc tiny-state))) + (implies (equal ins 0) + (equal (next tiny-state) + (let ((tiny-state (update-progc (+|10| progc 2) tiny-state))) + (popus (fix|10| (memi (+|10| progc 1) + tiny-state)) + tiny-state))))) + :hints (("Goal" :expand (next tiny-state)))) + +(defthm next-instr-pushs + (let* ((progc (progc tiny-state)) + (ins (memi progc tiny-state))) + (implies (equal ins 1) + (equal (next tiny-state) + (let ((tiny-state (update-progc (+|10| progc 2) tiny-state))) + (pushus (memi (fix|10| (memi (+|10| progc 1) tiny-state)) tiny-state) tiny-state))))) + :hints (("Goal" :expand (next tiny-state)))) + +(defthm next-instr-pushsi + (let* ((progc (progc tiny-state)) + (ins (memi progc tiny-state))) + (implies (equal ins 2) + (equal (next tiny-state) + (let ((tiny-state (update-progc (+|10| progc 2) tiny-state))) + (pushus (memi (+|10| progc 1) tiny-state) tiny-state))))) + :hints (("Goal" :expand (next tiny-state)))) + +(defthm next-instr-add + (let* ((progc (progc tiny-state)) + (dtos (dtos tiny-state)) + (ins (memi progc tiny-state))) + (implies (equal ins 3) + (equal (next tiny-state) + (let ((tiny-state (update-progc (+|10| progc 1) tiny-state))) + (let ((tiny-state (update-dtos (+|10| dtos 2) tiny-state))) + (pushus (add<32> (Int32 (memi (+|10| dtos 1) tiny-state)) + (Int32 (memi (+|10| dtos 2) tiny-state))) + tiny-state)))))) + :hints (("Goal" :expand (next tiny-state)))) + +(defthm next-instr-jump + (let* ((progc (progc tiny-state)) + (ins (memi progc tiny-state))) + (implies (equal ins 4) + (equal (next tiny-state) + (update-progc (fix|10| (memi (+|10| progc 1) tiny-state)) tiny-state)))) + :hints (("Goal" :expand (next tiny-state)))) + +(defthm next-instr-jumpz + (let* ((progc (progc tiny-state)) + (dtos (dtos tiny-state)) + (ins (memi progc tiny-state))) + (implies (equal ins 5) + (equal (next tiny-state) + (let ((nprogc (if (= (memi (+|10| dtos 1) tiny-state) 0) + (fix|10| (memi (+|10| progc 1) tiny-state)) + (+|10| progc 2)))) + (declare (type (unsigned-byte 10) nprogc)) + (let ((tiny-state (update-progc nprogc tiny-state))) + (update-dtos (+|10| dtos 1) tiny-state)))))) + :hints (("Goal" :expand (next tiny-state)))) + +(defthm next-instr-call + (let* ((progc (progc tiny-state)) + (ins (memi progc tiny-state))) + (implies (equal ins 6) + (equal (next tiny-state) + (let ((nadd (fix|10| (memi (+|10| progc 1) tiny-state)))) + (declare (type (unsigned-byte 10) nadd)) + (let ((tiny-state (update-progc nadd tiny-state))) + (pushcs (+|10| progc 2) tiny-state)))))) + :hints (("Goal" :expand (next tiny-state)))) + +(defthm next-instr-return + (let* ((progc (progc tiny-state)) + (ctos (ctos tiny-state)) + (ins (memi progc tiny-state))) + (implies (equal ins 7) + (equal (next tiny-state) + (let ((nadd (fix|10| (memi (+|10| ctos 1) tiny-state)))) + (declare (type (unsigned-byte 10) nadd)) + (let ((tiny-state (update-progc nadd tiny-state))) + (update-ctos (+|10| ctos 1) tiny-state)))))) + :hints (("Goal" :expand (next tiny-state)))) + +(defthm next-instr-sub + (let* ((progc (progc tiny-state)) + (dtos (dtos tiny-state)) + (ins (memi progc tiny-state))) + (implies (equal ins 8) + (equal (next tiny-state) + (let ((tiny-state (update-progc (+|10| progc 1) tiny-state))) + (let ((tiny-state (update-dtos (+|10| dtos 2) tiny-state))) + (pushus (max<32> 0 (sub<32> (memi (+|10| dtos 2) tiny-state) + (memi (+|10| dtos 1) tiny-state))) + tiny-state)))))) + :hints (("Goal" :expand (next tiny-state)))) + +(defthm next-instr-dup + (let* ((progc (progc tiny-state)) + (dtos (dtos tiny-state)) + (ins (memi progc tiny-state))) + (implies (equal ins 9) + (equal (next tiny-state) + (let ((tiny-state (update-progc (+|10| progc 1) tiny-state))) + (pushus (memi (+|10| dtos 1) tiny-state) tiny-state))))) + :hints (("Goal" :expand (next tiny-state)))) + +(defthm next-instr-halt + (let* ((progc (progc tiny-state)) + (ins (memi progc tiny-state))) + (implies (or (not (natp ins)) + (<= 10 ins)) + (equal (next tiny-state) + tiny-state))) + :hints (("Goal" :expand (next tiny-state)))) + + +#|==== Rules for infering when a program is loaded ====|# + +(defun memory-block-loadedp (address list array) + (declare (xargs :measure (acl2-count list))) + (or (endp list) + (and (equal (nth address array) + (first list)) + (memory-block-loadedp (1+ address) (rest list) array)))) + +;;Refine the type-set ACL2 infers for the len function +(defthm typset-len-zero + (implies (equal (len xs) 0) + (equal (consp xs) nil)) + :rule-classes ((:type-prescription))) + +(defthm posp-n-consp-repeat + (implies (posp n) + (consp (repeat n x))) + :rule-classes :type-prescription) + +(defthm car-repeat-posp + (implies (posp n) + (equal (car (repeat n x)) x))) + +;REVISIT: Is there an existing ACL2 idiom for specifying +; induction on the naturals? +(defun nat-induction (n) + (and (posp n) + (nat-induction (1- n)))) + +;;This function is defined only to cause ACL2 to generate +;; an induction scheme needed to prove the nth-repeat theorem +;; below. +(defun nat-nat-induction (k n) + (and (natp k) + (natp n) + (< 0 k) + (< 0 n) + (nat-nat-induction (1- k) (1- n)))) + +(defthm nth-repeat + (implies (and (natp k) + (natp n) + (< k n)) + (equal (nth k (repeat n x)) + x)) + :hints (("Goal" :in-theory (enable nth repeat) + :induct (nat-nat-induction k n)))) + +(defthm memory-block-unmodified + (implies (and (natp addr) + (natp start-addr) + (< addr (len memory)) + (<= (+ start-addr (len prog)) (len memory)) + (or (< addr start-addr) + (<= (+ start-addr (len prog)) addr))) + (iff (memory-block-loadedp start-addr + prog + (update-nth addr val memory)) + (memory-block-loadedp start-addr prog memory)))) + +;;Most memory accesses do not change the program code +(defthm code-not-self-modifying + (iff (program-loaded (update-nth *memi* memory tiny-state) + prog + start-addr) + (memory-block-loadedp start-addr prog memory)) + :hints (("goal" :in-theory (enable program-loaded)))) + +#|===== General lemmas needed during the proof of fib-partial-correctness ====|# + +;The following theorems implement an "improved" version of +; memp-update-nth that can be applied +; in more cases than memp-update-nth can. + +;;Used to generate a specialized induction scheme where an +;; index value is decreasing at the same rate as the length of a list. +(defun list-nat-induction (xs n) + (and (consp xs) + (posp n) + (list-nat-induction (cdr xs) (1- n)))) + +(defthm memp-is-truelist + (implies (memp m) + (true-listp m)) + :rule-classes :compound-recognizer) + +(defthm update-nth-zero + (implies (zp a) + (equal (update-nth a v xs) + (cons v (cdr xs)))) + :hints (("Goal" :expand (update-nth a v xs)))) + + +(defthm update-nth-truelistp + (implies (and (natp a) + (< a (len m))) + (iff (true-listp (update-nth a v m)) + (true-listp m))) + :hints (("Goal" :in-theory (enable (update-nth)) + :induct (list-nat-induction m a) + :do-not-induct t) + ("Subgoal *1/1.2" :expand (update-nth a v m)))) + +(defthm update-nth-truelistp-type + (implies (and (natp a) + (< a (len m)) + (true-listp m)) + (true-listp (update-nth a v m))) + :rule-classes :type-prescription) + +(defthm update-nth-not-truelistp-type + (implies (and (natp a) + (< a (len m)) + (not (true-listp m))) + (not (true-listp (update-nth a v m)))) + :rule-classes :type-prescription) + +(defthm nth-update-addr-integerp + (implies (and (memp (update-nth a v m)) + (natp a) + (< a (len m))) + (equal (integerp v) t)) + :hints (("Goal" :expand (update-nth a v m) + :induct (list-nat-induction m a) + :do-not-induct t))) + +(defthm memp-update-nth-2 + (let ((old-v (nth a m))) + (implies (and (natp a) + (< a (len m)) + (integerp old-v) + (<= -2147483648 old-v) + (<= old-v 2147483647)) + (iff (memp (update-nth a v m)) + (and (integerp v) + (<= -2147483648 v) + (<= v 2147483647) + (memp m))))) + :hints (("Goal" :in-theory (enable update-nth nth) + :induct (list-nat-induction m a) + :do-not-induct t))) + +(in-theory (disable update-nth-zero)) + +(defthm memp-nth-integerp + (implies (and (memp m) + (integerp a) + (<= 0 a) + (< a (len m))) + (integerp (nth a m))) + :rule-classes :type-prescription) + +(defthm signed-byte-p-32-bounds + (implies (signed-byte-p 32 n) + (and (<= -2147483648 n) + (<= n 2147483647)))) + +(defthm tiny-posp-next + (equal (tiny (next tiny-state) n) + (next (tiny tiny-state n))) + :hints (("Goal" :in-theory (enable tiny)))) + +(defthm memi-elements-leq + (implies (and (memp (nth *memi* tiny-state)) + (integerp n) + (<= 0 n) + (< n (len (nth *memi* tiny-state)))) + (<= (nth n (nth *memi* tiny-state)) 2147483647)) + :rule-classes :linear) + + +#|==== Rules for stepping tiny an arbitrary number of times ====|# + +;;The definition of TINY in tiny.lisp assumes that tiny will not +;; be stepped more than 2^32 times. For proving termination properties +;; of tiny we need to define a function that can step tiny any number +;; of times. + +;daron: i'm not sure why this wasn't made executable, so i changed the definition +;(defun run (tiny-state n) +; (declare (xargs :non-executable t)) +; (if (zp n) +; tiny-state +; (run (next tiny-state) (1- n)))) + +;(defun run (tiny-state n) +; (declare (xargs :stobjs (tiny-state) +; :guard (natp n))) +; (if (zp n) +; tiny-state +; (let ((tiny-state (next tiny-state))) +; (run tiny-state (1- n))))) + +;(defthm run-tiny-statep +; (implies (tiny-statep tiny-state) +; (tiny-statep (run tiny-state n))) +; :hints (("Goal" :in-theory (disable tiny-statep next)))) + +;(defthmd run-posp-next +; (implies (posp n) +; (equal (run tiny-state n) +; (next (run tiny-state (1- n)))))) + +;(defthm run-next +; (implies (natp n) +; (equal (run (next tiny-state) n) +; (next (run tiny-state n)))) +; :hints (("Goal" :induct (nat-induction n) +; :in-theory (enable run-posp-next)))) + +;(defthm run-run +; (implies (and (natp k) +; (natp n)) +; (equal (run (run tiny-state k) n) +; (run tiny-state (+ k n))))) diff --git a/books/workshops/2004/matthews-vroon/support/tiny-fib-example/tiny.lisp b/books/workshops/2004/matthews-vroon/support/tiny-fib-example/tiny.lisp new file mode 100644 index 0000000..13c4c5f --- /dev/null +++ b/books/workshops/2004/matthews-vroon/support/tiny-fib-example/tiny.lisp @@ -0,0 +1,1018 @@ +#| + +This file contains an interpreter for the "tiny" machine, an +experimental machine loosely based on Boyer's and Moore's small +machine, as described in "High-Speed Analyzable Simulators", Chapter 8 +of the book "Computer-Aided Reasoning: ACL2 Case Studies". We also +include a small benchmark program that calculates the remainder of two +integers. This file is the latest in a series of experiments to build +a toy interpreter that can be analyzed and run fast using many +different methods of constructing fast interpreters. + +Several of the changes made in Fall 1999 to reflect improvements in +ACL2, or highlight something in the chapter. In particular, we + + - Added symbolic field names. + + - Updated the model to use STOBJ. (STOBJ names were also +subsequently changed to comply with the name changes in the draft and +released versions of ACL2 2.4.) + + - Changed the definition of 32-bit add in order to avoid compiler +replacements altogether, as described in the chapter. + +Dave Greve and Matt Wilding + +September 1999 +(updated January 2000) + +Updates by David Hardin on 2004-04-01 (ha ha) + + - Re-enabled nu-rewriter; it's stable now. + + - Got rid of most of the linear arithmetic "hacks"; ACL2's + linear arithmetic processing is now much improved. + + - Deleted other unused rules, redundant hypotheses, etc. Not a + complete job by any means, but tiny now has 10% fewer lines, which + seemed a decent enough "spring cleaning". + + - Eliminated macros that provided symbolic names for fields; + defstobj now generates these automatically (e.g., *baz* for field baz). + + - Corrected comment on how to run the example outside of the ACL2 + read-eval-print loop (a stobj named foo is now accessed as *the-live-foo*). + + - Used the new (as of ACL2 2.8) include-book :dir :system keywords + to make the file more portable. +|# + +(in-package "ACL2") +(include-book "defstobj+") +(local (include-book "arithmetic/top-with-meta" :dir :system)) +(include-book "data-structures/list-defthms" :dir :system) +;(include-book "meta/meta" :dir :system) +(include-book "ihs/logops-lemmas" :dir :system) + +(disable-theory (theory 'logops-functions)) + +(set-verify-guards-eagerness 2) + +(defstobj+ tiny-state + (progc :type (unsigned-byte 10) :initially 0) + (mem :type (array (signed-byte 32) (1024)) :initially 0) + (dtos :type (unsigned-byte 10) :initially 0) + (ctos :type (unsigned-byte 10) :initially 0) + :inline t) + +;; Some proof speedup lemmas +;; Changed after Version 6.1 by Matt Kaufmann to replace obsolete the-error by +;; the-check. +(defthm the-check-noop + (equal (the-check g x y) y)) + +(defthm nth-update-nth-const + (implies + (and + (syntaxp (quotep n1)) + (syntaxp (quotep n2))) + (equal (nth n1 (update-nth n2 v l)) + (if (equal (nfix n1) (nfix n2)) v (nth n1 l)))) + :rule-classes ((:rewrite :loop-stopper nil))) + +(in-theory (disable the-check nth update-nth)) + +;; Some macros for convenient expression of declarations +(defmacro Int32 (x) `(the (signed-byte 32) ,x)) +(defmacro Nat10 (x) `(the (unsigned-byte 10) ,x)) +(defmacro MAX_INT<32> () 2147483647) +(defmacro MIN_INT<32> () -2147483648) +(defmacro MIN_INT<32>+1 () -2147483647) +(defmacro MAX_NAT<10> () 1023) +(defmacro MAX_NAT-1<10> () 1022) + +(defmacro fix|10| (x) + `(Nat10 (logand (MAX_NAT<10>) ,x))) + +(defmacro max<32> (x y) + `(Int32 (max ,x ,y))) + +(defmacro +<32> (x y) + `(Int32 (+ ,x ,y))) + +;; We introduce a speedy add function for 32-bit quantities, then a +;; not-so-speedy 32-bit add function that uses IHS library function +;; about which much has been previously proved. We show their +;; equivalence to make use of the proofs in the IHS library. + +;; The plus<32> guard proof requires 3 minutes on an Ultra 10, a long +;; time for a little theorem. + +(defun plus<32> (a b) + (declare (type (signed-byte 32) a) + (type (signed-byte 32) b) + ;; Added by Matt K. for v2-7: + (xargs :guard-hints (("Goal" :in-theory (enable signed-byte-p))))) + (Int32 + (if (< a 0) + (if (>= b 0) (+<32> a b) + (let ((psum (+<32> (+<32> (+<32> a (MAX_INT<32>)) 1) b))) + (declare (type (signed-byte 32) psum)) + (if (< psum 0) + (+<32> (+<32> (MAX_INT<32>) psum) 1) + (+<32> psum (MIN_INT<32>))))) + (if (< b 0) (+<32> a b) + (let ((psum (+<32> (+<32> a (MIN_INT<32>)) b))) + (declare (type (signed-byte 32) psum)) + (if (>= psum 0) + (+<32> (MIN_INT<32>) psum) + (+<32> (+<32> psum (MAX_INT<32>)) 1))))))) + +(defun +bv32 (x y) + (declare (type (signed-byte 32) x y)) + (logext 32 (+ x y))) + +(defthm plus<32>-works + (implies + (and + (signed-byte-p 32 a) + (signed-byte-p 32 b)) + (equal + (plus<32> a b) + (+bv32 a b))) + :hints (("goal" :use ((:instance logext-+-logext (size 32) (i (+ a b)) (j (- (expt 2 32)))) + (:instance logext-+-logext (size 32) (i (+ a b)) (j (expt 2 32)))) + :in-theory (set-difference-theories (enable signed-byte-p) '(logext-+-logext))))) + +(defthm integerp-means-rationalp + (implies (integerp x) (rationalp x)) + :rule-classes nil) + +(defthm integerp-plus + (implies + (and (integerp a) (integerp b)) + (integerp (+ a b))) + :rule-classes nil) + +;; Handy facts about 32-bit addition +(defthm +bv32-representable-as-32-bits + (and + (integerp (+bv32 a b)) + (< (+bv32 a b) 2147483648) ; modified by Matt K. for v2-7 + (>= (+bv32 a b) -2147483648)) + :hints (("goal" + :in-theory (set-difference-theories (enable signed-byte-p) '(signed-byte-p-logext)) + :use + ((:instance integerp-means-rationalp + (x (+bv32 a b))) + (:instance signed-byte-p-logext (size 32) (size1 32) (i (+ a b))) + (:instance integerp-plus + (a (LOGAND A 4294967295)) + (b (LOGAND B 4294967295))))))) + +(in-theory (disable plus<32> +bv32)) +(in-theory (enable signed-byte-p)) + +;; Macros for convenient arithmetic +(defmacro +|10| (x y) + `(Nat10 (logand (+<32> ,x ,y) (MAX_NAT<10>)))) + +(defmacro add<32> (x y) + `(Int32 (plus<32> ,x ,y))) + +(defmacro negate_32 (x) + `(let ((x ,x)) + (declare (type (signed-byte 32) x)) + (Int32 (if (= x (MIN_INT<32>)) (MIN_INT<32>) (Int32 (- x)))))) + +(defun sub<32> (x y) + (declare (type (signed-byte 32) x) + (type (signed-byte 32) y)) + (add<32> x (negate_32 y))) + + +(defthm integerp-- + (implies + (integerp x) + (integerp (- x)))) + +; Modified for Version 2.6 and further for v2-7 by Matt Kaufmann: +(defthm update-nth-memp + (implies + (and + (memp mem) + (< n (len mem)) + (integerp n) + (>= n 0)) + (equal (memp (update-nth n val mem)) + (and + (<= (- (expt 2 31)) val) + (< val (expt 2 31)) ; modified by Matt K. for v2-7 + (integerp val)))) + :hints (("goal" :in-theory (enable update-nth)))) + +; Modified by Matt Kaufmann for ACL2 Version 2.6. +(defthm arb-memory-proof + (implies + (and + (memp mem) + (< n2 (len mem)) + (<= 0 n2)) + (and + (<= (nth n2 mem) (MAX_INT<32>)) + (<= (MIN_INT<32>) (nth n2 mem)) + (integerp (nth n2 mem)))) + :hints (("goal" :in-theory (enable nth))) + :rule-classes nil) + +;; an element of memory is a 32-bit quantity. Really. +; Modified by Matt Kaufmann for ACL2 Version 2.6. +(defthm arb-memory + (implies + (and + (memp mem) + (< n2 (len mem)) + (<= 0 n2)) + (and + (<= (nth n2 mem) (MAX_INT<32>)) + (< (nth n2 mem) 2147483648) + (not (< 2147483648 (NTH n2 mem))) ; needed later on. + (<= (MIN_INT<32>) (nth n2 mem)) + (implies (not (equal (min_int<32>) (nth n2 mem))) + (< (MIN_INT<32>) (nth n2 mem))) + (integerp (nth n2 mem)) + (rationalp (nth n2 mem)) + (acl2-numberp (nth n2 mem)))) + :hints (("goal" :use arb-memory-proof))) + +; Always move the negation to the constant +(defthm less-neg-const + (implies + (syntaxp (quotep y)) + (and + (iff (< (- x) y) (> x (- y))) + (iff (< y (- x)) (> (- y) x)) + (iff (<= (- x) y) (>= x (- y))) + (iff (<= y (- x)) (>= (- y) x)))) + :rule-classes ((:rewrite :loop-stopper nil))) + +; Added by Matt K. for v2-7 to help with some guard proofs. +(in-theory (enable unsigned-byte-p)) + +;; Push a value onto the user stack. +(defun pushus (val tiny-state) + (declare (type (signed-byte 32) val) + (xargs :stobjs (tiny-state) + :guard (tiny-statep tiny-state))) + (let ((dtos (dtos tiny-state))) + (declare (type (unsigned-byte 10) dtos)) + (let ((tiny-state (update-memi dtos (Int32 val) tiny-state))) + (update-dtos (+|10| dtos -1) tiny-state)))) + +;; Pop a value off the user stack. +(defun popus (address tiny-state) + (declare (type (unsigned-byte 10) address) + (xargs :stobjs (tiny-state) + :guard (tiny-statep tiny-state))) + (let ((ndtos (+|10| (dtos tiny-state) 1))) + (declare (type (unsigned-byte 10) ndtos)) + (let ((tiny-state (update-memi address (memi ndtos tiny-state) tiny-state))) + (update-dtos ndtos tiny-state)))) + +;; Push a value on the call stack. +(defun pushcs (val tiny-state) + (declare (type (signed-byte 32) val) + (xargs :stobjs (tiny-state) + :guard (tiny-statep tiny-state))) + (let ((ctos (ctos tiny-state))) + (declare (type (unsigned-byte 10) ctos)) + (let ((tiny-state (update-memi ctos (Int32 val) tiny-state))) + (update-ctos (+|10| ctos -1) tiny-state)))) + +;; Pop a value off the call stack +(defun popcs (address tiny-state) + (declare (type (unsigned-byte 10) address) + (xargs :stobjs (tiny-state) + :guard (tiny-statep tiny-state))) + (let ((nctos (+|10| (ctos tiny-state) 1))) + (declare (type (unsigned-byte 10) nctos)) + (let ((tiny-state (update-memi address (memi nctos tiny-state) tiny-state))) + (update-dtos nctos tiny-state)))) + +;; Define the TINY instructions by defining the effect of executing +;; the current instruction. +(defun next (tiny-state) + (declare (xargs :stobjs (tiny-state) + :guard (tiny-statep tiny-state) + :guard-hints (("goal" :in-theory + (disable hard-error pushus popus pushcs))))) + (let ((progc (progc tiny-state)) + (dtos (dtos tiny-state)) + (ctos (ctos tiny-state))) + (declare (type (unsigned-byte 10) progc dtos ctos)) + + (let ((ins (memi progc tiny-state))) + (declare (type (signed-byte 32) ins)) + + (case ins + ; pop + (0 (let ((tiny-state (update-progc (+|10| progc 2) tiny-state))) + (popus (fix|10| (memi (+|10| progc 1) tiny-state)) tiny-state))) + + ; pushs + (1 (let ((tiny-state (update-progc (+|10| progc 2) tiny-state))) + (pushus (memi (fix|10| (memi (+|10| progc 1) tiny-state)) tiny-state) tiny-state))) + + ; pushsi + (2 (let ((tiny-state (update-progc (+|10| progc 2) tiny-state))) + (pushus (memi (+|10| progc 1) tiny-state) tiny-state))) + + ; add + (3 (let ((tiny-state (update-progc (+|10| progc 1) tiny-state))) + (let ((tiny-state (update-dtos (+|10| dtos 2) tiny-state))) + (pushus (add<32> (Int32 (memi (+|10| dtos 1) tiny-state)) + (Int32 (memi (+|10| dtos 2) tiny-state))) + tiny-state)))) + + ; jump + (4 (update-progc (fix|10| (memi (+|10| progc 1) tiny-state)) tiny-state)) + + ; jumpz + (5 (let ((nprogc (if (= (memi (+|10| dtos 1) tiny-state) 0) + (fix|10| (memi (+|10| progc 1) tiny-state)) + (+|10| progc 2)))) + (declare (type (unsigned-byte 10) nprogc)) + (let ((tiny-state (update-progc nprogc tiny-state))) + (update-dtos (+|10| dtos 1) tiny-state)))) + + ; call + (6 (let ((nadd (fix|10| (memi (+|10| progc 1) tiny-state)))) + (declare (type (unsigned-byte 10) nadd)) + (let ((tiny-state (update-progc nadd tiny-state))) + (pushcs (+|10| progc 2) tiny-state)))) + + ; return + (7 (let ((nadd (fix|10| (memi (+|10| ctos 1) tiny-state)))) + (declare (type (unsigned-byte 10) nadd)) + (let ((tiny-state (update-progc nadd tiny-state))) + (update-ctos (+|10| ctos 1) tiny-state)))) + + ; sub + (8 (let ((tiny-state (update-progc (+|10| progc 1) tiny-state))) + (let ((tiny-state (update-dtos (+|10| dtos 2) tiny-state))) + (pushus (max<32> 0 (sub<32> (memi (+|10| dtos 2) tiny-state) + (memi (+|10| dtos 1) tiny-state))) + tiny-state)))) + + ; dup + (9 (let ((tiny-state (update-progc (+|10| progc 1) tiny-state))) + (pushus (memi (+|10| dtos 1) tiny-state) tiny-state))) + + ; halt + (otherwise tiny-state))))) + +(defthm tiny-statep-next + (implies + (tiny-statep tiny-state) + (tiny-statep (next tiny-state)))) + +(defun tiny (tiny-state n) + (declare (xargs :stobjs (tiny-state) + :guard (tiny-statep tiny-state) + :guard-hints (("goal" :in-theory (disable next tiny-statep)))) + (type (signed-byte 32) n)) + (if (or (not (integerp (Int32 n))) (<= (Int32 n) (Int32 0))) ; ifix inefficient + tiny-state + (let ((tiny-state (next tiny-state))) + (tiny tiny-state (Int32 (1- (Int32 n))))))) + + +;;;;; +;; Functions for creating Tiny state + +;; Note: recursive functions involving s.t. objects must have a base +;; case listed first. Presumably ACL2 has this restriction in order +;; to allow ACL2 a simpler approach for determining whether a function +;; returns all the s.t. objects it needs to return, since every base +;; case must return every potentially-modified s.t. object. + +(defun load-memory-block (address list tiny-state) + (declare (xargs :stobjs (tiny-state) + :guard (tiny-statep tiny-state) + :verify-guards nil)) + (if (not (consp list)) tiny-state + (let ((tiny-state (update-memi address (car list) tiny-state))) + (load-memory-block (+|10| address 1) (cdr list) tiny-state)))) + +(defun load-memory (assoc tiny-state) + (declare (xargs :stobjs (tiny-state) + :verify-guards nil)) + (if (not (consp assoc)) tiny-state + (let ((tiny-state (load-memory-block (caar assoc) (cdar assoc) tiny-state))) + (load-memory (cdr assoc) tiny-state)))) + +(defun load-tiny (pc memlist tiny-state) + (declare (xargs :stobjs (tiny-state) + :verify-guards nil)) + (let ((tiny-state (update-progc pc tiny-state))) + (let ((tiny-state (update-dtos 900 tiny-state))) + (let ((tiny-state (update-ctos 1000 tiny-state))) + (load-memory memlist tiny-state))))) + +(defun encode (op) + (declare (xargs :verify-guards nil)) + (case op + ('pop 0) + ('pushs 1) + ('pushsi 2) + ('add 3) + ('jump 4) + ('jumpz 5) + ('call 6) + ('ret 7) + ('sub 8) + ('dup 9) + ('halt 10))) + +(defun assemble (code) + (declare (xargs :verify-guards nil)) + (if (consp code) + (cons + (if (integerp (car code)) (car code) (encode (car code))) + (assemble (cdr code))) + nil)) + +(defconst *mod-caller-prog* (assemble '(pushsi 0 pushsi 1 add pushsi 100 call 20 jump 6))) + +(defconst *mod-prog* (assemble '(pop 19 ;20 + pop 18 + pushs 18 ;24 + pushs 19 + sub + dup + jumpz 36 + pop 18 + jump 24 + pushs 19 ;36 + pushs 18 + sub + jumpz 45 + jump 49 + pushsi 0 ;45 + pop 18 + pop 19 ;49 + pushs 18 + ret + ))) + +(defun run-example-tiny-state (n tiny-state) + (declare (xargs :verify-guards nil :stobjs (tiny-state))) + (let ((tiny-state (load-tiny 4 (list (cons 4 *mod-caller-prog*) (cons 20 *mod-prog*)) tiny-state))) + (tiny tiny-state n))) + +#| +ACL2 !>:q + +Exiting the ACL2 read-eval-print loop. To re-enter, execute (LP). +ACL2>(time (run-example-tiny-state 10000000 *the-live-tiny-state*)) +real time : 12.000 secs +run time : 12.010 secs +(#(9) + #(0 0 0 0 2 0 2 1 3 2 100 6 20 4 6 0 0 0 50 0 0 19 0 18 1 18 1 19 8 9 + 5 36 0 18 4 24 1 19 1 18 8 5 45 4 49 2 0 0 18 0 19 1 18 7 0 0 0 0 0 + 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 + 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 + 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 + 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 + 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 + 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 + 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 + 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 + 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 + 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 + 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 + 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 + 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 + 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 + 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 + 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 + 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 + 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 + 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 + 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 + 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 + 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 + 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 + 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 + 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 50 1 51 0 0 0 0 0 0 0 + 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 + 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 + 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 13 0 0 0 0 0 0 0 0 0 + 0 0 0 0 0 0 0 0 0 0 0 0 0 0) + #(899) #(1000)) + +ACL2> + +|# + +;;;;; +;;;;; Proof about the benchmark program +;;;;; + +;;; The proof begins with many preliminaries that help us reason about +;;; programs of this type. + +;;; We are not interested in guard-proofs about functions we +;;; use for specification and proof +;(set-verify-guards-eagerness 0) + +;; Is "program" loaded at "location" in Tiny state? +(defun program-loaded (tiny-state program location) + (declare (xargs :stobjs (tiny-state) + :guard (and (integerp location) + (<= 0 location) + (< location (- 1024 (len program))) + (true-listp program)))) + (or (endp program) + (and (equal (memi location tiny-state) (car program)) + (program-loaded tiny-state (cdr program) (1+ location))))) + +(set-verify-guards-eagerness 0) + +(defthm prog-lookup + (implies (and (syntaxp (quotep n)) + (program-loaded tiny-state prog loc) + (integerp loc) + (<= loc (nfix n)) + (< (nfix n) (+ loc (len prog)))) + (equal (nth n (nth *memi* tiny-state)) + (nth (- n loc) prog))) + :hints (("goal" :in-theory (enable len nth)))) + +(in-theory (disable program-loaded)) + +(defthm +bv32-simple + (implies + (and + (integerp x) (integerp y) + (< x (expt 2 30)) ; modified by Matt K. for v2-7 + (>= x (- (expt 2 30))) + (< y (expt 2 30)) ; modified by Matt K. for v2-7 + (>= y (- (expt 2 30)))) + (equal (+bv32 x y) (+ x y))) + :hints (("goal" :in-theory (enable +bv32 signed-byte-p)))) + +(defthm +bv32-simple2 + (implies + (and + (integerp x) (integerp y) + (< x (expt 2 31)) ; modified by Matt K. for v2-7 + (>= x 0) + (< y (expt 2 31)) ; modified by Matt K. for v2-7 + (>= y 0)) + (equal (+bv32 x (- y)) (+ x (- y)))) + :hints (("goal" :in-theory (enable +bv32 signed-byte-p)))) + +(defthm +bv32-0 + (implies + (and + (integerp x) + (< x (expt 2 31)) ; modified by Matt K. for v2-7 + (<= (- (expt 2 31)) x)) + (equal (+bv32 x 0) x)) + :hints (("goal" :in-theory (enable +bv32 signed-byte-p)))) + +(defthm tiny-straightline + (implies + (syntaxp (quotep n)) + (equal (tiny tiny-state n) + (if (zp n) tiny-state (tiny (next tiny-state) (1- n))))) + :hints (("goal" :in-theory (disable next)))) + +(defun c+ (x y) (+ (nfix x) (nfix y))) + +(defthm tiny-c+ + (equal (tiny s (c+ x y)) + (tiny (tiny s x) y)) + :hints (("goal" :induct (tiny s x) + :in-theory (set-difference-theories (enable tiny) '(next))))) + +(in-theory (disable c+)) + +(defthm integerp-max + (implies + (and (integerp a) (integerp b)) + (integerp (max a b)))) + +(defthm max-less + (and + (equal + (< (max a b) c) + (and (< a c) (< b c))) + (equal + (< c (max a b)) + (or (< c a) (< c b))))) + +(defthm equal-max-x-x + (implies + (and (integerp b) (integerp a)) + (and + (equal (equal (max a b) a) (<= b a)) + (equal (equal (max b a) a) (<= b a)))) + :hints (("goal" :in-theory (enable max)))) + +(in-theory (disable max)) + +(defthm equal-plus-x-x + (implies + (and (integerp b) (integerp a)) + (equal (equal (+ a b) b) (equal a 0)))) + +(defthm integerp-unary-- + (implies + (integerp x) + (integerp (unary-- x)))) + +(defthm integerp-+ + (implies + (and + (integerp x) + (integerp y)) + (integerp (+ x y)))) + +(in-theory (disable tiny)) + +(defthm lessp-minus-hack4 + (implies + (and + (<= a n) + (<= b n) + (<= 0 b) + (integerp a) + (integerp b) + (integerp n)) + (<= (+ a (- b)) n))) + + +(defthm max-0-a-b + (and + (implies (<= a b) (equal (max 0 (+ a (- b))) 0)) + (implies (>= a b) (equal (max 0 (+ a (- b))) (+ a (- b))))) + :hints (("goal" :in-theory (enable max)))) + +(defthm max-open + (implies + (and + (<= a b) + (integerp a) (integerp b)) + (equal (max a b) b))) + +;; Try to backchain on nth-update-nth before casesplitting +(defthm nth-update-nth2 + (equal + (nth n1 (update-nth n2 v l)) + (if (equal (nfix n1) (nfix n2)) + v + (nth n1 l))) + :hints (("goal" :in-theory (enable update-nth nth)))) + +(defthm nth-update-nth-1 + (implies + (not (equal (nfix n1) (nfix n2))) + (equal + (nth n1 (update-nth n2 v l)) + (nth n1 l)))) + +(defthm nth-update-nth-2 + (implies + (equal (nfix n1) (nfix n2)) + (equal + (nth n1 (update-nth n2 v l)) + v))) + +(defun repeat (n v) + (if (zp n) + nil + (cons v (repeat (1- n) v)))) + +(defthm update-nth-nil + (equal (update-nth i v nil) + (append (repeat i nil) (list v))) + :hints (("goal" :in-theory (enable update-nth)))) + +(defthm update-nth-nth-noop-helper + (implies + (and (<= 0 n) (< n (len l))) + (equal (update-nth n (nth n l) l) l)) + :hints (("goal" :in-theory (enable nth update-nth)))) + +(defthm update-nth-nth-noop + (implies + (and (<= 0 n) (< n (len l1)) (equal (nth n l1) (nth n l2))) + (equal (update-nth n (nth n l2) l1) l1))) + +;; order update-nth terms based on update field value +(defthm update-nth-update-nth-diff + (implies + (not (equal (nfix i1) (nfix i2))) + (equal (update-nth i1 v1 (update-nth i2 v2 l)) + (update-nth i2 v2 (update-nth i1 v1 l)))) + :hints (("goal" :in-theory (enable update-nth))) + :rule-classes ((:rewrite :loop-stopper ((i1 i2))))) + +(defthm update-nth-update-nth-same + (equal (update-nth i v1 (update-nth i v2 l)) + (update-nth i v1 l)) + :hints (("goal" :in-theory (enable update-nth)))) + +(defthm len-repeat + (equal (len (repeat i v)) (nfix i))) + +(defthm len-update-nth-better + (equal (len (update-nth i v l)) (max (1+ (nfix i)) (len l))) + :hints (("goal" :in-theory (enable update-nth max)))) + +(defthm car-update-nth + (equal (car (update-nth i v l)) (if (zp i) v (car l))) + :hints (("goal" :in-theory (enable update-nth)))) + +(defthm len-pushus + (implies + (equal (len tiny-state) 4) + (equal (len (pushus val tiny-state)) 4)) + :hints (("goal" :in-theory (disable logand-with-mask)))) + +(defthm car-append + (equal (car (append x y)) + (if (consp x) (car x) (car y)))) + +(defthm cdr-append + (equal (cdr (append x y)) + (if (consp x) (append (cdr x) y) (cdr y)))) + +(defthm equal-plus-0 + (implies + (and (integerp a) (integerp b) (<= 0 a) (<= 0 b)) + (equal (equal 0 (+ a b)) (and (equal a 0) (equal b 0))))) + +(defthm equal-nat-neg-0 + (implies + (and + (integerp n1) + (integerp n2) + (<= 0 n1) + (<= 0 n2)) + (and + (equal (equal (+ n1 (- n2)) 0) (equal n1 n2)) + (equal (equal (+ (- n2) n1) 0) (equal n1 n2))))) + +(defthm car-nthcdr + (equal (car (nthcdr n l)) (nth n l)) + :hints (("goal" :in-theory (enable nth)))) + +(in-theory (disable next logand floor len update-nth max)) + +(in-theory (enable +bv32)) + +;; We start proving facts about the benchmark + +;; Effect of running loop once (taken from theorem prover output) +(defun mod-loop-once-effect (tiny-state) + (update-nth *progc* 24 + (update-nth *memi* + (update-nth 18 + (+ (nth 18 (nth *memi* tiny-state)) + (- (nth 19 (nth *memi* tiny-state)))) + (update-nth (nth *dtos* tiny-state) + (+ (nth 18 (nth *memi* tiny-state)) + (- (nth 19 (nth *memi* tiny-state)))) + (update-nth (+ -1 (nth *dtos* tiny-state)) + (+ (nth 18 (nth *memi* tiny-state)) + (- (nth 19 (nth *memi* tiny-state)))) + (nth *memi* tiny-state)))) + (update-nth *dtos* (nth *dtos* tiny-state) tiny-state)))) + +(in-theory (disable update-nth-update-nth)) +(in-theory (enable len)) + +(defthm mod-loop-repeat + (implies + (and + (tiny-statep tiny-state) + (< (dtos tiny-state) 1000) (>= (dtos tiny-state) 100) + (equal (progc tiny-state) 24) + (program-loaded tiny-state *mod-prog* 20) + (<= 0 (memi 19 tiny-state)) + (<= 0 (memi 18 tiny-state)) + (< (memi 19 tiny-state) (memi 18 tiny-state)) + (not (= (memi 19 tiny-state) (memi 18 tiny-state)))) ;;redundant, but simplifies proof + (equal (tiny tiny-state 7) + (mod-loop-once-effect tiny-state))) + :hints (("goal''" :in-theory (enable next signed-byte-p len)))) + +;; Effect of loop when it ends with no adjust needed (expression taken +;;from theorem prover output) +(defthm mod-loop-end1 + (implies + (and + (tiny-statep tiny-state) + (< (dtos tiny-state) 1000) (>= (dtos tiny-state) 100) + (<= (ctos tiny-state) 1020) (> (ctos tiny-state) 1010) + (equal (progc tiny-state) 24) + (program-loaded tiny-state *mod-prog* 20) + (<= 0 (memi 19 tiny-state)) + (< 0 (memi 18 tiny-state)) + (> (memi 19 tiny-state) (memi 18 tiny-state)) + (not (= (memi 19 tiny-state) (memi 18 tiny-state)))) ;;redundant + (equal (tiny tiny-state 13) + (update-nth *progc* + (logand (nth (+ 1 (nth *ctos* tiny-state)) (nth *memi* tiny-state)) + 1023) + (update-nth *memi* + (update-nth 19 0 + (update-nth (nth *dtos* tiny-state) + (nth 18 (nth *memi* tiny-state)) + (update-nth (+ -1 (nth *dtos* tiny-state)) + (+ (- (nth 18 (nth *memi* tiny-state))) + (nth 19 (nth *memi* tiny-state))) + (update-nth (+ -2 (nth *dtos* tiny-state)) + (nth 18 (nth *memi* tiny-state)) + (nth *memi* tiny-state))))) + (update-nth *dtos* (+ -1 (nth *dtos* tiny-state)) + (update-nth *ctos* (+ 1 (nth *ctos* tiny-state)) tiny-state)))))) + :hints (("goal''" :in-theory (enable next signed-byte-p)))) + +;; Effect of loop when it ends with an adjust needed (expression taken +;;from theorem prover output) +(defthm mod-loop-end2 + (implies + (and + (tiny-statep tiny-state) + (< (dtos tiny-state) 1000) (>= (dtos tiny-state) 100) + (<= (ctos tiny-state) 1020) (> (ctos tiny-state) 1010) + (equal (progc tiny-state) 24) + (program-loaded tiny-state *mod-prog* 20) + (<= 0 (memi 19 tiny-state)) + (< 0 (memi 18 tiny-state)) + (= (memi 19 tiny-state) (memi 18 tiny-state))) + (equal (tiny tiny-state 14) + (update-nth + *progc* + (logand (nth (+ 1 (nth *ctos* tiny-state)) (nth *memi* tiny-state)) + 1023) + (update-nth *memi* + (update-nth 18 0 + (update-nth 19 0 + (update-nth (nth *dtos* tiny-state) + 0 + (update-nth (+ -1 (nth *dtos* tiny-state)) + 0 + (update-nth (+ -2 (nth *dtos* tiny-state)) + (nth 18 (nth *memi* tiny-state)) + (nth *memi* tiny-state)))))) + (update-nth *dtos* (+ -1 (nth *dtos* tiny-state)) + (update-nth *ctos* (+ 1 (nth *ctos* tiny-state)) tiny-state)))))) + :hints (("goal''" :in-theory (enable next signed-byte-p)))) + +;; number of instructions needed to execute loop for values x and y. +(defun modloop-clock-helper (x y) + (if (or (not (integerp x)) (not (integerp y)) (>= 0 y) (<= x y)) + (if (equal x y) 14 13) + (c+ 7 (modloop-clock-helper (- x y) y)))) + +(defun modloop-clock (tiny-state) + (declare (xargs :stobjs (tiny-state))) + (let ((x (memi 18 tiny-state)) (y (memi 19 tiny-state))) + (modloop-clock-helper x y))) + +(defun remainder-prog-result (n p) + (if (or (zp p) (zp n) (< n p)) + (nfix n) + (remainder-prog-result (- n p) p))) + +(set-irrelevant-formals-ok :warn) + +(defun mod-loop-repeat-induct (x y s) + (if (or (not (integerp x)) (not (integerp y)) (>= 0 y) (<= x y)) + t + (mod-loop-repeat-induct (- x y) y (mod-loop-once-effect s)))) + +; Modified by Matt Kaufmann for ACL2 Version 2.6. +(defthm memp-update-nth + (implies + (and + (memp l) + (integerp a) + (<= 0 a) + (< a (len l))) + (equal (memp (update-nth a v l)) + (AND (INTEGERP v) (<= -2147483648 v) (<= v 2147483647)))) + :hints (("goal" :in-theory (enable update-nth)))) + +(in-theory (enable max)) + +(defun sub1-add1-cdr (n1 n2 l) + (if (consp l) + (sub1-add1-cdr (1- n1) (1+ n2) (cdr l)) + t)) + +(defthm update-nth-equal + (implies + (and + (< n (len l)) + (<= 0 n) (integerp n)) + (equal (update-nth n (nth n l) l) l)) + :hints (("goal" :in-theory (enable nth update-nth len)))) + +(defthm program-loaded-irrelevant + (implies + (not (equal n 1)) + (equal (program-loaded (update-nth n v tiny-state) prog loc) + (program-loaded tiny-state prog loc))) + :hints (("goal" :in-theory (enable update-nth program-loaded)))) + + +;; such a screwy rule. It's inelegant because program-loaded is a function +;; of state. +(defthm program-loaded-cons + (implies + (and + (or (< n loc) (< (+ (len prog) loc) n) (equal val (nth n mem))) + (integerp n) (<= 0 n) (integerp loc) (<= 0 loc) + (program-loaded (update-nth 1 mem tiny-state) prog loc)) + (program-loaded (update-nth 1 (update-nth n val mem) tiny-state) prog loc)) + :hints (("goal" :in-theory (enable program-loaded update-nth nth len)))) + +(defthm mod-loop-calculates-mod + (implies + (and + (tiny-statep tiny-state) + (< (dtos tiny-state) 1000) (>= (dtos tiny-state) 100) + (<= (ctos tiny-state) 1020) (> (ctos tiny-state) 1010) + (equal (progc tiny-state) 24) + (program-loaded tiny-state *mod-prog* 20) + (equal a (memi 18 tiny-state)) + (equal b (memi 19 tiny-state)) + (< 0 a) (< 0 b) + (equal s2 (tiny tiny-state (modloop-clock-helper a b)))) + (equal (memi (1+ (dtos s2)) s2) (remainder-prog-result a b))) + :rule-classes nil + :hints (("goal" :in-theory (set-difference-theories + (enable tiny-statep len) + '(tiny-straightline)) + :induct (mod-loop-repeat-induct a b tiny-state)) + ("Subgoal *1/1.1'" :expand (REMAINDER-PROG-RESULT (NTH 18 (NTH 1 TINY-STATE)) + (NTH 19 (NTH 1 TINY-STATE)))))) + +(defun remclock (tiny-state) + (declare (xargs :stobjs (tiny-state))) + (modloop-clock-helper (memi 18 tiny-state) (memi 19 tiny-state))) + +(defun good-initial-remainder-state (tiny-state) + (declare (xargs :stobjs (tiny-state))) + (and + (tiny-statep tiny-state) + (< (dtos tiny-state) 1000) (>= (dtos tiny-state) 100) + (<= (ctos tiny-state) 1020) (> (ctos tiny-state) 1010) + (equal (progc tiny-state) 24) + (program-loaded tiny-state *mod-prog* 20) + (< 0 (memi 18 tiny-state)) + (< 0 (memi 19 tiny-state)))) + +(defthm remainder-correct + (let ((s2 (tiny tiny-state (remclock tiny-state)))) + (implies + (good-initial-remainder-state tiny-state) + (equal (memi (1+ (dtos s2)) s2) + (remainder-prog-result (memi 18 tiny-state) (memi 19 tiny-state))))) + :rule-classes nil + :hints (("goal" + :use ((:instance mod-loop-calculates-mod + (s2 (tiny tiny-state (modloop-clock-helper (memi 18 tiny-state) (memi 19 tiny-state)))) + (a (memi 18 tiny-state)) + (b (memi 19 tiny-state)))) + :in-theory (disable tiny-straightline)))) + +;;; Show that our recursive version of remainder is identical to mod. +;;; Fortunately, Bishop Brock's been here before. + +(include-book "ihs/quotient-remainder-lemmas" :dir :system) + +(defthm remainder-is-mod + (implies + (and + (integerp x) + (<= 0 x) + (integerp y) + (<= 0 y)) + (equal (remainder-prog-result x y) (mod x y)))) + +(defthm mod-correct + (let ((s2 (tiny tiny-state (remclock tiny-state)))) + (implies + (good-initial-remainder-state tiny-state) + (equal (memi (1+ (dtos s2)) s2) + (mod (memi 18 tiny-state) (memi 19 tiny-state))))) + :rule-classes nil + :hints (("goal" :use ((:instance remainder-correct))))) + diff --git a/books/workshops/2004/matthews-vroon/support/tiny-fib-example/with-copy-of-stobj.lsp b/books/workshops/2004/matthews-vroon/support/tiny-fib-example/with-copy-of-stobj.lsp new file mode 100644 index 0000000..5aa1d0f --- /dev/null +++ b/books/workshops/2004/matthews-vroon/support/tiny-fib-example/with-copy-of-stobj.lsp @@ -0,0 +1,38 @@ +(defmacro with-copy-of-stobj (stobj mv-let-form) + (let ((copy-from-stobj (join-symbols stobj 'copy-from- stobj)) + (copy-to-stobj (join-symbols stobj 'copy-to- stobj))) + `(let ((stobj (,copy-from-stobj ,stobj))) + (with-local-stobj + ,stobj + (mv-let ,(nth 1 mv-let-form) + (let ((,stobj (,copy-to-stobj stobj ,stobj))) + ,(nth 2 mv-let-form)) + ,(nth 3 mv-let-form)))))) + +(defun steps-to-cutpoint (tiny-state) + (declare (xargs :stobjs (tiny-state))) + (let ((steps (steps-to-cutpoint-tail 0 (copy-from-tiny-state tiny-state)))) + (if (and (natp steps) ;the number of steps is a natural number + (with-copy-of-stobj + tiny-state + (mv-let (result tiny-state) + (let ((tiny-state (run steps tiny-state))) + (mv (at-cutpoint tiny-state) tiny-state)) + result))) + steps + (omega)))) + +(defun steps-to-cutpoint (tiny-state) + (declare (xargs :stobjs (tiny-state))) + (let ((steps (steps-to-cutpoint-tail 0 (copy-from-tiny-state tiny-state)))) + (if (and (natp steps) ;the number of steps is a natural number + (let ((ts (copy-from-tiny-state tiny-state))) ;all of this is to see if + (with-local-stobj ;we're at a cutpoint + tiny-state ;if we run the machine for + (mv-let (result tiny-state) ;steps steps + (let* ((tiny-state (copy-to-tiny-state ts tiny-state)) + (tiny-state (run steps tiny-state))) + (mv (at-cutpoint tiny-state) tiny-state)) + result)))) + steps + (omega))))
\ No newline at end of file |