FROST-GKR · Parano1d Lab

Skip to content

On this page The same permutation, proved again and againOne batch, three columnsWhy it is called FROSTHow two reductions prove the whole batchProve the engine once, describe the topology at its endpointsThe concrete gainWhy the advantage survives larger batchesWhat the theorem establishesHow Parano1d uses itPaper and reproducible artifact<br>AbstractFROST-GKR places permutation slots, rounds and state lanes on one Boolean product domain. A degree-nine global zerocheck proves every Poseidon2b round in the batch, and one degree-two shifted-view reduction returns all derived claims to three committed columns. In the 59-permutation reference workload, it reduces 472 constraint sumchecks to 2, the raw algebraic transcript from 287,712 to 5,568 bytes, prover time by 10.69× and verifier time by 14.80×. Endpoint relations reuse the same trace for chains, trees, sponges and Parano1d State computation.

The same permutation, proved again and again

Hash-based proof systems spend much of their work proving the same permutation again and again. The inputs change, but the S-box, round constants and linear maps do not. A conventional layer-by-layer arithmetization discards that regularity: every Poseidon2b execution receives its own columns and its own chain of algebraic reductions.

For Parano1d the problem was architectural. Wallet authorization, Merkle authentication, State computation, transcripts and recursive verification all reuse Poseidon2b. If every call carries a separate algebraic circuit, the hash layer grows with the protocol graph and eventually dominates the proof that is meant to verify it.

The reference workload in the FROST-GKR paper makes that wall concrete. It contains 59 width-four Poseidon2b executions. The preserved product-chain construction needs eight constraint sumchecks for each execution, 472 in total. FROST-GKR asks a different question: can the proof describe the permutation once and make the execution number another coordinate of the data?

The answer is one global committed trace. Every execution slot, every round and every state lane becomes a coordinate of a single Boolean product domain. Two structural sumchecks leave four point-value claims, which terminal batching reduces to one claim for each committed column.

The architectural result<br>FROST-GKR removed 470 of the 472 constraint sumchecks in the reference workload. More importantly, it turned repeated permutation verification into one reusable, linear-time backend. That change made the larger Parano1d proof architecture viable: adding another hash topology no longer means instantiating another copy of the internal Poseidon2b proof.

slot2s padded executions

round27 66 active rounds

lane22 width four

trace domain2s+9 one multilinear table

Permutation number is a trace coordinate, not a reason to create another circuit.

One batch, three columns

Let B be the number of live permutations and L = 2s ≥ B the padded slot count. Poseidon2b has four state lanes and 66 nonlinear rounds. FROST-GKR reserves 128 round positions, so a trace cell is indexed by

(slot, round, lane) ∈ {0,1}s × {0,1}7 × {0,1}2

The complete domain has n = s + 9 variables and N = 2n = 512L cells. Its committed witness contains only three multilinear columns:

state contains the state entering each round and the terminal state row;

s_in contains every active x^7 S-box input;

s_out contains the corresponding S-box output.

Public selectors identify live slots, active rounds and the lanes that receive the S-box. The implementation derives the selector sigma from the fixed round schedule. It may materialize that table while computing the sumcheck, but sigma is not a fourth witness commitment. The same three witness columns therefore represent full rounds, where all four lanes are nonlinear, and partial rounds, where only lane zero is nonlinear. In Parano1d the prover commits to those columns before any relation challenge is sampled. The standalone comparison stops at the same terminal multilinear claims and checks them directly.

Why it is called FROST

FROST means Frobenius Reduction over Shifted Tables . Both halves name a load-bearing part of the construction.

Over a binary field, Frobenius squaring is linear:

(a + b)2 = a2 + b2

The direct Poseidon2b S-box can be evaluated as x³ = x²·x and x⁷ = x⁴·x³. Squaring supplies x² and x⁴; only two general field multiplications remain. The proof keeps the direct degree-seven relation instead of decomposing every S-box into a ladder of auxiliary circuit layers.

Shifted tables solve the other hard part. A round equation reads the state at round r and the state at round r + 1. Incrementing a seven-bit round index is not an affine transformation of multilinear variables. A shifted-table evaluation therefore cannot simply be renamed as an opening of the original column at a transformed point. FROST-GKR proves that connection explicitly.

How two reductions prove the whole...