;(begin-book t :ttags :all)
(in-package "ACL2S")
(include-book "op-semantics")

; scalerize a vector instruction
(defun scalarize (inst)
;  :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)))

;scalerize the memory [0,pc]
(defun scalarize-mem (pc V)
;  :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)))))))

;; return number of scaler instruction between 0 and pc both including
(defun count-num-scaler-inst (inst)
;  :input-contract (mix-instp inst)
;  :output-contract (natp (count-num-scaler-inst inst))
  (cond ((vecinstp inst)
         2)
        ((instp inst)
         1)
        (t 0)))

; count total number of scalar instruction in [0,pc]
(defun get-num-inst (pc V)
;  :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))))))

;; Refinement map
(defun ref-map (s)
;  :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)
;  :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)
;  :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))))


; define a new run relation to reason about the upto-3-step-relation
(defun spec-run-expanded (s n)
  (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)))))

(defthm 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))))
  :rule-classes nil)

(defun-sk spec-run-expanded-exist (s u)
  (exists n 
    (and (posp n)
         (equal (spec-run-expanded s n) u))))

(acl2s-defaults :set testing-enabled nil)

(defthm 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)))))


(acl2s-defaults :set testing-enabled t)

(defthm get-scaler-inst-contract
  (implies (vecinstp inst)
           (imemp (scalarize inst)))
  :hints (("goal" :in-theory (enable vecinstp instp)))
  :rule-classes :forward-chaining)


(defthm scalarize-contract
  (implies (and (vecimemp vecimem)
                (integerp k))
           (imemp (scalarize (nth k vecimem))))
  :hints (("goal" :in-theory (enable vecinstp instp))))

(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))


(acl2s-defaults :set testing-enabled nil)
(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 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))))

(acl2s-defaults :set testing-enabled nil)

(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 some 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)))))))
  )

 (local (defthm mget-vecimem
          (implies (vecisa-statep s)
                   (vecimemp (vecisa-state-vecinmem s)))
          :hints (("goal" :in-theory (enable vecisa-statep)))
          :rule-classes :forward-chaining))

 (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)))))))
  )

 (local (defthm mget-vecimem
          (implies (vecisa-statep s)
                   (vecimemp (vecisa-state-vecinmem s)))
          :hints (("goal" :in-theory (enable vecisa-statep)))
          :rule-classes :forward-chaining))

 (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
  (defthmd lemma-7-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 (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 lemma-7-aux-k)
             :use ((:instance get-num-inst-scalarize-mem-reduction-+1 (k (mget :prc s)) (vecimem (vecisa-state-vecinmem s)))
                   (:instance lemma-7-aux-k (k (mget :prc s))
                              (vecimem (vecisa-state-vecinmem s)))))))
  )

 (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))

(acl2s-defaults :set testing-enabled nil)


(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 vecinst-or-inst-vecimem 
  (implies (and (vecimemp v)
                (natp k)
                (nth k v)
                (instp (nth k v)))
           (not (vecinstp (nth k v))))
  :hints (("goal" :in-theory (e/d (vecinstp instp) ))))

(defthmd case-exhaustive
  (implies (and (vecimemp v)
                (natp k)
                (nth k v)
                (not (case-1-inst k v)))
           (case-2-inst k v))
  :hints (("subgoal 1" :use ((:instance vecinst-or-inst-vecimem)))))

(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))))


;; Final Theorem
(defthm vector-skipping-refinement-of-scalar
  (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)))))