StateSync-GKR 发布带机器检验可靠性边界的稀疏证明器 1.2 版
原标题
GKR with a Machine-Checked Core, and a Sparse Prover Made Faster with Byte-Identical Proofs
内容摘要
作者在 Ethereum Research 发布 StateSync-GKR 工作，据称是首个针对一般分层电路的 GKR 可靠性边界的机器检验证明，在 Isabelle/HOL 中完成，开发含 20 个理论、11,112 行和 418 条命名命题，电路覆盖线性、乘积和立方门，挑战取自 31 位 KoalaBear 域的四次扩张，分母恰为 p⁴≈2¹²⁴。配套的稀疏证明器 release 1.2 将证明吞吐提升 2.41–2.71 倍且 13,824 个证明哈希与 1.1 版逐字节一致；宽度 4,096 时峰值内存较仅测试用的稠密参考低约 89 倍。安全性归约到树的位置绑定假设，节点哈希为无前馈的截断 Poseidon2，不具抗碰撞性。与 Rust 验证器之间的值关系是尚未闭合的最后一环。两篇论文见 arXiv，Fiat–Shamir 非交互化不在分析范围内。
节点哈希用截断的 Poseidon2 不具备抗碰撞性，安全性改为归约到树的位置绑定，且与 Rust 验证器之间的最后一环尚未闭合。
来源：Ethereum Research · 社区研究提案 · ethresear.ch
打开原文所属事件
StateSync-GKR 发布带机器检验可靠性边界的稀疏证明器 1.2 版
作者在 Ethereum Research 发布 StateSync-GKR 工作，称其为首个针对一般分层电路的 GKR 可靠性边界机器检验证明，在 Isabelle/HOL 中完成，含 20 个理论、11,112 行和 418 条命名命题。配套稀疏证明器 release 1.2 将证明吞吐提升 2.41–2.71 倍，13,824 个证明哈希与 1.1 版逐字节一致；宽度 4,096 时峰值内存较仅测试用的稠密参考低约 89 倍。安全性归约到树的位置绑定假设，与 Rust 验证器之间的值关系尚未闭合。
最新变化：作者发布 StateSync-GKR 1.2 版，证明吞吐提升 2.41–2.71 倍且证明哈希与 1.1 版一致。