Partially evaluate read-xreg-unsigned for the RV32I base.
We pick feat-rv32i-le, but we could have picked any of the variants for RV32I.
Function:
(defun read32i-xreg-unsigned{0} (reg stat) (declare (xargs :guard (and (natp reg) (statp stat) (featp (feat-rv32i-le)) (stat-validp stat (feat-rv32i-le)) (< (lnfix reg) (feat->xnum (feat-rv32i-le)))))) (let ((feat (feat-rv32i-le))) (b* ((reg (lnfix reg))) (if (= reg 0) 0 (unsigned-byte-fix (feat->xlen feat) (nth (1- reg) (stat->xregs stat)))))))
Theorem:
(defthm read-xreg-unsigned-becomes-read32i-xreg-unsigned{0} (implies (equal feat (feat-rv32i-le)) (equal (read-xreg-unsigned reg stat feat) (read32i-xreg-unsigned{0} reg stat))) :rule-classes :rewrite)