• 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
          • 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

Poseidon-main-definition

Main definition of the Poseidon hash function.

See poseidon for an overview.

Poseidon is parameterized over a number of aspects, such as the round constants, the MDS matrix, etc. We capture all these parameters in the param data structure, which also includes parameters for aspects that are not explicitly described in the Poseidon paper but that nevertheless need to be made precise in the definition. Perhaps these latter aspects are disambiguated by the reference implementation of Poseidon (which is also linked from the web site linked in poseidon), but it stil makes mathematical sense to parameterize the definition over those aspects. These are all described in detail in param. The top-level functions of our specification of Poseidon take a param as an input.

Poseidon uses a sponge construction, which is a more general concept. In a sponge construction, one can absorb any number of elements, squeeze any number of elements, and again absorb more elements and then squeeze them, and so on. We formalize this by explicating the state of the sponge in sponge, which consists of not only the current vector of elements, but also an index within the vector where elements are absorbed or squeezed next, and an indication of whether we are absorbing or squeezing; this is described in more detail in sponge. We define functions absorb and squeeze to absorb and squeeze elements, which take as input and return as output a sponge state, besides the other natural inputs and outputs. This is similar to some existing implementations of Poseidon.

The aforementioned absorb and squeeze functions take or return multiple input or output elements. If these functions were defined ``directly'', they would be somewhat complicated because of the need to handle a number of inputs or outputs that will start from the current index and that may require one or more permutations and index wrap-arounds. This is especially the case because, as described in param, we support several different ways to absorb and squeeze elements. To keep things simpler, we define functions absorb1 and squeeze1 that absorb or squeeze a single input or output element: these are much simpler to define and understand, even with the several different ways to absorb and squeeze elements. Then we define absorb and squeeze by simply iterating absorb1 and squeeze1.

At the very top level, we define a function hash that maps any number of inputs to any number of outputs. This is defined by internally creating and using a sponge state. Note that there is no need to include any explicit notion of padding, which can be performed externally to Poseidon proper as defined here.

Subtopics

Param
Fixtype of Poseidon parameters.
Hashp
Hash according to just the Poseidon permutation.
Absorb1
Absorb one element into the sponge.
Sponge
Fixtype of sponge states.
Hash
Hash any number of inputs to any number of outputs.
All-rounds
Perform all the rounds in a permutation.
Sponge-validp
Check if a sponge state is valid with respect to given parameters.
Squeeze1
Squeeze one element from the sponge.
Sub-words-partial
Apply the partial S-box substitution to the state vector.
Squeeze
Squeeze any number of elements from the sponge.
Round
Perform a round.
Partial-rounds
Perform a sequence of partial rounds.
Mode
Fixtype of sponge modes.
Full-rounds
Perform a sequence of full rounds.
Permute
Permutation.
Sub-words
Apply the S-box substitution to the state vector.
Add-round-constants
Add round constants to the state vector.
Mix-layer
Multiply the MDS matrix and the state vector.
Dot-product
Dot product of a matrix row and the state vector.
Absorb
Absorb any number of elements into the sponge.
Pow-by-alpha
Raise a field element to the \alpha power.
Param->size
Size of the state vector, i.e. r + c.
Sub-words-full
Apply the full S-box substitution to the state vector.
Param->capacity-then-rate-p
Negation of the param->rate-then-capacity-p parameter.
Param->partial-last-p
Negation of the param->partial-first-p parameter.
Param-additional-theorems
Additional theorems about the parameters in param.
Param->rounds
Total number of rounds, i.e. 2 R_f + R_P = R_F + R_P.
Param->descending-p
Negation of the param->ascending-p parameter.
Init-sponge
Initial sponge state.