本文提出一个名为 Distiller 的通用框架，旨在优化概率证明系统（包括交互式证明 IP、简洁非交互式论证 SNARK、概率可检验证明 PCP 等）的前端开销。在过去十年中，概率证明的实现虽受广泛关注，但由于前端需要将抽象计算转换为等价的算术约束，导致实现规模难以扩展。Distiller 的关键思想是：用户不需要将原始计算直接编码为约束，而是可以翻译一个抽象规格说明（abstracted specification），并在此基础上进行约束生成。该框架首次在此领域实现了可证明安全的转换，即转换过程本身具有形式化保证。此外，Distiller 将“在约束中编码检查”的思想推向逻辑极限，从而发现更多减少约束数量的机会。在基准测试中，Distiller 实现了 1.3 到 50 倍的成本降低，部分场景下获得了更好的渐近复杂度。这篇论文主要面向研究概率证明系统、零知识证明、SNARK 编译器及形式化验证方法的研究人员与高级工程人员，核心贡献在于提供了一种可证明安全的通用约束简化方法，为提升证明系统的可扩展性提供了新思路。

本文提出 Flock，一种基于哈希的 SNARK（简洁非交互式零知识证明）系统，旨在大幅加速大批量布尔计算（尤其是标准密码学哈希函数评估）的证明生成。在许多 SNARK 应用中，证明大量 SHA-256、Keccak、BLAKE3 等哈希评估是关键瓶颈。Flock 针对同一 R1CS 电路的批量证明进行优化，同时支持哈希链、Merkle 路径开证明，并可扩展至完整的哈希签名验证。其核心技术包括对 lincheck 和 zerocheck 协议的新优化，以及由编码智能体协同设计的激进优化的概念验证实现。实验表明，在 M4 Max 处理器单核上，Flock 每秒可证明 8.2 万次 BLAKE3 压缩函数评估、4.2 万次 SHA-256 压缩和 3 万次 Keccak 置换，开销仅为原生执行的约 250 倍；在十核上，吞吐量超过每秒 66 万次 BLAKE3 压缩。与当前最先进的 Binius64 相比，Flock 在 SHA-256 证明上快 9 倍以上，比最快的椭圆曲线 SNARK 快 500 倍以上。该工作显著降低了批量哈希证明的计算成本，可推动 SNARK 在区块链、可验证计算等场景中的实际部署。