		Search-engine friendly clone of the ACL2 documentation.

Poseidon-main-definition

Dot-product

Dot product of a matrix row and the state vector.

Signature
(dot-product row stat prime) → elem
Arguments: row — Guard (fe-listp row prime).; stat — Guard (fe-listp stat prime).; prime — Guard (primep prime).
Returns: elem — Type (fep elem prime), given (posp prime).

This views the state as a column vector. However, as explained in param, we could equivalently view the matrix row as a matrix column and the state as a row vector.

This could be a more general ACL2 function to perform the dot product of two vectors of field elements.

Definitions and Theorems

Function: dot-product

(defun dot-product (row stat prime)
  (declare (xargs :guard (and (primep prime)
                              (fe-listp row prime)
                              (fe-listp stat prime))))
  (declare (xargs :guard (equal (len stat) (len row))))
  (let ((__function__ 'dot-product))
    (declare (ignorable __function__))
    (cond ((endp row) 0)
          (t (add (mul (car row) (car stat) prime)
                  (dot-product (cdr row) (cdr stat) prime)
                  prime)))))

Theorem: fep-of-dot-product

(defthm fep-of-dot-product
  (implies (posp prime)
           (b* ((elem (dot-product row stat prime)))
             (fep elem prime)))
  :rule-classes :rewrite)