POSEIDON: A New Hash Function for Zero-Knowledge Proof Systems
Lorenzo Grassi, Dmitry Khovratovich, Christian Rechberger, Arnab Roy, Markus Schofnegger
2019 · Updated Version · eprint 2019/458
Disclaimer
This content was automatically converted from the original PDF and may have undergone post-processing. None of these steps have been reviewed or approved by the authors. Errors in formulas, definitions, proofs, or text may have been introduced during conversion. The authoritative version is the original paper on ePrint. Always cite and verify against the original publication.
Converted with: marker · 2026-02-12
Abstract
The area of practical computational integrity proof systems, like SNARKs, STARKs, Bulletproofs, is seeing a very dynamic development with several constructions having appeared recently with improved properties and relaxed setup requirements. Many use cases of such systems involve, often as their most expensive part, proving the knowledge of a preimage under a certain cryptographic hash function, which is expressed as a circuit over a large prime field.
In this paper, we present a modular framework and concrete instances of cryptographic hash functions which work natively with \text{GF}(p) objects. Our hash function POSEIDON uses up to 8x fewer constraints per message bit than Pedersen Hash. Our construction is not only expressed compactly as a circuit, but can also be tailored for various proof systems using specially crafted polynomials, thus bringing another boost in performance. We demonstrate this by implementing a 1-out-of-a-billion membership proof with Merkle trees in less than a second by using Bulletproofs.
Previous Versions
This paper is an updated version of [GKR+19] and [GKR+21] published at USENIX 2021. In this updated version, the authors limit themselves to POSEIDON over a prime field \mathbb{F}_p^t instantiated with x \mapsto x^\alpha, where \alpha \geq 3 is the smallest positive integer satisfying \gcd(\alpha, p-1) = 1. The security analysis has been updated to account for attacks in [KR21, BCD+20], flaws in the Groebner basis analysis have been fixed, and results from [ABM23] are incorporated. Both the entire family of STARKAD and POSEIDON instantiated with x \mapsto x^{-1} are considered dismissed.
1. Introduction
The recent advances in computational integrity proof systems made a number of computational tasks verifiable in short time and/or in zero knowledge. Several protocols require one party to prove the knowledge of a seed-derived secret, of an element being part of a large set, or their combination. An alternative to accumulator-based solutions is to express secret derivation using cryptographic hash functions, and to prove set membership by presenting an opening in a properly chosen Merkle tree.
The goal of Poseidon is to design a family of hash functions that are optimal in the R1CS metric (the most widespread) and good in the AET metric, while also supporting different finite field sizes. The substitution-permutation network (SPN) design allows for a generic hash function framework where the only security-critical parameter is the number of rounds.
The S-box is chosen as the power map x \mapsto x^\alpha, where \alpha \geq 3 is chosen as the smallest integer that guarantees invertibility. In particular, the choice \alpha = 5 is suitable for two of the most popular prime fields in ZK applications: the scalar fields of BLS12-381 and BN254.
The internal permutation Poseidon^\pi is based on the HADES design strategy, which uses a combination of full rounds (all state elements pass through the S-box) and partial rounds (only one element does). This reduces the R1CS or AET cost while maintaining equivalent security.
Table 1. Primary proposals and competitors. R1CS/bit costs are obtained by dividing the R1CS prover costs by the message rate. Timings from a third-party implementation on an i9-8950 CPU @2.9 GHz, 32 GB RAM.
| Name | S-box | Rate bits | Tree | R_F | R_P | R1CS/perm | R1CS/bit | Time/perm |
|---|---|---|---|---|---|---|---|---|
| Poseidon-80 | x^5 | 510 | 2:1 | 8 | 33 | 171 | 0.34 | 0.021 ms |
| x^5 | 1020 | 4:1 | 8 | 35 | 225 | 0.22 | 0.05 ms | |
| Poseidon-128 | x^5 | 510 | 2:1 | 8 | 57 | 243 | 0.47 | 0.033 ms |
| x^5 | 1020 | 4:1 | 8 | 60 | 300 | 0.29 | 0.08 ms | |
| x^5 | 2040 | 8:1 | 8 | 63 | 405 | 0.20 | 0.259 ms | |
| Poseidon-256 | x^5 | 1020 | 2:1 | 8 | 120 | 504 | 0.50 | 0.216 ms |
| x^5 | 2040 | 4:1 | 8 | 120 | 600 | 0.30 | 0.578 ms | |
| Pedersen Hash | — | 516 | 2:1 | — | — | 869 | 1.68 | — |
| Rescue | x^5 & x^{1/5} | 510 | 2:1 | 16 | — | 268 | 0.52 | 0.525 ms |
| x^5 & x^{1/5} | 1020 | 4:1 | 10 | — | 300 | 0.29 | 0.555 ms | |
| x^5 & x^{1/5} | 2040 | 8:1 | 10 | — | 450 | 0.22 | 1.03 ms |
Our Contributions
The authors design and analyze a family of hash functions over \text{GF}(p) named POSEIDON. The internal permutation Poseidon^\pi is based on the HADES design strategy [GLR+20], using substitution-permutation networks with t cells and partial rounds where only one S-box is used. Security levels of 80, 128, and 256 bits are supported, where the security is the same for collision and preimage resistance. An extensive cryptanalysis is provided with an accent on algebraic methods (interpolation, Groebner basis, higher-order differential attacks). Third-party benchmarks are available for PLONK (Table 6), Groth16 (Table 3), and Bulletproofs (Table 5).
Related Work
The Zcash designers introduced Pedersen hash [HBHW19], which utilizes 869 constraints per 516-bit message chunk (1.7 constraints per bit), whereas POSEIDON instances use from 0.2 to 0.45 constraints per bit. Ashur and Dhooghe [AD18] introduced the STARK-friendly JARVIS/FRIDAY, which were broken shortly after publication [ACG+19]. In response, the Rescue family [AABS+19] was created with two differences from POSEIDON: all S-box layers are full (no partial rounds), and every second layer uses x^{1/d} S-boxes, which prevents some algebraic attacks but requires more squarings in software.
Historic Remarks
Work on POSEIDON began in fall 2018, triggered by the STARK paper [BBHR19] proposing a Rijndael-based hash function. The design was inspired by LowMC [ARS+15] (partial S-box layers), SHARK [RDP+96] (inverse S-box + MDS matrix), and MiMC [AGR+16] (cube S-box). In 2019, the design split into the block cipher HADESMIMC and hash functions POSEIDON/STARKAD. STARKAD (binary fields) was eventually dropped due to security weaknesses [KR21, BCD+20]. After initial publication, third-party requests led to adding Merkle tree support, encryption modes, and additional security levels. The authors initially targeted Groth16, Bulletproofs, and STARKs, later adding PLONK due to its increased popularity.
2. Design
Poseidon maps strings over \mathbb{F}_p to fixed-length strings over \mathbb{F}_p, i.e., \text{Poseidon} : \mathbb{F}_p^* \to \mathbb{F}_p^o, where o is the output length (usually o = 1). It is constructed by instantiating a sponge function with the Poseidon^\pi permutation.
2.1 Sponge Construction
A sponge construction builds upon an internal permutation and is parametrized by two values: the rate r (throughput) and the capacity c (security level). The state width is t = r + c. The initial state contains all zeros: I = 0^r \| 0^c.
If the internal permutation is modeled as a randomly chosen permutation, the sponge function is indifferentiable from a random oracle for up to |\mathbb{F}|^{c/2} calls. A sponge hash function with capacity c can therefore provide 2^{c/2} bits of collision and preimage resistance.
A sponge is parametrized by a rate r, a capacity c, and an internal permutation over \mathbb{F}^t where t = r + c. Message blocks are absorbed into the rate portion, the permutation is applied between each block, and output is squeezed from the rate.
2.2 The HADES Design Strategy
Cryptographic permutations usually consist of an efficient round function applied sufficiently many times. HADES mixes rounds with full S-box layers and rounds with partial S-box layers. Full layers are expensive in ZK proof systems but protect against statistical attacks; partial layers are cheap but similarly effective against algebraic attacks.
The structure is: R_f full rounds at the beginning, R_P partial rounds in the middle (only 1 S-box per round), and R_f full rounds at the end. The total number of full rounds is R_F = 2 \cdot R_f.
The HADES design strategy configures the permutation with three phases: R_f full rounds, R_P partial rounds, then R_f full rounds.
Each round function consists of three operations applied in sequence:
- AddRoundConstants (ARC): add round-specific constants to each state element
- SubWords (S-box): apply the nonlinear S-box layer
- MixLayer (M): multiply the state by the MDS matrix
A full round applies the S-box to every state element; a partial round applies it only to the first element.
2.3 Components
The S-Box Layer. The S-box is defined as the power map \text{S-box}(x) = x^\alpha, where \alpha \geq 3 is the smallest positive integer satisfying \gcd(\alpha, p-1) = 1. The coprimality condition ensures the power map is a permutation over \mathbb{F}_p. The common choice is \alpha = 5, suitable for BLS12-381, BN254, and Ed25519 scalar fields.
A valid S-box exponent satisfies \alpha \geq 3 and \gcd(\alpha, p-1) = 1. The S-box function maps x \mapsto x^\alpha.
The Linear Layer. A t \times t MDS (Maximum Distance Separable) matrix with elements in \mathbb{F}_p exists when 2t + 1 \leq p. MDS matrices ensure full diffusion: every output element depends on every input element. One construction uses a Cauchy matrix: \mathcal{M}_{i,j} = 1/(x_i + y_j), where the sequences \{x_i\} and \{y_j\} are pairwise distinct.
A matrix is MDS if every square submatrix has nonzero determinant. Cauchy matrices are always MDS.
The Full Poseidon Hash. Poseidon bundles the HADES configuration with an MDS matrix, round constants, and sponge parameters. The permutation Poseidon^\pi applies R_f full rounds, then R_P partial rounds, then R_f full rounds. The hash function instantiates a sponge with this permutation.
Full configuration for a Poseidon instance, combining HADES, MDS matrix, round constants, and sponge parameters.
Domain Separation. The capacity element encodes the use case to prevent cross-domain attacks. Poseidon defines domain tags for Merkle trees, variable- and constant-length hashing, and encryption.
3. Applications
Poseidon is suggested for all applications of zero-knowledge-friendly hashing:
- Commitments: single-call permutation-based hashing with POSEIDON-128. Faster than Pedersen Hash and usable in signature schemes.
- Variable-length hashing: sponge-based hashing with POSEIDON-128 or POSEIDON-80 (width 5, rate 4).
- Merkle trees: recommended arity 4 (width 5) with POSEIDON-128 for highest ZK performance. Trees of arity 2 and other arities are also supported.
- Verifiable encryption: Poseidon inside the DuplexSponge authenticated encryption framework, initialized with a session key based on the recipient's public key.
Third-party protocols using Poseidon include Filecoin (Merkle tree proofs), Dusk Network (Zcash-like protocol for securities trading), Sovrin (Merkle-tree based revocation), and Loopring (private trading on Ethereum).
4. Concrete Instances
The primary instances use S-box f(x) = x^5 over the scalar fields of BLS12-381, BN254, and Ed25519 (all approximately 2^{255} in size). The round numbers include a security margin: +2 on R_F and +7.5% on R_P.
| Instance | t | R_F | R_P | Lean |
|---|---|---|---|---|
| POSEIDON^\pi-128 | 3 | 8 | 57 | poseidon128_t3 |
| POSEIDON^\pi-128 | 5 | 8 | 60 | poseidon128_t5 |
| POSEIDON^\pi-80 | 3 | 8 | 33 | poseidon80_t3 |
| POSEIDON^\pi-80 | 5 | 8 | 35 | poseidon80_t5 |
| POSEIDON^\pi-256 | 6 | 8 | 120 | poseidon256_t6 |
| POSEIDON^\pi-256 | 10 | 8 | 120 | poseidon256_t10 |
Round constants and MDS matrices are generated deterministically using the Grain LFSR in self-shrinking mode, providing the NUMS (Nothing-Up-My-Sleeve) property. See Appendix E.
5. Security Analysis
The security of Poseidon relies on choosing the number of rounds so that the internal permutation does not exhibit non-generic properties relevant to collision or preimage attacks faster than 2^M queries. The analysis considers both statistical attacks (differential, linear, truncated differential, rebound) and algebraic attacks (interpolation, Groebner basis, higher-order differential).
5.1 Security Definitions
The paper defines five security notions for hash functions and permutations, all formalized in Lean.
The function F is T-secure against collisions if there is no algorithm with expected complexity smaller than T that finds x_1 \neq x_2 with F(x_1) = F(x_2).
The function F is T-secure against preimages if there is no algorithm with expected complexity smaller than T that, given y, finds x with F(x) = y.
Given x_1, no algorithm finds x_2 with F(x_1) = F(x_2) in fewer than T steps.
The invertible function P is T-secure against the CICO (m_1, m_2)-problem if no algorithm with expected complexity smaller than T can, given partial input/output constraints, find the remaining values such that P(I_1 \| I_2) = O_1 \| O_2.
A collection of K disjoint sets \{X_1, \ldots, X_K\} such that for each set X_i: \sum_{x \in X_i} x = \sum_{x \in X_i} P(x) = 0. The authors explicitly do not claim security against zero-sum partitions, citing the gap between distinguishable rounds and attackable rounds (cf. full KECCAK-f is distinguishable but only 6-round KECCAK can be attacked).
5.2 Security Claims
POSEIDON-M is 2^M-secure against collisions and (second) preimages.
Poseidon^\pi is 2^{\min(M, m_1, m_2)}-secure against the CICO (m_1, m_2)-problem.
5.3 Statistical Attacks
At least 6 rounds with full S-box layers are necessary to provide security against differential and linear attacks. Specifically, for R_F < 6 when M \leq (\lfloor \log_2 p \rfloor - \mathcal{C}) \cdot (t+1) (where \mathcal{C} = \log_2(\alpha - 1)), or R_F < 10 otherwise, attacks may be possible. Truncated differentials with probability 1 cover at most a single round; 4 full rounds suffice against them, and 6 full rounds suffice against rebound attacks.
The choice of the MDS matrix (Section 2.3) prevents the existence of subspaces that generate infinitely long subspace trails with inactive S-boxes. For any MDS matrix, no such trail can cover more than t - 1 partial rounds.
\mathcal{S}^{(i)} := \{ v \in \mathbb{F}^t \mid [\mathcal{M}^j \cdot v]_0 = 0, \; j < i \}, where \dim(\mathcal{S}^{(i)}) \geq t - i.
5.4 Algebraic Attacks
The algebraic degree D_\alpha(r) of r-round Poseidon^\pi with S-box x^\alpha is at most \alpha^r, and is expected to reach this bound regardless of whether full or partial rounds are used.
Interpolation Attack. The attack constructs an interpolation polynomial describing the function. For a security level of M bits, the number of rounds that can be attacked is R \leq \lceil \log_\alpha(2) \cdot \min\{M, \log_2(p)\} \rceil + \lceil \log_\alpha(t) \rceil.
Groebner Basis Attack. One tries to solve a system of nonlinear equations describing the function. Three conditions, any of which allows an attack faster than 2^M:
- R_F + R_P \leq \log_\alpha(2) \cdot \min\{M, \log_2(p)\}
- R_F + R_P \leq t - 1 + \log_\alpha(2) \cdot \min\{M/(t+1), \log_2(p)/2\}
- (t-1) \cdot R_F + R_P \leq t - 2 + M / (2 \cdot \log_2(\alpha))
The round numbers must exceed all three bounds to ensure security.
5.5 Round Number Propositions
The following propositions give the minimum round numbers (before adding the security margin) for each security level. After adding +2 on R_F and +7.5% on R_P, these yield the concrete instances in Section 4.
With \alpha = 5, M = 128, \log_2(p) \approx 255: the minimum rounds before margin are R_F = 6, R = R_F + R_P = 56 + \lceil \log_5(t) \rceil. After margin: R_F = 8, R_P = 57 (t = 3).
With \alpha = 5, M = 80: minimum R_F = 6, R = R_F + R_P = 35 + \lceil \log_5(t) \rceil. After margin: R_F = 8, R_P = 33 (t = 3).
With \alpha = 5, M = 256: minimum R_F = 6, R = R_F + R_P = 111 + \lceil \log_5(t) \rceil. After margin: R_F = 8, R_P = 120 (t = 6).
5.6 Security Margin
Given the minimum number of rounds necessary for security, the authors add:
- Two more rounds with full S-box layers (+2 R_F)
- 7.5% more rounds with partial S-box layers (+7.5% R_P)
6. POSEIDON in Zero-Knowledge Proof Systems
The hash functions have been designed to be friendly to zero-knowledge applications. Specifically, the goal is to minimize the proof generation time, the proof size, and the verification time. A single hash function cannot be optimal for all ZK proof systems because they use different arithmetizations: STARKs can use prime and binary fields, Bulletproofs uses any prime field, whereas most SNARKs use a prime field based on a scalar field of a pairing-friendly elliptic curve. Therefore, for each proof system a new instance of POSEIDON may be needed.
6.1 State of the Art
Let \mathcal{P} be a circuit over some finite field \mathbb{F} where gates are low-degree polynomials. The computational integrity problem consists of proving that some given O_0 is the result of executing \mathcal{P} over some I_0. It is not difficult to show that any limited-time program on a modern CPU can be converted to such a circuit [BCTV14], and making the proof zero-knowledge is often possible with little overhead.
The first generation of SNARKs (Pinocchio [PHGR13], Groth16 [Gro16]) require a separate trusted setup for each circuit. The next generation (Sonic [MBKM19], PLONK [GWC19], Marlin [CHM+20]) can use one reference string of size d for all circuits with at most d gates. Later, proof systems without trusted setups appeared: Bulletproofs [BBB+18] (short proofs, linear verifier), STARKs [BBHR19] (post-quantum, iterative programs), and RedShift [KPV19] (STARK-inspired, large proofs). Current benchmarks demonstrate that programs with millions of gates can be processed within a few seconds.
The bottleneck of privacy-preserving applications (Zcash, Ethereum mixers) is the proof creation time, which took 42 seconds in the early version of Zcash. Both prover and verifier performance are determined by the size of the circuit that describes a Merkle proof, and thus dependent on the hash function constituting the tree.
6.2 SNARKs with Poseidon^\pi
In SNARKs, the prime field is typically the scalar field of a pairing-friendly elliptic curve. After p is fixed, we check if x^\alpha is invertible in \text{GF}(p), which is true if p \bmod \alpha \neq 1. The S-box x^3 requires 2 constraints and x^5 requires 3 constraints in R1CS. The total constraint count is:
- 2tR_F + 2R_P constraints for x^3-POSEIDON^\pi
- 3tR_F + 3R_P constraints for x^5-POSEIDON^\pi
No additional constraints are needed because linear layers and round constants can be incorporated. In the sponge mode, with 2M bits reserved for capacity, the constraints per bit are \frac{3tR_F + 3R_P}{N - 2M} for x^5-POSEIDON^\pi.
6.2.1 Groth16
Groth16 [Gro16] is an optimization of Pinocchio and currently the fastest SNARK with the smallest proofs. Its prover complexity is O(s), where s is the number of rank-1 constraints. Each full round with a full S-box layer is represented by constraints that incorporate the MDS matrix \mathcal{M}. In partial rounds, only one S-box constraint is needed; the remaining t - 1 linear constraints can be composed with constraints from adjacent rounds.
Table 3. libsnark [SCI] performance of the POSEIDON preimage prover (one permutation call). Intel Core i7-8700 CPU @3.2 GHz, 32 GiB RAM.
| Field | Arity (t) | Prove | Verify | R1CS |
|---|---|---|---|---|
| BN254 | 2:1 (3) | 43.1 ms | 1.2 ms | 276 |
| 4:1 (5) | 57.9 ms | 1.1 ms | 440 | |
| BN254 | 2:1 (3) | 32.8 ms | 1.2 ms | 180 |
| 4:1 (5) | 46.9 ms | 1.1 ms | 290 |
Top rows: Poseidon-128. Bottom rows: Poseidon-80.
6.2.2 Bulletproofs
Bulletproofs [BBB+18] is a proof system without trusted setup, notable for logarithmic proof sizes and the shortest range proofs without a trusted setup. However, its verifier is linear in the program size. The Bulletproofs library "dalek" is among the most popular ZK primitives. The authors implemented a Merkle tree prover for POSEIDON in Bulletproofs using the same R1CS constraint system as for Groth16.
Table 5. Bulletproofs performance to prove 1 out of 2^{30}-element Merkle tree (Poseidon-128).
| Field | Arity | Prove | Verify | R1CS |
|---|---|---|---|---|
| BLS12-381 | 2:1 | 16.8 s | 1.5 s | 7290 |
| 4:1 | 13.8 s | 1.65 s | 4500 | |
| 8:1 | 11 s | 1.4 s | 4050 | |
| BN254 | 2:1 | 11.2 s | 1.1 s | 7290 |
| 4:1 | 9.6 s | 1.15 s | 4500 | |
| 8:1 | 7.4 s | 1.0 s | 4050 | |
| Ristretto | 2:1 | 8.4 s | 0.78 s | 7290 |
| 4:1 | 6.45 s | 0.72 s | 4500 | |
| 8:1 | 5.25 s | 0.76 s | 4050 | |
| SHA-256 [BBB+18] | 582 s | 21 s | 762000 | |
6.2.3 PLONK
PLONK [GWC19] is a SNARK using a universal trusted setup, where a structured reference string of size d serves any circuit of d gates or less. The standard version works with R1CS constraints plus special machinery for wire layout. The prover complexity for a Poseidon^\pi permutation with S-box x^5 of width w and R rounds is 11(w(w+6)+3)R point multiplications, and the proof has 7 group elements and 7 field elements.
The authors suggest optimizations for POSEIDON's near-identical rounds in PLONK: (1) define a separate polynomial for each S-box line, (2) eliminate wire layout polynomials, (3) express round transitions as affine equations over polynomial values at adjacent points. This reduces the prover to only (w + 11)R point multiplications, with proofs of (w + 3) group elements and 2w field elements — a 25–40x increase in performance depending on w.
Table 6. PLONK performance to prove 1-out-of-2^n-Merkle tree of arity 4 (Poseidon-128 over BLS12-381). Third-party non-optimized Rust implementation, Intel i5-7300HQ @2.50 GHz.
| Set size | Prove | Verify | R1CS |
|---|---|---|---|
| 2^{16} | 3.59 s | 0.7 ms | 2400 |
| 2^{34} | 6.3 s | 1.55 ms | 5100 |
| 2^{68} | 9.9 s | 2.7 ms | 10200 |
6.2.4 RedShift
RedShift [KPV19] is a STARK-inspired proof system which works with an arbitrary set of constraints. It can be viewed as PLONK with pairing-based polynomial commitments replaced by Reed-Solomon trustless commitments. The RedShift proof size is c_\lambda \log d^2 KB, where d is the degree of circuit polynomials and c_\lambda \approx 2.5 for 120-bit security. The same optimizations as in PLONK apply, so the entire Merkle tree proof requires polynomials of degree 4800 for width 5, resulting in proofs around 12 KB in size.
6.3 Comparison with Other Hash Algorithms
For all systems considered, the prover performance increases monotonically (and in practice almost linearly) with the number of multiplications or equivalently the number of R1CS constraints. The following table provides a summary of constraint counts for a Merkle tree with 2^{30} elements.
Table 4. Number of R1CS constraints for a circuit proving leaf knowledge in a Merkle tree of 2^{30} elements.
| Hash | Arity | Width | R_F | R_P | Total |
|---|---|---|---|---|---|
| Poseidon-128 | 2:1 | 3 | 8 | 57 | 7290 |
| 4:1 | 5 | 8 | 60 | 4500 | |
| 8:1 | 9 | 8 | 63 | 4050 | |
| Rescue-x^5 | 2:1 | 3 | 16 | — | 8640 |
| 4:1 | 5 | 10 | — | 4500 | |
| 8:1 | 9 | 10 | — | 5400 | |
| Pedersen hash | — | 41400 | |||
| SHA-256 | — | 826020 | |||
| Blake2s | — | 630180 | |||
| MiMC-2p/p | 1:1 | 2 | 324 | — | 19440 |
POSEIDON and Rescue have the fastest provers among the compared hash functions, which is also confirmed for the STARK case [BSGL20]. However, Rescue has slower performance in the non-ZK case (Table 1).
6.4 STARKs with Poseidon^\pi
ZK-STARKs [BBHR19] is a proof system for computational integrity which is not vulnerable to quantum computers and does not use a trusted setup. STARKs operate with programs whose internal state is represented as w registers, each belonging to a 2^n-subgroup \mathbb{G} of a prime-order group. The program execution is represented as T internal states. The prover complexity is 8w \cdot T \cdot d \cdot \log(wT) operations in \mathbb{G}.
Poseidon^\pi can be represented with few registers, a small number of steps, and low degree. Setting w = t, we get T = R_F + \lceil R_P / t \rceil and wT = tR_F + R_P. The AET cost is:
- 24(tR_F + R_P) \cdot \log_2(tR_F + R_P) operations in \mathbb{G} for the prover
- Prover memory in \Omega(63 \cdot (tR_F + R_P))
- Communication (verifier time) of 63 \cdot (t + \log_2^2(24(tR_F + R_P)))
For the primary instance Poseidon-128 with width 3, the AET cost is 20540 per permutation call, yielding 40 operations per bit over 510 bits. For width 5, the AET cost is 38214, or 38 operations per bit.
7. Acknowledgements
This work is partially supported by the Ethereum Foundation, Starkware Ltd, and IOV42 Ltd. The authors thank Alexander Vlasov, Lovesh Harshandani, and Carlos Perez for benchmarking POSEIDON in various environments.
Appendix A. Auxiliary Files
The following files are provided as supplementary material:
-
generate_params_poseidon.sage— calculate round numbers, generate round constants and matrices -
poseidonperm_x5_254_3.sage,poseidonperm_x5_254_5.sage,poseidonperm_x5_255_3.sage,poseidonperm_x5_255_5.sage— reference implementations and test vectors -
test_vectors.txt— test vectors -
poseidonperm_x3_64_24_optimized.sage— optimized x^3-POSEIDON^\pi using the modifications from Appendix B
All supplementary files are available at
https://extgit.iaik.tugraz.at/krypto/hadeshash
.
Appendix B. Efficient Implementation
The partial nonlinear layer in R_P rounds can be used to reduce the size of round constants and the number of constant multiplications. The main advantage reduces multiplications from t^2 to 2t per partial round, which is particularly useful for large t and R_P.
Round Constants
In an SPN, one can swap the order of the linear layer and round constant addition (both being linear operations). For round constant c^{(i)}, the equivalent constant is \hat{c}^{(i)} = MC^{-1}(c^{(i)}), where MC is the linear layer. By splitting constants into the S-box part and the identity part, and moving the identity part through successive rounds, one obtains a representation where constants are only added to S-box outputs, apart from one constant applied to the entire state after the first R_f full rounds.
Linear Layer
For rounds with a single S-box, the t \times t MDS matrix \mathcal{M} decomposes as \mathcal{M} = \mathcal{M}' \times \mathcal{M}'', where:
- \mathcal{M}' is block-diagonal with (1) and \hat{\mathcal{M}} (the (t-1) \times (t-1) MDS submatrix)
- \mathcal{M}'' is sparse with \hat{w} = \hat{\mathcal{M}}^{-1} \times w and an identity block, having t^2 - 3t + 2 zero entries and t - 1 entries equal to one
By swapping the S-box layer and \mathcal{M}', each linear layer in the partial rounds reduces to multiplication by the sparse matrix \mathcal{M}'', greatly reducing operations. For example, x^3-Poseidon^\pi with (n,t,R_F,R_P)=(64,24,8,42) improves performance by about 5x (4 ms average in Sage).
Appendix C. Security Analysis: x^\alpha-Poseidon^\pi
The following analysis assumes x \mapsto x^\alpha is invertible (\gcd(\alpha, p-1) = 1). This is more tailored than the HADESMiMC analysis, as POSEIDON uses unkeyed permutations in a sponge function (no MitM approaches apply). The analysis considers settings with \chi < t input/output words, reflecting the sponge attacker model.
C.1 Statistical Attacks
The results for impossible differentials, the multiple-of-8 property, mixture differentials, and integral distinguishers are equivalent to those for HADESMiMC [GLR+20].
C.1.1 Differential Cryptanalysis
The cube function f(x) = x^3 is an almost perfect nonlinear (APN) permutation with differential probability bounded by 2/|\mathbb{F}_p|. POSEIDON^\pi is secure against differential cryptanalysis if each differential has probability at most p^{-t}. Working with the "weaker" permutation R^{R_f} \circ L \circ R^{R_f} (where L is an invertible linear layer), the minimum number of active S-boxes over R^s \circ L \circ R^r is at least (\lfloor s/2 \rfloor + \lfloor r/2 \rfloor) \cdot (t+1) plus end-of-round corrections. For S(x) = x^5, the bound DP_{\max} = 4/p applies, and R_F \geq 6 suffices.
C.1.2 Linear Cryptanalysis
The maximum square correlation of the cube function is 2/p [AABL12], providing optimal resistance against linear cryptanalysis with the same round numbers as for differential attacks.
C.1.3 Truncated Differential
Probability-1 truncated differentials cover at most a single round of POSEIDON^\pi (e.g., [\alpha, 0, \ldots, 0]^T \xrightarrow{R(\cdot)} \mathcal{M} \times [\beta, 0, \ldots, 0]^T). The next S-box layer destroys these linear relations. Four rounds with full S-box layers suffice for security.
C.1.4 Rebound Attacks
Rebound attacks [LMR+09, MRST09] have an inbound phase placed in the middle of the permutation and outbound phases at either end. The best rebound attack on AES covers 8 rounds. Since (1) one round of POSEIDON^\pi provides full diffusion (vs. 2 rounds for AES) and (2) the best truncated differential covers 1 round (vs. 3 for AES), 6 rounds with full S-box layers suffice.
C.1.5 Invariant Subspace Attack
Let K_{\text{weak}} be a set of keys and k \in K_{\text{weak}}. The subspace U generates an invariant subspace trail of length r for F_k(\cdot) \equiv F(\cdot) \oplus k if for each i = 1, \ldots, r there exists A_i \subseteq U^c such that \forall a_i \in A_i, \exists a_{i+1} \in A_{i+1} with F_{k^i}(U \oplus a_i) = U \oplus a_{i+1}.
Let (U_1, U_2, \ldots, U_{r+1}) be subspaces with \dim(U_i) \leq \dim(U_{i+1}). If for each i and each a_i there exists a_{i+1} such that F(U_i \oplus a_i) \subseteq U_{i+1} \oplus a_{i+1}, then this is a subspace trail of length r. If all hold with equality, it is a constant-dimensional subspace trail.
For full S-box layers, random round constants provide protection [BCLR17]. For partial S-box layers, a subspace trail can always be constructed for t - 1 rounds without activating any S-box, but due to the matrix choice in Section 2.3, t - 1 is also an upper bound.
C.2 Algebraic Attacks
C.2.1 Interpolation Attack
The interpolation attack [JK97] constructs a polynomial representation of the function. For \chi unknown input words, the number of monomials is estimated as (D_\alpha(R) + 1)^\chi. Requiring this to be close to \min\{2^M, p^\chi\}, the number of rounds must satisfy R \geq \min\{M, \log_\alpha(p)\}. Additionally, the polynomial must be dense, requiring 1 + \lceil \log_\alpha(p) \rceil + \lceil \log_\alpha(t) \rceil rounds. The backward direction (using x^{1/\alpha}) has higher degree, so the forward attack dominates. The MitM variant does not apply since the attacker sees only part of the output in the sponge setting.
The total round requirement is: R_P + R_F \geq 1 + \lceil \log_\alpha(2) \cdot \min\{M, \log_2(p)\} \rceil + \log_\alpha(t).
C.2.2 Groebner Basis Attack
The Groebner basis attack consists of (1) computing the basis in degrevlex order, (2) converting to lexicographic order, and (3) factorizing the univariate polynomial. The complexity for a system of \mathcal{N} polynomials in \mathcal{V} variables is O\left(\binom{\mathcal{V} + D_{\text{reg}}}{D_{\text{reg}}}\right)^\omega, where D_{\text{reg}} is the degree of regularity and 2 \leq \omega < 3 is the linear algebra constant.
Full-permutation equations: For \chi = 1 (one equation), root finding costs D \cdot \log_2(D)^2, giving r \leq \log_\alpha(2) \cdot \min\{M, \log_2(p)\}. For \chi \geq 2, the cost is at least \alpha^{2r\chi}, optimized at \chi = 2.
Exploiting \mathcal{S}^{(i)}: The subspace of texts with no active S-boxes over r partial rounds allows replacing nonlinear equations with linear ones. Due to the matrix assumption in Section 2.3, this covers at most t - 1 partial rounds, leading to R_F + R_P \geq t - 1 + \min\left\{\frac{\log_\alpha(2) \cdot M}{t+1}, \frac{\log_\alpha(2) \cdot \log_2(p)}{2}\right\}.
Round-level equations: Using degree-\alpha equations per S-box, the regularity is D_{\text{reg}} \approx 1 + (\alpha - 1)((t-1)R_F + R_P), giving (t-1)R_F + R_P \geq (t-2) + \frac{M}{2 \log_2(\alpha)}.
Follow-up [ABM23]: The system is not regular, giving a better estimate D_{\text{reg}} \approx r \cdot R_F/2 + R_P + \alpha. However, this does not affect instances currently in practice (t \in \{3, 5\} for SNARKs, t \in \{12, 24\} for FRI-based approaches).
Appendix D. Compact Constraints for STARKs and SNARKs
When t is relatively small compared to R_P, constraints can be generated for S-boxes that depend on only a few variables. Let A_r^i denote the ARK outputs in round r and B_r^i the MDS inputs. In full rounds, S(A_r^i) = B_r^i; in partial rounds, S(A_r^t) = B_r^t and A_r^i = B_r^i for i < t.
By working with two consecutive segments of t partial rounds, expressing intermediate values as affine functions, and substituting B_j^t \leftarrow S(A_j^t), a system P_1 of t degree-d polynomial constraints is obtained on 2t S-box input variables. This system is constant-independent (depending on r only in the constant term).
The resulting total for the entire permutation is tR_F + R_P - t constraints of degree d, structured as:
- First full rounds: t(R_F/2 - 1) constraints
- Bridge (last full ↔ first t partial): t constraints
- All R_P partial rounds: R_P constraints (grouped in blocks of t)
- Bridge (last t partial ↔ first full): t constraints
- Last full rounds: t(R_F/2 - 1) constraints
Appendix E. Grain LFSR Parameter Generation
Round constants and MDS matrices are generated deterministically using the Grain LFSR in self-shrinking mode. The 80-bit initial state encodes the Poseidon instance parameters (field type, S-box type, field size, state width, round numbers).
The generation process:
- Initialize the 80-bit LFSR with instance parameters.
- Update using the feedback polynomial: b_{i+80} = b_{i+62} \oplus b_{i+51} \oplus b_{i+38} \oplus b_{i+23} \oplus b_{i+13} \oplus b_i.
- Discard the first 160 bits.
- Use self-shrinking mode: evaluate bits in pairs. If the first bit is 1, output the second; otherwise discard both.
- Reject samples \geq p.
Appendix F. Concrete Instances with Security Margin
Concrete instances for x^3-POSEIDON^\pi and x^5-POSEIDON^\pi, including the security margin, are given in Tables 7 and 8.
Table 7. Concrete instances for x^3-Poseidon^\pi over \mathbb{F}_p, where S-box(x) = x^3.
| M | N | n | t | R_F | R_P | Cost |
|---|---|---|---|---|---|---|
| 128 | 1536 | 768 | 2 | 8 | 83 | 99 |
| 128 | 1536 | 384 | 4 | 8 | 84 | 116 |
| 128 | 1536 | 256 | 6 | 8 | 84 | 132 |
| 256 | 1536 | 768 | 2 | 8 | 170 | 186 |
| 256 | 1536 | 384 | 4 | 8 | 171 | 203 |
| 256 | 1536 | 256 | 6 | 8 | 171 | 219 |
Table 8. Concrete instances for x^5-POSEIDON^\pi over \mathbb{F}_p, where S-box(x) = x^5.
| M | N | n | t | R_F | R_P | Cost |
|---|---|---|---|---|---|---|
| 128 | 1536 | 768 | 2 | 8 | 56 | 72 |
| 128 | 1536 | 384 | 4 | 8 | 56 | 88 |
| 128 | 1536 | 256 | 6 | 8 | 57 | 105 |
| 256 | 1536 | 768 | 2 | 8 | 116 | 132 |
| 256 | 1536 | 384 | 4 | 8 | 116 | 148 |
| 256 | 1536 | 256 | 6 | 8 | 117 | 165 |
Appendix G. Selecting Number of Rounds in General Case
The design goal is to minimize R1CS costs. For a fixed S-box function, the minimum costs are delivered by the smallest number of S-boxes, though the field size also plays a role. For each combination (security level M, field type, S-box size, S-box function), the number of S-boxes is minimized subject to the constraints of Eq. (3) and Eq. (4).
The cost function to minimize is: \text{number of S-boxes} = t \cdot R_F + R_P, where t \geq 2. The procedure:
- Choose S(x) = x^\alpha using the smallest \alpha such that \gcd(\alpha, p-1) = 1
- Select minimum R_F for statistical attack security (at least R_F = 6)
- Select R_P that minimizes tR_F + R_P subject to algebraic attack bounds
A script is provided to calculate the optimal round numbers, using the security margin from Section 5.
Appendix H. Merkle Tree Instances of POSEIDON
POSEIDON instances with width t are used for Merkle trees with arity t - c where c is the capacity (at word level). In the prime field setting with 128-bit security and a 256-bit field, c = 1 and the arity is t - 1.
A tree node may have 0 to t - c child elements. Missing children are denoted by \emptyset. The node hash function \widehat{H} maps \widehat{\mathbb{F}}^{t-c} to \mathbb{F}^c, where \widehat{\mathbb{F}} = \mathbb{F} \cup \{\emptyset\}. A missing subtree of depth d has hash \widehat{H}^d_\emptyset = \widehat{H}(\widehat{H}^{d-1}_\emptyset, \ldots, \widehat{H}^{d-1}_\emptyset).
The capacity element encodes a bitmask of which leaves are present, using the Iverson bracket notation. For variable-length sponge instances, messages are padded with a single 1 \in \mathbb{F} and then zero elements to reach a multiple of t - c.
Appendix I. About STARKAD (Currently Dismissed)
Dismissed variant
STARKAD and all binary field variants are considered dismissed. "Weaker" versions have been broken in [KR21, BCD+20]. The authors advise against using them.
STARKAD is the binary field counterpart of POSEIDON, constructed by instantiating a sponge with the STARKAD^\pi permutation. The differences from POSEIDON^\pi are: (1) it operates over \mathbb{F}_{2^n}^t instead of a prime field, and (2) the S-box exponent \alpha must satisfy \gcd(\alpha, 2^n - 1) = 1.
The security analysis is similar to POSEIDON, but higher-order differential attacks are expected to be more effective over binary fields. The MDS matrices originally proposed for STARKAD were weak (their squares were multiples of the identity), a weakness exploited in [KR21, BCD+20].
Table 9. Old parameter sets for STARKAD with S-box(x) = x^3 (with security margin). These round numbers are not claimed to be secure.
| M | N | n | t | R_F | R_P | Field |
|---|---|---|---|---|---|---|
| 128 | 1512 | 63 | 24 | 8 | 45 | \mathbb{F}_{2^n} |
| 128 | 1551 | 33 | 47 | 8 | 25 | \mathbb{F}_{2^n} |
| 256 | 1512 | 63 | 24 | 8 | 45 | \mathbb{F}_{2^n} |
Appendix J. About x^{-1}-POSEIDON (Currently Dismissed)
Dismissed variant
The inverse S-box variant of POSEIDON (x \mapsto x^{-1}) is considered dismissed. Mistakes in the security analysis have been found, and no known application uses this version. The authors advise against using it.
Besides x^\alpha-POSEIDON^\pi, a version with S-box x \mapsto x^{-1} was proposed in the previous version [GKR+21]. The only difference regards the S-box details. Old parameter sets are listed in Table 10 for reference.
Table 10. Old x^{-1}-POSEIDON over \mathbb{F}_p^t (with security margin). These round numbers are not claimed to be secure.
| M | N | n | t | R_F | R_P | Cost |
|---|---|---|---|---|---|---|
| 128 | 1536 | 768 | 2 | 8 | 65 | 81 |
| 128 | 1536 | 256 | 6 | 8 | 57 | 105 |
| 256 | 1536 | 768 | 2 | 8 | 134 | 150 |
| 256 | 1536 | 256 | 6 | 8 | 126 | 174 |
Caveats
No claim on zero-sum partitions
The authors do not claim security against zero-sum partitions, citing the gap between distinguishable rounds and attackable rounds (cf. full KECCAK-f is distinguishable but only 6-round KECCAK can be attacked).
STARKAD and x^{-1}-POSEIDON dismissed
The binary field variant (STARKAD) and the inverse S-box variant are dismissed due to discovered weaknesses.
Groebner basis degree of regularity
The result from [ABM23] showing the degree of regularity is overestimated does not affect instances currently used in practice (t \in [3, 5] for SNARKs, t \in [12, 24] for FRI-based approaches).
References
- [GKRRS19] Grassi, Khovratovich, Rechberger, Roy, Schofnegger. POSEIDON: A New Hash Function for Zero-Knowledge Proof Systems (Updated Version). eprint 2019/458 .
- [GKR+21] Grassi, Khovratovich, Rechberger, Roy, Schofnegger. POSEIDON: A New Hash Function for Zero-Knowledge Proof Systems. USENIX Security 2021, pp. 519-535.
- [GLR+20] Grassi, Luftenegger, Rechberger, Rotaru, Schofnegger. On a Generalization of Substitution-Permutation Networks: The HADES Design Strategy. EUROCRYPT 2020, LNCS 12106, pp. 674-704. [page on this site]
- [BDPA08] Bertoni, Daemen, Peeters, Van Assche. On the Indifferentiability of the Sponge Construction. EUROCRYPT 2008, LNCS 4965.
- [BDPA11] Bertoni, Daemen, Peeters, Van Assche. Duplexing the Sponge: Single-Pass Authenticated Encryption. SAC 2011, LNCS 7118.
- [GRS21] Grassi, Rechberger, Schofnegger. Proving Resistance Against Infinitely Long Subspace Trails. IACR Trans. Symmetric Cryptol., 2021(2):314-352.
- [BCD+20] Beyne, Canteaut, Dinur et al. Out of Oddity — New Cryptanalytic Techniques against Symmetric Primitives Optimized for Integrity Proof Systems. CRYPTO 2020, LNCS 12172. [page on this site]
- [KR21] Keller, Rosemarin. Mind the Middle Layer: The HADES Design Strategy Revisited. EUROCRYPT 2021, LNCS 12697. [page on this site]
- [ABM23] Ashur, Buschman, Mahzoun. Algebraic Cryptanalysis of POSEIDON. IACR ePrint 2023/537.
- [HJMM08] Hell, Johansson, Maximov, Meier. The Grain Family of Stream Ciphers. eSTREAM Finalists, LNCS 4986.
- [Gro16] Groth. On the Size of Pairing-Based Non-Interactive Arguments. EUROCRYPT 2016, LNCS 9666.
- [BBB+18] Bunz, Bootle, Boneh et al. Bulletproofs: Short Proofs for Confidential Transactions and More. IEEE S&P 2018.
- [BBHR19] Ben-Sasson, Bentov, Horesh, Riabzev. Scalable Zero Knowledge with No Trusted Setup. CRYPTO 2019, LNCS 11694.
- [GWC19] Gabizon, Williamson, Ciobotaru. PLONK: Permutations over Lagrange-Bases for Oecumenical Noninteractive Arguments of Knowledge. ePrint 2019/953. [page on this site]
- [PHGR13] Parno, Howell, Gentry, Raykova. Pinocchio: Nearly Practical Verifiable Computation. IEEE S&P 2013.
- [CHM+20] Chiesa, Hu, Maller et al. Marlin: Preprocessing zkSNARKs with Universal and Updatable SRS. EUROCRYPT 2020.
- [KPV19] Kattis, Panarin, Vlasov. RedShift: Transparent SNARKs from List Polynomial Commitment IOPs. ePrint 2019/1400.
- [MBKM19] Maller, Bowe, Kohlweiss, Meiklejohn. Sonic: Zero-Knowledge SNARKs from Linear-Size Universal and Updatable Structured Reference Strings. CCS 2019.
- [BCTV14] Ben-Sasson, Chiesa, Tromer, Virza. Succinct Non-Interactive Zero Knowledge for a von Neumann Architecture. USENIX Security 2014.
- [AGR+16] Albrecht, Grassi, Rechberger et al. MiMC: Efficient Encryption and Cryptographic Hashing with Minimal Multiplicative Complexity. ASIACRYPT 2016, LNCS 10031.
- [ARS+15] Albrecht, Rechberger, Schneider et al. Ciphers for MPC and FHE. EUROCRYPT 2015, LNCS 9056.
- [RDP+96] Rijmen, Daemen, Preneel et al. The Cipher SHARK. FSE 1996, LNCS 1039.
- [AABS+19] Aly, Ashur, Ben-Sasson et al. Design of Symmetric-Key Primitives for Advanced Cryptographic Protocols. ePrint 2019/426.
- [HBHW19] Hopwood, Bowe, Hornby, Wilcox. Zcash Protocol Specification. 2019.
- [BSGL20] Ben-Sasson, Goldberg, Levit. STARK Friendly Hash — Survey and Recommendation. ePrint 2020/948.
- [JK97] Jakobsen, Knudsen. The Interpolation Attack on Block Ciphers. FSE 1997, LNCS 1267.
- [BCLR17] Beierle, Canteaut, Leander, Rotella. Proving Resistance Against Invariant Attacks: How to Choose the Round Constants. CRYPTO 2017, LNCS 10402.
- [DKP+19] Dinur, Kales, Promitzer et al. Linear Equivalence of Block Ciphers with Partial Non-Linear Layers. EUROCRYPT 2019, LNCS 11476.
- [KZG10] Kate, Zaverucha, Goldberg. Constant-Size Commitments to Polynomials and Their Applications. ASIACRYPT 2010, LNCS 6477.
- [SCI] SCIPR Lab. C++ Library for zkSNARKs (libsnark).
- [BS91] Biham, Shamir. Differential Cryptanalysis of DES-like Cryptosystems. J. Cryptology, 4(1):3-72, 1991.
- [LMR+09] Lamberger, Mendel, Rechberger et al. Rebound Distinguishers. ASIACRYPT 2009, LNCS 5912.
- [LAAZ11] Leander, Abdelraheem, AlKhzaimi, Zenner. A Cryptanalysis of PRINTcipher: The Invariant Subspace Attack. CRYPTO 2011, LNCS 6841.
- [GKRS22] Grassi, Khovratovich, Ronjom, Schofnegger. The Legendre Symbol and the Modulo-2 Operator in Symmetric Schemes. IACR Trans. Symmetric Cryptol., 2022(1):5-37.
- [BFSY05] Bardet, Faugere, Salvy, Yang. Asymptotic Behaviour of the Index of Regularity of Quadratic Semi-Regular Polynomial Systems. MEGA 2005.
- [BCD11] Boura, Canteaut, De Canniere. Higher-Order Differential Properties of Keccak and Luffa. FSE 2011, LNCS 6733.
- [W+14] Wood et al. Ethereum: A Secure Decentralised Generalised Transaction Ledger. 2014.
Formalization Status
| File | Content | Status |
|---|---|---|
| Security.lean | Collision, preimage, CICO, zero-sum | Stated |
| Sponge.lean | Generic sponge construction | Stated |
| SBox.lean | Power map, bijectivity, DP bounds | Stated |
| MDS.lean | Cauchy matrix, MDS property, subspaces | Stated |
| HADES.lean | Full/partial rounds, ARC, S-box layers | Partial |
| Basic.lean | Poseidon config, permutation, hash, domain separation | Stated |
| Poseidon/Security.lean | All security claims, lemma, propositions | Stated |
| Instances.lean | Concrete parameter sets (Table 2) | Complete |
| Grain.lean | LFSR parameter generation | Stated |
| — | Section 6: ZK proof systems (R1CS constraints, Groth16, Bulletproofs, PLONK, STARKs) | Not yet formalized |
| — | Appendix B: Efficient implementation (round constant optimization, sparse matrices) | Not yet formalized |
| — | Appendix C: Security analysis (differential, linear, interpolation, Groebner basis attacks) | Not yet formalized |
| — | Appendix D: Compact constraints for partial rounds | Not yet formalized |
| — | Appendix F: Concrete instances with security margin (Tables 7–8) | Not yet formalized |
| — | Appendix G–H: Round selection, Merkle tree instances | Not yet formalized |
History
- 2026-02-17Add disclaimer: content not author-approved, eprint is authoritative6638546
- 2026-02-16Add CONVERTED_DATE to existing 47 paper pages7191c14
- 2026-02-16Add crawler metadata to all 47 paper pagesc6638f2
- 2026-02-16Convert numeric citations to BibTeX-style keys across all papers71c86d3
- 2026-02-14Fix math rendering: add display math support, remove sub/sup tags0ed1494
- 2026-02-14Replace HTML sub/sup with KaTeX math environmentsa020da2
- 2026-02-12Add table of contents to Poseidon paper page06bd578
- 2026-02-12Replace all remaining static Lean code blocks with Lean4Web iframesaf59b63
- 2026-02-12Embed Lean4Web iframes, add vision, upgrade to Lean 4.27.0b01da05
- 2026-02-12Add full Poseidon paper page with Lean formalizationsd512636