		Search-engine friendly clone of the ACL2 documentation.

Jenkins-hash

Jenkins-acc-byte

Signature
(jenkins-acc-byte byte acc) → acc$
Returns: acc$ — Type (unsigned-byte-p 32 acc$).

Definitions and Theorems

Function: jenkins-acc-byte$inline

(defun jenkins-acc-byte$inline (byte acc)
  (declare
       (type (unsigned-byte 8) byte)
       (type (unsigned-byte 32) acc)
       (xargs :type-prescription (natp (jenkins-acc-byte byte acc)))
       (optimize (speed 3) (safety 0)))
  (declare (xargs :guard t))
  (the (unsigned-byte 32)
       (let* ((acc (u32-+ acc byte))
              (acc (u32-+ acc (u32-ash acc 10))))
         (logxor acc (u32-ash acc -6)))))

Theorem: return-type-of-jenkins-acc-byte

(defthm return-type-of-jenkins-acc-byte
  (b* ((acc$ (jenkins-acc-byte$inline byte acc)))
    (unsigned-byte-p 32 acc$))
  :rule-classes :rewrite)