Semantics of the
We use the 20 bits of the immediate as
the high bits of an unsigned 32-bit integer,
whose low bits are 0.
We write the integer to
Function:
(defun exec32-lui (rd imm stat) (declare (xargs :guard (and (ubyte5p rd) (ubyte20p imm) (state32p stat)))) (let ((__function__ 'exec32-lui)) (declare (ignorable __function__)) (b* ((result (ash (ubyte20-fix imm) 12)) (stat (write32-xreg rd result stat)) (stat (inc32-pc stat))) stat)))
Theorem:
(defthm state32p-of-exec32-lui (b* ((new-stat (exec32-lui rd imm stat))) (state32p new-stat)) :rule-classes :rewrite)
Theorem:
(defthm exec32-lui-of-ubyte5-fix-rd (equal (exec32-lui (ubyte5-fix rd) imm stat) (exec32-lui rd imm stat)))
Theorem:
(defthm exec32-lui-ubyte5-equiv-congruence-on-rd (implies (ubyte5-equiv rd rd-equiv) (equal (exec32-lui rd imm stat) (exec32-lui rd-equiv imm stat))) :rule-classes :congruence)
Theorem:
(defthm exec32-lui-of-ubyte20-fix-imm (equal (exec32-lui rd (ubyte20-fix imm) stat) (exec32-lui rd imm stat)))
Theorem:
(defthm exec32-lui-ubyte20-equiv-congruence-on-imm (implies (acl2::ubyte20-equiv imm imm-equiv) (equal (exec32-lui rd imm stat) (exec32-lui rd imm-equiv stat))) :rule-classes :congruence)
Theorem:
(defthm exec32-lui-of-state32-fix-stat (equal (exec32-lui rd imm (state32-fix stat)) (exec32-lui rd imm stat)))
Theorem:
(defthm exec32-lui-state32-equiv-congruence-on-stat (implies (state32-equiv stat stat-equiv) (equal (exec32-lui rd imm stat) (exec32-lui rd imm stat-equiv))) :rule-classes :congruence)