# Coma, an Intermediate Verification Language with Explicit Abstraction Barriers (extended version)

Andrei Paskevich, Paul Patault, Jean-Christophe Filliâtre

► To cite this version:

Andrei Paskevich, Paul Patault, Jean-Christophe Filliâtre. Coma, an Intermediate Verification Language with Explicit Abstraction Barriers (extended version). ESOP 2025 - 34th European Symposium on Programming, Viktor Vafeiadis, May 2025, Hamilton, Ontario, Canada. https://link.springer.com/book/10.1007/978-3-031-91118-7. hal-04839768v3

HAL Id: hal-04839768

https://hal.science/hal-04839768v3

Submitted on 13 Feb 2025

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>
# COMA, an Intermediate Verification Language with Explicit Abstraction Barriers (extended version)

Andrei Paskevich, Paul Patault, and Jean-Christophe Filliâtre*

Université Paris-Saclay, CNRS, ENS Paris-Saclay, Inria,
Laboratoire Méthodes Formelles, F-91405 Gif-sur-Yvette, France

**Abstract.** We introduce COMA, a formally defined intermediate verification language. Specification annotations in COMA take the form of assertions mixed with the executable program code. A special programming construct representing the abstraction barrier is used to separate, inside a subroutine, the “interface” part of the code, which is verified at every call site, from the “implementation” part, which is verified only once, at the definition site. In comparison with traditional contract-based specification, this offers us an additional degree of freedom, as we can provide separate specification (or none at all) for different execution paths. We define a verification condition generator for COMA and prove its correctness. For programs where specification is given in a traditional way, with abstraction barriers at the function entries and exits, our verification conditions are similar to the ones produced by a classical weakest-precondition calculus. For programs where abstraction barriers are placed in the middle of a function definition, the user-written specification is seamlessly completed with the verification conditions generated for the exposed part of the code. In addition, our procedure can factorize selected subgoals on the fly, which leads to more compact verification conditions. We illustrate the use of COMA on two non-trivial examples, which have been formalized and verified using our implementation: a second-order regular expression engine and a sorting algorithm written in unstructured assembly code.

## 1 Introduction

Consider a simple function, written in some ML dialect, which eliminates the root node from a binary tree, using an existing library function that merges two trees in one:

```hml
type tree = Node tree elt tree | Empty

let removeRoot (t: tree) : tree
  = match t with
    | Node l _ r → mergeTree l r
    | Empty → fail
```

If we want to use `removeRoot` in a formally verified program, we need to provide this code with a specification. In a traditional contract-based approach, this means writing a precondition and a postcondition, and here is how they would usually look:

<footnote>* This is an extended version of the paper accepted for presentation at the 34th European Symposium on Programming, ESOP 2025.</footnote>
```pascal
let removeRoot (t: tree) : tree
    requires { t ≠ Empty }
    ensures { match t with
               | Node l _ r → ∀e:elt. e ∈ result ↔ e ∈ l ∨ e ∈ r
               | Empty → false }
```

While this contract does its job, it is rather unpleasant. Not only does it take more space than the code it describes, it also basically repeats what is already written in the code. What is more, if we compute a verification condition (VC, for brevity) for the definition of `removeRoot`, it will take the form of one `match-with` formula implying another—or maybe two nested `match-with` formulas—and neither is easy to read and to prove.

Some programming languages, like Haskell and Agda, admit multiclause function definitions, and it is tempting to write our specification in this way, too:

```pascal
removeRoot (Node l _ r)
ensures { ∀e:elt. e ∈ result ↔ e ∈ l ∨ e ∈ r }
= mergeTree l r

removeRoot Empty = fail
```

This definition is much nicer. The postcondition in the first clause can refer to the results of the top-level pattern matching and does not need to do one itself. Furthermore, the second clause is self-explainable, so that we can omit the specification altogether.

However, from the verification point of view, something unusual is happening here. As we push the postcondition down the first branch of the pattern matching, we expose a part of the implementation (namely, the pattern matching itself) to the client code. Whenever `removeRoot` is called in our program, the VC for that call needs to perform the case analysis on the tree parameter in order to access the postcondition. Even more drastically, the second branch contains no specification at all, and so the caller's VC has to "inline" the entire second clause at the call site and prove that it is never reached.

What we did in this definition of `removeRoot`, is we moved the *abstraction barrier* inwards from the entry-exit boundary of a function, and even omitted it entirely on some of the execution paths. The question is, what are the rules of VC generation for programs with freely moving abstraction barriers? What if we do more in the exposed part of the code than just pattern matching or failure?

In this paper, we propose a formalism for computation and specification that intends to answer this question. We present a programming language called COMA that is small enough to comfortably study its properties, yet expressive enough to serve as a practical intermediate verification language for real-life applications. COMA programs are written in the continuation-passing style—the name COMA is short for Continuation Machine— which allows us to capture with just a few constructions the standard control structures: sequence, conditionals, loops, function calls, exception handling.

Specification annotations in COMA take the form of assertions mixed with executable code. Abstraction barriers are made explicit, as special tags that separate the “interface” part of a subroutine, which is verified at every call site, from the “implementation” part, which is verified only once, at the definition site.

Let us acquaint ourselves with this approach through a few examples. Here, we do not yet use the minimalistic syntax of COMA and stay with familiar ML-like constructs.
First, consider a simple wrapper for the Unix `exit` function, which expects an 8-bit unsigned integer and does not return to the caller. On the left, we show the traditional contract-based specification, and on the right, its rendition in the style of COMA:

```pascal
let wrapExit (r: int)          let wrapExit (r: int)
    requires { 0 ≤ r < 256 }     = assert { 0 ≤ r < 256 };
    = Unix.exit r                 (↑ Unix.exit r)
```

In COMA, the precondition moves into the function body as an assertion which precedes the actual implementation, and we hide the latter under the explicit abstraction barrier denoted `↑`. Since the assertion is put above the barrier, it must be verified at every call of `wrapExit`, whereas the rest of the body is invisible to the caller and produces no proof obligations at call sites. On the definition side, the instructions above the barrier are admitted without verification—which amounts here to simply assuming the asserted property—and the code under the barrier is verified under this assumption. Thus the VC for the definition of `wrapExit` is $\forall r. 0 \le r < 256 \rightarrow \varphi$, where $\varphi$ is the VC of the call `Unix.exit r`, whatever it might be.

The representation of postconditions in COMA is more involved, since we need to place them above the abstraction barrier (otherwise, the postcondition would be hidden from the caller), but the actual exit points are in the code below the barrier. We get around this complication by treating the postcondition of a function as the precondition of its continuation. Consider the following function, which, once again, is shown with a traditional specification on the left and rewritten in the COMA style on the right:

```pascal
let triple (x: int) : int      let triple (x: int) (ret: int → ⊥)
ensures { result = 3·x }         = let out (y: int) = assert { y = 3·x };
                                = x + x + x
                                              (↑ ret y)
                                in (↑ out (x + x + x))
```

On the COMA side, the continuation of `triple` is explicit, as a continuation parameter named `ret`. A locally defined function `out` provides a precondition for `ret`, similarly to `wrapExit` above. The definition of `out` is above the barrier in `triple`, and is verified whenever `triple` is called. This produces a VC of the form $\forall y. y = 3 \cdot x \rightarrow \varphi$, where $\varphi$ is the VC of `ret y`, that is, the verification condition of the rest of the computation, which follows the call of `triple` and is parametrized by the value returned. Note that this is exactly how a classical weakest-precondition calculus would handle calls of the `triple` function on the left-hand side. Conversely, when we verify the implementation of `triple`, the definition of `out` is admitted without proof, and we only need to verify the call of `out` under the barrier. This amounts to proving that $x + x + x$ is equal to $3 \cdot x$.

The flexibility and expressive power of explicit abstraction barriers become apparent when we implement the `removeRoot` function in the same fashion:

```pascal
let removeRoot (t: tree) (ret: tree → ⊥) = match t with
  | Node l _ r →
    let out (s: tree) = assert { ∀e:elt. e ∈ s ↔ e ∈ l ∨ e ∈ r };
                          (↑ ret s)
    in (↑ out (mergeTree l r))
  | Empty → fail
```
<figure><img src="image_2.png" /><figcaption>Fig. 1: Verification condition generation in COMA.</figcaption></figure>

Here, the postcondition and the abstraction barrier are put inside the first branch of the match operation, and the second branch contains no assertions or barriers. This means that the pattern matching and the inadmissibility of Empty are part of the interface of removeRoot, and will appear in the VC for every individual call of the function.

For non-recursive functions, the barriers can be omitted entirely. In this case, there are no proof obligations generated at the definition site, and the code of the function is effectively inlined during the computation of verification conditions at the call sites.

COMA is meant to serve as an internal language in program verification tools, rather than as a source language for human programmers. The conversion into continuation-passing style, the introduction of wrapper functions for postconditions, and the placement of barriers should be all performed automatically during translation from the front-end language. For example, when a source function is supplied with a contract, the barriers would protect the entire function body, as for *wrapExit* and *triple* above. A function without a contract would be translated as is, without barriers, and included transparently in the callers' verification conditions. For more complex specifications, like that of *removeRoot*, the front-end language should allow the programmer to express their intent through other means, such as multi-clause definitions, local contracts, etc.

Generation of verification conditions for COMA is a two-stage process, summarized in Fig. 1. A COMA program is first translated into a logical proposition, called a *recipe*. Recipes are formulas in a special higher-order logic, with an additional *neutralization operator* which is used for the parts of the code that are admitted without verification. An evaluation procedure, defined as an abstract machine *à la* Krivine, converts recipes into first-order formulas, suitable for automated proving. For COMA functions specified in a traditional manner, with the barrier at the entry-exit boundary, the resulting proof obligations are similar to those produced by a classical weakest-precondition calculus. However, we can also benefit from the intermediate higher-order form of our verification conditions, and factorize selected subformulas during evaluation. In this way, we curb the well-known exponential growth of classical weakest preconditions, and obtain proof obligations similar to the compact verification conditions of Flanagan and Saxe [7].

We introduce the logic of recipes and the evaluation operator ◦ in Sec. 3, together with a number of properties of this logic. The rules of verification condition generation, in the form of a VC operator $C_b^p$, are given afterwards in Sec. 4. The soundness of our VC generation method is stated in Theorem 3.

We implemented a VC generator for COMA programs and performed several case studies, two of which are presented here. While in this paper we focus on the pure fragment, our implementation also supports first-class alias-free mutable variables with effect inference and monadic translation into the pure core language. This implementation currently serves as a back-end for CREUSOT, a tool for deductive verification of Rust
programs [5]. Of particular interest for CREUSOT is COMA's ability to automatically infer the contracts of simple Rust closures (anonymous functions). This and other features are presented in more detail in Section 5.

To summarize, here are the main contributions of our work:

- a new intermediate verification language with higher-order functions and explicit abstraction barriers (Section 2);

- a rigorously defined and proved verification condition generator (Sections 3 and 4);

- a working implementation with numerous added features, including alias-free mutable variables, compact VC formulas via subgoal factorization, pre- and postcondition inference, etc. (Section 5);

- two non-trivial case studies: a second-order regular expression engine (Section 6) and a sorting algorithm written in x86-64 assembly code (Section 7).

## 2 Syntax and Semantics of COMA

The building blocks of COMA are *expressions*, which perform computations, and *terms*, which represent data. Expressions and terms are distinct syntactic entities: a term can be passed as an argument to an expression, but an expression cannot reduce to a term. An expression can be encapsulated in a named or anonymous *handler* (which is what we call subroutines), and either invoked directly or passed as a continuation argument to another expression.

Terms are composed of variables, constants, and pure total operations, provided that they have the same meaning in executable code and in specification. In theory, it would be possible to restrict the syntax of terms to variables and literal values, and delegate all computation to handlers, either predefined or introduced by the user. Still, for the sake of convenience, we admit in terms a handful of basic operations on unbounded integers, Booleans, and polymorphic finite sequences and binary trees. To handle type polymorphism, we treat types as a special kind of data: type expressions are considered to be terms of type Type, and we do not make a formal distinction between term and type variables. We denote variables with letters x, y, α, β (the latter two being reserved for types), and terms with s, t, τ, θ (again, the latter two being reserved for types). For specification, we use first-order formulas, denoted ϕ and ψ, which may contain variables and terms, but not handlers. By a slight abuse of notation, Boolean terms are accepted as atomic formulas.

Handlers accept term parameters (which includes type parameters) and handler parameters, also called continuation parameters or *outcomes*. The list of formal parameters of a handler is called its *type signature*. Since we adopt the continuation-passing style, handlers do not have return values. Handlers that have no parameters are said to have a *void type signature*, written with the symbol $\square$. We use letters $\pi$ and $\rho$ to denote type signatures, and letters $h, g, f$ for handler names.

We assume to have access to a number of predefined *primitive handlers*, which form the “standard library” of COMA. Here are the type signatures of five primitive handlers that we use throughout this paper:
<table><caption>Fig. 2: Handlers and expressions.</caption><tr><td>type signature:</td><td>π, ϱ ::= x : τ g : ϱ</td><td>parameter list</td></tr><tr><td>handler:</td><td>k, o ::= h<br>| π → d</td><td>handler symbol<br>anonymous handler</td></tr><tr><td>expression:</td><td>e, d ::= k s̄ ō<br>| e / h π = d<br>| {ϕ} e<br>| ↑ e<br>| ↓ e</td><td>handler call<br>handler definition<br>assertion<br>black-box barrier<br>white-box barrier</td></tr></table>

```
if: (c:bool) (then:□) (else:□)
unTree : (α:Type) (t:tree α) (onNode: (l:tree α) (v:α) (r:tree α)) (onEmpty:□)
get : (α:Type) (s:seq α) (i:int) (return: (v:α))
halt : □
fail : □
```

Handler `if` makes a choice between two continuations, represented by nullary outcomes then and `else`, depending on the condition c. Handler `unTree` inspects a binary tree `t`: if it is a node, then its datum and two subtrees are passed to the `onNode` continuation, otherwise `onEmpty` is called. Handler `get` retrieves the i-th element of sequence `s` and passes it to the continuation. This operation is allowed only when `i` is a valid index of `s`. Handler `halt` stops the computation. Finally, `fail` is an equivalent of `assert false`, it represents code that should never be reached in execution.

By allowing `Coma` computations to have multiple outcomes, we can represent as first-class entities what usually has to be hardwired into the core syntax of programming languages: conditionals and pattern matching. Handlers `halt` and `fail` are also noteworthy in this regard: as they do not accept continuation parameters, we know simply by looking at their signature that they cannot ever return control to the caller.

Type signatures are identified modulo parameter renaming. For example, the signature of `get` can be equivalently written as `(β:Type) (l:seq β) (k:int) (ret: (e:β))`. Each parameter binds the corresponding symbol in the types of subsequent parameters. This only matters for variables, as handler symbols cannot occur in type annotations.

The order of a type signature $\pi$ (and, by extension, of any handler with that signature) is defined recursively: if $\pi$ has no continuation parameters, it is of order zero; otherwise, the order of $\pi$ is one plus the highest order of its outcomes. The length and order of a type signature are invariant with respect to type instantiation: handlers can be polymorphic only in the data types.

Figure 2 presents the syntax of `Coma` expressions. An expression is an application of a named or anonymous handler to a list of arguments, on top of which we can put recursive handler definitions, logical assertions, and two barriers, denoted `↑` and `↓`, and called `black-box` and `white-box`, respectively. Handler definitions are placed to the right of the underlying expression; the slash symbol can be read as “where”. The barriers
<figure><img src="image_3.png" /><figcaption>Fig. 3: Typing rules for expressions.</figcaption></figure>

guide the generation of verification conditions, and do not affect execution. The black-box barrier is the abstraction barrier, which separates the exposed “interface” part of a handler definition from the hidden “implementation” part. The white-box barrier is an auxiliary construction that exposes the whole underlying expression. We use letters *e* and *d* to denote expressions, and letters *k* and *o* to denote handlers.

Type signatures serve as types for expressions, enumerating the expected arguments; in particular, a fully applied handler has type `□`. Typing contexts, denoted `Γ` and `Δ`, are sequences of type bindings of the form `x:τ` and `g:q`. A typing context is *well-formed* if no symbol is bound twice, and every variable type either is *Type* or has type *Type* with respect to the preceding bindings.

The typing rules for expressions are given in Fig. 3. In a judgement $\Gamma \vdash e : \pi$, the typing context is implicitly required to be well-formed. We consider as given the typing relations for terms and formulas, respectively denoted $\Gamma \vdash s : \tau$ and $\Gamma \vdash \varphi : \text{Prop}$; refer to Appendix A for the fragment used in this paper. Notice that bodies of handler definitions and anonymous handlers have to be fully applied. Thus, an anonymous handler $\pi \to d$ always has type $\pi$, modulo parameter renaming. As with type signatures, we identify expressions modulo renaming of bound symbols.

The initial typing context $\Gamma_{\text{prim}}$ binds the primitive handlers to their respective type signatures. An expression *e* is called a *program* when $\Gamma_{\text{prim}} \vdash e : \Box$.

We define a small-step operational semantics for COMA as a reduction relation $\to$. The reduction rules are shown in Fig. 4. We write $e // \Lambda$ to identify an expression under a series of nested handler definitions, where $\Lambda$ is a list of definitions, possibly empty. In other words, $e // h_1 \pi_1 = d_1, \dots, h_n \pi_n = d_n$ stands for $e / h_1 \pi_1 = d_1 / \dots / h_n \pi_n = d_n$.

The rule E-SYM expands handler definitions. We assume that no handler is defined in $\Lambda$ twice, as we can always rename bound handlers. The rules E-APP<sub>T</sub> and E-APP<sub>H</sub> perform $\beta$-reduction. The rule E-APP<sub>C</sub> turns an anonymous handler argument into a local handler definition. This is done in a capture-safe manner: we expect that the handler symbol *g* does not occur freely in *d* or in $\bar{o}$. The white-box barrier over *d* is needed to preserve the verification condition of the program, as we show later.
<figure><img src="image_4.png" /><figcaption>Fig. 4: Operational semantics.</figcaption></figure>

The rule E-PROP requires the asserted formula $\varphi$ to be valid before proceeding with the execution. The validity judgement $\vdash \varphi$ is made within the standard model for our data types: integers, Booleans, sequences and binary trees. Of course, the validity of an arbitrary proposition cannot be effectively verified in a practical implementation. However, our purpose here is different: we define the operational semantics of COMA in order to state and prove the correctness of our verification procedure—in particular, that a program with a valid verification condition cannot get stuck during its execution because of a failed assertion.

