		Search-engine friendly clone of the ACL2 documentation.

State-stobj

Read1-instruction{0}

Refine read-instr to use the stobj states.

Definitions and Theorems

Function: read1-instruction{0}

(defun read1-instruction{0} (addr stat feat)
 (declare (xargs :non-executable t))
 (declare
    (xargs :guard (non-exec (and (stat1p stat)
                                 (integerp addr)
                                 (statp (stat-from-stat1 stat))
                                 (featp feat)
                                 (stat-validp (stat-from-stat1 stat)
                                              feat)))))
 (prog2$
  (acl2::throw-nonexec-error 'read1-instruction{0}
                             (list addr stat feat))
  (b* (((unless (acl2::mbt$ (stat1p stat))) 0))
   (let ((addr (loghead (feat->xlen feat) addr))
         (stat (stat-from-stat1 stat)))
     (and (= (mod addr 4) 0)
          (let* ((b0 (read-mem8 addr stat feat))
                 (b1 (read-mem8 (+ addr 1) stat feat))
                 (b2 (read-mem8 (+ addr 2) stat feat))
                 (b3 (read-mem8 (+ addr 3) stat feat)))
            (logapp 8 b0
                    (logapp 8
                            b1 (logapp 8 b2 (logapp 8 b3 0))))))))))

Theorem: read1-instruction{0}-to-read-instr

(defthm read1-instruction{0}-to-read-instr
  (implies (stat1p stat)
           (equal (read1-instruction{0} addr stat feat)
                  (read-instr addr (stat-from-stat1 stat)
                              feat)))
  :rule-classes :rewrite)

Theorem: read-instr-to-read1-instruction{0}

(defthm read-instr-to-read1-instruction{0}
  (implies (statp stat)
           (equal (read-instr addr stat feat)
                  (read1-instruction{0} addr (stat1-from-stat stat)
                                        feat)))
  :rule-classes :rewrite)