(in-package "ACL2")

; The following general function recognizes when x is an association
; list in which all the keys are unique.  That is, x is a true list (a
; list ending in nil) of pairs and the car of every pair occurs as the
; car of no other pair in the list.

(defun bound (x alist)
  (cond ((endp alist) nil)
        ((equal x (car (car alist))) t)
        (t (bound x (cdr alist)))))
  
(defun fetch (x alist)
  (cond ((endp alist) nil)
        ((equal x (car (car alist))) (cdr (car alist)))
        (t (fetch x (cdr alist)))))

(defun unique-keysp (x)
  (cond ((endp x) (equal x nil))
        ((and (consp (car x))
              (not (bound (car (car x)) (cdr x))))
         (unique-keysp (cdr x)))
        (t nil)))

(defun deposit (addr val mem)
  (cond ((endp mem) (list (cons addr val)))
        ((equal addr (caar mem)) (cons (cons addr val) (cdr mem)))
        (t (cons (car mem) (deposit addr val (cdr mem))))))

; The three functions before that are subsidiary concepts
; used in that definition.  Their names suggest their behaviors.

(defun cache-okp (cache mem)
  (cond ((endp cache) t)
        ((caddr (car cache))
         (and (equal (cadr (car cache)) (fetch (car (car cache)) mem))
              (cache-okp (cdr cache) mem)))
        (t (cache-okp (cdr cache) mem))))

(defun every-cache-okp (caches mem)
  (cond ((endp caches) t)
        (t (and (cache-okp (cdr (car caches))
                           mem)
                (every-cache-okp (cdr caches) mem)))))

(defun every-cache-unique-keysp (caches)
  (cond ((endp caches) t)
        (t (and (unique-keysp (cdr (car caches)))
                (every-cache-unique-keysp (cdr caches))))))

(defun every-other-cache-okp (p caches mem)
  (cond ((endp caches) t)
        ((equal p (car (car caches)))
         (every-other-cache-okp p (cdr caches) mem))
        (t (and (cache-okp (cdr (car caches))
                           mem)
                (every-other-cache-okp p (cdr caches) mem)))))

(defun appropriate-eventsp (events caches)
  (cond ((endp events) t)
        ((bound (car (car events)) caches)
         (appropriate-eventsp (cdr events) caches))
        (t nil)))
         
(defthm cache-okp-implies-mem-agreement
  (implies (and (cache-okp cache mem)
                (cadr (fetch addr cache)))
           (iff (equal (car (fetch addr cache))
                       (fetch addr mem))
                t)))

(defthm every-cache-okp-implies-cache-okp
  (implies (and (bound p caches)
                (every-cache-okp caches mem))
           (cache-okp (fetch p caches)
                      mem)))

(defthm every-cache-okp-deposit
  (implies (and (cache-okp cache mem)
                (unique-keysp caches)
                (every-other-cache-okp p caches mem))
           (every-cache-okp (deposit p cache caches)
                            mem)))

(defthm bound-deposit
  (equal (bound addr1 (deposit addr2 val mem))
         (or (equal addr1 addr2)
             (bound addr1 mem))))

(defthm fetch-deposit
  (equal (fetch addr1 (deposit addr2 val mem))
         (if (equal addr1 addr2)
             val
           (fetch addr1 mem))))

(defthm cache-okp-deposit1
  (implies (and (cache-okp cache mem)
                (unique-keysp cache)
                (not (bound addr cache)))
           (cache-okp cache (deposit addr val mem))))
           
(defthm cache-okp-deposit2
  (implies (and (cache-okp cache mem)
                (unique-keysp cache))
           (cache-okp
            (deposit addr (list any nil) cache)
            (deposit addr val mem))))

(defthm cache-okp-deposit3
  (implies (and (cache-okp cache mem)
                (unique-keysp cache)
                (not (cadr (fetch addr cache))))
           (cache-okp cache
                      (deposit addr val mem))))  

(defthm unique-keysp-deposit
  (implies (unique-keysp cache)
           (unique-keysp (deposit addr val cache))))

(defthm every-cache-unique-keysp-deposit
  (implies (and (unique-keysp caches)
                (every-cache-unique-keysp caches)
                (unique-keysp cache))
           (every-cache-unique-keysp (deposit p cache caches))))

(defthm every-cache-unique-keysp-implies-unique-keysp
  (implies (and (unique-keysp caches)
                (every-cache-unique-keysp caches)
                (bound p caches))
           (unique-keysp (fetch p caches))))

(defthm cache-okp-deposit4
  (implies (and (unique-keysp cache)
                (cache-okp cache mem))
           (cache-okp (deposit addr (list val t) cache)
                      (deposit addr val mem))))

(defthm cache-okp-deposit
  (implies (and (unique-keysp cache)
                (equal val (fetch addr mem))
                (cache-okp cache mem))
           (cache-okp (deposit addr (list val t) cache)
                      mem)))
           
(defthm deposit-fetch
  (implies (and (unique-keysp caches)
                (bound p caches))
           (equal (deposit p
                           (fetch p caches)
                           caches)
                  caches)))

(defthm appropriate-eventsp-deposit
  (implies (appropriate-eventsp events caches)
           (appropriate-eventsp events (deposit p cache caches))))