Import acl2_7.4dfsg.orig.tar.gz

[dgit import orig acl2_7.4dfsg.orig.tar.gz]

10 files changed, 2148 insertions, 0 deletions

diff --git a/books/workshops/2015/jain-manolios/support/memory-controller/cert.acl2 b/books/workshops/2015/jain-manolios/support/memory-controller/cert.acl2
new file mode 100644
index 0000000..b3f4f2f
--- /dev/null
+++ b/books/workshops/2015/jain-manolios/support/memory-controller/cert.acl2
@@ -0,0 +1,12 @@
+; Added by Matt K. 1/7/2016, because override-hints aren't supported with
+; waterfall parallelism in ACL2(p).
+(set-waterfall-parallelism nil)
+
+(include-book "acl2s/portcullis" :dir :system)
+(include-book "acl2s/cgen/top" :dir :system :ttags :all)
+(include-book "data-structures/list-defthms" :dir :system)
+
+; cert-flags: ? t :ttags :all
+
+(in-package "ACL2S")
+(acl2s-defaults :set testing-enabled nil)
diff --git a/books/workshops/2015/jain-manolios/support/memory-controller/mem-array-cap-2.lisp b/books/workshops/2015/jain-manolios/support/memory-controller/mem-array-cap-2.lisp
new file mode 100644
index 0000000..f2e53cd
--- /dev/null
+++ b/books/workshops/2015/jain-manolios/support/memory-controller/mem-array-cap-2.lisp
@@ -0,0 +1,278 @@
+; This book contains the model and proof of skipping refinement for
+; memory controller with buffer capacity = 2
+(in-package "ACL2S")
+
+; element in the stack
+(defdata el nat)
+(defdata add nat)
+; memory cell
+(defdata mem (listof nat))
+
+; command
+(defdata req (oneof (list 'read nat)
+                    (list 'write nat el)
+                    (list 'refresh)))
+
+; list of commands
+(defdata reqs (listof req))
+
+(defdata sstate (record (mem-reqs . reqs)
+                        (dmem . mem)
+                        (pt . nat)))
+
+(defun mread (add mem)
+  "memory read"
+  (declare (ignore add))
+  mem)
+
+(defun mwrite (add el mem)
+  "memory write"
+  (update-nth add el mem))
+
+(defun mrefresh-aux (add mem)
+" read each memory location in [1,add] and write it back !!"
+(if (or (zp add) (>= add (len mem)))
+      mem
+    (mrefresh-aux (1- add) (mwrite add (nth add mem) mem))))
+
+ 
+(defun mrefresh (mem)
+  "read location [1, len-1] in the memory and write it back again."
+  (mrefresh-aux (1- (len mem)) mem))
+
+(defthm update-nth-nth-same 
+  (implies (and (natp add) (< add (len mem)))
+           (equal (mwrite add (nth add mem) mem)
+                  mem)))
+
+(defthm mrefresh-aux-mem-unchanged
+  (implies (and (natp add) 
+		(< add (len mem)))
+           (equal (mrefresh-aux add mem)
+                  mem))
+  :hints (("goal" :in-theory (e/d () (mwrite)))))
+
+(defthm mrefresh-mem-unchanged
+  (equal (mrefresh mem)
+         mem))
+
+(in-theory (disable mrefresh))
+
+(defun mem-step (req mem)
+  "returns next state of mem"
+  (let ((op (car req))
+        (add (cadr req)))
+   (cond ((equal op 'read)
+          (mread add mem))
+         ((equal op 'write)
+          (mwrite add (caddr req) mem))
+         ((equal op 'refresh)
+          (mrefresh mem))
+         (t mem))))
+
+(defun spec-step (s)
+  "single step of MEM machine"
+  (let* ((pt (sstate-pt s))
+         (reqs (sstate-mem-reqs s))
+         (req (nth pt reqs))
+         (mem (sstate-dmem s)))
+    (if (reqp req)
+        (sstate reqs (mem-step req mem) (1+ pt))
+      (sstate reqs mem (1+ pt)))))
+
+;; Optimized MEMC implimentation
+
+(defun rbuf-capacity ()
+  "capacity of rbuf"
+  2)
+
+(defun req-buffp (l)
+  (and (reqsp l)
+       (<= (len l) (rbuf-capacity))))
+
+(program)
+(defun nth-req-buff-enum (n)
+  (let ((mem-reqs (nth-reqs n)))
+    (if (<= (len mem-reqs) (rbuf-capacity))
+        mem-reqs
+      (let ((i1 (car mem-reqs))
+            (i2 (cadr mem-reqs))
+            (i3 (caddr mem-reqs)))
+        (list i1 i2 i3)))))
+(logic)
+(verify-guards rbuf-capacity)
+(verify-guards req-buffp)
+(register-custom-type req-buff t nth-req-buff-enum req-buffp)
+
+(defdata istate (record (dmem . mem)
+                        (rbuf . req-buff)
+                        (pt . nat)
+                        (mem-reqs . reqs)))
+
+(defun stutterp (req rbuf)
+" machine stutters if rbuf is not full (number of entries < buffer capacity)
+ and if the req is not 'read or 'refresh'"
+  (and (< (len rbuf) (RBUF-CAPACITY) )
+       (not (equal (car req) 'read))
+       ;; (not (equal (car req) 'refresh))
+       ))
+
+(defun enque (l c)
+  " enque c at the end of list l"
+  (if (endp l)
+      (list c)
+    (cons (car l) (enque (cdr l) c))))
+
+(defun impl-internal-step (req rbuf)
+  "enque req in rbuf"
+  (enque rbuf req))
+
+(defun impl-observable-mem-step (mem rbuf)
+  (cond ((endp rbuf);(equal rbuflen 0)
+          mem)
+         ((endp (cdr rbuf));(equal (len rbuf) 1)
+          (mem-step (car rbuf) mem))
+         ((endp (cddr rbuf));(equal (len rbuf) 2)
+          (let* ((req1 (car rbuf))
+                 (req2 (cadr rbuf))
+                 (op1 (car req1))
+                 (op2 (car req2))
+                 (add1 (cadr req1))
+                 (add2 (cadr req2))
+                 (nxt-mem (if (and (equal op1 'write)
+                                   (equal op2 'write)
+                                   (equal add1 add2))
+                              (mem-step req2 mem)
+                            (mem-step req2 (mem-step req1 mem)))))
+            nxt-mem))
+         ((endp (cdddr rbuf));(equal (len rbuf) 3)
+          (let* ((req1 (car rbuf))
+                 (op1 (car req1))
+                 (add1 (cadr req1))
+                 (req2 (cadr rbuf))
+                 (op2 (car req2))
+                 (add2 (cadr req2))
+                 (req3 (caddr rbuf))
+                 (op3 (car req3))
+                 (add3 (cadr req3))
+                 (nxt-mem (cond ((and (equal op1 'write)
+                                      (equal op2 'write)
+                                      (equal op3 'write)
+                                      (equal add1 add2)
+                                      (equal add2 add3))
+                                 ;; all three reqs are write to the same address
+                                 (mem-step req3 mem))
+                                ((and (equal op1 'write)
+                                      (equal op2 'write)
+                                      (equal add1 add2))
+                                 ;; first two reqs are write to the same address
+                                 (mem-step req3 (mem-step req2 mem)))
+                                ((and (equal op2 'write)
+                                      (equal op3 'write)
+                                      (equal add2 add3))
+                                 (mem-step req3 (mem-step req1 mem)))
+                                 ;; else
+                                (t (mem-step req3 (mem-step req2 (mem-step req1 mem)))))))
+            nxt-mem))))
+
+(defun impl-observable-rbuf-step (req)
+  (if (equal (car req) 'read)
+      nil
+    (list req)))
+
+; single step of buffered stack machine
+(defun impl-step (s)
+  (let* ((mem (mget :dmem s))
+         (rbuf (mget :rbuf s))
+         (reqs (istate-mem-reqs s))
+         (pt (mget :pt s))
+         (req (nth pt reqs)))
+    (if (reqp req)
+        (let ((nxt-mem (if (stutterp req rbuf)
+                           mem
+                         (impl-observable-mem-step mem rbuf)))
+              (nxt-rbuf (if (stutterp req rbuf)
+                            (impl-internal-step req rbuf)
+                          (impl-observable-rbuf-step req)))
+              (nxt-pt (1+ pt)))
+          (istate nxt-mem nxt-rbuf nxt-pt reqs))
+      (let ((nxt-pt (1+ pt))
+            (nxt-rbuf nil) 
+            (nxt-mem (impl-observable-mem-step mem rbuf)))
+        (istate nxt-mem nxt-rbuf nxt-pt reqs)))))
+
+(defun rank (s)
+  (nfix (- (rbuf-capacity) (len (istate-rbuf s)))))
+
+
+(defun commited-state (s)
+  (let ((pt (istate-pt s))
+        (rbuf (istate-rbuf s))
+        (mem-reqs (istate-mem-reqs s))
+        (dmem (istate-dmem s)))
+    (let ((rbuflen (cond ((endp rbuf)
+                          0)
+                         ((endp (cdr rbuf))
+                          1)
+                         ((endp (cddr rbuf))
+                          2))))
+      (istate dmem nil (nfix (- pt rbuflen)) mem-reqs))))
+
+(defun good-statep (s)
+  (let ((pt (istate-pt s))
+        (rbuf (istate-rbuf s)))
+    (and (istatep s)
+         (>= pt (len rbuf))
+         (let* ((cms (commited-state s))
+                (s-cms (cond ((endp rbuf);(equal rbuflen 0)
+                              cms)
+                             ((endp (cdr rbuf));(equal rbuflen 1)
+                              (impl-step cms))
+                             ((endp (cddr rbuf));(equal rbuflen 2)
+                              (impl-step (impl-step cms)))
+                             (t nil))))
+               (equal s-cms s)))))
+
+(defun ref-map (s)
+  (let* ((mem-reqs (istate-mem-reqs s))
+        (dmem (istate-dmem s))
+        (pt (istate-pt s))
+        (rbuf (istate-rbuf s)))
+    (let ((rbuflen (cond ((endp rbuf)
+                          0)
+                         ((endp (cdr rbuf))
+                          1)
+                         ((endp (cddr rbuf))
+                          2))))
+      (sstate mem-reqs dmem (nfix (- pt rbuflen))))))
+
+
+(defun spec-step-skip-rel (w v)
+  "is v reachable from w in <= 5 (= (rbuf-capacity) + 1) steps. Plus 1
+is to account for the case when the current inst is a TOP
+instruction."
+  (or (equal v (spec-step (spec-step w)))
+      (equal v (spec-step (spec-step (spec-step w))))))
+
+(defthm mset-rbuf-nil
+  (equal (mset :rbuf
+               nil (mset :mem-reqs (mget :mem-reqs s) nil))
+         (mset :mem-reqs (mget :mem-reqs s) nil))
+  :hints (("goal" :use (:instance acl2::mset-diff-mset (b :rbuf) (a :mem-reqs) (x (mget :mem-reqs s)) (y nil)
+                                  (r nil))
+           :in-theory (disable acl2::mset-diff-mset))))
+
+
+(defthm optmemc-skip-refines-memc
+  (implies (and (good-statep s)
+                (equal w (ref-map s)); s and r.s are related
+                (equal u (impl-step s)); s --> u
+                (not (equal (ref-map u); not (wfsk2a) r.u is related
+                                       ; to v (where w --> v)
+                            (spec-step w)))
+                (not (and (equal w (ref-map u)); not (wfsk2b) r.s and
+                                               ; r.u are related and
+                                               ; rank decreases
+                          (< (rank u) (rank s)))))
+           (spec-step-skip-rel w (ref-map u)))
+  :hints (("goal" :in-theory (disable reqp))))
diff --git a/books/workshops/2015/jain-manolios/support/memory-controller/mem-array-cap-3.lisp b/books/workshops/2015/jain-manolios/support/memory-controller/mem-array-cap-3.lisp
new file mode 100644
index 0000000..d0ce4e5
--- /dev/null
+++ b/books/workshops/2015/jain-manolios/support/memory-controller/mem-array-cap-3.lisp
@@ -0,0 +1,301 @@
+; This book contains the model and proof of skipping refinement for
+; memory controller with buffer capacity = 3
+
+(in-package "ACL2S")
+
+; element in the stack
+(defdata el nat)
+(defdata add nat)
+; memory cell
+(defdata mem (listof nat))
+
+; command
+(defdata req (oneof (list 'read nat)
+                    (list 'write nat el)
+                    (list 'refresh)))
+
+; list of commands
+(defdata reqs (listof req))
+
+(defdata sstate (record (mem-reqs . reqs)
+                        (dmem . mem)
+                        (pt . nat)))
+
+(defun mread (add mem)
+  "memory read"
+  (declare (ignore add))
+  mem)
+
+(defun mwrite (add el mem)
+  "memory write"
+  (update-nth add el mem))
+
+(defun mrefresh-aux (add mem)
+" read each memory location in [1,add] and write it back !!"
+(if (or (zp add) (>= add (len mem)))
+      mem
+    (mrefresh-aux (1- add) (mwrite add (nth add mem) mem))))
+
+ 
+(defun mrefresh (mem)
+  "read location [1, len-1] in the memory and write it back again."
+  (mrefresh-aux (1- (len mem)) mem))
+
+(defthm update-nth-nth-same 
+  (implies (and (natp add) (< add (len mem)))
+           (equal (mwrite add (nth add mem) mem)
+                  mem)))
+
+(defthm mrefresh-aux-mem-unchanged
+  (implies (and (natp add) 
+		(< add (len mem)))
+           (equal (mrefresh-aux add mem)
+                  mem))
+  :hints (("goal" :in-theory (e/d () (mwrite)))))
+
+(defthm mrefresh-mem-unchanged
+  (equal (mrefresh mem)
+         mem))
+
+(in-theory (disable mrefresh))
+
+(defun mem-step (req mem)
+  "returns next state of mem"
+  (let ((op (car req))
+        (add (cadr req)))
+   (cond ((equal op 'read)
+          (mread add mem))
+         ((equal op 'write)
+          (mwrite add (caddr req) mem))
+         ((equal op 'refresh)
+          (mrefresh mem))
+         (t mem))))
+
+(defun spec-step (s)
+  "single step of MEM machine"
+  (let* ((pt (sstate-pt s))
+         (reqs (sstate-mem-reqs s))
+         (req (nth pt reqs))
+         (mem (sstate-dmem s)))
+    (if (reqp req)
+        (sstate reqs (mem-step req mem) (1+ pt))
+      (sstate reqs mem (1+ pt)))))
+
+;; Optimized MEMC implimentation
+
+(defun rbuf-capacity ()
+  "capacity of rbuf"
+  3)
+
+(defun req-buffp (l)
+  (and (reqsp l)
+       (<= (len l) (rbuf-capacity))))
+
+(program)
+(defun nth-req-buff-enum (n)
+  (let ((mem-reqs (nth-reqs n)))
+    (if (<= (len mem-reqs) (rbuf-capacity))
+        mem-reqs
+      (let ((i1 (car mem-reqs))
+            (i2 (cadr mem-reqs))
+            (i3 (caddr mem-reqs)))
+        (list i1 i2 i3)))))
+(logic)
+(verify-guards rbuf-capacity)
+(verify-guards req-buffp)
+(register-custom-type req-buff t nth-req-buff-enum req-buffp)
+
+(defdata istate (record (dmem . mem)
+                        (rbuf . req-buff)
+                        (pt . nat)
+                        (mem-reqs . reqs)))
+
+(defun stutterp (req rbuf)
+" machine stutters if rbuf is not full (number of entries < buffer capacity)
+ and if the req is not 'read or 'refresh'"
+  (and (< (len rbuf) (RBUF-CAPACITY) )
+       (not (equal (car req) 'read))
+       ;; (not (equal (car req) 'refresh))
+       ))
+
+(defun enque (l c)
+  " enque c at the end of list l"
+  (if (endp l)
+      (list c)
+    (cons (car l) (enque (cdr l) c))))
+
+
+(defthm enque-contract
+  (implies (and (reqp c)
+                (reqsp l))
+           (reqsp (enque l c)))
+   :rule-classes :tau-system)
+
+(defun impl-internal-step (req rbuf)
+  "enque req in rbuf"
+  (enque rbuf req))
+
+(defun impl-observable-mem-step (mem rbuf)
+  (cond ((endp rbuf);(equal rbuflen 0)
+          mem)
+         ((endp (cdr rbuf));(equal (len rbuf) 1)
+          (mem-step (car rbuf) mem))
+         ((endp (cddr rbuf));(equal (len rbuf) 2)
+          (let* ((req1 (car rbuf))
+                 (req2 (cadr rbuf))
+                 (op1 (car req1))
+                 (op2 (car req2))
+                 (add1 (cadr req1))
+                 (add2 (cadr req2))
+                 (nxt-mem (if (and (equal op1 'write)
+                                   (equal op2 'write)
+                                   (equal add1 add2))
+                              (mem-step req2 mem)
+                            (mem-step req2 (mem-step req1 mem)))))
+            nxt-mem))
+         ((endp (cdddr rbuf));(equal (len rbuf) 3)
+          (let* ((req1 (car rbuf))
+                 (op1 (car req1))
+                 (add1 (cadr req1))
+                 (req2 (cadr rbuf))
+                 (op2 (car req2))
+                 (add2 (cadr req2))
+                 (req3 (caddr rbuf))
+                 (op3 (car req3))
+                 (add3 (cadr req3))
+                 (nxt-mem (cond ((and (equal op1 'write)
+                                      (equal op2 'write)
+                                      (equal op3 'write)
+                                      (equal add1 add2)
+                                      (equal add2 add3))
+                                 ;; all three reqs are write to the same address
+                                 (mem-step req3 mem))
+                                ((and (equal op1 'write)
+                                      (equal op2 'write)
+                                      (equal add1 add2))
+                                 ;; first two reqs are write to the same address
+                                 (mem-step req3 (mem-step req2 mem)))
+                                ((and (equal op2 'write)
+                                      (equal op3 'write)
+                                      (equal add2 add3))
+                                 (mem-step req3 (mem-step req1 mem)))
+                                 ;; else
+                                (t (mem-step req3 (mem-step req2 (mem-step req1 mem)))))))
+            nxt-mem))))
+
+(defun impl-observable-rbuf-step (req)
+  (if (equal (car req) 'read)
+      nil
+    (list req)))
+
+; single step of buffered stack machine
+(defun impl-step (s)
+  (let* ((mem (mget :dmem s))
+         (rbuf (mget :rbuf s))
+         (reqs (istate-mem-reqs s))
+         (pt (mget :pt s))
+         (req (nth pt reqs)))
+    (if (reqp req)
+        (let ((nxt-mem (if (stutterp req rbuf)
+                           mem
+                         (impl-observable-mem-step mem rbuf)))
+              (nxt-rbuf (if (stutterp req rbuf)
+                            (impl-internal-step req rbuf)
+                          (impl-observable-rbuf-step req)))
+              (nxt-pt (1+ pt)))
+          (istate nxt-mem nxt-rbuf nxt-pt reqs))
+      (let ((nxt-pt (1+ pt))
+            (nxt-rbuf nil) 
+            (nxt-mem (impl-observable-mem-step mem rbuf)))
+        (istate nxt-mem nxt-rbuf nxt-pt reqs)))))
+
+(defun rank (s)
+  (nfix (- (rbuf-capacity) (len (istate-rbuf s)))))
+
+
+(defun commited-state (s)
+  (let ((pt (istate-pt s))
+        (rbuf (istate-rbuf s))
+        (mem-reqs (istate-mem-reqs s))
+        (dmem (istate-dmem s)))
+    (let ((rbuflen (cond ((endp rbuf)
+                          0)
+                         ((endp (cdr rbuf))
+                          1)
+                         ((endp (cddr rbuf))
+                          2)
+                         ((endp (cdddr rbuf))
+                          3))))
+      (istate dmem nil (nfix (- pt rbuflen)) mem-reqs))))
+
+(defun good-statep (s)
+  (let ((pt (istate-pt s))
+        (rbuf (istate-rbuf s)))
+    (and (istatep s)
+         (>= pt (len rbuf))
+         (let* ((cms (commited-state s))
+                (s-cms (cond ((endp rbuf);(equal rbuflen 0)
+                              cms)
+                             ((endp (cdr rbuf));(equal rbuflen 1)
+                              (impl-step cms))
+                             ((endp (cddr rbuf));(equal rbuflen 2)
+                              (impl-step (impl-step cms)))
+                             ((endp (cdddr rbuf));(equal rbuflen 3)
+                              (impl-step (impl-step (impl-step cms))))
+                             (t nil))))
+               (equal s-cms s)))))
+
+
+(defun ref-map (s)
+  (let* ((mem-reqs (istate-mem-reqs s))
+        (dmem (istate-dmem s))
+        (pt (istate-pt s))
+        (rbuf (istate-rbuf s)))
+    (let ((rbuflen (cond ((endp rbuf)
+                          0)
+                         ((endp (cdr rbuf))
+                          1)
+                         ((endp (cddr rbuf))
+                          2)
+                         ;; ((endp (cdddr rbuf))
+                         ;;  3)
+                         ;; ((endp (cdr (cdddr rbuf)))
+                         ;;  4)
+                         )))
+      (sstate mem-reqs dmem (nfix (- pt rbuflen))))))
+
+
+(defun spec-step-skip-rel (w v)
+  "is v reachable from w in <= 5 (= (rbuf-capacity) + 1) steps. Plus 1
+is to account for the case when the current inst is a TOP
+instruction."
+  (or (equal v (spec-step (spec-step w)))
+      (equal v (spec-step (spec-step (spec-step w))))
+      (equal v (spec-step (spec-step (spec-step (spec-step w)))))))
+
+(defthm mset-rbuf-nil
+  (equal (mset :rbuf
+               nil (mset :mem-reqs (mget :mem-reqs s) nil))
+         (mset :mem-reqs (mget :mem-reqs s) nil))
+  :hints (("goal" :use (:instance acl2::mset-diff-mset (b :rbuf) (a :mem-reqs) (x (mget :mem-reqs s)) (y nil)
+                                  (r nil))
+           :in-theory (disable acl2::mset-diff-mset))))
+
+#|
+; The following form should work.  However, since it
+; takes ~3 hours (in 2015), we comment it and let the
+; interested user submit it themselves.
+ 
+(defthm optmemc-skip-refines-memc
+  (implies (and (good-statep s)
+                (equal w (ref-map s)) ; s and r.s are related
+                (equal u (impl-step s)); s --> u
+                (not (equal (ref-map u); not (wfsk2a) r.u is  related to v (where w --> v)
+                            (spec-step w)))
+                (not (and (equal w (ref-map u)); not (wfsk2b) r.s and
+                                               ; r.u are related and
+                                               ; rank decreases
+                          (< (rank u) (rank s)))))
+           (spec-step-skip-rel w (ref-map u)))
+  :hints (("goal" :in-theory (disable reqp))))
+|#
diff --git a/books/workshops/2015/jain-manolios/support/stack-machine/buffered-stack-cap-2.lisp b/books/workshops/2015/jain-manolios/support/stack-machine/buffered-stack-cap-2.lisp
new file mode 100644
index 0000000..566e8a2
--- /dev/null
+++ b/books/workshops/2015/jain-manolios/support/stack-machine/buffered-stack-cap-2.lisp
@@ -0,0 +1,293 @@
+; This book contains the model and proof of skipping refinement for
+; stack machine with buffer capacity = 3
+
+(in-package "ACL2S")
+
+;; STK 
+(defdata el all)
+
+(defdata stack (listof el))
+
+(defdata inst (oneof (list 'push el)
+                     (list 'pop)
+                     (list 'top)
+                     (list 'nop)))
+
+(defdata inst-mem (listof inst))
+
+;; State of STK machine
+(defdata sstate (record (imem . inst-mem)
+                        (pc . nat)
+                        (stk . stack)))
+
+
+(defun mpush (el stk)
+  "push an element from the stk"
+  (cons el stk))
+
+(defthm mpush-contract
+  (implies (stackp stk)
+           (stackp (mpush el stk)))
+  :rule-classes :tau-system)
+
+(defun mpop (stk)
+  "pop an element from the stk"
+  (cdr stk))
+
+(defthm mpop-contract
+  (implies (stackp stk)
+           (stackp (mpop stk)))
+  :rule-classes :tau-system)
+
+
+(defun mtop (stk)
+  "top leaves the stack unchanged."
+  stk)
+
+
+(defthm mtop-contract
+  (implies (stackp stk)
+           (stackp (mtop stk)))
+  :rule-classes :tau-system)
+
+
+(defun mnop (stk)
+  "no-op instruction"
+  stk)
+
+(defthm mnop-contract
+  (implies (stackp stk)
+           (stackp (mnop stk)))
+  :rule-classes :tau-system)
+
+(defun stk-step-inst (inst stk)
+  "returns next state of stk "
+  (let ((op (car inst)))
+    (cond ((equal op 'push)
+           (mpush (cadr inst) stk ))
+          ((equal op 'pop)
+           (mpop stk))
+          ((equal op 'top)
+           (mtop stk))
+          (t stk))))
+
+(defthm stk-step-inst-contract
+  (implies (and (instp inst)
+                (stackp stk))
+           (stackp (stk-step-inst inst stk)))
+    :rule-classes :tau-system)
+
+
+(defthm push-pop-unchanged
+  (equal (mpop (mpush el stk))
+         stk))
+
+(defthm mnop-unchanged
+  (equal (mnop s)
+         s))
+
+(defthm mtop-unchanged
+  (equal (mtop s)
+         s))
+  
+(in-theory (disable mpush mpop mtop mnop stk-step-inst))
+
+(defun spec-step (s)
+"single step STK machine"
+(let* ((pc (sstate-pc s))
+       (imem (sstate-imem s))
+       (inst (nth pc imem))
+       (stk (sstate-stk s)))
+  (if (instp inst)
+      (sstate imem (1+ pc) (stk-step-inst inst stk))
+    (sstate imem (1+ pc) stk))))
+
+
+;; BSTK Machine (implementation)
+
+(defun ibuf-capacity ()
+  "capacity of ibuf"
+  (declare (xargs :guard t))
+  2)
+
+(defun inst-buffp (l)
+  (and (inst-memp l)
+       (<= (len l) (ibuf-capacity))))
+
+(program)
+(defun nth-inst-buff-enum (n)
+  (let ((imem (nth-inst-mem n)))
+    (if (<= (len imem) (ibuf-capacity))
+        imem
+      (let ((i1 (car imem))
+            (i2 (cadr imem))
+            (i3 (caddr imem)))
+        (list i1 i2 i3)))))
+(logic)
+(verify-guards inst-buffp)
+(register-custom-type inst-buff t nth-inst-buff-enum inst-buffp)
+ 
+;; State of BSTK machine
+(defdata istate
+  (record (imem . inst-mem)
+          (pc . nat)
+          (stk . stack)
+          (ibuf . inst-buff)))
+
+(defun enque (el l)
+  "first in first out"
+  (if (endp l)
+      (list el)
+    (cons (car l) (enque el (cdr l)))))
+
+(defun impl-internal-ibuf-step (inst ibuf)
+  "enque the inst in ibuf"
+  (enque inst ibuf))
+
+(defun impl-observable-stk-step (stk ibuf)
+  "state of the stk when BSTK takes an observable step (i.e. does not
+  stutter) by executing all instructions enqueued in ibuf"
+  (cond ((endp ibuf)
+         stk)
+        ((endp (cdr ibuf))
+         (stk-step-inst (car ibuf) stk))
+        ((endp (cddr ibuf))
+         (let* ((stk (stk-step-inst (car ibuf) stk))
+                (stk (stk-step-inst (cadr ibuf) stk)))
+           stk))
+        ((endp (cdddr ibuf))
+         (let* ((stk (stk-step-inst (car ibuf) stk))
+                (stk (stk-step-inst (cadr ibuf) stk))
+                (stk (stk-step-inst (caddr ibuf) stk)))
+           stk))))
+
+
+(defun impl-observable-ibuf-step (inst)
+  "next state of ibuf when BSTK does not stutter"
+  (if (equal (car inst) 'top)
+      nil
+    (list inst)))
+
+(defun stutterp (inst ibuf)
+  "BSTK stutters if ibuf is not full or the current instruction is not 'top"
+  (and (< (len ibuf) (ibuf-capacity))
+       (not (equal (car inst) 'top))))
+
+
+(defun impl-step (s)
+  "sigle step of BSTK"
+  (let* ((stk (istate-stk s))
+         (ibuf (istate-ibuf s))
+         (imem (istate-imem s))
+         (pc (istate-pc s))
+         (inst (nth pc imem)))
+    (if (instp inst)
+        (let ((nxt-pc (1+ pc))
+              (nxt-stk (if (stutterp inst ibuf)
+                           stk
+                         (impl-observable-stk-step stk ibuf)))
+              (nxt-ibuf (if (stutterp inst ibuf)
+                            (impl-internal-ibuf-step inst ibuf)
+                          (impl-observable-ibuf-step inst))))
+          (istate imem nxt-pc nxt-stk nxt-ibuf))
+      (let ((nxt-pc (1+ pc))
+            (nxt-stk (impl-observable-stk-step stk ibuf))
+            (nxt-ibuf nil))
+        (istate imem nxt-pc nxt-stk nxt-ibuf)))))
+
+(defthm mset-ibuf-nil
+  (equal (mset :ibuf
+               nil (mset :imem (mget :imem s) nil))
+         (mset :imem (mget :imem s) nil))
+  :hints (("goal" :use (:instance acl2::mset-diff-mset (b :ibuf) (a :imem) (x (mget :imem s)) (y nil)
+                                  (r nil))
+           :in-theory (disable acl2::mset-diff-mset))))
+
+(defun commited-state (s)
+  (let* ((stk (istate-stk s))
+         (imem (istate-imem s))
+         (ibuf (istate-ibuf s))
+         (pc (istate-pc s))
+         (cpc (nfix (- pc (len ibuf)))))
+    (istate imem cpc stk nil)))
+
+  
+(defun good-statep (s)
+  "if it is reachable from a commited-state in |ibuf| steps"
+  (let ((pc (istate-pc s))
+        (ibuf (istate-ibuf s)))
+    (and (istatep s)
+         (>= pc (len ibuf))
+         (let* ((cms (commited-state s))
+                (s-cms (cond ((endp ibuf)
+                              cms)
+                             ((endp (cdr ibuf))
+                              (impl-step cms))
+                             ((endp (cddr ibuf))
+                              (impl-step (impl-step cms)))
+                             (t cms))))
+           (equal s-cms s)))))
+  
+
+(defthm good-statep-implies-istatep
+  (implies (good-statep s)
+           (istatep s)))
+
+(defthm commited-state-good-state
+  (implies (good-statep s)
+           (good-statep (commited-state s)))
+  :hints (("goal" :in-theory (e/d (istate istatep)(impl-step)))))
+
+(defthm good-state-inductive
+  (implies (good-statep s)
+           (good-statep (impl-step s)))
+  :hints (("goal" :in-theory (e/d (istatep)(instp)))))
+          
+
+(defun ref-map (s)
+  "refinement map returns the observable state of istate. This version
+assumes the capacity of ibuf = 2"
+  ;(declare (xargs :guard (good-statep s)))
+  (let* ((stk (istate-stk s))
+         (imem (istate-imem s))
+         (pc (istate-pc s))
+         (ibuf (istate-ibuf s))
+         (ibuflen (cond ((endp ibuf)
+                         0)
+                        ((endp (cdr ibuf))
+                         1)
+                        ((endp (cddr ibuf))
+                         2)
+                        (t 0)))
+         (rpc (nfix (- pc ibuflen))))
+    (sstate imem rpc stk)))
+
+(defun rank (s)
+  "rank of an istate s is capacity of ibuf - #inst in ibuf"
+  (nfix (- (ibuf-capacity) (len (istate-ibuf s)))))
+
+
+(defun spec-step-skip-rel (w v)
+  "is v reachable from w in <= 4 (= (ibuf-capacity) + 1) steps. Plus 1
+is to account for the case when the current inst is a TOP
+instruction."
+  (or (equal v (spec-step (spec-step w)))
+      (equal v (spec-step (spec-step (spec-step w))))))
+
+
+;; Final theorem BSTK refines STK
+(defthm bstk-skip-refines-stk
+  (implies (and (good-statep s)
+; s and r.s are related
+                (equal w (ref-map s))
+; s --> u
+                (equal u (impl-step s))
+; (wfsk2a) r.u is related to v (where w --> v)
+                (not (equal (ref-map u)
+                            (spec-step w)))
+; (wfsk2b) r.s and r.u are related and rank decreases
+                (not (and (equal w (ref-map u))
+                          (< (rank u) (rank s)))))
+           (spec-step-skip-rel w (ref-map u)))
+  :hints (("goal" :in-theory (e/d (stk-step-inst) (instp )))))
+
diff --git a/books/workshops/2015/jain-manolios/support/stack-machine/buffered-stack-cap-3.lisp b/books/workshops/2015/jain-manolios/support/stack-machine/buffered-stack-cap-3.lisp
new file mode 100644
index 0000000..d6a0509
--- /dev/null
+++ b/books/workshops/2015/jain-manolios/support/stack-machine/buffered-stack-cap-3.lisp
@@ -0,0 +1,325 @@
+; This book contains the model and proof of skipping refinement for
+; stack machine with buffer capacity = 3
+
+(in-package "ACL2S")
+
+;; STK 
+(defdata el all)
+
+(defdata stack (listof el))
+
+(defdata inst (oneof (list 'push el)
+                     (list 'pop)
+                     (list 'top)
+                     (list 'nop)))
+
+(defdata inst-mem (listof inst))
+
+;; State of STK machine
+(defdata sstate (record (imem . inst-mem)
+                        (pc . nat)
+                        (stk . stack)))
+
+
+(defun mpush (el stk)
+;  :input-contract (stackp stk) (elp el)
+;  :output-contract (stackp (mpush stk el))
+  (cons el stk))
+
+(defthm mpush-contract
+  (implies (stackp stk)
+           (stackp (mpush el stk)))
+  :rule-classes :tau-system)
+
+(defun mpop (stk)
+  "pop an element from the stk"
+;  :input-contract (stackp stk)
+;  :output-contract (stackp (mpop stk))
+  (cdr stk))
+
+(defthm mpop-contract
+  (implies (stackp stk)
+           (stackp (mpop stk)))
+  :rule-classes :tau-system)
+
+
+(defun mtop (stk)
+  "top leaves the stack unchanged."
+;  :input-contract (stackp stk)
+;  :output-contract  (stackp (mtop stk))
+  stk)
+
+
+(defthm mtop-contract
+  (implies (stackp stk)
+           (stackp (mtop stk)))
+  :rule-classes :tau-system)
+
+
+(defun mnop (stk)
+  "no-op instruction"
+;  :input-contract (stackp stk)
+;  :output-contract  (stackp (mnop stk))
+  stk)
+
+(defthm mnop-contract
+  (implies (stackp stk)
+           (stackp (mnop stk)))
+  :rule-classes :tau-system)
+
+(defun stk-step-inst (inst stk)
+  "returns next state of stk "
+; :input-contract (and (instp inst) (stackp stk))
+; :output-contract (stackp (stk-step-inst inst stk))
+  (let ((op (car inst)))
+    (cond ((equal op 'push)
+           (mpush (cadr inst) stk ))
+          ((equal op 'pop)
+           (mpop stk))
+          ((equal op 'top)
+           (mtop stk))
+          (t stk))))
+
+(defthm stk-step-inst-contract
+  (implies (and (instp inst)
+                (stackp stk))
+           (stackp (stk-step-inst inst stk)))
+    :rule-classes :tau-system)
+
+
+(defthm push-pop-unchanged
+  (equal (mpop (mpush el stk))
+         stk))
+
+(defthm mnop-unchanged
+  (equal (mnop s)
+         s))
+
+(defthm mtop-unchanged
+  (equal (mtop s)
+         s))
+  
+(in-theory (disable mpush mpop mtop mnop stk-step-inst))
+
+(defun spec-step (s)
+"single step STK machine"
+;  :input-contract (spec-statep s)
+;  :output-contract (spec-statep (spec-step s))
+(let* ((pc (sstate-pc s))
+       (imem (sstate-imem s))
+       (inst (nth pc imem))
+       (stk (sstate-stk s)))
+  (if (instp inst)
+      (sstate imem (1+ pc) (stk-step-inst inst stk))
+    (sstate imem (1+ pc) stk))))
+
+
+;; BSTK Machine (implementation)
+
+(defun ibuf-capacity ()
+  "capacity of ibuf"
+  (declare (xargs :guard t))
+  3)
+
+(defun inst-buffp (l)
+  (and (inst-memp l)
+       (<= (len l) (ibuf-capacity))))
+
+(program)
+(defun nth-inst-buff-enum (n)
+  (let ((imem (nth-inst-mem n)))
+    (if (<= (len imem) (ibuf-capacity))
+        imem
+      (let ((i1 (car imem))
+            (i2 (cadr imem))
+            (i3 (caddr imem)))
+        (list i1 i2 i3)))))
+(logic)
+(verify-guards inst-buffp)
+(register-custom-type inst-buff t nth-inst-buff-enum inst-buffp)
+ 
+;; State of BSTK machine
+(defdata istate
+  (record (imem . inst-mem)
+          (pc . nat)
+          (stk . stack)
+          (ibuf . inst-buff)))
+
+(defun enque (el l)
+  "first in first out"
+; :input-contract (true-listp l)
+; :output-contract (true-listp (enque el l))
+  (if (endp l)
+      (list el)
+    (cons (car l) (enque el (cdr l)))))
+
+(defun impl-internal-ibuf-step (inst ibuf)
+  "enque the inst in ibuf"
+; :input-contract (and (instp inst) (inst-memp ibuf))
+; :output-contract (inst-memp (impl-internal-ibuf-step inst ibuf))
+  (enque inst ibuf))
+
+(defun impl-observable-stk-step (stk ibuf)
+  "state of the stk when BSTK takes an observable step (i.e. does not
+  stutter) by executing all instructions enqueued in ibuf"
+;  :input-contract (and (stackp stk) (inst-memp ibuf))
+;  :output-contract (stackp (impl-observable-stk-step stk ibuf))
+  (cond ((endp ibuf)
+         stk)
+        ((endp (cdr ibuf))
+         (stk-step-inst (car ibuf) stk))
+        ((endp (cddr ibuf))
+         (let* ((stk (stk-step-inst (car ibuf) stk))
+                (stk (stk-step-inst (cadr ibuf) stk)))
+           stk))
+        ((endp (cdddr ibuf))
+         (let* ((stk (stk-step-inst (car ibuf) stk))
+                (stk (stk-step-inst (cadr ibuf) stk))
+                (stk (stk-step-inst (caddr ibuf) stk)))
+           stk))))
+
+
+(defun impl-observable-ibuf-step (inst)
+  "next state of ibuf when BSTK does not stutter"
+;  :input-contract (instp inst)
+;  :output-contract (instsp (impl-observable-ibuf-step inst))
+  (if (equal (car inst) 'top)
+      nil
+    (list inst)))
+
+(defun stutterp (inst ibuf)
+  "BSTK stutters if ibuf is not full or the current instruction is not 'top"
+;  :input-contract (and (instp inst) (inst-mem cbuf))
+;  :output-contract (booleanp (stutterp inst cbuf))
+  (and (< (len ibuf) (ibuf-capacity))
+       (not (equal (car inst) 'top))))
+
+
+(defun impl-step (s)
+  "sigle step of BSTK"
+;  :input-contract (impl-statep s)
+;  :output-contract (impl-statep (impl-step s))
+  (let* ((stk (istate-stk s))
+         (ibuf (istate-ibuf s))
+         (imem (istate-imem s))
+         (pc (istate-pc s))
+         (inst (nth pc imem)))
+    (if (instp inst)
+        (let ((nxt-pc (1+ pc))
+              (nxt-stk (if (stutterp inst ibuf)
+                           stk
+                         (impl-observable-stk-step stk ibuf)))
+              (nxt-ibuf (if (stutterp inst ibuf)
+                            (impl-internal-ibuf-step inst ibuf)
+                          (impl-observable-ibuf-step inst))))
+          (istate imem nxt-pc nxt-stk nxt-ibuf))
+      (let ((nxt-pc (1+ pc))
+            (nxt-stk (impl-observable-stk-step stk ibuf))
+            (nxt-ibuf nil))
+        (istate imem nxt-pc nxt-stk nxt-ibuf)))))
+
+(defthm mset-ibuf-nil
+  (equal (mset :ibuf
+               nil (mset :imem (mget :imem s) nil))
+         (mset :imem (mget :imem s) nil))
+  :hints (("goal" :use (:instance acl2::mset-diff-mset (b :ibuf) (a :imem) (x (mget :imem s)) (y nil)
+                                  (r nil))
+           :in-theory (disable acl2::mset-diff-mset))))
+
+(defun commited-state (s)
+  (let* ((stk (istate-stk s))
+         (imem (istate-imem s))
+         (ibuf (istate-ibuf s))
+         (pc (istate-pc s))
+         (cpc (nfix (- pc (len ibuf)))))
+    (istate imem cpc stk nil)))
+
+  
+(defun good-statep (s)
+  "if it is reachable from a commited-state in |ibuf| steps"
+  (let ((pc (istate-pc s))
+        (ibuf (istate-ibuf s)))
+    (and (istatep s)
+         (>= pc (len ibuf))
+         (let* ((cms (commited-state s))
+                (s-cms (cond ((endp ibuf)
+                              cms)
+                             ((endp (cdr ibuf))
+                              (impl-step cms))
+                             ((endp (cddr ibuf))
+                              (impl-step (impl-step cms)))
+                             ((endp (cdddr ibuf))
+                              (impl-step (impl-step (impl-step cms))))
+                             (t cms))))
+           (equal s-cms s)))))
+  
+(defthm good-statep-implies-istatep
+  (implies (good-statep s)
+           (istatep s)))
+
+(defthm commited-state-good-state
+  (implies (good-statep s)
+           (good-statep (commited-state s)))
+  :hints (("goal" :in-theory (e/d (istate istatep)(impl-step)))))
+
+(defthm good-state-inductive
+  (implies (good-statep s)
+           (good-statep (impl-step s)))
+  :hints (("goal" :in-theory (e/d (istatep)(instp)))))
+          
+
+(defun ref-map (s)
+  "refinement map returns the observable state of istate. This version
+assumes the capacity of ibuf = 2"
+  ;(declare (xargs :guard (good-statep s)))
+  (let* ((stk (istate-stk s))
+         (imem (istate-imem s))
+         (pc (istate-pc s))
+         (ibuf (istate-ibuf s))
+         (ibuflen (cond ((endp ibuf)
+                         0)
+                        ((endp (cdr ibuf))
+                         1)
+                        ((endp (cddr ibuf))
+                         2)
+                        ((endp (cdddr ibuf))
+                         3)
+                        (t 0)))
+         (rpc (nfix (- pc ibuflen))))
+    (sstate imem rpc stk)))
+
+(defun rank (s)
+  "rank of an istate s is capacity of ibuf - #inst in ibuf"
+  (nfix (- (ibuf-capacity) (len (istate-ibuf s)))))
+
+
+(defun spec-step-skip-rel (w v)
+  "is v reachable from w in <= 4 (= (ibuf-capacity) + 1) steps. Plus 1
+is to account for the case when the current inst is a TOP
+instruction."
+  (or (equal v (spec-step (spec-step w)))
+      (equal v (spec-step (spec-step (spec-step w))))
+      (equal v (spec-step (spec-step (spec-step (spec-step w)))))))
+
+
+;; Final theorem BSTK refines STK
+#|
+; The following form should work.  However, since it
+; takes 3 hours (in 2015), we comment it and let the
+; interested user submit it themselves.
+
+(defthm bstk-skip-refines-stk
+  (implies (and (good-statep s)
+                (equal w (ref-map s)) ; s and r.s are related
+                (equal u (impl-step s)) ; s --> u
+                (not (equal (ref-map u); (wfsk2a) r.u is related to v
+                                       ; (where w --> v)
+                            (spec-step w)))
+                (not (and (equal w (ref-map u)); (wfsk2b) r.s and r.u
+                                               ; are related and rank
+                                               ; decreases
+                          (< (rank u) (rank s)))))
+           (spec-step-skip-rel w (ref-map u)))
+  :hints (("goal" :in-theory (e/d (stk-step-inst) (instp )))))
+
+|#
diff --git a/books/workshops/2015/jain-manolios/support/stack-machine/cert.acl2 b/books/workshops/2015/jain-manolios/support/stack-machine/cert.acl2
new file mode 100644
index 0000000..b3f4f2f
--- /dev/null
+++ b/books/workshops/2015/jain-manolios/support/stack-machine/cert.acl2
@@ -0,0 +1,12 @@
+; Added by Matt K. 1/7/2016, because override-hints aren't supported with
+; waterfall parallelism in ACL2(p).
+(set-waterfall-parallelism nil)
+
+(include-book "acl2s/portcullis" :dir :system)
+(include-book "acl2s/cgen/top" :dir :system :ttags :all)
+(include-book "data-structures/list-defthms" :dir :system)
+
+; cert-flags: ? t :ttags :all
+
+(in-package "ACL2S")
+(acl2s-defaults :set testing-enabled nil)
diff --git a/books/workshops/2015/jain-manolios/support/vectorizing-transformation/cert.acl2 b/books/workshops/2015/jain-manolios/support/vectorizing-transformation/cert.acl2
new file mode 100644
index 0000000..b3f4f2f
--- /dev/null
+++ b/books/workshops/2015/jain-manolios/support/vectorizing-transformation/cert.acl2
@@ -0,0 +1,12 @@
+; Added by Matt K. 1/7/2016, because override-hints aren't supported with
+; waterfall parallelism in ACL2(p).
+(set-waterfall-parallelism nil)
+
+(include-book "acl2s/portcullis" :dir :system)
+(include-book "acl2s/cgen/top" :dir :system :ttags :all)
+(include-book "data-structures/list-defthms" :dir :system)
+
+; cert-flags: ? t :ttags :all
+
+(in-package "ACL2S")
+(acl2s-defaults :set testing-enabled nil)
diff --git a/books/workshops/2015/jain-manolios/support/vectorizing-transformation/data-struct.lisp b/books/workshops/2015/jain-manolios/support/vectorizing-transformation/data-struct.lisp
new file mode 100644
index 0000000..8417bff
--- /dev/null
+++ b/books/workshops/2015/jain-manolios/support/vectorizing-transformation/data-struct.lisp
@@ -0,0 +1,39 @@
+(in-package "ACL2S")
+
+(defdata pc nat)
+(defdata reg nat) 
+(defdata address nat) 
+(defdata data integer) 
+(defdata register-file (oneof nil (acons address data register-file)))
+; no jump, branch and indirect store (consider only a basic block)
+(defdata op-code (enum '(add sub mul)))
+(defdata vec-op-code (enum '(vadd vsub vmul)))
+
+(defdata inst (record (op . op-code)
+                      (rc . reg)
+                      (ra . reg)
+                      (rb . reg)))
+
+  
+(defdata imem (listof inst))
+
+(defdata isa-state (record (prc . pc)
+                           (regs . register-file)
+                           (inmem . imem)))
+
+
+(defdata vecreg (cons reg reg))
+
+(defdata vecinst (record (op . vec-op-code)
+                         (rc . vecreg)
+                         (ra . vecreg)
+                         (rb . vecreg)))
+
+(defdata mix-inst (oneof inst vecinst))
+
+(defdata vecimem (listof mix-inst))
+
+(defdata vecisa-state (record (prc . pc)
+                              (regs . register-file)
+                              (vecinmem . vecimem)))
+
diff --git a/books/workshops/2015/jain-manolios/support/vectorizing-transformation/op-semantics.lisp b/books/workshops/2015/jain-manolios/support/vectorizing-transformation/op-semantics.lisp
new file mode 100644
index 0000000..b5c349f
--- /dev/null
+++ b/books/workshops/2015/jain-manolios/support/vectorizing-transformation/op-semantics.lisp
@@ -0,0 +1,102 @@
+; This file contains semantics for scalar and vector machines.
+
+(in-package "ACL2S")
+(include-book "data-struct")
+
+(defun get-val (r regs)
+  (cdr (assoc r regs)))
+
+(defun add-rc (ra rb rc regs)
+  (put-assoc-eq rc (+ (get-val ra regs)
+              (get-val rb regs))
+        regs))
+
+(defun ISA-add (rc ra rb ISA)
+  (isa-state (1+ (mget :prc ISA))
+             (add-rc ra rb rc (mget :regs ISA))
+             (isa-state-inmem  ISA)))
+
+(defun sub-rc (ra rb rc regs)
+  (put-assoc-eq rc (- (get-val ra regs)
+                      (get-val rb regs))
+                regs))
+
+(defun ISA-sub (rc ra rb ISA)
+  (isa-state (1+ (mget :prc ISA))
+       (sub-rc ra rb rc (mget :regs ISA))
+       (isa-state-inmem  ISA)
+       ))
+
+(defun mul-rc (ra rb rc regs)
+  (put-assoc-eq rc (* (get-val ra regs)
+              (get-val rb regs))
+        regs))
+
+(defun ISA-mul (rc ra rb ISA)
+  (isa-state (1+ (mget :prc ISA))
+       (mul-rc ra rb rc (mget :regs ISA))
+       (isa-state-inmem  ISA)
+       ))
+
+(defun ISA-default (ISA)
+  ISA)
+
+(defun ISA-step (ISA)
+  (let ((inst (nth  (mget :prc ISA) (isa-state-inmem  ISA))))
+   (let ((op (mget  :op inst))
+         (rc (mget  :rc     inst))
+         (ra (mget  :ra     inst))
+         (rb (mget  :rb     inst)))
+    (case op
+      (add       (ISA-add rc ra rb ISA))  ; REGS[rc] := REGS[ra] + REGS[rb]
+      (sub       (ISA-sub rc ra rb ISA))
+      (mul       (ISA-mul rc ra rb ISA))
+      (otherwise (ISA-default ISA))))))
+
+(defun ISA-run (ISA n)
+  (if (zp n)
+      ISA
+      (ISA-run (ISA-step ISA) (- n 1))))
+
+(defun step-vec-reg (inst regs)
+  (let ((opv (mget  :op inst))
+        (rc1 (car (mget :rc inst)))
+        (ra1 (car (mget :ra inst)))
+        (rb1 (car (mget :rb inst)))
+        (rc2 (cdr (mget :rc inst)))
+        (ra2 (cdr (mget :ra inst)))
+        (rb2 (cdr (mget :rb inst))))
+    (case opv
+      (vadd (add-rc ra2 rb2 rc2 
+                    (add-rc ra1 rb1 rc1 regs)))
+      (vsub (sub-rc ra2 rb2 rc2 
+                    (sub-rc ra1 rb1 rc1 regs)))
+      (vmul (mul-rc ra2 rb2 rc2 
+                    (mul-rc ra1 rb1 rc1 regs)))
+      (otherwise regs))))
+
+;; this function is exactly same as isa-step but can potentially be
+;; different in a different implementation. For example, this could be
+;; binary implementation of the operations.
+(defun step-scalar-reg (inst regs)
+  (let* ((op (mget  :op inst))
+         (rc (mget  :rc inst))
+         (ra (mget  :ra inst))
+         (rb (mget  :rb inst)))
+    (case op
+      (add (add-rc ra rb rc regs))  ; REGS[rc] := REGS[ra] + REGS[rb]
+      (sub (sub-rc ra rb rc regs))
+      (mul (mul-rc ra rb rc regs))
+      (otherwise regs))))
+
+(defun step-reg (inst regs)
+  (cond ((vecinstp inst)
+         (step-vec-reg inst regs))
+        (t ;(instp inst)
+         (step-scalar-reg inst regs))))
+
+(defun vecisa-step (s)
+  (let* ((inst (nth (mget :prc s) (vecisa-state-vecinmem s))))
+    (vecisa-state (1+ (mget :prc s))
+                  (step-reg inst (mget :regs s))
+                  (vecisa-state-vecinmem s))))
diff --git a/books/workshops/2015/jain-manolios/support/vectorizing-transformation/scalar-vector.lisp b/books/workshops/2015/jain-manolios/support/vectorizing-transformation/scalar-vector.lisp
new file mode 100644
index 0000000..3c26bcc
--- /dev/null
+++ b/books/workshops/2015/jain-manolios/support/vectorizing-transformation/scalar-vector.lisp
@@ -0,0 +1,774 @@
+; This file contains the proof of skipping simulation theorem for
+; vectorizing compiler transformation
+(in-package "ACL2S")
+(include-book "op-semantics")
+
+(defun scalarize (inst)
+  "scalerize a vector instruction"
+;  :input-contract (mix-instp inst)
+;  :output-contract (imemp (scalarize inst))
+  (cond ((vecinstp inst)
+         (let ((op (mget :op inst))
+               (ra1 (car (mget :ra inst)))
+               (ra2 (cdr (mget :ra inst)))
+               (rb1 (car (mget :rb inst)))
+               (rb2 (cdr (mget :rb inst)))
+               (rc1 (car (mget :rc inst)))
+               (rc2 (cdr (mget :rc inst))))
+          (case op
+            (vadd (list (inst 'add rc1 ra1 rb1)
+                        (inst 'add rc2 ra2 rb2)))
+            (vsub (list (inst 'sub rc1 ra1 rb1)
+                        (inst 'sub rc2 ra2 rb2)))
+            (vmul (list (inst 'mul rc1 ra1 rb1)
+                        (inst 'mul rc2 ra2 rb2))))))
+        ((instp inst) (list inst))
+        (t nil)))
+
+
+(defun scalarize-mem (pc V)
+  "scalerize the memory [0,pc]"
+;  :input-contract (and (natp pc) (vecimemp V))
+;  :output-contract (imemp (scalarize-mem pc V))
+  (if (or (not (integerp pc))
+          (< pc 0))
+      nil
+    (let ((inst (nth pc V)))
+     (cond
+      ((zp pc) ;=0
+       (scalarize inst))
+      (t
+       (append  (scalarize-mem (1- pc) V) (scalarize inst)))))))
+
+(defun count-num-scaler-inst (inst)
+  "return number of scaler instruction between 0 and pc both including"
+;  :input-contract (mix-instp inst)
+;  :output-contract (natp (count-num-scaler-inst inst))
+  (cond ((vecinstp inst)
+         2)
+        ((instp inst)
+         1)
+        (t 0)))
+
+; 
+(defun get-num-inst (pc V)
+  "count total number of scalar instruction in [0,pc]"
+;  :input-contract (and (natp pc) (vecimemp V))
+;  :output-contract (natp (get-num-inst pc V)
+  (let ((inst (nth pc V)))
+   (cond ((or (not (integerp pc))
+              (< pc 0))
+          0)
+         ((zp pc)
+          (count-num-scaler-inst inst))
+         (t (+ (count-num-scaler-inst inst) (get-num-inst (1- pc) V))))))
+
+(defun ref-map (s)
+  "refinement map"
+;  :input-contract (vecisa-statep s)
+;  :output-contract (isa-statep (ref-map s))
+  (let* ((regs (mget :regs s))
+         (V (vecisa-state-vecinmem s))
+         (isapc (get-num-inst (1- (mget :prc s)) V)))
+    (isa-state isapc regs (scalarize-mem (len V) V))))
+
+(defun spec-run-upto-2 (s n)
+  "spec step for n steps"
+;  :input-contract (and (spec-statep s) (natp n))
+;  :output-contract (spec-statep (spec-run-upto-3 s n))
+  (cond ((equal n 1)
+         (isa-step s))
+        ((equal n 2)
+         (isa-step (isa-step s)))
+        (t s)))
+
+(defun spec-run-upto-2-rel (s u)
+  "u is reachable from s in atmost 2 steps"
+;  :input-contract (and (spec-statep s) (spec-statep u))
+;  :output-contract (booleanp (spec-run-upto-3-rel s u))
+  (or (equal (spec-run-upto-2 s 1) u)
+      (equal (spec-run-upto-2 s 2) u)))
+
+; y is reachable from x in one or more steps
+(defun-sk spec-step+ (s u)
+  (exists n
+    (and (posp n)
+         (equal (isa-run s n)
+                u))))
+
+ (defun spec-run-expanded (s n)
+   "define a new run relation to reason about the upto-2-step-relation"
+   (cond ((zp n) s)
+        ((equal n 1) (isa-step s))
+        ((equal n 2) (isa-step (isa-step s)))
+        (t (spec-run-expanded (isa-step s) (1- n)))))
+ 
+(defthmd run-expanded-equivalent-isa-run-n
+  (equal (spec-run-expanded s n)
+         (isa-run s n))
+  :hints (("goal" :induct (isa-run s n)
+           :in-theory (e/d () (isa-step)))))
+
+(defun-sk spec-run-expanded-exist (s u)
+  (exists n 
+    (and (posp n)
+         (equal (spec-run-expanded s n) u))))
+
+
+(defthmd run-expanded-exist-equivalent
+  (implies (spec-run-expanded-exist s u)
+         (spec-step+ s u))
+  :hints (("goal" :use
+           ((:instance  run-expanded-equivalent-isa-run-n
+                        (n (spec-run-expanded-exist-witness
+                            s u)))
+            (:instance spec-run-expanded-exist-suff)
+            (:instance spec-step+-suff (n (spec-run-expanded-exist-witness s u))))
+           :in-theory (e/d () (spec-step+)))))
+
+(defthm finite-step-implies-exists
+  (implies (spec-run-upto-2-rel s u)
+           (spec-run-expanded-exist s u))
+  :hints (("goal" :use ((:instance spec-run-expanded-exist-suff (n 1))
+                        (:instance spec-run-expanded-exist-suff (n 2))
+                        (:instance spec-run-expanded-exist-suff (n 3)))
+           :in-theory (e/d () (isa-step)))))
+
+(defthm finite-step-implies-spec-step-+
+  (implies (spec-run-upto-2-rel s u)
+           (spec-step+ s u))
+  :hints (("goal" :use ((:instance finite-step-implies-exists)
+                        (:instance run-expanded-exist-equivalent)))))
+
+
+(defthm inst-or-vecinst-vecimem
+  (implies (and (vecimemp vecimem)
+                (natp k)
+                (nth k vecimem)
+                (not (instp (nth k vecimem))))
+           (vecinstp (nth k vecimem)))
+  :rule-classes :forward-chaining)
+
+(defthm opcode-case-analysis
+  (implies (and (instp i)
+                (not (equal (mget :op i) 'add))
+                (not (equal (mget :op i) 'sub)))
+           (equal (mget :op i) 'mul))
+  :hints (("goal" :in-theory (enable op-codep instp))))
+
+(defthm nth-=>len 
+  (implies (and (natp j) (>= j (len l)))
+           (null (nth j l))))
+
+(defthm nth-append-l+1
+  (equal (nth (len l) (append l (cons x l2)))
+         x))
+
+
+(encapsulate 
+ ()
+ (local 
+  (defun f-ind (k l)
+    (if (endp l)
+        nil
+      (+ k (f-ind (1- k) (cdr l)))))
+  )
+
+ (defthm nth-app-lemma-2
+   (implies (and (natp k) (> k (len l1))
+                 (true-listp l1) (true-listp l))
+            (equal (nth k (append l1 l))
+                   (nth (- k (len l1)) l)))
+   :hints (("goal" :induct (f-ind k l1)))
+   :rule-classes (:linear :rewrite))
+ )
+
+(encapsulate 
+ ()
+ (local
+  (defun f-ind-1 (k) 
+    (if (zp k)
+        1
+      (1+ (f-ind-1 (1- k)))))
+
+  )
+ (defthm nth-lemma-1
+   (implies (and (vecimemp l) 
+                 (nth k l))
+            (nth (1- k) l))
+   :rule-classes (:forward-chaining :rewrite))
+ )
+
+
+(defthm count-num-scaler-inst->0
+  (implies (and (vecimemp vecimem)
+                (or (instp i)
+                    (vecinstp i)))
+           (> (count-num-scaler-inst i) 0))
+  :rule-classes :linear)
+
+
+(defthm vecopcode-case-analysis
+  (implies (and (vecinstp i)
+                (not (equal (mget :op i) 'vadd))
+                (not (equal (mget :op i) 'vsub)))
+           (equal (mget :op i) 'vmul))
+  :hints (("goal" :in-theory (enable vecinstp vec-op-codep))))
+
+; relate the length after flatten and gen-num-inst  
+(defthm flatten-len-get-num-inst
+  (implies (and (vecimemp vecimem)
+                (integerp k))
+           (equal (get-num-inst k vecimem)
+                  (len (scalarize-mem k vecimem)))))
+
+; lemma for len of scalarize-mem when one more instruction is added
+(defthm len-k-1-flatten-k-vecimem
+  (implies (and (vecimemp vecimem)
+                (integerp k)
+                (not (equal (len (scalarize-mem k vecimem))
+                            (len (scalarize-mem (1- k) vecimem))))
+                (not (equal (len (scalarize-mem k vecimem))
+                            (+ 2 (len (scalarize-mem (1- k) vecimem))))))
+           (equal (len (scalarize-mem k vecimem))
+                  (1+ (len (scalarize-mem (1- k) vecimem)))))
+  :hints (("goal" :use (:instance vecopcode-case-analysis)))
+  :rule-classes (:linear :rewrite))
+
+(defthm len-flatten-case-lemma-inst-+1
+  (implies (and (natp k) 
+                (vecimemp vecimem)
+                (instp (nth k vecimem))
+                (not (vecinstp (nth k vecimem)))
+                )
+           (equal (len (scalarize-mem k vecimem))
+                  (+ 1 (len (scalarize-mem (1- k) vecimem)))))
+  :hints (("goal" :in-theory (disable instp vecimemp))))
+
+(defthm len-flatten-case-lemma-vecinst-+2
+  (implies (and (natp k) 
+                (vecimemp vecimem)
+                (vecinstp (nth k vecimem))
+                )
+           (equal (len (scalarize-mem k vecimem))
+                  (+ 2 (len (scalarize-mem (1- k) vecimem)))))
+  :hints (("goal" :in-theory (disable instp vecimemp))))
+
+
+(encapsulate 
+ ()
+;lemma to move from k to any j >= k in LHS (flatten-1 k vecimem) 
+; in particular k = (len vecimem)
+ (local
+  ; alternate definition of scalarize starting from the first instruction
+  (defun S (L)
+    (if (endp L)
+        nil
+      (append (scalarize (car L)) (S (cdr L)))))
+  )
+
+ (local
+  (defun seg (k L)
+    (if (endp L)
+        nil
+      (if (zp k)
+          (list (car L))
+        (cons (car L)
+              (seg (1- k) (cdr L))))))
+  )
+
+ (local
+  ; relate two definitions of scalerize
+  (defthm S-rel-Scalarize-mem
+    (implies (and (vecimemp V)
+                  (natp k))
+             (equal (scalarize-mem k V)
+                    (S (seg k V))))
+    :hints (("goal" :in-theory (disable scalarize))))
+  )
+
+ (local
+  (defthm full-segment
+    (implies (true-listp L)
+             (equal (seg (len L) L) L)))
+  )
+
+ (local
+  (defun segmentp (X Y)
+    (if (endp X)
+        T
+      (if (endp Y)
+          nil
+        (and (equal (car X) (car Y))
+             (segmentp (cdr X) (cdr Y))))))
+  )
+
+ (local
+  (defthm subset-index-rel
+    (implies (and (true-listp l)
+                  (natp j)
+                  (< j (len l1))
+                  (segmentp l1 l))
+             (equal (nth j l)
+                    (nth j l1))))
+  )
+
+ (local
+  (defthm segments-indexes-rel
+    (implies (and (true-listp l)
+                  (< j (len L)))
+             (segmentp (seg j l) l)))
+  )
+
+ (local
+  (defthm S-sewgf
+    (implies (vecimemp V)
+             (segmentp (S (seg k V)) (S V))))
+  )
+
+ (local
+  (defthm nth-inst-in-alternate-defs-same
+    (implies (and (natp k)
+                  (vecimemp V)
+                  (natp j)
+                  (< j (len (scalarize-mem k V))))
+             (equal (nth j (S V))
+                    (nth j (scalarize-mem k V)))))
+  )
+ 
+ (defthm scalarize-invariant-upto-j
+   (implies (and (natp k)
+                 (vecimemp l)
+                 (< k (len l))
+                 (natp j)
+                 (< j (len (scalarize-mem k l))))
+            (equal (nth j (scalarize-mem (len l) l))
+                   (nth j (scalarize-mem k l)))))
+ )
+
+
+(defthmd get-num-inst-decreases
+  (implies (and (vecimemp vecimem)
+                (natp k)
+                (nth k vecimem))
+           (< (get-num-inst (1- k) vecimem)
+              (get-num-inst k vecimem)))
+  :rule-classes :linear)
+
+(defthmd get-num-inst-scalarize-mem-reduction
+  (implies (and (natp k)
+                (vecimemp vecimem)
+                (nth k vecimem)
+                (< k (len vecimem))
+                )
+           (equal (nth (get-num-inst (1- k) vecimem)
+                       (scalarize-mem (len vecimem) vecimem))
+                  (nth (get-num-inst (1- k) vecimem)
+                       (scalarize-mem k vecimem))))
+  :hints (("goal" :use ((:instance scalarize-invariant-upto-j (j (get-num-inst (1- k) vecimem)) (l vecimem))
+                        (:instance flatten-len-get-num-inst)
+                        (:instance get-num-inst-decreases))
+           :in-theory (disable get-num-inst scalarize-mem
+                               (:rewrite scalarize-invariant-upto-j)
+                               (:rewrite flatten-len-get-num-inst)))))
+
+(defthmd get-num-inst-decreases-1
+  (implies (and (vecimemp vecimem)
+                (natp k)
+                (vecinstp (nth k vecimem)))
+           (< (1+ (get-num-inst (1- k) vecimem))
+              (get-num-inst k vecimem)))
+  :rule-classes :linear)
+
+(defthmd get-num-inst-scalarize-mem-reduction-+1
+  (implies (and (natp k)
+                (vecimemp vecimem)
+                (nth k vecimem)
+                (vecinstp (nth k vecimem))
+                (< k (len vecimem))
+                )
+           (equal (nth (1+ (get-num-inst (1- k) vecimem))
+                       (scalarize-mem (len vecimem) vecimem))
+                  (nth (1+ (get-num-inst (1- k) vecimem))
+                       (scalarize-mem k vecimem))))
+  :hints (("goal" :use ((:instance scalarize-invariant-upto-j (j (1+ (get-num-inst (1- k) vecimem))) (l vecimem))
+                        (:instance flatten-len-get-num-inst)
+                        (:instance get-num-inst-decreases-1))
+           :in-theory (disable get-num-inst count-num-scaler-inst
+                               scalarize-mem
+                               (:rewrite scalarize-invariant-upto-j)
+                               (:rewrite flatten-len-get-num-inst)))))
+
+;; vecimem is mapped to (flatten vecimem) by the refinement map. I
+;; need a relation that relates the instruction executed in the vector
+;; machine at vecpc and the one pointed by the get-num-inst in the
+;; flattened vecimem. Infact, I need to prove that the instruction is
+;; same in case the next instruction to be executed in vector machine
+;; is a scaler instruction and similarly if the next is a vector
+;; instruction then its decomposition is two consecutive scalar
+;; instruction. These obligations are captured in lemma 5,6,7
+(encapsulate
+ ()
+ (local 
+  (defthm lemma-5-main
+  (implies (and (natp k)
+                (vecimemp vecimem)
+                (instp (nth k vecimem))
+                (not (vecinstp (nth k vecimem))))
+           (equal (nth (1- (len (scalarize-mem k vecimem))) (scalarize-mem k vecimem))
+                  (nth k vecimem))))
+)
+ (local
+  (defthmd lemma-5-aux-consp
+    (implies (and (natp k)
+                  (vecimemp vecimem)
+                  (instp (nth k vecimem))
+                  (not (vecinstp (nth k vecimem))))
+             (equal (nth (get-num-inst (1- k) vecimem) ;; number of scaler instruction from [0,k)
+                         (scalarize-mem k vecimem))
+                    (nth k vecimem)))
+    :hints (("goal" :in-theory (disable instp vecinstp vecinst scalarize get-num-inst scalarize-mem vecimemp nth inst)
+             :use ((:instance inst-or-vecinst-vecimem)
+                   (:instance lemma-5-main)
+                   (:instance len-k-1-flatten-k-vecimem)
+                   (:instance flatten-len-get-num-inst)
+                   (:instance len-flatten-case-lemma-inst-+1)))))
+  )
+
+ 
+ (local
+  (defthmd lemma-5-aux-k
+    (implies (and (natp k)
+                  (vecimemp vecimem)
+                  (instp (nth k vecimem))
+                  (not (vecinstp (nth k vecimem))))
+             (equal (nth (get-num-inst (1- k) vecimem)
+                         (scalarize-mem k vecimem))
+                    (nth k vecimem)))
+    :hints (("goal" :in-theory (disable instp inst get-num-inst scalarize-mem vecimemp)
+             :use ((:instance lemma-5-aux-consp))
+             :cases ((null vecimem) (consp vecimem)))))
+  )
+
+ (local
+  (defthmd lemma-5-1
+    (implies (and (vecisa-statep s)
+                  (vecimemp (vecisa-state-vecinmem s))
+                  (instp (nth (mget :prc s) (vecisa-state-vecinmem s)))
+                  (not (vecinstp (nth (mget :prc s) (vecisa-state-vecinmem s))))
+                  (< (mget :prc s) (len (vecisa-state-vecinmem s))))
+             (equal (nth (get-num-inst (1- (mget :prc s)) (vecisa-state-vecinmem s))
+                         (scalarize-mem (len (vecisa-state-vecinmem s))
+                                        (vecisa-state-vecinmem s)))
+                    (nth (mget :prc s) (vecisa-state-vecinmem s))))
+    :hints (("goal"  :in-theory (disable scalarize-mem get-num-inst scalarize inst vecopcode-case-analysis lemma-5-aux-k)
+             :use ((:instance get-num-inst-scalarize-mem-reduction (k (mget :prc s)) (vecimem (vecisa-state-vecinmem s)))
+                   (:instance lemma-5-aux-k (k (mget :prc s))
+                              (vecimem (vecisa-state-vecinmem s)))))))
+
+  )
+ (local
+  (defthmd lemma-5-2
+    (implies (and (vecisa-statep s)
+                  (instp (nth (mget :prc s) (vecisa-state-vecinmem s)))
+                  (not (vecinstp (nth (mget :prc s) (vecisa-state-vecinmem s))))
+                  (>= (mget :prc s) (len (vecisa-state-vecinmem s))))
+             (equal (nth (get-num-inst (1- (mget :prc s)) (vecisa-state-vecinmem s))
+                         (scalarize-mem (len (vecisa-state-vecinmem s))
+                                        (vecisa-state-vecinmem s)))
+                    (nth (mget :prc s) (vecisa-state-vecinmem s))))
+    :hints (("goal" :in-theory (disable scalarize-mem get-num-inst scalarize inst vecopcode-case-analysis lemma-5-aux-k)
+             :use ((:instance nth-=>len (j (mget :prc s)) (l (vecisa-state-vecinmem s)))))))
+  )
+
+ (defthmd lemma-5
+   (implies (and (vecisa-statep s)
+                 (instp (nth (mget :prc s) (vecisa-state-vecinmem s)))
+                 (not (vecinstp (nth (mget :prc s) (vecisa-state-vecinmem s)))))
+            (equal (nth (get-num-inst (1- (mget :prc s)) (vecisa-state-vecinmem s))
+                        (scalarize-mem (len (vecisa-state-vecinmem s))
+                                       (vecisa-state-vecinmem s)))
+                   (nth (mget :prc s) (vecisa-state-vecinmem s))))
+   :hints (("goal" :cases ((>= (mget :prc s) (len (vecisa-state-vecinmem s))) (< (mget :prc s) (len (vecisa-state-vecinmem s))))
+            :in-theory (disable vecinstp instp vecisa-statep scalarize-mem flatten-len-get-num-inst))
+           ("Subgoal 2" :use (:instance lemma-5-2))
+           ("Subgoal 1" :use ((:instance lemma-5-1)))))
+ )
+
+(encapsulate
+ ()
+ ; last but one instruction (= 2- len) in the (scalarize-mem k vecimem) is the same as the
+ ; first instruction on scalerizing the k the instruction in vecimem
+ (local
+  (defthm lemma-main-6
+    (implies (and (natp k)
+                  (vecimemp vecimem)
+                  (vecinstp (nth k vecimem)))
+             (equal (nth (- (len (scalarize-mem k vecimem)) 2) (scalarize-mem k vecimem))
+                    (car (scalarize (nth k vecimem))))))
+  )
+
+ (local
+  (defthmd lemma-6-aux
+    (implies (and (natp k)
+                  (vecimemp vecimem)
+                  (vecinstp (nth k vecimem)))
+             (equal (nth (get-num-inst (1- k) vecimem) ;; number of scaler instruction from [0,k)
+                         (scalarize-mem k vecimem))
+                    (car (scalarize (nth k vecimem)))))
+    :hints (("goal" :in-theory (disable instp vecinstp vecinst scalarize get-num-inst scalarize-mem vecimemp nth inst)
+             :use ((:instance lemma-main-6)))))
+  )
+
+ (local
+  (defthmd lemma-6-aux-k
+    (implies (and (natp k)
+                  (vecimemp vecimem)
+                  (vecinstp (nth k vecimem)))
+             (equal (nth (get-num-inst (1- k) vecimem) ;; number of scaler instruction from [0,k)
+                         (scalarize-mem k vecimem))
+                    (car (scalarize (nth k vecimem)))))
+    :hints (("goal" :in-theory (disable instp inst get-num-inst scalarize-mem vecimemp)
+             :use ((:instance lemma-6-aux))
+             :cases ((null vecimem) (consp vecimem)))))
+  )
+
+ (local
+  (defthmd lemma-6-1
+    (implies (and (vecisa-statep s)
+                  (vecimemp (vecisa-state-vecinmem s))
+                  (vecinstp (nth (mget :prc s) (vecisa-state-vecinmem s)))
+                  (< (mget :prc s) (len (vecisa-state-vecinmem s))))
+             (equal (nth (get-num-inst (1- (mget :prc s)) (vecisa-state-vecinmem s))
+                         (scalarize-mem (len (vecisa-state-vecinmem s))
+                                        (vecisa-state-vecinmem s)))
+                    (car (scalarize (nth (mget :prc s) (vecisa-state-vecinmem s))))))
+    :hints (("goal"  :in-theory (disable scalarize-mem get-num-inst scalarize inst vecopcode-case-analysis)
+             :use ((:instance get-num-inst-scalarize-mem-reduction (k (mget :prc s)) (vecimem (vecisa-state-vecinmem s)))
+                   (:instance lemma-6-aux-k (k (mget :prc s))
+                              (vecimem (vecisa-state-vecinmem s)))))))
+  )
+
+ (local
+  (defthmd lemma-6-2
+    (implies (and (vecisa-statep s)
+                  (vecinstp (nth (mget :prc s) (vecisa-state-vecinmem s)))
+                  (>= (mget :prc s) (len (vecisa-state-vecinmem s))))
+             (equal (nth (get-num-inst (1- (mget :prc s)) (vecisa-state-vecinmem s))
+                         (scalarize-mem (len (vecisa-state-vecinmem s))
+                                        (vecisa-state-vecinmem s)))
+                    (car (scalarize (nth (mget :prc s) (vecisa-state-vecinmem s))))))
+    :hints (("goal" :in-theory (disable scalarize-mem get-num-inst scalarize inst vecopcode-case-analysis)
+             :use ((:instance nth-=>len (j (mget :prc s)) (l (vecisa-state-vecinmem s)))))))
+  )
+
+ (defthmd lemma-6
+    (implies (and (vecisa-statep s)
+                  (vecinstp (nth (mget :prc s) (vecisa-state-vecinmem s))))
+             (equal (nth (get-num-inst (1- (mget :prc s)) (vecisa-state-vecinmem s))
+                         (scalarize-mem (len (vecisa-state-vecinmem s))
+                                        (vecisa-state-vecinmem s)))
+                    (car (scalarize (nth (mget :prc s) (vecisa-state-vecinmem s))))))
+    :hints (("goal" :cases ((>= (mget :prc s) (len (vecisa-state-vecinmem s))) (< (mget :prc s) (len (vecisa-state-vecinmem s))))
+             :in-theory (disable vecinstp instp vecisa-statep scalarize-mem flatten-len-get-num-inst))
+            ("Subgoal 2" :use (:instance lemma-6-2))
+            ("Subgoal 1" :use ((:instance lemma-6-1)))))
+ )
+
+(encapsulate
+ ()
+ ; last instruction (= 1- len) in the (scalarize-mem k vecimem) is the same as the
+ ; first instruction on scalerizing the k the instruction in vecimem
+ (local
+  (defthm lemma-7-main
+    (implies (and (natp k)
+                  (vecimemp vecimem)
+                  (vecinstp (nth k vecimem)))
+             (equal (nth (1- (len (scalarize-mem k vecimem))) (scalarize-mem k vecimem))
+                    (cadr (scalarize (nth k vecimem))))))
+  )
+
+ (local
+  (defthmd lemma-7-aux-consp
+    (implies (and (natp k)
+                  (vecimemp vecimem)
+                  (vecinstp (nth k vecimem)))
+             (equal (nth (1+ (get-num-inst (1- k) vecimem)) ;; number of scaler instruction from [0,k)
+                         (scalarize-mem k vecimem))
+                    (cadr (scalarize (nth k vecimem)))))
+    :hints (("goal" :in-theory (disable instp vecinstp vecinst scalarize get-num-inst scalarize-mem vecimemp nth inst)
+             :use ((:instance lemma-7-main)))))
+  )
+ (local
+  (defthmd lemma-7-aux-k
+    (implies (and (natp k)
+                  (vecimemp vecimem)
+                  (vecinstp (nth k vecimem)))
+             (equal (nth (1+ (get-num-inst (1- k) vecimem)) ;; number of scaler instruction from [0,k)
+                         (scalarize-mem k vecimem))
+                    (cadr (scalarize (nth k vecimem)))))
+    :hints (("goal" :in-theory (disable instp inst get-num-inst scalarize-mem vecimemp)
+             :use ((:instance lemma-7-aux-consp))
+             :cases ((null vecimem) (consp vecimem)))))
+  )
+
+ (local
+  (deftheory my-th
+   '((:rewrite get-num-inst-scalarize-mem-reduction-+1)
+     (:rewrite lemma-7-aux-k))))
+ 
+ (local
+   (defthmd lemma-7-1
+     (implies (and (vecisa-statep s)
+                   (natp (mget :prc s))
+                   (vecimemp (vecisa-state-vecinmem s))
+                   (vecimemp (vecisa-state-vecinmem s))
+                   (nth (mget :prc s) (vecisa-state-vecinmem s))
+                   (vecinstp (nth (mget :prc s) (vecisa-state-vecinmem s)))
+                   (< (mget :prc s) (len (vecisa-state-vecinmem s))))
+              (equal (nth (1+ (get-num-inst (1- (mget :prc s)) (vecisa-state-vecinmem s)))
+                          (scalarize-mem (len (vecisa-state-vecinmem s))
+                                         (vecisa-state-vecinmem s)))
+                     (cadr (scalarize (nth (mget :prc s) (vecisa-state-vecinmem s))))))
+     :hints (("goal" :in-theory (union-theories (theory 'my-th) nil)))))
+    
+ (local
+  (defthmd lemma-7-2
+    (implies (and (vecisa-statep s)
+                  (vecinstp (nth (mget :prc s) (vecisa-state-vecinmem s)))
+                  (>= (mget :prc s) (len (vecisa-state-vecinmem s))))
+             (equal (nth (1+ (get-num-inst (1- (mget :prc s)) (vecisa-state-vecinmem s)))
+                         (scalarize-mem (len (vecisa-state-vecinmem s))
+                                        (vecisa-state-vecinmem s)))
+                    (cadr (scalarize (nth (mget :prc s) (vecisa-state-vecinmem s))))))
+    :hints (("goal" :in-theory (disable scalarize-mem get-num-inst scalarize inst vecopcode-case-analysis)
+             :use ((:instance nth-=>len (j (mget :prc s)) (l (vecisa-state-vecinmem s)))))))
+  )
+ 
+ (defthmd lemma-7
+   (implies (and (vecisa-statep s)
+                 (vecinstp (nth (mget :prc s) (vecisa-state-vecinmem s))))
+            (equal (nth (1+ (get-num-inst (1- (mget :prc s)) (vecisa-state-vecinmem s)))
+                        (scalarize-mem (len (vecisa-state-vecinmem s))
+                                       (vecisa-state-vecinmem s)))
+                   (cadr (scalarize (nth (mget :prc s) (vecisa-state-vecinmem s))))))
+   :hints (("goal" :cases ((>= (mget :prc s) (len (vecisa-state-vecinmem s))) (< (mget :prc s) (len (vecisa-state-vecinmem s))))
+            :in-theory (disable vecinstp instp vecisa-statep scalarize-mem flatten-len-get-num-inst))
+           ("Subgoal 2" :use (:instance lemma-7-2))
+           ("Subgoal 1" :use ((:instance lemma-7-1)))))
+ )
+
+(defun case-inst-1 (s)
+  (equal (mget :op (nth (mget :prc s) (vecisa-state-vecinmem s)))
+         'add))
+
+(defun case-inst-2 (s)
+  (equal (mget :op (nth (mget :prc s) (vecisa-state-vecinmem s)))
+         'sub))
+
+(defun case-inst-3 (s)
+  (equal (mget :op (nth (mget :prc s) (vecisa-state-vecinmem s)))
+         'mul))
+
+(defthm case-inst-exhaustive
+  (implies (and (vecisa-statep s)
+                (instp (nth (mget :prc s) (vecisa-state-vecinmem s)))
+                (not (case-inst-1 s))
+                (not (case-inst-2 s)))
+           (case-inst-3 s))
+  :hints (("goal" :in-theory (enable instp))))
+
+(in-theory (disable flatten-len-get-num-inst))
+
+(defthm simulation-inst
+  (implies (and (vecisa-statep s)
+                (instp (nth (mget :prc s) (vecisa-state-vecinmem s)))
+                (equal (vecisa-step s) u)
+                (equal w (ref-map s))
+                )
+           (equal (isa-step w)
+                  (ref-map u)))
+  :hints (("goal" :use ((:instance lemma-5)
+                        (:instance case-inst-exhaustive))
+           :cases ((case-inst-1 s) (case-inst-2 s) (case-inst-3 s)))))
+
+(defun case-vinst-1 (s)
+  (equal (mget :op (nth (mget :prc s) (vecisa-state-vecinmem s)))
+         'vadd))
+
+(defun case-vinst-2 (s)
+  (equal (mget :op (nth (mget :prc s) (vecisa-state-vecinmem s)))
+         'vsub))
+
+(defun case-vinst-3 (s)
+  (equal (mget :op (nth (mget :prc s) (vecisa-state-vecinmem s)))
+         'vmul))
+
+(defthm case-vecinst-exhaustive
+  (implies (and (vecisa-statep s)
+                (vecinstp (nth (mget :prc s) (vecisa-state-vecinmem s)))
+                (not (case-vinst-1 s))
+                (not (case-vinst-2 s)))
+           (case-vinst-3 s))
+  :hints (("goal" :in-theory (enable vecinstp))))
+
+(in-theory (disable vecopcode-case-analysis add-rc sub-rc mul-rc))
+
+(defthm simulation-vecinst
+  (implies (and (vecisa-statep s)
+                (vecinstp (nth (mget :prc s) (vecisa-state-vecinmem s)))
+                (equal (vecisa-step s) u)
+                (equal w (ref-map s)))
+           (equal (isa-step (isa-step w))
+                  (ref-map u)))
+  :hints (("goal"   :use ((:instance case-vecinst-exhaustive)
+                          (:instance lemma-6)
+                          (:instance lemma-7))
+           :cases ((case-vinst-1 s) (case-vinst-2 s) (case-vinst-3 s)))))
+
+(defun case-1-inst (k v)
+  (and (vecinstp (nth k v))
+       (not (instp (nth k v)))))
+
+(defun case-2-inst (k v)
+  (and (not (vecinstp (nth k v)))
+       (instp (nth k v))))
+
+
+(defthmd case-exhaustive
+  (implies (and (vecimemp v)
+                (natp k)
+                (nth k v)
+                (not (case-1-inst k v)))
+           (case-2-inst k v)))
+
+(in-theory (disable simulation-vecinst simulation-inst vecisa-step
+                    vecisa-statep isa-step ref-map ))
+                
+(defthm impl-simulates-vecinst-run-lemma
+  (implies (and (vecisa-statep s)
+                (nth (mget :prc s) (vecisa-state-vecinmem s))
+                (equal (vecisa-step s) u)
+                (equal w (ref-map s)))
+           (spec-run-upto-2-rel w (ref-map u)))
+  :hints (("goal" :cases ((case-1-inst (mget :prc s) (vecisa-state-vecinmem s))
+                          (case-2-inst (mget :prc s) (vecisa-state-vecinmem s)))
+           :use ((:instance case-exhaustive (k (mget :prc s)) (v (vecisa-state-vecinmem s))))
+           )
+          ("subgoal 3" :in-theory (disable case-1-inst case-2-inst))
+          ("subgoal 1" :use (:instance simulation-inst))
+          ("subgoal 2" :use (:instance simulation-vecinst))))
+
+
+(defthm impl-simulates-spec
+  (implies (and (vecisa-statep s)
+                (vecisa-statep u)
+                (isa-statep w)
+                (isa-statep (ref-map u))
+                (equal w (ref-map s))
+                (nth (mget :prc s) (vecisa-state-vecinmem s))
+                (equal (vecisa-step s) u))
+           (spec-step+ (ref-map s) (ref-map u)))
+  :hints (("goal" :use ((:instance finite-step-implies-exists 
+                                   (s (ref-map s)) (u (ref-map u)))
+                        (:instance impl-simulates-vecinst-run-lemma)))))