; Copyright (C) 2000 Panagiotis Manolios and J Strother Moore
; 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 Panagiotis Manolios who can be reached as follows.
; Email: pete@cs.utexas.edu, moore@cs.utexas.edu
; Postal Mail:
; Department of Computer Sciences
; Taylor Hall 2.124 [C0500]
; The University of Texas at Austin
; Austin, TX 78712-1188 USA
; (include-book "/v/hank/v104/text/defpun/examples")
; (certify-book "tjvm-examples" 1)
(in-package "TJVM")
(include-book "defpun")
(defmacro defpun (&rest rest) (cons 'acl2::defpun rest))
(defun haltedp (s) (equal s (step s)))
(defpun stepw (s)
(if (haltedp s)
s
(stepw (step s))))
(defun == (a b)(equal (stepw a) (stepw b)))
(defequiv ==)
(in-theory (disable step-opener))
(defthm stepw-step
(equal (stepw s) (stepw (step s)))
:rule-classes nil)
; This event is here only so we can exhibit it in the paper.
(defthm ==-step
(== (make-state call-stack heap class-table)
(step (make-state call-stack heap class-table)))
:rule-classes nil)
(defthm ==-stepper
(implies (and (consp (NTH (PC (TOP call-stack))
(PROGRAM (TOP call-stack))))
(not (equal (car (NTH (PC (TOP call-stack))
(PROGRAM (TOP call-stack))))
'invokestatic)))
(== (make-state
call-stack
heap
class-table)
(step (make-state
call-stack
heap
class-table))))
:hints (("Goal" :in-theory (disable step))))
(defthm general-==-stepper
(implies (equal call-stack call-stack) ; not an abbreviation rule!
(== (make-state call-stack
heap
class-table)
(step (make-state call-stack
heap
class-table)))))
(defun stepn (s n)
(if (zp n)
s
(stepn (step s) (- n 1))))
(defthm ==-stepn
(== (stepn s n) s))
(defthm ==-Y
(implies (== (stepn s1 n)
(stepn s2 m))
(== s1 s2))
:rule-classes nil)
(in-theory (disable general-==-stepper ==))
(in-theory (enable step))
; A consequence of this setup is that for every primitive instruction
; except for invokestatic we have a theorem like the following.
(defthm ==-load-rewrite
(implies (equal (nth (pc (top call-stack))
(program (top call-stack)))
`(load ,var))
(== (make-state call-stack
heap
class-table)
(make-state
(push (make-frame (+ 1 (pc (top call-stack)))
(locals (top call-stack))
(push (binding var (locals (top call-stack)))
(stack (top call-stack)))
(program (top call-stack)))
(pop call-stack))
heap
class-table)))
:rule-classes nil)
; Ok, that completes the general work. Now let's deal with fact.
(defun fact-==-hint (call-stack heap table n)
(if (zp n)
(list call-stack heap table)
(fact-==-hint
(push (make-frame 6
(list (cons 'n (top (stack (top call-stack)))))
(push (- (top (stack (top call-stack))) 1)
(push (top (stack (top call-stack)))
nil))
(method-program (\bf_fact)))
(push (make-frame (+ 1 (pc (top call-stack)))
(locals (top call-stack))
(pop (stack (top call-stack)))
(program (top call-stack)))
(pop call-stack)))
heap
table
(- n 1))))
(defun Math-class-loadedp (class-table)
(equal (assoc-equal "Math" class-table)
(\bfMath-class)))
; The following lemma is proved just so we can prove the next
; theorem without any hints. The hintless version is shown in the paper.
(defthm ==-invokestatic-fact-lemma
(implies (and (equal (nth (pc (top call-stack))
(program (top call-stack)))
'(invokestatic "Math" "fact" 1))
(Math-class-loadedp class-table)
(equal n (top (stack (top call-stack))))
(natp n))
(== (make-state call-stack
heap
class-table)
(make-state
(push (make-frame (+ 1 (pc (top call-stack)))
(locals (top call-stack))
(push (fact n)
(pop (stack (top call-stack))))
(program (top call-stack)))
(pop call-stack))
heap
class-table)))
:hints (("Goal" :in-theory (enable general-==-stepper top-frame)
:restrict ((general-==-STEPPER
((call-stack call-stack)
(heap heap)
(class-table class-table))))
:induct (fact-==-hint call-stack heap class-table n))))
(defthm ==-invokestatic-fact-rewrite
(implies (and (equal (nth (pc (top call-stack))
(program (top call-stack)))
'(invokestatic "Math" "fact" 1))
(Math-class-loadedp class-table)
(equal n (top (stack (top call-stack))))
(natp n))
(== (make-state call-stack
heap
class-table)
(make-state
(push (make-frame (+ 1 (pc (top call-stack)))
(locals (top call-stack))
(push (fact n)
(pop (stack (top call-stack))))
(program (top call-stack)))
(pop call-stack))
heap
class-table))))
; We now define poised-on and modify appropriately so that we can
; restate ==-load and ==-invokevirtual-fact more simply. Poised-on is
; a slight misnomer: it also insures that the state is a triple. But
; this is fair because the original versions of ==-load, etc., only
; applied to make-state triples. The whole reason we restate our
; theorems is so that the reader can see their similarity. The
; restated versions are not really very useful because, as rewrite
; rules, they rewrite the variable symbol s.
(defun statep (x)
(and (consp (cddr x))
(equal (cdddr x) nil)))
(defthm make-state-elim
(implies (statep s)
(equal (make-state (call-stack s)
(heap s)
(class-table s))
s))
:rule-classes :elim
:hints (("Goal" :in-theory (enable make-state call-stack heap class-table))))
(defun poised-on (s inst)
(and (statep s)
(equal (next-inst s) inst)))
; In the formal definitions of m3 and m4, a modify macro similar to
; this is used.
(defmacro modify (s &key
(pc '0 pcp)
(locals 'nil localsp)
(stack 'nil stackp)
(heap 'nil heapp))
`(make-state
(push (make-frame
,(if pcp pc `(pc (top (call-stack ,s))))
,(if localsp locals `(locals (top (call-stack ,s))))
,(if stackp stack `(stack (top (call-stack ,s))))
(program (top (call-stack ,s))))
(pop (call-stack ,s)))
,(if heapp heap `(heap ,s))
(class-table ,s)))
(defthm ==-load
(implies
(poised-on s `(load ,var))
(== s
(modify s
:pc (+ 1 (pc (top (call-stack s))))
:stack (push (binding var (locals (top (call-stack s))))
(stack (top (call-stack s)))))))
:rule-classes nil)
(defthm ==-invokestatic-fact
(implies
(and (poised-on s '(invokestatic "Math" "fact" 1))
(Math-class-loadedp (class-table s))
(equal n (top (stack (top (call-stack s)))))
(natp n))
(== s
(modify s
:pc (+ 1 (pc (top (call-stack s))))
:stack (push (fact n)
(pop (stack (top (call-stack s))))))))
:rule-classes nil)