← 研踪 PaperTrailarXiv:2610.05335 · v2
Machine-Checked Soundness of the GKR Protocol for Sparse-Merkle Updates
首次提交 2026-10-04 23:56
版本更新 2026-10-26 20:41
雷达观测 2026-10-29 00:36
摘要
Proofs of authenticated-data-structure updates built on the Goldwasser-Kalai-Rothblum (GKR) protocol are sound only if three arguments hold together: the soundness of the protocol, the exactness of the arithmetization that turns an update into a circuit, and the binding of the hash commitments. For GKR, the mechanizations we know of stop at the sumcheck subprotocol. For sparse-Merkle membership, non-membership and update as compiled by the StateSync-GKR prover, we machine-check in Isabelle/HOL the first two arguments, their composition, and the leaf side of the third. For layered circuits with linear, product and cube gates, the cube gate serving the $x^3$ S-box of Poseidon2, we prove that for a false output claim, the event that some layer's sumcheck accepts a false sum while all earlier carried claims are false has probability at most $(s_{\mathrm{out}} + \sum_i (2 s_i d_i + 1))/|\mathbb{F}|$, where layer $i$ has $2^{s_i}$ wires and $d_i$ bounds the degree of its sumcheck polynomial. We instantiate the bound over the exact quartic extension of the 31-bit KoalaBear field from which small-field provers draw challenges, so that the denominator is $p^4 \approx 2^{124}$, and lift base-field layers and false outputs into it. In a constraint-level model of the compiler, with the hash sub-circuits as abstract functions, the verifier model accepts exactly the valid transitions, and leaf-commitment collisions reduce to sponge collisions. Their composition is mechanized for claims that no witness makes valid, and from the mechanized theorems it follows on paper that the bad event has probability at most this bound for every input that does not encode a valid transition. All bounds concern the interactive public-coin protocol with uniform challenges; the Fiat-Shamir transformation, knowledge soundness and zero knowledge are outside the model.
作者备注：26 pages, 3 figures, 7 tables, 2 listings. v2 reorganizes the paper around its cryptographic statements, adds a per-input soundness corollary and a proof-engineering appendix, and corrects the description of the extension-field lifting; v1 theorem statements unchanged. Companion paper: arXiv:2610.14849. Software: https://github.com/Oraclizer/statesync-gkr (doi:10.5281/zenodo.23280552)
观测到的版本
相邻记录可能跳过中间版本；首次发现 v2 及以上也会标为版本更新。
v3 · 2026-11-03 17:57 · 最新观测版本
Soundness of the GKR Protocol for Sparse-Merkle Updates, with a Machine-Checked Core
The GKR soundness theorem bounds the acceptance of a false output claim for a fixed circuit and input. It does not say what the outputs of a compiled circuit mean for that input, and that has to be proved for each family of circuits. For a sparse Merkle tree over a compressing hash, heuristically almost every root admits a valid path for almost any leaf, so the needed statement concerns the witness as well as the claim. We prove per-input soundness for membership, non-membership and update claims, for trees of every depth, in the delegation setting of GKR: the verifier reads the circuit input in the clear and leaves the node hashes to the circuit. Assuming correct hash sub-circuits, every accepted input, honestly encoded or not, determines a valid witness, and the chain constraint cannot be dropped. If the witness read from an input fixed before the challenges is not valid, this verifier accepts with probability at most $\bigl(s_{\mathrm{out}}+\sum_i(8s_i+1)\bigr)/|\mathbb{F}|$ for a circuit with $2^{s_{\mathrm{out}}}$ outputs and $2^{s_i}$ wires read at layer $i$. This covers cube gates for the Poseidon2 S-box and, with $|\mathbb{F}| = p^4$, circuits over the 31-bit KoalaBear field with challenges from its quartic extension. The implemented node hash, a truncated permutation, is not collision resistant, so the statement that accepted runs for one key and root assert the same leaf assumes position binding of the tree. All our results are proved in the paper. Isabelle/HOL also checks a layer-chain bound, the exactness of the verifier's checks on encoded witnesses in a constraint-level model with abstract hash sub-circuits and, over one field, their composition for claims with no valid witness. All bounds concern the interactive public-coin protocol.
查看此版本解读 →查看此版本原文 ↗v2 · 2026-10-26 20:41
Machine-Checked Soundness of the GKR Protocol for Sparse-Merkle Updates
Proofs of authenticated-data-structure updates built on the Goldwasser-Kalai-Rothblum (GKR) protocol are sound only if three arguments hold together: the soundness of the protocol, the exactness of the arithmetization that turns an update into a circuit, and the binding of the hash commitments. For GKR, the mechanizations we know of stop at the sumcheck subprotocol. For sparse-Merkle membership, non-membership and update as compiled by the StateSync-GKR prover, we machine-check in Isabelle/HOL the first two arguments, their composition, and the leaf side of the third. For layered circuits with linear, product and cube gates, the cube gate serving the $x^3$ S-box of Poseidon2, we prove that for a false output claim, the event that some layer's sumcheck accepts a false sum while all earlier carried claims are false has probability at most $(s_{\mathrm{out}} + \sum_i (2 s_i d_i + 1))/|\mathbb{F}|$, where layer $i$ has $2^{s_i}$ wires and $d_i$ bounds the degree of its sumcheck polynomial. We instantiate the bound over the exact quartic extension of the 31-bit KoalaBear field from which small-field provers draw challenges, so that the denominator is $p^4 \approx 2^{124}$, and lift base-field layers and false outputs into it. In a constraint-level model of the compiler, with the hash sub-circuits as abstract functions, the verifier model accepts exactly the valid transitions, and leaf-commitment collisions reduce to sponge collisions. Their composition is mechanized for claims that no witness makes valid, and from the mechanized theorems it follows on paper that the bad event has probability at most this bound for every input that does not encode a valid transition. All bounds concern the interactive public-coin protocol with uniform challenges; the Fiat-Shamir transformation, knowledge soundness and zero knowledge are outside the model.
查看此版本解读 →查看此版本原文 ↗