		Search-engine friendly clone of the ACL2 documentation.

Poseidon-main-definition

Sponge-validp

Check if a sponge state is valid with respect to given parameters.

Signature
(sponge-validp sponge param) → yes/no
Arguments: sponge — Guard (spongep sponge).; param — Guard (paramp param).
Returns: yes/no — Type (booleanp yes/no).

The state vector must consist of prime field elements, and must have length equal to r + c. Furthermore, the index must not exceed r. We allow the index to be r, which happens just after we have absorbed or squeezed all of the r elements of the state vector. If one more element is absorbed and squeezed, a permutation is performed and the index is reset to 0 (see absorb1 and squeeze1), but in case there is no next element absorbed or squeezed, we avoid the permutation by letting the index be r.

Definitions and Theorems

Function: sponge-validp

(defun sponge-validp (sponge param)
  (declare (xargs :guard (and (spongep sponge) (paramp param))))
  (let ((__function__ 'sponge-validp))
    (declare (ignorable __function__))
    (and (fe-listp (sponge->stat sponge)
                   (param->prime param))
         (equal (len (sponge->stat sponge))
                (param->size param))
         (<= (sponge->index sponge)
             (param->rate param)))))

Theorem: booleanp-of-sponge-validp

(defthm booleanp-of-sponge-validp
  (b* ((yes/no (sponge-validp sponge param)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: sponge-validp-of-sponge-fix-sponge

(defthm sponge-validp-of-sponge-fix-sponge
  (equal (sponge-validp (sponge-fix sponge)
                        param)
         (sponge-validp sponge param)))

Theorem: sponge-validp-sponge-equiv-congruence-on-sponge

(defthm sponge-validp-sponge-equiv-congruence-on-sponge
  (implies (sponge-equiv sponge sponge-equiv)
           (equal (sponge-validp sponge param)
                  (sponge-validp sponge-equiv param)))
  :rule-classes :congruence)

Theorem: sponge-validp-of-param-fix-param

(defthm sponge-validp-of-param-fix-param
  (equal (sponge-validp sponge (param-fix param))
         (sponge-validp sponge param)))

Theorem: sponge-validp-param-equiv-congruence-on-param

(defthm sponge-validp-param-equiv-congruence-on-param
  (implies (param-equiv param param-equiv)
           (equal (sponge-validp sponge param)
                  (sponge-validp sponge param-equiv)))
  :rule-classes :congruence)