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

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 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.

1 Introduction

Computer scientists have gained great success in developing foundationally sound program verification systems in the past decade. The word foundationally means: not only are programs’ correctness properties verified, but the correctness proofs and the dependent proof rules are also verified and machine-checked in a proof assistant like Coq [4] or Isabelle [33, 35]. Foundational verification tools like Verified Software Toolchain (VST) [2, 9], Iris [20], CSimpl [38], CakeML [18], etc. enable their users to verify programs written in real programming languages like C, Rust and OCaml using Hoare-style logic.

Extended Proof Rules

Theoretically, a Hoare logic with compositional rules, the consequence rule, and proof rules for singleton commands (like assignments) is powerful enough to prove all valid judgements [14]. These rules are often referred to as primary rules. Figure 1A shows a sound and complete logic for a toy language with only the skip command, the assignment, the sequential composition, and the if-statement.

Fig. 1

An example Hoare logic for a toy language: primary rules and extended rules

But in practice [9], a verification tool can be much easier to use if more rules are added to aid our proofs. Figure 1B shows two extended proof rules for the toy language. seq-assoc changes the associativity of sequential composition and allows provers to verify a program both from the beginning to the end in the forward style and from the end to the beginning in the backward style; if-seq distributes the command $c_3$ after an if-block to two branches inside it, and in this way, instead of finding an intermediate assertion that merges post-conditions of two branches $c_1$ and $c_2$, provers can directly verify $c_1\,;c_3$ and $c_2\,;c_3$, with no obligation to find a common post-condition for two branches. In this paper, we also incorporate control flow reasoning in program logics, which allows realistic program verification. This induces more extended rules with increased complexity, which are also covered in this paper.

We make a distinction between extended rules and derived rules. Derived rules are directly derived from primary rules with mostly trivial proofs, and these proofs are the same across different embedding of a logic with the same primary rules. Figure 1C shows an example of derived proof rules. hoare-conseq-pre is easily derivable from hoare-conseq and it allows weakening the precondition but keeps the postcondition untouched. This paper focuses on extended rules, whose proofs are usually non-trivial and differ across different embeddings (ways a program logic is formalized). Both derived rules and extended rules are useful in practice and we admit both as necessary components of VST.

Extended Rules and Hoare Logic Embeddings.

To utilize extended rules in program verifications, developers should first prove them in their logics. However, these extended rules may not be easily provable in every foundational verification tool, because different tools may choose various ways, i.e., various embeddings, to formalize their program languages and program logics to obtain unique features. A deeply embedded program logic defines the logic by inductive proof trees, while a shallowly embedded one directly defines Hoare triple’s validity using a program’s semantics. We further clarify the notion of embeddings in Sects. 3 and 4.

Due to differences in embedding methods, not all these extended rules are valid under each embedding, and challenges we might encounter in their proofs also vary from embedding to embedding. For example, shallowly embedded VST [2, 9] does not provide seq-inv (in Fig. 3) due to its significant proof burden while we can develop a simple formal proof of it in our deeply embedded VST. Therefore, in this paper, we (1) present four mainstream Hoare logic embeddings (one deep embedding, and three shallow embeddings respectively based on the big-step semantics, the weakest precondition, and the continuation) based on our survey of Hoare-logic-based program verification projects like VST, (2) identify a set of extended proof rules that can benefit verification automation in VST; and (3) formally verify these extended proof rules under these different embeddings.

Another Contribution: A Lifting Approach

We summarize the main challenges in proofs of these extended rules and find that most proofs of extended proof rules in shallowly embedded program logics are more complicated than those in the deeply embedded one. We claim that it would take more proof effort to equip some verification tools using shallow embeddings (like VST) with these extended proof rules. Another contribution of our paper is to present a much easier way to extend shallowly embedded program logic with extended proof rules: we can first lift the shallowly embedded logic into a deeply embedded one with acceptable proof effort. Then, we may derive extended proof rules, which are difficult for the original shallow embedding, using simpler proofs under the deep embedding.

We may not be the first ones to discover and utilize such an approach, but to our knowledge, it has never been formally presented in literature and we believe it can help with the design of foundational verification tools. To evaluate the lifting approach, we lift the shallowly embedded VST [2, 9], a verification framework for C programs, to the deeply embedded VST which supports most extended rules and is the basis of the current VST.

Our survey and formalization techniques can benefit future verification tools in the following ways. Firstly, our surveys and proofs indicate the level of support for extended proof rules under differently embedded program logics. Knowing which extended proof rules a verification tool supports, verification tool users may decide in advance which tool best matches their proof goals. By understanding the advantages and limitations of different embedding methods, verification tool developers can design proof systems satisfying the growing industrial demands. Secondly, our lifting approach can help existing verification tools to improve their framework by implementing extended rules with alleviated proof burden, as we demonstrate in our deeply embedded VST.

Paper Structure

Firstly, in Sect. 2, we fix the primitives of the programming language and primary proof rules of the program logic that this paper focuses on. Based on this logic, we present three categories of extended proof rules and explain how they benefit verification tools.

We then clarify the concept of deep/shallow embeddings for programming languages, assertion languages, and program logics, along with the settings of this paper in Sect. 3, since they will affect the correctness of extended proof rules. In Sect. 4, we formally define a deep embedding and three shallow embeddings of the Hoare logic supporting control flow reasoning. We also briefly review existing Hoare-logic-based verification frameworks using these embeddings.

Then, in Sect. 5, we present formal proofs of these extended rules under each embedding method and discuss their main challenges. In Sect. 6, we present our approach to lifting a shallowly embedded program logic into a deeply embedded one to avoid otherwise challenging proofs of extended rules. This approach relies on careful choices (explained in Sect. 7) of primary rules.

After that, we discuss various extensions to the Hoare logic and its embedding in Sect. 8. They include separation logic, procedure calls, total correctness, non-determinism, and impredicative assertions.

In Sect. 9, we apply our lifting method to shallowly embedded VST to obtain our deeply embedded VST.

Lastly, we discuss related works of program logic embeddings in Sect. 10 and conclude the paper in Sect. 11.

We formalize all shallow embeddings in Sect. 4 and related proofs in Sect. 5 in a Coq repository [15]. We refer readers to our deeply embedded VST (Sect. 9) for formalizations of the deep embedding and related proofs. Our deeply embedded VST are integrated into the VST repository (https://github.com/PrincetonUniversity/VST).

2 Program Logic and Extended Rules

A verification tool always comes with some very basic primary rules, like compositional rules, the consequence rule, and singleton command rules. However, we could further enrich its capability by adding extended proof rules, some of which will be of great assistance to users for proof simplification and automation.

In this section, we first present in Sect. 2.1 a toy language and a set of primary rules for the program logic that we will use for demonstration throughout this paper. Then, based on this program logic, we introduce in the remainder of this section three categories of useful extended proof rules: transformation rules (Sect. 2.2), structural rules (Sect. 2.3), and inversion rules (Sect. 2.4). We demonstrate some representative rules in each category (Fig. 3) and show their potential usage.

Fig. 2

The While-CF programming language and primary proof rules

2.1 The Toy Language and the Program Logic

The While-CF language (While-language with control flow commands) in Fig. 2 includes the assignment statement, $x = e$, which assigns the value of e to variable x, and empty command $\texttt{skip}$ which does nothing. It includes three basic structural commands: the sequential composition $c_1 \,;c_2$, the if-statement $\texttt {if}\,e \,\texttt {then}\,c_1 \,\texttt {else}\,c_2$, and the for-loop statement $\texttt{for}(;;c_2)~c_1$ in C language style, where $c_1$ is the loop body and $c_2$ is the increment step after the execution of each loop iteration. This for-loop statement itself does not exit the loop without the help of $\texttt {break}\,$ and $\texttt {continue}$ commands, which are responsible for manipulating control flows in the loop. Although the language is named While-CF, we use the for-loop instead of the while-loop because the for-loop will yield more interesting extended proof rules, and it is also the choice of the VST. It is also non-trivial because a continue command in the for-loop body $c_1$ does not skip the increment step $c_2$, which cannot be easily encoded by a while-loop.

Figure 2 shows some terms of the assertion language. It includes basic first-order logic terms and terms to support express evaluation and variable assignment. The term $[\![ e ]\!]$ denotes the value of e evaluated on given state $\sigma$, i.e., $\text {eval}(e, \sigma )$, and $[\![ e ]\!] = v$ means expression e evaluates to value v. $P[x \mapsto e]$ denotes the assertion after substitution of all occurrences of x by the value of e evaluated on the current state. We use the same notation for the boolean expression b.

Primary proof rules are listed in Fig. 2. Intuitively and informally, $\vdash \{ P \} c \{ Q, [R_\text {brk}, R_\text {con}] \}$ (we use $[\vec {R}]$ as syntax sugar for $[R_\text {brk}, R_\text {con}]$ in the rest of the paper) means that: starting from any program state satisfying pre-condition P,

• (safety) the execution of the command c never cause an error,

• (correctness) and if the execution of c terminates and its termination is caused by $\texttt{break}$ or $\texttt{continue}$, the post-state will satisfy corresponding control flow post-conditions $R_\text {brk}$ and $R_\text {con}$, respectively. Otherwise, if the program terminates naturally, the post-state will satisfy the normal post-condition Q.

The hoare-skip, hoare-break rule, and hoare-continue are rules for singleton control flow commands that introduce the pre-condition into corresponding control flow post-conditions. The singleton command rule hoare-assign.¹ asserts that the value of variable x used in the pre-condition will be changed in the post-condition. The hoare-seq rule splits the proof of two sequentially composed commands. The hoare-loop rule uses two triples of the loop body and the increment step to build a specification for the for-loop statement. The hoare-if rule splits the proof of the if-statement into two branches to prove them separately. The hoare-consequence rule allows provers to strengthen the pre-condition and weaken the post-condition.

Although this programming language is a simple toy example, we may extend it with heap manipulation commands and function invocations as the paper will discuss in Sect. 8. Other primary rules related to separation logic and function invocation can also be included. But to demonstrate our results about extended rules in Sects. 2 and 5, the language and proof rules in Fig. 2 are sufficient. These primary rules are expressive enough to reason about loop control flows and also present in real verification tools like VST [2].

In Fig. 2, the assertion language and the program logic are presented in a deep embedding style using the syntax of assertions and derivation rules, but it is only for the purpose of demonstration. However, both of them can also be defined using shallow embeddings directly using their interpretation and semantics. We will soon investigate different embeddings of them in Sect. 3.

Fig. 3

Three categories of extended rules and their representatives

There are lots of useful extended rules that can be implemented above the program logic in Fig. 2, and we organize them into three categories and present some representatives of them in Fig. 3. We explain in detail the usage of these extended rules in the following sections.

2.2 Transformation Rules

It is often the case that we know two different programs are semantically equivalent and we should be able to substitute one of them for the other in a Hoare triple while preserving the triple’s validity. Rules like if-seq, loop-nocontinue, and loop-unroll1² allow such semantic preserving transformations, and provers can transform the program into one that is easier to verify and sometimes automate its proof. We classify these extended rules that transform the command in a Hoare triple as transformation rules.

The proof rule if-seq. The program $(\texttt{if}~b~\texttt{then}~c_1~\texttt{else}~c_2) \,;c_3$ and $\texttt{if}~b~\texttt{then}~c_1 \,;c_3~\texttt{else}~{c_2 \,;c_3}$ behaves similarly and we can use if-seq to transform the one into the other.

Example 1

For a concise demonstration, we first start with a toy example (for which exists another workaround instead of using if-seq and we will discuss it soon), where we want to prove the following for some given $m, e, c_2, Q, \vec {R}$,

$$\begin{aligned} \vdash \{ \underset{P}{\underbrace{\exists n.\, [\![ x ]\!] = n \times m \wedge [\![ y ]\!] = m}} \} (\texttt{if}~b~\texttt{then}~\texttt{break}~\texttt{else}~\underset{c_1}{\underbrace{z=x/y}}) \,;c_2 \{ Q, [\vec {R}] \} \end{aligned}$$

Regularly, we need to explicitly provide an intermediate assertion $Q'$ and show³

(1)

But when we move $c_2$ inside the if-statement by $\textsc {if-seq}$, we only need to prove

(2)

As the reader may wonder, to prove the sequential composition $c_1;c_2$ in (2), we still need to prove the last two goals for $c_1$ and $c_2$ in (1). The difference here is that when verifying (2), we can symbolically execute $c_1$ along with $c_2$ from the beginning to the end. But in (1), we need to symbolically execute two branches to a unifying post-condition $Q'$ before executing $c_2$, while symbolic executions of two branches might produce different free variables in their postconditions and it brings troubles. We explain this difficulty in detail in the following paragraphs.

Symbolic execution in theorem provers is a technique for proof automation. It simulates the execution of the program and applies the execution’s effect to the pre-condition according to proof rules. VST’s proof automation relies heavily on such a technique. For example, symbolic execution can automatically transform the proof goal of the false branch (sequentially composed with a skip command for demonstration) in (1) as (3) shows (arrows represent symbolic execution steps by labeled proof rules).

(3)

During the symbolic execution, it will apply hoare-ex (demonstrated in Sect. 2.3) to eliminate quantifiers in the pre-condition and introduce the bounded variable as a free one into the context to reason about it. On the contrary, symbolic execution cannot automatically determine which free variables should be reverted back into the assertion as bounded ones in which order so that the following execution steps can proceed.

Back to the example, symbolic execution of $c_1$ in (3) will introduce n into the context, which is necessary for forwarding $z=x/y$. To achieve a unifying $Q'$ in (1), we need to revert n back into $Q'$ in the symbolic execution of $c_1$, since the other branch does not introduce n and it remains bounded. In other words, the $Q'$ in (3) should become $\exists n.\,[\![ z ]\!] = n \wedge [\![ x ]\!] = n \times m \wedge [\![ y ]\!] = m \wedge \cdots$, instead of the final assertion in (3). However, in (2), after we introduce n in the execution of $c_1$, we do not need to revert it back and when $c_2$ access z and n during its execution, we do not need to introduce n again. if-seq reduces the complexity of symbolic execution in this case.

Remark

As we have mentioned, the toy example can be resolved without applying if-seq. As the proof scheme in (4) indicates, we can extract n in P before we start the proof of the sequential composition and in this way, there is no need to revert n back again when finding the post-conditions of if-branches.

(4)

However, this does not mean the example is meaningless, because in many cases, the existential quantifier in the precondition cannot and should not be eliminated in advance. For example, the precondition below is an assertion to state the storage of a linked list in the heap. To prove the Hoare triple below for some $x, l, e, c_1', c_2, Q, \vec {R}$, we are unable to eliminate all quantifiers in listrep by hoare-ex without a fixed length of list l. In practice, we should be able to prove the triple below without such knowledge and keep the listrep predicate folded until reaching a test-empty operation to the linked list, and then should we unfold the predicate once and extract quantifiers. if-seq is the only option in these cases.

$$\begin{aligned}{} & {} \vdash \{ \text {listrep}(x, l) \} (\texttt{if}~b~\texttt{then}~\texttt{break}~\texttt{else}~c_1') \,;c_2 \{ Q, [\vec {R}] \}\\{} & {} \begin{aligned} \text {where } \text {listrep}(x,l)&\triangleq (l = \text {nil} \wedge \texttt {emp}) \\&\vee (\exists y, v, l'.\, l = v {:}{:} l' \wedge x\mapsto (v, y) * \text {listrep}(y, l')) \end{aligned} \end{aligned}$$

The proof rule loop-nocontinue. Another exemplary transformation rule in Fig. 3 is loop-nocontinue, which allows merging loop body and incremental step into one command when neither of them contains $\texttt{continue}$. In this way, users only need to provide one loop invariant for the loop body instead of two (one before the loop body and one before the increment step) when reasoning about a loop with no $\texttt{continue}$.

Example 2

This example combines loop-nocontinue and if-seq. The program divides x by y twice but separates two divisions in the incremental step and the loop body.

$$\begin{aligned} \vdash \Bigg \{\underset{P}{\underbrace{\exists n. \begin{array}{c} [\![ x ]\!]=m^{2n}\\ \wedge [\![ y ]\!] = m \end{array}}}\Bigg \} \texttt{for}(;;\underset{c_2}{\underbrace{x=z/y}})~ \texttt {if } \underset{e}{\underbrace{x>1}} \ \begin{array}{l}\\ \texttt {then } \texttt{break}\\ \texttt {else } \underset{c_1}{\underbrace{z=x/y}} \end{array} \Bigg \{\underset{Q}{\underbrace{[\![ x ]\!] = 1}}, [\bot ]\Bigg \} \end{aligned}$$

The precondition P can serve as a loop invariant, but regularly, we still need to find another loop invariant after the loop body but before the incremental step. However, by the symbolic execution (5), it first removes the incremental step and with $\texttt{skip}$ as the incremental step, it is obvious that another loop invariant is the same as P. Then, it can open the loop and prove that the loop body obeys the invariant. With the help of if-seq, it can automatically reach two easily provable proof goals without manual assistance.

$$\begin{aligned} \begin{aligned}&\vdash \{ P \} \texttt{for}(;;c_2)~\texttt{if}~b~\texttt{then}~\texttt{break}~\texttt{else}~c_1 \{ Q, [\bot ] \} \\ \xrightarrow [\textsc {nocontinue}]{\textsc {loop-}}&\vdash \{ P \} \texttt{for}(;;\texttt{skip})~(\texttt{if}~b~\texttt{then}~\texttt{break}~\texttt{else}~c_1) \,;c_2 \{ Q, [\bot ] \} \\ \xrightarrow [\textsc {if-seq}]{\textsc {hoare-loop}}&\vdash \{ P \} \texttt{if}~b~\texttt{then}~\texttt{break}\,;c_2~\texttt{else}~(c_1 \,;c_2) \{ P, [P, Q] \} \\ \xrightarrow [\textsc {hoare-break}]{\textsc {hoare-if}}&P \wedge \lnot [\![ b ]\!] \vdash Q \quad \text {and} \quad \vdash \{ P \} c_1 \,;c_2 \{ P, [P, Q] \} \end{aligned} \end{aligned}$$

(5)

The proof rule loop-unroll1. One more transformation rule we want to mention here is the loop-unroll1 rule. It allows peeling the first iteration of a for-loop and proving it as a separate triple. This is especially useful in two cases: when the first iteration of a loop does something different from the remaining iterations, e.g., initialization of some data, and the loop invariant for the remaining iterations can be greatly simplified without the first iteration; and when the loop only runs constant number of iterations, it may be easier to simply unfold it into a sequence of loop bodies and use symbolic execution to prove them automatically.

Although the loop-unroll1 rule in Fig. 3 does not perfectly match our criterion for transformation rules, their essence is the same. The loop-unroll1 rule has its counterpart, the following while-unroll1 for the while command, in the While language without control flow statements. It unrolls the first iteration of the while-loop into an if-statement.

If there are control flow commands like $\texttt{break}$ or $\texttt{continue}$, we cannot simply transform the for-loop into an if-statement because these commands will jump out of the scope of the original loop and interfere with executions outside the loop. As a result, we need to split the if-statement in while-unroll1 into several Hoare triples in loop-unroll1 and specify control flow post-conditions for the loop body and the increment command.

2.3 Structural Rules

We classify extended rules that transforms pre-/post-conditions in proof goals as structural rules. These rules allow provers to adjust pre-/post-conditions into forms that permit more organized proofs.

A typical case is the use of the primary rule hoare-consequence⁴. For example, in the last step of symbolic execution (5) from the last section, we need to prove the following assumption for the then-branch in order to apply hoare-if to verify the if-statement, where direct application of hoare-break does not work since the pre-condition does not match the break post-condition P and other two post-conditions are not $\bot$. We will use hoare-consequence to weaken the pre-condition into Q and strengthen the post-condition P into $\bot$ to match the form of hoare-break. In this way, we can directly apply hoare-break to prove the new triple.

In this section, we mainly discuss two structural rules in Fig. 3, hoare-ex and nocontinue, which we consider as extensions of hoare-consequence. When separation logic is taken into consideration in Sect. 8.1.1, we will encounter two more structural rules, frame and hypo-frame, and we postpone their discussions until then.

