		Search-engine friendly clone of the ACL2 documentation.

States32

Write32-mem-ubyte32-lendian

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

Signature
(write32-mem-ubyte32-lendian addr val stat) → new-stat
Arguments: addr — Guard (integerp addr).; val — Guard (ubyte32p val).; stat — Guard (state32p stat).
Returns: new-stat — Type (state32p new-stat).

This is similar to write32-mem-ubyte16-lendian, but with 4 bytes instead of 2.

Definitions and Theorems

Function: write32-mem-ubyte32-lendian

(defun write32-mem-ubyte32-lendian (addr val stat)
  (declare (xargs :guard (and (integerp addr)
                              (ubyte32p val)
                              (state32p stat))))
  (let ((__function__ 'write32-mem-ubyte32-lendian))
    (declare (ignorable __function__))
    (b* ((val (ubyte32-fix val))
         (b0 (logand val 255))
         (b1 (logand (ash val -8) 255))
         (b2 (logand (ash val -16) 255))
         (b3 (ash val -24))
         (stat (write32-mem-ubyte8 addr b0 stat))
         (stat (write32-mem-ubyte8 (+ 1 (ifix addr))
                                   b1 stat))
         (stat (write32-mem-ubyte8 (+ 2 (ifix addr))
                                   b2 stat))
         (stat (write32-mem-ubyte8 (+ 3 (ifix addr))
                                   b3 stat)))
      stat)))

Theorem: state32p-of-write32-mem-ubyte32-lendian

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

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

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

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

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

Theorem: write32-mem-ubyte32-lendian-of-ubyte32-fix-val

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

Theorem: write32-mem-ubyte32-lendian-ubyte32-equiv-congruence-on-val

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

Theorem: write32-mem-ubyte32-lendian-of-state32-fix-stat

(defthm write32-mem-ubyte32-lendian-of-state32-fix-stat
  (equal (write32-mem-ubyte32-lendian addr val (state32-fix stat))
         (write32-mem-ubyte32-lendian addr val stat)))

Theorem: write32-mem-ubyte32-lendian-state32-equiv-congruence-on-stat

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