A verified algebraic representation of Cairo program execution
This work provides a verified foundation for cryptographic proof systems in blockchain, though it is incremental as it builds on existing encoding methods.
The researchers tackled the problem of verifying the correctness of an algebraic encoding for the Cairo model of computation used in blockchain proof systems, and they successfully verified it using the Lean 3 proof assistant.
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.