The rule E-VOID replaces a nullary anonymous handler by its body. The barriers are ignored during execution (rules E-BBOX and E-WBOX). Finally, the rule E-GC prunes the context by removing unreachable handler definitions. This rule commutes with the rest of the rules, making COMA non-deterministic, yet still strongly confluent.<fnref n="1" /> We can define the operational semantics of COMA without the E-GC rule; however, it helps keeping our definition context clean by removing local handler definitions once the parent handler finishes its computation.

We also postulate the evaluation rules for the primitive handlers. As for E-PROP, the application of these rules depends on validity of logical properties that express the pre- and postcondition of the primitives. For example, the Boolean condition of an `if` must be valid for the evaluation to progress along the first outcome (as mentioned in the beginning of the section, we admit Boolean terms as atomic formulas). In the rules for `unTree`, the function symbols `Node` and `Empty` are the constructors of the `tree` type. In

<footnote n="1">¹ Modulo semantic equality of answer terms during evaluation of primitive handlers; see below.</footnote>
<figure><img src="image_5.png" /><figcaption>Fig. 5: Russian Peasant Multiplication in COMA.</figcaption></figure>

the rule for `get`, we use the (total) slice operator on sequence $s_1$ to isolate the element at the position $s_2$, which must be a valid index in $s_1$. The answer terms in the rules for `unTree` and `get` can be any ground terms that validate the rule premises: for example, the expression `get int [42] 0 return //A` can reduce both to `return 42 //A` and `return 6*7 //A`. While we could introduce some form of normalization to avoid this syntactical divergence, there is no need for that, since all conditions in our evaluation rules are expressed in terms of semantic validity. Finally, `halt` and `fail` represent the final states of a computation and cannot be evaluated.

COMA is a type-safe language. Type preservation is easy to establish, either through a direct proof or by embedding in a more expressive framework like System F<sub>ω</sub> or CoC. As for the progress property, the blocking semantics of assertions limits it to programs with a valid verification condition; and so we defer this subject until Section 4.

We conclude with two examples. First, we rewrite `removeRoot` in proper COMA:

<figure><img src="image_6.png" /></figure>

Just like in Sec. 1, the implementation starts with a case analysis on the tree parameter `t`, using the primitive `unTree` handler. The two branches of the case analysis are represented, respectively, by an anonymous handler, which is called when `t` is a binary node, and the `fail` primitive, invoked when `t` is `Empty`. The anonymous handler makes a call of `mergeTree`, which we assume to be available and polymorphic akin to `unTree`. The result of `mergeTree` is passed to a wrapper handler `out` which asserts the postcondition of the first branch, before calling the continuation parameter of `removeRoot`.

In Fig. 5, we show the Russian Peasant Multiplication algorithm written in COMA. This code is specified in a more traditional manner: the entire implementation of the `product` handler is put behind the abstraction barrier. Left in the interface part are the starting assertion `{b ≥ 0}`, which naturally becomes the precondition of `product`, and the wrapper handler `break`, which plays the same role as `out` in `removeRoot`, and whose precondition `{c = a · b}` is the postcondition of `product`.
The implementation defines and calls a recursive handler named `loop`. This handler does not return to the caller: to do that, it would need to receive a continuation parameter and call it, like `removeRoot` and `product` do. Instead, `loop` escapes by calling `break` at the end of computation. In this respect, `loop` behaves indeed rather like a loop than a recursive function: its continuation is determined statically, by its lexical context, rather than dynamically by its caller. Consequently, there is no distinct postcondition associated to `loop`: in `COMA`, postconditions are preconditions of continuation parameters (attached via wrapper handlers like `out` and `break`), and `loop` has none thereof. And the precondition of `loop`, placed above the barrier, is just the loop invariant.

In practice, the majority of `COMA` programs would be generated by mechanical translation from existing languages like `OCaml` or `Rust`. Part of this translation would be a `CPS` transformation, required by our language. While in most cases, this transformation is not problematic, and allows us to reduce a large number of control structures to just two—definitions and calls—there are limits to what can be easily translated into `COMA`. Consider, for example, an `OCaml` exception that carries a closure:

```
exception E of (int → int)
```

In `COMA`, exception-raising functions are written as handlers that have multiple continuation parameters: one for the normal outcome, and one for each exception that might be raised in the handler code. However, if the closures passed with the exception `E` were themselves liable to raise `E`, we would not be able to give them a finite type in `COMA`. Incidentally, it is not a coincidence that higher-order exceptions can be used to realize fixed point computations without explicit recursion.

## 3 The Logic of Recipes

In their final form, verification conditions for `COMA` programs are first-order logical formulas, which we can handle with the usual methods of automated and interactive theorem proving. Their generation, however, goes through an intermediate stage, where a preliminary higher-order verification condition, called *recipe*, is constructed and then transformed, deterministically and in a finite number of steps, into the first-order form.

Recipes are formulas in a particular variety of higher-order logic, where bound predicate variables represent verification conditions of individual handlers and can only appear in a positive position. We denote recipes with letters $\Phi, \Psi, \Upsilon$. The syntax of recipes is given in Fig. 6. In recipes, handler symbols become predicate variables of the same name and arity as the original handler. The symbol $\emptyset$ is the verification condition of `fail`, a logical contradiction. The *neutralization operator*, denoted $\searrow$, suppresses proof obligations in the underlying recipe. Finally, notice that the antecedent in an implication is not a recipe, but a first-order formula, which cannot have occurrences of handler symbols. We write $\lambda\pi.\Phi$ and $\forall\pi.\Phi$ to denote a series of nested $\lambda$-abstractions or quantifications. By convention, $\lambda\Box.\Phi$ and $\forall\Box.\Phi$ are the same as $\Phi$.

Universal quantification over a predicate variable is defined recursively, as an instan-
tiation with a *joker recipe* $\mathbf{0}_{\pi}$. A joker recipe is the verification condition of a handler
of which nothing is known: on any input, the handler may fail or it may call any of its
outcomes with arbitrary arguments. On a void type signature, the joker $\mathbf{0}_{\square}$ is simply $\mathbf{0}$.
$$
\begin{align*}
\Phi, \Psi, \Upsilon &::= h \mid \Phi s \mid \lambda x : \tau . \Phi \mid \forall x : \tau . \Phi \mid \Phi \wedge \Psi \\
&\qquad \mid \mathbf{0} \mid \Phi \Psi \mid \lambda g : \varrho . \Phi \mid \varphi \rightarrow \Phi \mid \mathfrak{h} \Phi \\
\forall h : \pi . \Phi &\triangleq (\lambda h : \pi . \Phi) \mathbf{0}_{\pi} \\
\mathbf{0}_{\pi} &\triangleq \lambda \pi . \mathbf{0} \wedge \bigwedge_{(f : \mathbf{x} : \tau, \mathbf{g} : \varrho) \in \pi} \forall \mathbf{x} : \tau . \forall \mathbf{g} : \varrho . f \bar{x} \bar{g}
\end{align*}
$$

<caption>Fig. 6: Preliminary verification conditions (recipes).</caption>

$$
\begin{array}{l@{\qquad}l}
\overline{\Gamma \vdash \mathbf{0} : \square} & (\text{TC-FAIL}) \qquad \frac{\Gamma \vdash \Phi : \pi \qquad \Gamma \vdash \Psi : \pi}{\Gamma \vdash \Phi \wedge \Psi : \pi} \quad (\text{TC-CONJ}) \\
h : \pi \in \Gamma & (\text{TC-SYM}) \qquad \frac{\Gamma \vdash \varphi : \text{Prop}}{\Gamma \vdash \varphi \rightarrow \Phi : \square} \quad (\text{TC-IMPL}) \\
\frac{\Gamma \vdash \Phi : \pi}{\Gamma \vdash \mathfrak{h}\Phi : \pi} & (\text{TC-NEU}) \qquad \frac{\Gamma, x : \tau \vdash \Phi : \square}{\Gamma \vdash \forall x : \tau . \Phi : \square} \quad (\text{TC-ALLT}) \\
\frac{\Gamma \vdash \Phi : (x : \tau) \pi \qquad \Gamma \vdash s : \tau}{\Gamma \vdash \Phi s : \pi [x \mapsto s]} & (\text{TC-APPT}) \qquad \frac{\Gamma, x : \tau \vdash \Phi : \pi}{\Gamma \vdash \lambda x : \tau . \Phi : (x : \tau) \pi} \quad (\text{TC-PART}) \\
\frac{\Gamma \vdash \Phi : (g : \varrho) \pi \qquad \Gamma \vdash \Psi : \varrho}{\Gamma \vdash \Phi \Psi : \pi} & (\text{TC-APPC}) \qquad \frac{\Gamma, g : \varrho \vdash \Phi : \pi}{\Gamma \vdash \lambda g : \varrho . \Phi : (g : \varrho) \pi} \quad (\text{TC-PARC})
\end{array}
$$

<caption>Fig. 7: Typing rules for recipes.</caption>

A fully applied recipe is a logical proposition, which is why we disregard the result
type (that is, Prop) and use type signatures once again as types for predicate variables
and recipes. The typing rules are given in Fig. 7. The typing contexts are the same as for
COMA expressions, and, like before, are implicitly required to be well-formed. Unlike
implication and universal quantification, the conjunction connective applies to any two
recipes of the same type, and not only to fully applied recipes. We identify recipes
modulo renaming of bound symbols.

The semantics of recipes is given by means of a Krivine-style abstract machine [10]
that converts a fully applied recipe into a first-order formula, where all bound predicate
variables are eliminated. We have chosen this approach both for theoretical and practical
reasons. First, the properties of recipes are naturally proved using logical relations [15],
which are straightforward to express in this setting. Second, our implementation of a
verification condition generator for COMA is based on the same abstract machine. In the
rest of the section, we introduce this evaluator and establish some of its properties.

A *cell* is a triplet ⟨b, Σ, Φ⟩, where Φ is a recipe, Σ a *cell context*, binding every free handler symbol in Φ to a cell, and *b* a Boolean value. Such a cell can be converted into a recipe by replacing the free handler symbols in Φ with the corresponding converted cells from Σ. We assign the type signature of the resulting recipe to the initial cell. In what follows, we denote cells with letters *C* and *D*, and assume that all cells and recipes under consideration are well-typed.
<figure><img src="image_7.png" /><figcaption>Fig. 8: Recipe evaluation.</figcaption></figure>

We associate a specification recipe to each primitive handler:

$$ \Psi_{if} \triangleq \lambda c:bool.\lambda then:\square.\lambda else:\square. (c \to then) \wedge (\neg c \to else) $$

$$ \begin{align*} \Psi_{\text{unTree}} &\triangleq \lambda\alpha:\text{Type.}\lambda t:\text{tree } \alpha.\lambda\text{onNode:} (1:\text{tree } \alpha)(v:\alpha)(r:\text{tree } \alpha).\lambda\text{onEmpty:\square.} \\ & \quad (\forall 1:\text{tree } \alpha.\forall v:\alpha.\forall r:\text{tree } \alpha. t = \text{Node } l \lor v \to \text{onNode } l \lor r) \wedge \\ & \quad (t = \text{Empty} \to \text{onEmpty}) \\ \Psi_{\text{get}} &\triangleq \lambda\alpha:\text{Type.}\lambda s:\text{seq } \alpha.\lambda i:\text{int.}\lambda\text{return:} (v:\alpha). \\ & \quad 0 \le i < \text{length s} \wedge \forall v:\alpha.s[i..i+1] = [v] \to \text{return v} \end{align*} $$

$$ \begin{align*} \Psi_{halt} &\triangleq \mathfrak{h}0 & \Sigma_{\text{prim}} &\triangleq [\text{if} \mapsto (\perp, \emptyset, \Psi_{\text{if}}), \\ \Psi_{\text{fail}} &\triangleq \mathbf{0} & \text{unTree} &\mapsto (\perp, \emptyset, \Psi_{\text{unTree}}), \text{get} &\mapsto (\perp, \emptyset, \Psi_{\text{get}}), \\ & & \text{halt} &\mapsto (\perp, \emptyset, \Psi_{\text{halt}}), \text{fail} &\mapsto (\perp, \emptyset, \Psi_{\text{fail}})] \end{align*} $$

$$ \begin{align*} \Psi_{halt} &\triangleq \mathfrak{h}0 & \Sigma_{\text{prim}} &\triangleq [\text{if} \mapsto (\perp, \emptyset, \Psi_{\text{if}}), \\ \Psi_{\text{fail}} &\triangleq \mathbf{0} & \text{unTree} &\mapsto (\perp, \emptyset, \Psi_{\text{unTree}}), \text{get} &\mapsto (\perp, \emptyset, \Psi_{\text{get}}), \\ & & \text{halt} &\mapsto (\perp, \emptyset, \Psi_{\text{halt}}), \text{fail} &\mapsto (\perp, \emptyset, \Psi_{\text{fail}})] \end{align*} $$

The initial cell context $\Sigma_{\text{prim}}$ binds primitive handlers to their respective specifications.

The depth of a cell $C = \langle b, \Sigma, \Phi \rangle$ is zero if its cell context $\Sigma$ is empty; otherwise, it is one plus the maximum depth of the cells in $\Sigma$. The neutralization of $C$, denoted $\mathfrak{h}C$, is the cell $\langle \tau, \mathfrak{h}\Sigma, \Phi \rangle$, where $\mathfrak{h}\Sigma$ is obtained by neutralizing every cell in $\Sigma$. Obviously, neutralization does not affect the type or depth of a cell.

A stack is a mixed sequence of terms and cells. An empty stack is denoted $\varepsilon$. The neutralization of a stack $\ell$, denoted $\mathfrak{h}\ell$, is obtained by neutralizing every cell in $\ell$. We say that a stack is aligned with a cell, when the length of the stack and the types of its elements coincide with the cell's signature. In other words, an aligned stack contains appropriate arguments for the cell.

An $n$-ary relation $R$ on same-typed cells holds on stacks $\ell_1, \dots, \ell_n$ when they all have the same length and type signature, and for each position $i$, if $\ell_{1i}, \dots, \ell_{ni}$ are terms, then they are all identical, and if they are cells, then both $R(\ell_{1i}, \dots, \ell_{ni})$ and $R(\mathfrak{h}\ell_{1i}, \dots, \mathfrak{h}\ell_{ni})$ are true. Similarly, $R$ holds on cell contexts $\Sigma_1, \dots, \Sigma_n$ when they bind the same handler names, and for every bound $h$, both $R(\Sigma_1(h), \dots, \Sigma_n(h))$ and $R(\mathfrak{h}\Sigma_1(h), \dots, \mathfrak{h}\Sigma_n(h))$ are true. It is easy to see that $R(\Sigma_1, \dots, \Sigma_n)$ implies $R(\mathfrak{h}\Sigma_1, \dots, \mathfrak{h}\Sigma_n)$, as $\mathfrak{h}\mathfrak{h}C = \mathfrak{h}C$.

As a special case of the above, any property of cells is said to hold for a stack $\ell$ or a cell context $\Sigma$ whenever for every cell $C$ in $\ell$ or $\Sigma$, both $C$ and $\mathfrak{h}C$ have this property. Furthermore, if the property holds for a cell context $\Sigma$, then it also holds for $\mathfrak{h}\Sigma$.

The evaluation operator $\circ$, defined in Fig. 8, applies a cell to an aligned stack and produces a first-order logical formula. In the rule for $\forall x:\tau.\Phi$, we assume that $x$ does not occur in the cell context $\Sigma$, to avoid collisions.
**Theorem 1.** The evaluation operator ◦ is defined on all aligned cells and stacks.

*Proof.* We say that a cell $C$ is *normalizing* if for any aligned normalizing stack $\ell$, the evaluation $C \circ \ell$ is defined. This definition is well-founded, because every cell in $\ell$ is of lower order than $C$. We need to show that all cells (ergo, all stacks) are normalizing. In fact, it suffices to prove that every cell $\langle b, \Sigma, \Upsilon \rangle$ is normalizing, if its cell context $\Sigma$ is normalizing. Afterward, a simple induction over cell depth allows us to conclude.

We proceed by induction over the size of $\Upsilon$, counting only the subrecipes, so that term substitutions do not affect the size. Take an arbitrary aligned normalizing stack $\ell$.

Case $\Upsilon$ is $\mathbf{0}$. As $\mathbf{0}$ is $\Box$-typed, $\ell$ has to be empty, and $\langle b, \Sigma, \mathbf{0} \rangle \circ \varepsilon$ is defined.

Case $\Upsilon$ is $h$. Since every cell in $\Sigma$ is normalizing, the evaluation $\Sigma(h) \circ \ell$ is defined.

Case $\Upsilon$ is $\mathfrak{h}\Phi$. The context $\mathfrak{h}\Sigma$ is normalizing, and the induction hypothesis applies.

Case $\Upsilon$ is $\Phi\Psi$. Let $D$ be $\langle b, \Sigma, \Psi \rangle$. Since $\mathfrak{h}\Sigma$ is normalizing, both cells, $D$ and $\mathfrak{h}D$, are normalizing by the induction hypothesis. As the cell $\langle b, \Sigma, \Phi \rangle$ is also normalizing by the induction hypothesis, the evaluation $\langle b, \Sigma, \Phi \rangle \circ D$, $\ell$ is defined.

Case $\Upsilon$ is $\lambda h : \pi . \Phi$. Then the stack $\ell$ is of the form $D, \ell'$, where both $D$ and $\mathfrak{h}D$ are normalizing. Thus, $\Sigma \uplus [h \mapsto D]$ is normalizing and the induction hypothesis applies.

In every other case, we pick a rule for ◦ and apply the induction hypothesis. $\Box$

<figure><img src="image_8.png" /></figure>

A cell $C$ is said to be *neutral*, if for any aligned neutral stack $\ell$, the formula $C \circ \ell$ is valid. Just as above, this recursive definition is well-founded, because every cell in $\ell$ is of lower order than $C$.

**Lemma 1.** Any *neutralized* cell $\mathfrak{h}C$ is *neutral*.

*Proof.* We proceed in the same way as in Theorem 1, via an intermediate lemma stating that any cell of the form $\langle \tau, \Sigma, \Upsilon \rangle$ is neutral, if its cell context $\Sigma$ is neutral. $\Box$

<figure><img src="image_9.png" /></figure>

