|
|
|---|
|
|
|
|---|
Specification for the
(rcl-spec size dst src input-rflags) → (mv * * *)
Source: Intel Manual, Volume 2B, Instruction Set Reference (N-Z).
The RCL instruction shifts the CF flag into the least-significant bit and shifts the most-significant bit into the CF flag. ... 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 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 rcl-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 (rcl-spec-8 dst src input-rflags)) (2 (rcl-spec-16 dst src input-rflags)) (4 (rcl-spec-32 dst src input-rflags)) (8 (rcl-spec-64 dst src input-rflags)) (otherwise (mv 0 0 0))))
Theorem:
(defthm natp-mv-nth-0-rcl-spec (natp (mv-nth 0 (rcl-spec size dst src input-rflags))) :rule-classes :type-prescription)
Theorem:
(defthm n32p-mv-nth-1-rcl-spec (unsigned-byte-p 32 (mv-nth 1 (rcl-spec size dst src input-rflags))) :rule-classes (:rewrite (:type-prescription :corollary (natp (mv-nth 1 (rcl-spec size dst src input-rflags))) :hints (("Goal" :in-theory '(unsigned-byte-p integer-range-p natp)))) (:linear :corollary (and (<= 0 (mv-nth 1 (rcl-spec size dst src input-rflags))) (< (mv-nth 1 (rcl-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-rcl-spec (unsigned-byte-p 32 (mv-nth 2 (rcl-spec size dst src input-rflags))) :rule-classes (:rewrite (:type-prescription :corollary (natp (mv-nth 2 (rcl-spec size dst src input-rflags))) :hints (("Goal" :in-theory '(unsigned-byte-p integer-range-p natp)))) (:linear :corollary (and (<= 0 (mv-nth 2 (rcl-spec size dst src input-rflags))) (< (mv-nth 2 (rcl-spec size dst src input-rflags)) 4294967296)) :hints (("Goal" :in-theory '(unsigned-byte-p integer-range-p (:e expt)))))))