Matching Logic Proofs Meet Succinct Cryptographic Proofs
by Bailey, Bolton, Chen, Xiaohong, Fiedler, Adam, Malvai, Harjasleen, Miller, Andrew, Mishra, Pratyush, Rodrigues, Nishant and Rosu, Grigore
Summary
We present the syntax and the proof system of matching logic and introduce the research problem of producing succinct cryptographic proofs for checking matching logic proofs, aka Proof of Proof. This technical report was first published on Chen’s personal GitHub repository at https://github.com/xc93/pi-square-doc/commits/main/mlzk.pdf in June 2023. The idea of achieving verifiable computing via combining mathematical proofs and cryptographic proofs was firstly explained by Roşu in his presentation The K Approach and Vision in 2020; see slide 99 of the slide deck at https://drive.google.com/file/d/1iXda2NyGzKVWxkd02IlXj5Tq5cOM_gNd/view. We thank Don Beaver and Rahul Maganti for early brainstorming on the Proof of Proof ideas and algorithms.