The proof rule hoare-ex. As we have already seen in Sect. 2.2, it is a common situation in that we need to prove a Hoare triple whose precondition is existentially quantified, e.g., loop invariants are usually existentially quantified.⁵ If provers can eliminate those existential quantifiers and extract bounded variables and related pure facts in preconditions into the meta-logic context, they can then apply domain-specific theories to those extracted variables — they are not buried in assertions any longer. hoare-ex enable us to perform such extraction.

Example 3

In the symbolic execution example (3) in Sect. 2.2 (rephrased below), the first step is applying hoare-ex to remove the existential quantifier. To verify the assignment $z=x/y$, we know the result of z will be n and it must be a free variable so that we can perform substitution of z by n according to hoare-assign.

hoare-ex is different from and sometimes cannot be derived directly from hoare-consequence. hoare-consequence changes pre-/post-conditions by entailments of the assertion logic, while hoare-ex is a direct entailment between two Hoare triples in the meta-logic.

The proof rule nocontinue. This rule allows us to modify the continue assertion arbitrarily since the program will never exit by a continue. We can use it as an enhancement to the consequence rule when we need to change the continue assertion. We can use this proof rule to support derivations of loop-related extended rules. For example, as we will see later in Fig. 4, we can prove loop-nocontinue using the nocontinue and inversion rules, which is the proof taken by VST.

2.4 Inversion Rules

Compositional rules allow us to combine proofs for separate modules into one proof for a larger program specification. But in some cases, we would like to extract information for these modules from the complete specification for other purposes. We classify extended rules that extract premises of a primary rule from its goal as inversion rules.

Figure 3 shows two example inversion rules, the seq-inv and loop-inv. seq-inv is the reversed sequencing rule, where the triple about $c_1 \,;c_2$ gives us the triples of $c_1$ and $c_2$. loop-inv is the reversed loop rule, which gives us the intermediate loop invariant. They are typical rules that reproduce the premises in compositional rules from the original conclusion. In the following sections, we discuss only the seq-inv rule because it is the most representative inversion rule and other ones have similar conclusions.

Example 4

With inversion rules, we can more easily reorganize proof trees in deeply embedded logic, and in our deeply embedded VST, they have been used extensively in proving other extended rules like transformation rules and structural rules. For example, in Fig. 4, the transformation rule loop-nocontinue can be proven given seq-inv and loop-inv.

We first extract information from the original triple by inversion rules and use nocontinue to adjust the continue post-condition of the increment step $c_2$ to $\bot$ so that we can subsequently apply hoare-loop to obtain the triple of the new loop.

Fig. 4

A derivation of loop-nocontinue based on inversion rules and structural rules

Example 5

More crucially, inversion rules enable the extraction of premises from shallowly embedded triples without unfolding the definition of the triple and users can reorganize existing “proofs” to produce new triples. This is especially useful when one want to add more automation to annotation-based verification and is used in VST-A [49] to better utilize existing annotations.

Fig. 5

Control flow graph of Example 5

For example, consider an annotated program $\texttt{for}(;;c_3)~c_1;\texttt {assert }I ;c_2$, where $\texttt {assert }I$ asserts that the assertion I holds between executions of $c_1$ and $c_2$ and it can guide prover’s verification. Usually, the main burden of verifying a loop is to find the loop invariant $I_1$ and $I_2$ as indicated in the control flow graph in Fig. 5. But for this program, if we can check $\vdash \{ P \} c_1 \{ I, [Q, \bot ] \}$ and $\vdash \{ I \} c_2 ;c_3 ;c_1 \{ I, [Q, \bot ] \}$ to be true, then the following derivation directly proves the triple $\vdash \{ P \} \texttt{for}(;;c_3)~c_1;\texttt {assert }I ;c_2 \{ Q, [\bot , \bot ] \}$ for the loop.

With the help of seq-inv, two intermediate assertions $I_1$ and $I_2$ are extracted for free. By re-ordering commands into a new loop body $c_2 ;c_3 ;c_1$ using I as the invariant, $P \vee I_1$ and $I_2$ become our loop invariants and we reconstructed Hoare triples for three paths in Fig. 5. As a result, we have verified the triple of the for-loop without any additional proof. Notice that the triples we need to provide as the premise of this derivation can be verified symbolic execution without the need to manually construct intermediate assertions $I_1$ and $I_2$. This approach of using seq-inv to rearrange program orders helps simplify the proof of this kind of loop by making it easier to apply symbolic executions.

Summary

In summary, inversion rules have a one-to-one correspondence to primary rules. For each primary rule, we can derive an inversion rule that produces the premises of it from the conclusion. Users often apply inversion rules to assumptions to extract information from them and use this information to aid their proofs. On the contrary, transformation rules and structural rules do not have such correspondence and are applied directly to the proof goals (the Hoare triple specification) to generate sub-goals with easier proofs. Transformation rules change the program in the specification but keep original pre-/post-conditions, while structural rules only have effect on pre-/post-conditions but not the program.

Although the discussion of extended rules in this paper focuses on a programming language with control flow commands, most of these rules are still meaningful in a language that does not feature the control flow commands. For example, if-seq and hoare-ex do not depend on the control flow post-condition. loop-unroll1 also has a counterpart while-unroll for loops without break and continue. For any programming language and program logic, it will always have its own set of inversion rules corresponding to its primary rules. Moreover, we believe adding other features to the language and the logic will yield more extended rules, but they are not well-studied and are not the focus of this paper.

3 Nomenclature

We have presented the program logic and extended rules in Sect. 2, but did not mention how they are formalized at all and we cannot check the correctness of these extended rules until we formally define the program logic. This section clarifies the notion of deep embedding and shallow embedding, which are two different approaches to formalizing languages and logics. In short, deep embeddings formalize structures while shallow embeddings formalize underlying semantics.

A program-logic-based foundational verification tool contains at least three elements where we could choose different embeddings: the programming language, the assertion language that describes program state properties, and the program logic that reasons about functional correctness of a program. Different verification projects choose different combinations of embeddings for these three elements as Table 1 shows. For shallow embeddings of program logics, we could further divide them into sub-categories: big-step-based (BigS.), weakest-precondition-based (WP), and continuation-based (Cont.), which we will discuss in detail in Sect. 4.

Table 1 Choices between shallow embedding and deep embedding

In the rest of this section, we explain what are shallow/deep embeddings for a programming language, an assertion language, and a program logic.

3.1 Embeddings of Programming Languages

When formalizing a language (e.g. a programming language or an assertion language), a deep embedding formalizes its syntax tree first and defines its meaning separately. In contrast, a shallow embedding uses the language’s intrinsic semantics as its definition directly. For example, Fig. 6 shows their differences in defining simple program expressions that only contain integer variables and addition. The addition operation is defined as a syntax tree constructor in the deeply embedded one and we use another evaluation function to define the semantics of all expressions. In the shallowly embedded one, the operation is directly defined as a function that computes the summation of its operands’ evaluation results or a relation from the expression to the final result.

Fig. 6

Example: deeply/shallowly embedded expressions

Most foundational verification tools including VST choose to use deeply embedded programming languages. The deeply embedded languages separate the syntax and semantics of programs and would allow structural induction over the program’s syntax tree in some proofs. Comparably, typical shallowly embedded languages use functions from initial program states to ending states, or binary relations between initial states and ending states, to represent programs. In other words, programs are formalized in proof assistants by their denotations instead of syntax trees, which makes it difficult to equip them with structural inductions. It is also difficult (although not impossible [40]) for a shallowly embedded programming language to support concurrency and other extensions. For example, to implement concurrency, a deeply embedded programming language can syntactically parallel-compose two programs and then choose small-step semantics for describing concurrency since one can interleave parallel steps that programs take. However, it is less convenient for the denotational shallow embedding to implement such an interleaving. In the denotational shallow embedding, a program expression itself is a big-step denotation that hides the intermediate states of its execution, so we cannot directly define the program with other threads interleaving at these intermediate states.

In some cases, developers would also use mixed embeddings of their programming languages [40, 45]: these languages use deep embedding to formalize structural compositions and use shallow embedding for singleton commands. For example, in the $\mu$C framework [45] for verifying OS kernels, Xu et. al formalize atomic operations $\gamma$ via a shallow embedding and formalize operation compositions (e.g., sequential composition $s_1; s_2$ and non-deterministic choice $s_1 + s_2$) via a deep embedding. Thus, a command s is defined by both embeddings in the formula below.

$$\begin{aligned} \begin{array}{rcl} s &{}\in &{} \text {Command} {:}{=} \gamma ~\vert ~ s_1; s_2 ~\vert ~ s_1 + s_2 ~\vert ~ {\textbf {end}} ~\vert ~ \cdots \\ \gamma &{}\in &{} \text {Abstract State} \rightarrow \text {Abstract State} \rightarrow \text {Prop} \end{array} \end{aligned}$$

Remark

In a shallowly embedded language, transformation rules become trivial and meaningless. For example, in if-seq rule, we have two programs defined below.

$$\begin{aligned} \texttt{if}~b~\texttt{then}~c_1 \,;c_3~\texttt{else}~c_2 \,;c_3&\triangleq \lambda \sigma .\, \textsf {match } \text {eval}(b, \sigma ) \textsf { with} ~\vert ~ \texttt {false}\Rightarrow c_3(c_1(\sigma )) \\&\,\,\qquad \qquad \qquad \qquad \qquad \qquad \vert ~ \texttt {true}\Rightarrow c_3(c_2(\sigma )). \\ (\texttt{if}~b~\texttt{then}~c_1~\texttt{else}~c_2) \,;c_3&\triangleq \lambda \sigma .\, c_3(\textsf {match } \text {eval}(b, \sigma ) \textsf { with} ~\vert ~ \texttt {false}\Rightarrow c_1(\sigma ) \\&\,\,\,\quad \qquad \qquad \qquad \qquad \qquad \qquad \vert ~ \texttt {true}\Rightarrow c_2(\sigma )). \end{aligned}$$

They are exactly the same function in the meta-language and will satisfy the same Hoare triple. Proofs of structural rules and inversion rules for a shallowly embedded language are similar to their proofs in a big-step-based shallowly embedded program logic (Sect. 4.1) since both uses big-step semantics to define the semantics. In this paper, we will mainly discuss deeply embedded programming languages.

3.2 Embeddings of Assertion Languages

To reason about a program’s effect on program states, a Hoare-style program logic uses an assertion language to describe program state. A shallowly embedded assertion is a predicate in the meta-logic that directly defines the set of states. A deeply embedded assertion language specifies syntax trees of assertions first and then defines how to interpret assertions as sets of states. For example, Fig. 2 defines a deep embedding of an assertion language. Figure 7 defines a shallow embedding of the assertion language (only a snippet of it), which is also the interpretation for the deeply embedded one.

Fig. 7

A shallowly embedded assertion language: for clarity, we write $\sigma \vDash P$ for $P \, \sigma$ to denote that $\sigma$ satisfies the assertion in the rest of the paper

Unlike programming languages, we observe that shallowly embedded assertion languages are generally preferred by program verification framework developers, as Table 1 indicates that almost all existing works rely on a shallow assertion language. The reason is that the shallowly embedded assertion often has more expressiveness. For one fixed deeply embedded assertion language, we need to define its interpretation in the meta-logic. This interpretation is a meta-logic function from assertions’ syntax trees to sets of program states, i.e., $[\![ \cdot ]\!]\in \text {Assertion}_{\text {deep}} \rightarrow \text {state} \rightarrow \text {Prop}$. Thus, the expressiveness of this deep embedding is no stronger than the expressiveness of “sets of states”, as which the assertion language is formalized in a shallow embedding, i.e., $\text {Assertion}_{\text {shallow}} \triangleq \text {state} \rightarrow \text {Prop}$.

The cause of different embedding choices for the programming language and the assertion language is the difference in the object they describe. Assertion languages describe static objects, i.e. an assertion is always used to determine a set of program states. Thus, it is suitable to directly model assertions as sets. Comparably, programming languages describe dynamic objects and transitions of program states. Verification projects for different real programming languages need to embody different features of those languages, e.g., concurrency. However, there exists no simple shallow embedding of a programming language that can describe these features concisely, e.g., we have mentioned in the previous part that denotational shallow embeddings are difficult to express concurrency. Therefore, formalizing different programming languages’ syntax in deep embeddings is preferable to directly using shallow embeddings.

In this paper, we will stick to the shallow embedding of assertion languages defined in Fig. 7.

3.3 Embeddings of Program Logics

When formalizing logics⁶ (e.g. the propositional logic or a Hoare logic), a shallowly embedded logic defines a statement to be valid directly using semantics. We mainly consider partial correctness in this paper, and one common definition of shallowly embedded Hoare triple is: $\vDash \{ P \} c \{ Q \}$ iff. for any initial state $\sigma _1$, if $\sigma _1$ satisfies assertion P, then the execution of c from $\sigma _1$ does not cause an error; and for and any ending state $\sigma _2$ reachable from $\sigma _1$ in the execution of c, $\sigma _2$ satisfies Q. Verification tool developers can prove many properties about valid triples and use them as “proof rules” to assist users in program verification. In practice, there are different ways to shallowly embed a program logic, which we discuss in Sects. 4.1, 4.2, 4.3.

In contrast, a deeply embedded logic formalizes the proof tree inductively by giving admitted proof rules, and we say a statement is provable under the logic, denoted by $\vdash \{ P \} c \{ Q \}$, iff. it can be constructed from these proof rules. Users of a verification tool can use these proof rules to build a proof tree of their program specifications.

To ensure proof rules given in a deeply embedded logic are consistent with program behaviors, one needs to additionally prove the logic sound, that is, every provable statement is also valid, i.e., for any statement S, if $\vdash S$ then $\vDash S$. In simple and common cases, this soundness theorem can be proved by induction over proof trees, i.e. it suffices to prove that every proof rule will always generate valid Hoare triples from valid triples. Using the sequential rule (hoare-seq) as an example,

the induction step is to prove:

$$\begin{aligned} \vDash \{P\} c_1 \{Q\} \text { and } \vDash \{Q\} c_2 \{R\} \text { imply }\vDash \{P\} c_1 ;c_2 \{R\} \end{aligned}$$

(6)

In comparison, there is no counterpart of this soundness property when using a shallowly embedded logic. To use this sequential rule in a shallowly embedded logic, one needs to directly prove property (6). This fact implies that the implementation of a sound deeply embedded program logic always accompanies an underlying shallowly embedded one.

In some nontrivial cases, one has to introduce an auxiliary validity definition in order to prove the soundness of logic in two steps: (1) for any triple S, prove $\vdash S$ implies by induction over the proof tree; (2) show that does imply $\vDash S$ by semantic analysis. For example, Brookes’s concurrent separation logic soundness proof [7] uses this technique. In comparison, a shallow embedding strategy will directly formalize the auxiliary validity, and establish “proof rules” based on it. We discuss this soundness proof technique later in Sect. 8.1.2.

In conclusion, we can choose arbitrary combinations of shallow/deep embeddings among the programming language, the assertion language, and the program logic to instantiate a foundational verification tool. In this paper, we mainly focus on a deeply embedded programming language and a shallowly embedded assertion language, but consider different embeddings of program logics which we will discuss soon in Sect. 4.

4 Different Embeddings of Program Logics

As we have mentioned, there exists different ways to embed a program logic. In this section, we present three different shallow embeddings (Sects. 4.1, 4.2, 4.3) and a deep embedding (Sect. 4.4) to formalize the program logic in Fig. 2. Under each formalization, the chosen primary rules in Fig. 2 are sound. For each embedding method, we also demonstrate which existing Hoare-logic-based verification projects and how do their program logic fit into the category as Table 1 shows.

Meanwhile, there also exists other non-Hoare-logic-based verification approaches, which we discuss in Sect. 4.5.

Verification projects we review in this section all have certain unique features and complex mechanisms and it is difficult to cover all of them, e.g., support for concurrency. Some also do not support control flow reasoning and we do not discuss how to extend them with control flows to support our toy language. We only discuss some basics of their embeddings and related features that can classify them into each category.

4.1 Big-step (BigS) Based Shallow Embedding

Figure 8 describes notations defining the big-step semantics of the While-CF language, where $(c, \sigma _1) \Downarrow (\text {ek}, \sigma _2)$ states that from program state $\sigma _1$, the program c may terminate with exit kind $\text {ek}$, which could be normal exit, denoted by $\epsilon$, or break, continue exit, and the state will be changed to $\sigma _2$. We use $(c, \sigma ) \Uparrow$ to denote that an error would occur for the execution of c from state $\sigma$. The big-step semantics is defined recursively, e.g., the semantics of the sequencing command is Seq1 and Seq2. For the sake of space, we put the full definition (which is standard) in Appendix A.

Fig. 8

Notations for Big-step semantics

Based on this big-step semantics, a (partial correctness) triple is defined to be valid, $\vDash _\text {b}\{ P \} c \{ Q, [R_\text {brk}, R_\text {con}] \}$, iff. for any $\sigma _1$ satisfying precondition P, (1) the execution of c from $\sigma _1$ is safe and does not cause error, and (2) if the execution terminates, the ending program state satisfies the corresponding post-condition.

$$\begin{aligned} \begin{array}{rcl} \vDash _\text {b}\{ P \} c \{ Q, [R_\text {brk}, R_\text {con}] \} &{} \text {iff.} &{} \text {for all}\, \sigma _1 \vDash P, \lnot \,(c, \sigma _1)\Uparrow \\ &{}&{} \text {and for all } \text {ek}, \sigma _2, \text {if }(c, \sigma _1) \Downarrow (\text {ek}, \sigma _2) \\ &{}&{} \quad \text {then }\text {ek}= \epsilon \text { implies } \sigma _2 \vDash Q\\ &{}&{} \quad \text {and }\text {ek}= \text {brk}\text { implies } \sigma _2 \vDash R_\text {brk}\\ &{}&{} \quad \text {and }\text {ek}= \text {con}\text { implies } \sigma _2 \vDash R_\text {con}\end{array} \end{aligned}$$

Related Projects

Klein et al. [8] formalizes an imperative functional programming language in Isabelle/HOL, which is a shallowly embedded one using the state monad in HOL. Based on this language, Lammich [24] builds a logic in big-step-based shallow embedding in Isabelle/HOL. The logic embedding is almost identical to the one discussed above, but it does not consider control flows and only requires the ending state of the normal exit to satisfy the post-condition. Thus, its definition does not have the last two conjuncts above. Based on Lammich’s logic [24], Zhan [48] verifies imperative implementations of some data structures in Isabelle/HOL using its auto2 prover [47]. Nipkow’s Hoare logic in Isabelle/HOL [32, 33] also uses big-step embedding. Many verification has been performed based on these logics in Isabelle, e.g., Lammich and Nipkow [25] proves the correctness of priority search tree and Prim’s and Dijkstra’s algorithm in Isabelle.

Cook’s famous Hoare logic’s soundness and completeness proof [14] uses big-step-based shallow embedding as the logic’s validity definition and proves many properties including logic’s soundness and completeness w.r.t. it.

Software foundation [36] is a famous textbook for teaching Coq formalization. Its second volume introduces Hoare logics both in the big-step-based embedding and the deep embedding, where the former is also the validity definition of the latter. Its sixth volume introduces a separation logic built with the big-step-based embedding. The simplicity of the big-step-based embedding makes it a good introduction to separation logic for beginners.

However, similar to the situation of shallowly embedded language (Sect. 3.1), the big-step semantics struggles to support complex semantic features like concurrency. Indeed, among concurrent program verification projects we have surveyed, none of them is based on the big-step semantics.

4.2 Weakest Precondition (WP) Based Shallow Embedding

Another shallow embedding method is to embed the logic using the weakest precondition defined by small-step semantics. We want to emphasize that the weakest precondition here is directly defined by semantics instead of encoding by some existing Hoare logic.

