		Search-engine friendly clone of the ACL2 documentation.

Poseidon-main-definition

Partial-rounds

Perform a sequence of partial rounds.

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

The number of partial rounds in the sequence is determined by the length of the list of lists of constants passed as input.

Definitions and Theorems

Function: partial-rounds

(defun partial-rounds (stat constants
                            alpha partial-first-p mds prime)
  (declare (xargs :guard (and (integerp alpha)
                              (booleanp partial-first-p)
                              (primep prime)
                              (fe-listp stat prime)
                              (fe-list-listp constants prime)
                              (fe-list-listp mds prime))))
  (declare (xargs :guard (and (all-len-equal-p constants (len stat))
                              (all-len-equal-p mds (len stat))
                              (equal (len mds) (len stat)))))
  (let ((__function__ 'partial-rounds))
    (declare (ignorable __function__))
    (b* (((when (endp constants)) stat)
         (stat (round stat (car constants)
                      alpha partial-first-p mds prime nil)))
      (partial-rounds stat (cdr constants)
                      alpha partial-first-p mds prime))))

Theorem: fe-listp-of-partial-rounds

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

Theorem: len-of-partial-rounds

(defthm len-of-partial-rounds
 (implies
  (equal (len mds) (len stat))
  (b* ((?new-stat (partial-rounds stat constants
                                  alpha partial-first-p mds prime)))
    (equal (len new-stat) (len stat)))))