		Search-engine friendly clone of the ACL2 documentation.

Cryptography

Hash160

Hash160 function.

Signature
(hash160 bytes) → hash
Arguments: bytes — Guard (byte-listp bytes).
Returns: hash — Type (byte-listp hash).

This is SHA-256 followed by RIPEMD-160. It is sometimes called `Hash160', e.g. see the OP_HASH160 opcode, or see the documentation of BIP 32.

Definitions and Theorems

Function: hash160

(defun hash160 (bytes)
  (declare (xargs :guard (byte-listp bytes)))
  (declare (xargs :guard (< (len bytes) (expt 2 61))))
  (let ((__function__ 'hash160))
    (declare (ignorable __function__))
    (ripemd-160-bytes (sha-256-bytes bytes))))

Theorem: byte-listp-of-hash160

(defthm byte-listp-of-hash160
  (b* ((hash (hash160 bytes)))
    (byte-listp hash))
  :rule-classes :rewrite)

Theorem: len-of-hash160

(defthm len-of-hash160
  (b* ((hash (hash160 bytes)))
    (equal (len hash) 20))
  :rule-classes :rewrite)