Read an unsigned 32-bit little endian integer from memory.
This is similar to read32-mem-ubyte16-lendian, but with 4 bytes instead of 2.
Function:
(defun read32-mem-ubyte32-lendian (addr stat) (declare (xargs :guard (and (integerp addr) (state32p stat)))) (let ((__function__ 'read32-mem-ubyte32-lendian)) (declare (ignorable __function__)) (b* ((b0 (read32-mem-ubyte8 addr stat)) (b1 (read32-mem-ubyte8 (+ 1 (ifix addr)) stat)) (b2 (read32-mem-ubyte8 (+ 2 (ifix addr)) stat)) (b3 (read32-mem-ubyte8 (+ 3 (ifix addr)) stat))) (+ b0 (ash b1 8) (ash b2 16) (ash b3 24)))))
Theorem:
(defthm ubyte32p-of-read32-mem-ubyte32-lendian (b* ((val (read32-mem-ubyte32-lendian addr stat))) (ubyte32p val)) :rule-classes :rewrite)
Theorem:
(defthm read32-mem-ubyte32-lendian-of-ifix-addr (equal (read32-mem-ubyte32-lendian (ifix addr) stat) (read32-mem-ubyte32-lendian addr stat)))
Theorem:
(defthm read32-mem-ubyte32-lendian-int-equiv-congruence-on-addr (implies (acl2::int-equiv addr addr-equiv) (equal (read32-mem-ubyte32-lendian addr stat) (read32-mem-ubyte32-lendian addr-equiv stat))) :rule-classes :congruence)
Theorem:
(defthm read32-mem-ubyte32-lendian-of-state32-fix-stat (equal (read32-mem-ubyte32-lendian addr (state32-fix stat)) (read32-mem-ubyte32-lendian addr stat)))
Theorem:
(defthm read32-mem-ubyte32-lendian-state32-equiv-congruence-on-stat (implies (state32-equiv stat stat-equiv) (equal (read32-mem-ubyte32-lendian addr stat) (read32-mem-ubyte32-lendian addr stat-equiv))) :rule-classes :congruence)