		Search-engine friendly clone of the ACL2 documentation.

Poseidon-main-definition

All-rounds

Perform all the rounds in a permutation.

Signature
(all-rounds stat constants alpha partial-first-p mds full-rounds-half partial-rounds 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).; full-rounds-half — Guard (natp full-rounds-half).; partial-rounds — Guard (natp partial-rounds).; prime — Guard (primep prime).
Returns: new-stat — Type (fe-listp new-stat prime), given (and (primep prime) (fe-listp stat prime)).

We pass the number of initial and final full rounds R_f and the number of partial rounds R_P, along with a list of lists of constants where the outer list has length 2 R_f + R_P.

Definitions and Theorems

Function: all-rounds

(defun all-rounds (stat constants alpha partial-first-p mds
                        full-rounds-half partial-rounds prime)
 (declare (xargs :guard (and (integerp alpha)
                             (booleanp partial-first-p)
                             (natp full-rounds-half)
                             (natp partial-rounds)
                             (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))
                             (equal (len constants)
                                    (+ (* 2 full-rounds-half)
                                       partial-rounds))
                             (all-len-equal-p mds (len stat))
                             (equal (len mds) (len stat)))))
 (let ((__function__ 'all-rounds))
   (declare (ignorable __function__))
   (b*
    ((full-rounds-first-constants (take full-rounds-half constants))
     (partial-rounds-constants
          (take partial-rounds
                (nthcdr full-rounds-half constants)))
     (full-rounds-last-constants
          (nthcdr (+ full-rounds-half partial-rounds)
                  constants))
     (stat (full-rounds stat full-rounds-first-constants
                        alpha partial-first-p mds prime))
     (stat (partial-rounds stat partial-rounds-constants
                           alpha partial-first-p mds prime))
     (stat (full-rounds stat full-rounds-last-constants
                        alpha partial-first-p mds prime)))
    stat)))

Theorem: fe-listp-of-all-rounds

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

Theorem: len-of-all-rounds

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

Theorem: nat-listp-of-all-rounds

(defthm nat-listp-of-all-rounds
 (implies
   (and (primep prime)
        (fe-listp stat prime))
   (b*
    ((?new-stat (all-rounds stat constants alpha partial-first-p mds
                            full-rounds-half partial-rounds prime)))
    (nat-listp new-stat))))