		Search-engine friendly clone of the ACL2 documentation.

Jenkins-hash

Jenkins-acc-nat

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

Definitions and Theorems

Function: jenkins-acc-nat

(defun jenkins-acc-nat (n acc)
  (declare (type unsigned-byte n)
           (type (unsigned-byte 32) acc)
           (xargs :type-prescription (natp (jenkins-acc-nat n acc)))
           (optimize (speed 3) (safety 0)))
  (declare (xargs :guard t))
  (let ((__function__ 'jenkins-acc-nat))
    (declare (ignorable __function__))
    (if (or (not (mbt (natp n))) (< n *u8-max*))
        (jenkins-acc-byte (the (unsigned-byte 8) n)
                          acc)
      (jenkins-acc-nat (the unsigned-byte (ash n -8))
                       (jenkins-acc-byte (the (unsigned-byte 8)
                                              (logand n *u8-max*))
                                         acc)))))

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

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