https://galoishlee.github.io/tags/engineering/ Recent content in Engineering on As it was Hugo zh-CN maocred@gmail.com (Halois) maocred@gmail.com (Halois) This work is licensed under a Creative Commons Attribution-NonCommercial 4.0 International License. Wed, 10 Dec 2025 08:00:00 +0800 https://galoishlee.github.io/zkevm-constraint-soundness/ Wed, 10 Dec 2025 08:00:00 +0800maocred@gmail.com (Halois) https://galoishlee.github.io/zkevm-constraint-soundness/ <blockquote> <p>Reading: soundness is only as strong as the constrained surface.</p> </blockquote> <p>zkEVM 文章最容易写歪的地方，是把“有 EVM opcode、能出 proof、链上 verifier 接受”误当成安全性本身。真正需要抓住的是：proof 只覆盖那些被约束、被 commitment 绑定、再被 transcript 吸收进去的对象。任何没有被这条链路真正绑住的语义，都不在证明系统的 soundness boundary 里。</p> <p>所以这篇不讨论产品对比，而讨论 engineering attack surface。zkEVM 不等于“把客户端代码翻译成电路”；更准确地说，它是把 opcode 语义、memory read/write、storage queue、状态根更新、lookup 表、递归聚合这些对象拆成一组 constraint obligations，再证明这些 obligations 一起闭合。<sup id="fnref:1"><a href="#fn:1" class="footnote-ref" role="doc-noteref">1</a></sup> <sup id="fnref:2"><a href="#fn:2" class="footnote-ref" role="doc-noteref">2</a></sup> <sup id="fnref:3"><a href="#fn:3" class="footnote-ref" role="doc-noteref">3</a></sup></p> <p>也因此，最典型的 failure mode 不是某条大公式明显写错，而是 linkage 丢了。某个 selector 没把实例绑定到正确路径，某个 queue payload 没和前一层结果相等，某个 lookup 只检查 limb 合法却没检查重组，某个 challenge 没吸收所有 commitments。只要缺一条边，prover 就可能构造一个“局部都像样、全局却不是你想证明的执行”的 witness。</p>