		Search-engine friendly clone of the ACL2 documentation.

Other-non-deterministic-computations

Hw_rnd_gen-logic

Signature
(hw_rnd_gen-logic size x86) → (mv * * x86)

Definitions and Theorems

Function: hw_rnd_gen-logic

(defun hw_rnd_gen-logic (size x86)
  (declare (xargs :stobjs (x86)))
  (declare (type (integer 2 8) size))
  (declare (xargs :guard (or (equal size 2)
                             (equal size 4)
                             (equal size 8))))
  (let ((__function__ 'hw_rnd_gen-logic))
    (declare (ignorable __function__))
    (b* (((mv cf x86) (undef-flg x86))
         ((mv rand x86) (undef-read x86))
         (rand (loghead (ash size 3) rand)))
      (mv cf rand x86))))

Theorem: x86p-of-mv-nth-2-hw_rnd_gen-logic

(defthm x86p-of-mv-nth-2-hw_rnd_gen-logic
  (implies (x86p x86)
           (x86p (mv-nth 2 (hw_rnd_gen-logic size x86)))))