		Search-engine friendly clone of the ACL2 documentation.

Attachments

Keccak-256-attachment

Executable attachment for the Keccak-256 interface that operates on bytes.

We define a wrapper of the executable definition and attach the wrapper to the constrained function. The wrapper just serves to use the fixtypes for byte lists, and to fix the input accordingly.

Definitions and Theorems

Function: keccak-256-bytes-wrapper

(defun keccak-256-bytes-wrapper (bytes)
  (declare (xargs :guard (byte-listp bytes)))
  (let ((__function__ 'keccak-256-bytes-wrapper))
    (declare (ignorable __function__))
    (b* ((bytes (mbe :logic (byte-list-fix bytes)
                     :exec bytes)))
      (keccak::keccak-256-bytes bytes))))

Theorem: byte-listp-of-keccak-256-bytes-wrapper

(defthm byte-listp-of-keccak-256-bytes-wrapper
  (b* ((hash (keccak-256-bytes-wrapper bytes)))
    (byte-listp hash))
  :rule-classes :rewrite)

Theorem: len-of-keccak-256-bytes-wrapper

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

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

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

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

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