买专利卖专利找龙图腾，真高效！ 查专利查商标用IPTOP,全免费！专利年费监控用IP管家,真方便！

龙图腾网获悉同济大学申请的专利一种针对Circom编译器功能正确性验证方法及系统获国家发明授权专利权，本发明授权专利权由国家知识产权局授予，授权公告号为：CN120045457B 。

龙图腾网通过国家知识产权局官网在2026-01-06发布的发明授权授权公告中获悉：该发明授权的专利申请号/专利号为：202510118352.5，技术领域涉及：G06F11/3668；该发明授权一种针对Circom编译器功能正确性验证方法及系统是由张苗苗;蒙俊杰;陈韩悦;杜博闻设计研发完成，并于2025-01-24向国家知识产权局提交的专利申请。

本一种针对Circom编译器功能正确性验证方法及系统在说明书摘要公布了：本发明提供了一种针对Circom编译器功能正确性验证方法及系统，用于保障编译器基于Circom源代码的编译产物与源文件在约束一致性和计算一致性方面的正确性，包括以下步骤：S1，对Circom编译器调用的汇编函数进行验证；S2，对Circom源代码进行编译；S3，提取Circom源代码的抽象语法树；S4，解析抽象语法树，提取约束模型和计算模型；S5，解析R1CS文件，提取编译产物的约束模型；S6，提取编译产物的计算模型；S7，将源代码的约束模型与R1CS文件的约束模型进行等价验证；S8，对源代码和CPP文件的计算模型进行等价性验证；S9，证明Circom编译器能够正确编译该Circom源文件。

本发明授权一种针对Circom编译器功能正确性验证方法及系统在权利要求书中公布了：1.一种针对Circom编译器功能正确性验证方法，其特征在于，包括： 步骤S1，预先针对Circom编译器所调用的汇编函数库中的各个汇编函数进行验证，验证功能正确性，并形成对应的形式化规约，记作汇编函数功能形式化规约； 步骤S2，使用Circom编译器对Circom源代码进行编译，若能通过，则保存编译所得的.sym，.dat，json格式的R1CS文件以及CPP文件； 步骤S3，从所述Circom源代码中提取抽象语法树，并以json文件格式进行存储； 步骤S4，对所述Circom源代码的抽象语法树进行解析，基于Circom语言的语法语义，提取所述Circom源代码所对应的约束模型和计算模型，记作源代码所对应的约束模型和源代码所对应的计算模型； 步骤S5，基于.sym文件对编译所得R1CS文件进行解析，提取编译产物所对应的约束模型，记作R1CS文件所对应的约束模型； 步骤S6，基于所述汇编函数功能形式化规约和.sym文件对.dat和CPP文件进行解析，提取编译产物所对应的计算模型，记作.dat文件所对应的计算模型和CPP文件所对应的计算模型，以及element_dict用来存储signal在CPP文件中的映射关系； 步骤S7，将所述源代码所对应的约束模型和所述R1CS文件所对应的约束模型使用等价关系连接，取反后使用CVC5求解器进行求解，若无解，则表明Circom编译器能够保障编译产物与源文件的约束一致性，若有解，即存在反例，则表明Circom编译器存在错误； 步骤S8，基于所述element_dict，结合SMT求解器验证所述源代码所对应的计算模型和所述CPP文件所对应的计算模型的等价性形成目标性质，使用CVC5求解器进行求解，若无解，则表明Circom编译器能够保障编译产物与源文件的计算一致性，若有解，即存在反例，则表明Circom编译器存在错误； 步骤S9，若S7和S8的求解结果均为无解，即表明Circom编译器能够对Circom源文件进行正确编译。

如需购买、转让、实施、许可或投资类似专利技术，可联系本专利的申请人或专利权人同济大学，其通讯地址为：200092 上海市杨浦区四平路1239号；或者联系龙图腾网官方客服，联系龙图腾网可拨打电话0551-65771310或微信搜索“龙图腾网”。

以上内容由龙图腾AI智能生成。