		Search-engine friendly clone of the ACL2 documentation.

Attachments

Sha-256-attachment

Executable attachment for the SHA-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: sha-256-bytes-wrapper

(defun sha-256-bytes-wrapper (bytes)
  (declare (xargs :guard (byte-listp bytes)))
  (declare (xargs :guard (< (len bytes) (expt 2 61))))
  (let ((__function__ 'sha-256-bytes-wrapper))
    (declare (ignorable __function__))
    (b* ((bytes (mbe :logic (byte-list-fix bytes)
                     :exec bytes)))
      (sha2::sha-256-bytes bytes))))

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

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

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

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

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

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

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

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