A cell $C_1$ *entails* $C_2$, denoted $C_1 \Rightarrow C_2$, when they have the same type and for any aligned stacks $\ell_1$ and $\ell_2$ such that $\ell_1 \Rightarrow \ell_2$, we have $C_1 \circ \ell_1 \Rightarrow C_2 \circ \ell_2$. Here and below, the symbol $\Rightarrow$ stands for logical consequence, and $\Leftrightarrow$ for logical equivalence, under the same standard model used for assertions. Cell $C_1$ is *equivalent* to $C_2$, denoted $C_1 \equiv C_2$, when $C_1 \Rightarrow C_2$ and $C_2 \Rightarrow C_1$.

**Lemma 2.** *Cell entailment is reflexive and transitive.*

*Proof.* We prove reflexivity as in Theorem 1 and Lemma 1, via an intermediate lemma stating that for any same-typed $C_1 = \langle b, \Sigma_1, \Upsilon \rangle$ and $C_2 = \langle b, \Sigma_2, \Upsilon \rangle$ where $\Sigma_1 \Rightarrow \Sigma_2$, we have $C_1 \Rightarrow C_2$. To establish transitivity, given $C_1 \Rightarrow C_2$ and $C_2 \Rightarrow C_3$, we consider aligned stacks $\ell_1$ and $\ell_2$ such that $\ell_1 \Rightarrow \ell_2$. Then we have $C_1 \circ \ell_1 \Rightarrow C_2 \circ \ell_2$ by definition, and $C_2 \circ \ell_2 \Rightarrow C_3 \circ \ell_2$, since $\ell_2 \Rightarrow \ell_2$. $\Box$

<figure><img src="image_10.png" /></figure>

**Lemma 3.** *Consider two cells of the same type, $C_1$ and $C_2$, such that for any aligned stack $\ell$, we have $C_1 \circ \ell \Rightarrow C_2 \circ \ell$. Then $C_1 \Rightarrow C_2$.*

*Proof.* Let $\ell_1$ and $\ell_2$ be aligned stacks such that $\ell_1 \Rightarrow \ell_2$. Then $C_1 \circ \ell_1 \Rightarrow C_1 \circ \ell_2$ by Lemma 2, and $C_1 \circ \ell_2 \Rightarrow C_2 \circ \ell_2$ by the lemma assumption. $\Box$

<figure><img src="image_11.png" /></figure>
Note that $C_1 \Rightarrow C_2$ does not imply $\mathfrak{h}C_1 \Rightarrow \mathfrak{h}C_2$. For example, the cell $\langle \perp, \emptyset, \lambda g : \square. g \rangle$ entails $\langle \perp, \emptyset, \lambda g : \square. g \rangle$, yet, when we apply their neutralizations to $\langle \perp, \emptyset, \mathbf{0} \rangle$, we obtain $\top$ and $\perp$, respectively. Thus, to establish $\ell_1 \Rightarrow \ell_2$, we must show pairwise entailment not only for the cells in the two stacks, but also for their neutralizations.

Given three cells $C_1 = \langle b_1, \Sigma_1, \Phi \rangle$, $C_2 = \langle b_2, \Sigma_2, \Phi \rangle$, and $C_3 = \langle b_3, \Sigma_3, \Phi \rangle$ that have the same type and the same recipe $\Phi$, we say that $C_1$ is the fusion of $C_2$ and $C_3$ when $b_1 = b_2 \wedge b_3$ and $\Sigma_1$ is the fusion of $\Sigma_2$ and $\Sigma_3$. Quite obviously, if $C_1$ is the fusion of $C_2$ and $C_3$, then $\mathfrak{h}C_1$ is the fusion of $\mathfrak{h}C_2$ and $\mathfrak{h}C_3$ (all three are actually the same). Furthermore, any cell $C$ is the fusion of itself and $\mathfrak{h}C$.

A cell $C_1$ is a *meet* of $C_2$ and $C_3$ if they all have the same type, the neutralized cells $\mathfrak{h}C_2$ and $\mathfrak{h}C_3$ are equivalent, and for any aligned stacks $\ell_1, \ell_2, \ell_3$ such that $\ell_1$ is a meet of $\ell_2$ and $\ell_3$, we have $C_1 \circ \ell_1 \Leftrightarrow C_2 \circ \ell_2 \wedge C_3 \circ \ell_3$.

**Lemma 4.** If $C_1$ is the fusion of $C_2$ and $C_3$, then $C_1$ is a meet of $C_2$ and $C_3$.

*Proof.* We proceed as in Theorem 1, via an intermediate lemma stating that for all same-typed $C_1 = \langle b_1, \Sigma_1, \Upsilon \rangle$, $C_2 = \langle b_2, \Sigma_2, \Upsilon \rangle$, and $C_3 = \langle b_3, \Sigma_3, \Upsilon \rangle$ where $b_1 = b_2 \wedge b_3$ and $\Sigma_1$ is a meet of $\Sigma_2$ and $\Sigma_3$, cell $C_1$ is a meet of $C_2$ and $C_3$. The equivalence of $\mathfrak{h}C_2$ and $\mathfrak{h}C_3$ directly follows from the intermediate lemma in the proof of Lemma 2. $\square$

**Corollary 1.** For any cell $C$ and aligned stack $\ell$, we have $C \circ \ell \Leftrightarrow \mathfrak{h}C \circ \ell \wedge C \circ \mathfrak{h}\ell$.

**Corollary 2.** Any cell $C$ entails $\mathfrak{h}C$.

**Lemma 5.** Consider cells $C_1, C_2, C_3$ of the same type, such that $\mathfrak{h}C_2 \equiv \mathfrak{h}C_3$ and for any aligned stack $\ell$, we have $C_1 \circ \ell \Leftrightarrow C_2 \circ \ell \wedge C_3 \circ \ell$. Then $C_1$ is a meet of $C_2$ and $C_3$.

*Proof.* Consider aligned stacks $\ell_1, \ell_2, \ell_3$ such that $\ell_1$ is a meet of $\ell_2$ and $\ell_3$.

$$C_1 \circ \ell_1 \Leftrightarrow C_1 \circ \ell_2 \wedge C_1 \circ \ell_3 \qquad (\text{Lemma 4})$$

$$\Leftrightarrow C_2 \circ \ell_2 \wedge C_3 \circ \ell_2 \wedge C_2 \circ \ell_3 \wedge C_3 \circ \ell_3 \qquad (\text{assumption})$$

$$\Leftrightarrow \mathfrak{h}C_2 \circ \ell_2 \wedge C_2 \circ \mathfrak{h}\ell_2 \wedge \mathfrak{h}C_3 \circ \ell_2 \wedge C_3 \circ \mathfrak{h}\ell_2 \wedge \mathfrak{h}C_2 \circ \ell_3 \wedge C_2 \circ \mathfrak{h}\ell_3 \wedge \mathfrak{h}C_3 \circ \ell_3 \wedge C_3 \circ \mathfrak{h}\ell_3 \qquad (\text{Corollary 1})$$

$$\Leftrightarrow \mathfrak{h}C_2 \circ \ell_2 \wedge C_2 \circ \mathfrak{h}\ell_2 \wedge \mathfrak{h}C_2 \circ \ell_2 \wedge C_3 \circ \mathfrak{h}\ell_3 \wedge \mathfrak{h}C_3 \circ \ell_3 \wedge C_2 \circ \mathfrak{h}\ell_2 \wedge \mathfrak{h}C_3 \circ \ell_3 \wedge C_3 \circ \mathfrak{h}\ell_3 \qquad (\mathfrak{h}C_2 \equiv \mathfrak{h}C_3, \mathfrak{h}\ell_2 \equiv \mathfrak{h}\ell_3)$$

$$\Leftrightarrow C_2 \circ \ell_2 \wedge C_3 \circ \ell_3 \qquad (\text{Corollary 1}) \qquad \square$$

This leads to a surprising distributivity property. Consider a cell $D = \langle b, \Sigma, \Phi \wedge \Psi \rangle$ and its conjuncts $D_1 = \langle b, \Sigma, \Phi \rangle$ and $D_2 = \langle b, \Sigma, \Psi \rangle$. If $\mathfrak{h}D_1$ is equivalent to $\mathfrak{h}D_2$, then, by Lemma 5, $D$ is a meet of $D_1$ and $D_2$, and $\mathfrak{h}D$ is a meet of $\mathfrak{h}D_1$ and $\mathfrak{h}D_2$. Then, for any appropriate cell $C$ and stack $\ell$, the formula $C \circ D, \ell$ is logically equivalent to the conjunction of $C \circ D_1, \ell$ and $C \circ D_2, \ell$. Informally speaking, we can split a recipe over any cell conjunction, no matter where it occurs inside the recipe, as long as the conjuncts have equivalent neutralizations.

**Theorem 2.** Consider a type signature $\pi$ and a cell $J = \langle \perp, \Sigma, \mathbf{0}_{\pi} \rangle$. For every cell $C$ of type $\pi$, we have $J \Rightarrow C$ and $\mathfrak{h}J \Rightarrow \mathfrak{h}C$.
The proof of Theorem 2 is given in Appendix B. This result justifies our use of joker recipes to represent universal quantification over predicate variables. Indeed, for any $\Phi : \square$ and $\Psi : \varrho$, and a type-compatible $\Sigma$, the cell $\langle \perp, \Sigma, \forall g : \varrho. \Phi \rangle$ entails $\langle \perp, \Sigma, (\lambda g : \varrho. \Phi) \Psi \rangle$, and the same holds for their neutralizations.

In the process of evaluation, we can factorize selected first-order monomorphic cells, that is, those that only have term parameters whose type is not Type.

**Lemma 6.** Consider a cell $C = \langle b, \Sigma, \lambda g : (\bar{x} : \tau) . \Phi \rangle$ and an aligned stack $D, \ell$, such that none of the types $\tau_i$ is Type. Let $D'$ be the cell $\langle \perp, \emptyset, \lambda \bar{x} : \tau . z_1 = x_1 \wedge \dots \wedge z_n = x_n \to 0 \rangle$ for some fresh variables $\bar{z}$. Then $C \circ D, \ell \Leftrightarrow C \circ \mathfrak{h}D, \ell \wedge \forall \bar{z} : \tau . (\mathfrak{h}C \circ D', \mathfrak{h}\ell) \lor (D \circ \bar{z})$.

The proof of Lemma 6 is given in Appendix C. This lemma provides us with an alternative evaluation rule for cell arguments which are eligible and useful to factorize. The latter is a matter of heuristic choice: in our current implementation, we select non-neutral cells that are used multiple times in the final VC and are derived from executable code instead of just a sequence of assertions.

The new rule splits the formula $C \circ D, \ell$ into two parts. The first part, $C \circ \mathfrak{h}D, \ell$, erases all subgoals stemming from $D$. In the second part, the formula $\mathfrak{h}C \circ D', \mathfrak{h}\ell$ erases all subgoals that are *not* stemming from $D$, and replaces every occurrence of $D$ with a “unification subgoal” $D'$, which captures a term substitution in the answer variables $\bar{z}$. These substitutions are transferred to the single instance of $D$ in the formula $D \circ \bar{z}$.

