Matching Logic Proofs Meet Succinct Cryptographic Proofs

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 in June 2023. The idea of achieving verifiable computing via combining mathematical proofs and cryptographic proofs was firstly explained by Rosu 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.