(in-package "ACL2")

(include-book "misc/defpun" :dir :system)

(in-theory (disable nfix))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

;;; We define a very simple machine.  The state consists of a program
;;; counter stack, a program, and a memory.  The instructions are
;;; loadi, add, mult, sub, ifgt, ifodd, goto, call, ret, nop, and spin.

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

;;; The state is modeled as a list.

;;; The pc-stack is stored in the car of st.

(defun get-pc-stack (st)
  (car st))

(defun get-pc (st)
  (car (get-pc-stack st)))

(defun set-pc (pc st)
    (cons (cons pc (cdr (get-pc-stack st)))
          (cdr st)))

(defun push-pc (pc st)
    (cons (cons pc (get-pc-stack st))
          (cdr st)))

(defun pop-pc (st)
    (cons (cdr (get-pc-stack st))
          (cdr st)))

;;; The program is stored in the cadr of st.  It consists of a list of
;;; (pc <inst>) pairs.

(defun get-program (st)
  (cadr st))

(defun get-inst-aux (pc program)
  (cond ((endp program)
         '(spin))
        ((equal pc (car (car program)))
         (cadr (car program)))
        (t
         (get-inst-aux pc (cdr program)))))

(defun get-inst (st)
  (get-inst-aux (get-pc st) (get-program st)))

(defun program-loaded-p (program st)
  (if (endp program)
      t
    (and (equal (get-inst-aux (car (car program)) (get-program st))
                (cadr (car program)))
         (program-loaded-p (cdr program) st))))

;;; The cddr of st is the memory.  We regard this as a linear,
;;; zero-based, layout of the memory.

(defun get-memory (st)
  (cddr st))

(defun get-addr-aux (index mem)
  (if (zp index) 
      (car mem)
    (get-addr-aux (+ -1 index) (cdr mem))))

(defun get-addr (addr st)
  (get-addr-aux addr (get-memory st)))

(defun set-addr-aux (index val mem)
  (if (zp index)
      (cons val (cdr mem))
    (cons (car mem) 
          (set-addr-aux (+ -1 index) val (cdr mem)))))

(defun set-addr (addr val st)
  (cons (car st)
        (cons (get-program st)
              (set-addr-aux addr val (get-memory st)))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(defthm len-get-pc-stack-set-pc
  (implies (consp (get-pc-stack st))
           (equal (len (get-pc-stack (set-pc pc st)))
                  (len (get-pc-stack st)))))

(defthm len-get-pc-stack-push-pc
  (implies (consp (get-pc-stack st))
           (equal (len (get-pc-stack (push-pc pc st)))
                  (+ 1 (len (get-pc-stack st))))))

(defthm len-get-pc-stack-pop-pc
  (implies (consp (get-pc-stack st))
           (equal (len (get-pc-stack (pop-pc st)))
                  (+ -1 (len (get-pc-stack st))))))

(defthm len-get-pc-stack-set-addr
  (equal (len (get-pc-stack (set-addr addr val st)))
         (len (get-pc-stack st))))

(defthm consp-get-pc-stack-set-pc
  (consp (get-pc-stack (set-pc pc st))))

(defthm consp-get-pc-stack-push-pc
  (consp (get-pc-stack (push-pc pc st))))

(defthm consp-get-pc-stack-set-addr
  (equal (consp (get-pc-stack (set-addr addr val st)))
         (consp (get-pc-stack st))))

(defthm len-get-memory-set-pc
  (equal (len (get-memory (set-pc pc st)))
         (len (get-memory st))))

(defthm len-get-memory-push-pc
  (equal (len (get-memory (push-pc pc st)))
         (len (get-memory st))))

(defthm len-get-memory-pop-pc
  (equal (len (get-memory (pop-pc st)))
         (len (get-memory st))))

(encapsulate ()

 (local
  (defthm helper-0
    (implies t
    (equal (LEN (SET-ADDR-AUX ADDR VAL NIL))
           (+ 1 (nfix addr))))
    :hints (("Goal" :expand ((SET-ADDR-AUX 1 VAL NIL))
                    :in-theory (enable nfix)))))

 (local
  (defthm helper-1
    (equal (len (set-addr-aux addr val mem))
         (max (len mem)
              (+ 1 (nfix addr))))
    :hints (("Goal" :in-theory (enable nfix)))))

(defthm len-get-memory-set-addr
  (equal (len (get-memory (set-addr addr val st)))
         (max (len (get-memory st))
              (+ 1 (nfix addr)))))
)

;;; get/set of same type:

(defthm set-pc-set-pc
  (equal (set-pc pc1 (set-pc pc2 st))
         (set-pc pc1 st)))

(defthm get-pc-set-pc
  (equal (get-pc (set-pc pc st))
         pc))

(defthm get-pc-push-pc
  (equal (get-pc (push-pc pc st))
         pc))

(defthm get-pc-pop-pc-set-addr
  (equal (get-pc (pop-pc (set-addr addr val st)))
         (get-pc (pop-pc st))))

(defthm pop-pc-push-pc
  (implies (consp st)
           (equal (pop-pc (push-pc pc st))
                  st)))

(defthm pop-pc-set-pc
  (equal (pop-pc (set-pc pc st))
         (pop-pc st)))

(defthm get-addr-set-addr-same
  (implies (equal addr1 addr2)
           (equal (get-addr addr1 (set-addr addr2 val st))
                  val))
  :otf-flg t)

(encapsulate ()

  (local
   (defthm helper-1
     (IMPLIES (AND (INTEGERP ADDR2)
                   (< 0 ADDR2))
              (EQUAL (CAR (SET-ADDR-AUX ADDR2 VAL st))
                     (CAR ST)))))

  (local
   (defthm helper-2
     (IMPLIES (AND (INTEGERP ADDR1)
                   (<= 0 ADDR1)
                   (INTEGERP ADDR2)
                   (<= 0 ADDR2)
                   (NOT (EQUAL ADDR1 ADDR2)))
              (EQUAL (GET-ADDR-AUX ADDR1 (SET-ADDR-AUX ADDR2 VAL st))
                     (GET-ADDR-AUX ADDR1 st)))))

  (defthm get-addr-set-addr-different
    (implies (not (equal (nfix addr1) (nfix addr2)))
             (equal (get-addr addr1 (set-addr addr2 val st))
                    (get-addr addr1 st)))
    :hints (("Goal" :in-theory (enable nfix)))
    :otf-flg t)

)

(encapsulate ()

 (local
  (defthm helper-1
    (IMPLIES (< (nfix ADDR) (LEN mem))
         (EQUAL (SET-ADDR-AUX ADDR (GET-ADDR-AUX ADDR mem)
                              mem)
                mem))
    :hints (("Goal" :in-theory (enable nfix)))))

 (local
  (defthm helper-2
    (implies (< (nfix addr) (len (get-memory st)))
             (equal (set-addr addr (get-addr addr st) st)
                    st))))

 (defthm set-get-crock
   (implies (and (< (nfix addr) (len (get-memory big-st)))
                 (equal (get-addr addr st)
                        (get-addr addr big-st)))
            (equal (set-addr addr (get-addr addr st) big-st)
                   big-st))
   :hints (("Goal" :in-theory (disable get-addr set-addr get-memory get-program))))
)

(encapsulate ()

  (local
   (defthm helper-1
     (IMPLIES (NOT (EQUAL (nfix ADDR1) (nfix ADDR2)))
         (EQUAL (SET-ADDR-AUX ADDR2 VAL2
                              (SET-ADDR-AUX ADDR1 VAL1 mem))
                (SET-ADDR-AUX ADDR1 VAL1
                              (SET-ADDR-AUX ADDR2 VAL2 mem))))
     :hints (("Goal" :in-theory (enable nfix)))))

  (defthm set-addr-set-add-diff
    (implies (not (equal (nfix addr1) (nfix addr2)))
             (equal (set-addr addr2 val2 (set-addr addr1 val1 st))
                    (set-addr addr1 val1 (set-addr addr2 val2 st))))
    :rule-classes ((:rewrite :loop-stopper ((addr2 addr1)))))
)

;;; get/set of different type:

(defthm get-pc-set-addr
  (equal (get-pc (set-addr addr val st))
         (get-pc st)))

(defthm get-pc-stack-pop-pc-set-addr
  (EQUAL (GET-PC-STACK (POP-PC (SET-ADDR addr val st)))
         (GET-PC-STACK (POP-PC ST))))

(defthm get-addr-set-pc
  (equal (get-addr addr (set-pc pc st))
         (get-addr addr st)))

(defthm get-addr-push-pc
  (equal (get-addr addr (push-pc pc st))
         (get-addr addr st)))

(defthm get-addr-pop-pc
  (equal (get-addr addr (pop-pc st))
         (get-addr addr st)))

(defthm get-program-set-pc
  (equal (get-program (set-pc pc st))
         (get-program st)))

(defthm program-loaded-p-set-pc
  (equal (program-loaded-p prog (set-pc pc st))
         (program-loaded-p prog st)))

(defthm get-program-push-pc
  (equal (get-program (push-pc pc st))
         (get-program st)))

(defthm program-loaded-p-push-pc
  (equal (program-loaded-p prog (push-pc pc st))
         (program-loaded-p prog st)))

(defthm get-program-pop-pc
  (equal (get-program (pop-pc st))
         (get-program st)))

(defthm program-loaded-p-pop-pc
  (equal (program-loaded-p prog (pop-pc st))
         (program-loaded-p prog st)))

(defthm get-program-set-addr
  (equal (get-program (set-addr addr val st))
         (get-program st)))

(defthm program-loaded-p-set-addr
  (equal (program-loaded-p prog (set-addr addr val st))
         (program-loaded-p prog st)))

;;; Functional nesting order:
;;; (set-pc push-pc) set-addr

(defthm set-addr-set-pc
  (equal (set-addr addr val (set-pc pc st))
         (set-pc pc (set-addr addr val st))))

(defthm set-addr-push-pc
  (equal (set-addr addr val (push-pc pc st))
         (push-pc pc (set-addr addr val st))))

(defthm set-addr-set-addr-same
  (implies (equal addr1 addr2)
           (equal (set-addr addr1 val1 (set-addr addr2 val2 st))
                  (set-addr addr1 val1 st)))
  :otf-flg t)

;;; get-inst openers

(defthm get-inst-aux-opener
  (implies (and (syntaxp (quotep pc))
                (syntaxp (quotep program)))
           (equal (get-inst-aux pc program)
                  (cond ((endp program)
                         '(spin))
                        ((equal pc (car (car program)))
                         (cadr (car program)))
                        (t
                         (get-inst-aux pc (cdr program)))))))

(defthm get-inst-opener
  (implies (and (syntaxp (quotep (mfc-rw `(get-pc ,st) '? nil mfc state))))
           (equal (get-inst st)
                  (get-inst-aux (get-pc st) (get-program st)))))
                  

(in-theory (disable get-pc-stack
                    get-pc 
                    set-pc 
                    push-pc
                    pop-pc
                    get-program
                    get-inst get-inst-aux
                    get-memory
                    get-addr get-addr-aux
                    set-addr set-addr-aux))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

;;; Having dealt with the state, we now move on to define the
;;; instructions

(defun inc-pc (st)
  (set-pc (+ 1 (get-pc st)) st))

(defun loadi (addr val st)
  ;; We load val (presumably a constant) into addr
  (inc-pc (set-addr addr val st)))

(defun add (addr1 addr2 st)
  ;; We add the values in addr1 and addr2, and store the result in
  ;; addr1.
  (inc-pc (set-addr addr1 
                    (+ (get-addr addr1 st) (get-addr addr2 st))
                    st)))

(defun sub (addr1 addr2 st)
  ;; We subtract the value in addr2 from that in addr1, and store the
  ;; result in addr1.
  (inc-pc (set-addr addr1 
                    (- (get-addr addr1 st) (get-addr addr2 st))
                    st)))

(defun mult (addr1 addr2 st)
  ;; We multiply the values in addr1 and addr2, and store the result
  ;; in addr1.
  (inc-pc (set-addr addr1 
                    (* (get-addr addr1 st) (get-addr addr2 st))
                    st)))

(defun ifgt (addr1 addr2 pc st)
  ;; If addr1 > addr2, we jump to pc.
  ;; Note that test below is negation of test in op.
  (if (<= (get-addr addr1 st)
          (get-addr addr2 st))
      (inc-pc st)
    (set-pc pc st)))

(defun ifodd (addr pc st)
  ;; If the value in addr is odd, we jump to pc.
  (if (oddp (get-addr addr st))
      (set-pc pc st)
    (inc-pc st)))

(defun goto (pc st)
  ;; We set the pc to pc
  (set-pc pc st))

(defun call (pc st)
  (push-pc pc (inc-pc st)))

(defun ret (st)
  (pop-pc st))

(defun nop (st)
  (inc-pc st))

(defun spin (st)
  ;; Don't just do something, sit there.
  st)

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(defun next (st)
  (let* ((inst (get-inst st))
         (op-code (car inst))
         (op1 (cadr inst))
         (op2 (caddr inst))
         (op3 (cadddr inst)))
    (case op-code
      (loadi (loadi op1 op2 st))
      (add (add op1 op2 st))
      (sub (sub op1 op2 st))
      (mult (mult op1 op2 st))
      (ifgt (ifgt op1 op2 op3 st))
      (ifodd (ifodd op1 op2 st))
      (goto (goto op1 st))
      (call (call op1 st))
      (ret (ret st))
      (spin (spin st))
      (nop (nop st))
      (otherwise st))))

(defthm next-opener
  (implies (syntaxp (quotep (mfc-rw `(get-inst ,st) '? nil mfc state)))
           (equal (next st)
                  (let* ((inst (get-inst st))
                         (op-code (car inst))
                         (op1 (cadr inst))
                         (op2 (caddr inst))
                         (op3 (cadddr inst)))
                    (case op-code
                          (loadi (loadi op1 op2 st))
                          (add (add op1 op2 st))
                          (sub (sub op1 op2 st))
                          (mult (mult op1 op2 st))
                          (ifgt (ifgt op1 op2 op3 st))
                          (ifodd (ifodd op1 op2 st))
                          (goto (goto op1 st))
                          (call (call op1 st))
                          (ret (ret st))
                          (spin (spin st))
                          (nop (nop st))
                          (otherwise st))))))

(in-theory (disable next))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(defun run (st n)
  (if (zp n)
      st
    (run (next st) (+ -1 n))))

(defthm run-opener
  (implies (syntaxp (quotep n))
           (equal (run st n)
                  (if (zp n)
                      st
                    (run (next st) (+ -1 n))))))

(defun c+ (x y)
  (+ x y))

(defthm run-c+-opener
  (implies (and (natp n1)
                (natp n2))
           (equal (run st (c+ n1 n2))
                  (run (run st n1) n2))))

(defthm natp-c+
  (implies (and (natp n1)
                (natp n2))
           (natp (c+ n1 n2))))

(defthm get-program-run
  (equal (get-program (run st n))
         (get-program st))
  :hints (("Goal" :in-theory (enable next
                                     get-program
                                     set-pc set-addr pop-pc push-pc))))

(defthm program-loaded-p-run
  (equal (program-loaded-p x (run st n))
         (program-loaded-p x st))
  :hints (("Goal" :in-theory (disable run))))

(in-theory (disable run
                    c+ (:executable-counterpart c+)))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(defun cutpointp (pc list)
  (member pc list))

;;; Why does this not work?
#|
(defpun nextcutpoint (st list)
  (if (cutpointp (get-pc st) list)
      st
    (nextcutpoint (next st)))
  :hints (("Goal" :in-theory (enable nfix))))
|#

(encapsulate ()

  (local (in-theory (enable nfix)))

  (defpun next-cutpoint (st list)
    (if (cutpointp (get-pc st) list)
        st
      (next-cutpoint (next st) list)))

)

;;; The next two theorems replace the traditional run ``opener''
;;; theorem.

(defthm next-cutpoint-1
  (implies (cutpointp (get-pc st) list) 
           (equal (next-cutpoint st list)
                  st)))

(defthm next-cutpoint-2
  (implies (not (cutpointp (get-pc st) list))
           (equal (next-cutpoint st list)
                  (next-cutpoint (next st) list)))
  :hints (("Goal"
           :in-theory (disable cutpointp next))))
      
;;; For efficiency
(in-theory (disable next-cutpoint-def))

(defun equal-cutpoints (st0 st1 list)
  (and (cutpointp (get-pc st0) list)
       (equal (get-pc st0) (get-pc st1))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(defthm equal-nfix-x-pos-int-const
  (implies (and (syntaxp (quotep c))
                (integerp c)
                (< 0 c))
           (equal (equal (nfix x) c)
                  (equal x c)))
  :hints (("Goal" :in-theory (enable nfix))))

(defthm equal-nfix-x-non-int-const
  (implies (and (syntaxp (quotep c))
                (not (integerp c)))
           (not (equal (nfix x) c)))
  :hints (("Goal" :in-theory (enable nfix))))

(defthm equal-nfix-x-neg-const
  (implies (and (syntaxp (quotep c))
                (< c 0))
           (not (equal (nfix x) c)))
  :hints (("Goal" :in-theory (enable nfix))))