By rewriting the second part as an implication $\forall \bar{z} : \tau . \neg (\mathfrak{h}C \circ D', \mathfrak{h}\ell) \to (D \circ \bar{z})$, we can see the antecedent as the cumulated logical premise (or the strongest postcondition) of the context $C \circ []$, $\ell$ for the continuation in the hole. In the next section, we show how this rule allows us to produce more compact verification conditions.

# 4 Verification Condition Generation

Verification conditions for COMA expressions are computed by the operator $C_{\mathfrak{D}}^{\mathfrak{P}}$, where Boolean flags $\mathfrak{p}$ and $\mathfrak{d}$ establish the mode:

$C_{\perp}^{\top}$: caller verification condition, to verify individual calls of a defined handler.

$C_{\top}^{\perp}$: callee verification condition, to prove the correctness of a handler definition.

$C_{\top}^{\top}$: full verification condition, which merges the proof goals of the first two modes.

$C_{\perp}^{\top}$: null verification condition, which is always true on fully applied expressions.

The caller mode extracts the specification (or the contract) of a defined handler from its definition. It treats every assertion as a precondition to verify at call sites, and it stops at the black-box barrier which separates the “interface” part of the definition from the hidden “implementation” part. The callee mode, on the contrary, treats every assertion as a precondition to assume, and verifies the correctness of the implementation part, after the black-box barrier, under those assumptions. In the full mode, which is the starting verification mode for COMA expressions, we prove assertions both before and after a barrier. In the null mode, which is equivalent to stopping verification, no proof obligations are generated at all. A COMA program *e* is said to be *correct*, when its fully evaluated verification condition $\langle \perp, \Sigma_{\text{prim}}, C_{\top}^{\top}(e) \rangle \circ \varepsilon$ is valid.
<figure><img src="image_12.png" /><figcaption>Fig. 9: Verification condition generation.</figcaption></figure>

Figure 9 shows the rules of VC generation. The notation **let h π = Ψ in Φ** in the rule for handler definitions stands for $(\lambda h : \pi . \Phi) (\lambda \pi . \forall h : \pi . \Psi)$—notice the universal quantifier that covers the occurrences of *h* in *Ψ* and ensures that this symbol is bound in the resulting recipe, just as it is bound in the original COMA expression. In this rule, we assign the handler’s specification $\lambda \pi . \forall h : \pi . C_{\perp}^{\top}(d)$ to a predicate variable with the same name *h*. This recipe is verified every time *h* is called from the underlying expression *e* or recursively from the definition body *d*.

Informally, flag **p** determines whether we should generate proof obligations—prove
assertions, verify handler definitions, ensure the safety of handler calls—at the current
position in the expression. For example, in the rule for {$\varphi$} *e*, we only generate a subgoal
for $\varphi$ (expressed as a double negation $\neg\varphi \rightarrow \mathbf{0}$), when **p** is true. Similarly, in the rule
for handler definitions, we verify the correctness of the implementation only when **p** is
true; otherwise, the formula $C_{\perp}^{\top}(d)$ always reduces to $\top$. Finally, on handler invocation,
when **p** is false, the corresponding predicate variable is neutralized, which effectively
cancels all proof obligations in the handler’s specification, as **0** becomes evaluated as $\top$.

When we pass through a black-box barrier $\uparrow$, the second flag $\mathbf{d}$ takes the place of $\mathbf{p}$.
Thus, when we compute the specification of a handler by applying $C_{\perp}^{\top}$ to the handler's
body, we stop at the black-box barrier, where we switch to $C_{\perp}^{\top}$, which evaluates to $\top$.
On the other hand, when we verify the correctness of a handler definition using $C_{\top}^{\top}$, we
do not generate proof obligations for assertions and handler calls until we arrive at the
black-box barrier, where we pass into the full mode $C_{\top}^{\top}$ for the rest of the definition.

The white-box barrier $\downarrow$ replaces the second flag with $\mathbf{p}$. This preserves the current value of $\mathbf{p}$ for the rest of the expression, regardless of the subsequent barriers.

The rule for handler calls simply propagates the VC operator down to the individual
handlers without changing the mode. Similarly, the rule for anonymous handlers pushes
the VC operator in its current mode under the $\lambda$-prefix—however, we must, in addition,
verify the handler in the complementary mode, with both $\mathbf{p}$ and $\mathbf{d}$ negated. This secondary
verification condition is only concerned with the continuation parameters of the handler,
and not with its proper proof obligations, which is why we neutralize the corresponding
recipe. To see why both conditions are necessary, consider the following COMA code:

$$
\text{crash} / \text{crash} = ((f:\square) \rightarrow \uparrow f) \text{ fail}
$$

This program reduces to *fail*: we unfold *crash* (E-SYM), purge the now-unreachable
definition (E-Gc), substitute *fail* into *f* (E-AppH), and drop the barrier (E-BBox). Thus,
we should not be able to prove it correct. Let us look at the full verification condition:

$$
\begin{align*}
C_{\top}^{\top}(\text{crash} / \text{crash} = (f \to \uparrow f) \text{ fail})
&= \text{let crash} = C_{\perp}^{\top}((f \to \uparrow f) \text{ fail}) \text{ in } C_{\top}^{\top}(\text{crash}) \wedge C_{\top}^{\perp}((f \to \uparrow f) \text{ fail}) \\
&= \text{let crash} = C_{\perp}^{\top}(f \to \uparrow f) C_{\perp}^{\top}(\text{fail}) \text{ in crash} \wedge C_{\top}^{\perp}(f \to \uparrow f) C_{\top}^{\perp}(\text{fail}) \\
&= \text{let crash} = ((\lambda f. C_{\perp}^{\top}(\uparrow f)) \wedge \mathfrak{h}(\lambda f. C_{\perp}^{\perp}(\uparrow f))) \text{ fail in crash} \wedge C_{\perp}^{\perp}(f \to \uparrow f) (\mathfrak{h} \text{ fail}) \\
&= \text{let crash} = ((\lambda f. C_{\perp}^{\perp}(f)) \wedge \mathfrak{h}(\lambda f. C_{\perp}^{\top}(f))) \text{ fail in crash} \wedge C_{\top}^{\perp}(f \to \uparrow f) (\mathfrak{h} \text{ fail}) \\
&= \text{let crash} = ((\lambda f. \mathfrak{h}f) \wedge \mathfrak{h}(\lambda f. \mathfrak{h}f)) \text{ fail in crash} \wedge C_{\perp}^{\perp}(f \to \uparrow f) (\mathfrak{h} \text{ fail}) \\
&= \text{let crash} = ((\lambda f. \mathfrak{h}f) \wedge \mathfrak{h}(\lambda f. \mathfrak{h}f)) \text{ fail in crash} \wedge ((\lambda f. \mathfrak{h}) \wedge \mathfrak{h}(\lambda f. \mathfrak{h}f)) (\mathfrak{h} \text{ fail}) \\
&\approx (\lambda f. \mathfrak{h}f) \mathbf{0} \wedge (\mathfrak{h}\lambda f. \mathfrak{h}f) \mathbf{0} \wedge (\lambda f. \mathfrak{h}) (\mathfrak{h} \mathbf{0}) \wedge (\mathfrak{h}\lambda f. \mathfrak{h}f) (\mathfrak{h} \mathbf{0})
\end{align*}
$$

For the sake of readability, we perform several reductions directly on the recipe in the last step; it is easy to show that the resulting recipe leads to the same final VC formula. Out of the four conjuncts, only the second one evaluates to $\perp$, and the other three to $\top$. If the rule for anonymous handlers did not include the second condition $\mathfrak{h}\lambda\pi \cdot C_{\neg\mathfrak{h}}^{\neg\mathfrak{p}}(d)$, we would end up with only the first and the third conjunct, which both evaluate to $\top$.

Let us further illustrate the rules of VC generation on the example from Sec. 1:

$$
\begin{align*}
\texttt{triple} \ 14 \ ((a:\text{int}) \to \{a=42\} \ \texttt{halt}) \ / \ \texttt{triple} \ (x:\text{int}) \ (\texttt{ret} \ r) \\
= \ (\uparrow \ \texttt{out} \ (x+x+x)) \ / \ \texttt{out} \ (y:\text{int}) = \{y=3 \cdot x\} \ (\uparrow \ \texttt{ret} \ y)
\end{align*}
$$

The full verification condition of this expression has the form

$$
\begin{align*}
\texttt{let triple} \ (x:\text{int}) \ (\text{ret} \ (r:\text{int})) &= C_{\perp}^{\top}(e) \ \texttt{in} \\
\texttt{triple} \ 14 \ ((\lambda a.(a = 42 \to \text{halt}) \wedge (\top \to \neg(a = 42 \to \mathbf{0})) \wedge \\
&\qquad \mathfrak{h}(\lambda a.(a = 42 \to \mathfrak{h}\text{halt}) \wedge (\perp \to \neg(a = 42 \to \mathbf{0}))) \wedge \forall x. \forall \text{ret.} C_{\top}^{\perp}(e))
\end{align*}
$$

where *e* is the body of *triple*. We can safely drop the secondary verification condition for the anonymous handler in the continuation of *triple*. Indeed, it is produced in the null mode and will evaluate to a tautologically true proof obligation for any argument *a*.

The caller and callee verification conditions of *triple* are as follows:

$$
C_{\perp}^{\top}(e) = \text{let out } (y:\text{int}) = C_{\perp}^{\top}(d) \text{ in } \mathfrak{h} \text{out } (x+x+x) \wedge \forall y. C_{\perp}^{\top}(d)
$$

$$
C_{\perp}^{\perp}(e) = \text{let out } (y:\text{int}) = C_{\perp}^{\perp}(d) \text{ in out } (x+x+x) \wedge \forall y. C_{\perp}^{\perp}(d)
$$

where *d* is the body of *out*. And the three VCs of *out* are as follows:

$$
C_{\perp}^{\top}(d) = (y = 3 \cdot x \rightarrow \mathfrak{h} \text{ret } y) \wedge (\top \rightarrow \neg(y = 3 \cdot x) \rightarrow \mathbf{0}) \quad \approx y = 3 \cdot x
$$

$$
C_{\perp}^{\top}(d) = (y = 3 \cdot x \rightarrow \text{ret } y) \wedge (\perp \rightarrow \neg(y = 3 \cdot x) \rightarrow \mathbf{0}) \quad \approx y = 3 \cdot x \rightarrow \text{ret } y
$$

$$
C_{\perp}^{\top}(d) = (y = 3 \cdot x \rightarrow \mathfrak{h} \text{ret } y) \wedge (\perp \rightarrow \neg(y = 3 \cdot x) \rightarrow \mathbf{0}) \quad \approx \top
$$

On the right we show the first-order formulas to which these recipes evaluate. Notice that for any predicate *ret*, the recipe $\mathfrak{h} \text{ret } y$ evaluates to a tautology.

Now we can evaluate the verification conditions of triple. Since $\mathfrak{h} \text{out}$ evaluates to a tautology for any argument, the caller VC, $C_{\perp}^{\top}(e)$, evaluates to $\forall y. y = 3 \cdot x \rightarrow \text{ret } y$. And the callee VC, $C_{\perp}^{\perp}(e)$, evaluates to $x+x+x = 3 \cdot x$. After simplification, the full VC of the initial expression is $(\forall y. y = 3 \cdot 14 \rightarrow y = 42) \wedge (\forall x. x+x+x = 3 \cdot x)$.
Verification conditions produced by the $C_T^\perp$ operator are for partial correctness: they do not ensure the termination of COMA programs. Here is one possible way to verify total correctness. Let us say that a handler definition $f \bar{x} : \tau \overline{g} : \rho = d$ is equipped with a variant, if there exists an int-typed term $t[\bar{x}]$ such that every occurrence of $f$ in $d$ is in an expression of the form $\{t[\bar{s}] < t[\bar{x}] \wedge \theta \le t[\bar{x}]\} f \bar{s} \bar{o}$. Here we assume that variables are not bound twice, so that the variables $\bar{x}$ in the assertion refer to the formal parameters of $f$. The ordering relation in the assertion is well-founded, therefore, an infinite tower of recursive calls of $f$ is impossible. A practical implementation would, of course, accept other well-founded relations, such as structural decrease on binary trees, lexicographic orderings on tuples, etc. While the definition above does not allow us to use $f$ as a handler argument inside $d$, this is not a limitation, as we can always move such occurrences into a local wrapper handler definition.

Below we list the main results about our VC generation procedure. The proofs are given in Appendix D.

**Lemma 7.** For any COMA expression $e$, any cell of the form $\langle b, \Sigma, C_\perp^\perp(e) \rangle$ is neutral.

Consequently, any VC of the form $C_\perp^\perp(e)$, where $e$ is a fully applied expression, can be safely replaced with a tautological recipe such as $\vdash 0$.

**Lemma 8.** For any COMA expression $e$, any cell of the form $\langle b, \Sigma, C_\perp^p(e) \rangle$ is a meet of $\langle b, \Sigma, C_\perp^p(e) \rangle$ and $\langle b, \Sigma, C_\perp^\perp(e) \rangle$ for all $p$ and $\delta$.

The fact that $C_T^\perp(e)$ can be split into $C_\perp^\perp(e)$ and $C_T^\perp(e)$ is the basis of the correctness preservation theorem:

**Theorem 3 (Preservation of Correctness).** For any COMA programs $e$ and $e'$, if $e$ is correct and $e \to e'$, then $e'$ is correct.

**Theorem 4 (Progress).** For any correct COMA program $e$, either $e$ is halt, or $e \to e'$ for some program $e'$.

In conclusion, let us show some examples of verification conditions. For clarity, we omit type annotations, inline the specifications of primitive handlers, treat $0$ as $\perp$ in the callee mode, and remove trivial subgoals coming from $C_\perp^\perp(\cdot)$ or $\perp \to \Phi$. The caller VC of removeRoot on page 9, for a given tree $t$ and continuation return, is the recipe

$$ (\forall \text{lvr. } t = \text{Node l vr} \to \forall s. (\forall e. e \in s \leftrightarrow e \in l \lor e \in r) \to \text{return s}) \land \\ (t = \text{Empty} \to \mathbf{0}) $$

This recipe is the specification of removeRoot, instantiated and proved at each call site. The subrecipe $(\forall e. e \in s \leftrightarrow e \in l \lor e \in r) \to \text{return s}$ is the callee VC for the out handler. Notice that the assertion $\{\forall e:\text{int.} e \in s \leftrightarrow e \in l \lor e \in r\}$ does not generate a subgoal here: as it occurs before the black-box barrier, it is treated as an assumption in the callee mode.

Here is the callee VC for removeRoot, to be proved for all values of $t$:

$$ \forall \text{lvr. } t = \text{Node l vr} \to \text{mergeTree elt l r} (\lambda s. \forall e. e \in s \leftrightarrow e \in l \lor e \in r) $$
There is no subgoal generated for the second outcome of unTree, as it does not contain an abstraction barrier. The predicate argument of mergeTree is the caller VC of out; this time the assertion does generate a subgoal.

Here is the specification of the product handler in Fig. 5, for given integers a, b and a continuation return:

$$ (b \neq 0 \rightarrow 0) \land (\forall c. c = a \cdot b \rightarrow \text{return } c) $$

The callee VC for product, to be proved for all values of a and b, is as follows:

$$
\begin{align*}
b \geq 0 & \rightarrow \\
a \cdot b + 0 &= a \cdot b \land b \geq 0 \land \\
\forall pqr. p \cdot q + r &= a \cdot b \land q \geq 0 \rightarrow \\
(q > 0 & \rightarrow \\
(q \mod 2 = 1 & \rightarrow (p+p) \cdot (q \text{ div } 2) + r + p = a \cdot b \land q \text{ div } 2 \geq 0) \land \\
(q \mod 2 \neq 1 & \rightarrow (p+p) \cdot (q \text{ div } 2) + r = a \cdot b \land q \text{ div } 2 \geq 0) \land \\
(q \neq 0 & \rightarrow r = a \cdot b)
\end{align*}
$$

Notice how this formula coincides with the verification condition for the definition of product obtained by the traditional weakest-precondition calculus. Consider now the same VC, when we select the next handler for factorization, as described in Section 3:

$$
\begin{align*}
b \geq 0 & \rightarrow \\
a \cdot b + 0 &= a \cdot b \land b \geq 0 \land \\
\forall pqr. p \cdot q + r &= a \cdot b \land q \geq 0 \rightarrow \\
(q > 0 & \rightarrow \\
\forall s. ((q \mod 2 = 1 \land s = r + p) \lor (q \mod 2 \neq 1 \land s = r)) \rightarrow \\
(p + p) \cdot (q \text{ div } 2) + s &= a \cdot b \land q \text{ div } 2 \geq 0) \land \\
(q \neq 0 & \rightarrow r = a \cdot b)
\end{align*}
$$

The formula $\lambda s. (q \mod 2 = 1 \land s = r + p) \lor (q \mod 2 \neq 1 \land s = r)$ is the strongest post-condition of the expression if $(q \mod 2 = 1) \rightarrow (\text{next}(r+p)) \rightarrow (\text{next} r)$ with respect to the continuation next. The method of compact verification conditions proposed by Flanagan and Saxe [7] aggregates in a similar way the strongest postconditions across alternative execution paths. The connection between the compact verification conditions and the classical weakest-precondition calculus was studied by Leino [12]. Our approach makes this connection even more prominent, as it allows us to derive both forms from the common precursor verification condition.

# 5 Implementation

We have implemented the COMA language and its VC generator on top of the WHY3 platform [6]. The terms and formulas of COMA are written in the logical language of WHY3. This way, we can make use of logical theories from the WHY3 standard library, and we readily benefit from WHY3's interface with many automated theorem provers. In addition to what is presented in the previous sections, our implementation offers a few extensions, described below.
```pascal
product (a b:int) {b >= 0} (return (c:int) {c=a*b})
= loop a b 0
/ loop (p q r:int) {p·q + r = a·b ∧ q ≥ 0}
= if (q > 0) (→ if (q mod 2 = 1) (→ next (r + p)) (→ next r)
/ next (s:int) = loop (p + p) (q div 2) s)
(→ return r)
```

<caption>Fig. 10: Extended handler prototypes.</caption>

**Extended handler prototypes.** To facilitate writing and understanding of COMA programs, we provide a suitable syntax for writing pre- and postconditions directly in the handler prototype, as shown in Fig. 10. This notation is desugared into assertions, barriers, and wrapper handlers of the core COMA language; in particular, the code in Fig. 10 is translated into what is shown in Fig. 5. The precondition `{b ≥ 0}` in the prototype of product becomes an assertion put on top of the definition body, now hidden under a black-box barrier. The same transformation is applied to the precondition of the inner loop handler. The postcondition `{c = a·b}`, attached to return, forces creation of a wrapper handler above the main black-box barrier and becomes the precondition in the body of this wrapper handler.

**Let-binding for variables.** We added a proper syntax for binding a variable to a term, to avoid writing anonymous handler applications `((x:τ) → e) s`. The new construction is written `e / x:τ = s`. We show its use in the example in Fig. 13 in the next section.

**Mutable state.** Our implementation supports mutable variables (references) that can be allocated, modified, and passed as arguments to handlers. References are alias-free, which means that is forbidden to pass a statically accessible reference as an argument or to pass the same reference argument twice. Each handler is annotated with a pre-write clause, which lists the references in its lexical scope that might be modified before the handler is executed. For example, here is the prototype of a handler that increments an integer reference received as argument and returns its previous value:

```pascal
incr (&r:int) (return [r] (p:int))
```

The pre-write annotation `[r]` for the return outcome signifies that the code that calls return—namely, the incr handler—may change the value of r before the call. Pre-write annotations are automatically inferred for defined handlers and their continuation parameters. However, we do not infer them for the higher-order outcomes (i.e., continuation parameters of a continuation parameter).

The code with references is translated into pure COMA via a fine-grained monadic transformation, during which the references in the pre-write annotations become additional term parameters. In the example above, after translation, incr would return to the caller the updated value of r along with its previous value in p.

To capture the pre-state of references, we admit let-bindings in handler prototypes. The full prototype of incr, together with its specification, is as follows:

```pascal
incr (&r:int) [o:int = r] (return [r] (p:int) {r = o + 1 ∧ p = o})
```
<figure><img src="image_13.png" /><figcaption>Fig. 11: VC generation time: COMA vs WHY3 (lower values favor COMA).</figcaption></figure>

**Specification extraction.** Given a first-order handler, COMA can produce, on request, the logical predicates that represent its pre- and postconditions. Consider the following handler which returns the value stored in the root node of a non-empty tree:

```
getRoot (t: tree elt) (return (v: elt)) =
unTree elt t ((nil: tree elt) (u: elt) (nil: tree elt) -> return u) fail
```

The caller VC of `getRoot`, for a given tree `t` and continuation `return`, is the recipe

$$ (\forall \mathit{lvr}. t = \mathit{Node} \ l \ v \ r \rightarrow \mathit{return} v) \wedge (t = \mathit{Empty} \rightarrow \mathbf{0}) \quad (\star) $$

To compute the precondition of `getRoot`, we merely need to instantiate `return` with a neutral recipe `λx.‡0`. After evaluation and simplification, we obtain `t ≠ Empty`.

To compute the postcondition, we neutralize the recipe `(★)`, eliminating the subgoals that belong to the precondition, and instantiate `return` with the recipe `λx.z = x → 0`, where `z` is fresh. After evaluation, we obtain `∀lvr.t = Node l v r → z = v → ⊥`, which is equivalent to `¬(∃lr.t = Node l z r)`. This last formula is exactly the negated postcondition of `getRoot`, where `z` denotes the returned value.

This procedure works in a similar way to subgoal factorization discussed in Sec. 3. It is easily extended to handlers with multiple outcomes, producing a separate postcondition for each of them.

**Benchmarks.** We evaluated the performance of our VC generator using the CREUSOT test suite<fnref n="2" />. CREUSOT switched its VC generation back-end from WHY3 to COMA at release 0.2. We used the Rust files from the test suite that did not change during the switch (235 files). For each of those files, we measured the VC generation time with both back-ends and excluded those where the absolute difference was smaller than the sum of two standard deviations. For the 33 remaining files, Fig. 11 shows the relative and the absolute time difference (black and white bars, respectively). The negative values in the chart are where the VCgen of COMA is faster than that of WHY3, which is the case for all but one test file. For a third of the tests, COMA was more than 50% faster.

<footnote n="2">² This evaluation can be reproduced using the instructions in the Zenodo archive available online at https://doi.org/10.5281/zenodo.14766822.</footnote>
<figure><img src="image_14.png" /><figcaption>Fig. 12: Regular expression engine in OCaml.</figcaption></figure>

<figure><img src="image_15.png" /><figcaption>Fig. 13: Regular expression engine in COMA.</figcaption></figure>

## 6 Case Study: Regular Expression Processing

In this section, we demonstrate the use of COMA by verifying a small, yet non-trivial OCaml program, that uses higher-order functions, exceptions, and requires giving specification to closures in order to be verified. Figure 12 shows a function `accept` that checks if a string `s` is recognized by a regular expression `r`. The code traverses the string with a recursive function `a`, which takes three parameters: a current regexp `r`, an integer index `i`, and a continuation `k`. This function tries to match a substring `s[i..j]` with `r`, and then applies the continuation `k` to index `j` to proceed with the matching of `s[j..]`. If no such `j` exists, function `a` returns the unit value `()`. The initial continuation passed to function `a` signals a success by raising the predefined exception `Exit`.

Figure 13 contains a COMA version of the `accept` function, which can be obtained by a mechanical CPS-translation of the OCaml code. The `accept` handler has a `return` outcome that receives the Boolean computation result. The local handler `a` has a continuation `o`, that corresponds to the normal outcome of the original OCaml function.
```
predicate cons (s: string) (r: regexp) (ck: int → bool) (i: int) =
    exists j. i ≤ j ≤ length s ∧ mem s[i..j] r ∧ ck j

accept (r: regexp) (s: string) (return (b: bool) { b ↔ mem s r })
    = a r θ (j ↦ j = n) (j h → if (j = n) (→ return true) h) (→ return false)
/ a (r: regexp) (i: int) (ck: int → bool) { θ ≤ i ≤ n }
    (k (j: int) { mem s[i..j] r ∧ i ≤ j ≤ n } (h { not (ck j)}))
    (o { not (cons s r ck i) })

= unRe r empty eps char alt cat star
/ empty = o
/ eps = k i o
/ char c = if (i < n && s[i] = c) (k (i + 1) o) o
/ alt r1 r2 = a r1 i ck k (→ a r2 i ck k o)
/ cat r1 r2 = a r1 i (j ↦ cons s r2 ck j) (j h → a r2 j ck k h) o
/ star r1 = k i (→ a r1 i (j ↦ i < j ∧ cons s r ck j)
    (j h → if (i < j) (→ a r j ck k h) h) o)

/ n: int = length s
```

<caption>Fig. 14: Regular expression engine in COMA, with specification.</caption>

Finally, the continuation k is transformed itself into CPS-style, and thus has its own outcome, named h. Another way to look at this code is to interpret k and o as success and error/backtrack continuations, respectively, as in a double-barreled CPS [17]. The pattern-matching on the regular expression r is performed using a library handler unRe similar to the unTree handler.

To verify this program, we need to add specifications. Figure 14 contains a version of accept with added preconditions (in cyan) and ghost parameters (in gray). As explained in Section 5, specification annotations in handler prototypes are automatically desugared into assertions, black-box barriers, and wrapper handlers. The postcondition of accept (i.e., the precondition of return) uses a built-in logical predicate mem, where mem s r holds if and only if the string s belongs to the language of r.

We add a ghost parameter ck to handler a for the purpose of its specification. Note that the current implementation of COMA does not provide any special treatment for ghost code and data. In future, we plan to introduce the necessary checks that ensure that ghost computations do not interfere with the observable part of the program. As in the OCaml code, handler a tries to match a substring `s[i..j]` with r, and then applies the continuation k to index j to proceed with the matching of `s[j..]`. The ck parameter is a first-class predicate which characterizes the index j passed to k. The cons predicate, declared on top of the figure, is a shortcut to simplify annotations.

In addition to the annotations given in Fig. 14, we have also instrumented the COMA code to verify the termination of handler a, as described in Section 4. In this case, the variant is a pair (`|s| - i`, `r`), ordered lexicographically: namely, we either progress in string s or we move to a smaller regular expression. When the VC for handler accept is sent to WHY3, it is split into 44 individual proof tasks which are easily discharged by the SMT solvers Z3 [4] and Alt-Ergo [3].
```c
# sort the bits of %rdi using ``I can't believe it can sort''
sortbits:
    mov    %rdi, %rax
    mov    $0x8000000000000000, %rdi
loop1:  #@ invariant pop(rdi) = 1 ^ pop(rax) = pop(rdi@sortbits)
        mov    $0x8000000000000000, %rsi
loop2:  #@ invariant pop(rsi) = 1 ^ pop(rax) = pop(rdi@sortbits)
        mov    %rax, %rcx              # if !(rax & rdi)
        and    %rdi, %rcx
        jnz    cont2
test2:  mov    %rax, %rcx              # and (rax & rsi)
        and    %rsi, %rcx
        jz     cont2
swap:   or     %rdi, %rax              # then swap bits
        andn   %rax, %rsi, %rax
cont2:  shr    $1, %rsi
        jnz    loop2
cont1:  shr    $1, %rdi
        jnz    loop1
        #@ assert pop(rax) = pop(rdi@sortbits)
        ret
```

<caption>Fig. 15: Example of verified x86-64 code.</caption>

## 7 Case Study: Verified Assembly Code

We believe that COMA is a suitable intermediate language for the verification of unstructured programs. As a proof of concept, we have built a prototype tool for the deductive verification of x86-64 assembly programs. The input of the tool is assembly code annotated with assumptions, assertions, and loop invariants. Figure 15 shows the x86-64 assembly code for a function sortbits that sorts the bits of a 64-bit integer using the "I can't believe it can sort" algorithm by Fung [8]. We use the AT&T syntax, with the destination operand on the right. For instance, `mov A, B` copies the register A into B, and `andn A, B, C` computes $A \land \neg B$ and stores it in C. Integer literals start with a `$` sign. The code contains unnecessary labels (e.g., `test2`), which are only introduced to simplify the forthcoming explanations.

Function sortbits receives an integer in the rdi register and returns an integer in the rax register, with the same number of bits, which are moved to the least significant positions. The code iterates over all pairs of bits $0 \le i, j < 64$, using registers rdi and rsi, with two nested loops. Whenever the bit i is clear and the bit j is set, the two bits are swapped. (It is not obvious why this sorting procedure is correct; see Fung's paper for an explanation.) The code contains logical annotations as special comments: namely, two loop invariants and one assertion before the function end. Here, we only show that the population count remains constant (using a logical function pop), but we do not show that bits are indeed sorted. We use the notation `rdi@sortbits` to refer to the value of the rdi register at function entry.
<figure><img src="image_16.png" /><figcaption>Fig. 16: Compilation passes for sortbits.</figcaption></figure>

Our tool parses the code and its annotations, and starts with building its control-flow graph (depicted in Fig. 16a). Then, it computes the dominator tree, the entry point being the function entry. A basic block A dominates a block B whenever any path from the entry to B traverses A. For instance, block loop2 dominates block test2, which itself dominates swap2. Finally, our tool builds a COMA code that follows the structure of the dominator tree. In this way, we do not need to repeat the outer invariant in the inner loop for variables that are not modified. For instance, the handler swap2 is a local definition in handler test2, which is itself a local definition in handler loop2. Each invariant is translated into an assertion followed by a barrier. Figure 16b shows the structure of the COMA code for sortbits. For an easier reading, we omit type annotations and we have left only what relates to control-flow and specification. Conditional jumps are translated using the primitive if (and suitable Boolean conditions $b_i$), and unconditional jumps are handler calls. Parts where references are modified are written "[...]" for clarity. The translated code relies on our WHY3 model of a fragment of the x86-64 instruction set. For instance, the instruction andn is translated into a COMA reference assignment &rax ← andn rax rsi, where the logical function andn is defined in the accompanying WHY3 library.

The COMA back-end computes the VC for the code in Fig. 16b, and sends it to WHY3. There it is split into 5 proof tasks—two instances of invariant initialization, two instances of invariant preservation, and the final postcondition—which are automatically proved by Z3 and Alt-Ergo.
# 8 Related work

To our knowledge, no deductive verification system features explicit abstraction barriers in the style of COMA. Compared to the widely used intermediate verification languages like BOOGIE [13], VIPER [14] or WHYML [6], COMA is a smaller language, with fewer constructs and a simpler VC generator. Still, we are not aware of an autoactive program verifier that would admit the higher-order regexp example from Section 6. To handle stateful computations, COMA implements first-class alias-free mutable variables, which is close to what is provided by BOOGIE and WHYML. VIPER, in comparison, offers a significantly more powerful ownership-based reasoning framework.

There is a natural connection between the weakest-precondition calculus and the CPS transformation, the former being a predicate transformer and the latter a structurally similar code transformer. This connection was first studied on a minimal imperative language by Jensen [9]. This work was later extended with exception handling and goto statement by Audebaud and Zucca [1], and furthermore, with recursion, higher-order functions, and side effects by Kura [11]. A predicate transformer called the Dijkstra monad, introduced by Swamy et al. [16] and used to verify higher-order and effectful F\* programs, also highlights this connection. COMA exploits in a similar manner the relation between the continuation-based style and the WP computation. Explicit abstraction barriers allow us to verify recursive code without computing a fixed point of its verification condition.

The CFML tool developed by Charguéraud [2] serves for interactive verification of higher-order stateful programs, written in a subset of OCaml. Programs are translated into so-called characteristic formulas, which essentially capture the weakest precondition of the programs, with respect to a shallow embedding of separation logic in Coq. Specifications are proved in the form of lemmas derived from characteristic formulae. Unlike COMA, or other VC-based program verifiers, the program logic rules of CFML have to be applied manually in the course of an interactive Coq proof. Assertions and invariants are provided as the proof progresses, which limits the possibilities for automation. On the other hand, CFML offers a greater flexibility in stating properties of program code, such as verifying a given function against two different contracts.

# 9 Conclusion

We presented COMA, a higher-order IVL with explicit abstraction barriers that can be placed inside function definitions to make the exposed part of the computation appear in the specification. This allows us to write specifications in a more concise and flexible way, without having to manually translate executable code into logical specification.

In the future, we consider adding the mechanisms of ownership and borrowing to handle the mutable state, and using prophecy variables in verification conditions. We are also interested in supporting more advanced control structures, such as iterators, coroutines, and algebraic effects. We consider an alternative VC rule, where an above-barrier subhandler definition is verified at the callee site rather than the caller site. In certain programs with nested loops, like the sortbits example from Sec. 7, this allows us to move all invariants into inner loops, avoiding repetition and reducing specification burden. Finally, we continue to improve the efficiency of our implementation, in particular the recipe evaluation engine and the subgoal factorization heuristics.
References

1. Audebaud, P., Zucca, E.: Deriving proof rules from continuation semantics. Formal aspects of computing 11, 426–447 (1999)

2. Charguéraud, A.: Characteristic formulae for the verification of imperative programs. In: Chakravarty, M.M.T., Hu, Z., Danvy, O. (eds.) Proceeding of the 16th ACM SIGPLAN International Conference on Functional Programming (ICFP). vol. 46(9), pp. 418–430. ACM, Tokyo, Japan (September 2011)

3. Conchon, S., Coquereau, A., Igu kernela, M., Mebsout, A.: Alt-Ergo 2.2. In: SMT Workshop: International Workshop on Satisfiability Modulo Theories (2018)

4. De Moura, L., Bjørner, N.: Z3: An efficient SMT solver. In: International conference on Tools and Algorithms for the Construction and Analysis of Systems. vol. 4963, pp. 337–340. Springer (2008)

5. Denis, X., Jourdan, J.-H., Marché, C.: Creusot: a foundry for the deductive verification of Rust programs. In: International Conference on Formal Engineering Methods. vol. 13478, pp. 90–105. Springer (2022)

6. Filliâtre, J.-C., Paskevich, A.: Why3 — where programs meet provers. In: Felleisen, M., Gardner, P. (eds.) Proceedings of the 22nd European Symposium on Programming. Lecture Notes in Computer Science, vol. 7792, pp. 125–128. Springer (Mar 2013)

7. Flanagan, C., Saxe, J.B.: Avoiding exponential explosion: Generating compact verification conditions. In: Principles Of Programming Languages. vol. 36(3), pp. 193–205. ACM (2001)

8. Fung, S.P.Y.: Is this the simplest (and most surprising) sorting algorithm ever? arXiv preprint arXiv:2110.01111 (2021)

9. Jensen, K.: Connection between Dijkstra's predicate-transformers and denotational continuation-semantics. DAIMI Report Series 86 (1978)

10. Krivine, J.-L.: Un interprèteur du λ-calcul. Unpublished report (1985)

11. Kura, S.: Higher-Order Weakest Precondition Transformers via a CPS transformation. arXiv preprint arXiv:2301.09997 (2023)

12. Leino, K.R.M.: Efficient weakest preconditions. Information Processing Letters 93(6), 281–288 (2005)

13. Leino, K.R.M.: This is Boogie 2. KRML Manuscript 178 (2008)

14. Müller, P., Schwerhoff, M., Summers, A.J.: Viper: A verification infrastructure for permission-based reasoning. In: Verification, Model Checking, and Abstract Interpretation: 17th International Conference. vol. 9583, pp. 41–62. Springer (2016)

15. Statman, R.: Logical relations and the typed λ-calculus. Information and control 65(2-3), 85–97 (1985)

16. Swamy, N., Weinberger, J., Schlesinger, C., Chen, J., Livshits, B.: Verifying higher-order programs with the Dijkstra monad. ACM SIGPLAN Notices 48(6), 387–398 (2013)

17. Thielecke, H.: Comparing control constructs by double-barrelled CPS. Higher-Order and Symbolic Computation 15, 141–160 (2002)
A Terms and formulas

The grammar of types, terms and logical formulas, as used in this paper, is presented below. Of course, any practical implementation of COMA will choose its own set of types and operations, and may also allow the programmer to extend it when desired.

$$
\begin{array}{l@{\hspace{2em}}l}
\text{variable:} & x, y, \alpha, \beta \\[1.5ex]
\text{term:} & s, t, \tau, \theta \\
\phantom{\text{term:}} & ::= \begin{array}[t]{@{}l@{}}
\text{Type} \mid \mathbf{bool} \mid \mathbf{int} \\
\quad x \mid \text{tree } \tau \mid \text{seq } \tau \\
\quad \top \mid \bot \mid \theta \mid 1 \mid 2 \mid \dots \\
\quad s + t \mid s - t \mid s * t \\
\quad s = t \mid s < t \mid s > t \\
\quad \text{Node } s_1 \ s_2 \ s_3 \mid \text{Empty} \\
\quad \llbracket \bar{s} \rrbracket \mid s_1 \ [ \ s_2 \ \dots \ s_3 \ ] \\
\quad \text{concat } s \ t \mid \text{length } s
\end{array} \\[1.5ex]
\end{array}
$$

$$
\begin{array}{lcl}
\text{formula:} & \varphi, \psi & ::= \\
& & \quad s \mid \neg \varphi \mid \varphi \wedge \psi \\
& & \quad \varphi \rightarrow \psi \mid \varphi \vee \psi \\
& & \quad \forall x : \tau . \varphi \mid \exists x : \tau . \varphi
\end{array}
$$

As explained in Section 2, type expressions are treated as terms, so that a type annotation `s`: `τ` matches both `42:int` and `int:Type`. We do not include an access operator for sequences; instead, we use the ternary slice operator `s[i..j]`, which is defined for all sequences `s` and integers `i`, `j`, producing the sequence (possibly empty) of all elements `s_k` such that `i ≤ k < j`. Finally, we use Boolean terms as atomic formulas; however, a non-atomic formula cannot be used as a Boolean term.

Figure 17 shows the typing rules for terms. Since we do not distinguish type and term variables, the rule for `x`: `τ` also applies to `α`: `Type`. Notice, however, that the symbol `Type` itself does not have any type assigned to it.

Figure 18 shows the typing rules for logical formulas. The quantifiers in user-written formulas are restricted to data variables, whose type is not Type. This restriction is relaxed in fully evaluated verification conditions, as produced by the `◦` operator from Section 3: in those, type variables can be universally quantified. Such quantifiers may only appear in positive positions, and never under an existential quantifier, avoiding the need in dependent types.

B Undefined Behaviour (Proof of Theorem 2)

A stack `l` covers a cell `C = ⟨b, Σ, Φ⟩` if one of the two condition holds: either `C` appears in `l`, or `b = τ` and `l` covers `Σ`. As with any property of cells extended to cell contexts, the last condition means that `l` covers every cell in `Σ` as well as its neutralization; the latter requirement is trivially satisfied, since any neutralized cell admits an arbitrary cover.

We say that a cell $C = \langle b, \Sigma, \Phi \rangle$ *submits* to a type signature $\pi$ if for every aligned stack $\ell$ that submits to $\pi$, for every cell $C_0 = \langle b_0, \Sigma_0, \mathbf{0}_\pi \rangle$ and aligned stack $\ell_0$, such that $b_0$ implies $b$ and $\ell_0$ covers both $\Sigma$ and $\ell$, we have $C_0 \circ \ell_0 \Rightarrow C \circ \ell$.
<figure><img src="image_17.png" /><figcaption>Fig. 17: Typing rules for terms.</figcaption></figure>

<figure><img src="image_18.png" /><figcaption>Fig. 18: Typing rules for formulas.</figcaption></figure>
**Lemma 9.** *All cells submit to all type signatures.*

*Proof.* By induction over the order of the type signature. Let us pick a type signature $\pi$ and assume, by the induction hypothesis, that all cells submit to every type signature of a lower order than $\pi$. Now it suffices to prove that for any cell $C = \langle b, \Sigma, \Upsilon \rangle$, if $\Sigma$ submits to $\pi$, then so does $C$. Once this is established, a simple induction over cell depth will allow us to conclude. We proceed by induction over the size of $\Upsilon$, counting only the subrecipes, so that term substitutions do not affect the size.

Consider a stack $\ell$ aligned with $C$ that submits to $\pi$. Consider a cell $C_0 = \langle b_0, \Sigma_0, \mathbf{0}_\pi \rangle$ such that $b_0$ implies $b$, and an aligned stack $\ell_0$ that covers $\Sigma$ and $\ell$. We need to show $C_0 \circ \ell_0 \Rightarrow C \circ \ell$. If $b_0$ is $\perp$, then $C_0 \circ \ell_0$ evaluates to $\perp$, which trivially entails $C \circ \ell$. Otherwise, both $b_0$ and $b$ are $\top$, and we have the following cases to consider.

Case $\Upsilon$ is $\mathbf{0}$. Since $b$ is $\top$, the formula $C \circ \ell$ is also $\top$.

Case $\Upsilon$ is $h$. Let $\Sigma(h)$ be a cell $C_h = \langle b_h, \Sigma_h, \Phi_h \rangle$. As $\ell_0$ covers $C_h$, either $C_h$ is in $\ell_0$ or $b_h = \top$ and $\ell_0$ covers $\Sigma_h$. If the latter, we have $C_0 \circ \ell_0 \Rightarrow C_h \circ \ell$, as $C_h$ submits to $\pi$. Otherwise, $C_h$ appears in $\ell_0$. By Corollary 1, we have $C_h \circ \ell \Leftrightarrow \mathfrak{h}C_h \circ \ell \wedge C_h \circ \mathfrak{h}\ell$. The cell $\mathfrak{h}C_h$ submits to $\pi$ and $\ell_0$ covers the neutralized context $\mathfrak{h}\Sigma_h$. Then $C_0 \circ \ell_0 \Rightarrow \mathfrak{h}C_h \circ \ell$. To prove $C_0 \circ \ell_0 \Rightarrow C_h \circ \mathfrak{h}\ell$, we note that $C_0 \circ \ell_0$ evaluates to a conjunction, where one part is of the form $\langle \top, \Sigma'_0, \forall \bar{x}:\bar{\tau}. \forall \bar{g}:\bar{\rho}. f \bar{x} \bar{g} \rangle \circ \varepsilon$ such that $\Sigma'_0(f)$ is $C_h$. By evaluating this formula further, we obtain $\forall \bar{x}:\bar{\tau}. C_h \circ \bar{x}, \langle \top, \Sigma''_0, g_1 \rangle, \dots, \langle \top, \Sigma''_0, g_n \rangle$, where $\Sigma''_0$ is $\Sigma'_0 \upharpoonright [g_1 \mapsto \langle \top, \Sigma'_0, \mathbf{0}_{\varrho_1} \rangle, \dots, g_n \mapsto \langle \top, \Sigma'_0, \mathbf{0}_{\varrho_n} \rangle]$. Consider any cell $\langle \top, \Sigma''_0, g_i \rangle$ along with the $i$-th cell in $\mathfrak{h}\ell$, which we shall denote $\mathfrak{h}D_i$. The two cells have the same type $\varrho_i$. Since the order of $\varrho_i$ is two less than the order of $\pi$, all cells submit to $\varrho_i$. Therefore, for any aligned stack $\ell''$, we obtain $\langle \top, \Sigma''_0, g_i \rangle \circ \ell'' = \langle \top, \Sigma'_0, \mathbf{0}_{\varrho_i} \rangle \circ \ell'' \Rightarrow \mathfrak{h}D_i \circ \ell''$, since $\ell''$ covers itself as well as the neutralized cell context of $\mathfrak{h}D_i$. Then $\langle \top, \Sigma''_0, g_i \rangle \Rightarrow \mathfrak{h}D_i$ by Lemma 3. By the same reasoning, we also have $\mathfrak{h}\langle \top, \Sigma''_0, g_i \rangle \Rightarrow \mathfrak{h}\mathfrak{h}D_i$. Consequently, $\forall \bar{x}:\bar{\tau}. C_h \circ \bar{x}, \langle \top, \Sigma''_0, g_1 \rangle, \dots, \langle \top, \Sigma''_0, g_n \rangle \Rightarrow \forall \bar{x}:\bar{\tau}. C_h \circ \bar{x}, \mathfrak{h}D_1, \dots, \mathfrak{h}D_n \Rightarrow C_h \circ \mathfrak{h}\ell$. Thus, $C_0 \circ \ell_0$ implies $C_h \circ \ell$.

Case $\Upsilon$ is $\mathfrak{h}\Phi$. As neutralized cells admit any cover, $\ell_0$ covers $\mathfrak{h}\Sigma$. By the induction hypothesis, $\langle \top, \mathfrak{h}\Sigma, \Phi \rangle$ submits to $\pi$, and $C_0 \circ \ell_0 \Rightarrow \langle \top, \mathfrak{h}\Sigma, \Phi \rangle \circ \ell$.

Case $\Upsilon$ is $\Phi\Psi$. Let $C_1$ be $\langle \top, \Sigma, \Phi \rangle$ and $C_2$ be $\langle \top, \Sigma, \Psi \rangle$. By the induction hypothesis, $C_1, C_2, \mathfrak{h}C_2$ submit to $\pi$. Also, $\ell_0$ covers $C_2$ and $\mathfrak{h}C_2$, and so $C_0 \circ \ell_0 \Rightarrow C_1 \circ C_2, \ell$.

Case $\Upsilon$ is $\lambda g: \varrho. \Phi$. The stack $\ell$ is of the form $C', \ell'$, where the cells $C'$ and $\mathfrak{h}C'$ submit to $\pi$ and are covered by $\ell_0$. Then $\Sigma \upharpoonright [g \mapsto C']$ also submits to $\pi$ and is covered by $\ell_0$. By the induction hypothesis, $C_0 \circ \ell_0 \Rightarrow \langle \top, \Sigma \upharpoonright [g \mapsto C'], \Phi \rangle \circ \ell'$.

Case $\Upsilon$ is $\Phi \wedge \Psi$. Let $C_1$ be $\langle \top, \Sigma, \Phi \rangle$ and $C_2$ be $\langle \top, \Sigma, \Psi \rangle$. By the induction hypothesis, $C_0 \circ \ell_0$ entails both $C_1 \circ \ell$ and $C_2 \circ \ell$.

Case $\Upsilon$ is $\forall x: \tau. \Phi$. By the induction hypothesis, $C_0 \circ \ell_0$ implies $\langle \top, \Sigma, \Phi \rangle \circ \varepsilon$. We can safely assume that the variable $x$ does not occur in $C_0 \circ \ell_0$, and thus, $C_0 \circ \ell_0$ entails $\forall x: \tau. \langle \top, \Sigma, \Phi \rangle \circ \varepsilon$.

The rest of the cases are handled in a similar way. $\square$

**Corollary 3 (Theorem 2).** *Consider a type signature $\pi$ and a cell $J = \langle \perp, \Sigma, \mathbf{0}_\pi \rangle$. For every cell $C$ of type $\pi$, we have $J \Rightarrow C$ and $\mathfrak{h}J \Rightarrow \mathfrak{h}C$.*

*Proof.* By Lemma 3. For any aligned stack $\ell$, we have $J \circ \ell = \perp \Rightarrow C \circ \ell$. For the second part, we note that $\ell$ covers itself and the cell context of $\mathfrak{h}C$, hence $\mathfrak{h}J \circ \ell \Rightarrow \mathfrak{h}C \circ \ell$. $\square$
## C Cell factorization (Proof of Lemma 6)

Consider a cell $D$ of type $\bar{x}:\bar{\tau}$, where none of the term types $\tau_i$ is equal to Type. We say that a cell $C = \langle b, \Sigma, \Phi \rangle$ wraps around $D$ when either $C$ is equal to $D$ or $b = \top$ and $\Sigma$ wraps around $D$. This is a special case of a broader notion from the previous section: $C$ wraps around $D$ exactly when the singleton stack $D$ covers $C$. We say that $C$ releases $D$, when $C$ wraps around $D$ and for any stack $\ell$ that is aligned with $C$ and releases $D$, we have $C \circ \ell \Leftrightarrow \forall \bar{z}:\bar{\tau}. (C' \circ \ell') \lor (D \circ \bar{z})$, where $C'$ and $\ell'$ are obtained by replacing every occurrence of $D$ in $\Sigma$ and $\ell$, respectively (including recursively inside nested cell contexts), with the cell $D' = \langle \bot, \emptyset, \lambda \bar{x}:\bar{\tau}. z_1 = x_1 \land \dots \land z_n = x_n \to \mathbf{0} \rangle$.

**Lemma 10.** Any cell $D$ of type $\bar{x}:\bar{\tau}$, where none of the types $\tau_i$ is Type, releases itself.

*Proof.* Since $D$ cannot appear in its own cell context, and any aligned stack is a sequence of terms, we obtain $\forall \bar{z}:\bar{\tau}. (D \circ \bar{s}) \lor (D \circ \bar{z}) \Leftrightarrow (D \circ \bar{s}) \lor (\forall \bar{z}:\bar{\tau}. D \circ \bar{z}) \Leftrightarrow D \circ \bar{s}$. $\square$

**Lemma 11.** Consider a cell $D$ of type $\bar{x}:\bar{\tau}$, where none of the term types $\tau_i$ is Type. Any cell $C$ that wraps around $D$, releases $D$.

*Proof.* It is sufficient to prove that every cell $C = \langle \top, \Sigma, \Upsilon \rangle$, where $\Sigma$ releases $D$, also releases $D$. Once this is established, a simple induction over cell depth together with Lemma 10 allow us to conclude. We proceed by induction over the size of $\Upsilon$, counting only the subrecipes, so that term substitutions do not affect the size. Since first component of $C$ is $\top$ and $\Sigma$ wraps around $D$, the cell $C$ also wraps around $D$. Consider a stack $\ell$ that is aligned with $C$ and releases $D$. Let $\Sigma'$ and $\ell'$ denote the result of replacing all occurrences of $D$ throughout $\Sigma$ and $\ell$, respectively, with the cell $D' = \langle \bot, \emptyset, \lambda \bar{x}:\bar{\tau}. z_1 = x_1 \land \dots \land z_n = x_n \to \mathbf{0} \rangle$. Let $C'$ be the cell $\langle \top, \Sigma', \Upsilon \rangle$. We need to prove that $C \circ \ell \Leftrightarrow \forall \bar{z}:\bar{\tau}. (C' \circ \ell') \lor (D \circ \bar{z})$.

Case $\Upsilon$ is $h$ and $\Sigma(h) = D$. Then $\ell$ is a sequence of terms $\bar{s}$, and $\ell' = \ell$. We have

$$ 
\begin{align*}
\forall \bar{z}:\bar{\tau}. (C' \circ \bar{s}) \lor (D \circ \bar{z}) &= \forall \bar{z}:\bar{\tau}. (D' \circ \bar{s}) \lor (D \circ \bar{z}) \\
&= \forall \bar{z}:\bar{\tau}. (z_1 = s_1 \land \dots \land z_n = s_n \to \bot) \lor (D \circ \bar{z}) \\
&\Leftrightarrow \forall \bar{z}:\bar{\tau}. z_1 = s_1 \land \dots \land z_n = s_n \to D \circ \bar{z} \\
&\Leftrightarrow D \circ \bar{s} = C \circ \bar{s}
\end{align*}
$$

Case $\Upsilon$ is $h$ and $\Sigma(h) \neq D$. By hypothesis, $\Sigma(h)$ releases $D$. Let $C''$ denote $\Sigma(h)$ after replacing all occurrences of $D$ in its cell context with $D'$. We have $C \circ \ell = \Sigma(h) \circ \ell \Leftrightarrow \forall \bar{z}:\bar{\tau}. (C'' \circ \ell') \lor (D \circ \bar{z}) = \forall \bar{z}:\bar{\tau}. (C' \circ \ell') \lor (D \circ \bar{z})$.

Case $\Upsilon$ is $\mathbf{0}$. Since the first component of $C$ is $\top$, we have $C \circ \varepsilon = C' \circ \varepsilon = \top$.

Case $\Upsilon$ is $\mathfrak{h}\Phi$. Let $\Sigma''$ be the result of replacing all occurrences of $D$ in $\mathfrak{h}\Sigma$ with $D'$. By induction hypothesis, $C \circ \ell = \langle \top, \mathfrak{h}\Sigma, \Phi \rangle \circ \ell \Leftrightarrow \forall \bar{z}:\bar{\tau}. (\langle \top, \Sigma'', \Phi \rangle \circ \ell') \lor (D \circ \bar{z})$. Also, $\forall \bar{z}:\bar{\tau}. (C' \circ \ell') \lor (D \circ \bar{z}) = \forall \bar{z}:\bar{\tau}. (\langle \top, \mathfrak{h}\Sigma', \Phi \rangle \circ \ell') \lor (D \circ \bar{z})$. If $D$ is neutralized (that is, $D = \mathfrak{h}D$), then $D \circ \bar{z} \Leftrightarrow \top$. If $D$ is not neutralized, then it cannot occur in $\mathfrak{h}\Sigma$, and so $\Sigma'' = \mathfrak{h}\Sigma$. Furthermore, $\mathfrak{h}D \equiv \mathfrak{h}D'$, and consequently, $\mathfrak{h}\Sigma' \equiv \mathfrak{h}\Sigma$.

Case $\Upsilon$ is $\Phi\Psi$ and $\langle \top, \Sigma, \Psi \rangle = D$. Then $\Sigma$ cannot contain $D$, and $\Sigma' = \Sigma$. As the first component of $D$ is $\top$ and $\Sigma$ wraps around $D$, the cell $D$ is neutralized. Consequently, $\mathfrak{h}D = D$ and both cells release $D$ by Lemma 10. We obtain $C \circ \ell = \langle \top, \Sigma, \Phi \rangle \circ D$, $\ell \Leftrightarrow$
$\forall \overline{z}:\tau. (\langle\overline{\tau}, \Sigma, \Phi\rangle \circ D', \ell') \lor (D \circ \overline{z}) \Leftrightarrow \overline{\tau} \Leftrightarrow \forall \overline{z}:\tau. (\langle\overline{\tau}, \Sigma, \Phi\rangle \circ D, \ell') \lor (D \circ \overline{z}) \Leftrightarrow \forall \overline{z}:\tau. (C' \circ \ell') \lor (D \circ \overline{z}).$

Case $\Upsilon$ is $\Phi\Psi$ and $\langle\overline{\tau}, \Sigma, \Psi\rangle \neq D$. The cell $\langle\overline{\tau}, \Sigma, \Psi\rangle$ releases $D$ by the induction hypothesis, and so does its neutralization. Then $C \circ \ell = \langle\overline{\tau}, \Sigma, \Phi\rangle \circ \langle\overline{\tau}, \Sigma, \Psi\rangle$, $\ell \Leftrightarrow \forall \overline{z}:\tau. (\langle\overline{\tau}, \Sigma', \Phi\rangle \circ \langle\overline{\tau}, \Sigma', \Psi\rangle, \ell') \lor (D \circ \overline{z}) \Leftrightarrow \forall \overline{z}:\tau. (C' \circ \ell') \lor (D \circ \overline{z}).$

Case $\Upsilon$ is $\Phi \wedge \Psi$. Then we have

$$
\begin{align*}
C \circ \ell &= (\langle \overline{\tau}, \Sigma, \Phi \rangle \circ \ell) \wedge (\langle \overline{\tau}, \Sigma, \Psi \rangle \circ \ell) \\
&\Leftrightarrow (\forall \overline{z}:\tau. (\langle \overline{\tau}, \Sigma', \Phi \rangle \circ \ell') \lor (D \circ \overline{z})) \wedge (\forall \overline{z}:\tau. (\langle \overline{\tau}, \Sigma', \Psi \rangle \circ \ell') \lor (D \circ \overline{z})) \\
&\Leftrightarrow \forall \overline{z}:\tau. (\langle \overline{\tau}, \Sigma', \Phi \rangle \circ \ell' \wedge \langle \overline{\tau}, \Sigma', \Psi \rangle \circ \ell') \lor (D \circ \overline{z}) \\
&\Leftrightarrow \forall \overline{z}:\tau. (C' \circ \ell') \lor (D \circ \overline{z})
\end{align*}
$$

The rest of the cases are handled in a similar way. $\square$

**Lemma 12 (Lemma 6).** Consider a cell $C = \langle b, \Sigma, \lambda g : (\overline{x}:\tau) \cdot \Phi \rangle$ and an aligned stack $D, \ell$, such that none of $\tau_i$ is Type. Let $D'$ be $\langle \perp, \emptyset, \lambda \overline{x}:\tau, z_1 = x_1 \wedge \dots \wedge z_n = x_n \to 0 \rangle$ for some fresh variables $\overline{z}$. Then $C \circ D, \ell \Leftrightarrow C \circ \mathfrak{h}D, \ell \wedge \forall \overline{z}:\tau. (\mathfrak{h}C \circ D', \mathfrak{h}\ell) \lor (D \circ \overline{z}).$

*Proof.* By Lemma 4, $C \circ D, \ell \Leftrightarrow C \circ \mathfrak{h}D, \ell \wedge \mathfrak{h}C \circ D, \mathfrak{h}\ell$. If $D$ is neutralized, then $C \circ D, \ell = C \circ \mathfrak{h}D, \ell$ and $\mathfrak{h}C \circ D, \mathfrak{h}\ell \Leftrightarrow \overline{\tau}$. Otherwise, $D$ does not occur in $\mathfrak{h}C$ or $\mathfrak{h}\ell$. We conclude by Lemma 11, as neutralized cells wrap around any cell. $\square$
D Verification Condition Generation

**Lemma 13.** For any expression *e* and term substitution *σ*, we have $C_b^p(e)\sigma = C_b^p(e\sigma)$.

*Proof.* By structural induction over *e*. □

**Lemma 14.** For any expression *e* and handler symbols *f*, *g*, we have $C_b^p(e)[g \mapsto f] = C_b^p(e[g \mapsto f])$.

*Proof.* By structural induction over *e*. □

**Lemma 15.** Consider a cell *C* of the form $\langle b, \Sigma, \Phi[g \mapsto f] \rangle$. Let *b'* be an arbitrary Boolean value, and $\Sigma'$ a cell context such that $\Sigma'(f) = \Sigma(f)$. Then *C* is equivalent to $\langle b, \Sigma, \psi[g \mapsto \langle b', \Sigma', f \rangle], \Phi \rangle$.

*Proof.* By structural induction over $\Phi$. □

**Lemma 16 (Lemma 7).** For any expression $e_0$, any cell $D = \langle b, \Sigma, C_{\perp}^{\perp}(e_0) \rangle$ is neutral.

*Proof.* We proceed by induction over the size of $e_0$, counting only the subexpressions, so that term substitutions do not affect the size. Let $\ell$ be an aligned neutral stack. We need to prove that the formula $D \circ \ell$ is valid.

Case $e_0$ is $h$. Then $D \circ \ell = \langle b, \Sigma, h \rangle \circ \ell = \langle \tau, h\Sigma, h \rangle \circ \ell$ and Lemma 1 applies.

Case $e_0$ is $\pi \to e$. Then, for some cell context $\Sigma'$ and substitution $\sigma$, we have

$$ 
\begin{align*}
D \circ \ell &= \langle b, \Sigma, (\lambda\pi. C_{\perp}^{\perp}(e)) \wedge h(\lambda\pi. C_{\perp}^{\perp}(e)) \rangle \circ \ell \\
&= \langle b, \Sigma, \lambda\pi. C_{\perp}^{\perp}(e) \rangle \circ \ell \wedge \langle \tau, h\Sigma, \lambda\pi. C_{\perp}^{\perp}(e) \rangle \circ \ell \\
&\Leftrightarrow \langle b, \Sigma, \lambda\pi. C_{\perp}^{\perp}(e) \rangle \circ \ell \wedge \tau \tag{Lem. 1}
\end{align*}
$$

$$ 
\begin{align*}
&\Leftrightarrow \langle b, \Sigma', C_{\perp}^{\perp}(e)\sigma \rangle \circ \varepsilon \\
&= \langle b, \Sigma', C_{\perp}^{\perp}(e\sigma) \rangle \circ \varepsilon \tag*{(Lem. 13)}
\end{align*}
$$

$$ \Leftrightarrow \tau \tag{IH} $$

Case $e_0$ is $k \bar{s} \bar{o}$. Then we have

$$ 
\begin{align*}
D \circ \ell &= \langle b, \Sigma, C_{\perp}^{\perp}(k) \bar{s} C_{\perp}^{\perp}(o_1) \dots C_{\perp}^{\perp}(o_n) \rangle \circ \ell \\
&= \langle b, \Sigma, C_{\perp}^{\perp}(k) \rangle \circ \bar{s}, \langle b, \Sigma, C_{\perp}^{\perp}(o_1) \rangle, \dots, \langle b, \Sigma, C_{\perp}^{\perp}(o_n) \rangle, \ell
\end{align*}
$$

Each cell $\langle b, \Sigma, C_{\perp}^{\perp}(o_i) \rangle$ added to the stack is neutral by the induction hypothesis and the neutralization of this cell is neutral by Lemma 1. Thus the new stack is neutral and we conclude by the induction hypothesis.

Case $e_0$ is $\{\varphi\}e$. The stack $\ell$ is empty and we have

$$ 
\begin{align*}
D \circ \varepsilon &= \langle b, \Sigma, (\varphi \rightarrow C_{\perp}^{\perp}(e)) \wedge (\perp \rightarrow \neg \varphi \rightarrow \mathbf{0}) \rangle \circ \varepsilon \\
&= \langle b, \Sigma, \varphi \rightarrow C_{\perp}^{\perp}(e) \rangle \circ \varepsilon \wedge \langle b, \Sigma, \perp \rightarrow \neg \varphi \rightarrow \mathbf{0} \rangle \circ \varepsilon \\
&= (\varphi \rightarrow \langle b, \Sigma, C_{\perp}^{\perp}(e) \rangle \circ \varepsilon) \wedge (\perp \rightarrow \neg \varphi \rightarrow \langle b, \Sigma, \mathbf{0} \rangle \circ \varepsilon) \\
&\Leftrightarrow (\varphi \rightarrow \tau) \wedge (\perp \rightarrow \neg \varphi \rightarrow b) \tag*{(IH)}
\end{align*}
$$

$$ \Leftrightarrow \tau \wedge \tau $$
Case $e_0$ is $e / h \pi = d$. Let $\Sigma_h$ be $\Sigma \uplus [h \mapsto \langle b, \Sigma, \lambda\pi.\forall h:\pi.\mathbb{C}_{\perp}^{\top}(d)\rangle]$ and $\bar{x}:\tau$ the term parameters in $\pi$. The stack $\ell$ is empty and, for some cell context $\Sigma'$, we have

$$
\begin{align*}
D \circ \varepsilon &= \langle b, \Sigma, \text{let } h \pi = \mathbb{C}_{\perp}^{\top}(d) \text{ in } \mathbb{C}_{\perp}^{\perp}(e) \wedge \forall \pi. \mathbb{C}_{\perp}^{\perp}(d) \rangle \circ \varepsilon \\
&= \langle b, \Sigma_h, \mathbb{C}_{\perp}^{\perp}(e) \rangle \wedge \forall \pi. \mathbb{C}_{\perp}^{\perp}(d) \rangle \circ \varepsilon \\
&= \langle b, \Sigma_h, \mathbb{C}_{\perp}^{\perp}(e) \rangle \circ \varepsilon \wedge \langle b, \Sigma_h, \forall \pi. \mathbb{C}_{\perp}^{\perp}(d) \rangle \circ \varepsilon \\
&= \langle b, \Sigma_h, \mathbb{C}_{\perp}^{\perp}(e) \rangle \circ \varepsilon \wedge \forall \bar{x}:\tau. \langle b, \Sigma', \mathbb{C}_{\perp}^{\perp}(d) \rangle \circ \varepsilon \\
&\iff \top \wedge \top \tag{IH}
\end{align*}
$$

Case $e_0$ is $\uparrow e$ or $\downarrow e$. Then $\mathbb{C}_{\perp}^{\perp}(e_0)$ is $\mathbb{C}_{\perp}^{\perp}(e)$, and the induction hypothesis applies. $\square$

**Corollary 4.** Any cell of the form $\langle b, \Sigma, \mathbb{C}_{\perp}^{\top}(\pi \to e) \rangle$ is equivalent to $\langle b, \Sigma, \lambda\pi. \mathbb{C}_{\perp}^{\top}(e) \rangle$.

*Proof.* For any aligned stack $\ell$, there exist a cell context $\Sigma'$ and a term substitution $\sigma$ such that

$$
\begin{align*}
\langle b, \Sigma, \mathbb{C}_{\perp}^{\top}(\pi \to e) \rangle \circ \ell &= \langle \tau, \mathfrak{h}\Sigma, (\lambda\pi.\mathbb{C}_{\perp}^{\top}(e)) \wedge \lambda\pi.\mathbb{C}_{\perp}^{\perp}(e) \rangle \circ \ell \\
&= \langle b, \Sigma, \lambda\pi.\mathbb{C}_{\perp}^{\top}(e) \rangle \circ \ell \wedge \langle b, \Sigma, \mathfrak{h}\lambda\pi.\mathbb{C}_{\perp}^{\perp}(e) \rangle \circ \ell \\
&= \langle b, \Sigma, \lambda\pi.\mathbb{C}_{\perp}^{\top}(e) \rangle \circ \ell \wedge \langle \tau, \Sigma', \mathbb{C}_{\perp}^{\perp}(e)\sigma \rangle \circ \varepsilon \\
&= \langle b, \Sigma, \lambda\pi.\mathbb{C}_{\perp}^{\top}(e) \rangle \circ \ell \wedge \langle \tau, \Sigma', \mathbb{C}_{\perp}^{\perp}(e\sigma) \rangle \circ \varepsilon \tag{Lem. 13} \\
&\iff \langle b, \Sigma, \lambda\pi.\mathbb{C}_{\perp}^{\top}(e) \rangle \circ \ell \wedge \tau \tag{Lem. 7} \\
&\iff \langle b, \Sigma, \lambda\pi.\mathbb{C}_{\perp}^{\top}(e) \rangle \circ \ell \tag{Lem. 8}
\end{align*}
$$

**Lemma 17.** For any COMA expression $e_0$ and cell context $\Sigma$, the neutralized cells $D_1 = \langle \tau, \mathfrak{h}\Sigma, \mathbb{C}_{\perp}^{\top}(e_0) \rangle$ and $D_2 = \langle \tau, \mathfrak{h}\Sigma, \mathbb{C}_{\perp}^{\perp}(e_0) \rangle$ are equivalent.

*Proof.* We proceed by structural induction over $e_0$. By Lemma 3, it suffices to prove that $D_1 \circ \ell \Leftrightarrow D_2 \circ \ell$ for any aligned stack $\ell$.

Case $e_0$ is $h$. We can assume, without loss of generality, that $p$ is $\top$. Then we have $D_2 \circ \ell = \langle \tau, \mathfrak{h}\Sigma, \mathfrak{h}h \rangle \circ \ell = \langle \tau, \mathfrak{h}\mathfrak{h}\Sigma, h \rangle \circ \ell = \langle \tau, \mathfrak{h}\Sigma, h \rangle \circ \ell = D_1 \circ \ell$, by the idempotence of neutralization.

Case $e_0$ is $\pi \to e$. Given that $\mathfrak{h}\mathfrak{h}\Sigma = \mathfrak{h}\Sigma$, we have

$$
\begin{align*}
D_1 \circ \ell &= \langle \tau, \mathfrak{h}\Sigma, (\lambda\pi.\mathbb{C}_{\perp}^{\top}(e)) \wedge \mathfrak{h}(\lambda\pi.\mathbb{C}_{\perp}^{\perp}(e)) \rangle \circ \ell \\
&= \langle \tau, \mathfrak{h}\Sigma, \lambda\pi.\mathbb{C}_{\perp}^{\top}(e) \rangle \circ \ell \wedge \langle \tau, \mathfrak{h}\Sigma, \mathfrak{h}\lambda\pi.\mathbb{C}_{\perp}^{\perp}(e) \rangle \circ \ell \\
&= \langle \tau, \mathfrak{h}\mathfrak{h}\Sigma, \lambda\pi.\mathbb{C}_{\perp}^{\top}(e) \rangle \circ \ell \wedge \langle \tau, \mathfrak{h}\mathfrak{h}\Sigma, \lambda\pi.\mathbb{C}_{\perp}^{\perp}(e) \rangle \circ \ell \\
&= \langle \tau, \mathfrak{h}\Sigma, \mathfrak{h}\lambda\pi.\mathbb{C}_{\perp}^{\top}(e) \rangle \circ \ell \wedge \langle \tau, \mathfrak{h}\Sigma, \lambda\pi.\mathbb{C}_{\perp}^{\perp}(e) \rangle \circ \ell \\
&\iff \langle \tau, \mathfrak{h}\Sigma, \mathfrak{h}\lambda\pi.\mathbb{C}_{\perp}^{\top}(e) \rangle \circ \ell \wedge \langle \tau, \mathfrak{h}\Sigma, \lambda\pi.\mathbb{C}_{\perp}^{\top}(e) \rangle \circ \ell \\
&= \langle \tau, \mathfrak{h}\Sigma, (\lambda\pi.\mathbb{C}_{\perp}^{\top}(e)) \wedge \mathfrak{h}(\lambda\pi.\mathbb{C}_{\perp}^{\top}(e)) \rangle \circ \ell \\
&= D_2 \circ \ell
\end{align*}
$$

Case $e_0$ is $k\bar{s}\bar{o}$. Then we have $D_1 \circ \ell = \langle \tau, \mathfrak{h}\Sigma, \mathbb{C}_{\perp}^{\top}(k) \rangle \circ \bar{s} \wedge \mathbb{C}_{\perp}^{\top}(o_1) \wedge \dots \wedge \mathbb{C}_{\perp}^{\top}(o_n) \rangle \circ \ell = \langle \tau, \mathfrak{h}\Sigma, \mathbb{C}_{\perp}^{\top}(k) \rangle \circ \bar{s} \wedge \langle \tau, \mathfrak{h}\Sigma, \mathbb{C}_{\perp}^{\top}(o_1) \rangle \wedge \dots \wedge \langle \tau, \mathfrak{h}\Sigma, \mathbb{C}_{\perp}^{\top}(o_n) \rangle \circ \ell$. Each cell $\langle \tau, \mathfrak{h}\Sigma, \mathbb{C}_{\perp}^{\top}(o_i) \rangle$
is equivalent to $\langle \tau, \mathfrak{h}\Sigma, \mathbb{C}_{-\mathfrak{h}}^{\neg p}(o_i) \rangle$ by induction hypothesis. These cells are neutralized, hence the new stack is equivalent to $\bar{s}, \langle \tau, \mathfrak{h}\Sigma, \mathbb{C}_{-\mathfrak{h}}^{\neg p}(o_1) \rangle, \dots, \langle \tau, \mathfrak{h}\Sigma, \mathbb{C}_{-\mathfrak{h}}^{\neg p}(o_n) \rangle, \ell$. Since the cells $\langle \tau, \mathfrak{h}\Sigma, \mathbb{C}_{-\mathfrak{h}}^{p}(k) \rangle$ and $\langle \tau, \mathfrak{h}\Sigma, \mathbb{C}_{-\mathfrak{h}}^{\neg p}(k) \rangle$ are also equivalent by induction hypothesis, we obtain $D_1 \circ \ell \Leftrightarrow D_2 \circ \ell$ by definition of cell equivalence.

In all other cases, the expression $e_0$ is fully applied, and so are the cells $D_1$ and $D_2$. Then the stack $\ell$ is empty, and $D_1 \circ \varepsilon \Leftrightarrow \tau \Leftrightarrow D_2 \circ \varepsilon$ by Lemma 1. $\square$

**Lemma 18 (Lemma 8).** Given any expression $e_0$ and three cells $D = \langle b, \Sigma, \mathbb{C}_{\tau}^{\top}(e_0) \rangle$, $D_1 = \langle b, \Sigma, \mathbb{C}_{\mathfrak{h}}^{p}(e_0) \rangle$, and $D_2 = \langle b, \Sigma, \mathbb{C}_{-\mathfrak{h}}^{\neg p}(e_0) \rangle$, the cell $D$ is a meet of $D_1$ and $D_2$.

*Proof.* By Lemma 17, we have $\mathfrak{h}D_1 \equiv \mathfrak{h}D_2$. We proceed by induction on the size of $e_0$. By Lemma 5, it suffices to prove that $D \circ \ell \Leftrightarrow D_1 \circ \ell \wedge D_2 \circ \ell$ for any aligned stack $\ell$.

Case $e_0$ is $h$. We can assume, without loss of generality, that $\mathfrak{p}$ is $\tau$. Then $D$ is the same as $D_1$, and $D_2 \circ \ell$ is equal to $\mathfrak{h}D_1 \circ \ell$. Then $D \circ \ell \Leftrightarrow D_1 \circ \ell \wedge D_2 \circ \ell$ by Lemma 4.

Case $e_0$ is $\pi \to e$. Then, for some cell contexts $\Sigma', \Sigma''$ and term substitution $\sigma$, which are determined by $\pi$ and $\ell$, we have

$$D \circ \ell = \langle b, \Sigma, \mathbb{C}_{\tau}^{\top}(\pi \to e) \rangle \circ \ell \Leftrightarrow \langle b, \Sigma, \lambda\pi. \mathbb{C}_{\tau}^{\top}(e) \rangle \circ \ell \quad \text{(Cor. 4)}$$

$$= \langle b, \Sigma', \mathbb{C}_{\tau}^{\top}(e)\sigma \rangle \circ \varepsilon = \langle b, \Sigma', \mathbb{C}_{\tau}^{\top}(e\sigma) \rangle \circ \varepsilon \quad \text{(Lem. 13)}$$

$$\Leftrightarrow \langle b, \Sigma', \mathbb{C}_{\mathfrak{h}}^{p}(e\sigma) \rangle \circ \varepsilon \wedge \langle b, \Sigma', \mathbb{C}_{-\mathfrak{h}}^{\neg p}(e\sigma) \rangle \circ \varepsilon \quad \text{(IH)}$$

$$= \langle b, \Sigma', \mathbb{C}_{\mathfrak{h}}^{p}(e)\sigma \rangle \circ \varepsilon \wedge \langle b, \Sigma', \mathbb{C}_{-\mathfrak{h}}^{\neg p}(e)\sigma \rangle \circ \varepsilon \quad \text{(Lem. 13)}$$

$$= \langle b, \Sigma, \lambda\pi. \mathbb{C}_{\mathfrak{h}}^{p}(e) \rangle \circ \ell \wedge \langle b, \Sigma, \lambda\pi. \mathbb{C}_{-\mathfrak{h}}^{\neg p}(e) \rangle \circ \ell$$

$$\Leftrightarrow \langle b, \Sigma, \lambda\pi. \mathbb{C}_{\mathfrak{h}}^{p}(e) \rangle \circ \ell \wedge \langle b, \Sigma, \lambda\pi. \mathbb{C}_{-\mathfrak{h}}^{p}(e) \rangle \circ \ell \wedge \quad \text{(C} \Rightarrow \mathfrak{h}C)$$

$$\langle b, \Sigma, \lambda\pi. \mathbb{C}_{-\mathfrak{h}}^{\neg p}(e) \rangle \circ \ell \wedge \mathfrak{h}\langle b, \Sigma, \lambda\pi. \mathbb{C}_{-\mathfrak{h}}^{\neg p}(e) \rangle \circ \ell$$

$$\Leftrightarrow \langle b, \Sigma, \lambda\pi. \mathbb{C}_{\mathfrak{h}}^{p}(e) \rangle \circ \ell \wedge \langle b, \Sigma, \mathfrak{h}\lambda\pi. \mathbb{C}_{-\mathfrak{h}}^{\neg p}(e) \rangle \circ \ell \wedge$$

$$\langle b, \Sigma, \lambda\pi. \mathbb{C}_{-\mathfrak{h}}^{\neg p}(e) \rangle \circ \ell \wedge \langle b, \Sigma, \mathfrak{h}\lambda\pi. \mathbb{C}_{-\mathfrak{h}}^{\neg p}(e) \rangle \circ \ell$$

$$= \langle b, \Sigma, (\lambda\pi. \mathbb{C}_{\mathfrak{h}}^{p}(e)) \wedge \mathfrak{h}(\lambda\pi. \mathbb{C}_{-\mathfrak{h}}^{\neg p}(e)) \rangle \circ \ell \wedge$$

$$\langle b, \Sigma, (\lambda\pi. \mathbb{C}_{-\mathfrak{h}}^{\neg p}(e)) \wedge \mathfrak{h}(\lambda\pi. \mathbb{C}_{-\mathfrak{h}}^{\neg \neg p}(e)) \rangle \circ \ell$$

$$= D_1 \circ \ell \wedge D_2 \circ \ell$$

Case $e_0$ is $\{\varphi\}e$. Then the stack $\ell$ is empty and we have

$$D \circ \varepsilon = \langle b, \Sigma, (\varphi \to \mathbb{C}_{\tau}^{\top}(e)) \wedge (\tau \to \neg\varphi \to \mathbf{0}) \rangle \circ \varepsilon \\
= (\varphi \to \langle b, \Sigma, \mathbb{C}_{\tau}^{\top}(e) \rangle \circ \varepsilon) \wedge (\tau \to \neg\varphi \to b) \\
\Leftrightarrow (\varphi \to (\langle b, \Sigma, \mathbb{C}_{\mathfrak{h}}^{p}(e) \rangle \circ \varepsilon \wedge \langle b, \Sigma, \mathbb{C}_{-\mathfrak{h}}^{\neg p}(e) \rangle \circ \varepsilon)) \wedge (\neg\varphi \to b) \quad \text{(IH)}$$

$$\Leftrightarrow (\varphi \to \langle b, \Sigma, \mathbb{C}_{\mathfrak{h}}^{p}(e) \rangle \circ \varepsilon) \wedge (\mathfrak{p} \to \neg\varphi \to b) \wedge \\ (\varphi \to \langle b, \Sigma, \mathbb{C}_{-\mathfrak{h}}^{\neg p}(e) \rangle \circ \varepsilon) \wedge (\neg\mathfrak{p} \to \neg\varphi \to b)$$

$$= \langle b, \Sigma, (\varphi \to \mathbb{C}_{\mathfrak{h}}^{p}(e)) \wedge (\mathfrak{p} \to \neg\varphi \to \mathbf{0}) \rangle \circ \varepsilon \wedge$$

$$\langle b, \Sigma, (\varphi \to \mathbb{C}_{-\mathfrak{h}}^{\neg p}(e)) \wedge (\neg\mathfrak{p} \to \neg\varphi \to \mathbf{0}) \rangle \circ \varepsilon$$

$$= D_1 \circ \varepsilon \wedge D_2 \circ \varepsilon$$
Case E-SYM. Then $e_1$ is of the form $h \bar{s} \bar{o} // \Lambda$ and $e_2$ of the form $(\pi \to d) \bar{s} \bar{o} // \Lambda$. Let $\ell$ denote the stack $\bar{s}, \langle \perp, \Sigma_\Lambda, \mathbb{C}_\perp^T(o_1) \rangle, \dots, \langle \perp, \Sigma_\Lambda, \mathbb{C}_\perp^T(o_n) \rangle$. Assuming that the type signature $\pi$ is of the form $\bar{x}:\tau \overline{g}:\varrho$, let $\sigma$ be the term substitution $[\bar{x} \mapsto \bar{s}]$ and $\Sigma'$ the cell context $\Sigma_\Lambda \omega [g_1 \mapsto \langle \perp, \Sigma_\Lambda, \mathbb{C}_\perp^T(o_1) \rangle, \dots, g_n \mapsto \langle \perp, \Sigma_\Lambda, \mathbb{C}_\perp^T(o_n) \rangle]$. Assuming that $\Lambda$ is of the form $\Lambda_1, h \pi = d, \Lambda_2$, we obtain

$$
\begin{align*}
& \langle \perp, \Sigma_\Lambda, \mathbb{C}_\perp^T(h \bar{s} \bar{o}) \rangle \circ \varepsilon \wedge \psi_\Lambda \\
&= \langle \perp, \Sigma_\Lambda, \mathbb{C}_\perp^T(h) \rangle \circ \ell \wedge \psi_\Lambda \\
&= \langle \perp, \Sigma_{\Lambda_2}, \lambda \pi. \forall h : \pi. \mathbb{C}_\perp^T(d) \rangle \circ \ell \wedge \psi_\Lambda \\
&\Leftrightarrow \langle \perp, \Sigma_{\Lambda_2}, \lambda \pi. \forall h : \pi. \mathbb{C}_\perp^T(d) \rangle \circ \ell \wedge \langle \perp, \Sigma_{h\pi=d, \Lambda_2}, \forall \pi. \mathbb{C}_\perp^T(d) \rangle \circ \varepsilon \wedge \psi_\Lambda \\
&\Leftrightarrow \langle \perp, \Sigma_\Lambda, \lambda \pi. \forall h : \pi. \mathbb{C}_\perp^T(d) \rangle \circ \ell \wedge \langle \perp, \Sigma_\Lambda, \forall \pi. \mathbb{C}_\perp^T(d) \rangle \circ \varepsilon \wedge \psi_\Lambda \\
&\Rightarrow \langle \perp, \Sigma_\Lambda, \lambda \pi. \forall h : \pi. \mathbb{C}_\perp^T(d) \rangle \circ \ell \wedge \langle \perp, \Sigma_\Lambda, \lambda \pi. \mathbb{C}_\perp^T(d) \rangle \circ \ell \wedge \psi_\Lambda \tag{Thm. 2} \\
&\Leftrightarrow \langle \perp, \Sigma', \forall h : \pi. \mathbb{C}_\perp^T(d\sigma) \rangle \circ \varepsilon \wedge \langle \perp, \Sigma', \mathbb{C}_\perp^T(d\sigma) \rangle \circ \varepsilon \wedge \psi_\Lambda \tag{Lem. 13} \\
&\Rightarrow \langle \perp, \Sigma', \mathbb{C}_\perp^T(d\sigma) \rangle \circ \varepsilon \wedge \langle \perp, \Sigma', \mathbb{C}_\perp^T(d\sigma) \rangle \circ \varepsilon \wedge \psi_\Lambda \tag{Thm. 2} \\
&\Leftrightarrow \langle \perp, \Sigma', \mathbb{C}_\perp^T(d\sigma) \rangle \circ \varepsilon \wedge \psi_\Lambda \tag{Lem. 8} \\
&= \langle \perp, \Sigma_\Lambda, \lambda \pi. \mathbb{C}_\perp^T(d) \rangle \circ \ell \wedge \psi_\Lambda \tag{Lem. 13} \\
&\Leftrightarrow \langle \perp, \Sigma_\Lambda, \mathbb{C}_\perp^T(\pi \to d) \rangle \circ \ell \wedge \psi_\Lambda \tag{Cor. 4} \\
&= \langle \perp, \Sigma_\Lambda, \mathbb{C}_\perp^T((\pi \to d) \bar{s} \bar{o}) \rangle \circ \varepsilon \wedge \psi_\Lambda
\end{align*}
$$

Case E-APPT. Then $e_1$ is of the form $((x:\tau) \pi \to e) t \bar{s} \bar{o} // \Lambda$ and $e_2$ is of the form $(\pi \to e)[x \mapsto t] \bar{s} \bar{o} // \Lambda$. Let $\ell$ stand for $\bar{s}, \langle \perp, \Sigma_\Lambda, \mathbb{C}_\perp^T(o_1) \rangle, \dots, \langle \perp, \Sigma_\Lambda, \mathbb{C}_\perp^T(o_n) \rangle$. Then

$$
\begin{align*}
& \langle \perp, \Sigma_\Lambda, \mathbb{C}_\perp^T(((x:\tau) \pi \to e) t \bar{s} \bar{o}) \rangle \circ \varepsilon \wedge \psi_\Lambda \\
&= \langle \perp, \Sigma_\Lambda, \mathbb{C}_\perp^T((x:\tau) \pi \to e) \rangle \circ t, \ell \wedge \psi_\Lambda \\
&\Leftrightarrow \langle \perp, \Sigma_\Lambda, \lambda x : \tau. \lambda \pi. \mathbb{C}_\perp^T(e) \rangle \circ t, \ell \wedge \psi_\Lambda \tag{Cor. 4} \\
&= \langle \perp, \Sigma_\Lambda, (\lambda \pi. \mathbb{C}_\perp^T(e))[x \mapsto t] \rangle \circ \ell \wedge \psi_\Lambda \\
&= \langle \perp, \Sigma_\Lambda, \lambda \pi[x \mapsto t]. \mathbb{C}_\perp^T(e[x \mapsto t]) \rangle \circ \ell \wedge \psi_\Lambda \tag{Lem. 13} \\
&\Leftrightarrow \langle \perp, \Sigma_\Lambda, \mathbb{C}_\perp^T(\pi \to e)[x \mapsto t] \rangle \circ \ell \wedge \psi_\Lambda \tag{Cor. 4} \\
&= \langle \perp, \Sigma_\Lambda, \mathbb{C}_\perp^T((\pi \to e)[x \mapsto t]) \rangle \circ \ell \wedge \psi_\Lambda \tag{Lem. 13} \\
&= \langle \perp, \Sigma_\Lambda, \mathbb{C}_\perp^T((\pi \to e)[x \mapsto t] \bar{s} \bar{o}) \rangle \circ \varepsilon \wedge \psi_\Lambda
\end{align*}
$$

Case E-APPH. Then $e_1$ is of the form $((g:\varrho) \pi \to e) f \bar{o} // \Lambda$ and $e_2$ is of the form $(\pi \to e)[g \mapsto f] \bar{o} // \Lambda$. Let $\ell$ stand for $\langle \perp, \Sigma_\Lambda, \mathbb{C}_\perp^T(o_1) \rangle, \dots, \langle \perp, \Sigma_\Lambda, \mathbb{C}_\perp^T(o_n) \rangle$. Then

$$
\begin{align*}
& \langle \perp, \Sigma_\Lambda, \mathbb{C}_\perp^T(((g:\varrho) \pi \to e) f \bar{o}) \rangle \circ \varepsilon \wedge \psi_\Lambda \\
&= \langle \perp, \Sigma_\Lambda, \mathbb{C}_\perp^T((g:\varrho) \pi \to e) \rangle \circ \langle \perp, \Sigma_\Lambda, \mathbb{C}_\perp^T(f) \rangle, \ell \wedge \psi_\Lambda \\
&\Leftrightarrow \langle \perp, \Sigma_\Lambda, \lambda g : \varrho. \lambda \pi. \mathbb{C}_\perp^T(e) \rangle \circ \langle \perp, \Sigma_\Lambda, \mathbb{C}_\perp^T(f) \rangle, \ell \wedge \psi_\Lambda \tag{Cor. 4} \\
&= \langle \perp, \Sigma_\Lambda, \omega [g \mapsto \langle \perp, \Sigma_\Lambda, f \rangle], \lambda \pi. \mathbb{C}_\perp^T(e) \rangle \circ \ell \wedge \psi_\Lambda \\
&\Leftrightarrow \langle \perp, \Sigma_\Lambda, \omega [g \mapsto \langle \perp, \Sigma_\Lambda, f \rangle], \mathbb{C}_\perp^T(\pi \to e) \rangle \circ \ell \wedge \psi_\Lambda \tag{Cor. 4} \\
&\Leftrightarrow \langle \perp, \Sigma_\Lambda, \mathbb{C}_\perp^T(\pi \to e)[g \mapsto f] \rangle \circ \ell \wedge \psi_\Lambda \tag{Lem. 15} \\
&= \langle \perp, \Sigma_\Lambda, \mathbb{C}_\perp^T((\pi \to e)[g \mapsto f]) \rangle \circ \ell \wedge \psi_\Lambda \tag{Lem. 14} \\
&= \langle \perp, \Sigma_\Lambda, \mathbb{C}_\perp^T((\pi \to e)[g \mapsto f] \bar{o}) \rangle \circ \varepsilon \wedge \psi_\Lambda
\end{align*}
$$
Case E-APP C. Then $e_1$ is of the form $((g : \varrho) \pi \to e) (\varrho \to d) \bar{o} // \Lambda$ and $e_2$ of the form $(\pi \to e) \bar{o} / g \varrho = \downarrow d // \Lambda$, assuming that $g$ does not occur freely in $d$ or in $\bar{o}$. Let $\Sigma'$ denote the cell context $\Sigma_{g\varrho=\downarrow d, \Lambda} = \Sigma_\Lambda \uplus [g \mapsto \langle \perp, \Sigma_\Lambda, \lambda\varrho. \forall g : \varrho. C_\perp^\top(\downarrow d) \rangle]$. It is easy to show that the stack $\ell = \langle \perp, \Sigma_\Lambda, C_\perp^\top(o_1) \rangle, \dots, \langle \perp, \Sigma_\Lambda, C_\perp^\top(o_n) \rangle$ is equivalent to the stack $\ell' = \langle \perp, \Sigma', C_\perp^\top(o_1) \rangle, \dots, \langle \perp, \Sigma', C_\perp^\top(o_n) \rangle$. Then we have

$$
\begin{align*}
& \langle \perp, \Sigma_\Lambda, C_\perp^\top(((g : \varrho) \pi \to e) (\varrho \to d) \bar{o}) \rangle \circ \varepsilon \wedge \psi_\Lambda \\
&= \langle \perp, \Sigma_\Lambda, C_\perp^\top((g : \varrho) \pi \to e) \rangle \circ \langle \perp, \Sigma_\Lambda, C_\perp^\top(\varrho \to d) \rangle, \ell \wedge \psi_\Lambda \tag{Cor. 4} \\
&\Leftrightarrow \langle \perp, \Sigma_\Lambda, \lambda g : \varrho. \lambda \pi. C_\perp^\top(e) \rangle \circ \langle \perp, \Sigma_\Lambda, \lambda \varrho. C_\perp^\top(d) \rangle, \ell \wedge \psi_\Lambda \\
&\Leftrightarrow \langle \perp, \Sigma_\Lambda, \lambda g : \varrho. \lambda \pi. C_\perp^\top(e) \rangle \circ \langle \perp, \Sigma_\Lambda, \lambda \varrho. \forall g : \varrho. C_\perp^\top(\downarrow d) \rangle, \ell \wedge \psi_\Lambda \tag{*} \\
&= \langle \perp, \Sigma', \lambda \pi. C_\perp^\top(e) \rangle \circ \ell \wedge \psi_\Lambda \\
&\Leftrightarrow \langle \perp, \Sigma', C_\perp^\top(\pi \to e) \rangle \circ \ell \wedge \psi_\Lambda \tag{Cor. 4} \\
&\Leftrightarrow \langle \perp, \Sigma', C_\perp^\top(\pi \to e) \rangle \circ \ell \wedge \langle \perp, \Sigma', \forall \varrho. C_\perp^\top(d) \rangle \circ \varepsilon \wedge \psi_\Lambda \tag{Lem. 7} \\
&\Leftrightarrow \langle \perp, \Sigma', C_\perp^\top(\pi \to e) \rangle \circ \ell' \wedge \langle \perp, \Sigma', \forall \varrho. C_\perp^\top(\downarrow d) \rangle \circ \varepsilon \wedge \psi_\Lambda \tag{$\ell \equiv \ell'$} \\
&= \langle \perp, \Sigma', C_\perp^\top(\pi \to e) \bar{o} \wedge \forall \varrho. C_\perp^\top(\downarrow d) \rangle \circ \varepsilon \wedge \psi_\Lambda \\
&= \langle \perp, \Sigma_\Lambda, \text{let } g \varrho = C_\perp^\top(\downarrow d) \text{ in } C_\perp^\top(\pi \to e) \bar{o} \wedge \forall \varrho. C_\perp^\top(\downarrow d) \rangle \circ \varepsilon \wedge \psi_\Lambda \\
&= \langle \perp, \Sigma_\Lambda, C_\perp^\top((\pi \to e) \bar{o} / g \varrho = \downarrow d) \rangle \circ \varepsilon \wedge \psi_\Lambda
\end{align*}
$$

On the step marked (*), we can safely introduce the universal quantifier over $g$, since this handler symbol does not occur in $C_\perp^\top(d)$.

Case E-VOID. Then $e_1$ is of the form $\square \to e // \Lambda$ and $e_2$ of the form $e // \Lambda$. We have $\langle \perp, \Sigma_\Lambda, C_\perp^\top(\square \to e) \rangle \circ \varepsilon \wedge \psi_\Lambda \Leftrightarrow \langle \perp, \Sigma_\Lambda, C_\perp^\top(e) \rangle \circ \varepsilon \wedge \psi_\Lambda$ by Corollary 4.

Case E-PROP. Then $e_1$ is of the form $\{\varphi\} e // \Lambda$, where the formula $\varphi$ is valid, and $e_2$ is of the form $e // \Lambda$. We obtain

$$
\begin{align*}
& \langle \perp, \Sigma_\Lambda, C_\perp^\top(\{\varphi\} e) \rangle \circ \varepsilon \wedge \psi_\Lambda \\
&= \langle \perp, \Sigma_\Lambda, (\varphi \to C_\perp^\top(e)) \wedge (\tau \to \neg \varphi \to \mathbf{0}) \rangle \circ \varepsilon \wedge \psi_\Lambda \\
&= (\varphi \to \langle \perp, \Sigma_\Lambda, C_\perp^\top(e) \rangle \circ \varepsilon) \wedge (\tau \to \neg \varphi \to \perp) \wedge \psi_\Lambda \\
&\Leftrightarrow (\varphi \to \langle \perp, \Sigma_\Lambda, C_\perp^\top(e) \rangle \circ \varepsilon) \wedge \varphi \wedge \psi_\Lambda \\
&\Rightarrow \langle \perp, \Sigma_\Lambda, C_\perp^\top(e) \rangle \circ \varepsilon \wedge \psi_\Lambda
\end{align*}
$$

Case E-Gc. Then $e_1$ is of the form $e / h \pi = d // \Lambda$, where $h$ does not occur in $e$, and $e_2$ is $e // \Lambda$. Let $\Sigma'$ stand for $\Sigma_{h\pi=d,\Lambda} = \Sigma_\Lambda \uplus [h \mapsto \langle \perp, \Sigma_\Lambda, \lambda \pi. \forall h : \pi. C_\perp^\top(d) \rangle]$. Then

$$
\begin{align*}
& \langle \perp, \Sigma_\Lambda, C_\perp^\top(e / h \pi = d) \rangle \circ \varepsilon \wedge \psi_\Lambda \\
&= \langle \perp, \Sigma_\Lambda, \text{let } h \pi = C_\perp^\top(d) \text{ in } C_\perp^\top(e) \wedge \forall \pi. C_\perp^\top(d) \rangle \circ \varepsilon \wedge \psi_\Lambda \\
&= \langle \perp, \Sigma', C_\perp^\top(e) \wedge \forall \pi. C_\perp^\top(d) \rangle \circ \varepsilon \wedge \psi_\Lambda \\
&= \langle \perp, \Sigma', C_\perp^\top(e) \rangle \circ \varepsilon \wedge \langle \perp, \Sigma', \forall \pi. C_\perp^\top(d) \rangle \circ \varepsilon \wedge \psi_\Lambda \\
&\Rightarrow \langle \perp, \Sigma', C_\perp^\top(e) \rangle \circ \varepsilon \wedge \psi_\Lambda \\
&\Leftrightarrow \langle \perp, \Sigma_\Lambda, C_\perp^\top(e) \rangle \circ \varepsilon \wedge \psi_\Lambda \tag{h does not occur in e}
\end{align*}
$$

Cases E-BBOX and E-WBOX are trivial.
The rest of the cases correspond to the use of primitive handlers. For example, let expression $e_1$ be of the form $if sko // Λ$. Then we have

$$ 
\begin{align*}
& \langle \perp, \Sigma_{\Lambda}, C_{\perp}^{\top}(if sko) \rangle \circ \varepsilon \wedge \psi_{\Lambda} \\
&= \langle \perp, \emptyset, \Psi_{if} \rangle \circ s, \langle \perp, \Sigma_{\Lambda}, C_{\perp}^{\top}(k) \rangle, \langle \perp, \Sigma_{\Lambda}, C_{\perp}^{\top}(o) \rangle \wedge \psi_{\Lambda} \\
&= \langle \perp, [\text{then} \mapsto \langle \perp, \Sigma_{\Lambda}, C_{\perp}^{\top}(k) \rangle, \text{else} \mapsto \langle \perp, \Sigma_{\Lambda}, C_{\perp}^{\top}(o) \rangle], \\
& \qquad (s \to \text{then}) \wedge (\neg s \to \text{else}) \rangle \circ \varepsilon \wedge \psi_{\Lambda} \\
&= (s \to \langle \perp, \Sigma_{\Lambda}, C_{\perp}^{\top}(k) \rangle \circ \varepsilon) \wedge (\neg s \to \langle \perp, \Sigma_{\Lambda}, C_{\perp}^{\top}(o) \rangle \circ \varepsilon) \wedge \psi_{\Lambda}
\end{align*}
$$

Depending on whether we progressed along the first or the second rule for if, the last formula entails either $\langle \perp, \Sigma_{\Lambda}, C_{\perp}^{\top}(k) \rangle \circ \varepsilon \wedge \psi_{\Lambda}$ or $\langle \perp, \Sigma_{\Lambda}, C_{\perp}^{\top}(o) \rangle \circ \varepsilon \wedge \psi_{\Lambda}$.

The applications of unTree and get are treated in the similar way. □

**Theorem 6 (Theorem 4).** For any correct COMA program $e_1$, either $e_1$ is halt, or $e_1 \rightarrow e_2$ for some program $e_2$.

*Proof.* Here we only consider the premise of the E-PROP rule, as well as the premises of the evaluation rules for the primitive handlers—the rest of the proof is straightforward. Just like in the proof of Theorem 3, we will use the fact that for any program $e // \Lambda$, the formula $\langle \perp, \Sigma_{\text{prim}}, C_{\perp}^{\top}(e // \Lambda) \rangle \circ \varepsilon$ is logically equivalent to $\langle \perp, \Sigma_{\Lambda}, C_{\perp}^{\top}(e) \rangle \circ \varepsilon \wedge \psi_{\Lambda}$. Then we can easily show that the premise of E-PROP, as well as the first premise of the evaluation rule for get, are logical consequences of the verification condition of $e_1$. Furthermore, the standard model for Booleans, integers, binary trees, and sequences, which we adopt for our semantics, guarantees that every ground Boolean term is either $\top$ or $\perp$, every ground term of type tree $\tau$ is either a Node or an Empty, every sequence contains an element for every valid index, etc. □