		Search-engine friendly clone of the ACL2 documentation.

Poseidon-main-definition

Permute

Permutation.

Signature
(permute stat param) → new-stat
Arguments: stat — Guard (fe-listp stat (param->prime param)).; param — Guard (paramp param).
Returns: new-stat — Type (fe-listp new-stat (param->prime param)), given (fe-listp stat (param->prime param)).

This is a wrapper of all-rounds that provides a more compact interface, consisting of a state vector and the parameters, whose components are passed to all-rounds.

Definitions and Theorems

Function: permute

(defun permute (stat param)
 (declare (xargs :guard (and (paramp param)
                             (fe-listp stat (param->prime param)))))
 (declare (xargs :guard (equal (len stat) (param->size param))))
 (let ((__function__ 'permute))
   (declare (ignorable __function__))
   (all-rounds stat (param->constants param)
               (param->alpha param)
               (param->partial-first-p param)
               (param->mds param)
               (param->full-rounds-half param)
               (param->partial-rounds param)
               (param->prime param))))

Theorem: return-type-of-permute

(defthm return-type-of-permute
  (implies (fe-listp stat (param->prime param))
           (b* ((new-stat (permute stat param)))
             (fe-listp new-stat (param->prime param))))
  :rule-classes :rewrite)

Theorem: len-of-permute

(defthm len-of-permute
  (implies (and (equal (len stat) (param->size param))
                (paramp param))
           (b* ((?new-stat (permute stat param)))
             (equal (len new-stat) (len stat)))))