		Search-engine friendly clone of the ACL2 documentation.

Poseidon-main-definition

Squeeze

Squeeze any number of elements from the sponge.

Signature
(squeeze count sponge param) → (mv outputs new-sponge)
Arguments: count — Guard (natp count).; sponge — Guard (spongep sponge).; param — Guard (paramp param).
Returns: outputs — Type (fe-listp outputs (param->prime param)), given (sponge-validp sponge param).; new-sponge — Type (spongep new-sponge).

We use squeeze1 for each output, whose count is passed to this ACL2 function, threading the sponge state through the sequence.

Definitions and Theorems

Function: squeeze

(defun squeeze (count sponge param)
  (declare (xargs :guard (and (natp count)
                              (spongep sponge)
                              (paramp param))))
  (declare (xargs :guard (sponge-validp sponge param)))
  (let ((__function__ 'squeeze))
    (declare (ignorable __function__))
    (b* (((when (zp count))
          (mv nil (sponge-fix sponge)))
         ((mv output sponge)
          (squeeze1 sponge param))
         ((mv outputs sponge)
          (squeeze (1- count) sponge param)))
      (mv (cons output outputs) sponge))))

Theorem: fe-listp-of-squeeze.outputs

(defthm fe-listp-of-squeeze.outputs
  (implies (sponge-validp sponge param)
           (b* (((mv ?outputs ?new-sponge)
                 (squeeze count sponge param)))
             (fe-listp outputs (param->prime param))))
  :rule-classes :rewrite)

Theorem: spongep-of-squeeze.new-sponge

(defthm spongep-of-squeeze.new-sponge
  (b* (((mv ?outputs ?new-sponge)
        (squeeze count sponge param)))
    (spongep new-sponge))
  :rule-classes :rewrite)

Theorem: sponge-validp-of-squeeze

(defthm sponge-validp-of-squeeze
  (implies (sponge-validp sponge param)
           (b* (((mv ?outputs ?new-sponge)
                 (squeeze count sponge param)))
             (sponge-validp new-sponge param)))
  :rule-classes :rewrite)

Theorem: len-of-squeeze.outputs

(defthm len-of-squeeze.outputs
  (b* (((mv ?outputs ?new-sponge)
        (squeeze count sponge param)))
    (equal (len outputs) (nfix count))))