Verifying Programs with Logic and Extended Proof Rules: Deep Embedding vs. Shallow Embedding

Many foundational program verification tools have been developed to build machine-checked program correctness proofs, a majority of which are based on Hoare logic. Their program logics, their assertion languages, and their underlying programming languages can be formalized by either a shallow embedding or a deep embedding. Tools like early versions of Verified Software Toolchain (before 2018) choose different shallow embeddings to formalize their program logic. But the pros and cons of these different embeddings were not yet well studied. Therefore, we want to study the impact of the program logic’s embedding on logic’s proof rules in this paper. This paper considers a set of useful extended proof rules, which aided the proof automation in VST, and four different logic embeddings: one deep embedding and three common shallow embeddings. We prove the validity of these extended rules under these embeddings and discuss their main challenges. Furthermore, we propose a method to lift existing shallowly embedded logics to deeply embedded ones to greatly simplify proofs of extended rules in VST. We implemented our theory in VST by lifting the originally shallowly embedded VST to our deeply embedded VST and establishing these extended rules.