		Search-engine friendly clone of the ACL2 documentation.

Blake2-hash

Blake2s-256

The function \mathsf{BLAKE2s}\textsf{-}\mathsf{256} [ZPS:5.4.1.2].

Signature
(blake2s-256 pers input) → output
Arguments: pers — Guard (byte-listp pers).; input — Guard (byte-listp input).
Returns: output — Type (byte-listp output).

This is the instantiation \ell=\mathsf{256} of the general function \mathsf{BLAKE2s}\textsf{-}\ell. We may generalize this ACL2 function to take \ell as a parameter, at some point.

[ZPS] puts no restrictions on the size of the data (i.e. input), but we follow the guard in the BLAKE2 library. The output must be 32 bytes, i.e. 256 bits.

We pass the empty list of bytes as both key and salt.

Definitions and Theorems

Function: blake2s-256

(defun blake2s-256 (pers input)
  (declare (xargs :guard (and (byte-listp pers)
                              (byte-listp input))))
  (declare (xargs :guard (and (= (len pers) 8)
                              (<= (len input)
                                  blake::*max-input-bytes*))))
  (let ((__function__ 'blake2s-256))
    (declare (ignorable __function__))
    (blake::blake2s-extended input nil nil pers 32)))

Theorem: byte-listp-of-blake2s-256

(defthm byte-listp-of-blake2s-256
  (b* ((output (blake2s-256 pers input)))
    (byte-listp output))
  :rule-classes :rewrite)

Theorem: len-of-blake2s-256

(defthm len-of-blake2s-256
  (b* ((?output (blake2s-256 pers input)))
    (equal (len output) 32)))