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.

翻译：许多基础性程序验证工具已被开发出来，用于构建机器可检验的程序正确性证明，其中大多数基于霍尔逻辑。这些工具的程序逻辑、断言语言及其底层编程语言可以通过浅层嵌入或深层嵌入进行形式化。诸如Iris和早期版本的已验证软件工具链（VST）等工具选择了不同的浅层嵌入来形式化它们的程序逻辑，但这些不同嵌入方式的优劣尚未得到充分研究。因此，本文旨在研究程序逻辑的嵌入方式对逻辑证明规则的影响。本文考虑了一组有用的扩展证明规则，以及四种不同的逻辑嵌入：一种深层嵌入和三种常见的浅层嵌入。我们证明了这些扩展规则在这些嵌入下的有效性，并讨论了它们的主要挑战。此外，我们提出了一种方法，将现有的浅层嵌入逻辑提升为深层嵌入逻辑，从而大幅简化特定证明系统中扩展规则的证明。我们基于两个现有的验证工具评估了我们的成果。我们将最初浅层嵌入的VST提升为我们的深层嵌入VST，以支持扩展规则，并基于Iris框架实现了Iris-CF和深层嵌入的Iris-Imp，以在真实验证项目中评估我们的理论。