; M1 Correctness Without a Clock
; Copyright (C) 2004 J Strother Moore and John R. Cowles,
; University of Texas at Austin and
University of Wyoming
; This program is free software; you can redistribute it and/or
; modify it under the terms of the GNU General Public License as
; published by the Free Software Foundation; either version 2 of
; the License, or (at your option) any later version.
; This program is distributed in the hope that it will be useful,
; but WITHOUT ANY WARRANTY; without even the implied warranty of
; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
; GNU General Public License for more details.
; You should have received a copy of the GNU General Public
; License along with this program; if not, write to the Free
; Software Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139,
; USA.
; Written by: John R. Cowles
; email: cowles@uwyo.edu
; Department of Computer Science
; University of Wyoming
; Laramie, WY 82071 U.S.A.
; Based on earlier work and ideas of
; J Strother Moore and Panagiotis Manolios
; email: Moore@cs.utexas.edu manolios@cc.gatech.edu
; Department of Computer Sciences College of Computing
; University of Texas at Austin Georgia Institute of Technology
; Austin, TX 78712-1188 U.S.A. Atlanta Georgia 30332-0280 U.S.A.
;==================================================================
(include-book "m1-utilities")
(in-package "M1")
; This is the Defpun book by Manolios and Moore. It may be found
; on the class website.
; You should copy the Defpun book to your file system and
; recertify it.
; Then change the absolute path name below to point to your copy
; of defpun.lisp.
(include-book "defpun")
; Defpun is not part of the m1-utilities, so it is added by macro.
(defmacro defpun (g args &rest tail)
`(acl2::defpun ,g ,args ,@tail))
;; The clocked interpreter for M1 is
;; (DEFUN RUN (S N)
;; (IF (ZP N)
;; S
;; (RUN (STEP S) (- N 1))))
;; An interpreter without a clock for M1 is given below by run-w.
;; (run-w s) runs state s to termination, if a halted state can be
;; reached by repeated steps of M1. The value of (run-w s) on
;; states that do not terminate is not specified.
(defun haltedp (s)
(equal s (step s)))
(defpun run-w (s)
(if (haltedp s)
s
(run-w (step s))))
;; The following equivalence relation holds between two terminating
;; states precisely when they terminate in the same state.
(defun == (s1 s2)
(equal (run-w s1)
(run-w s2)))
;; ==-IS-AN-EQUIVALENCE
(defequiv ==)
(in-theory (disable step-opener))
;; Any state is related by == to the state obtained by stepping
;; M1 once.
(defthm ==-step
(== s (step s))
:rule-classes nil)
(defthm ==-stepper
(implies (and (consp (next-inst
(make-state call-stack defs)))
(not (equal
(op-code (next-inst
(make-state call-stack defs)))
'call)))
(== (make-state call-stack defs)
(step (make-state call-stack defs)))))
(defthm general-==-stepper
(implies (equal call-stack call-stack) ; not an abbreviation rule!
(== (make-state call-stack defs)
(step (make-state call-stack defs)))))
(defthm ==-run
(== (run s n) s)
:hints (("Goal"
:in-theory (enable run))))
;; The next theorem implies that if the execution paths from s1
;; s2 intersect, then (== s1 s2).
(defthm ==-Y
(implies (== (run s1 n)
(run s2 m))
(== s1 s2))
:rule-classes nil)
(in-theory (disable == general-==-stepper))
(in-theory (enable step))
;;-----------------------------------------------------
;; Square
(defconst *sq-def*
'(sq (n)
(load n)
(dup)
(mul)
(ret)))
(defabbrev sq (x)
(* x x))
(defun execute-SQ (s)
(modify s
:pc (+ 1 (pc s)) ;; (pc s) = pc of
;; (top-frame s)
:stack (push (sq (top (stack s))) ;; (stack s) = stack
(pop (stack s))))) ;; of (top-frame s)
;; The M1 program for the function sq behaves as expected:
(defthm ==-sq
(implies (equal (bound? 'sq (defs s))
*sq-def*)
(== (do-inst '(call sq) s)
(execute-sq s))))
;;----------------------------------------------------
;; Max
(defconst *max-def*
'(max (x y)
(load x)
(load y)
(sub)
(ifle 3)
(load x)
(ret)
(load y)
(ret)))
(defun execute-MAX (s)
(modify s
:pc (+ 1 (pc s)) ;; (pc s) = pc of
;; (top-frame s)
:stack (push (max (top (pop (stack s)))
(top (stack s)));; (stack s) = stack
(pop (pop (stack s))))));; of (top-frame s)
;; The M1 program for the function max behaves as expected:
(defthm ==-max
(implies (equal (bound? 'max (defs s))
*max-def*)
(== (do-inst '(call max) s)
(execute-max s))))
;;---------------------------------------------------
;; Recursive factorial
(defconst *fact-def*
'(fact (n)
(load n) ;; 0
(ifgt 3) ;; 1
(push 1) ;; 2
(ret) ;; 3
(load n) ;; 4
(load n) ;; 5
(push 1) ;; 6
(sub) ;; 7
(call fact) ;; 8
(mul) ;; 9
(ret))) ;; 10
(defun ! (n)
(if (zp n)
1
(* n (! (- n 1)))))
(defun execute-FACT (s)
(modify s
:pc (+ 1 (pc s)) ;; (pc s) = pc of
;; (top-frame s)
:stack (push (! (top (stack s))) ;; (stack s) = stack
(pop (stack s))))) ;; of (top-frame s)
(in-theory (disable (:EXECUTABLE-COUNTERPART MAKE-FRAME)))
;; This induction-hint was created from the failed proof
;; of ==-fact-lemma without the induction hint.
(defun ==-fact-hint (call-stack defs n)
(if (zp n)
(list call-stack defs)
(==-fact-hint
(push (make-frame 8
(list (cons 'n
(top (stack
(make-state call-stack
defs)))))
(push (+ -1 (top (stack
(make-state call-stack
defs))))
(push (top (stack
(make-state call-stack
defs)))
nil))
(cddr *fact-def*))
(push (make-frame (+ 1 (pc (make-state call-stack
defs)))
(locals (make-state call-stack
defs))
(pop (stack (make-state call-stack
defs)))
(program (make-state call-stack
defs)))
(pop call-stack)))
defs
(- n 1))))
;; Note the :restrict hint below.
;; This hint restricts the application of the rewrite rule,
;; general-==-stepper.
;; Please look up the :restrict hint in ACL2's documentation.
;; Look under HINTS.
(defthm ==-fact-lemma
(implies (and (equal (bound? 'fact defs)
*fact-def*)
(equal (next-inst (make-state call-stack
defs))
'(call fact))
(equal n (top (stack (make-state call-stack
defs))))
(integerp n)
(>= n 0))
(== (make-state call-stack defs)
(execute-FACT (make-state call-stack defs))))
:hints (("Goal"
:in-theory (enable general-==-stepper)
:restrict ((general-==-stepper
((call-stack call-stack)
(defs defs))))
:induct (==-fact-hint call-stack defs n))))
;; The M1 program for the function fact behaves as expected:
(defthm ==-fact
(implies (and (equal (bound? 'fact (defs s))
*fact-def*)
(integerp (top (stack s)))
(>= (top (stack s)) 0))
(== (do-inst '(call fact) s)
(execute-FACT s))))
(in-theory (disable ==-fact-lemma))
;;----------------------------------------------------
;; Use the interpreter without a clock for M1, run-w, to
;; state and prove an M1 program correctness result.
;; Informal Correctness Result
;; Let s be the following state
;; (modify nil
;; :pc 0
;; :locals local-vars
;; :stack s0
;; :program '((load x) ;; 0
;; (call sq) ;; 1
;; (call fact) ;; 2
;; (load x) ;; 3
;; (call fact) ;; 4
;; (call sq) ;; 5
;; (call max) ;; 6
;; (store y) ;; 7
;; (halt)) ;; 8
;; :defs (list *sq-def*
;; *max-def*
;; *fact-def*)).
;; Let x be the value of the variable 'x in (locals s).
;; If x is a nonnegative integer and s is run to
;; termination, then M1 ends in the following state:
;; (modify s
;; :pc 8
;; :locals (bind 'y (max (! (sq x))
;; (sq (! x)))
;; (locals s)))
;; First we show that the initial state above is related
;; by == to the final state above.
(defthm ==-s-halt-state
(let* ((s (modify nil
:pc 0
:locals local-vars
:stack s0
:program '((load x) ;; 0
(call sq) ;; 1
(call fact) ;; 2
(load x) ;; 3
(call fact) ;; 4
(call sq) ;; 5
(call max) ;; 6
(store y) ;; 7
(halt)) ;; 8
:defs (list *sq-def*
*max-def*
*fact-def*)))
(x (binding 'x (locals s))))
(implies (and (integerp x)
(>= x 0))
(== s
(modify s
:pc 8
:locals (bind 'y (max (! (sq x))
(sq (! x)))
(locals s))))))
:rule-classes nil
:hints (("Goal"
:in-theory (enable general-==-stepper))))
;; Formal Correctness Result
(defthm prog-is-correct
(let* ((s (modify nil
:pc 0
:locals local-vars
:stack s0
:program '((load x) ;; 0
(call sq) ;; 1
(call fact) ;; 2
(load x) ;; 3
(call fact) ;; 4
(call sq) ;; 5
(call max) ;; 6
(store y) ;; 7
(halt)) ;; 8
:defs (list *sq-def*
*max-def*
*fact-def*)))
(x (binding 'x (locals s))))
(implies (and (integerp x)
(>= x 0))
(equal (run-w s)
(modify s
:pc 8
:locals (bind 'y (max (! (sq x))
(sq (! x)))
(locals s))))))
:hints (("Goal"
:in-theory (enable ==)
:use ==-s-halt-state)))