formal_baby_snark:使用精益定理证明者对babySNARK证明系统进行形式验证 源码

正式的小蛇 该存储库使用实现对证明系统的形式验证。 这是一个进展中的工作。 截至2020年1月29日,babySNARK的知识健全证明免费。 定理的完整证明可以在Knowledge_soundness.lean的末尾找到。 精益代码摘要 Knowledge_soundness.lean文件具有几个与babySNARK实例化的参数匹配的参数语句。 这些是: $ F $定义多项式的字段。 $ m $,$ n_ {stmt} $,$ n_ {wit} $,对应于论文中的$ m $,$ l $和$ nl $。 $ r $,多项式$ t $的根的索引集合 $ u_ {stmt},u_ {wit}