		Search-engine friendly clone of the ACL2 documentation.

Poseidon-main-definition

Sub-words

Apply the S-box substitution to the state vector.

Signature
(sub-words stat alpha partial-first-p prime full-p) → 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).; full-p — Guard (booleanp full-p).
Returns: new-stat — Type (fe-listp new-stat prime), given (and (primep prime) (fe-listp stat prime)).

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

The substitution is full or partial, depending on the full-p parameter.

Definitions and Theorems

Function: sub-words

(defun sub-words (stat alpha partial-first-p prime full-p)
  (declare (xargs :guard (and (integerp alpha)
                              (booleanp partial-first-p)
                              (primep prime)
                              (booleanp full-p)
                              (fe-listp stat prime))))
  (let ((__function__ 'sub-words))
    (declare (ignorable __function__))
    (if full-p (sub-words-full stat alpha prime)
      (sub-words-partial stat alpha partial-first-p prime))))

Theorem: fe-listp-of-sub-words

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

Theorem: len-of-sub-words

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