		Search-engine friendly clone of the ACL2 documentation.

Instruction-semantic-functions

Shrd-spec

Specification for the SHRD instruction.

Signature
(shrd-spec size dst src cnt input-rflags) → (mv * * * *)

Definitions and Theorems

Function: shrd-spec$inline

(defun shrd-spec$inline (size dst src cnt input-rflags)
  (declare (type (member 2 4 8) size)
           (type (unsigned-byte 32) input-rflags))
  (declare (xargs :guard (and (unsigned-byte-p 6 cnt)
                              (case size
                                (2 (and (n16p dst) (n16p src)))
                                (4 (and (n32p dst) (n32p src)))
                                (8 (and (n64p dst) (n64p src)))
                                (otherwise nil)))))
  (case size
    (2 (shrd-spec-16 dst src cnt input-rflags))
    (4 (shrd-spec-32 dst src cnt input-rflags))
    (8 (shrd-spec-64 dst src cnt input-rflags))
    (otherwise (mv 0 nil 0 0))))

Theorem: natp-mv-nth-0-shrd-spec

(defthm natp-mv-nth-0-shrd-spec
  (natp (mv-nth 0
                (shrd-spec size dst src cnt input-rflags)))
  :rule-classes :type-prescription)

Theorem: booleanp-of-mv-nth-1-shrd-spec

(defthm booleanp-of-mv-nth-1-shrd-spec
  (booleanp (mv-nth 1
                    (shrd-spec size dst src cnt input-rflags))))

Theorem: n32p-mv-nth-2-shrd-spec

(defthm n32p-mv-nth-2-shrd-spec
 (unsigned-byte-p
      32
      (mv-nth 2
              (shrd-spec size dst src cnt input-rflags)))
 :rule-classes
 (:rewrite
  (:type-prescription
      :corollary
      (natp (mv-nth 2
                    (shrd-spec size dst src cnt input-rflags)))
      :hints
      (("Goal" :in-theory '(unsigned-byte-p integer-range-p natp))))
  (:linear
   :corollary
   (and (<= 0
            (mv-nth 2
                    (shrd-spec size dst src cnt input-rflags)))
        (< (mv-nth 2
                   (shrd-spec size dst src cnt input-rflags))
           4294967296))
   :hints
   (("Goal"
        :in-theory '(unsigned-byte-p integer-range-p (:e expt)))))))

Theorem: n32p-mv-nth-3-shrd-spec

(defthm n32p-mv-nth-3-shrd-spec
 (unsigned-byte-p
      32
      (mv-nth 3
              (shrd-spec size dst src cnt input-rflags)))
 :rule-classes
 (:rewrite
  (:type-prescription
      :corollary
      (natp (mv-nth 3
                    (shrd-spec size dst src cnt input-rflags)))
      :hints
      (("Goal" :in-theory '(unsigned-byte-p integer-range-p natp))))
  (:linear
   :corollary
   (and (<= 0
            (mv-nth 3
                    (shrd-spec size dst src cnt input-rflags)))
        (< (mv-nth 3
                   (shrd-spec size dst src cnt input-rflags))
           4294967296))
   :hints
   (("Goal"
        :in-theory '(unsigned-byte-p integer-range-p (:e expt)))))))

Subtopics

Shrd-spec-64
Shrd-spec-32
Shrd-spec-16