		Search-engine friendly clone of the ACL2 documentation.

Poseidon-main-definition

Absorb

Absorb any number of elements into the sponge.

Signature
(absorb inputs sponge param) → new-sponge
Arguments: inputs — Guard (fe-listp inputs (param->prime param)).; sponge — Guard (spongep sponge).; param — Guard (paramp param).
Returns: new-sponge — Type (spongep new-sponge).

We use absorb1 on each input, threading the sponge state through the sequence.

Definitions and Theorems

Function: absorb

(defun absorb (inputs sponge param)
  (declare
       (xargs :guard (and (spongep sponge)
                          (paramp param)
                          (fe-listp inputs (param->prime param)))))
  (declare (xargs :guard (sponge-validp sponge param)))
  (let ((__function__ 'absorb))
    (declare (ignorable __function__))
    (b* (((when (endp inputs))
          (sponge-fix sponge))
         (sponge (absorb1 (car inputs) sponge param)))
      (absorb (cdr inputs) sponge param))))

Theorem: spongep-of-absorb

(defthm spongep-of-absorb
  (b* ((new-sponge (absorb inputs sponge param)))
    (spongep new-sponge))
  :rule-classes :rewrite)

Theorem: sponge-validp-of-absorb

(defthm sponge-validp-of-absorb
  (implies (sponge-validp sponge param)
           (b* ((new-sponge (absorb inputs sponge param)))
             (sponge-validp new-sponge param)))
  :rule-classes :rewrite)