; Copyright (C) 2001 J Strother Moore

; This book 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 book 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 book; if not, write to the Free
; Software Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139,
; USA.

#|
; Certification Instructions.

(include-book "m5")

(certify-book "utilities" 1)

J Moore
|#

(in-package "M5")

; Here we develop the general theory for proving things about the
; M5 bytecode.

; Arithmetic

(include-book
 "/projects/acl2/v2-6/books/arithmetic/top-with-meta")

; We prove a few things about int arithmetic.  We ought to prove
; many more, but I just put enough here to get the factorial
; proof to go through.

(include-book
 "/projects/acl2/v2-6/books/ihs/quotient-remainder-lemmas")

(defun intp (x)
  (and (integerp x)
       (<= (- (expt 2 31)) x)
       (< x (expt 2 31))))

(defthm int-lemma0
  (implies (intp x)
           (integerp x))
  :rule-classes (:rewrite :forward-chaining))

(defthm int-lemma1
  (intp (int-fix x)))

(local (in-theory (cons 'zp (disable mod))))

(defthm int-lemma2
  (implies (and (intp x)
                (not (zp x)))
           (equal (int-fix (+ -1 x))
                  (+ -1 x))))

(defthm int-lemma3
  (implies (and (intp x)
                (not (zp x)))
           (intp (+ -1 x))))

(defthm int-lemma4a
  (implies (and (integerp x)
                (integerp y))
           (equal (int-fix (* x (int-fix y)))
                  (int-fix (* x y)))))

(defthm int-lemma5a
  (implies (and (integerp x)
                (integerp y))
           (equal (int-fix (+ x (int-fix y)))
                  (int-fix (+ x y)))))

; This is a special case of the above.  I need a more general
; handling of this, but this will do for the moment.

(defthm int-lemma5a1
  (implies (and (integerp x1)
                (integerp x2)
                (integerp y))
           (equal (int-fix (+ x1 x2 (int-fix y)))
                  (int-fix (+ x1 x2 y))))
  :hints (("Goal" :use (:instance int-lemma5a (x (+ x1 x2))))))

(defthm int-lemma6
  (implies (intp x)
           (equal (int-fix x) x)))

(in-theory (disable intp int-fix))

(defthm int-lemma4b
  (implies (and (integerp x)
                (integerp y))
           (equal (int-fix (* (int-fix y) x))
                  (int-fix (* y x)))))

(defthm int-lemma5b
  (implies (and (integerp x)
                (integerp y))
           (equal (int-fix (+ (int-fix y) x))
                  (int-fix (+ y x)))))

; Structures

(defthm states
  (and (equal (thread-table (make-state tt h c)) tt)
       (equal (heap (make-state tt h c)) h)
       (equal (class-table (make-state tt h c)) c)))

(in-theory (disable make-state thread-table heap class-table))

(defthm frames
  (and
   (equal (pc (make-frame pc l s prog sync-flg cur-class))
          pc)
   (equal (locals (make-frame pc l s prog sync-flg cur-class))
          l)
   (equal (stack (make-frame pc l s prog sync-flg cur-class))
          s)
   (equal (program (make-frame pc l s prog sync-flg cur-class))
          prog)
   (equal (sync-flg (make-frame pc l s prog sync-flg cur-class))
          sync-flg)
   (equal (cur-class (make-frame pc l s prog sync-flg cur-class))
          cur-class)))

(in-theory
 (disable make-frame pc locals stack program sync-flg cur-class))

(defthm stacks
  (and (equal (top (push x s)) x)
       (equal (pop (push x s)) s)))

(in-theory (disable push top pop))

; Mappings

(defthm assoc-equal-bind
  (equal (assoc-equal key1 (bind key2 val alist))
         (if (equal key1 key2)
             (cons key1 val)
           (assoc-equal key1 alist))))

(defthm bind-bind
  (equal (bind x v (bind x w a))
         (bind x v a)))

; Semi-Ground Terms

(defthm bind-formals-opener
  (implies (and (integerp n)
                (<= 0 n))
           (equal (bind-formals (+ 1 n) stack)
                  (cons (top stack)
                        (bind-formals n (pop stack))))))

(defthm nth-opener
  (and (equal (nth 0 lst) (car lst))
       (implies (and (integerp n)
                     (<= 0 n))
                (equal (nth (+ 1 n) lst)
                       (nth n (cdr lst))))))

(in-theory (disable nth))

(defthm popn-opener
  (implies (and (integerp n)
                (<= 0 n))
           (equal (popn (+ 1 n) stack)
                  (popn n (pop stack)))))

(defun repeat (th n)
  (if (zp n)
      nil
    (cons th (repeat th (- n 1)))))

(defthm repeat-opener
  (implies (and (integerp n)
                (<= 0 n))
           (equal (repeat th (+ 1 n))
                  (cons th (repeat th n)))))

; The nil conjunct below is needed because we will disable run.

(defthm run-opener
  (and (equal (run nil s) s)
       (equal (run (cons th sched) s)
              (run sched (step th s))))
  :hints (("Goal" :in-theory (disable step))))

;(in-theory (enable top pop push lookup-method))

; Step Stuff

(defthm step-opener
  (implies (consp (next-inst th s))
           (equal (step th s)
                  (if (equal (status th s) 'SCHEDULED)
                      (do-inst (next-inst th s) th s)
                    s)))
  :hints (("Goal" :in-theory (disable do-inst))))

(in-theory (disable step))

; Clocks



(defthm run-append
  (equal (run (append sched1 sched2) s)
         (run sched2 (run sched1 s))))
  
(in-theory (disable run))