		Search-engine friendly clone of the ACL2 documentation.

Interfaces

Keccak-256-interface

Keccak-256 is specified in the Keccak web site, in particular `The Keccak Reference' document, Version 3.0.

According to the aforementioned specification, the input of Keccak-256 is a sequence of any number of bits, or any number of bytes.

According to the aforementioned specification, the output of Keccak-256 is a sequence of exactly 256 bits, or 32 bytes.

Definitions and Theorems

Theorem: bit-list-of-keccak-256-bits

(defthm bit-list-of-keccak-256-bits
        (bit-listp (keccak-256-bits bits)))

Theorem: byte-list-of-keccak-256-bytes

(defthm byte-list-of-keccak-256-bytes
        (byte-listp (keccak-256-bytes bytes)))

Theorem: len-of-keccak-256-bits

(defthm len-of-keccak-256-bits
        (equal (len (keccak-256-bits bits))
               256))

Theorem: len-of-keccak-256-bytes

(defthm len-of-keccak-256-bytes
        (equal (len (keccak-256-bytes bytes))
               32))

Theorem: keccak-256-bits-of-bit-list-fix-bits

(defthm keccak-256-bits-of-bit-list-fix-bits
        (equal (keccak-256-bits (acl2::bit-list-fix bits))
               (keccak-256-bits bits)))

Theorem: keccak-256-bits-bit-list-equiv-congruence-on-bits

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

Theorem: keccak-256-bytes-of-byte-list-fix-bytes

(defthm keccak-256-bytes-of-byte-list-fix-bytes
        (equal (keccak-256-bytes (byte-list-fix bytes))
               (keccak-256-bytes bytes)))

Theorem: keccak-256-bytes-byte-list-equiv-congruence-on-bytes

(defthm keccak-256-bytes-byte-list-equiv-congruence-on-bytes
        (implies (byte-list-equiv bytes bytes-equiv)
                 (equal (keccak-256-bytes bytes)
                        (keccak-256-bytes bytes-equiv)))
        :rule-classes :congruence)

Theorem: true-listp-of-keccak-256-bits

(defthm true-listp-of-keccak-256-bits
        (true-listp (keccak-256-bits bits))
        :rule-classes :type-prescription)

Theorem: true-listp-of-keccak-256-bytes

(defthm true-listp-of-keccak-256-bytes
        (true-listp (keccak-256-bytes bytes))
        :rule-classes :type-prescription)

Theorem: consp-of-keccak-256-bits

(defthm consp-of-keccak-256-bits
        (consp (keccak-256-bits bits))
        :rule-classes :type-prescription)

Theorem: consp-of-keccak-256-bytes

(defthm consp-of-keccak-256-bytes
        (consp (keccak-256-bytes bytes))
        :rule-classes :type-prescription)

Theorem: byte-list32p-of-keccak-256-bytes

(defthm byte-list32p-of-keccak-256-bytes
        (byte-list32p (keccak-256-bytes bytes)))