		Search-engine friendly clone of the ACL2 documentation.

Poseidon-main-definition

Add-round-constants

Add round constants to the state vector.

Signature
(add-round-constants stat constants prime) → new-stat
Arguments: stat — Guard (fe-listp stat prime).; constants — Guard (fe-listp constants prime).; prime — Guard (primep prime).
Returns: new-stat — Type (fe-listp new-stat prime), given (posp prime).

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

Besides the state, it needs the constants for the round, in number that matches the state vector.

This could be a more general ACL2 function to add two vectors of field elements.

Definitions and Theorems

Function: add-round-constants

(defun add-round-constants (stat constants prime)
  (declare (xargs :guard (and (primep prime)
                              (fe-listp stat prime)
                              (fe-listp constants prime))))
  (declare (xargs :guard (equal (len constants) (len stat))))
  (let ((__function__ 'add-round-constants))
    (declare (ignorable __function__))
    (cond ((endp stat) nil)
          (t (cons (add (car stat) (car constants) prime)
                   (add-round-constants (cdr stat)
                                        (cdr constants)
                                        prime))))))

Theorem: fe-listp-of-add-round-constants

(defthm fe-listp-of-add-round-constants
  (implies
       (posp prime)
       (b* ((new-stat (add-round-constants stat constants prime)))
         (fe-listp new-stat prime)))
  :rule-classes :rewrite)

Theorem: len-of-add-round-constants

(defthm len-of-add-round-constants
  (b* ((?new-stat (add-round-constants stat constants prime)))
    (equal (len new-stat) (len stat))))