(in-package "ACL2")

(include-book "system")

; A Non-Cache System

; Now here is an analogous system that does not have any caches.
; Actions take place directly against the memory.  We run events
; analogously, pairing the processor identifier, p, with memory's
; response.

(defun step-mem (action mem)
  (let ((op (car action))
        (addr (cadr action))
        (val (caddr action)))
    (case op
      (READ (mv (fetch addr mem) mem))
      (otherwise ; WRITE
       (mv val (deposit addr val mem))))))

(defun run-mem (events mem)
  (cond ((endp events) nil)
        (t (let ((p (car (car events)))
                 (action (cadr (car events))))
             (mv-let (response mem^)
                     (step-mem action mem)
                     (cons (cons p response)
                           (run-mem (cdr events) mem^)))))))

(defthm mv-nth-0-step-csys
  (implies (and (good-csysp csys)
                (bound p (caches csys)))
           (equal (mv-nth 0 (step-csys p action csys))
                  (mv-nth 0 (step-mem action (mem csys))))))

(defthm mv-nth-1-step-csys
  (implies (and (good-csysp csys)
                (bound p (caches csys)))
           (equal (mem (mv-nth 1 (step-csys p action csys)))
                  (mv-nth 1 (step-mem action (mem csys))))))

(defthm cache-system-correct
  (implies (and (good-csysp csys)
                (appropriate-eventsp events (caches csys)))
           (equal (run-csys events csys)
                  (run-mem events (mem csys))))
  :hints (("Goal"
           :in-theory (disable good-csysp step-csys step-mem))))