发表机构
Oraclizer Labs, Inc.; Oraclizer Labs Korea（Oraclizer Labs 公司; Oraclizer Labs 韩国）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
该工作通过Isabelle/HOL机器验证，将稀疏默克尔状态转换的电路正确性与GKR验证协议组装成信任链，并明确剩余实现与密码学义务。
AI 中文摘要
GKR健全性限制了关于算术电路的虚假输出声明，但应用程序还需要保证其电路编码了预期的状态转换。我们在Isabelle/HOL中机器验证了稀疏默克尔成员资格、非成员资格和更新的这一联系。一个编译器模型在双向方向上关联电路接受与转换有效性。一个可复用的协议模型将层归约、布线谓词扩展和导入的sumcheck健全性组装成对显式链事件的界限。它们的组合将语义无效性转移到该界限，且见证在挑战实验之前固定。具体解释和前提激活暴露了仅靠干净构建无法发现的空洞假设集。进一步的开发构造了精确的四次KoalaBear扩展，提升了基域电路对象，并在其声明的挑战假设下建立了分母为$p^4$的组装界限。一个可执行的Rust证明器伴随该模型。Creusot/Why3契约提供了部分实现连接，一个条件定理在未解除的值对应前提下将成功的验证器轨迹关联到模型事件。转录本的在线挑战分布和多轮Fiat-Shamir归约均未建立。贡献在于在一个证明助手内，将编译器正确性与GKR组装模型组合在一起，并明确说明了剩余的实现和密码学义务。
英文摘要
GKR soundness bounds false output claims about arithmetic circuits, but an application also needs assurance that its circuit encodes the intended state transition. We machine-check this connection for sparse-Merkle membership, non-membership, and update in Isabelle/HOL. A compiler model relates circuit acceptance to transition validity in both directions. A reusable protocol model assembles layer reduction, wiring-predicate extensions, and imported sumcheck soundness into a bound on an explicit chain event. Their composition transfers semantic invalidity to that bound, with the witness fixed before the challenge experiment. Concrete interpretations and premise activations expose vacuous assumption sets that a clean build alone would miss. A further development constructs the exact degree-four KoalaBear extension, lifts the base-field circuit objects, and establishes the assembly bound with denominator $p^4$ under its stated challenge assumptions. An executable Rust prover accompanies the model. Creusot/Why3 contracts provide a partial implementation connection, and a conditional theorem relates successful verifier traces to the model event under an undischarged value-correspondence premise. Neither the transcript's online challenge distribution nor a multi-round Fiat--Shamir reduction is established. The contribution is the composition, within one proof assistant, of compiler correctness with a GKR assembly model, together with an explicit account of the remaining implementation and cryptographic obligations.
Comments17 pages, 3 figures, 3 tables. Software artifact: https://github.com/Oraclizer/statesync-gkr (v1.1.0; archived source DOI: 10.5281/zenodo.23136385)
