		Search-engine friendly clone of the ACL2 documentation.

Instruction-semantic-functions

Sarx-spec

Specification for the SARX instruction.

Signature
(sarx-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: sarx-spec$inline

(defun sarx-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 (sarx-spec-32 src cnt))
    (8 (sarx-spec-64 src cnt))
    (otherwise 0)))

Theorem: natp-sarx-spec

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

Subtopics

Sarx-spec-64
Sarx-spec-32