		Search-engine friendly clone of the ACL2 documentation.

Poseidon-main-definition

Mix-layer

Multiply the MDS matrix and the state vector.

Signature
(mix-layer rows stat prime) → elems
Arguments: rows — Guard (fe-list-listp rows prime).; stat — Guard (fe-listp stat prime).; prime — Guard (primep prime).
Returns: elems — Type (fe-listp elems prime), given (posp prime).

This is the \mathit{MixLayer} function in the paper.

This views the matrix as a list of rows and the state as a column vector, but as explained in param and mentioned in dot-product we could equivalently view the matrix rows as matrix columns and the state as a row vector.

Definitions and Theorems

Function: mix-layer

(defun mix-layer (rows stat prime)
  (declare (xargs :guard (and (primep prime)
                              (fe-list-listp rows prime)
                              (fe-listp stat prime))))
  (declare (xargs :guard (all-len-equal-p rows (len stat))))
  (let ((__function__ 'mix-layer))
    (declare (ignorable __function__))
    (cond ((endp rows) nil)
          (t (cons (dot-product (car rows) stat prime)
                   (mix-layer (cdr rows) stat prime))))))

Theorem: fe-listp-of-mix-layer

(defthm fe-listp-of-mix-layer
  (implies (posp prime)
           (b* ((elems (mix-layer rows stat prime)))
             (fe-listp elems prime)))
  :rule-classes :rewrite)

Theorem: len-of-mix-layer

(defthm len-of-mix-layer
  (b* ((?elems (mix-layer rows stat prime)))
    (equal (len elems) (len rows))))