		Search-engine friendly clone of the ACL2 documentation.

Poseidon-main-definition

Init-sponge

Initial sponge state.

Signature
(init-sponge size) → sponge
Arguments: size — Guard (natp size).
Returns: sponge — Type (spongep sponge).

The state vector consists of all zeros; we pass r+ c to determine the size. The mode is absorbing. The index is 0.

Definitions and Theorems

Function: init-sponge

(defun init-sponge (size)
  (declare (xargs :guard (natp size)))
  (let ((__function__ 'init-sponge))
    (declare (ignorable __function__))
    (make-sponge :stat (repeat size 0)
                 :mode (mode-absorb)
                 :index 0)))

Theorem: spongep-of-init-sponge

(defthm spongep-of-init-sponge
  (b* ((sponge (init-sponge size)))
    (spongep sponge))
  :rule-classes :rewrite)

Theorem: sponge-validp-of-init-sponge

(defthm sponge-validp-of-init-sponge
  (sponge-validp (init-sponge (param->size param))
                 param))