		Search-engine friendly clone of the ACL2 documentation.

States64

Read64-mem-ubyte64-lendian

Read an unsigned 64-bit little endian integer from memory.

Signature
(read64-mem-ubyte64-lendian addr stat) → val
Arguments: addr — Guard (integerp addr).; stat — Guard (state64p stat).
Returns: val — Type (ubyte64p val).

This is similar to read64-mem-ubyte16-lendian and read64-mem-ubyte32-lendian, but with 8 bytes instead of 2 or 4.

Definitions and Theorems

Function: read64-mem-ubyte64-lendian

(defun read64-mem-ubyte64-lendian (addr stat)
  (declare (xargs :guard (and (integerp addr) (state64p stat))))
  (let ((__function__ 'read64-mem-ubyte64-lendian))
    (declare (ignorable __function__))
    (b* ((b0 (read64-mem-ubyte8 addr stat))
         (b1 (read64-mem-ubyte8 (+ 1 (ifix addr))
                                stat))
         (b2 (read64-mem-ubyte8 (+ 2 (ifix addr))
                                stat))
         (b3 (read64-mem-ubyte8 (+ 3 (ifix addr))
                                stat))
         (b4 (read64-mem-ubyte8 (+ 4 (ifix addr))
                                stat))
         (b5 (read64-mem-ubyte8 (+ 5 (ifix addr))
                                stat))
         (b6 (read64-mem-ubyte8 (+ 6 (ifix addr))
                                stat))
         (b7 (read64-mem-ubyte8 (+ 7 (ifix addr))
                                stat)))
      (+ b0 (ash b1 8)
         (ash b2 16)
         (ash b3 24)
         (ash b4 32)
         (ash b5 40)
         (ash b6 48)
         (ash b7 56)))))

Theorem: ubyte64p-of-read64-mem-ubyte64-lendian

(defthm ubyte64p-of-read64-mem-ubyte64-lendian
  (b* ((val (read64-mem-ubyte64-lendian addr stat)))
    (ubyte64p val))
  :rule-classes :rewrite)

Theorem: read64-mem-ubyte64-lendian-of-ifix-addr

(defthm read64-mem-ubyte64-lendian-of-ifix-addr
  (equal (read64-mem-ubyte64-lendian (ifix addr)
                                     stat)
         (read64-mem-ubyte64-lendian addr stat)))

Theorem: read64-mem-ubyte64-lendian-int-equiv-congruence-on-addr

(defthm read64-mem-ubyte64-lendian-int-equiv-congruence-on-addr
  (implies (acl2::int-equiv addr addr-equiv)
           (equal (read64-mem-ubyte64-lendian addr stat)
                  (read64-mem-ubyte64-lendian addr-equiv stat)))
  :rule-classes :congruence)

Theorem: read64-mem-ubyte64-lendian-of-state64-fix-stat

(defthm read64-mem-ubyte64-lendian-of-state64-fix-stat
  (equal (read64-mem-ubyte64-lendian addr (state64-fix stat))
         (read64-mem-ubyte64-lendian addr stat)))

Theorem: read64-mem-ubyte64-lendian-state64-equiv-congruence-on-stat

(defthm read64-mem-ubyte64-lendian-state64-equiv-congruence-on-stat
  (implies (state64-equiv stat stat-equiv)
           (equal (read64-mem-ubyte64-lendian addr stat)
                  (read64-mem-ubyte64-lendian addr stat-equiv)))
  :rule-classes :congruence)