We use $(c, \kappa , \sigma ) \rightarrow _c (c', \kappa ', \sigma ')$ to describe a small-step in command reduction and $\rightarrow _c^*$ to describe the reflexive transitive closure of $\rightarrow _c$. The small-step reduction is a binary relation between triples of the focused term⁷c, the continuation (control stack) $\kappa$, and the program state $\sigma$. The control flow commands make it slightly different from textbook definitions. We mainly follow Comp-Cert Clight’s definition style and list the most important semantic rules in Fig. 9.

• (1) When the focused term begins with a for-loop, the loop is pushed into the control flow stack and the loop body (followed by $\texttt{continue}$) is loaded into the focused term.

• (2) When the increment step for the previous iteration finishes, the loop body is loaded for the next iteration.⁸

• (3) When the focused term reduces to , the increment step $c_2$ is loaded and the innermost loop’s continuation is updated to Kloop$_2$.

• (4) When the focused term reduces to $\texttt{break}$, the innermost loop is popped out of the continuation and the program is set to to continue execute the remaining control stack.

• (5), (6) When the focused term reduces to or , any KSeq continuation at the top of the continuation will be skipped. As a result, if an execution from terminates, it must terminate at , , or .

Fig. 9

Notations for Small-step semantics

The shallowly embedded weakest pre-condition can be defined on this small-step semantics. We use $\sigma ~\vDash ~\textsf {WP} (c, \kappa ) \{ Q, [\vec {R}] \}$ to denote that a program state $\sigma$ satisfies the weakest pre-condition for the focused program c and the continuation $\kappa$ with post-conditions Q and $[\vec {R}]$. The $\textsf {WP}$ is defined as the largest set such that $\sigma ~\vDash ~\textsf {WP} (c, \kappa ) \{ Q, [\vec {R}] \}$ iff.

• Terminal Case: $\kappa$ is $\epsilon$ and (1) $c = \texttt{skip}$ and $\sigma \vDash Q$ or (2) $c = \texttt{break}$ and $\sigma \vDash R_\text {brk}$ or (3) $c = \texttt{continue}$ and $\sigma \vDash R_\text {con}$;

• Preservation Case: Or there exists some $c', \kappa ', \sigma '$ that $(c, \kappa , \sigma )$ can be further reduced to, i.e. $(c, \kappa , \sigma ) \rightarrow _c (c', \kappa ', \sigma ')$, and for any $c', \kappa ', \sigma '$ such that $(c, \kappa , \sigma ) \rightarrow _c (c', \kappa ', \sigma ')$, the judgement $\sigma ' \vDash \textsf {WP} (c', \kappa ') \{ Q, [\vec {R}] \}$ holds.

The terminal case ensures that the ending program state will satisfy post-conditions, and the preservation case guarantees that it can always step forward and eventually reach an ending state satisfying post-conditions.

A triple is defined to be valid under the weakest-precondition-based shallow embedding, $\vDash _w \{ P \} c \{ Q \}$, iff. for any state $\sigma$ satisfying precondition P, we have $\sigma \vDash \textsf {WP} (c, \epsilon ) \{ Q, [\vec {R}] \}$.

Define WP Using Bourbaki–Witt Fixed Point Thereom

We may implement the above weakest-precondition’s definition using the Bourbaki–Witt fixed point theorem [6, 44], which is used by many existing frameworks to define the weakest-precondition-based embedding and is used in our Coq formalization.

Theorem 1

(Bourbaki–Witt fixed point theorem) If $(L, \le )$ is a non-empty complete ordered chain, and $f: L \rightarrow L$ satisfies $f(x) \ge x$ forall x, then f has a fixed point. For some $x_0 \in L$, let $g: \mathbb {N} \rightarrow L$ be a function with

$$\begin{aligned} g(0) = x_0 \qquad g(n+1) = f(g(n)), \end{aligned}$$

then $\lim _{n\rightarrow \infty }g(n)$ is a fixed point.

Here, the type L is sets of program configuration, i.e., $\mathcal {P}(\text {state} \times \text {command} \times \text {continuation})$, and order $\le$ is $\supseteq$. The function f is defined as below, which removes configurations that will either cause an error or contradict with the post-conditions from the input set x.

where

$$\begin{aligned} \text {reducible}(c, \kappa , \sigma ) \text { iff. } \exists c', \kappa ', \sigma '.\, (c, \kappa , \sigma ) \rightarrow _c (c', \kappa ', \sigma ') \end{aligned}$$

To utilize Theorem 1, we only need to find a function g satisfying these conditions and use its limit as the fixed point. We define the function g as

$$\begin{aligned} \lambda n.\, \lambda \sigma , c, \kappa .\, \forall m \le n.\, \sigma \vDash {\textrm{WP}}(m, c, \kappa )\{ Q,[\vec {R}] \} \end{aligned}$$

where

