		Search-engine friendly clone of the ACL2 documentation.

Interfaces

Ripemd-160-interface

RIPEMD-160 is specified in the `RIPEMD-160: A Strengthened Version of RIPEMD' document.

According to the aforementioned document, the input of RIPEMD-160 is a sequence of any number of bits, or any number of bytes.

According to the aforementioned document, the output of RIPEMD-160 is a sequence of exactly 160 bits, or 20 bytes.

Definitions and Theorems

Theorem: bit-list-of-ripemd-160-bits

(defthm bit-list-of-ripemd-160-bits
  (bit-listp (ripemd-160-bits bits)))

Theorem: byte-list-of-ripemd-160-bytes

(defthm byte-list-of-ripemd-160-bytes
  (byte-listp (ripemd-160-bytes bytes)))

Theorem: len-of-ripemd-160-bits

(defthm len-of-ripemd-160-bits
  (equal (len (ripemd-160-bits bits))
         160))

Theorem: len-of-ripemd-160-bytes

(defthm len-of-ripemd-160-bytes
  (equal (len (ripemd-160-bytes bytes))
         20))

Theorem: ripemd-160-bits-of-bit-list-fix-bits

(defthm ripemd-160-bits-of-bit-list-fix-bits
  (equal (ripemd-160-bits (acl2::bit-list-fix bits))
         (ripemd-160-bits bits)))

Theorem: ripemd-160-bits-bit-list-equiv-congruence-on-bits

(defthm ripemd-160-bits-bit-list-equiv-congruence-on-bits
  (implies (acl2::bit-list-equiv bits bits-equiv)
           (equal (ripemd-160-bits bits)
                  (ripemd-160-bits bits-equiv)))
  :rule-classes :congruence)

Theorem: ripemd-160-bytes-of-byte-list-fix-bytes

(defthm ripemd-160-bytes-of-byte-list-fix-bytes
  (equal (ripemd-160-bytes (byte-list-fix bytes))
         (ripemd-160-bytes bytes)))

Theorem: ripemd-160-bytes-byte-list-equiv-congruence-on-bytes

(defthm ripemd-160-bytes-byte-list-equiv-congruence-on-bytes
  (implies (byte-list-equiv bytes bytes-equiv)
           (equal (ripemd-160-bytes bytes)
                  (ripemd-160-bytes bytes-equiv)))
  :rule-classes :congruence)

Theorem: true-listp-of-ripemd-160-bits

(defthm true-listp-of-ripemd-160-bits
  (true-listp (ripemd-160-bits bits))
  :rule-classes :type-prescription)

Theorem: true-listp-of-ripemd-160-bytes

(defthm true-listp-of-ripemd-160-bytes
  (true-listp (ripemd-160-bytes bytes))
  :rule-classes :type-prescription)

Theorem: consp-of-ripemd-160-bits

(defthm consp-of-ripemd-160-bits
  (consp (ripemd-160-bits bits))
  :rule-classes :type-prescription)

Theorem: consp-of-ripemd-160-bytes

(defthm consp-of-ripemd-160-bytes
  (consp (ripemd-160-bytes bytes))
  :rule-classes :type-prescription)

Theorem: byte-list20p-of-ripemd-160-bytes

(defthm byte-list20p-of-ripemd-160-bytes
  (byte-list20p (ripemd-160-bytes bytes)))