Cairo程序执行的一种验证代数表示
A verified algebraic representation of Cairo program execution
摘要：
加密交互式证明系统提供了一种有效且可扩展的方法来验证区块链上的计算结果。一个证明器构造一个链外证明，证明程序在给定输入上的执行以某个结果终止。然后，证明者发布一个证书，该证书可以被有效地和可靠地验证，以普遍接受的密码学假设为模。该方法依赖于程序执行轨迹的代数编码。在这里，我们报告这样的编码的正确性的验证开罗模型的计算相对于STARK交互式证明系统，使用精益3证明助手。
英文摘要：
Cryptographic interactive proof systems provide an efficient and scalable means of verifying the results of computation on blockchain. A prover constructs a proof, off-chain, that the execution of a program on a given input terminates with a certain result. The prover then publishes a certificate that can be verified efficiently and reliably modulo commonly accepted cryptographic assumptions. The method relies on an algebraic encoding of execution traces of programs. Here we report on a verification of the correctness of such an encoding of the Cairo model of computation with respect to the STARK interactive proof system, using the Lean 3 proof assistant.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
