		Search-engine friendly clone of the ACL2 documentation.

State-stobj

Read1-mem16{0}

Refine read-mem16 to use the stobj states.

Definitions and Theorems

Function: read1-mem16{0}

(defun read1-mem16{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-mem16{0}
                                    (list addr stat feat))
         (let ((feat1 (stat1p stat)))
           (cond ((acl2::mbt$ feat1)
                  (let ((b0 (read-mem8 addr (stat-from-stat1 stat)
                                       feat))
                        (stat (stat-from-stat1 stat)))
                    (let ((b1 (read-mem8 (+ (lifix addr) 1)
                                         stat feat)))
                      (cond ((feat-little-endianp feat)
                             (logapp 8 b0 (logapp 8 b1 0)))
                            ((feat-big-endianp feat)
                             (logapp 8 b1 (logapp 8 b0 0)))
                            (t (acl2::impossible-fn))))))
                 (t 0)))))

Theorem: read1-mem16{0}-to-read-mem16

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

Theorem: read-mem16-to-read1-mem16{0}

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