		Search-engine friendly clone of the ACL2 documentation.

States32i

Read32i-xreg-unsigned{0}

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.

Definitions and Theorems

Function: read32i-xreg-unsigned{0}

(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: read-xreg-unsigned-becomes-read32i-xreg-unsigned{0}

(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)