通用零知识虚拟机与高效区块链累加器技术文档 ========================================== 本文档介绍三项相互配合的核心技术方案： - HyperWASM 通用零知识虚拟机系统（V1.0）面向任意 WASM 程序的通用电路化与可验证执行，后端采用 HyperPlonk（多线性多项式 + Sumcheck）与 Zeromorph（多线性 PCS 归约与移位优化）。 - 高效密码学累加器系统（V1.0.0）面向 Merkle 累加器的高性能零知识验证，核心采用 Anemoi 哈希与 Jive 压缩模式，并配套低门数的电路约束优化。 - AC4 约束验证器（V1.0）面向零知识电路的“约束健全性审计”，用于识别输出信号是否存在不恰当约束（under-constrained / over-constrained），可对 Circom 与 Halo2 两类电路进行统一分析。 .. contents:: 目录 :local: :depth: 2 .. _s1-terms: 术语、符号与设计约束 -------------------- 术语 ^^^^ .. list-table:: :header-rows: 1 :widths: 20 80 * - 术语 - 含义 * - ZKP / SNARK - 零知识证明 / 简洁非交互式论证。 * - zkVM - 通用零知识虚拟机，对任意程序执行生成可验证证明。 * - WASM - WebAssembly，栈式虚拟机字节码。 * - Plonk / Plonkish - Plonk 类约束系统与其工程实现形态（表格化约束、选择器、置换、查找等）。 * - HyperPlonk - 将 Plonk 从单变量多项式迁移到多线性多项式与 Sumcheck 的证明系统，目标是线性时间证明者并支持高阶自定义门。 * - PCS - 多项式承诺方案（Polynomial Commitment Scheme），用于“先承诺、后开点求值证明”。 * - KZG - 基于配对的单变量多项式承诺体系（需要可信设置或公共参数）。 * - Zeromorph - 将多线性多项式的承诺与求值证明归约到单变量 PCS 的通用构造，并提供高效移位（shift/rotate）开点优化。 * - Sumcheck - 验证布尔超立方体上多线性多项式求和等式的交互式协议，可通过 Fiat–Shamir 变为非交互。 * - Lookup - 查找论证，把“值属于表”或“读写一致性”等关系规约为集合成员/多重集等价问题。 * - Accumulator - 累加器：把集合状态压缩为一个摘要（例如 Merkle 根），并支持成员/非成员证明。 符号约定 ^^^^^^^^ 本文默认电路规模为 :math:`N`，常取 :math:`N = 2^k` 以便在布尔超立方体 :math:`H=\{0,1\}^k` 上建模；多线性多项式记为 :math:`f(X_1,\ldots,X_k)`（每个变量次数 :math:`\\le 1`），其单变量化记为 :math:`\\hat{f}(X)`；:math:`u=(u_1,\ldots,u_k)` 表示开点向量，:math:`f(u)=v` 表示多线性多项式在 :math:`u` 处求值为 :math:`v`。 设计约束与目标 ^^^^^^^^^^^^^^ 系统的主要目标是：对任意 WASM 程序稳定生成可证明电路结构（通用性）；在大规模电路下保持可编译与可证明，避免 :math:`O(N\\log N)` 瓶颈主导（可扩展性）；在工程层面保持模块边界清晰，支持不同后端/承诺方案与并行加速（可工程化）；并满足完备性、知识健全性（soundness）与零知识（ZK）要求（可验证性与隐私性）。 .. _s2-hyperwasm: HyperWASM 通用零知识虚拟机系统（V1.0） ------------------------------------- 背景与问题陈述 ^^^^^^^^^^^^^^ 零知识证明技术在隐私保护、可验证计算、可信执行与区块链扩展性等方向展现出巨大潜力，但要在工程上规模化落地，必须解决两个长期痛点： #. 通用计算的算术化成本：现有系统常为特定业务电路定制，难以覆盖任意程序语义。 #. 大电路证明的性能瓶颈：传统 Plonk 体系大量依赖 FFT/IFFT 等准线性算子，证明者复杂度通常为 :math:`O(N\\log N)`；当电路规模与约束复杂度上升时，对数因子会成为系统吞吐的主要限制。 HyperWASM 的总体思路是：以 zkWASM 前端实现 WASM→电路 的通用性，以 HyperPlonk+Zeromorph 后端实现线性时间证明者与移位友好开点，共同形成可扩展的通用 zkVM 方案。 总体架构（分层与模块化） ^^^^^^^^^^^^^^^^^^^^^^^^ 系统采用“前端指令翻译层 → 证明系统核心层 → 多项式承诺层 → 工程优化层”的分层结构：前端负责 WASM 算术化，把栈机语义、控制流、内存/表操作转为 Plonkish 约束系统；证明核心层以 HyperPlonk 为主，将门约束、连线一致性、查找与集合等价统一聚合，并通过 Sumcheck 完成全局一致性验证，从而避免 FFT 成为主瓶颈；承诺层使用 Zeromorph 在单变量 PCS（如 KZG）上实现多线性承诺与开点，并对旋转/移位求值提供近常数额外开销的优化；工程优化层则围绕多项式算术、MSM、批量开点、Transcript 复用与缓存布局进行并行化与常数优化，以提升整体吞吐。 模块化边界（参考 Plonkish 的工程分解思路） ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ 为便于扩展与维护，系统按职责划分为若干逻辑组件（强调“接口/职责”而非代码组织）：后端层（Backend）定义证明系统生命周期接口（预处理、证明、验证），核心实现为 HyperPlonk，并显式支持“含移位关系”的证明/验证流程；承诺层（PCS）抽象承诺与开点接口并扩展移位开点能力，Zeromorph 作为多线性 PCS 的核心实现可构建在单变量 KZG 等成熟 PCS 之上；前端层（Frontend）把 WASM 执行翻译为 Plonkish 约束描述并可对接 Halo2 等电路接口；多项式表示与算子层（Poly）提供多线性/单变量多项式的表示、求值、折叠与旋转/移位相关访问；基础设施层（Util）提供 Transcript（Fiat–Shamir）、并行框架、MSM/配对算子封装与表达式引擎等，为性能与可观测性（计时、日志）提供支撑。 总体流程（从 WASM 到 proof） ^^^^^^^^^^^^^^^^^^^^^^^^^^^^ HyperWASM 的工作流可概括为四段连续链路：首先装载并解析 WASM 模块结构（类型段、函数段、导出信息与内存布局）；随后构建与电路生成强相关的 IR，将栈操作边界、控制流边界与内存读写行为显式化，并据此生成约束与布线计划；接着进行预处理与参数化，依据电路规模生成通用参数，并对选择器、置换、查找表等固定多项式进行承诺与索引化以得到证明/验证参数；最后进入证明生成与验证阶段，证明端承诺并执行 HyperPlonk 各子检查与 Sumcheck，验证端反转录并校验承诺开点、移位开点以及 Sumcheck 交互痕迹。 以下章节分别对“前端算术化”和“后端协议/承诺”给出更细的技术解释。 前端：WASM 指令翻译与电路化细节 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ 为什么选择 WASM 作为通用前端 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~ WASM 是高度标准化、语言无关的中间表示：其栈式指令集统一，便于把“入栈/出栈关系”映射为行/列约束；控制流结构化（block/loop/if），天然适合以“门级路径选择”表达；内存模型清晰，便于通过 lookup/表驱动方式约束读写一致性。 IR 与“列—行”电路模型的桥接 ~~~~~~~~~~~~~~~~~~~~~~~~~~~ 直接从 WASM 字节码生成约束往往会遇到三类问题：栈高度变化频繁导致布线难以稳定；控制流合流点复杂容易引入不完备约束；内存读写涉及“地址—值—操作类型”的三元关系，难以用纯门约束高效表达。为此系统引入面向电路的中间表示（IR），把执行语义显式化为栈状态演化（每条指令的输入/输出栈片段）、控制流边界（分支/循环的进入退出与路径选择信号）以及内存/表事件流（读写事件、地址、值、时序与范围），从而更顺畅地桥接到“列—行”电路模型。 该 IR 的输出目标是生成一个“Plonkish 表”：它由多列 witness、固定列（常量/表）、选择器列、置换与查找配置组成，满足后端证明系统可消费的接口。 栈式指令的约束映射（算术与逻辑） ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 对于典型算术指令（如 add/mul），电路化的关键是将其表示为低次数多项式约束，并由选择器精确激活。例如：加法/乘法可写成 :math:`a + b - c = 0`、:math:`ab - c = 0` 等低次数关系；比较/布尔逻辑常通过范围约束、布尔化约束或表驱动（lookup）实现；类型/位宽转换可通过范围检查或分解约束实现（工程上常与 lookup 结合以节省约束）。 为了避免“所有约束在所有行都生效”，系统使用选择器或预处理常量列将约束限定在对应指令行上。 控制流电路化（结构化门与路径守恒） ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ WASM 的 if/else、br、loop 是结构化控制流。电路化的主要挑战是：不同路径的执行必须在电路上“对齐”，否则会出现未约束的自由度。 HyperWASM 的处理原则是：用路径选择信号表达“当前行属于哪条路径”；在合流点施加路径守恒/一致性约束，保证任意路径下关键状态（例如栈顶值、程序计数语义）一致；将循环展开为可证明的“状态机步进”，每一步保持固定形态的约束集合，并通过选择信号控制是否继续迭代。 这种门级路径表达方式避免了“电路中存在不受约束跳转”的风险，提升了语义正确性。 内存与表访问（Lookup 驱动的一致性校验） ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 内存读写本质是三元关系：``(address, value, op_type)``，并且还要满足时序与范围约束。纯门约束表达会导致约束数量膨胀。 因此系统将其规约为 lookup 关系：把合法的“地址—数据—操作类型”映射为表项，通过 lookup 论证保证每次读写事件都能在表中找到对应条目；对于读写一致性（例如同一地址的读值等于最近一次写值），可引入排序/时间戳列，并通过集合等价/多重集一致性（multiset equality）来约束。 对于内存密集型程序，系统对 lookup 进行批处理与聚合，降低表项体积与开点次数，提高可编译性与证明效率。 后端核心：HyperPlonk（多线性多项式 + Sumcheck） ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ 传统 Plonk 的瓶颈：单变量多项式与 FFT 主导 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 在标准 Plonk 中，见证轨迹与约束通常编码为单变量多项式在某个乘法子群上的取值。要证明约束在整个域上成立，往往需要通过 FFT/IFFT 在系数域与值域之间转换，构造商多项式（quotient polynomial）并在随机点评估，同时为置换/查找等论证引入额外多项式与多次开点。 当 :math:`N` 很大时，FFT 的 :math:`O(N\\log N)` 成为主要成本之一，并且在复杂查找/移位关系中还会放大开点负担。 HyperPlonk 的范式转移：布尔超立方体上的多线性表示 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ HyperPlonk 将电路视为布尔超立方体 :math:`H=\{0,1\}^k` 上的取值问题：:math:`N=2^k` 行对应 :math:`H` 的 :math:`2^k` 个点；witness、选择器与固定列被表示为 :math:`k` 变量的多线性多项式；所有约束最终聚合为一个多线性恒等式 :math:`C(x)=0`（对所有 :math:`x \\in H` 成立）。 核心问题转化为：如何高效证明 :math:`C(x)` 在整个 :math:`H` 上恒等为零，而不遍历全部点。 Sumcheck 协议：把“2^k 求和”降维为“单点求值” ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Sumcheck 用来验证如下声明： 证明 :math:`S = \\sum_{x \\in \\{0,1\\}^k} g(x)` 对某个多线性多项式 :math:`g` 成立。 协议（交互式形式）可以概括为 :math:`k` 轮： #. 证明者在第 1 轮提交一个关于 :math:`X_1` 的低度单变量多项式 :math:`p_1(X_1)`，其含义是对其余变量求和后的结果；验证者检查 :math:`p_1(0)+p_1(1)=S`，通过后采样随机挑战 :math:`r_1`。 #. 第 2 轮证明者“绑定” :math:`X_1=r_1`，再提交关于 :math:`X_2` 的 :math:`p_2(X_2)`；验证者检查 :math:`p_2(0)+p_2(1)=p_1(r_1)` 并采样 :math:`r_2`。 #. 重复直到第 :math:`k` 轮结束，最终验证者只需检查一次 :math:`g(r_1,\\ldots,r_k)` 与最后一轮多项式在 :math:`r_k` 的一致性。 其“魔法”在于：它把 :math:`2^k` 个点上的求和验证折叠为 :math:`k` 次一致性检查与一次单点求值（维度折叠）；证明者每轮主要工作可组织为对向量/表的一次线性扫描，从而整体可做到 :math:`O(N)`（线性复杂度）；并可用 Fiat–Shamir 将挑战 :math:`r_i` 通过 transcript 哈希产生，使协议成为非交互证明的一部分（可非交互化）。 用 Sumcheck 证明“恒等为零” ~~~~~~~~~~~~~~~~~~~~~~~~~ 要证明 :math:`C(x)=0` 对所有 :math:`x \\in H` 成立，HyperPlonk 常用的标准技巧是引入等值多项式（equality polynomial）： 定义 .. math:: eq(x,y)=\prod_{i=1}^k \bigl(x_i y_i + (1-x_i)(1-y_i)\bigr), 当且仅当 :math:`x=y`（在 :math:`\\{0,1\\}^k` 上）时取值为 1，否则为 0。于是“对所有 :math:`y`，有 :math:`\\sum_{x \\in H} C(x)\\,eq(x,y) = 0`”等价于“:math:`C` 在 :math:`H` 上处处为 0”；随机选择 :math:`y` 并结合 Schwartz–Zippel 引理，可得到高概率健全性保证。 因此，HyperPlonk 将电路约束聚合到 :math:`C(x)` 后，通过 Sumcheck 证明上述求和恒等式成立，取代传统 Plonk 中对商多项式与 FFT 的依赖。 子检查分层：从局部到全局的严密归约 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ HyperPlonk 在工程上通常把约束分解为多个模块并逐层聚合：先用 Gate Identity 检查门约束语义（由选择器激活），再用 Wiring Identity 通过置换关系保证复制约束/跨门引用正确；对查找相关约束可采用 Lookup/Logup 将其规约为集合成员与多重集一致性问题，并通过 MultiSetEquality/ProductCheck 以乘积恒等式验证多重集相等；随后用 ZeroCheck 将所有子检查聚合为单个“应为零”的全局多项式，最后用 Sumcheck 对该全局多项式执行折叠求和验证，从而得到简洁可验证的证据。 该分层结构的优点是：各模块高内聚、可并行，并能为复杂约束（查找、置换、高阶门）提供统一的代数接口。 多项式承诺层：Zeromorph（多线性→单变量的通用归约） ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ PCS 在系统中的角色 ~~~~~~~~~~~~~~~~~ 证明系统需要频繁完成两类操作：其一是对 witness/固定多项式做承诺，把高维对象压缩成短摘要（commitment）；其二是在随机点提供开点证明，证明“该多项式在该点的取值等于某值”，同时不泄露多项式本身。 对于多线性多项式，直接设计 PCS 往往成本高；Zeromorph 的关键贡献是把多线性 PCS 的问题系统性地归约到成熟的单变量 PCS（如 KZG）上。 多线性到单变量的同构映射 :math:`\mathcal{U}_n` ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Zeromorph 基于一个线性同构 :math:`\\mathcal{U}_n`：它将 :math:`n` 变量多线性多项式空间映射到次数 :math:`<2^n` 的单变量多项式空间；直观地说，就是把多线性多项式在布尔超立方体 :math:`\\{0,1\\}^n` 上的 :math:`2^n` 个取值，当作单变量多项式的 :math:`2^n` 个系数。 例如，当 :math:`n=2` 时，若 :math:`f` 在 :math:`(0,0),(1,0),(0,1),(1,1)` 的取值分别为 :math:`a_{00},a_{10},a_{01},a_{11}`，则其单变量化为： .. math:: \hat{f}(X) = a_{00} + a_{10}X + a_{01}X^2 + a_{11}X^3. 因此要承诺多线性多项式 :math:`f`，可以先计算其单变量化 :math:`\\hat{f}=\\mathcal{U}_n(f)`，再用任意“加法同态”的单变量 PCS 对 :math:`\\hat{f}` 承诺即可。 多线性求值证明：从欧几里得分解到单点开点 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 目标是证明 :math:`f(u)=v`。Zeromorph 利用多线性多项式的“分解等价”： .. math:: f - v = \sum_{i=1}^n (X_i - u_i)\,q_i. 其中 :math:`q_i` 是低维多线性商多项式。该恒等式成立当且仅当 :math:`f(u)=v`。 接下来利用 :math:`\\mathcal{U}_n` 的线性性，把多线性恒等式映射为单变量恒等式（形式上会出现 :math:`\\mathcal{U}_n(X_i q_i)` 与 :math:`u_i\\mathcal{U}_n(q_i)` 的组合）。协议的关键步骤可概括为：证明者需要计算各 :math:`q_i` 并对其单变量化多项式分别承诺；验证者随后执行次数检查（degree check），确保各 :math:`q_i` 的次数上界与变量维度匹配（例如 :math:`<2^{i}-1` 量级），否则证明者可能通过“超次数自由度”在挑战点伪造恒等式而破坏健全性；接着验证者给出随机挑战点 :math:`z`（经 Fiat–Shamir 可非交互化）；最后双方基于承诺的同态性构造一个“目标单变量多项式”，证明者只需对其在 :math:`z` 处做一次标准单变量开点，证明取值为 0，即可完成多线性求值证明。 直观上，Zeromorph 把“多变量求值正确性”压缩为“少量辅助承诺 + 一次单点开点”，从而显著降低通用电路下的求值证明开销。 零知识开销的量级改善 ~~~~~~~~~~~~~~~~~~~~ 传统零知识化方法往往需要引入大规模随机掩码多项式，在高维场景下开销容易膨胀。Zeromorph 的零知识版本主要额外成本是对 :math:`n` 个低维 :math:`q_i` 的承诺与少量检查，使得开销从朴素方式的指数级增长下降到近似线性的 :math:`O(n)` 增量（在工程上表现为“接近常数级”的额外开销）。 移位（Shift/Rotate）开点优化：Zeromorph 的关键工程价值 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ 为什么 shift 是系统瓶颈之一 ~~~~~~~~~~~~~~~~~~~~~~~~~~~ 在 zkVM/状态机/lookup 等场景中，大量约束天然包含“跨行关系”，例如“下一步状态等于当前步状态经过转移函数”、“表驱动约束需要对排序后的事件序列做相邻一致性校验”、“连线/置换关系需要引用相邻行或固定偏移行的值”等。 这些都可以抽象为：对某个多项式 :math:`f` 的“移位版本” :math:`f_{\\leftarrow}` 的求值证明需求。如果每个移位都单独承诺或单独开点，成本会非常高；在长距离移位时，早期方案可能出现指数级开点膨胀。 Zeromorph 的核心单变量恒等式 ~~~~~~~~~~~~~~~~~~~~~~~~~~~ 设 :math:`f` 的取值向量为 :math:`(a_0,a_1,\\ldots,a_{N-1})`，其循环左移对应 :math:`f_{\\leftarrow}` 的取值向量为 :math:`(a_1,\\ldots,a_{N-1},a_0)`。Zeromorph 给出关键恒等式（在单变量化域中）： .. math:: X \cdot \mathcal{U}_n(f_{\leftarrow}) = \mathcal{U}_n(f) - a_0 + a_0 X^N, 其中 :math:`a_0 = f(0,\\ldots,0)`。 该恒等式把“移位多项式的单变量化”与“原多项式的单变量化”联系起来，从而避免为 :math:`f_{\\leftarrow}` 重新做承诺：证明者只需提供 :math:`a_0` 的一致性证据，随后移位求值证明即可转化为与常规 Zeromorph 求值证明几乎同形的协议，额外代价接近常数。 影响：把“长距离移位”从不可用变为可工程化 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 在实际系统中，移位关系往往成百上千次出现。该优化使得多移位开点可以批量聚合，并与 Sumcheck 折叠流程共享挑战与 transcript，从而在通用电路（包括 zkVM 这类长执行轨迹电路）中显著降低证明生成时间与证明大小。 与 zkVM/查找/状态机的关系 ~~~~~~~~~~~~~~~~~~~~~~~~~ 在通用 zkVM 电路中，移位关系可视为“跨行引用”的统一抽象（例如读取下一行的寄存器状态、对齐执行轨迹、检查相邻事件一致性）。Zeromorph shift 优化在工程上的直接含义是：不需要为每一种偏移量额外承诺多项式；可以把大量偏移量的开点合并到极少数批量开点中；并在与 Transcript 的挑战复用后，显著减少证明大小与验证端配对/MSM 负担。因此，该优化在很大程度上决定了“通用电路 + 大量跨行约束”的可证明性与吞吐上界。 工程优化要点（面向吞吐与可扩展性） ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ 系统核心计算包括多项式运算、MSM、承诺与开点、以及约束折叠求解。为最大化 CPU/GPU 资源利用率，系统在工程上采用： 任务分片与并行调度 ~~~~~~~~~~~~~~~~~~ 系统抽象任务分块与调度单元（Task Shards），统一管理多项式与曲线运算任务，并通过线程池与 Rayon-like 并行框架动态调节任务粒度与线程数量。 多项式算术与 FFT 的“降主导” ~~~~~~~~~~~~~~~~~~~~~~~~~~~ HyperPlonk 的核心验证不再依赖 FFT，但工程中仍可能在预处理或特定算子中使用 FFT/IFFT：此时可采用 Cooley–Tukey 分治的层级并行调度，并根据核数与缓存（L2/L3）做自适应配置，以避免同步阻塞与缓存抖动。 MSM 优化 ~~~~~~~~ MSM 计算通常结合 Pippenger 算法与桶化策略，对同批标量归并与预计算，以降低多次 MSM 调用的常数因子并提升承诺/开点吞吐。 承诺/开点批处理与 transcript 复用 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 承诺与开点阶段会对多开点、多移位开点执行批量聚合，从而减少配对与 MSM 次数；同时与 Sumcheck 共用 transcript，通过挑战聚合减少重复 Fiat–Shamir 调用与数据复制。 安全性与可信假设（概要） ^^^^^^^^^^^^^^^^^^^^^^^^ 安全性层面，系统需满足完备性（约束满足时应接受）、知识健全性（随机挑战下伪造通过概率可忽略，依赖多项式恒等式检验与 Sumcheck 健全性）与零知识性（证明不泄露 witness，Zeromorph 的零知识版本通过低维辅助多项式承诺实现高效隐藏）。协议非交互化通常采用 Fiat–Shamir，在随机预言机模型（ROM）下分析；PCS 若采用 KZG，则安全性依赖双线性群上的离散对数相关假设，并通常依赖公共参数（可信设置或安全生成流程）。 .. _s3-accumulator: 高效密码学累加器系统（基于 Anemoi 与 Merkle 累加器，V1.0.0） ----------------------------------------------------------- 背景：零知识电路中的哈希瓶颈与累加器需求 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Merkle 树广泛用于链上状态承诺、集合成员性证明与数据完整性验证。在零知识场景中，电路的原生运算是有限域上的算术运算，而传统哈希（SHA/Keccak）大量依赖布尔位运算，电路化成本极高，常成为整个证明系统的瓶颈。 因此需要“SNARK-friendly 哈希”：其代数结构可在有限域上以低次数约束表达，从而用极少门完成哈希验证。Anemoi 作为代表性设计之一，置换结构可调（参数化状态宽度与轮数），在 Groth16/Plonk/Halo2 等多种证明系统下约束友好，并且适合用高阶自定义门表达，从而进一步压缩门数。 在此基础上，系统将 Anemoi 的电路优化成果用于 Merkle 累加器，实现成员/非成员的高效零知识验证。 Merkle 累加器总体流程（从集合到证明） ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ 系统把集合状态压缩为一个摘要（Merkle 根），并围绕该摘要提供零知识证明能力： #. 构建累加器状态：对叶子集合构建三叉 Merkle 树（或可扩展到其他分支因子），每层用 Anemoi-Jive 压缩得到父节点，迭代得到根。 #. 生成证明见证（路径轨迹）：记录从叶子到根的兄弟节点与位置选择，形成路径轨迹（trace）。 #. 电路化路径验证：把“给定叶子与路径可导出根”算术化为一组约束：每层压缩必须正确、位置选择必须一致、最终根必须等于公开根。 #. 证明与验证：证明端承诺 witness 并生成零知识证明；验证端用公开根等输入验证 proof。 对于非成员证明，常见做法是在稀疏 Merkle 树（SMT）中用默认空值与路径证明表达“该键未被写入”，或在前缀/有序结构中证明相邻键的夹逼关系。本系统的技术核心（高效哈希与路径电路）可作为上述非成员方案的基础构件。 成员性证明的形式化描述（以三叉 Merkle 为例） ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 设叶子为 :math:`h_0`，第 :math:`t` 层的兄弟节点为 :math:`(s_{t,1}, s_{t,2})`，位置选择为 :math:`pos_t \\in \\{L,M,R\\}`。每一层压缩计算可统一写为“把 :math:`h_t` 放在由 :math:`pos_t` 指定的位置，并与两个兄弟节点一起输入到 Jive”，从而得到 :math:`h_{t+1}`：当 :math:`pos_t = L` 时 :math:`h_{t+1} = Jive(h_t, s_{t,1}, s_{t,2}; salt)`；当 :math:`pos_t = M` 时 :math:`h_{t+1} = Jive(s_{t,1}, h_t, s_{t,2}; salt)`；当 :math:`pos_t = R` 时 :math:`h_{t+1} = Jive(s_{t,1}, s_{t,2}, h_t; salt)`。 最终约束为 :math:`h_d = root`（:math:`d` 为深度）。电路化时需要同时约束 :math:`pos_t` 的合法性与选择一致性（确保三个输入排列正确）、每层 Jive 压缩的内部置换关系正确，以及最终根与公开输入一致。 非成员性证明的可扩展方向（概要） ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 非成员证明并非单一电路即可统一表达，常见路径包括：在稀疏 Merkle 树（SMT）中证明给定键对应叶子为“默认空值”并提供到根的路径一致性证明；或在有序/前缀结构中证明某键处于两相邻已存在键之间，结合范围约束与路径一致性推出“不在集合中”。无论采用哪种方式，底层都依赖“路径压缩哈希的高效电路化”，因此 Anemoi-Jive 仍是性能关键。 证明系统链路（以 Halo2/Plonkish 体系为例） ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 在工程上，Merkle 累加器电路通常通过如下链路进入证明系统：先将约束系统编译为后端可消费的多项式约束表达（门、置换、查找等）；再生成 PCS 公共参数并派生验证密钥与证明密钥（密钥绑定电路结构以保证验证正确性）；随后证明端承诺 witness/固定多项式并执行约束一致性检查以产出 proof（包含承诺、挑战、求值与开点证明等）；最后验证端基于公开输入与验证密钥重放 transcript，校验开点证明并判定接受/拒绝。该链路与第一部分的 HyperPlonk/Zeromorph 机制兼容：当电路中存在大量移位与查找约束时，Zeromorph shift 优化与批量开点会显著降低总体成本。 Anemoi 哈希：面向电路的置换设计 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ SPN 总体结构 ~~~~~~~~~~~~ Anemoi 属于算术友好置换（Permutation）原语，采用经典 SPN（Substitution–Permutation Network）骨架。状态可写为二维矩阵形式：两行 :math:`X`、:math:`Y`，共 :math:`l` 列，总维度 :math:`2l`（每个元素为域元素）。 每轮置换可以概括为四个连续步骤：先做常量加（第 :math:`r` 轮对 :math:`X` 加轮常量向量 :math:`C_r`，对 :math:`Y` 加 :math:`D_r`，常量由公开生成过程确定）；再做线性层（对 :math:`X` 应用扩散矩阵 :math:`M`，对 :math:`Y` 先做列移位 :math:`\\rho(\\cdot)` 再应用扩散或等价结构，以增强跨列扩散）；随后做伪哈达玛变换（PHT），以极低开销完成行间线性混合，例如形如 :math:`Y \\leftarrow Y + X`、:math:`X \\leftarrow X + Y`（不同参数化下系数略有变化），要求可逆并提升扩散；最后进入 S-Box 层，对每列 :math:`(x_i,y_i)` 应用 Flystel 结构的非线性变换。其关键优势在于：前向置换可包含较强非线性（如指数/逆幂），而验证关系可用低次数多项式约束表达，从而显著降低电路代价。 Flystel S-Box 的电路友好性（核心直觉） ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 在许多 SNARK-friendly 设计中，目标不是让电路直接计算昂贵的非线性，而是让电路验证一个“低度数等式”来证明非线性步骤正确。Flystel 的“开/闭”两种形式允许证明者离线计算时保持高非线性，而在电路约束侧保持低次数，从而减少门与开点成本，并通过 CCZ 等价等密码学性质保障安全强度。 Jive 模式：面向 Merkle 的高效压缩 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Merkle 树需要多对一压缩函数（CRH）。通用海绵结构通常需要多轮吸收-挤出，电路成本较高。Jive 模式的核心思想是仅执行一轮置换，再对若干状态字做线性抽取/线性混合得到输出；在 Merkle 场景中可构造 :math:`3\\to 1` 压缩以天然适配三叉 Merkle 树；同时通过加入常量盐值实现域分离（domain separation），降低跨协议重用带来的结构性风险。 这种“单轮置换 + 线性混合”的模式避免了冗余流程，使每层 Merkle 压缩的约束数量显著降低，是系统在 256 层等深度场景下仍保持高性能的关键因素之一。 电路约束优化：以“预计算轮密钥”压缩选择器开销 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ 在 Plonkish 表格约束中，选择器用于控制约束在哪些行被激活。若每个门都引入独立选择器，会带来额外承诺与开点负担。 本系统采用的典型优化策略是：将线性层（常量加、MDS、PHT）展开后，可把其效果写成“输入的线性组合 + 可预计算常量”的形式；这些常量可以以固定列写入，形成预计算轮密钥（PRK）多项式。由于 PRK 在非相关行取 0，它还可以兼作“选择信号”，从而减少显式选择器多项式数量；再结合表格列复用（例如在固定列数约束下把某些中间量映射到共享列），即可进一步压缩门数与约束数。 在典型参数（如 :math:`l=2,\\alpha=3`）下，单轮置换只需少量核心约束即可表达，整套置换约 20 个门量级，从而使“Merkle 每层压缩”的电路成本达到实用的低水平。 性能表现与工程特征（概要） ^^^^^^^^^^^^^^^^^^^^^^^^^^ 在以 Merkle 路径为主的电路中，哈希是主成本来源。通过 Anemoi-Jive 与约束优化，本系统可在深度为 256 的场景下，相较常见 Poseidon/MiMC Halo2 实现显著降低：门数量与证明时间，以及承诺与开点次数（在批处理策略下效果更显著）。 此外，由于 Anemoi 的约束具备结构化与重复性，工程上易于：批量化哈希层计算与 witness 生成，并将多层约束以流水方式组织以提升 CPU/GPU 并行利用率。 安全与零知识特性（概要） ^^^^^^^^^^^^^^^^^^^^^^^^ 安全性与零知识特性主要体现在：Jive 模式的线性抽取与盐值可用于域分离，避免不同上下文复用引起的结构性攻击面；路径中的叶子值与中间节点可设为秘密输入，使证明只暴露根或必要公开量；每层压缩与位置选择均被约束，最终根与公开根一致即代表成员性成立，而非成员性可在 SMT 等结构上用“空值路径”或相邻边界证明实现；系统底层假设与所采用的 PCS 与证明系统一致（如 KZG + Fiat–Shamir），并继承其绑定性与知识健全性保证。 .. _s4-ac4: AC4 约束验证器（电路约束健全性审计，V1.0） ------------------------------------------- 总体目标：识别不恰当约束 ^^^^^^^^^^^^^^^^^^^^^^^^^ AC4 的总体目标是验证零知识证明使用到的电路中是否存在不恰当的约束。为刻画这一问题，学界常用 under-constrained（欠约束）与 over-constrained（过约束）两种性质： - 欠约束：约束系统存在多个解，使得输出变量的取值不唯一，可能导致“伪造输出”等风险。 - 过约束：约束系统无解，说明电路约束之间存在冲突，证明系统无法产生有效见证。 例如，约束 :math:`a(a-1)=0` 将变量 :math:`a` 限制在集合 :math:`\\{0,1\\}` 中；若没有其他约束，则 :math:`a` 的取值不唯一，可视为欠约束。若再加入 :math:`a(a-2)=0`，则仅 :math:`a=0` 可同时满足两条约束，可视为约束充分。与之相反，若加入 :math:`a-2=0`，则不存在同时满足两条约束的解，可视为过约束。 在 AC4 的问题设定中，系统主要关注电路输出信号变量（后简称输出变量）是否被合理约束，因此把输入信号变量（后简称输入变量）视为参量（参数），并在输出维度判断欠约束/过约束风险。 技术路线：从电路约束到有限域多项式方程组 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ 为达成上述验证目标，AC4 将零知识电路中的约束转化为有限域上的含参多项式方程组，然后通过计算机代数方法判断方程组的可解性与解的数量： - 若存在多解，则认为原电路（在输出变量维度上）可能是 under-constrained； - 若无解，则认为原电路是 over-constrained； - 若唯一解，则认为输出变量被充分约束。 整体上 AC4 分为前端与后端两部分：前端负责把不同电路形态转化为统一的方程组表示（JSON）；后端对方程组进行分类，并调用相应求解器完成判定与报告输出。 系统架构：统一的 JSON 约束表示 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ AC4 通过 Circom 与 Halo2 两条管线提取约束并落盘为统一格式 JSON： - Circom 电路：先由 Circom 编译器输出 R1CS 文件；AC4 内置转换器读取 R1CS 与符号表，生成方程组 JSON。 - Halo2 电路：先由 Halo2 analyzer 将电路约束转写为中间表示（如 SMT/约束文件）；AC4 内置转换器再把该中间表示转换为方程组 JSON。 每个 JSON 对象对应一个方程组，其核心字段包括： - ``out_sig_list``：输出变量列表 - ``unknown_sym_str_list``：未知变量（输出变量 + 中间变量） - ``known_sym_str_list``：参量（输入变量） - ``expr_str_list``：约束表达式列表（每条为有限域上的等式/多项式表达式） 该“统一约束格式”使得后端求解逻辑与电路来源解耦：同一套求解与分类策略可复用在 Circom 与 Halo2 两类电路上。 后端分类与求解：线性/带参线性/高次三类 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ 后端读取 JSON 后，首先按方程组最高次数对约束系统进行分类，并在不同类别下采用不同求解策略： #. 线性方程组：所有方程均为线性。AC4 提取系数矩阵并在有限域上执行高斯消元，以判断解空间维度，并进一步检查“输出变量是否多解”（中间变量的多解可忽略）。 - 多解：``Precise Under-constrained`` - 单解：``Precise Exact-constrained`` - 无解：``Precise Over-constrained`` #. 带参线性方程组：每个方程要么为线性，要么仅包含形如 ``x·y`` 的乘积项，其中 ``x`` 是某个输入变量的一次项（参量），``y`` 是某个输出/中间变量的一次项。AC4 提取带参矩阵并做消元求解。由于参量可能取 0，某些情况下会使“原本唯一解”退化为多解（或使“原本无解”在特定参量取值下出现解）。因此在该分类下，AC4 除了报告是否存在输出变量多解外，也会区分“精确”与“代数”层面的判定： - 多解：``Precise Under-constrained`` - 单解：``Algebraic Exact-constrained`` - 无解：``Algebraic Over-constrained`` #. 高次方程组：存在二次及以上的非线性项（超出“带参线性”的限制）。AC4 调用相应的方程求解器（例如基于 Gröbner 基的消元/判定流程）计算可解性与解的数量，并同样以输出变量维度判断： - 多解：``Precise Under-constrained`` - 单解：``Precise Exact-constrained`` - 无解：``Precise Over-constrained`` 工程链路：作为“证明前”的约束审计环节 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ AC4 并不替代证明系统的 setup/prove/verify 链路，而是作为“电路上线/集成前”的审计环节插入工程流程： #. 从电路源（Circom/Halo2）提取约束并生成 JSON 中间表示； #. AC4 后端对 JSON 方程组分类求解并输出结果； #. 对发现的 under-constrained/over-constrained 问题进行定位、修复与回归，再进入正式证明链路。 在 zkVM 与累加器等大规模电路场景下，该流程可用于对关键输出（例如状态根、累加器根、承诺摘要等）的约束健全性进行快速检查，降低“约束缺失导致的错误证明”风险。 输出形态（概要） ^^^^^^^^^^^^^^^^ AC4 的输出通常包括：每个电路（或每组约束）的分类结果（well/under/over 等），以及用于定位的约束/变量日志信息。工程上可按电路名汇总输出，形成可追踪的审计报告，便于在电路迭代与参数变更时持续回归。 .. _s5-references: 参考文献 -------- #. Chen B, Bünz B, Boneh D, et al. *HyperPlonk: Plonk with Linear-Time Prover and High-Degree Custom Gates*. EUROCRYPT 2023. #. Kohrita T, Towa P. *Zeromorph: Zero-Knowledge Multilinear-Evaluation Proofs from Homomorphic Univariate Commitments*. Journal of Cryptology, 2024. #. Liu J, Patil H, Peddireddy A S, et al. *An Efficient Verifiable State for zk-EVM and Beyond from the Anemoi Hash Function*. Cryptology ePrint Archive, 2022.