文件名称：formal_baby_snark：使用精益定理证明者对babySNARK证明系统进行形式验证
文件大小：14KB
文件格式：ZIP
更新时间：2024-03-01 07:30:42
lean mathlib snark Lean
正式的小蛇 该存储库使用实现对证明系统的形式验证。 这是一个进展中的工作。 截至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} $，索引对应于论文中$ u_i $的单变量多项式的集合。 代数群模型给出的对手多项式的各种系数。 该文件还从这些参数定义了各种值，包括： $ t $，取模的单项多项式。 $ t $的多变量类
【文件预览】：
formal_baby_snark-master
----src()
--------soundness.lean(1KB)
--------knowledge_soundness.lean(23KB)
--------auxiliary_lemmas.lean(0B)
--------vars.lean(201B)
--------general_lemmas()
----leanpkg.toml(250B)
----README.md(3KB)
----.gitignore(44B)