Specification for the
(rol-spec size dst src input-rflags) → (mv * * *)
Source: Intel Manual, Volume 2B, Instruction Set Reference (N-Z).
For the ROL and ROR instructions, the original value of the CF flag is not a part of the result, but the CF flag receives a copy of the bit that was shifted from one end to the other. ... The OF flag is defined only for the 1-bit rotates; it is undefined in all other cases (except ROL and RCR instructions only: a zero-bit rotate does nothing, that is affects no flags). For left rotates, the OF flag is set to the exclusive OR of the CF bit (after the rotate) and the most-significant bit of the result.
Function:
(defun rol-spec$inline (size dst src input-rflags) (declare (type (member 1 2 4 8) size) (type (unsigned-byte 32) input-rflags)) (declare (xargs :guard (and (n06p src) (case size (1 (n08p dst)) (2 (n16p dst)) (4 (n32p dst)) (8 (n64p dst)) (otherwise nil))))) (case size (1 (rol-spec-8 dst src input-rflags)) (2 (rol-spec-16 dst src input-rflags)) (4 (rol-spec-32 dst src input-rflags)) (8 (rol-spec-64 dst src input-rflags)) (otherwise (mv 0 0 0))))
Theorem:
(defthm natp-mv-nth-0-rol-spec (natp (mv-nth 0 (rol-spec size dst src input-rflags))) :rule-classes :type-prescription)
Theorem:
(defthm n32p-mv-nth-1-rol-spec (unsigned-byte-p 32 (mv-nth 1 (rol-spec size dst src input-rflags))) :rule-classes (:rewrite (:type-prescription :corollary (natp (mv-nth 1 (rol-spec size dst src input-rflags))) :hints (("Goal" :in-theory '(unsigned-byte-p integer-range-p natp)))) (:linear :corollary (and (<= 0 (mv-nth 1 (rol-spec size dst src input-rflags))) (< (mv-nth 1 (rol-spec size dst src input-rflags)) 4294967296)) :hints (("Goal" :in-theory '(unsigned-byte-p integer-range-p (:e expt)))))))
Theorem:
(defthm n32p-mv-nth-2-rol-spec (unsigned-byte-p 32 (mv-nth 2 (rol-spec size dst src input-rflags))) :rule-classes (:rewrite (:type-prescription :corollary (natp (mv-nth 2 (rol-spec size dst src input-rflags))) :hints (("Goal" :in-theory '(unsigned-byte-p integer-range-p natp)))) (:linear :corollary (and (<= 0 (mv-nth 2 (rol-spec size dst src input-rflags))) (< (mv-nth 2 (rol-spec size dst src input-rflags)) 4294967296)) :hints (("Goal" :in-theory '(unsigned-byte-p integer-range-p (:e expt)))))))