		Search-engine friendly clone of the ACL2 documentation.

Jenkins-hash

U32-+

Signature
(u32-+ x y) → product
Returns: product — Type (unsigned-byte-p 32 product).

Definitions and Theorems

Function: u32-+$inline

(defun u32-+$inline (x y)
  (declare (type (unsigned-byte 32) x)
           (type (unsigned-byte 32) y)
           (xargs :type-prescription (natp (u32-+ x y)))
           (optimize (speed 3) (safety 0)))
  (declare (xargs :guard t))
  (the (unsigned-byte 32)
       (logand (+ x y) *u32-max*)))

Theorem: return-type-of-u32-+

(defthm return-type-of-u32-+
  (b* ((product (u32-+$inline x y)))
    (unsigned-byte-p 32 product))
  :rule-classes :rewrite)