		Search-engine friendly clone of the ACL2 documentation.

State-stobj

Read1-memory-unsigned64

Refine read-memory-unsigned64 to use the stobj states.

Definitions and Theorems

Function: read1-memory-unsigned64

(defun read1-memory-unsigned64 (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-memory-unsigned64
                             (list addr stat feat))
  (let ((feat1 (stat1p stat)))
   (cond
    ((acl2::mbt$ feat1)
     (let ((b0 (read-memory-unsigned8 addr (stat-from-stat1 stat)
                                      feat))
           (stat (stat-from-stat1 stat)))
      (let* ((b1 (read-memory-unsigned8 (+ (lifix addr) 1)
                                        stat feat))
             (b2 (read-memory-unsigned8 (+ (lifix addr) 2)
                                        stat feat))
             (b3 (read-memory-unsigned8 (+ (lifix addr) 3)
                                        stat feat))
             (b4 (read-memory-unsigned8 (+ (lifix addr) 4)
                                        stat feat))
             (b5 (read-memory-unsigned8 (+ (lifix addr) 5)
                                        stat feat))
             (b6 (read-memory-unsigned8 (+ (lifix addr) 6)
                                        stat feat))
             (b7 (read-memory-unsigned8 (+ (lifix addr) 7)
                                        stat feat)))
       (cond
        ((feat-little-endianp feat)
         (logapp
          8 b0
          (logapp
           8 b1
           (logapp
            8 b2
            (logapp
             8 b3
             (logapp 8 b4
                     (logapp 8
                             b5 (logapp 8 b6 (logapp 8 b7 0)))))))))
        ((feat-big-endianp feat)
         (logapp
          8 b7
          (logapp
           8 b6
           (logapp
            8 b5
            (logapp
             8 b4
             (logapp 8 b3
                     (logapp 8
                             b2 (logapp 8 b1 (logapp 8 b0 0)))))))))
        (t (acl2::impossible-fn))))))
    (t 0)))))

Theorem: read1-memory-unsigned64-to-read-memory-unsigned64

(defthm read1-memory-unsigned64-to-read-memory-unsigned64
 (implies (stat1p stat)
          (equal (read1-memory-unsigned64 addr stat feat)
                 (read-memory-unsigned64 addr (stat-from-stat1 stat)
                                         feat)))
 :rule-classes :rewrite)

Theorem: read-memory-unsigned64-to-read1-memory-unsigned64

(defthm read-memory-unsigned64-to-read1-memory-unsigned64
  (implies
       (statp stat)
       (equal (read-memory-unsigned64 addr stat feat)
              (read1-memory-unsigned64 addr (stat1-from-stat stat)
                                       feat)))
  :rule-classes :rewrite)