		Search-engine friendly clone of the ACL2 documentation.

Two-byte-opcodes

X86-rdrand

Signature
(x86-rdrand proc-mode start-rip temp-rip prefixes rex-byte opcode modr/m sib x86) → x86
Returns: x86 — Type (x86p x86), given (x86p x86).

Note from the Intel Manual (March 2017, Vol. 1, Section 7.3.17):

Under heavy load, with multiple cores executing RDRAND in parallel, it is possible, though unlikely, for the demand of random numbers by software processes or threads to exceed the rate at which the random number generator hardware can supply them. This will lead to the RDRAND instruction returning no data transitorily. The RDRAND instruction indicates the occurrence of this rare situation by clearing the CF flag.

See Intel's Digital Random Number Generator Guide for more details.

Definitions and Theorems

Function: x86-rdrand

(defun x86-rdrand
       (proc-mode start-rip temp-rip
                  prefixes rex-byte opcode modr/m sib x86)
 (declare (xargs :stobjs (x86)))
 (declare (type (integer 0 4) proc-mode)
          (type (signed-byte 48) start-rip)
          (type (signed-byte 48) temp-rip)
          (type (unsigned-byte 52) prefixes)
          (type (unsigned-byte 8) rex-byte)
          (type (unsigned-byte 8) opcode)
          (type (unsigned-byte 8) modr/m)
          (type (unsigned-byte 8) sib))
 (declare (ignorable proc-mode start-rip temp-rip
                     prefixes rex-byte opcode modr/m sib))
 (declare (xargs :guard (and (prefixes-p prefixes)
                             (modr/m-p modr/m)
                             (sib-p sib)
                             (rip-guard-okp proc-mode temp-rip))))
 (let ((__function__ 'x86-rdrand))
  (declare (ignorable __function__))
  (b* ((?ctx 'x86-rdrand)
       (?r/m (the (unsigned-byte 3)
                  (modr/m->r/m modr/m)))
       (?mod (the (unsigned-byte 2)
                  (modr/m->mod modr/m)))
       (?reg (the (unsigned-byte 3)
                  (modr/m->reg modr/m))))
    (b*
      (((the (integer 1 8) operand-size)
        (select-operand-size proc-mode nil
                             rex-byte nil prefixes nil nil nil x86))
       ((mv cf rand x86)
        (hw_rnd_gen operand-size x86))
       ((when (ms x86))
        (!!ms-fresh :x86-rdrand (ms x86)))
       ((when (or (not (unsigned-byte-p 1 cf))
                  (not (unsigned-byte-p (ash operand-size 3)
                                        rand))))
        (!!ms-fresh :x86-rdrand-ill-formed-outputs (ms x86)))
       (x86 (!rgfi-size operand-size (reg-index reg rex-byte 2)
                        rand rex-byte x86))
       (x86 (let* ((x86 (!flgi :cf cf x86))
                   (x86 (!flgi :pf 0 x86))
                   (x86 (!flgi :af 0 x86))
                   (x86 (!flgi :zf 0 x86))
                   (x86 (!flgi :sf 0 x86))
                   (x86 (!flgi :of 0 x86)))
              x86))
       (x86 (write-*ip proc-mode temp-rip x86)))
      x86))))

Theorem: x86p-of-x86-rdrand

(defthm x86p-of-x86-rdrand
  (implies
       (x86p x86)
       (b* ((x86 (x86-rdrand proc-mode start-rip temp-rip prefixes
                             rex-byte opcode modr/m sib x86)))
         (x86p x86)))
  :rule-classes :rewrite)