Efforts to verify Zero-Knowledge Proof circuit encodings have highlighted the challenge of proving the correctness of quantifier-free statements that make use of both bitvector and finite field operations. Existing verification workflows are either manual or rely on SMT solvers, which scale poorly on some classes of problems for reasons that include difficulties with conversion operators and challenges reasoning about inequalities. To address these limitations, we present a novel Lean tactic BitModEq that leverages range lemmas and case analysis to produce verified translations from finite fields to bitvectors. Our approach, combined with bit-blasting, outperforms state-of-the-art SMT solvers, solving 19% more ZKP arithmetization benchmarks.

翻译：验证零知识证明电路编码的工作凸显了证明同时使用位向量和有限域操作的无量词语句正确性的挑战。现有验证流程要么依赖人工手动操作，要么依赖SMT求解器，而后者在处理某些类别问题时扩展性较差，其原因包括转换运算符的复杂性以及不等式推理的困难。为解决这些限制，我们提出了一种新颖的Lean策略BitModEq，该方法利用范围引理和情形分析，生成从有限域到位向量的可验证转换。结合位爆破技术，我们的方法优于现有SMT求解器，在零知识证明算术化基准测试中多解决了19%的问题。