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

TL;DR

This paper compares deep and shallow embeddings in program verification logics, analyzing their impact on proof rules, and proposes a method to lift shallow embeddings to deep ones, demonstrated on existing tools.

Contribution

It provides a formal comparison of deep versus shallow embeddings for program logics and introduces a lifting method to simplify proofs in verification tools.

Findings

Deep embeddings facilitate proof rule validation.

Shallow embeddings are easier to implement but less flexible.

Lifting shallow to deep embeddings simplifies extended rule proofs.

Abstract

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 Iris and early versions of Verified Software Toolchain (VST) choose different shallow embeddings to formalize their program logics. 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, 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 specific proof systems. We evaluate our results on two existing verification tools. We lift the originally shallowly embedded VST to our deeply embedded VST to support extended rules, and we implement Iris-CF and deeply embedded Iris-Imp based on the Iris framework to evaluate our theory in real verification projects.