• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
      • Apt
      • Zfc
      • Acre
      • Milawa
      • Smtlink
      • Abnf
      • Vwsim
      • Isar
      • Wp-gen
      • Dimacs-reader
      • Pfcs
      • Legacy-defrstobj
      • Proof-checker-array
      • Soft
      • C
      • Farray
      • Rp-rewriter
      • Instant-runoff-voting
      • Imp-language
      • Sidekick
      • Leftist-trees
      • Java
      • Taspi
      • Bitcoin
      • Riscv
      • Des
      • Ethereum
      • X86isa
      • Sha-2
      • Yul
      • Zcash
      • Proof-checker-itp13
      • Regex
      • ACL2-programming-language
      • Json
      • Jfkr
      • Equational
      • Cryptography
      • Poseidon
        • Poseidon-main-definition
          • Param
          • Hashp
          • Absorb1
          • Sponge
            • Sponge-fix
            • Sponge-equiv
            • Spongep
            • Make-sponge
            • Change-sponge
            • Sponge->stat
            • Sponge->mode
            • Sponge->index
          • 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
      • Axe
      • Bigmems
      • Builtins
      • Execloader
      • Aleo
      • Solidity
      • Paco
      • Concurrent-programs
      • Bls12-377-curves
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
    • Math
    • Testing-utilities
  • Poseidon-main-definition

Sponge

Fixtype of sponge states.

This is a product type introduced by fty::defprod.

Fields
stat — nat-list
mode — mode
index — natp

This consists of a state vector, an absorbing or squeezing mode, and an index. The index points to an element of the sublist of the state vector that consists of the r elements against which inputs are absorbed or outputs are squeezed: the index indicates the next element absorbed or squeezed.

Here we just say that the state vector is a list of natural numbers, because we do not have the prime that defines the prime field. Requirements on the state vector, and on the absorbing or squeezing index, are expressed in sponge-validp, since they involve the parameters.

Subtopics

Sponge-fix
Fixing function for sponge structures.
Sponge-equiv
Basic equivalence relation for sponge structures.
Spongep
Recognizer for sponge structures.
Make-sponge
Basic constructor macro for sponge structures.
Change-sponge
Modifying constructor for sponge structures.
Sponge->stat
Get the stat field from a sponge.
Sponge->mode
Get the mode field from a sponge.
Sponge->index
Get the index field from a sponge.