		Search-engine friendly clone of the ACL2 documentation.

Poseidon-main-definition

Sub-words-full

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

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

We raise to the \alpha power every element of the state vector.

Definitions and Theorems

Function: sub-words-full

(defun sub-words-full (stat alpha prime)
  (declare (xargs :guard (and (integerp alpha)
                              (primep prime)
                              (fe-listp stat prime))))
  (let ((__function__ 'sub-words-full))
    (declare (ignorable __function__))
    (cond ((endp stat) nil)
          (t (cons (pow-by-alpha (car stat) alpha prime)
                   (sub-words-full (cdr stat)
                                   alpha prime))))))

Theorem: fe-listp-of-sub-wordsfull

(defthm fe-listp-of-sub-wordsfull
  (implies (primep prime)
           (b* ((new-stat (sub-words-full stat alpha prime)))
             (fe-listp new-stat prime)))
  :rule-classes :rewrite)

Theorem: len-of-sub-words-full

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