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.
翻译：加密互动验证系统提供了一种有效和可扩缩的方法来核查在块链上的计算结果。 证明人构建了一种非链证据,证明对特定输入程序的执行会终止并产生一定结果。 证明人随后公布一份证明,证明人可以有效可靠地核实常见的混合加密假设。 该方法依赖于对程序执行痕迹的代数编码。 我们在此报告使用利恩3号验证助理核实开罗计算模型对STARK互动验证系统的编码是否正确。
相关内容
微信扫码咨询专知VIP会员