		Search-engine friendly clone of the ACL2 documentation.

Rv64im-le-states

Write64-mem-ubyte64-lendian

Write an unsigned 64-bit little endian integer to memory.

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

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

Definitions and Theorems

Function: write64-mem-ubyte64-lendian

(defun write64-mem-ubyte64-lendian (addr val stat)
  (declare (xargs :guard (and (integerp addr)
                              (ubyte64p val)
                              (state64p stat))))
  (b* ((val (loghead 64 val))
       (b0 (logand val 255))
       (b1 (logand (ash val -8) 255))
       (b2 (logand (ash val -16) 255))
       (b3 (logand (ash val -24) 255))
       (b4 (logand (ash val -32) 255))
       (b5 (logand (ash val -40) 255))
       (b6 (logand (ash val -48) 255))
       (b7 (ash val -56))
       (stat (write64-mem-ubyte8 addr b0 stat))
       (stat (write64-mem-ubyte8 (+ 1 (ifix addr))
                                 b1 stat))
       (stat (write64-mem-ubyte8 (+ 2 (ifix addr))
                                 b2 stat))
       (stat (write64-mem-ubyte8 (+ 3 (ifix addr))
                                 b3 stat))
       (stat (write64-mem-ubyte8 (+ 4 (ifix addr))
                                 b4 stat))
       (stat (write64-mem-ubyte8 (+ 5 (ifix addr))
                                 b5 stat))
       (stat (write64-mem-ubyte8 (+ 6 (ifix addr))
                                 b6 stat))
       (stat (write64-mem-ubyte8 (+ 7 (ifix addr))
                                 b7 stat)))
    stat))

Theorem: state64p-of-write64-mem-ubyte64-lendian

(defthm state64p-of-write64-mem-ubyte64-lendian
  (b* ((new-stat (write64-mem-ubyte64-lendian addr val stat)))
    (state64p new-stat))
  :rule-classes :rewrite)

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

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

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

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

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

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

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

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