		Search-engine friendly clone of the ACL2 documentation.

Poseidon-main-definition

Absorb1

Absorb one element into the sponge.

Signature
(absorb1 input sponge param) → new-sponge
Arguments: input — Guard (fep input (param->prime param)).; sponge — Guard (spongep sponge).; param — Guard (paramp param).
Returns: new-sponge — Type (spongep new-sponge).

If the index is r or the mode is squeezing, we permute the state and reset the index to 0.

If the parameters say that indices are increasing in the list, the index of the sponge is also the index in the sublist of r elements. Otherwise, we flip the index.

Given the index in the sublist of r elements, we obtain the index in the stat list as follows. If the r elements come before the c elements, it is the same index. Otherwise, we add c to the index.

The resulting index is the one of the state element to be combined with the input. The combination is field addition, whose result replaces the element in the state.

We return an updated sponge state with the updated state vector, the next index, and the aborbing mode (unchanged if the sponge was already absorbing). Note that the index in the sponge state is always increasing, regardless of the parameter about the ascending or descending indices in the state vector list.

Definitions and Theorems

Function: absorb1

(defun absorb1 (input sponge param)
  (declare (xargs :guard (and (spongep sponge)
                              (paramp param)
                              (fep input (param->prime param)))))
  (declare (xargs :guard (sponge-validp sponge param)))
  (let ((__function__ 'absorb1))
    (declare (ignorable __function__))
    (b* (((sponge sponge) sponge)
         ((param param) param)
         ((mv stat index)
          (if (or (equal sponge.index param.rate)
                  (mode-case sponge.mode :squeeze))
              (mv (permute sponge.stat param) 0)
            (mv sponge.stat sponge.index)))
         (list-index-in-rate (if param.ascending-p index
                               (- (1- param.rate) index)))
         (list-index-in-stat
              (if param.rate-then-capacity-p list-index-in-rate
                (+ param.capacity list-index-in-rate)))
         (stat (update-nth list-index-in-stat
                           (add (nth list-index-in-stat stat)
                                input param.prime)
                           stat)))
      (make-sponge :stat stat
                   :mode (mode-absorb)
                   :index (1+ index)))))

Theorem: spongep-of-absorb1

(defthm spongep-of-absorb1
  (b* ((new-sponge (absorb1 input sponge param)))
    (spongep new-sponge))
  :rule-classes :rewrite)

Theorem: sponge-validp-of-absorb1

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