		Search-engine friendly clone of the ACL2 documentation.

Implementation

Jenkins-hash

An implementation of Jenkins one-at-a-timehash.

Signature
(jenkins-hash x) → hash
Returns: hash — Type (unsigned-byte-p 32 hash).

This is a non-cryptographic hash function.

The implementation is similar to acl2::fchecksum-obj (see ACL2::checksum) in how we collect input bytes for the hash while walking over the ACL2 object.

Function: jenkins-hash

(defun jenkins-hash (x)
  (declare (xargs :type-prescription (natp (jenkins-hash x)))
           (optimize (speed 3) (safety 0)))
  (declare (xargs :guard t))
  (let ((__function__ 'jenkins-hash))
    (declare (ignorable __function__))
    (the (unsigned-byte 32)
         (let* ((acc (the (unsigned-byte 32)
                          (jenkins-acc-true-list (list x) 0)))
                (acc (u32-+ acc (u32-ash acc 3)))
                (acc (the (unsigned-byte 32)
                          (logxor acc (u32-ash acc -11)))))
           (u32-+ acc (u32-ash acc 15))))))

References

Subtopics

Jenkins-acc-string-nonfixnum-index
Jenkins-acc-string-fixnum-index
Jenkins-acc-true-list
Jenkins-acc-nat
Jenkins-acc-ACL2-number
Jenkins-acc-string
Jenkins-acc-integer
Jenkins-acc-complex-rational
Jenkins-acc-atom
Jenkins-acc-symbol
Jenkins-acc-rational
Jenkins-acc-character
Jenkins-acc-byte
U32-+
U32-ash