		Search-engine friendly clone of the ACL2 documentation.

Missing-parents

Movbe-reverse-bytes

Reverse the bytes in an operand of a given byte size.

Signature
(movbe-reverse-bytes val size) → rev-val
Arguments: val — Guard (unsigned-byte-p (* 8 size) val).; size — Guard (natp size).
Returns: rev-val — Type (unsigned-byte-p (* 8 size) rev-val), given the guard.

Definitions and Theorems

Function: movbe-reverse-bytes

(defun movbe-reverse-bytes (val size)
  (declare (xargs :guard (and (natp size)
                              (unsigned-byte-p (* 8 size) val))))
  (let ((__function__ 'movbe-reverse-bytes))
    (declare (ignorable __function__))
    (cond ((zp size) 0)
          (t (logapp (* 8 (1- size))
                     (movbe-reverse-bytes (logtail 8 val)
                                          (1- size))
                     (loghead 8 val))))))

Theorem: return-type-of-movbe-reverse-bytes

(defthm return-type-of-movbe-reverse-bytes
  (implies (and (natp size)
                (unsigned-byte-p (binary-* '8 size)
                                 val))
           (b* ((rev-val (movbe-reverse-bytes val size)))
             (unsigned-byte-p (* 8 size) rev-val)))
  :rule-classes :rewrite)