$$\begin{aligned} \sigma \vDash {\textrm{WP}}(m, c, \kappa )\{ Q,[\vec {R}] \}&\text { iff. } \left( \begin{aligned} \kappa = \epsilon \wedge \left( \begin{aligned} (c = \texttt{skip}\wedge \sigma \vDash Q) \vee \\ (c = \texttt{break}\wedge \sigma \vDash R_\text {brk}) \vee \\ (c = \texttt{continue}\wedge \sigma \vDash R_\text {con}) \end{aligned}\right) \end{aligned} \right) \nonumber \\ \vee&\left( \begin{aligned} 0 < m \Rightarrow \left( \begin{aligned} \text {reducible}(c, \kappa , \sigma ) \wedge \\ \forall c',\kappa ',\sigma '. \left( \begin{aligned} (c,\kappa ,\sigma )\rightarrow _c(c',\kappa ',\sigma ') \Rightarrow \\ \sigma ' \vDash {\textrm{WP}}(m-1, c', \kappa ')\{ Q,[\vec {R}] \} \end{aligned}\right) \end{aligned}\right) \end{aligned}\right) \end{aligned}$$

(7)

One may prove that $g(0) \in L$ and $g(n+1) = f(g(n))$ and define the weakest precondition by taking the limit of g(n) as below.

$$\begin{aligned} \sigma \vDash {\textrm{WP}}(c, \kappa )\{ Q,[\vec {R}] \} \text { iff. } \forall n \in \mathbb {N}.\, \sigma \vDash {\textrm{WP}}(n, c, \kappa )\{ Q,[\vec {R}] \} \end{aligned}$$

If the reader is familiar with the step-indexing technique [3], they may find that a meta-logic equipped with step-indices (e.g., Iris [20]) can also define the weakest precondition as the Bourbaki–Witt fixed point. In a step-indexed world, one may add an index number to the interpretation of a predicate and use a later modality to lower the index by one.

$$\begin{aligned} \sigma \vDash P&\iff \forall n.\, \sigma \vDash P_n \\ \sigma \vDash (\triangleright P)_n&\iff n = 0 \vee \sigma \vDash P_{n-1} \end{aligned}$$

To use step indexing to define the weakest precondition, the number of execution steps is considered as the index. For example, the ordinal number n in $\sigma \vDash {\textrm{WP}}(n, c, \kappa )\{ Q,[\vec {R}] \}$ represents the number of execution steps during which this predicates guarantees the program to not produce an error. The weakest precondition’s definition can also be simplified using these step-indexing notations.

$$\begin{aligned} \sigma \vDash {\textrm{WP}}(c, \kappa )\{ Q,[\vec {R}] \}&\text { iff. } \left( \begin{aligned} \kappa = \epsilon \wedge \left( \begin{aligned} (c = \texttt{skip}\wedge \sigma \vDash Q) \vee \\ (c = \texttt{break}\wedge \sigma \vDash R_\text {brk}) \vee \\ (c = \texttt{continue}\wedge \sigma \vDash R_\text {con}) \end{aligned}\right) \end{aligned} \right) \\&\vee \left( \begin{aligned} \text {reducible}(c, \kappa , \sigma ) \,\wedge \\ \forall c',\kappa ',\sigma '. \left( \begin{aligned} (c,\kappa ,\sigma )\rightarrow _c(c',\kappa ',\sigma ') \\ \Rightarrow \sigma ' \vDash \triangleright {\textrm{WP}}(c', \kappa ')\{ Q,[\vec {R}] \} \end{aligned}\right) \end{aligned}\right) \end{aligned}$$

Define WP Using Tarski Fixed Point Thereom

The other way to define the weakest-precondition is through the Tarski fixed point theorem [42].

Theorem 2

(Tarski fixed point theorem) For a complete lattice $(L, \le )$ and a monotone function $f: L \rightarrow L$, the set of all fixed points of f is also a complete lattice with $\sup \{x\in L \,\vert \, x \le f(x)\}$ as the greatest fixed point.

Here, the type L is still sets of program configuration, and the order $\le$ is the subset relation $\subseteq$. The function f(x) increases (thus it guarantees monotonicity) the input configuration set x with configurations that can become configurations in x after one step of execution, and if the input set is empty, it returns configurations already satisfying the post-conditions Q and $\vec {R}$.

One may simply applies the Tarski fixed point theorem by taking the supremum of the chain $\emptyset \le f(\emptyset ) \le f(f(\emptyset )) \le \cdots$ as the weakest-precondition definition.

This approach is equivalent to directly using a co-inductive definition in Coq. While we did not find any work that uses co-inductive definitions for weakest-precondition, Liang [26] and Xu et al. [45] uses co-inductively defined simulations when formalizing their relational Hoare logic. We also proved in our Coq formalization that co-inductively defined weakest-preconditions are equivalent to the one defined using the Bourbaki–Witt fixed point.

Related Projects

Fine-grained Concurrent Separation Logic (FCSL) [40] is a framework for verifying concurrent programs. It uses mixed embedding (deep and shallow embedding) for its programming language and a weakest-precondition-based shallow embedding for its program logic. Its program is defined by an action tree, where each edge, the atomic action, is defined by a transition between states, i.e., a shallow embedding. In the action tree’s syntax definition below, $\omega$ is a leaf node indicating the divergence of a thread and $\text {ret } v$ is a leaf node indicating the termination of a thread with return value v. The concatenation a :  : k of the action a and the context k is the sequential execution a and k with a’s result as arguments. Similarly, parallel composition first interleaves executions of tree $t_1$ and $t_2$ and passes their results to the context k.

$$\begin{aligned} \begin{array}{rcl} t, t_1, t_2 \in \text {Tree} &{}{:}{=}&{} \omega ~\vert ~ \text {ret } v ~\vert ~ a {:}{:} (k: \text {Val}\rightarrow \text {Tree})\\ &{} ~\vert ~ &{} (t_1 \Vert t_2) {:}{:} (k: \text {Val} \times \text {Val} \rightarrow \text {Tree}) \\ a \in \text {Action} &{}{:}{=}&{} \text {state}\rightarrow \text {state}\rightarrow \text {Prop} \end{array} \end{aligned}$$

The definition below is FCSL’s [40] embedding of their Hoare triple (we omit details about concurrency). The always predicate (8) is similar to our weakest precondition’s definition, which asserts that the memory safety at each step and at each step the assertion P should hold for the program state and the action tree. This assertion of always predicate in the Hoare triple (10) ensures that the post-condition holds at leaf nodes. It also uses the Bourbaki–Witt fixed point approach to define the weakest precondition. The k in (8) and (9) serves the purpose of an ordinal number.

$$\begin{aligned} \text {always}^{k}\,\sigma \,t\,Q&\text { iff. } \text {memsafe}(\sigma , t) \wedge Q(\sigma ,t) \wedge \nonumber \\&\quad \quad \forall \sigma ', t'.\, (k > 0 \wedge ((\sigma , t)\rightarrow (\sigma ', t'))) \Rightarrow \text {always}^{k-1}\,\sigma '\,t'\,Q \end{aligned}$$

(8)

$$\begin{aligned} \text {always}\,\sigma \,t\,Q&\text { iff. } \forall k \in \mathbb {N}.\, \text {always}^{k}\,\sigma \,t\,Q \end{aligned}$$

(9)

$$\begin{aligned} \vDash \{ P \} c \{ Q \}&\text { iff. } \forall \sigma .\, \sigma \vDash P \Rightarrow \text {always}\,\sigma \,t\,(\lambda \sigma , t.\, \forall v.\, t = \text {Ret }v \Rightarrow Q(\sigma ,v)) \end{aligned}$$

(10)

Iris is a higher order concurrent separation logic for verifying the correctness of functional programs. Its framework is parameterized with a programming language and uses the weakest-precondition-based embedding. When concurrency is not involved (Sect. 6.3.2 of [20]), Iris embeds their logic by weakest pre-conditions below as a separation logic proposition in Iris (iProp).

(11)

(12)

The first disjunct (11) asserts that if the expression e is a value, then the evaluation has terminated and the program state and the evaluation result e should satisfy $\Phi$. The second disjunct (12) specifies behaviors when e is not a terminal and should be further reduced. $S(\sigma )$ injects program state $\sigma$ into an iProp. The disjunct (12) will first consume a piece of memory injected by $\sigma$ and asserts that expression e is reducible with this piece of memory ($\text {reducible}(e, \sigma )$). Then, for any new expressions $e'$ and $\sigma '$ it can reduce to by small-step semantics $\rightarrow _t$, we can still have the memory $S(\sigma ')$ that it reduces to and the new expression $e'$ still preserves the weakest pre-condition. Iris’s propositions iProp uses the step-index to solve the circularity when defining higher-ordered ghost states, which happens to be a suitable choice of the ordinal number in the definition of the co-inductive weakest precondition. Iris’s Hoare triple⁹$\{ P \} e \{ \Phi \}$ is embedded as $P \vdash \textsf {WP}\,e\,\{\Phi \}$, which conforms with our prototypical weakest-precondition-based embedding.

FCSL and Iris both support concurrent program verifications through mechanisms of angelic updates (view shifts in Iris). Iris is also extended to support prophecy variables [21]. However, these features are out of this paper’s scope. For simplicity, definitions in this section only consider sequential programs and remove features supporting concurrency. For the complete definition, readers may refer to their original papers [20, 40].

4.3 Continuation (Cont.) based Shallow Embedding

Continuation-based shallow embedding defines the Hoare triple through Hoare tuple $\{ P \} (c, k)$, pronounced P guards (c, k). An assertion P guards the execution of a program c and a continuation $\kappa$, $\{ P \} (c, \kappa )$, iff. for any program state $\sigma$ satisfying the pre-condition P, we have safe($c, \kappa , \sigma$), which is the largest set of configurations with following properties.

• Terminal Case: $\kappa$ is $\epsilon$, and c is $\texttt{skip}$, $\texttt{break}$, or $\texttt{continue}$;

• Preservation Case: Or $(c, \kappa , \sigma )$ can be further reduced by $\rightarrow _c$, and for any $(c', \kappa ', \sigma ')$ it reduces to, we should have safe$(c', \kappa ', \sigma ')$.

One could use either fixed point formalization in Sect. 4.2 for defining safe($c, \kappa , \sigma$).

A triple $\{ P \} c \{ Q, [\vec {R}] \}$ is valid iff. for arbitrary continuation $\kappa$,

$$\begin{aligned} \text {if } \quad {\left\{ \begin{array}{ll} \quad \{ Q \} (\texttt{skip}, \kappa ) &{}\\ \quad \{ R_\text {brk} \} (\texttt{break}, \kappa ) &{}\\ \quad \{ R_\text {con} \} (\texttt{continue}, \kappa ) &{} \end{array}\right. } \text {then } \quad \{ P \} (c, \kappa ). \end{aligned}$$

It states that for any continuation that safely executes from different post-conditions with corresponding exit kind, it should safely executes after program c’s execution from the pre-condition.

Related Projects

The original shallowly embedded VST [2] uses a deeply embedded programming language and a program logic in continuation-based shallow embedding. The Hoare triples in shallowly embedded VST extend our definition with function invocations and concurrent separation logic. Besides these features, which we discuss later in Sect. 9, its embedding is almost identical to the prototypical definition above.

4.4 Deep Embeddings

As clarified in Sect. 3, a deep embedding of program logic is a proof system with inductively defined proof trees. Different deep embeddings of program logics with fixed languages and forms of judgements have different sets of admitted proof rules. For example, we may consider a proof system with primary proof rules from Fig. 2 as a deep embedding. In Coq, one can define the deep embedding with an inductive relation shown below. Here, provable P c Q Rb Rc stands for the Hoare triple $\vdash \{ P \} c \{ Q, [R_b, R_c] \}$.

An arbitrary set of admitted proof rules may not be correct, thus we need to prove the soundness of such a proof system. To do so, we need to define the validity of a logic judgement, i.e., the corresponding shallowly embedded logic. We can prove the soundness by showing that each proof rule is valid in the shallow embedding and the shallowly embedded logic is sound. We can easily prove primary proof rules in Fig. 2 to be valid under all three shallow embeddings in Sect. 4.1, 4.2, 4.3.

Related Projects

Simpl [39] is a tool in Isabelle/HOL for verifying sequential programs, which has been used to verify seL4 code [22]. It uses a deeply embedded programming language and program logic. Its judgement is $\vdash \{ P \} c \{ Q,Q_\text {ek} \}$ with the following validity definition.

$$\begin{aligned} \begin{array}{rcl} \vDash \{ P \} c \{ Q, Q_\text {ek} \} &{}\triangleq &{} \forall \sigma _1, \sigma _2.\, \sigma _1 \in \text {Normal } P \Rightarrow \langle c, \sigma _1 \rangle \Downarrow \sigma _2 \Rightarrow \\ &{}&{} \sigma _2 \in \text {Normal }Q \cup \text {Abrupt }Q_\text {ek}\end{array} \end{aligned}$$

The above definition says after the execution from program states satisfying the precondition, the resulting state satisfies the normal and abrupt post-conditions depending on its exit kind. Both $\text {Normal }Q$ and $\text {Abrupt }Q_\text {ek}$ exclude any faulty state, ensuring the safety of the program. Simpl also has mechanisms to ignore certain errors in the program logic and to support total correctness, which we omit here.

CSimpl [38] is a framework for concurrent program verification based on rely guarantee reasoning. Its programming language is a deeply embedded imperative language supporting concurrency. Its logic is deeply embedded by giving inference rules of the logic with judgement $\vdash \{ P \} c \{ Q, Q_\text {ek} \}$, where P is the pre-condition and $Q, Q_\text {ek}$ are normal and control flow post-conditions respectively. It uses the rely-guarantee method to reason about concurrency. We omit details related to the usage of rely-guarantee in its formalization and refer readers to its original paper. To show the soundness of its proof system, CSimpl defines judgement’s validity in three steps.

• It uses $\text {assum}(c, P)$ to denote a set of small-step reduction steps of c (lists of intermediate commands and states) from pre-condition P.

• It uses $\text {comm}(Q, Q_\text {ek})$ to denote a set of reduction steps that have terminal state satisfying post-conditions $Q, Q_\text {ek}$.

• The judgement $\vdash \{ P \} c \{ Q, Q_\text {ek} \}$ is valid iff. $\text {assum}(c, P)$ is a subset of $\text {comm}(Q, Q_\text {ek})$. The inclusion implies any execution of c from pre-condition P will terminate in post-conditions $Q, Q_\text {ek}$.

The definition of the set $\text {comm}(Q, Q_\text {ek})$ is almost identical to the weakest precondition in Sect. 4.2. In conclusion, CSimpl uses deeply embedded logic with the weakest-precondition-based shallow embedding as its validity.

Certified assembly program (CAP) [46] and XCAP [31] use deeply embedded language and deeply embedded logic with judgement $\vdash \{P\}\, c$ to verify assembly programs. The logic guarantees that an assembly program c can execute safely if the program state satisfies the pre-condition P. Both work formalize the logic with a set of inference rules as its deep embedding and prove the soundness under the continuation-based shallow embedding. Both work’s objective is to verify the program’s safety instead of functional correctness, therefore the judgement and logic look different from the one in our paper.

Xu et al. [45] develop $\mu$C, a framework for verifying preemptive operating systems. The framework uses deeply embedded program logic. The logic is proven sound w.r.t. a weakest-precondition-based shallow embedding, which is similar to those in Sect. 4.2.

Software foundation [36] introduces a toy example of a deeply embedded Hoare logic with big-step-based shallow embedding as its validity, as we have mentioned in Sect. 4.1.

4.5 Other Logic Based Verification Methods

So far, we have discussed four Hoare logic embeddings and foundational verification frameworks that use these embeddings. Most of these frameworks use Hoare triples as program specifications and prove them mainly by applying proof rules to Hoare triples, which we refer to as Hoare-logic-based verification. Nevertheless, there exist other logic-based verification methods that do not use Hoare triples and Hoare logics as their primary tools. In this section, we will briefly review some of these non-Hoare-logic-based verification techniques: Hoare monad and Dijkstra monad in Sect. 4.5.1, Iris (weakest-precondition-based verification) in Sect. 4.5.2, and Characteristic Formulae in Sect. 4.5.3. It is not clear whether these approaches are better than pure Hoare-logic-based ones, and the comparison among them is not the focus of this paper.

4.5.1 Hoare Monad and Dijkstra Monad

Instead of Hoare logic, we can also use Hoare monad and Dijkstra monad to assert and verify the correctness of a program. Based on their Hoare type theory [30], Nanevski et al. [29] type a program using the Hoare monad $\texttt {ST}\, P\, A\, Q$, where the type of the program asserts the its execution from state satisfying the pre-condition P will return with a value of type A, and the return value and the ending state will satisfy the post-condition Q over both the return value and the program state. The type of a large program is derived from the types of statements that assemble it.

For example, the rule above defines how to compose two Hoare monads through the bind operation (lambda function application), which is similar to the hoare-seq rule. The type of $e_1\,e_2$ is derived by the type of $e_1$ and $e_2$.

The typing proof of Hoare monad cannot be easily automated due to some existential quantifiers over some intermediate program state. A series of works [1, 19, 27, 41] develops Dijkstra monad to improve the automation of such technique and allow reasoning about program with more features like exception, non-determinism, and IO. Different from Hoare monad, Dijkstra monad types a program as $\texttt {WP\_ST}\,A\,\textsf {wp}$, a predicate transformer mapping a postcondition of the computation to its precondition, where A is the return type and wp is the weakest precondition. The weakest precondition wp is of the type

$$\begin{aligned} (A \times \text {state} \rightarrow \text {Prop}) \rightarrow \text {state} \rightarrow \text {Prop} \end{aligned}$$

which is exactly a predicate transformer from the postcondition to the precondition. Below is the typing rule for the bind in the Dijkstra monad.

This rule composes predicate transformers $\textsf {wp}_1\,v$ (parameterized over the return value v) and $\textsf {wp}_2$ into a new one to type $e_1\,e_2$.

The typing of programs such as Hoare monads and Dijkstra monads resembles the definition of the program’s big-step semantics, as all of them are definitions by structural induction over the program’s syntax. Still using the bind operation as an example, bind-bigs defines the big-step semantics of $e_1\,e_2$.

It is similar to bind-hst except that the relationship between the beginning state and ending state defined in bind-bigs becomes the relationship between the precondition and postcondition in bind-hst. This similarity is even more obvious in bind-dst, where programs’ effects on the pre/post-conditions are composed instead of composing their effects on the program state.

4.5.2 Weakest-Precondition-Based Verification

In Sect. 4.2, we have embedded a Hoare triple using the weakest precondition: $\vDash _w \{ P \} c \{ Q \}$, iff. for any state $\sigma$ satisfying precondition P, we have $\sigma \vDash \textsf {WP} (c, \epsilon ) \{ Q, [\vec {R}] \}$. Although we use the Hoare logic to reason about triples using this embedding, it is also possible to directly reason about the weakest precondition, which is the approach taken by Iris [20].

We use the if-seq rule to demonstrate the weakest-precondition-based verification method and its advantage. Suppose we want to prove $\{ P \} (\texttt{if}~e~\texttt{then}~c_1~\texttt{else}~c_2) \,;c_3 \{ Q \}$ in Iris for some $c_1, c_2, c_3, e$. It is equivalent to prove that , which has the following weakest precondition derivation (13). Since Iris’s meta-logic is a separation logic, we may use in place of implications.

(13)

We can first apply the wp-bind rule to hide the second part $c_3$ of the sequential composition into the post-condition as another weakest precondition. The rule wp-bind extract the evaluation context (K) of the first command to execute (c) into a separate weakest precondition into the post-condition. This enables provers to focus on the execution of command c before verifying the evaluation of K that will be affected by the outcome v of c.

Then, by wp-if rule, we need to prove the weakest preconditions of two branches, ($\dagger$) and ($\ddagger$), separately. Then, take ($\dagger$) for example, we can further symbolically execute $c_1$ in Iris’s weakest precondition calculus until it reaches a terminal value $v_1$ with the memory satisfying $P'$. Then, by wp-val and wp-seq, we can further reduce the proof goal into a weakest precondition only about the remaining $c_3$ and eventually reach a tautology after symbolic executions of $c_3$’s weakest precondition. We can do a similar proof for the other branch ($\ddagger$) as well.

(14)

As we can see, the proof of two branches ($\dagger$) and ($\ddagger$) is exactly the proof of two branches of $\texttt{if}~b~\texttt{then}~c_1 \,;c_3~\texttt{else}~c_2 \,;c_3$. The ability to put future computations (like $c_3$ in this example) into the post-condition and postpone their proofs essentially makes extended rules like if-seq for free.

Users of Iris mainly use this kind of symbolic execution for weakest precondition, instead of the symbolic execution for Hoare triples. Therefore, most of our discussions about extended rules do not apply to the Iris framework.

4.5.3 Characteristic Formulae

Charguéraud [10, 11] and Guénea et al. [17] use characteristic formulae to verify programs and builds CFML above its logic for the verification of imperative Caml programs. The main idea of characteristic formulae is to define a function $\textsf {cf}$ of type $\text {command} \rightarrow (\text {assertion} \rightarrow \text {assertion} \rightarrow \text {Prop})$. The result $\textsf {cf}(c)$ defines the relationship between the precondition and the postcondition of command c’s Hoare triple. For example, the result for the sequential composition is defined below.

$$\begin{aligned} \textsf {cf}(c_1 \,;c_2) \triangleq \lambda P.\, \lambda Q.\, \exists R.\, \textsf {cf}(c_1)\,P\,R \wedge \textsf {cf}(c_2)\,R\,Q \end{aligned}$$

(15)

This formalization is highly similar to the deeply embedded Hoare logic. The proof tree for a program in a deeply embedded Hoare logic is built recursively according to the program’s syntax tree. While characteristic formulae are also generated recursively according to the program’s syntax tree in a similar fashion. For example, the definition (15) resembles the deeply embedded sequence rule below.

After a characteristic formula is generated, users can then verify in the meta-logic whether it satisfies the specification they want to prove. In this way, they can directly apply features in the meta-logic (usually the one directly supported by the interactive theorem prover like Coq) to do the proof.

On the other hand, the characteristic formulae generator cf is proved sound w.r.t. a big-step semantics,

$$\begin{aligned} \forall c, P, Q.\, \textsf {cf}(c)\,P\,Q \Rightarrow \, \vDash _b \{ P \} c \{ Q \} \end{aligned}$$

(16)

which makes the framework foundational. Here, the soundness definition (16) is a simplified version using the big-step-based embedding (but without control flows) introduced in Sect. 4.1, while the original definition in Charguéraud’s work (Vol.6 of Software Foundation [10]) also considers features like separation logics.

5 Proving Extended Rules in Different Embeddings

So far, we introduced three categories of extended proof rules in Sect. 2 and reviewed four common embedding methods for Hoare logic in Sect. 4. This section investigates proofs or disproofs of these rules under different embedding methods. We start by arguing the necessity to prove extended rules in different embeddings.

Different embeddings define different sets of triples. Given a Hoare logic embedding $\vDash$, we use it to define a set of all triples that are satisfiable under the embedding as $\{S ~\vert ~ \vDash S\}$. For two different embeddings $\vDash _1$ and $\vDash _2$, if there exists some triple S such that ${\vDash _1 S} \nLeftrightarrow {\vDash _2 S}$, then we know sets $\{S ~\vert ~ \vDash _1 S\}$ and $\{S ~\vert ~ \vDash _2 S\}$ are not equal. Typically, a property that holds for elements in one set does not necessarily hold for those in a different set. Extra elements in a different set may not satisfy the property. As a result, a rule admissible in one embedding is not necessarily admissible in another embedding. Thus, it is necessary to check whether each extended rule holds under each of these embeddings.

• The shallow embeddings we have considered so far define different sets of triples. Although it is possible to bridge the big-step-based embedding and the weakest-precondition-based embedding by proving the equivalence of two semantics, the equivalence between these embeddings and the continuation-based one is not trivial. The continuation-based embedding quantifies over an arbitrary continuation following the original command, which is absent in other embeddings. It also employs a reversed implication pattern, a property about post-conditions implies a property about the pre-condition, while other embeddings are not. The difficulty in proofs of extended rules also makes us to believe that different embeddings define different sets of triples.

• The deep embedding in this paper defines different sets of triples from those under shallow embeddings. This is true unless the deep one is proven both sound and complete w.r.t. the shallow one. However, completeness is usually not necessary for a program verification tool because users mainly require the correctness (soundness) of the tool.

  In practice, tool developers do not provide completeness proof because the proofs involved are challenging for a complex program logic. Therefore, we assume the deeply embedded logic is not complete.

Table 2 Extended proof rules in different embedding methods

We find all extended rules in Fig. 3 can be proved for all four embeddings, but some proofs are complicated and some proof obligations may be unreasonably heavy in reality for a more complex language. We list our techniques to overcome these difficulties in Table 2 and make some brief comments here.

• Most proofs for the deep embedding, except the proof of hoare-ex, are simple inductions over proof trees. Rules are proved correct mainly by definitions for the big-step based embedding. These proofs are relatively trivial.

• Most proofs in the weakest precondition based embedding involve defining a simulation relation between pairs of expressions and program states. The if-seq and loop-nocontinue proof in the continuation based embedding uses the same idea. The principle behind these proofs is not difficult but do require significantly more work than those for deep embedding and big-step based embedding. Thus, we would say they are of medium difficulty.

• Proofs for seq-inv and nocontinue in the continuation based embedding not only require this simulation technique, but also demand complex constructions of continuations. These proofs are very complicated.

• hoare-ex’s proofs under shallow embeddings are trivial but are relatively complicated under deep embedding.

In following sections, we will demonstrate our proofs under different embeddings using our WhileCF toy language. These proofs are one of the major contributions of the paper and are formalized in Coq [15].

To review, we paste the extended rules we are going to prove in Fig. 10.

Fig. 10

Representative extended proof rules to be proved

5.1 Deep Embedding

5.1.1 The Choice of the Deep Embedding

Before proving extended rules in some deeply embedded language, we should first fix the deep embedding we want to discuss. Theoretically, difference choices of the primary rule set determine different deep embeddings of program logic. We find that, if we only pick compositional rules, singleton command rules and the consequence rule, we can prove all inversion rules quite easily by proof-tree induction, and on top of that, we can then establish most transformation rules and structural rules in a straightforward way. We choose the deep embedding with rules in Fig. 2 as primary rules. We first stick to this specific deep embedding in this subsection to demonstrate extended rules’ proofs and discuss other possible choices afterwards in Sect. 7.

Proving Inversion Rules.

The proofs of inversion rules in the deep embedding are mainly by induction over the original proof trees. We prove seq-inv and loop-inv in Theorem 3 and Theorem 4 for demonstration. Other inversion rules like if-inv have similar proofs.

Theorem 3

For any P, $c_1$, $c_2$, Q and $\vec {R}$, if $\vdash \{ P \} c_1 \,;c_2 \{ Q, [\vec {R}] \}$, then there exists another assertion S such that $\vdash \{ P \} c_1 \{ S, [\vec {R}] \}$ and $\vdash \{ S \} c_2 \{ Q, [\vec {R}] \}$.

Proof

We prove it by induction over the proof tree of shape $\vdash \{ \cdot \} c_1 \,;c_2 \{ \cdot , [\cdot ] \}$. In fact, the last step of proving $\{ P \} c_1 \,;c_2 \{ Q, [\vec {R}] \}$ is either hoare-seq or hoare-consequence. For the former situation, the conclusion obviously holds. For the latter situation, we can find $P'$, $Q'$ and $\vec {R'}$ such that

$$\begin{aligned} \vdash \{ P' \} c_1 \,;c_2 \{ Q', [\vec {R'}] \}, P \vdash P', Q' \vdash Q, R'_{\text {brk}} \vdash R_{\text {brk}}, \text { and } R'_{\text {con}} \vdash R_{\text {con}}. \end{aligned}$$

By induction hypothesis, we can find S such that $\vdash \{ P' \} c_1 \{ S, [\vec {R'}] \}$ and $\vdash \{ Q \} c_2 \{ Q', [\vec {R'}] \}$. Then, we get $\vdash \{ P \} c_1 \{ S, [\vec {R}] \}$ and $\vdash \{ S \} c_2 \{ Q, [\vec {R}] \}$ by hoare-consequence.

$\square$

Theorem 4

For any $P, c_1, c_2, Q$ and $\vec {R}$, if $\vdash \{ P \} \texttt{for}(;;c_2)~c_1 \{ Q, [R_\text {brk}, R_\text {con}] \}$, then there exists two assertions $I_1, I_2$ such that

$$\begin{aligned} \vdash \{ I_1 \} c_1 \{ I_2, [Q, I_2] \} \text { and } \vdash \{ I_2 \} c_2 \{ I_1, [Q, \bot ] \}, \text { and } P \vdash I_1. \end{aligned}$$

Proof

We prove it by induction over the proof tree of shape $\vdash \{ \cdot \} \texttt{for}(;;c_2)~c_1 \{ \cdot \}$. Similar to the previous proof, the last step in the proof tree is either hoare-loop or hoare-consequence. For the first case, the conclusion trivially holds. For the second case, we can find $P'$, $Q'$ and $\vec {R'}$ such that

$$\begin{aligned} \vdash \{ P' \} \texttt{for}(;;c_2)~c_1 \{ Q', [\vec {R'}] \}, P \vdash P', Q' \vdash Q, R'_{\text {brk}} \vdash R_{\text {brk}}, \text { and } R'_{\text {con}} \vdash R_{\text {con}}. \end{aligned}$$

By induction hypothesis, we can find $I_1, I_2$ such that $\vdash \{ I_1 \} c_1 \{ I_2, [Q', I_2] \}$ and $\vdash \{ I_2 \} c_2 \{ I_1, [Q', \bot ] \}$ and $P' \vdash I_1$. This also implies $P \vdash I_1$ and by hoare-consequence we have $I_1, I_2$ such that $\vdash \{ I_1 \} c_1 \{ I_2, [Q, I_2] \}$ and $\vdash \{ I_2 \} c_2 \{ I_1, [Q, \bot ] \}$.$\square$

Proving hoare-ex rule.

hoare-ex (Theorem 7) is hard to prove in a deeply embedded logic since the proof tree of $\vdash \{ P(x) \} c \{ Q, [\vec {R}] \}$ may be different for a different x. We prove it by induction on the syntax tree of c instead. Here, we only show one induction step in the proof—the case for sequential composition. Other induction steps are proved similarly. A complete proof can be found in our Coq development.

This proof is based on one important assumption about the assertion language: we can quantify over assertions inside an assertion and inject from the meta-logic’s propositions into the assertion language, and moreover:

Hypothesis 5

For any assertion $P, Q, \vec {R}$ and program c, if $\vdash \{ P \} c \{ Q, [\vec {R}] \}$ holds, then we have $P \ \vdash \ \exists P_0. \ \left( \vdash \{ P_0 \} c \{ Q, [\vec {R}] \}\right) \wedge P_0$.

This hypothesis above is an entailment in the assertion logic and the right-hand side is an assertion. In this assertion, $P_0$ is an existentially quantified assertion inside another assertion, and $\left( \vdash \{ P_0 \} c \{ Q, [\vec {R}] \}\right)$ is a meta-logic proposition, stating that a triple is provable, used as a conjunct in a compound assertion. This hypothesis is obviously true since the existentially quantified $P_0$ on the right-hand side can be instantiated by P.

Remark

This kind of assertions, where universe quantifiers and existential quantifiers can quantify over assertions and Hoare triples can be admitted as assertions, are known as impredicative assertions or impredicative polymorphism [31]. Our proof here assumes impredicative assertions are available in the assertion language, which we discuss later in Sect. 8.1.2.

Back to our proof, Hypothesis 5 and seq-inv immediately validates Lemma 6, which is used in the proof of hoare-ex (Theorem 7).

Lemma 6

For any P, $c_1$, $c_2$, R and $\vec {S}$, if $\vdash \{ P \} c_1 \,;c_2 \{ R, [\vec {S}] \}$, then

$$\begin{aligned} \vdash \left\{ P\right\} c_1\left\{ \exists Q. \left( \vdash \{ Q \} c_2 \{ R, [\vec {S}] \}\right) \wedge Q, [\vec {S}]\right\} . \end{aligned}$$

Theorem 7

For any T, P, c, Q and $\vec {R}$, if for any x of type T, we have $\vdash \{ P(x) \} c \{ Q, [\vec {R}] \}$, then $\vdash \{ \exists x.\, P(x) \} c \{ Q, [\vec {R}] \}$.

Proof

By induction on the syntax tree of c, the induction step for the sequential composition is to prove $\vdash \{ \exists x. \ P(x) \} c_1 \,;c_2 \{ R, [\vec {S}] \}$ under the following assumptions:

(IH1):

For any type T and P, Q, R, if $\vdash \{ P(x) \} c_1 \{ Q, [\vec {R}] \}$ holds for any x : T, then $\vdash \{ \exists x. \ P(x) \} c_1 \{ Q, [\vec {R}] \}$.

(IH2):

For any type T and P, Q, R, if $\vdash \{ P(x) \} c_2 \{ Q, [\vec {R}] \}$ holds for any x : T, then $\vdash \{ \exists x. \ P(x) \} c_2 \{ Q, [\vec {R}] \}$.

(Assu):

$\vdash \{ P(x) \} c_1 \,;c_2 \{ R, [\vec {S}] \}$ holds for any x : T.

First, by (Assu) and Lemma 6, $\vdash \left\{ P(x)\right\} { c_1 }\left\{ \exists Q.\, \left( \vdash \{ Q \} c_2 \{ R, [\vec {S}] \}\right) \wedge Q, [\vec {S}]\right\}$ holds for any x of type T. Then, using (IH1), we can get:

$$\begin{aligned} \vdash \left\{ \exists x. \ P(x)\right\} { c_1 }\left\{ \exists Q. \ \left( \vdash \{ Q \} c_2 \{ R, [\vec {S}] \}\right) \wedge Q, [\vec {S}]\right\} . \end{aligned}$$

Now, if we can prove $\vdash \{ \exists Q. \ \left( \vdash \{ Q \} c_2 \{ R, [\vec {S}] \}\right) \wedge Q \} c_2 \{ R, [\vec {S}] \}$, then our conclusion will immediately follow according to hoare-seq. In fact, it is straightforward. By (IH2), we only need to prove that for any assertion Q,

$$\begin{aligned} \vdash \{ \left( \vdash \{ Q \} c_2 \{ R, [\vec {S}] \}\right) \wedge Q \} c_2 \{ R, [\vec {S}] \}. \end{aligned}$$

Suppose $T_0$ is the set of proofs of $\vdash \{ Q \} c_2 \{ R, [\vec {S}] \}$, then

$$\begin{aligned} \left( \vdash \{ Q \} c_2 \{ R, [\vec {S}] \}\right) \wedge Q \dashv \vdash \exists x: T_0. \ Q \end{aligned}$$

Thus, by hoare-consequence, we only need to prove $\vdash \{ \exists x: T_0. \ Q \} c_2 \{ R, [\vec {S}] \}$. By (IH2) again, we only need to prove: if $\vdash \{ Q \} c_2 \{ R, [\vec {S}] \}$ has a proof, then $\vdash \{ Q \} c_2 \{ R, [\vec {S}] \}$; this is tautology. Now we complete the induction step for sequential composition. $\square$

The above proof of the sequential composition branch in proving Theorem 7 is based on seq-inv through Lemma 6. In fact, the induction over the syntax tree of the program c has to consider all possible constructors of a command. Therefore, it is necessary to develop inversion rules and inversion lemmas like Lemma 6 for each constructor. Moreover, only careful design of primary rules for the deeply embedded Hoare logic can establish these inversion rules: for each program constructor, there should exist exactly one primary rule corresponding to it. Otherwise, the indeterminacy of the Hoare triple’s proof tree will obstruct the proof of inversion rules.

Proving Other Rules.

The proof of other extended rules in the deep embedding follows a common pattern. We first extract information from Hoare triples in premises using inversion rules and then use primary rules to combine these information to establish new triples. This is exactly the proof scheme presented in Fig. 4 in Sect. 2.3 when we prove nocontinue using inversion rules. The proof for other rules is similar to this one and is omitted here.

This proof technique using inversion rules can also be applied to shallowly embedded logics, if these inversion rules are true. However, we would like to explore proofs without assuming the correctness of inversion rules in the following sections. Even though they are true for our toy language and shallow embeddings for their logics, they may not be true in reality when some other features are added to the logic. In these cases, a proof to circumvent inversion rules would be helpful.

Application in VST-A.

VST-A [49] is an annotation verifier built above VST. Its soundness proof not only utilizes inversion rules but also the proof pattern used in this section.

VST-A accepts programs with assertion annotations provided by the programmer. The annotations specify what the programmer believes the program state will satisfy at a given point during program execution and are used to guide the verification of the whole program. VST-A splits the program into paths connecting these assertions and the pre-/post-conditions and generates proof goals (Hoare triples) of these paths. These paths are much simpler than the whole program, so that the verifier can automate most of their proofs, and the prover can prove the remaining one with reasonable effort. Eventually, VST-A’s soundness will guarantee the correctness of the whole program given the Hoare triples of all these paths. VST-A’s soundness proof is formalized as the following proposition.

Proposition 1

(VST-A Soundness) For any P, Q, C, where C is the annotated program, if $\textrm{AllHyps}(P, Q, \textrm{paths}(C))$ is true, then $\{ P \} C\Downarrow \{ Q \}$ is true.

Here $\text {AllHyps}(P, Q, \text {paths}(C))$ means triples of all paths in C generated by VST-A is provable, and $\{ P \} C\Downarrow \{ Q \}$ means the Hoare triple holds with $C\Downarrow$ removing annotations from C. VST-A uses induction over C’s syntax tree to prove the soundness. For example, in the sequential composition case, the authors of VST-A need to find an intermediate assertion R and prove:

$$\begin{aligned} \begin{array}{ll} \text {if}&{} \text {AllHyps}(P, R, \text {paths}(C_1)) \Rightarrow \{ P \} C_1\Downarrow \{ R \} \\ \text {and}&{} \text {AllHyps}(R, Q, \text {paths}(C_2)) \Rightarrow \{ R \} C_2\Downarrow \{ Q \} \\ \text {then}&{} \text {AllHyps}(P, Q, \text {paths}(C_1\,;C_2)) \Rightarrow \{ P \} C_1\,;C_2\Downarrow \{ Q \} \end{array} \end{aligned}$$

To prove this, it suffices to show that $\text {AllHyps}(P, Q, \text {paths}(C_1\,;C_2))$ ensures $\text {AllHyps}(P, R, \text {paths}(C_1))$ and $\text {AllHyps}(R, Q, \text {paths}(C_2))$, i.e., they need to split Hoare triples for paths in $C_1\,;C_2$ to paths in $C_1$ and $C_2$. A non-trivial case is where a path includes commands from both $C_1$ and $C_2$, and they use the inversion lemma for hoare-seq to extract the intermediate assertion R and prove this condition using lemmas similar to Hypothesis 5 and Lemma 6.

5.2 Big-Step-Based Shallow Embedding

Proving Transformation Rules.

There is a general proof scheme for transformation rules under shallow embeddings. We can first prove some notion of “semantic similarity” of two programs in the goal and premise, then lift this “semantic similarity” to the logic level and derive a relation between Hoare triples, i.e., the extended rule. For example, the “semantic similarity” in the big-step-based embedding is exactly the refinement of the big-step reduction.

Definition 1

We say program $c_1$ refines $c_2$ ($c_1 \sqsubseteq c_2$) w.r.t. a big-step semantics iff.

• for any $s_1, s_2, \text {ek}$, if $(c_1, s_1) \Downarrow (\text {ek}, s_2)$, then $(c_2, s_1) \Downarrow (\text {ek}, s_2)$;

• and for any s, if $(c_1, s) \Uparrow$, then $(c_2, s) \Uparrow$.

Lemma 8 lifts the big-step refinement to the implication between Hoare triples using the big-step embedding.

Lemma 8

For any $c_1, c_2$, if $c_2 \sqsubseteq c_1$, then for any $P, Q, \vec {R}$, $\vDash _b \{ P \} c_1 \{ Q, [\vec {R}] \}$ implies $\vDash _b \{ P \} c_2 \{ Q, [\vec {R}] \}$.

Proof

The proof of the theorem is straightforward. Assume the pre-state is $s_1$, which satisfies P.

• We use contradiction to prove $c_2$ has no error. If it can cause error, $(c_2, s_1) \Uparrow$, then according to $c_2 \sqsubseteq c_1$, we can also construct an error in $c_1$’s execution, $(c_1, s_1) \Uparrow$, which contradicts with $\vDash _b \{ P \} c_1 \{ Q, [\vec {R}] \}$.

• For any ending configuration $(\text {ek}, s_2)$ which $c_2$ can reach, we construct $(c_1, s_1) \Downarrow (\text {ek}, s_2)$ from $(c_2, s_1) \Downarrow (\text {ek}, s_2)$ according to $c_2 \sqsubseteq c_1$. By $\vDash _b \{ P \} c_1 \{ Q, [\vec {R}] \}$, we can show $(\text {ek}, s_2)$ satisfies the post-condition and thus prove $\vDash _b \{ P \} c_2 \{ Q, [\vec {R}] \}$

$\square$

With Lemma 8, proofs for transformation rules if-seq and loop-nocontinue become apparent with the following two refinements.

$$\begin{aligned} \begin{aligned} (\texttt{if}~b~\texttt{then}~c_1~\texttt{else}~c_2) \,;c_3&\sqsubseteq \texttt{if}~b~\texttt{then}~c_1 \,;c_3~\texttt{else}~c_2 \,;c_3\\ \texttt{for}(;;c_2)~c_1&\sqsubseteq \texttt{for}(;;\texttt{skip})~c_1 \,;c_2 \end{aligned} \end{aligned}$$

Their proofs are straightforward. For example, we can split the big-step reduction

$$\begin{aligned} ((\texttt{if}~b~\texttt{then}~c_1~\texttt{else}~c_2) \,;c_3, s_1) \Downarrow (\epsilon , s_2) \end{aligned}$$

into the following proposition, which essentially encodes the reduction segments of two execution paths.

$$\begin{aligned} \begin{aligned} (\text {eval}(b, s_1)&= \texttt {true}\wedge (c_1, s_1)\Downarrow (\epsilon , s_3) \wedge (c_3, s_3) \Downarrow (\epsilon , s_2)) \\&\vee (\text {eval}(b, s_1) = \texttt {false}\wedge (c_2, s_1)\Downarrow (\epsilon , s_3) \wedge (c_3, s_3) \Downarrow (\epsilon , s_2)) \end{aligned} \end{aligned}$$

We can easily reconstruct a reduction of $\texttt{if}~b~\texttt{then}~c_1 \,;c_3~\texttt{else}~c_2 \,;c_3$ from $s_1$ to $(\epsilon , s_2)$ using this proposition. Other branches of if-seq’s refinement proof are similar, which can be easily enumerated by discussing four different reductions (three different exit control flows and one error case) of the program.

The proof for the loop-nocontinue is similar but involves induction over the loop iteration. The reduction of each iteration of $\texttt{for}(;;c_2)~c_1$ will be split into two reduction segments of $c_1$ and $c_2$, which can be easily combined into a reduction of $c_1 \,;c_2$ since both contain no $\texttt{continue}$. Since the reduction of $c_1 \,;c_2$ is exactly one iteration of $\texttt{for}(;;\texttt{skip})~c_1 \,;c_2$, combined with the induction hypothesis, it reproduces the reduction of $\texttt{for}(;;\texttt{skip})~c_1 \,;c_2$ and proves the refinement.

The above proof strategy is also taken by Software Foundations Vol. 6 [36] to prove a similar transformation rule in the big-step-based embedding. We will see later in the following sections that this approach can also be applied to the weakest-precondition-based embedding and the continuation-based embedding but can have quite different definitions of “semantic similarity”.

Proving Structural Rules.

We then show the proof for hoare-ex here and prove other rules in Appendix B. The conclusion for hoare-ex holds for another two shallow embeddings with similar proofs, which we omit in the following sections.

Theorem 9

For all c, P, and Q, if for all x, $\vDash _b \{ P(x) \} c \{ Q \}$, then $\vDash _b \{ \exists x.\, P(x) \} c \{ Q \}$.

Proof

For $\sigma \vDash \exists x.\, P(x)$, we know there exists some x such that $\sigma \vDash P(x)$. By the definition of $\vDash _b$, we can instantiate the premise with initial state $\sigma$ and the conclusion immediately follows by definition. $\square$

Proving Inversion Rules.

Proofs for the inversion rules of the big-step-based embedding is similar to those of the deep embedding. The big-step semantics is defined inductively w.r.t. the structure of a program, and we can reorganize the big-step relation underlying the triple just like what we do for the deeply embedded logic. As a result, we can easily prove inversion rules. We only demonstrate the proof for seq-inv here.

Theorem 10

For all $c_1, c_2, P, Q$, and R, if $\vDash _b \{ P \} c_1 \,;c_2 \{ Q, [\vec {R}] \}$, then there exists $Q'$ such that (1) $\vDash _b \{ P \} c_1 \{ Q', [\vec {R}] \}$ and (2) $\vDash _b \{ Q' \} c_2 \{ Q, [\vec {R}] \}$.

Proof

We use the weakest pre-condition of $c_2$ as $Q'$: $\sigma \vDash Q'$ iff. it never cause error, i.e., not $(c_2, \sigma ) \Uparrow$, and $\forall \sigma _1. (c_2, \sigma ) \Downarrow (\epsilon , \sigma _1)$ implies $\sigma _1 \vDash Q$.

(1) The safety of $c_1$ is guaranteed by the safety of $c_1 \,;c_2$ and we only need to show the state after $c_1$ terminates satisfies post-conditions. If $c_1$ exits normally, we combine the premise in the weakest pre. and have $(c_1 \,;c_2, \sigma ) \Downarrow (\epsilon , \sigma _1)$. By premise, we have $\sigma _1 \vDash Q$ and the intermediate state satisfies $Q'$ the conclusion holds by the definition of the strongest postcondition. If $c_1$ exits by control flow, say $(c_1, \sigma ) \Downarrow (\text {ek}, \sigma ')$, we have $(c_1 \,;c_2, \sigma ) \Downarrow (\text {ek}, \sigma ')$ and by premise, we prove the conclusion.

(2) The conclusion is obvious by the definition of weakest precondition $Q'$. $\square$

5.3 Weakest-Precondition-Based Shallow Embedding

Proving Transformation Rules: Refinement.

The principle for proving transformation rules in Sect. 5.2 still applies to small-step-based embeddings (both weakest-precondition-based embedding and continuation-based embedding). But we need to find an appropriate definition of “semantic similarity”. A first attempt is to use the refinement again, but under the small-step semantics.

Definition 2

We say program $c_1$ refines $c_2$ (denoted $c_1 \sqsubseteq _s c_2$) in small-step semantics iff. for any initial states $\sigma _1$ and terminal configuration $(c, \kappa , \sigma )$, the following is true.

$$\begin{aligned} ((c_1, \epsilon , \sigma _1) \rightarrow (c, \kappa , \sigma )) \Rightarrow ((c_2, \epsilon , \sigma _1) \rightarrow (c, \kappa , \sigma )) \end{aligned}$$

We also have Lemma 11 to lift the semantic refinement to the implication between weakest preconditions, which immediately implies the implication between Hoare triples.

Lemma 11

For any $c_1, c_2$, if $c_2 \sqsubseteq _s c_1$, then for any $\sigma , P, Q, \vec {R}$, $\sigma \vDash {\textrm{WP}}(c_1, \epsilon ) \{ Q, [\vec {R}] \}$ implies $\sigma \vDash {\textrm{WP}}(c_2, \epsilon ) \{ Q, [\vec {R}] \}$.

The proof for Lemma 11 is a simple and straightforward co-induction over $\sigma \vDash {\textrm{WP}}(c_2, \epsilon ) \{ Q, [\vec {R}] \}$.

To use the lemma, we need to again prove the following two refinements.

$$\begin{aligned} \begin{aligned} (\texttt{if}~b~\texttt{then}~c_1~\texttt{else}~c_2) \,;c_3&\sqsubseteq _s \texttt{if}~b~\texttt{then}~c_1 \,;c_3~\texttt{else}~c_2 \,;c_3\\ \texttt{for}(;;c_2)~c_1&\sqsubseteq _s \texttt{for}(;;\texttt{skip})~c_1 \,;c_2 \end{aligned} \end{aligned}$$

A possible proof idea is similar to the one in Sect. 5.2. We need to split the reduction of the left-hand-side program into several reduction segments along all execution paths. However, the notion of “reduction segments” is not for free in the small-step semantics as it is in the big-step semantics. For example, a direct inversion of the following reduction does not yield the reduction segments of $c_1$, $c_2$, and $c_3$.

$$\begin{aligned} ((\texttt{if}~b~\texttt{then}~c_1~\texttt{else}~c_2) \,;c_3, \epsilon , \sigma _1) \rightarrow ^* (c, \kappa , \sigma ) \end{aligned}$$

We need to manually prove that the sequential composition can be split into two reductions and the if-statement can be split into two reductions of two branches, i.e., there exists an ending configuration¹⁰$(c', \kappa ', \sigma ')$, such that

$$\begin{aligned} \begin{aligned}&\bigl (((b, \sigma _1) \rightarrow ^* (\texttt {true}, \sigma _1) \wedge (c_1, , \sigma _1) \rightarrow ^* (c', \kappa ', \sigma ')) \\&\quad \vee ((b, \sigma _1) \rightarrow ^* (\texttt {false}, \sigma _1) \wedge (c_2, , \sigma _1) \rightarrow ^* (c', \kappa ', \sigma '))\bigr ) \\&\quad \wedge (\kappa ' = \epsilon \Rightarrow (c', \kappa ' \cdot \text {KSeq}(c_3), \sigma ') \rightarrow ^* (c, \kappa , \sigma )) \end{aligned} \end{aligned}$$

The proof needs to be split into two separate lemmas for the sequential composition and the if-statement. Both are proved by induction over the reduction length. We can then reorganize these reduction segments to form a reduction of $\texttt{if}~b~\texttt{then}~c_1 \,;c_3~\texttt{else}~c_2 \,;c_3$.

While it is still a reasonable proof for the if-seq, the proof for the loop is overwhelming. In Sect. 5.2, we can directly induct over the number of loop iterations, since it is how the big-step semantic for loops is defined, we cannot do the same thing for loops in small-step semantics. A direct induction can only be performed to induct over the small-step reduction length! We need to have another inductive definition for reduction segments of a loop, which we present informally in definition 3.

Definition 3

For any ending configuration $(c, \kappa , s)$, the reduction from $(\texttt{for}(;;c_2)~c_1, \epsilon , s_1)$ to $(c, \kappa , s)$ can be decomposed into an $n-$iteration segment iff.

• $n = 0$, then $(c, \kappa , s)$ is reached by some $\texttt{break}$ from $(c_1 \,;c_2, \epsilon , s_1)$, or it is some stuck configuration reachable from $(c_1 \,;c_2, \epsilon , s_1)$, or $c_2$ eventually reduces to $\texttt{continue}$ and $(c, \kappa , s) = (\texttt{continue}, \text {KLoop}_{2}(c_1, c_2), s)$ gets stuck.

• $n = n' + 1$, then $(c_1 \,;c_2, \epsilon , s_1) \rightarrow ^* (\texttt{skip}, \epsilon , s')$, and $(\texttt{for}(;;c_2)~c_1, \epsilon , s') \rightarrow ^* (c, \kappa , s)$ can be decomposed into an $n'-$iteration segment.

Numerous details of handling control flows have been neglected in this definition. To prove such decomposition is possible, we use induction over the reduction length, and it involves many auxiliary definitions, which we do not demonstrate here. Instead, we present another more organized proof technique: simulation.

Proving Structural Rules: Simulation.

The idea is to directly induct over the length of reductions for the left-hand-side program in a refinement, and for each head reduction, we find zero or finitely many head reductions of the right-hand-side program that corresponds to it. This is exactly the idea of simulation, and we use the simulation relation (definition 4) to record this kind of correspondence, which is used for both the weakest-precondition-based embedding and the continuation-based embedding.

Definition 4

(Simulation) A relation $\sim$ between two programs is a simulation relation iff. for any $c_1, \kappa _1, c_2, \kappa _2$, if the source program $(c_1, \kappa _1)$ can be simulated by the target program $(c_2, \kappa _2)$, i.e. $(c_1, \kappa _1) \sim (c_2, \kappa _2)$, then

• Termination: if $(c_1, \kappa _1)$ has safely terminated, i.e., $\kappa _1$ is empty $\epsilon$ and $c_1$ is $\texttt{skip}$, $\texttt {break}\,\!$, or $\texttt {continue}$, then $(c_2, \kappa _2)$ can reduce to $(c_1, \kappa _1)$ in zero or finite steps without modifying the program state, (or it can stuck in an infinite loop without modifying the state)¹¹;

• Preservation: if for some program state $\sigma$, $(c_1, \kappa _1, \sigma )$ reduces to $(c_1', \kappa _1', \sigma ')$, then there exists $(c_2', \kappa _2')$ simulates $(c_1', \kappa _1')$ by $(c_1', \kappa _1') \sim (c_2', \kappa _2')$, and $(c_2, \kappa _2)$ can reduce to $(c_2', \kappa _2')$ in zero or finite steps with same state modifications, i.e., $(c_2, \kappa _2, \sigma ) \rightarrow _c^* (c_2', \kappa _2', \sigma ')$¹²

• Error: if for some state $\sigma$, $(c_1, \kappa _1, \sigma )$ does not belong to either of the above cases, i.e., it is stuck by an error, then $(c_2, \kappa _2, \sigma )$ will also reduce into some error in zero or finite steps.

Intuitively, in the termination case, when the source terminates, the target that simulates the source will also terminate in finite number of steps and these steps have no virtual effect on the program state. In the preservation case, any reduction step of the source can be simulated by zero or finite steps of the target, which mimic the source’s modifications to the program state, and program pairs they reduce to preserve the simulation relation. In the error case, when the source causes an error, the target will also raise an error along a certain execution trace.

One may expect that the simulation directly implies the refinement, but the simulation definition here is more general than the refinement because it does not require two programs to reduce to the same error. However, we can directly use the simulation as the notion of “semantic similarity” for embeddings using small-step semantics. We can use a simulation lemma (Lemma 12 and Lemma 16) to lift simulations to the logic level. The simulation lemma here (Lemma 12) lifts the simulation between two programs to the implication between their weakest preconditions.

Lemma 12

(Weakest Pre. Simulation) If there is a simulation relation $\sim$ and $(c_1, \kappa _1)$ simulates $(c_2, \kappa _2)$, i.e., $(c_2, \kappa _2) \sim (c_1, \kappa _1)$, then for all $\sigma , c_1, c_2, \kappa _1, \kappa _2, Q$, and $\vec {R}$, $\sigma \vDash \textsf {WP}\, (c_1, \kappa _1) \{ Q, [\vec {R}] \}$ implies $\sigma \vDash \textsf {WP}\, (c_2, \kappa _2) \{ Q, [\vec {R}] \}$.

Proof

We prove the lemma by induction over the reduction of $(c_2, \kappa _2, \sigma )$.

• If $(c_2, \kappa _2)$ has terminated, the simulation implies $(c_1, \kappa _1)$ will terminate with the same exit kind and we prove the conclusion by reflexivity.

• If $(c_2, \kappa _2)$ has an error, the simulation implies $(c_1, \kappa _1)$ will also have an error, which contradicts the safety guarantee (the program never causes an error) in its weakest precondition.

• If $(c_2, \kappa _2)$ further reduces, the simulation relation guides us on how to reduce $(c_1, \kappa _1)$ while preserving the simulation. We then unfold the weakest pre.’s definition and forward the execution accordingly and prove the lemma by the induction hypothesis.

$\square$

To prove if-seq and loop-nocontinue, we only need to construct two simulations $\sim _1$ and $\sim _2$ with the following properties respectively.

$$\begin{aligned} \begin{array}{c} ((\texttt{if}~b~\texttt{then}~c_1~\texttt{else}~c_2) \,;c_3, \epsilon ) \sim _1 (\texttt{if}~b~\texttt{then}~c_1 \,;c_3~\texttt{else}~c_2 \,;c_3, \epsilon )\\ (\texttt{for}(;;c_2)~c_1, \epsilon ) \sim _2 (\texttt{for}(;;\texttt{skip})~c_1 \,;c_2, \epsilon ) \end{array} \end{aligned}$$

For example, we can define the simulation for loop-nocontinue as the smallest relation with the following properties for any $c_1, c_2$ containing no $\texttt{continue}$.

$$\begin{aligned}&(\forall c,\kappa . (c, \kappa ) \sim _2 (c, \kappa )) \qquad \qquad \qquad \qquad \qquad \wedge \\&\left( \forall \kappa . \left( \begin{aligned}&(\texttt{for}(;;c_2)~c_1, \kappa ) \sim _2 (\texttt{for}(;;\texttt{skip})~c_1\,;c_2, \kappa ) \\ \wedge&\bigl ((c_1 \,;\texttt{continue}, \text {KLoop}_{1}(c_1, c_2) \cdot \kappa ) \sim _2 (c_1, c_2 \cdot \texttt{continue}\cdot \text {KLoop}_{1}(c_1 \,;c_2, \texttt{skip}) \cdot \kappa )\bigr ) \\ \wedge&\left( \begin{aligned}&\forall c_0, \kappa _0. (c_0, \kappa _0) \text { has no continue} \Rightarrow \\&(c_0, \kappa _0 \cdot \texttt{continue}\cdot \text {KLoop}_{1}(c_1, c_2) \cdot \kappa ) \sim _2 \\&\quad (c_0, \kappa _0 \cdot c_2 \cdot \texttt{continue}\cdot \text {KLoop}_{1}(c_1 \,;c_2, \texttt{skip}) \cdot \kappa ) \end{aligned} \right) \\ \wedge&\left( (\texttt{continue}, \text {KLoop}_{1}(c_1, c_2) \cdot \kappa ) \sim _2 (c_2, \texttt{continue}\cdot \text {KLoop}_{1}(c_1 \,;c_2, \texttt{skip}) \cdot \kappa ) \right) \\ \wedge&\left( \begin{aligned}&\forall c_0, \kappa _0. (c_0, \kappa _0) \text { has no continue} \Rightarrow \\&(c_0, \kappa _0 \cdot \text {KLoop}_{2}(c_1, c_2) \cdot \kappa ) \sim _2 (c_0, \kappa _0 \cdot \texttt{continue}\cdot \text {KLoop}_{1}(c_1 \,;c_2, \texttt{skip}) \cdot \kappa ) \end{aligned} \right) \\ \wedge&\left( (\texttt{skip}, \text {KLoop}_{2}(c_1, c_2) \cdot \kappa ) \sim _2 (\texttt{skip}, \text {KLoop}_{2}(c_1 \,;c_2, \texttt{skip}) \cdot \kappa ) \right) \\ \wedge&\left( (\texttt{break}, \text {KLoop}_{2}(c_1, c_2) \cdot \kappa ) \sim _2 (\texttt{break}, \text {KLoop}_{2}(c_1 \,;c_2, \texttt{skip}) \cdot \kappa ) \right) \end{aligned}\right) \right) \end{aligned}$$

This seemingly daunting definition is simply a conjunction of all possible intermediate configurations of two programs that need to be related together. Similarly, one can also prove the relation $\sim _2$ to be a simulation. We simply prove that in each conjunction branch, after one small-step reduction of the left-hand-side program, we can make zero or finite steps in the right-hand-side program and arrive at another conjunction branch in this relation. For example, in the first branch,

$$\begin{aligned} (\texttt{for}(;;c_2)~c_1, \kappa ) \sim _2 (\texttt{for}(;;\texttt{skip})~c_1\,;c_2, \kappa ) \end{aligned}$$

after one step of $(\texttt{for}(;;c_2)~c_1, \kappa )$, we take three steps of $(\texttt{for}(;;\texttt{skip})~c_1\,;c_2, \kappa )$ and arrive at the second branch

$$\begin{aligned} (c_1 \,;\texttt{continue}, \text {KLoop}_{1}(c_1, c_2) \cdot \kappa ) \sim _2 (c_1, c_2 \cdot \texttt{continue}\cdot \text {KLoop}_{1}(c_1 \,;c_2, \texttt{skip}) \cdot \kappa ). \end{aligned}$$

This is just a simple proof that can be automated through small-step symbolic execution, while the complicated induction proofs are all hidden in the simulation lemma. Then, by Lemma 12, we prove loop-nocontinue.

In fact, the construction of these simulation relations $\sim _2$ can guide the proof using pure refinement. All conjunction branches will correspond to some intermediate proofs using definition 3. Strictly speaking, there is no obvious advantages using either approach, but we believe the simulation approach is more suitable for proving small-step properties by thinking in small-step semantics. It also helps proofs of other extended rules as we will see soon.

Proving Structural Rules.

We prove nocontinue by showing the correctness of Lemma 13.

Lemma 13

For all $\sigma , c, \kappa , Q, R_\text {brk}, R_\text {con}$, and $R_\text {con}'$, if $\sigma \vDash \textsf {WP}\, (c, \kappa ) \{ Q, [R_\text {brk}, R_\text {con}] \}$ and c and $\kappa$ contains no $\texttt{continue}$, then $\sigma \vDash \textsf {WP}\, (c, \kappa ) \{ Q, [R_\text {brk}, R_\text {con}'] \}$.

Proof

We first prove in Lemma 14 that command reduction preserves the no-continue property, which is obvious by discussing all constructors of the small-step semantics.

Lemma 14

For all $c, c', \kappa , \kappa ', \sigma$, and $\sigma '$, if c and $\kappa$ contains no $\texttt{continue}$ and $(c, \kappa , \sigma ) \rightarrow _c (c', \kappa ', \sigma ')$, then c and $\kappa$ contains no $\texttt{continue}$.

We then induct over the number of steps $(c, \kappa )$ takes to terminate.

• For the base case where $(c, \kappa )$ is a terminal, the conclusion is obvious.

• For the case where $(c, \kappa , \sigma )$ can step into $(c', \kappa ', \sigma ')$, we forward the execution of $(c, \kappa , \sigma )$ in both weakest preconditions and only need to prove

  $$\begin{aligned} \sigma ' \vDash \textsf {WP}\, (c', \kappa ') \{ Q, [R_\text {brk}, R_\text {con}] \} \text { implies } \sigma ' \vDash \textsf {WP}\, (c', \kappa ') \{ Q, [R_\text {brk}, R_\text {con}'] \} \end{aligned}$$

  which follows from the induction hypothesis and Lemma 14.

$\square$

Proving Inversion Rules

We prove seq-inv, a representative inversion rule, by Lemma 15, where the simulation lemma helps again.

Lemma 15

For all $c_1, c_2, Q$, and $\vec {R}$, there exists $Q'$ such that for all $\sigma$, (1) if $\sigma \vDash \textsf {WP}\, (c_1 \,;c_2, \epsilon ) \{ Q, [\vec {R}] \}$ then $\sigma \vDash \textsf {WP}\, (c_1, \epsilon ) \{ Q', [\vec {R}] \}$, and (2) if $\sigma \vDash Q'$ then $\sigma \vDash \textsf {WP}\, (c_2, \epsilon ) \{ Q, [\vec {R}] \}$.

Proof

To prove seq-inv, we need to find an intermediate assertion $Q'$, for which we use $\textsf {WP}\, (c_2, \epsilon ) \{ Q, [\vec {R}] \}$. This immediately gives us (2) and we can prove (1) following the scheme proposed in Fig. 11, where bind-inv is the inversion of bind rule. This is true because we know when $c_1$ exits by a break or a continue, we will skip $c_2 \cdot \epsilon$ and reach post-conditions in $\vec {R}$; when $c_1$ exits normally, we will step into $c_2 \cdot \epsilon$ and the weakest precondition for it should be satisfied. $\square$

Fig. 11

Proof scheme of seq-inv with weakest precondition

5.4 Continuation-Based Shallow Embedding

Proving Transformation Rules.

Similar to weakest-precondition-based embedding, we may use the simulation as the “semantic similarity” with the simulation lemma (Lemma 16) that lifts a simulation relation to relations between guard predicates.

Here, we use another definition of the simulation relation. We add the disjunction in parentheses in definition 4, which asserts that when the source terminates, the target will no longer change the program state and will either terminate in zero or finite steps, or stuck in an infinite loop. Because under the continuation-based embedding, we only require the simulation lemma to provide the derivation between the safety of two programs, i.e., they can proceed without error. The simulation does not need to simulate their terminations, which they may never reach. This is an important property which we use in proofs.

Lemma 16

(Guard Simulation) For all $c_1, c_2, \kappa _1, \kappa _2$, and P, if $\{ P \} (c_1, \kappa _1)$ and we have the simulation $(c_2, \kappa _2) \sim (c_1, \kappa _1)$, then $\{ P \} (c_2, \kappa _2)$.

Proof

The proof is similar to the one for Lemma 12 by induction over the reduction of $(c_2, \kappa _2)$. The only difference is the termination case, where we no longer require any information from $(c_1, \kappa _1)$ since the conclusion holds by definition.

With Lemma 16, we can easily prove if-seq and loop-nocontinue. The proof idea is similar to the one in Sect. 5.3 and we omit it here.

Proving Structural Rules

Lemma 17 is the key step for proving nocontinue in continuation-based embedding, where complex constructions of continuations are involved.

Lemma 17

For all $c, \kappa _0, P, Q, R_\text {brk}$, and $R_\text {con}$, we have $\{ Q \} (\texttt{skip}, \kappa _0)$ and $\{ R_\text {brk} \} (\texttt{break}, \kappa _0)$ imply $\{ P \} (c, \kappa _0)$, if (1) c has no $\texttt{continue}$; and (2) for all $\kappa$, $\{ Q \} (\texttt{skip}, \kappa )$ and $\{ R_\text {brk} \} (\texttt{break}, \kappa )$ and $\{ R_\text {con} \} (\texttt{continue}, \kappa )$ imply $\{ P \} (c, \kappa )$.

Proof

Here, we set $R_\text {con}'$ in nocontinue to $\bot$, which can derive any other $R_\text {con}'$ by hoare-consequence rule. As a result, we only know the execution of $\kappa _0$ is guarded by Q and $R_\text {brk}$ but not $R_\text {con}$. However, we can construct a new $\kappa$ from $\kappa _0$ such that the behaviors of two continuations are “similar” when entering by normal exit and break exit, but $\kappa$ “terminates” immediately when entering by continue exit to guarantee $\{ R_\text {con} \} (\texttt{continue}, \kappa )$. Also, since c has no $\texttt{continue}$, we know the behaviors of $(c, \kappa _0)$ and $(c, \kappa )$ are “similar” so that they can simulate.

For such construction to be viable, we first need Lemma 18 to enable conversion from continuations to commands, whose proof is trivial and omitted.

Lemma 18

For any continuation $\kappa$, we can construct a command $c_\kappa$, such that $(\texttt{skip}, \kappa ) \sim (c_\kappa , \epsilon )$, by chaining expressions corresponds to each level in $\kappa$ using sequencing commands and virtual loops¹³.

We then show the existence of such construction from $\kappa _0$ to $\kappa$.

We define program $\texttt {dead} \triangleq \texttt{for}(;;\texttt{skip})~\texttt{skip}$. It will always cause $c \,;\texttt {dead}$ stuck in an infinite loop after the execution of c and it is always safe to execute $\texttt {dead}$ from any program state.

We assume $\kappa _0$ takes the form of

$$\begin{aligned} \begin{array}{ccccc} \underbrace{K_A} &{} \cdot &{} \underbrace{\text {KLoop}_{i}(c_1, c_2)} &{} \cdot &{} \underbrace{K_C} \\ A &{} &{} B &{} &{} C \end{array} \end{aligned}$$

where B is the first (innermost) loop continuation in $\kappa _0$. The case where $\kappa _0$ contains no loop, i.e., B and C is empty $\epsilon$, is trivial and is not discussed here. The normal entry into it executes all ABC; the break entry into it executes C only; the continue entry into it executes BC. We use $c_{AB}$ to denote the command transformed from continuation AB by Lemma 18. Now, we construct¹⁴

$$\begin{aligned} \begin{array}{rccccc} \kappa \triangleq &{} \underbrace{c_{AB} \cdot \texttt{break}} &{} \cdot &{} \underbrace{\text {KLoop}_{1}(\texttt{skip}, \texttt {dead})} &{} \cdot &{} \underbrace{K_C} \\ &{} A' &{} &{} B' &{} &{} C' \end{array} \end{aligned}$$

The normal entry will execute $c_{AB}$ and then skip the loop in $B'$ to execute $K_C$, i.e., it will execute all continuations ABC in $\kappa _0$; the break entry will skip $A'$¹⁵ and is scoped by the loop in $B'$ and enter $K_C$ through normal entry, which is equivalent to first skipping loop in B then executing $K_C$; the continue entry will skip $A'$ and stuck in a dead loop in $B'$. As a result, $\{ Q \} (\texttt{skip}, \kappa _0)$ will imply $\{ Q \} (\texttt{skip}, \kappa )$, $\{ Q_\text {brk} \} (\texttt{break}, \kappa _0)$ will imply $\{ Q_\text {brk} \} (\texttt{continue}, \kappa )$, and $\{ Q_\text {con} \} (\texttt{continue}, \kappa )$ unconditionally holds because a dead loop always make progress.

By premise, we have $\{ P \} (c, \kappa )$. Notice that $(c, \kappa )$ simulates $(c, \kappa _0)$ because $\kappa$ simulates $\kappa _0$ when c exit normally or by break, but c can only exit in these ways instead of continue exit. By Lemma 16, we prove $\{ P \} (c, \kappa _0)$. $\square$

Proving Inversion Rules

Similar to the proof of nocontinue, the proof of seq-inv (Lemma 19) is also based on constructions of continuations.

Lemma 19

For all $c_1, c_2$ and P, if for all $\kappa$, $\{ Q \} (\texttt{skip}, \kappa )$ and $\{ R_\text {brk} \} (\texttt{break}, \kappa )$ and $\{ R_\text {con} \} (\texttt{continue}, \kappa )$ imply $\{ P \} (c_1 \,;c_2, \kappa )$, then there exists $Q'$ such that for all $\kappa _0$,

• (1) $\{ Q' \} (\texttt{skip}, \kappa _0)$ and $\{ R_\text {brk} \} (\texttt{break}, \kappa _0)$ and $\{ R_\text {con} \} (\texttt{continue}, \kappa _0)$ imply $\{ P \} (c_1, \kappa _0)$,

• (2) $\{ Q \} (\texttt{skip}, \kappa _0)$ and $\{ R_\text {brk} \} (\texttt{break}, \kappa _0)$ and $\{ R_\text {con} \} (\texttt{continue}, \kappa _0)$ imply $\{ P \} (c_2, \kappa _0)$.

Proof

We construct $Q'$ as the strongest post. of $c_1$: $\sigma \vDash Q'$ iff. $\exists \sigma _0.\, (c_1, \epsilon , \sigma _0) \rightarrow _c (\texttt{skip}, \epsilon , \sigma )$ and $\sigma _o \vDash P$.

(1) Similar to the proof of nocontinue, we need to construct a $\kappa$ from $\kappa _0$ to utilize the premise by satisfying $\{ Q \} (\texttt{skip}, \kappa )$. We take $\kappa \triangleq \texttt {dead} \cdot \kappa _0$. $\kappa$ simulates $\kappa _0$ through break and continue entry and we have $\{ R_\text {brk} \} (\texttt{break}, \kappa )$ and $\{ R_\text {con} \} (\texttt{continue}, \kappa )$ by Lemma 16. $\kappa$ always loops through the normal entry and we have $\{ Q \} (\texttt{skip}, \kappa )$. By premise, we have $\{ P \} (c_1 \,;c_2, \kappa )$. This guarantees $c_1$ can execute safely from P, and we only need to show that $\kappa _0$ can execute safely after $c_1$.

When $c_1$ exits through break and continue, $(c_1 \,;c_2) \cdot \kappa$ simulates $c_1 \cdot \kappa _0$ and we have $\{ P \} (c_1, \kappa _0)$; $\{ Q' \} (\texttt{skip}, \kappa _0)$ tells us when $c_1$ exits normally, we can keep executing $\kappa _0$ safely. Together, we have $\{ P \} (c_1, \kappa _0)$ in all cases.

(2) By specializing the premise with $\kappa _0$, we can reduce the proof goal to $\{ P \} (c_1 \,;c_2, \kappa _0)$ implies $\{ Q' \} (c_2, \kappa _0)$. This is obvious because $\{ P \} (c_1 \,;c_2, \kappa _0)$ shows the safety $c_2 \cdot \kappa _0$ after we exit $c_1$ normally, and $Q'$, program states after $c_1$’s normal exit, which apparently guards $c_2 \cdot \kappa _0$. $\square$

Summary

In summary, we have proved representatives (Fig. 10) of extended rules in three categories under four different embeddings.

• The deep embedding allows most of the proofs to be simple, but it has a relatively complicated proof for the hoare-ex rule.

• The big-step-based embedding has relatively simple proofs for all extended rules. There is also a general proof principle for transformation rules under all shallow embeddings: first prove a relationship between two programs’ semantics, then lift it to a relationship between two programs’ Hoare triple. However, as mentioned in Sect. 3.1 and Sect. 4.1, the difficulty to extend it with more complex semantic features like concurrency limits its applications.

• In the weakest-precondition-based embedding, proofs are of medium difficulty. We incorporate the general proof principle and the simulation relation to produce more organized proofs. The simulation relation is straightforward to construct and is used throughout all extended rule’s proof in this embedding, but it could be tedious to define when the program is complicated.

• In the continuation-based embedding, complexities for transformation rules’ proofs are still acceptable with the general proof principle, but is very difficult for other extended rules. We need complex constructions for new continuations to utilize information in the premise.

Using deep embedding appears to have more benefits with minimum limits on the logic’s application. Its extended rules’ proofs are mainly at the logic level, instead of the semantic level. Therefore, we do not need to worry about simulations and defining continuations in this embedding. The only problem is the hoare-ex rule, which we have proved in this section and the proof can be maintained when extending the language and logic, as long as there exists exactly one primary rule corresponds to it for each program constructor as mentioned in Sect. 5.1.

6 From Shallow Embedding to Deep Embedding

In Sect. 5, we have seen proofs for extended proof rules under different program logic embeddings. The proofs under shallow embeddings (except the big-step-based one) are relatively complicated for certain extended rules, e.g., if-seq and nocontinue. Proofs under both the weakest-precondition-based one and the continuation-based one involve the notion of simulation. Proofs under the continuation-based one even require complex constructions of continuations. Although it may be possible to formalize these complicated proofs in real verification tools, we propose an easier way to work around them by building a deeply embedded logic above the existing shallowly embedded logic and proving these extended rules under the deeply embedded one.

Fig. 12

The Framework for Building Deep Embedding from Shallow Embedding. (i) Proofs are represented by arrows labeled with numbers. (ii) Proofs of arrows with matching textures can be reused in place of the other. (iii) Symbol $\vdash$ represents the deeply embedded logic, while $\vDash$ represents the shallowly embedded logic. (iv) The proof $\textcircled {6}$ is easier than proof $\textcircled {3}$

Figure 12 presents our framework for building a deeply embedded logic by reusing most of the proofs from an existing shallowly embedded one. The existing shallow embedding contains the following:

• The definition of the shallow embedding $\vDash \{ P \} c \{ Q, \vec {R} \}$.

• A set of primary rules and their proofs $\textcircled {1}$ directly based on the definition.

• A set of derived rules and their proofs $\textcircled {2}$ built on primary rules.

• A set of extended rules and their proofs $\textcircled {3}$ directly based on the definition.

• User’s proof $\textcircled {4}$ of their programs using only¹⁶ rules of these three types.

The deeply embedded verification tool we want needs to provide the followings:

• The definition of the embedding, i.e., the set of primary rules for proving $\vdash \{ P \} c \{ Q, \vec {R} \}$.

• A set of derived rules and a set of extended rules along with their proofs $\textcircled {5}\textcircled {6}$ directly built on primary rules.

• User’s proof $\textcircled {7}$ of their own programs using rules of these three types.

• To guarantee the correctness of the deep embedding, a soundness theorem and its proof $\textcircled {8}$ is required.

We use the same sets of proof rules in the deep embedding as the shallow one. The primary rules, derived rules, and extended rules in the shallow embedding and the deep embedding have the same forms. In this way, many proofs in the shallow embedding side can be reused to assist the construction of the deep embedding as indicated in Fig. 12.

• Proof reuse (a). Since all proof rules in two embedding have same forms, users can upgrade their proofs in the shallow embedding $\textcircled {4}$ to those in the deep one $\textcircled {7}$ with only one change in proofs. They only need to replace occurrences of proof rules with their counterparts in the deep one. The new proof establishes the program correctness as deeply embedded Hoare triples.

• Proof reuse (b). As mentioned in Sect. 1, derived rules are directly derived from primary rules with trivial proofs. Since primary rules in two embeddings have same forms, derived rules’ proofs $\textcircled {2}$ and $\textcircled {5}$ are in the same situation as case (a) and we can reuse them.

• Proof reuse (c). The most important part in a deeply embedded logic is its soundness proof $\textcircled {8}$, which guarantees the logic’s correctness. However, we can construct the soundness proof for free by reusing existing primary rules’ proofs $\textcircled {1}$ in the shallow embedding. To prove the soundness, we start by induction over the proof tree and obtain subgoals that are identical to shallowly embedded primary rules, which are already proved.

  Moreover, given the soundness and user program correctness in the deep embedding, we can also derive program correctness in the shallow embedding $\textcircled {9}$, if it is of user’s desire. It is a trivial instantiation of the soundness theorem on deeply embedded Hoare triples of user programs, where both are generated by reusing proofs in the shallow embedding.

If the original shallowly embedded logic does prove some extended rules, we may also reuse them. However, as we have shown in Sect. 5, their proofs $\textcircled {3}$ in the shallow embedding are often complex constructions, while in the deep embedding, their proofs $\textcircled {6}$ are mostly simple inductions over the proof tree. In many cases, for extended rules not proved on the shallow embedding side, we can easily prove them on the lifted deep embedding side.

In conclusion, building deeply embedded verification tools from an existing shallowly embedded one mainly involves simple reuses of existing proofs and simplified proofs of extended rules. Existing user’s proofs can also be easily upgraded to the deeply embedded version.

7 Choices of Primary Rules in Deep Embedding

At the beginning of Sect. 5.1, we have fixed our deeply embedded logic with only primary rules from Fig. 2. In fact, we may choose deep embeddings with other admitted primary rules. For example, we may choose frame rule as a primary rule as discussed in Sect. 8.1.2. In this section, we want to discuss the choices of making extended rules as primary rules.

Choosing hoare-ex as a Primary Rule.

In Sect. 5, we notice that the proof of hoare-ex is simpler in shallow embeddings than its proof in the deep embedding. It seems a good choice to make it a primary rule and use the technique in Sect. 6 to lift its simple shallow embedding proof to the deep embedding’s soundness proof. However, we still prefer not to choose it as a primary proof rule in the deeply embedded logic and prove it as an extended rule. This is also the design choice in our deeply embedded VST. Adding hoare-ex as a primary rule causes problems.

Adding more primary rules to the proof system would invalidate the original proofs of other extended rules. In deep embedding, we mainly use induction over proof trees when proving extended rules, and now we need to discuss one more case in such induction where the Hoare triple is constructed by hoare-ex. Taking seq-inv as an example, the extra case is that $\vdash \{ P \} c_1;c_2 \{ Q, [\vec {R}] \}$ is constructed by hoare-ex, i.e., P must takes the form of $\exists x: T.P'(x)$. The induction hypothesis is that for any x of type T we can find an S such that $\vdash \{ P'(x) \} c_1 \{ S, [\vec {R}] \}$ and $\vdash \{ S \} c_2 \{ Q, [\vec {R}] \}$. We then need to use the axiom of choice (AC) to complete the proof: we need to find a function $S'$ from T to assertions, such that for any x of type T, $\vdash \{ P'(x) \} c_1 \{ S'(x), [\vec {R}] \}$ and $\vdash \{ S'(x) \} c_2 \{ Q, [\vec {R}] \}$. It is controversial whether we should accept AC when we prove meta-theorems. The original VST does not need AC. But to complete this proof in Coq, we actually need the computational version of AC (FunctionalChoice_on in Coq¹⁷). It allows us to construct the $S'$ in the above proof.

To prevent such problems when we want more extended rule, we treat hoare-ex as an extended rule and prove it as a meta-theorem.

Choosing Transformation Rules as Primary Rules.

Transformation rules cannot treated as primary rules either. Transformation rules and primary rules for the same primitive bring non-determinism to the proof tree of a program, which invalidates our previous proof of inversion rules.

For example, if we admit loop-nocontinue as a primary rule, then in the proof of loop-inv, we need to consider one more induction case: given $\vdash \{ P \} \texttt{for}(;;\texttt{skip})~c_1\,;c_2 \{ Q, [\vec {R}] \}$, we need to show that there exists $I_1$ and $I_2$ such that $\vdash \{ I_1 \} c_1 \{ I_2, [Q, I_2] \}$ and $\vdash \{ I_2 \} c_2 \{ I_1, [Q, \bot ] \}$ and $P \vdash I_1$. Different from the case in Sect. 5.2, the induction hypothesis cannot extract any information from the premise. The loop must take the form of $\texttt{for}(;;c_2)~c_1$ to apply the induction hypothesis. As a result, we fail to prove loop-inv.

Moreover, admitting transformation rules as primary rules acquires developers to give their soundness proof in some shallow embedding. As we have seen in Sect. 5, their proofs under weakest-precondition-based embedding and continuation-based embedding is not as simple as other primary rules’ proofs.

Choosing other Extended Rules as Primary Rules.

Inversion rules cannot be chosen as primary rules. Conclusions of primary rules must take the form of Hoare triples, while those of inversion rules are often propositions led by meta-language’s existential quantifier. We cannot define the provable relation for these propositions.

Other structural rules like loop-nocontinue are preferred not chosen as primary rules for the same reason as transformation rules. In Sect. 8.1 and Sect. 8.1.2, we introduce two more structural rules, the frame rule and the hypo-frame rule, which are preferred not chosen as primary rules as well.

As a result, our current choice of primary rules (compositional rules, the consequence rule, and singleton command rules) is the most suitable one for instantiating a deeply embedded verification tool.

8 Discussion: Extensions of Hoare Logic

In this section, we discus various extensions of the Hoare logic discussed in previous sections and their potential influence on the logic embedding. Specifically, we will first consider program logics with load and store to discuss some basics of separation logic embeddings. Then, we introduce rules related to procedure calls above it and further discuss embeddings for the logic with procedure calls. We will also discuss various features of the program logic and assertion language like total correctness, non-determinism, and impredicative assertions, along with the soundness proof technique mentioned in Sect. 3.3.

8.1 Embeddings of Separation Logic

When reasoning about memory operations, it is useful to extend the Hoare logic to a separation logic [37]. A separation logic adds a logic connective, “$*$”, separating conjunction, to the assertion language. The assertion $P * Q$ asserts two disjoint pieces of memory satisfying P and Q respectively. Typically, a separation logic adds proof rules for memory-related assignments (rules for load and store) and the frame rule to Hoare logic. Also, when a function call is involved in a programming language, separation logic allows verifiers to specify only the local effects of callee functions, while proving how the caller uses this function to modify the global memory.

Figure 13 extends our previous toy WhileCF language with the following memory operations.

• Allocation, $x = \textrm{new}(v)$, where x is a program variable that stores the location storing the value v.

• Simple load, $x = [y]$, where x and y are program variables, and this command loads the value from the location with address y into variable x.

• Simple store, $[x] = y$, where x and y are program variables, and this command stores the value of y into the location with address y.

Fig. 13

Additional Proof Rules for Separation Logics

In addition, we assume that there is no memory load in an expression. Every memory operation is performed as a load or store command. This is similar to the Clight program in CompCert [23] and the C program in VST-Floyd [9].

To verify these memory operations, Fig. 13 adds three standard primary rules, hoare-alloc, hoare-load and hoare-store, to our previous logic in Sect. 2. The frame rule is the main focus of this section.

8.1.1 Frame Rule and More Potential Shallow Embeddings

The frame rule allows prover to remove unused separating conjuncts (assertions in separation logics) of memory from both pre-/post-conditions and prove the specification with remaining memories. The derivability of the frame rule depends on whether the programming language satisfies a property named the “frame property”. Gotsman et al. [16] proved that if the operational semantics satisfies the frame property, then the frame rule is sound. The following hypotheses state the frame property via a big-step semantics and via a small-step semantics. We use $\sigma ' \oplus \sigma$ to represent the disjoint union of two pieces of memory, $\sigma '$ and $\sigma$.

Hypothesis 20

(Frame property for a big-step semantics) For any c, $\text {ek}$, $\sigma _1$, $\sigma '_2$, $\sigma$,

• if $(c, \sigma _1 \oplus \sigma ) \Uparrow$, then $(c, \sigma _1) \Uparrow$;

• if $(c, \sigma _1 \oplus \sigma ) \Downarrow (\text {ek}, \sigma '_2)$, then either $(c, \sigma _1) \Uparrow$ or $\sigma '_2 = \sigma _2 \oplus \sigma$ for some $\sigma _2$ and $(c, \sigma _1) \Downarrow (\text {ek}, \sigma _2)$.

Hypothesis 21

(Frame property for a small-step semantics) For any $c_1$, $c_2$, $\kappa _1$, $\kappa _2$, $\sigma _1$, $\sigma '_2$, $\sigma$,

• if $(c_1, \kappa _1, \sigma _1 \oplus \sigma ) \not \rightarrow _c$, then $(c_1, \kappa _1, \sigma _1) \not \rightarrow _c$;

• if $(c_1, \kappa _1, \sigma _1 \oplus \sigma ) \rightarrow _c (c_2, \kappa _2, \sigma '_2)$, then either $(c_1,\kappa _1, \sigma _1) \not \rightarrow _c$ or $\sigma '_2 = \sigma _2 \oplus \sigma$ for some $\sigma _2$ and $(c_1, \kappa _1, \sigma _1) \rightarrow _c (c_2, \kappa _2, \sigma _2)$.

These two properties are true for the WhileCF language extended with memory operations as well as for most of reasonable languages (including realistic languages like C). The above conclusion by Gotsman et al. [16] holds for $\vDash _b$, $\vDash _w$, and $\vDash _c$ (respectively stand for the validity definition under big-step-based embedding, weakest-precondition-based embedding, and continuation-based embedding). For example, Theorem 22 proves the frame rule in the big-step-based embedding.

Theorem 22

If the Hypothesis 20 is true, the frame rule holds for the big-step-based embedding defined in Sect. 4.1.

Proof

To prove $\vDash _\text {b}\{ P*F \} c \{ Q*F, [R_\text {brk}*F, R_\text {con}*F] \}$, we need to show that for any $\sigma \vDash P*F$ (1) $\lnot \,(c, \sigma )\Uparrow$, and (2) $\text {for all } \text {ek}, \sigma _2, \text {if }(c, \sigma ) \Downarrow (\text {ek}, \sigma _2)$, $\sigma _2$ satisfies corresponding post-conditions with the frame F according to $\text {ek}$.

According to the premise $\vDash _\text {b}\{ P \} c \{ Q, [R_\text {brk}, R_\text {con}] \}$, we know for any $\sigma _1 \vDash P$ (i) $\lnot \,(c, \sigma _1)\Uparrow$, and (ii) $\text {for all } \text {ek}, \sigma _2, \text {if }(c, \sigma _1) \Downarrow (\text {ek}, \sigma _2)$, $\sigma _2$ satisfies corresponding post-conditions without the frame F according to $\text {ek}$.

We can split $\sigma$, according to $\sigma \vDash P*F$, into $\sigma _1$ and $\sigma '$ satisfying

$$\begin{aligned} \sigma = \sigma _1 \oplus \sigma ' \quad \text {and}\quad \sigma _1 \vDash P \quad \text {and}\quad \sigma ' \vDash F. \end{aligned}$$

By (i), we know $\lnot \,(c, \sigma _1)\Uparrow$. Then, by Hypothesis 20, we have $\lnot \,(c, \sigma _1 \oplus \sigma ')\Uparrow$ because otherwise we have a contradiction and we prove (1).

To prove (2), by Hypothesis 20, for any $\text {ek}, \sigma _2$ with $(c, \sigma _1 \oplus \sigma ') \Downarrow (\text {ek}, \sigma _2)$, we know that

• either $(c, \sigma _1)\Uparrow$, which contradicts with the premise (i) and finishes the proof;

• or there exists $\sigma _2'$ with $\sigma _2 = \sigma _2' \oplus \sigma '$ and $(c, \sigma _1) \Downarrow (\text {ek}, \sigma _2')$. By (ii), we know $\sigma _2'$ satisfies corresponding post-conditions without the frame F according to $\text {ek}$ (i.e., $\sigma _2' \vDash Q$, $\sigma _2' \vDash R_\text {brk}$, or $\sigma _2' \vDash R_\text {con}$). Since $\sigma ' \Vdash F$, we know $\sigma _2 = \sigma _2' \oplus \sigma '$ satisfies corresponding post-conditions with the frame F according to $\text {ek}$ (i.e., $\sigma _2 \vDash Q*F$, $\sigma _2 \vDash R_\text {brk}*F$, or $\sigma _2 \vDash R_\text {con}*F$), which finishes the proof.

$\square$

Interestingly, a different style of shallow embeddings for separation logic [5] are widely used and the frame rule will hold intrinsically. The frame rule in this formalization is called the “baked-in frame rule” in some literatures. For any shallow embedding $\vDash _x$ among $\vDash _b$, $\vDash _w$, and $\vDash _c$, it defines the Hoare triple as

$$\begin{aligned} \vDash _{\text {sep}-x} \{ P \} c \{ Q, [R_\text {brk}, R_\text {con}] \} \ \text {iff. for any} \ F, \vDash _x \{ P*F \} c \{ Q*F, [R_\text {brk}* F, R_\text {con}* F] \}. \end{aligned}$$

Taking continuation-based shallow embedding for example, we can use another definition: $\vDash _{\text {sep}-c} \{ P \} c \{ Q, [R_\text {brk}, R_\text {con}] \}$ iff. for arbitrary continuation $\kappa$ and arbitrary frame F (also a separation logic assertion),

$$\begin{aligned} \text {if } \quad {\left\{ \begin{array}{ll} \quad \{ Q * F \} (\texttt{skip}, \kappa ) \\ \quad \{ Q_\text {brk}* F \} (\texttt{break}, \kappa ) \\ \quad \{ Q_\text {con}* F \} (\texttt{continue}, \kappa ) \end{array}\right. } \text {then } \quad \{ P * F \} (c, \kappa ). \end{aligned}$$

Above is also shallowly embedded VST’s definition of Hoare triples. Under such embedding, we can easily verify the frame rule without using the frame property of small-step operational semantics. The premise $\vDash _{\text {sep}-c}~\!\{ P \} c \{ Q, [R_\text {brk}, R_\text {con}] \}$ means that for arbitrary frame $F''$,

$$\begin{aligned}\vDash _{c} \{ P * F'' \} c \{ Q * F'', [R_\text {brk}* F'', R_\text {con}* F''] \}.\end{aligned}$$

Let $F'' = F * F'$. Then, we know $\vDash _{c} \{ (P * F) * F' \} c \{ (Q * F) * F', [(R_\text {brk}* F) * F', (R_\text {con}* F) * F'] \}$ for any F and $F'$, which exactly states the conclusion of frame:

$$\begin{aligned}\vDash _{\text {sep}-c} \{ P*F \} c \{ Q*F \}.\end{aligned}$$

Although such sep$-x$ embedding does not invalidate any primary rules or extended rules we have mentioned so far, it does make other proofs more complicated since we need to deals with this extra frame F. In comparison, both embedding styles are feasible. The original one makes proofs of other primary rules and extended rules relatively concise, while the sep$-x$ version makes the proof of the frame rule simple.

To summarize, in a shallow embedding, we can either directly prove the frame rule if Hypothesis 20 and Hypothesis 21 are true, or use the baked-in frame rule and reprove other rules using the new shallow embedding $\vDash _{\text {sep-x}}$. It does not matter whether the frame rule is a primary rule or an extended rule in a shallow embedding because both types of proof rules are just lemmas.

8.1.2 Frame Rule and Deep Embeddings

In deeply embedded program logics, we can either choose to make frame a primary rule or treat it as an extended rule.

The former option means that the separation logic’s soundness is based on the fact that frame preserves Hoare triple’s validity. This proof is very similar to the verification of frame in shallowly embedded logics. When developing a deeply embedded logic based on a shallowly embedded logic (see Sect. 6), one could directly reuse the proof of the frame rule in the shallow embedding. However, as discussed in previous sections, adding one more primary rule to the proof system may invalidate the other proofs because every case analysis and induction on proof trees will have one more branch to prove. In the case of frame rule, although extended rules we have discussed may not be invalidated by this extra case, such a choice would cause more uncertainty when we want to add more extended rules where this extra case may be unprovable. Keeping the proof system concise with only singleton rules, compositional rules, and the consequence rule will make the logic more extensible and thus we give up this design choice and prove the frame rule as an extended rule.

Nevertheless, we are not yet able to prove the frame rule with our previous deeply embedded program logic by simple induction over the proof tree of $\{ P \} c \{ Q \}$. Two base cases corresponding to hoare-load and hoare-store are not provable. We should allow these rules to be compatible with extra frames. For example, we use hoare-load-frame to replace hoare-load.

Then, we can easily prove the frame rule by induction over the proof tree. Similarly, for a language with more commands, we only need to guarantee proof rules for memory-related operations are compatible with extra frames.

To summarize, there are also two ways to formalize the frame rule in a deep embedding: either directly admit it as a primary rule, or bake the frame rule into singleton rules for memory operations. Both require admitting the frame rule as part of the primary rules but the second one makes maintaining existing extended rules’ proofs easier.

Procedure Calls and Hypothetical Frame Rule

In this section, we further extend the language and logic in Fig. 13 with procedure calls. Figure 14 adds the command for procedure calls, $\text {call} \, f()$, where procedure calls have no arguments or return value. Function arguments and return values are written to specific locations to be transferred between the caller and the callee.

Different from the logic in previous sections, the judgement of the logic in Fig. 14 takes the form of $\Delta \vdash \{ P \} c \{ Q, [\vec {R}] \}$. Here, $\Delta$ is a list of function hypotheses (a.k.a. the type-context in VST), containing a list of Hoare triples $\forall X_i.\,\{ P_i \} k_i \{ Q_i \}$ specifying the pre/post-condition of the procedure with identifier $k_i\in \text {FuncID}$ and logical variables $X_i$ the triple depends on. With the function hypothesis, hoare-call can determine the effect of procedure call by looking up the callee’s specification in $\Delta$.

Fig. 14

Additional Proof Rules for Separation Logics and Procedure Calls

Shallow embeddings of judgement involving procedure calls [34] are different from those in Sect. 4. Taking the denotational semantics based shallow embedding $\vDash _b$ for example, we introduce $\eta$ in (17), a mapping from procedures $k_i$ to their denotations, to avoid circularity.

$$\begin{aligned} \eta \in \text {FuncID} \rightarrow \text {state} \rightarrow \text {state} \rightarrow \text {exit\_kind} \rightarrow \text {Prop} \end{aligned}$$

(17)

We use $\eta (k_i)$ to lookup the procedure’s denotation and $c[\![ \eta ]\!]$ to represent the program after substituting call to procedures by their denotations. The shallow embedding $\Delta \vDash _b \{ P \} c \{ Q, [\vec {R}] \}$ is defined as: for any $(\forall X_i.\,\{ P_i[X_i] \} k_i \{ Q_i[X_i] \}) \in \Delta$, X, and $\eta$, $\vDash _b \{ P_i[X] \} \eta (k_i) \{ Q_i[X], [\bot , \bot ] \}$ is true, then $\vDash _b \{ P \} c[\![ \eta ]\!] \{ Q, [\vec {R}] \}$ is true.

In a logic combining separation logic and procedure call, we can generalize the frame rule to the hypo-frame rule in Fig. 14, which was first proposed by O’Hearn et. al [34]. This rule allows extending specifications of both the main program c and procedures $k_i$ it invokes by composing an extra frame R to their preconditions ($P_i[X_i]$ and P) and postconditions ($Q_i[X_i]$ and Q). It is easily derivable in a deeply embedded logic by induction over the proof tree with modified atomic rules in Sect. 8.1.1, and it is proved for the shallow embedding we introduced in this section by O’Hearn et. al [34].

Total Correctness

Throughout the paper, we have been discussing the Hoare logic for partial correctness, where we only require the program to produce no error and its output and ending state to satisfy certain assertions. Another correctness property that researchers care about a program is its total correctness. The total correctness adds one more condition on top of the partial correctness: the execution of the program terminates.

In a simple While language with only assignment, sequential composition, if-statement, and while-loop, the only way to cause non-termination is by executing an infinite loop. A famous approach to prove the termination of a loop is through loop variant [28]. For example, the while-total rule below uses an expression e as the loop-variant, which evaluates to some nature number. The value of e is guaranteed to decrease and when it reaches 0, the loop terminates. With the while-total rule and other standard proof rules for other language constructs (e.g., those in Fig. 2), a program logic can reason about the total correctness of the While language.

In a deeply embedded program logic, the inversion corresponding to the loop trivially holds. With only the loop proof rule being substituted, other extended rules remain unaffected.

In practice, users may care about how long a program terminates rather than just whether a program terminates. Charguéraud et. al [13] formalize a separation logic framework with time credits and use it to verify the amortized complexity of a union-find implementation. They provide a proof rule to unroll a recursive function application, and then use the meta-level induction to prove that the program terminates within a certain number of steps bounded by the time credit. However, this paper does not consider the meta-level induction nor the time credit, and what extended rules they will contribute to the logic is worth future investigation.

Non-determinism

Non-determinism is also a feature researchers want to support in Hoare logic, especially when verifying non-deterministic programs like concurrent programs. This paper’s result does not rely on a programming language being deterministic. One may freely introduce language primitives with demonic non-determinism and equip the deeply embedded program logic with corresponding primary rules. For these primary rules, one may prove their corresponding inversion rules, which then ensures the correctness of structural rules as we show in Sect. 5.1. Since only primary rules are added, transformation rules and other inversion rules are unaffected. Therefore, users can still embrace various extended rules with non-determinism involved.

Impredicative Assertions

Impredicative assertions are assertions whose universe quantifiers and existential quantifiers can quantify over assertions variables. These assertion languages usually also admits Hoare triples as assertions. This feature is required for our hoare-ex proof in Sect. 5.1 to work.

Whether impredicative assertions are available depends on the choice of meta logic. For a shallowly embedded assertion language in Coq, which we use for our proofs in Sect. 5, the formalization of these impredicative assertions is inherent because we can inject meta-logic propositions into assertions. Definitions (18) and (19) show how to define the interpretation (shallow embeddings) of these assertions.

$$\begin{aligned}{} & {} \sigma \vDash \exists P_0. S(P_0) \ \text {iff.} \ \text {there exists an assertion } P_0 \ \text {s.t.} \ \sigma \vDash S(P_0) \end{aligned}$$

(18)

$$\begin{aligned}{} & {} \sigma \vDash M \ \text {iff.} \ M \ \text {where} \ M \ \text {is a meta-logic proposition } (\text {e.g., }\vdash \{ P \} c \{ Q, [\vec {R}] \}) \end{aligned}$$

(19)

In general, impredicative quantification and does no interact well with complex inductive definitions. For example, impredicative quantification is absent in Agda. Coq poses constraints on the impredicatively quantified object, while Isabelle/HOL does not allow complex inductive definitions, making impredicativity available in both.

If we would use a deeply embedded assertion language, we need to construct the counterpart of the provable judgement and higher-order quantifiers in the assertion language. This is possible, and defining such a syntax system is not hard. The following definition could be a reasonable candidate:

$$\begin{aligned} \begin{array}{rcl} x &{} \in &{} \text {individual-variables-name} \\ A &{} \in &{} \text {assertion-variable-name} \\ t &{} {:}{:}{=} &{} \dots \ \mid \ x \\ P &{} {:}{:}{=} &{} t = t \ \mid \ A \ \mid \ \lnot P \ \mid \ P \wedge P \ \mid \ \exists x. \ P \ \mid \ \exists A. \ P \ \mid \ \ \vdash \{ P \} c \{ P, [P, P] \} \end{array}\end{aligned}$$

Technical problems may appear when defining assertions’ interpretation $\sigma \vDash P$. A simple syntactical substitution of the quantified variable for its value will result in a non-decreasing recursive interpretation function. For example, in the definition below, the assertion $P'$ that substitutes A in P may be larger than P, which makes the interpretation function non-terminating.

$$\begin{aligned} \sigma \vDash \exists A. P \iff \text {there exists assertion } P' \text { such that } \sigma \vDash P[A/P'] \end{aligned}$$

Instead of a direct syntactical substitution, we can use an interpretation assignment J to store interpretations of free variables.

$$\begin{aligned} J \in \text {assertion-variable-name} \rightarrow (\text {state} \rightarrow \text {Prop}) \end{aligned}$$

We use the judgement $\sigma , J \vDash P$ to help define the interpretation of an assertion. For higher-ordered existential quantifiers, we choose in the meta-level the interpretation d of the assertion variable A and assign d to A in the assignment J.

$$\begin{aligned} \sigma , J \vDash \exists A. P \iff \text {there exists } d \in \text {state} \rightarrow \text {Prop} \text { such that } \sigma , J[A/d] \vDash P \end{aligned}$$

The above interpretation makes the assertion P to be potentially an open term with the free variable A occurring in P. When we need to interpret a free assertion variable A on a state $\sigma$, we simply query J for A’s interpretation function and apply it to $\sigma$.

$$\begin{aligned} \sigma , J \vDash A \iff J[A](\sigma ) \end{aligned}$$

For these Hoare triple assertions, we can directly interpret them as their validities (shallow embeddings). Taking the big-step-based embedding for example, we simply copy and paste the definition in Sect. 4.1 and add assignment J when interpreting pre-/post-conditions.

$$\begin{aligned} \sigma , J \vDash (\vdash \{ P \} c \{ Q, [\vec {R}] \}) \iff \left( \begin{aligned}&\text {for all}\, \sigma _1,J \vDash P, \lnot \,(c, \sigma _1)\Uparrow \\&\text {and for all } \text {ek}, \sigma _2, \text {if }(c, \sigma _1) \Downarrow (\text {ek}, \sigma _2) \\&\quad \text {then }\text {ek}= \epsilon \text { implies } \sigma _2,J \vDash Q\\&\quad \text {and }\text {ek}= \text {brk}\text { implies } \sigma _2,J \vDash R_\text {brk}\\&\quad \text {and }\text {ek}= \text {con}\text { implies } \sigma _2,J \vDash R_\text {con}\end{aligned} \right) \end{aligned}$$

For a closed assertion P, we will interpret it on any assignment because it should not depend on it.

$$\begin{aligned} \sigma \vDash P \iff P \text { is closed and } \sigma , J \vDash P \text { is true for any } J \end{aligned}$$

Another approach is to inductively define the interpretation of assertions as a deep embedding, which is proposed by Ni and Shao [31]. For example, the interpretation rule for the existential quantifier is the following.

This definition only defines the interpretations for assertions that have finite derivation trees. Assertions with unbounded size (brought by higher-ordered quantifiers) will not have a finite derivation tree as well as an interpretation. This deeply embedded interpretation is then proved sound w.r.t. assertions true meaning. Interested readers may refer to their work [31] for more details.

The Soundness Proof Technique

Section 3.3 mentioned a soundness proof technique, where logic developers first prove the logic is sound w.r.t. some auxiliary validity definition , i.e.,

(20)

and then prove this auxiliary validity implies the real validity $\vDash S$, i.e.,

(21)

The auxiliary validity differs from the real validity $\vdash S$ in that usually has extra information about programs execution which makes proving (20) easier, while this information is not available when proving the real validity $\vDash S$ and therefore a lemma (21) that erases this information is required. For example, in Brookes’s soundness proof for the concurrent separation logic [7], it first uses thread local enabling $(s, h, A) \xrightarrow [\Gamma ]{\lambda } (s', h', A')$ to define the auxiliary validity $\Gamma \vdash \{ P \} c \{ Q \}$ for their Hoare triples, and then use this to derive the real validity $\vdash \{ P \} c \{ Q \}$ defined using the true semantics of the program running in a machine.

9 Deeply Embedded VST

Besides the program logic for our WhileCF toy language discussed so far, we also implement proposed theories in a real verification projects. We use the scheme in Sect. 6 to lift originally shallowly embedded VST [2] into a deeply embedded VST, where extended rules are easily proved.

We build deeply embedded VST¹⁸ based on the shallowly embedded VST, a verification framework for C programs. It is originally designed to use continuation-based shallow embedding to formalize the Hoare logic. Different from our toy language and toy logic, VST is designed to support named function invocations as well and we demonstrate the details VST adds to the triple.

VST uses the continuation-based shallow embedding with small-step semantics defined as $ge \vdash (c, \kappa , m) \rightarrow (c', \kappa ', m')$. Different from our small-step semantics in Sect. 4, it contains a global environment ge that stores external variables and functions. When an external call occurs, it will look up the function body from ge and add it to the continuation $\kappa$.

VST’s triples take the form of $\Delta \vDash \{ P \} c \{ Q, [\vec {R}] \}$, where $\Delta$ is the type-context containing function specifications. Its formalization in Coq is similar to the continuation-based shallow embedding ($\vDash _{\text {sep}-c}$) discussed in this paper. Specifically, the triple means: if every function obey specifications in $\Delta$, then for all continuations $\kappa$ and all separation logic frames F,

$$\begin{aligned} \text {if } {\left\{ \begin{array}{ll} \{ Q * F \} (\texttt{skip}, \kappa )\\ \text {and }\{ R_\text {brk}* F \} (\texttt {break}\,, \kappa )\\ \text {and }\{ R_\text {con}* F \} (\texttt{continue}, \kappa )\\ \text {and }\{ R_\text {ret}* F \} (\texttt {return}\,, \kappa ) \end{array}\right. }, \text { then } \{ P * F \} (c, \kappa ). \end{aligned}$$

A function f obeys specification $\{ P \} f \{ Q \}$ in $\Delta$ iff. its function body c has $\Delta \vDash \{ P \} c \{ Q \}$. VST uses step-indexing to resolve the circularity in the definition.

The shallowly embedded VST does not provide extended rules like seq-inv and nocontinue, which we prove in Sect. 5.4 and find their proof construction challenging. We then seek to formalize a deeply embedded Hoare logic. As proposed in Sect. 6, we first define the provable predicate for Hoare triple by primary proof rules (atomic rules, compositional rules, and the consequence rule) and then directly use the validity definition and soundness proofs in the original shallowly embedded VST to establish the soundness of our deeply embedded VST. We then prove extended rules in the deep embedding by induction over the proof tree. As discussed in Sects. 6 and 8.1.2, we choose to treat hoare-ex and frame rule as extended rules and prove them along with other extended rules, although they were proved sound in the original shallowly embedded VST. Also, VST did support proof rules like hoare-load-frame and hoare-store-frame in its original development. Thus, those modifications discussed at the end of Sect. 8.1.2 are not even needed.

Table 3 Evaluation of deeply embedded VST

We demonstrate the evaluation of our deeply embedded VST in Table 3. It only takes very few lines of code to formalize primary rules and logic soundness by reusing original proofs from the shallow embedding. We are able to formalize extended rules in the deep embedding with reasonable lines of code, which was not available in the shallow embedding. Moreover, there is no need to modify user proofs and users can upgrade their projects depending on the shallowly embedded VST to our deeply embedded one for free.

10 Related Work

In Sect. 4, we have already introduced various verification projects using different Hoare logic embeddings. In this section, we review other work on program logic embeddings.

Cook’s [14] proof of relative completeness for Hoare logic gives another view of problems we have discussed in Sect. 5. We now assume the deeply embedded logic $\vdash S$ comes with its completeness proof w.r.t. the shallowly embedded logic $\vDash S$, instead of the incompleteness assumption in Sect. 5. With completeness, the proof of inversion rules under all shallow embeddings can be greatly simplified. Take seq-inv as an example, the completeness allows entailment from $\vDash \{ P \} c_1\,;c_2 \{ Q, [\vec {R}] \}$ to $\vdash \{ P \} c_1\,;c_2 \{ Q, [\vec {R}] \}$, and use the seq-inv under the deep embedding to get $\vdash \{ P \} c_1 \{ S, [\vec {R}] \}$ and $\vdash \{ S \} c_2 \{ Q, [\vec {R}] \}$. Lastly, by the soundness of the deeply embedded logic, we get $\vDash \{ P \} c_1 \{ S, [\vec {R}] \}$ and $\vDash \{ S \} c_2 \{ Q, [\vec {R}] \}$ and finish the proof. The completeness enables proofs of this style for inversion rules, which can be further utilized to simplify proofs of structural rules and transformation rules. Nevertheless, as we have mentioned in Sect. 5, the completeness proof is often missing for logics in real verification projects, and our complicated constructive proofs under the shallow embedding should be trivial when compared to the even more complex completeness proof.

Nipkow [43] compares shallowly and deeply embedded assertion languages in an early paper. He considers a combination of shallowly embedded programming languages, shallowly embedded assertion languages and shallowly embedded program logics. He also considers a combination of deeply embedded programming languages, deeply embedded assertion languages and executable symbolic execution functions. His focus is the comparison between these two settings, while we compare multiple logic embeddings with fixed language and assertion embeddings.

11 Conclusion

In this paper, we clarify the nomenclature of “deep embedding” and “shallow embedding” for formalizing programming languages, assertion languages, and program logics and explore one deep embedding and three different techniques to shallowly embed a program logic. We identify a set of extended rules that could benefit the verification work, and we point out critical proof steps to validate them under different embeddings. We find they are relatively easier to prove under the deeply embedded logic because we can use induction over the proof tree. To alleviate the proof burden of instantiating extended rules for existing verification tools using shallow embeddings, we propose a method to build deeply embedded program logics on existing shallowly embedded ones, where we only need to reuse proofs for primary rules under the shallow embedding to build the deep one.

We also extend our results from conventional Hoare logics to separation logics. We present the deeply embedded VST, where we reuse the original shallowly embedded VST’s proofs for soundness proofs of primary rules and prove extended rules under the deep embedding, which is much easier than the proofs in the original VST (e.g. if-seq, loop-nocontinue). With deeply embedded VST, we demonstrate the feasibility of our theory in a real verification project.

In conclusion, this paper shows that using different embedding to formalize a program logic brings different benefits, where the shallow embedding allows a more straightforward formalization and the deep embedding makes it easier to add extended proof rules. Our work also indicates the possibility of formalizing a deeply embedded logic based on a shallowly embedded logic by reusing its soundness proof. Moreover, for any shallowly embedded logic (even with different embedding techniques), we can build its corresponding deeply embedded logic by the same set of primary rules. This could be an efficient way to extend existing verification tools to support more powerful proof rules like our extended proof rules.

Appendices

Appendix A: Big-Step Semantics

Figure 15 and Fig. 16 list the complete big-step semantics for the toy language. We use $(c, \sigma ) \Downarrow (\text {ek}, \sigma ')$ to denote that the program c starts execution from state $\sigma$ will safely terminate in state $\sigma '$ with exit kind $\text {ek}$. We use $(c, \sigma ) \Uparrow$ to denote that the program c starts execution from state $\sigma$ will run into an error.

Fig. 15

Big-step semantics of the Toy Language (1)

Fig. 16

Big-step semantics of the Toy Language (2)

Appendix B: Proofs of Some Extended Rules in Big-Step Semantics

We give some proofs of extended rules that are not covered in Sect. 5.2. All extended rules are proved in our Coq formalization.

Theorem 23

(if-seq) Forall $P, Q, \vec {R}, c_1, c_2, c_3$, if

$$\begin{aligned} \vDash _b \{ P \} \texttt{if}~b~\texttt{then}~c_1;c_3~\texttt{else}~c_2 ;c_3 \{ Q, [\vec {R}] \},\end{aligned}$$

then

$$\begin{aligned} \vDash _b \{ P \} (\texttt{if}~b~\texttt{then}~c_1~\texttt{else}~c_2) ;c_3 \{ Q, [\vec {R}] \}.\end{aligned}$$

Proof

Consider the initial state to be $\sigma _1$ with $\sigma _1 \vDash P$.

If $\textrm{eval}(e, \sigma _1) = \text {true}$, then we know $c_1 ;c_3$ will not cause error, and therefore $c_1$ and $c_3$ will not cause error and $(\texttt{if}~b~\texttt{then}~c_1~\texttt{else}~c_2) ;c_3$ will not cause error. The same happens when $\textrm{eval}(e, \sigma _1) = \text {false}$, and we know $\texttt{if}~b~\texttt{then}~c_1;c_3~\texttt{else}~c_2 ;c_3$ will not cause error.

If $\textrm{eval}(e, \sigma _1) = \text {true}$ and $c_1$ terminates with normal exit, then we know forall $\sigma _3$ with

$$\begin{aligned} ((\texttt{if}~b~\texttt{then}~c_1~\texttt{else}~c_2) ;c_3, \sigma _1) \Downarrow (\text {ek}, \sigma _3) \end{aligned}$$

there exists $\sigma _2$ such that

$$\begin{aligned} (c_1, \sigma _1) \Downarrow (\epsilon , \sigma _2) \quad \quad (c_3, \sigma _2) \Downarrow (\text {ek}, \sigma _3) \end{aligned}$$

and we can construct by

and by the triple in the premise, we know $(\text {ek}, \sigma ) \vDash \{Q, [\vec {R}]\}$ and we prove the triple in the proof goal. If $\textrm{eval}(e, \sigma _1) = \text {true}$ and $c_1$ terminates with some control flow exit, then $\texttt{if}~b~\texttt{then}~c_1;c_3~\texttt{else}~c_2 ;c_3$ terminates with the same exit and state, and therefore we know the terminal state satisfies post-conditions. The same happens when $\textrm{eval}(e, \sigma _1) = \text {false}$, and we prove the triple to be valid.

Theorem 24

(nocontinue) Forall $P,Q,R_{\text {brk}},R_{\text {con}},R_{\text {con}}',c$, if c does not contain $\texttt{continue}$ and $\vDash _b \{ P \} c \{ Q, [R_{\text {brk}}, R_{\text {con}}] \},$ then $\vDash _b \{ P \} c \{ Q, [R_{\text {brk}}, R_{\text {con}}'] \}.$

Proof

Consider the initial state to be $\sigma _1$ with $\sigma _1 \vDash P$.

The triple in the premise guarantees c will not cause error and we only need to show any $(\text {ek}, \sigma _2)$ that $(c, \sigma _1)$ reduces to satisfies $[R_{\text {brk}}, R_{\text {con}}']$. In fact, we can prove by induction over $(c, \sigma _1) \Downarrow (\text {ek}, \sigma _2)$ that $\text {ek}$ is not $\text {con}$, i.e., it never exits with continue because c does not contain $\texttt{continue}$. Therefore, $(\text {ek}, \sigma _2)$ satisfies $[R_{\text {brk}}, \bot ]$ and obviously satisfies $[R_{\text {brk}}, R_{\text {con}}']$. $\square$

The proof idea of nocontinue in the big-step-based embedding is similar to that in the weakest-precondition-based embedding, but we do not need to do the simulation because there is no requirement after each step of reduction in the big-step-based one, and we only need to show certain properties of the final state it reduces to. They are very different from the proof in the continuation-based one because the interpretation of the post-condition’s satisfiability is different.