		Search-engine friendly clone of the ACL2 documentation.

Instruction-semantic-functions

Shrx-spec

Specification for the SHRX instruction.

Signature
(shrx-spec size src cnt) → *
Arguments: cnt — Guard (unsigned-byte-p 6 cnt).

Since this instruction does not affect the flags, this function does not take or return flags.

Definitions and Theorems

Function: shrx-spec$inline

(defun shrx-spec$inline (size src cnt)
  (declare (type (member 4 8) size))
  (declare (xargs :guard (unsigned-byte-p 6 cnt)))
  (declare (xargs :guard
                  (case size
                    (4 (n32p src))
                    (8 (n64p src))
                    (otherwise nil))))
  (case size
    (4 (shrx-spec-32 src cnt))
    (8 (shrx-spec-64 src cnt))
    (otherwise 0)))

Theorem: natp-shrx-spec

(defthm natp-shrx-spec
  (natp (shrx-spec size src cnt))
  :rule-classes :type-prescription)

Subtopics

Shrx-spec-64
Shrx-spec-32