• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
    • Apt
    • Acre
    • Milawa
    • Smtlink
    • Aleobft
    • Abnf
    • Vwsim
    • Isar
    • Wp-gen
    • Dimacs-reader
    • Pfcs
    • Legacy-defrstobj
    • Proof-checker-array
    • Soft
    • Farray
    • Rp-rewriter
    • Instant-runoff-voting
    • Imp-language
    • Sidekick
    • Leftist-trees
    • C
    • Java
    • Taspi
    • Bitcoin
    • Des
    • Ethereum
    • X86isa
    • Sha-2
    • Yul
    • Riscv
    • Zcash
    • Proof-checker-itp13
    • Regex
    • ACL2-programming-language
    • Json
    • Jfkr
    • Equational
    • Cryptography
    • Poseidon
      • Poseidon-main-definition
        • Param
        • Hashp
        • Absorb1
        • Sponge
        • Hash
        • All-rounds
        • Sponge-validp
        • Squeeze1
        • Sub-words-partial
        • Squeeze
        • Round
        • Partial-rounds
        • Mode
        • Full-rounds
        • Permute
        • Sub-words
        • Add-round-constants
        • Mix-layer
        • Dot-product
        • Absorb
        • Pow-by-alpha
        • Param->size
        • Sub-words-full
        • Param->capacity-then-rate-p
        • Param->partial-last-p
        • Param-additional-theorems
        • Param->rounds
        • Param->descending-p
        • Init-sponge
      • Poseidon-instantiations
    • Where-do-i-place-my-book
    • Bigmems
    • Builtins
    • Axe
    • Execloader
    • Solidity
    • Leo
    • Paco
    • Concurrent-programs
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Poseidon-main-definition

Squeeze1

Squeeze one element from the sponge.

Signature

(squeeze1 sponge param) → (mv output new-sponge)

Arguments

sponge — Guard (spongep sponge).

param — Guard (paramp param).

Returns

output — Type (fep output (param->prime param)), given (sponge-validp sponge param).

new-sponge — Type (spongep new-sponge).

This is quite analogous to absorb1 (see that function's documentation), with the roles of the modes swapped. The main difference is that the state vector is unchanged, and instead we return the element of the state pointed to by the index.

Definitions and Theorems

Function: squeeze1

(defun squeeze1 (sponge param)
  (declare (xargs :guard (and (spongep sponge) (paramp param))))
  (declare (xargs :guard (sponge-validp sponge param)))
  (let ((__function__ 'squeeze1))
    (declare (ignorable __function__))
    (b* (((sponge sponge) sponge)
         ((param param) param)
         ((mv stat index)
          (if (or (equal sponge.index param.rate)
                  (mode-case sponge.mode :absorb))
              (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)))
         (output (nth list-index-in-stat stat)))
      (mv output
          (make-sponge :stat stat
                       :mode (mode-squeeze)
                       :index (1+ index))))))

Theorem: fep-of-squeeze1.output

(defthm fep-of-squeeze1.output
  (implies (sponge-validp sponge param)
           (b* (((mv ?output ?new-sponge)
                 (squeeze1 sponge param)))
             (fep output (param->prime param))))
  :rule-classes :rewrite)

Theorem: spongep-of-squeeze1.new-sponge

(defthm spongep-of-squeeze1.new-sponge
  (b* (((mv ?output ?new-sponge)
        (squeeze1 sponge param)))
    (spongep new-sponge))
  :rule-classes :rewrite)

Theorem: sponge-validp-of-squeeze1

(defthm sponge-validp-of-squeeze1
  (implies (sponge-validp sponge param)
           (b* (((mv ?output ?new-sponge)
                 (squeeze1 sponge param)))
             (sponge-validp new-sponge param)))
  :rule-classes :rewrite)