|
|
|---|
|
|
|
|---|
Specification for the
(ror-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 RCL and RCR instructions only: a zero-bit rotate does nothing, that is affects no flags). For right rotates, the OF flag is set to the exclusive OR of the two most-significant bits of the result.
Function:
(defun ror-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 (ror-spec-8 dst src input-rflags)) (2 (ror-spec-16 dst src input-rflags)) (4 (ror-spec-32 dst src input-rflags)) (8 (ror-spec-64 dst src input-rflags)) (otherwise (mv 0 0 0))))
Theorem:
(defthm natp-mv-nth-0-ror-spec (natp (mv-nth 0 (ror-spec size dst src input-rflags))) :rule-classes :type-prescription)
Theorem:
(defthm n32p-mv-nth-1-ror-spec (unsigned-byte-p 32 (mv-nth 1 (ror-spec size dst src input-rflags))) :rule-classes (:rewrite (:type-prescription :corollary (natp (mv-nth 1 (ror-spec size dst src input-rflags))) :hints (("Goal" :in-theory '(unsigned-byte-p integer-range-p natp)))) (:linear :corollary (and (<= 0 (mv-nth 1 (ror-spec size dst src input-rflags))) (< (mv-nth 1 (ror-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-ror-spec (unsigned-byte-p 32 (mv-nth 2 (ror-spec size dst src input-rflags))) :rule-classes (:rewrite (:type-prescription :corollary (natp (mv-nth 2 (ror-spec size dst src input-rflags))) :hints (("Goal" :in-theory '(unsigned-byte-p integer-range-p natp)))) (:linear :corollary (and (<= 0 (mv-nth 2 (ror-spec size dst src input-rflags))) (< (mv-nth 2 (ror-spec size dst src input-rflags)) 4294967296)) :hints (("Goal" :in-theory '(unsigned-byte-p integer-range-p (:e expt)))))))