		Search-engine friendly clone of the ACL2 documentation.

Poseidon-main-definition

Sub-words-partial

Apply the partial S-box substitution to the state vector.

Signature
(sub-words-partial stat alpha partial-first-p prime) → new-stat
Arguments: stat — Guard (fe-listp stat prime).; alpha — Guard (integerp alpha).; partial-first-p — Guard (booleanp partial-first-p).; prime — Guard (primep prime).
Returns: new-stat — Type (fe-listp new-stat prime), given (and (primep prime) (fe-listp stat prime)).

We raise to the \alpha power either the first or the last element of the state vector, depending on the partial-first-p parameter. If the state vector is empty, we return the empty state vector; this does not happen in Poseidon because r + c > 0, but in this function definition we do not need that requirement.

Definitions and Theorems

Function: sub-words-partial

(defun sub-words-partial (stat alpha partial-first-p prime)
 (declare (xargs :guard (and (integerp alpha)
                             (booleanp partial-first-p)
                             (primep prime)
                             (fe-listp stat prime))))
 (let ((__function__ 'sub-words-partial))
   (declare (ignorable __function__))
   (if
     (consp stat)
     (if partial-first-p (cons (pow-by-alpha (car stat) alpha prime)
                               (cdr stat))
       (append (butlast stat 1)
               (list (pow-by-alpha (car (last stat))
                                   alpha prime))))
     nil)))

Theorem: fe-listp-of-sub-words-partial

(defthm fe-listp-of-sub-words-partial
 (implies
  (and (primep prime)
       (fe-listp stat prime))
  (b*
   ((new-stat (sub-words-partial stat alpha partial-first-p prime)))
   (fe-listp new-stat prime)))
 :rule-classes :rewrite)

Theorem: len-of-sub-words-partial

(defthm len-of-sub-words-partial
 (b*
  ((?new-stat (sub-words-partial stat alpha partial-first-p prime)))
  (equal (len new-stat) (len stat))))