		Search-engine friendly clone of the ACL2 documentation.

Rv32im-le-states

Write32-mem-ubyte16-lendian

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

Signature
(write32-mem-ubyte16-lendian addr val stat) → new-stat
Arguments: addr — Guard (integerp addr).; val — Guard (ubyte16p val).; stat — Guard (stat32p stat).
Returns: new-stat — Type (stat32p new-stat).

We decompose the integer into bytes, and we write the low one at the given address, and the high one at the address just after that, which could be 0 if the given address is the last one in the space.

Definitions and Theorems

Function: write32-mem-ubyte16-lendian

(defun write32-mem-ubyte16-lendian (addr val stat)
  (declare (xargs :guard (and (integerp addr)
                              (ubyte16p val)
                              (stat32p stat))))
  (b* ((val (loghead 16 val))
       (b0 (logand val 255))
       (b1 (ash val -8))
       (stat (write32-mem-ubyte8 addr b0 stat))
       (stat (write32-mem-ubyte8 (1+ (ifix addr))
                                 b1 stat)))
    stat))

Theorem: stat32p-of-write32-mem-ubyte16-lendian

(defthm stat32p-of-write32-mem-ubyte16-lendian
  (b* ((new-stat (write32-mem-ubyte16-lendian addr val stat)))
    (stat32p new-stat))
  :rule-classes :rewrite)

Theorem: write32-mem-ubyte16-lendian-of-ifix-addr

(defthm write32-mem-ubyte16-lendian-of-ifix-addr
  (equal (write32-mem-ubyte16-lendian (ifix addr)
                                      val stat)
         (write32-mem-ubyte16-lendian addr val stat)))

Theorem: write32-mem-ubyte16-lendian-int-equiv-congruence-on-addr

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

Theorem: write32-mem-ubyte16-lendian-of-stat32-fix-stat

(defthm write32-mem-ubyte16-lendian-of-stat32-fix-stat
  (equal (write32-mem-ubyte16-lendian addr val (stat32-fix stat))
         (write32-mem-ubyte16-lendian addr val stat)))

Theorem: write32-mem-ubyte16-lendian-stat32-equiv-congruence-on-stat

(defthm write32-mem-ubyte16-lendian-stat32-equiv-congruence-on-stat
 (implies (stat32-equiv stat stat-equiv)
          (equal (write32-mem-ubyte16-lendian addr val stat)
                 (write32-mem-ubyte16-lendian addr val stat-equiv)))
 :rule-classes :congruence)