{'fraction_non_alphanumeric': 0.04125583132802252, 'fraction_numerical': 0.004439193474124975, 'mean_word_length': 4.193178742217811, 'pattern_counts': {'":': 0, '<': 1, '<?xml version=': 0, '>': 2, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 26, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
A Higher-Order Logic for Concurrent Termination-Preserving Refinement

Compiler correctness proofs for higher-order concurrent languages are difficult: they involve establishing a termination-preserving refinement between a concurrent high-level source language and an implementation that uses low-level shared memory primitives. However, existing logics for proving concurrent refinement either neglect properties such as termination, or only handle first-order state. In this paper, we address these limitations by extending Iris, a recent higher-order concurrent separation logic, with support for reasoning about termination-preserving refinements. To demonstrate the power of these extensions, we prove the correctness of an efficient implementation of a higher-order, session-typed language. To our knowledge, this is the first program logic capable of giving a compiler correctness proof for such a language. The soundness of our extensions and our compiler correctness proof have been mechanized in Coq.


Introduction
Parallelism and concurrency impose great challenges on both programmers and compilers. In order to make compiled code more efficient and help programmers avoid errors, languages can provide type systems or other features to constrain the structure of programs and provide useful guarantees. The design of these kinds of concurrent languages is an active area of research. However, it is frequently difficult to prove that efficient compilers for these languages are correct, and that important properties of the source-level language are preserved under compilation.
For example, in work on session types [19,45,17,10,42], processes communicate by sending messages over channels. These channels are given a type which describes the kind of data sent over the channel, as well as the order in which each process sends and receives messages. Often, the type system in these languages ensures the absence of undesired behaviors like races and deadlocks; for instance, two threads cannot both be trying to send a message on the same channel simultaneously.
Besides preventing errors, the invariants enforced by session types also permit these language to be compiled efficiently to a shared-memory target language [43]. For example, because only one thread can be sending a message on a given channel at a time, channels can be implemented without performing locking to send and receive messages. It is particularly important to prove that such an implementation does not introduce races or deadlocks, since this would destroy the very properties that make certain session-typed languages so interesting.
In this paper, we develop a higher-order program logic for proving the correctness of such concurrent language implementations, in a way that ensures that termination is preserved. We have used this program logic to give a machinechecked proof of correctness for a lock-free implementation of a higher-order session-typed language, i.e., a language in which closures and channels can be sent over channels. To our knowledge, this is the first such proof of its kind.
As we describe below, previously developed program logics cannot be used to obtain these kinds of correctness results due to various limitations. In the remainder of the introduction, we will explain why it is so hard to prove refinements between higher-order, concurrent languages. To this end, we first have to provide some background.
Refinement for concurrent languages. To show that a compiler is correct, one typically proves that if a source expression E is well-typed, its translation E refines E. In the sequential setting, this notion of refinement is easy to define 3 : (1) if the target program E terminates in some value v, we expect E to also have an execution that terminates with value v, and (2) if E diverges, then E should also have a diverging execution.
In the concurrent setting, however, we need to change this definition. In particular, the condition (2) concerning diverging executions is too weak. To see why, consider the following program, where x initially contains 0: while (*x == 0) {} || *x = 1; Here, || represents parallel composition of two threads. In every execution where the thread on the right eventually gets to run, this program will terminate. However, the program does have a diverging execution in which only the left thread runs: because x remains 0, the left thread continues to loop. Such executions are "unrealistic" in the sense that generally, we rely on schedulers to be fair and not let a thread starve. As a consequence, for purposes of compiler correctness, we do not want to consider these "unrealistic" executions which only diverge because the scheduler never lets a thread run. Formally, an infinite execution is said to be fair [27] if every thread which does not terminate in a value takes infinitely many steps. 4 In the definition of refinement above, we change (2) to demand that if E has a fair diverging execution, then E also has a fair diverging execution. We impose no such requirement about unfair diverging executions. This leads us to fair termination-preserving refinement.
Logics for proving refinement. To prove our compiler correct, we need to reason about the concurrent execution and (non)termination of the source and target programs. Rather than reason directly about all possible executions of these programs, we prefer to use a concurrent program logic in order to re-use ideas found in rely-guarantee reasoning [21] and concurrent separation logic [34]. However, although a number of concurrency logics have recently been developed for reasoning about termination and refinements, they cannot be used to prove our compiler correctness result because they either: are restricted to first-order state [18,36,29,30,28], -only deal with termination, not refinement [18,36], or handle a weaker form of refinement that is not fair termination-preserving [40,29,30].
Although the limitations are different in each of the above papers, let us focus on the approach by Turon et al.
[40] since we will build on it. That paper establishes a termination-insensitive form of refinement, i.e., a diverging program refines every program. Refinement is proven in a higher-order concurrent separation logic which, in addition to the usual points-to assertions l ֒→ v, also provides assertions about the source language's state. For instance, the assertion 5 source(i, E) says thread i in the source language's execution is running expression E. A thread which "owns" this resource is allowed to modify the state of the source program by simulating steps of the execution of E. Then, we can prove that e refines E by showing: {source(i, E)} e {v. source(i, v)} As usual, the triple enforces that the post-condition holds on termination of e. Concretely for the triple above, the soundness theorem for the logic implies that if target expression e terminates with a value v, then there is an execution of source expression E that also terminates with value v. However, the Hoare triple above only expresses partial correctness. That means if e does not terminate, then the triple above is trivial, and so these triples can only be used to prove termination-insensitive refinements.
Ideally, one would like to overcome this limitation by adapting ideas from logics that deal with termination for first-order state. Notably, Liang et al. [28] have recently developed a logic for establishing fair refinements (as defined above).
However, there is a serious difficulty in trying to adapt these ideas. Semantic models of concurrency logics for higher-order state usually involve stepindexing [3,7]. In step-indexed logics, the validity of Hoare triples is restricted to program executions of arbitrary but finite length. How can we use these to reason about fairness, a property which is inherently about infinite executions?
In this paper, we show how to overcome this difficulty: the key insight is that when the source language has only bounded non-determinism, step-indexed Hoare triples are actually sufficient to establish properties of infinite program executions. Using this observation, we extend Iris [23,22], a recent higherorder concurrent separation logic, to support reasoning about fair terminationpreserving refinement. The soundness of our extensions to Iris and our case studies have been verified in Coq.
Overview. We start by introducing the case study that we will focus on in this paper: a session-typed source language, a compiler into an ML-like language, and the compiler's correctness property -fair, termination-preserving refinement ( §2). Then we present our higher-order concurrent separation logic for establishing said refinement ( §3). We follow on by explaining the key changes to Iris that were necessary to perform this kind of reasoning ( §4). We then use the extended logic to prove the correctness of the compiler for our session-typed language ( §5). Finally, we conclude by describing connections to related work and limitations of our approach that we hope to address in future work ( §6).

Session-Typed Language and Compiler
This section describes the case study that we chose to demonstrate our logic: a concurrent message-passing language and a type system establishing safety and race-freedom for this language. On top of that, we explain how to implement the message-passing primitives in terms of shared-memory concurrency, i.e., we define a compiler translating the source language into an ML-like target language. Finally, we discuss the desired correctness statement for this compiler.

Source Language
The source language for our compiler is a simplified version of the language described in Gay and Vasconcelos [17]. The syntax and semantics are given in Figure 1. It is a functional language extended with primitives for message passing and a command fork{E} for creating threads. The semantics is defined by specifying a reduction relation for a single thread, which is then lifted to a concurrent semantics on thread-pools in which at each step a thread is selected non-deterministically to take the next step.
Threads can communicate asynchronously with each other by sending messages over channels. For example, consider the following program (which will be a running example of the paper): let (x, y) = newch in fork{send(x, 42)}; let ( , v) = recv(y) in v The command newch creates a new channel and returns two end-points (bound to x and y in the example). An end-point consists of a channel id c and a side s (either left or right), and is written as c s . Each channel is a pair of buffers (b → , b ← ), which are lists of messages. Buffer b → stores messages traveling left-to-right (from x to y, in the example above), and b ← is for right-to-left messages, as shown in the visualization in Figure 1.
A thread can then use send(c s , V ) to send a value V along the channel c, with the side s specifying which buffer is used to store the message. For instance, when s is left, it inserts the value at the end of the first buffer (SendLeft). This value will then later be taken by a thread receiving on the right side (RecvRight). Alternatively, if the buffer is empty when receiving, recv takes an "idle" step and tries again (RecvRightIdle). (The reason send and recv return the endpoint again will become clear when we explain the type system.) In the example above, after creating a new channel, the initial thread forks off a child which will send 42 from the left end-point, x. Meanwhile, the parent thread tries to receive from the right end-point y, and returns the message it gets. If the parent thread does this recv before the child has done its send, there will be no message and the parent thread will take an idle step. Otherwise, the receiver will see the message and the program will evaluate to 42.

Session Type System
A type system for this language is shown in Figure 1. This is a simplified version of the type system given in Gay and Vasconcelos [17]. 6 In addition to base types Int and Unit, we have pair types τ 1 ⊗ τ 2 , function types τ 1 ⊸ τ 2 , and session types S. Session types are used to type the end-points of a channel. These types describe a kind of protocol specifying what types of data will flow over the channel, and in what order messages are sent. Notice that this type system is higher-order in the sense that both closures and channel end-points are first-class values and can, in particular, be sent over channels.
Session types. The possible session types are specified by the grammar in Figure 1. If an end-point has the session type !τ. S, this means that the next use of this end-point must be to send a value of type τ (Send). Afterward, the endpoint that is returned by the send will have type S. Dually, ?τ. S says that the end-point can be used in a receive (Recv), in which case the message read will have type τ , and the returned end-point will have type S. Notice that this is the same end-point that was passed to the command, but at a different type. The type of the end-point evolves as messages are sent and received, always representing the current state of the protocol. Finally, end is a session type for an end-point on which no further messages will be sent or received.
When calling newch to create a new channel, it is important that the types of the two end-points match: whenever one side sends a message of type τ , the other side should be expecting to receive a message of the same type. This relation is called duality. Given a session type S, its dual S is the result of swapping sends and receives in S. In our example (1), the end-point x is used to send a single integer, so it can be given the type !Int. end. Conversely, y receives a single integer, so it has the dual type !Int. end = ?Int. end.
Affinity. The type system of the source language is affine, which means that a variable in the context can be used at most once. This can be seen, e.g., in the rule Fork: the forked-off thread E f and the local continuation E are typed using the two disjoint contexts Γ 1 and Γ 2 , respectively.
One consequence of affinity is that after using an end-point to send or receive, the variable passed to send/recv has been "used up" and cannot be used anymore. Instead, the program has to use the channel returned from send/recv, which has the new "evolved" type for the end-point.
The type system given here ensures safety and race-freedom. However, it does not guarantee termination. We discuss alternative type systems guaranteeing different properties in the conclusion.

Compilation
We now describe a simple translation from this session-typed source language to a MiniML language with references and a forking primitive like the one in the source language. We omit the details of the MiniML syntax and semantics as they are standard.
Our translation needs to handle essentially one feature: the implementation of channel communication in terms of shared memory references.
The code for the implementation of the channel primitives is shown in Figure 2. We write E for the translation in which we replace the primitives of the source language with the corresponding implementations. Concretely, applying the translation to our running example program we get: Each channel is implemented as a linked list which represents both buffers. Nodes in this list are pairs (l, v), where l is a reference to the (optional) next node, and v is the message that was sent. Why is it safe to use just one list? Duality in the session types guarantees that if a thread is sending from one end-point, no thread can at the same time be sending a message on the other end-point. This ensures that at least one of the two buffers in a channel is always empty. Hence we just need one list to represent both buffers.
The implementation of newch, given by heapNewch, creates a new empty linked list by allocating a new reference l which initially contains none. The function heapSend implements send by appending a node to the end (l ′ ) of the list, and returning the new end. Meanwhile, for recv, heapRecv takes an end-point l and waits in a loop until it finds that the end-point contains a node. Fig. 2. Implementation of message passing primitives.

Refinement
Having given the implementation, let us now clarify what it means for the compiler to be correct. Intuitively, we want to show that if we take a well-typed source expression E, all the behaviors of its translation E are also possible behaviors of E. We say that E refines E.
Before we come to the formal definition of refinement, we need to answer the question: which behaviors do we consider equivalent? In our case, the only observation that can be made about a whole program is its return value, so classifying "behaviors" amounts to relating return values. Formally speaking: For integer and unit values, we expect them to be exactly equal; similarly, pairs are the same if their components are. Coming to locations/end-points and closures, we do not consider them to be interpretable by the user looking at the result of a closed program. So, we just consider all closures to be equivalent, and all heap locations to relate to all channel end-points. Of course, the proof of compiler correctness will use a more fine-grained logical relation between source and target values.
Based on this notion of equivalent observations, we define what it means for a MiniML program e to refine a source program E, written e ⊑ E. When executing from an initial "empty" state ∅, the following conditions must hold: 1. If ([e], ∅) → * ([e 1 , ... , e n ], σ) then no e i is stuck in state σ.
In other words: the target program does not reach a stuck state.
there is an execution of ([E], ∅) in which some thread gets stuck. That is, if all threads of the target program terminate with a value, then either all threads of the source program terminate in some execution and the return values of the first (main) source thread and target thread are equivalent; or the source program can get stuck.
3. If ([e], ∅) has a fair diverging execution, then ([E], ∅) also has a fair diverging execution. Recall that an infinite execution is fair if every non-terminating thread takes infinitely many steps. This last condition makes the refinement a fair, termination-preserving refinement.
To understand why we have emphasized the importance of fair terminationpreservation, suppose we had miscompiled our running example as: That is, we removed the sender thread. We consider this to be an incorrect compilation; i.e., this program should not be considered a refinement of the source program. But imagine that we removed the word "fair" from condition (3) above: then this bad target program would be considered a refinement of the source. How is that? The program does not get stuck, so it satisfies condition (1). Condition (2) holds vacuously since the target program will never terminate; it will loop in heapRecv y, forever waiting for a message. Finally, to satisfy condition (3), we have to exhibit a diverging execution in the source program. Without the fairness constraint, we can pick the (unfair) execution in which the sender source thread never gets to run.
Notice that this unfair execution is very much like the example we gave in the introduction, where a thread waited forever for another one to perform a change in the shared state.
We consider such unfair executions to be unrealistic [27]; they should not give license to a compiler to entirely remove a thread from the compiled program. That's why our notion of refinement restricts condition (3) to fair executions, i.e., executions in which all non-terminating threads take infinitely many steps.
Compiler correctness. We are now equipped to formally express the correctness statement of our compiler: Theorem 1. For every well-typed source program E, we have that: We prove this theorem in §5. In the intervening sections, we first develop and explain a logic to help carry out this proof.

A Logic for Proving Refinement
Proving Theorem 1 is a challenging exercise. Both the source and the target program are written in a concurrent language with higher-order state, which is always a difficult combination to reason about. Moreover, the invariant relating the channels and buffers to their implementation as linked lists is non-trivial and relies on well-typedness of the source program.
The contribution of this paper is to provide a logic powerful enough to prove theorems like Theorem 1. In this section, we will give the reader an impression of both the logic and the proof by working through a proof of one concrete instance of our general result: we will prove that the translation of our running example is in fact a refinement of its source.

Refinement as a Hoare Logic
Our logic is an extension of Iris [23, 22], a concurrent higher-order separation logic. We use the ideas presented by Turon et al. [40] to extend this (unary) Hoare logic with reasoning principles for refinement. Finally, we add some further extensions which become necessary due to the termination-preserving nature of our refinement. We will highlight these extensions as we go.
The following grammar covers the assertions from our logic that we will need: 7 Many of these assertions are standard in separation logics, and our example proof will illustrate the non-standard ones.
Recalling the example and its translation,we want to prove: or, for short, e ex ⊑ E ex . Following Ht-refine (Figure 3), it is enough to prove In other words, we "just" prove a Hoare triple for e ex (the MiniML program). In order to obtain a refinement from a Hoare proof, we equip our logic with assertions talking about the source program E. The assertion source(i, E, d) states that source-level thread i is about to execute E, and we have delay d left. (We will come back to delays shortly.) The assertion c ֒→ s (b → , b ← ) says that sourcelevel channel c currently has buffer contents (b → , b ← ). As usual in separation logic, both of these assertions furthermore assert exclusive ownership of their thread or channel. For example, in the case of c ֒→ s (b → , b ← ), this means that no other thread can access the channel and we are free to mutate it (i.e., send or receive messages) -we will see later how the logic allows threads to share these resources. Put together, these two assertions let us control the complete state of the source program's execution.
So far, we have not described anything new. However, to establish terminationpreserving refinement, we have to add two features to this logic: step shifts and linear assertions.
Step Shift Rules: (all d and d ′ must be ≤ some fixed upper-bound D) (Symmetric rules and side-condition on d ′ omitted.) Basic Hoare Triples: Refinement Rule: Step shifts. The rules given in Figure 3 let us manipulate the state of the source program's execution by taking steps in the source program. Such steps are expressed using step shifts ⇛ ⇛. Every step shift corresponds to one rule in the operational semantics ( Figure 1). For example, src-newch expresses that if we have source(i, K[newch], d) (which means that the source is about to create a new channel), we can "execute" that newch and obtain some fresh channel c and ownership of the channel (c ֒→ s ([], [])). We also obtain source(i, K[c], d ′ ), so we can go on executing the source thread. Crucially, having P ⇛ ⇛ Q shows that in going from P to Q, the source has taken a step. We need to force the source to take steps because the refinement we show is termination-preserving. If a proof could just decide not to ever step the source program, we could end up with a MiniML program e diverging, while the corresponding source program E cannot actually diverge. That would make Ht-refine unsound. So, to avoid this, all rules that take a step in the MiniML program ( Figure 3) force us to also take a step shift.
A strict implementation of this idea requires a lock-step execution of source and target program. This is too restrictive. For that reason, the source assertion does not just record the state of the source thread, but also a delay d. Decrementing the delay counts as taking a step in the source (src-delay). When we take an actual source step, we get to reset the delay to some new d ′ -so long as d ′ is less than or equal to some fixed upper bound D that we use throughout the proof. There are also rules that allow executing multiple source steps when taking just a single step in the target program; we omit these rules for brevity. For the remainder of this proof, we will also gloss over the bookkeeping for the delay and just write source(i, e).
The assertion Stopped expresses that a source thread can no longer take steps. As expected, this happens when the source thread reaches a value (src-stopped).
Linearity. There is one last ingredient we have to explain before we start the actual verification: linearity. Assertions in our logic are generally linear, which means they cannot be "thrown away", i.e., P * Q ⊢ P does not hold generically in P and Q. As a consequence, assertions represent not only the right to perform certain actions (like modifying memory), but also the obligation to keep performing steps in the source program. This ensures that we do not "lose track" of a source thread and stop performing step shifts justifying its continued execution.
The modality A(P ) says that we have a proof of P , and that this is an affine proof -so there are no obligations encoded in this assertion, and we can throw it away. Some rules are restricted to affine assertions, e.g., rules for framing around a Hoare triple or a step shift ( Figure 3; the rule Ht-csq will be explained later). Again, this affine requirement ensures that we do not "smuggle" a source thread around the obligation to perform steps in the source. All the base assertions, with the exception of source(i, e), are affine.
Coming back to the Hoare triple (2) above that we have to prove, the precondition source(i, E ex ) expresses that we start out with a source program executing E ex (and not owning any channels), and we somehow have to take steps in the source program to end up with source(i, V ) such that V is "equivalent" (in the sense defined in §2.4) to the return value of the target program. Intuitively, because we can only manipulate source by taking steps in the source program, and because we end up stepping from source(i, E ex ) to "the same" return value as the one obtained from e, proving the Hoare triple actually establishes a refinement between the two programs. Furthermore, since source is linear and we perform a step shift at every step of the MiniML program, the refinement holds even for diverging executions.

Proof of the Example
The rest of this section will present in great detail the proof of our example (2). The rough structure of this proof goes as follows: after a small introduction covering the allocation of the channel, we will motivate the need for state-transition systems (STS), a structured way of controlling the interaction between cooperating threads. We will define the STS used for the example and decompose the remainder of the proof into two pieces: one covering the sending thread and one for the receiving thread.
Getting started. The first statement in both source and target program is the allocation of a channel. The following Hoare triple that's easily derived from ml-alloc summarizes the action of heapNewch: It allocates a channel in both programs.
Let us pause a moment to expand on that post-condition. On the source side, we have a channel c with both buffers being empty; on the target side we have a location l representing the empty buffer with none. The return value x is a pair with both components being l. Finally, the source thread changed from K[newch] in the pre-condition to K[(c left , c right )], meaning that the newch has been executed and the context can now go on with its evaluation based on the pair (c left , c right ). We apply this triple for heapNewch with the appropriate evaluation context K for the source program, and the post-condition of (3) becomes our new context of current assertions. Next, we reduce the let on both sides, so we end up with where e comm (c) fork{send(c left , 42)}; let ( , v) = recv(c right ) in v and the remaining MiniML code is fork{heapSend l 42}; let ( , v) = heapRecv l in v (In the following, we will perform these pure reduction steps and the substitutions implicitly.)  As we can see, both programs are doing a fork to concurrently send and receive messages on the same channel. Usually, this would be ruled out by the exclusive nature of ownership in separation logic. To enable sharing, the logic provides a notion of protocols coordinating the interaction of multiple threads on the same shared state. The protocol governs ownership of both l (in the target) and c (in the source), and describes which thread can perform which actions on this shared state.
State-transition systems. A structured way to describe protocols is the use of state-transition systems (STS), following the ideas of Turon et al. [40]. An STS S consists of a directed graph with the nodes denoting states and the arrows denoting transitions.
The STS for our example is given in Figure 4. It describes the interaction of our two threads over the shared buffer happening in three phases. In the beginning, the buffer is empty (init). Then the message is sent by the forkedoff sending thread (sent). Finally, the message is received by the main thread (received).
The STS also contains two tokens. Tokens are used to represent actions that only particular threads can perform. In our example, the state sent requires the token [S]. The STS enforces that, in order to step from init to sent, a thread must provide (and give up) ownership of [S]. This is called the law of token preservation [40]: Because sent contains more tokens than init, the missing tokens have to be provided by the thread performing the transition. Similarly, [R] is needed to transition to the final state received.
To tie the abstract state of the STS to the rest of the verification, every STS comes with an interpretation ϕ. For every state, it defines an affine assertion that has to hold at that state. In our case, we require the buffer to be initially empty, and to contain 42 in state sent. Once we reach the final state, the programs no longer perform any action on their respective buffers, so we stop keeping track.
We need a way to track the state of the STS in our proof. To this end, the assertion StsSt(s, T ) states that the STS is at least in state s, and that we own tokens T . We cannot know the exact current state of the STS because other threads may have performed further transitions in the mean time. The proof rules for STSs can be found in the appendix; in the following, we will keep the reasoning about the STS on an intuitive level to smooth the exposition.
Plan for finishing the proof. Let us now come back to our example program. We already described the STS we are going to use for the verification (Figure 4). The next step in the proof is thus to initialize said STS.
Remember our current context is (4). When allocating an STS, we get to pick its initial state -that would be init, of course. We have to provide ϕ(init) to initialize the STS, so we give up ownership of l and c. In exchange, we obtain StsSt and the tokens. Our context is now The next command executed in both programs is fork. We are thus going to apply ml-fork and prove the step shift using src-fork. The two remaining premises of ml-fork are the following two Hoare triples: Showing these will complete the proof. The post-condition Stopped of (6) is mandated by ml-fork; we will discuss it when verifying that Hoare triple. Note that we are splitting the StsSt to hand the two tokens that we own to two different threads.
Verifying the sender. To prove the sending Hoare triple (6), the context we have available is StsSt(init, [S]) * source(j, send(c left , 42)), and the code we wish to verify is (unfolding the definition of heapSend, and performing some pure reductions): The allocation is easily handled with ml-alloc, and it turns out we don't even need to remember anything about the returned l new . The next step is the core of this proof: showing that we can change the value stored in l. Notice that we do not own l ֒→ ; the STS "owns" l as part of its interpretation. So we will open the STS to get access to l.
Looking at Figure 4, we can see that doing the transition from init to sent requires the token [S], which we own -as a consequence, nobody else could perform this transition. It follows that the STS is currently in state init. We obtain ϕ(init), so that we can apply ml-store with src-send-left, yielding To finish up accessing the STS, we have to pick a new state and show that we actually possess the tokens to move to said state. In our case, we cannot pick received, since we do not own the token [R] necessary for that step. Instead, we will pick sent and give up our token. This means we have to establish ϕ(sent). Doing so consumes most of our context (8), leaving only source(j, c left ). What remains to be done? We have to establish the post-condition of our triple (6), which is Stopped. By src-stopped, this immediately follows from the fact that we reduced the source thread to c left , which is a value.
Notice that this last step was important: We showed that when the MiniML thread terminates, so does the source thread. The original fork rule for Iris allows picking any post-condition for the forked-off thread, because nothing happens any more with this thread once it terminates. However, we wish to establish that if all MiniML threads terminate, then so do all source threads -and for this reason, ml-fork forces us to prove Stopped, which asserts that all the threads we keep track of have reduced to a value. This finishes the proof of the sender.
Verifying the receiver. The next (and last) step in establishing the refinement (2) is to prove the Hoare triple for the receiving thread (7). This is the target code to verify: Since heapRecv is a recursive function, we use ml-rec, which says that we can assume that recursive occurrences of heapRecv have already been proven correct. It may be surprising to see this rule -after all, rules like ml-rec are usually justified by saying that all we do is partial correctness. Notice, however, that we are not showing that E ex terminates. All we show is that, if E ex diverges, then so does e ex . That is, we are establishing termination-preservation, not termination.
In continuing the proof, we thus get to assume correctness of the recursive call. Our current context is and the code we are verifying is with post-condition ( , n). n = 42 * source(j, 42). The first command of this program is !l. To access l, we have to again open the STS. Since we own [R], we can rule out being in state received. We perform a case distinction over the remaining two states.
We use ml-load with src-recv-right-miss. Notice how we use c ֒→ s ([], []) to justify performing an "idle" step in the source. This is crucial -after all, we are potentially looping indefinitely in the target, reading l over and over; we have to exhibit a corresponding diverging execution in the source. Since we did not change any state, we close the invariant again in the init state. Next, the program executes the none arm of the match: heapRecv l.
Here, we use our assumption that the recursive call is correct to finish the proof.
-Otherwise, the current state is sent, and we obtain l ֒→ some ( , 42) * c ֒→ s ([42], []). We use ml-load with src-recv-right-hit; this time we know that the recv in the source will succeed. We also know that we are loading ( , 42) from l. We pick received as the next state (giving up our STS token), and trivially establish ϕ(received). We can now throw away ownership of l and c as well as StsSt(received) since we no longer need them -we can do this because all these assertions are affine. All that remains is the source thread: Next, the target program will execute the some branch of the match. To finish, we need to justify the post-condition: ( , n). n = 42 * source(j, 42). We already established that the second component of the value loaded from l is 42, and the source thread is easily reduced to 42 as well.
This finishes the proof of (7) and therefore of (2): we proved that e ex ⊑ E ex .

Soundness of the Logic
We have seen how to use our logic to establish a refinement for a particular simple instance of our translation. We now need to show that this logic is sound. As already mentioned, our logic is an extension of Iris, so we need to adapt the soundness proof of Iris [22]. The two extensions that were described in §3.1 are: 1. We add a notion of a step shift, which is used to simulate source program threads. 2. We move from an affine logic to a linear logic. This is needed to capture the idea that some resources (like source) represent obligations that cannot be thrown away.
In this section we describe how we adapt the semantic model of Iris to handle these changes. Although our extensions sound simple, the modification of the model requires some care. Many of the features we used in §3, such as STSs [23] and reasoning about the source language, are derived constructions that are not "baked-in" to the logic. As we change the model, we need to ensure that all of these features can still be encoded. We also strive to keep our extensions as general as possible so as to not unnecessarily restrict the flexibility of Iris.
Brief review of the Iris model. We start by recalling some aspects of the Iris model [22] that we modify in our extensions. A key concept is the notion of a resource. Resources describe the physical state of the program as well as additional ghost state that is added for the purpose of verification and used, e.g., to interpret STSs or the assertions talking about source programs. Resources are instances of a partial commutative monoid-like algebraic structure; in particular, two resources a, b can be composed to a · b. This operation is used to combine resources held by different threads. When the composition a · b is defined, the elements a and b are said to be compatible. Iris always ensures that the resources held by different threads are compatible. This guarantees that, e.g., different threads cannot own the same channel or the same STS token. The operation also gives rise to a pre-order on resources, defined as a 1 a 2 ∃a 3 . a 1 · a 3 = a 2 , i.e., a 1 is included in a 2 if the former can be extended to the latter by adding some additional resource a 3 .
Ideally, we would just interpret an assertion P as a set of resources. For technical reasons (that we will mostly gloss over), Iris needs an additional component: the step-index n. An assertion is thus interpreted as a set of pairs (n, a) of step-indices and resources. We write n, a |= P to indicate that (n, a) ∈ P , and read this as saying that a satisfies P for n steps of the target program's execution.
Iris furthermore demands that assertions (interpreted as sets) satisfy two closure properties: They must be closed under larger resources and smaller stepindices. Formally: 1. If n, a |= P and a a ′ , then n, a ′ |= P . 2. If n, a |= P and n ′ ≤ n, then n ′ , a |= P .
The first point above makes Iris an affine as opposed to a linear logic: we can always "add-on" more resources and continue to satisfy an assertion. Put differently, there is no way to state an upper bound on our resources. The second point says that if P holds for n steps, then it also holds for fewer than n steps.
To give a model to assertions like l ֒→ v, we need a function HeapRes(l, v) describing, as a resource, a heap which maps location l to v. We then define: Notice the use of , ensuring that the closure property (1) holds.
Equipping Iris with linear assertions. In order to move to a linear setting with minimal disruption to the existing features of Iris, we replace the judgment n, a |= P with n, a, b |= P . That is, assertions are now sets of triples: a stepindex and two resources. The downward closure condition on n and the upward closure condition on a still apply, but we do not impose such a condition on b: this second resource will represent the "linear piece" of an assertion. Crucially, whereas affine assertions like l ֒→ v continue to "live" in the a piece, the linear source resides in b: where ε is the unit of the monoid. We assume SourceRes(i, E, d) to define, as a resource, a source thread i executing E with d delay steps left.
As we can see, source describes the exact linear resources b that we own, whereas ֒→ merely states a lower bound on the affine resources a (due to the upwards closure on a). Notice that a and b are both elements of the same set of resources; it is just their treatment in the closure properties of assertions which makes one affine and the other linear. Because there is no upward closure condition on the second monoid element, the resulting logic is not affine: if n, a, b |= P * Q, then it is not necessarily the case that n, a, b |= P .
We define the affine modality by: This says that in addition to satisfying P , b should equal the unit of the monoid. That is, the linear part is "empty"; there are no obligations encoded in P . That makes it sound to throw away P or to frame it. The advantage of this "two world" model is that it does not require us to change many of the encodings already present in Iris, like STSs.
Step Shifts. We are now ready to explain the ideas behind the step shift. Remember the goal here is to account for the steps taken in the source program, in a way that we can prove refinements by proving Hoare triples (Ht-refine). This is subtle because by the definition of refinement ( §2.4), we need to make statements even about infinite executions, i.e., executions that never have to satisfy the post-condition.
The key idea is to equip the resources of Iris with a relation that represents a notion of taking a (resource) step. We write a b, and say that a steps to b. We will then pick the resources in such a way as to represent the status of a source program, 8 and we define the resource step to be taking a step in the source program. All the other components of the resource, like STSs, will not be changed by resource steps.
Recall that the resources owned by different threads always need to be compatible. To ensure this, we define a relation that performs a step while maintaining compatibility with the resources owned by other threads. Formally, a frame-preserving step-update a, b The intuition is that, if a thread owns some resources a and b, that restricts the ownership of other threads to frames c that are compatible with a and b. Since a ′ and b ′ are also compatible with the frame, the step is guaranteed not to interfere with resources owned by other threads.
These frame-preserving step-updates are reflected into the logic through the step shift assertions: P ⇛ ⇛ Q holds if, whenever some resources satisfy P , it is possible to perform a frame-preserving step-update to resources satisfying Q.
We then connect Hoare triples to these resource steps. To this end, we change the definition of Hoare triples so that whenever a target thread takes a step, we have to also take a step on our resources. This gives rise to the proof rules in Figure 3, which force the user of the logic to perform a step shift alongside every step of the MiniML program. We also enforce that forked-off threads must have a post-condition of Stopped, ensuring that target language threads cannot stop executing while source language threads are still running.
Soundness of the refinement. Having extended the definition of Hoare triples in this way, we can prove our refinement theorem. Recall that the definition of refinement had three parts. For each of these parts, we proved an adequacy theorem for our extensions relating Hoare triples to properties of program executions. These theorems are parameterized by the kind of resource picked by the user, and in particular the kind of resource step. Below, we show these theorems specialized to the case where resource steps correspond to source language steps.
The first refinement condition, which says that the target program must not get stuck, follows from a "safety" theorem that was already present in the original Iris: ... , e n ], σ), then each e i is either a value or it can take a step in state σ.
The second refinement condition says that if the execution of e terminates, then there should be a related terminating execution in the source. Remember that the definition of the Hoare triple requires us to take a step in the source whenever the target steps (modulo a finite number of delays). Hence a proof of such a triple must have "built-up" the desired source execution: Here, we are already making crucial use of both linearity of source and the fact that forked-off threads must have post-condition Stopped: if it were not for these requirements, even when all target threads terminated with a value v i , we could not rule out the existence of source threads that can go on executing.
Finally, we come to the third condition, which says fair diverging executions of the target should correspond to fair diverging executions of the source: , ∅) has a diverging execution, then ([E], ∅) has a diverging execution as well. Moreover, if the diverging target execution is fair, then the source execution is too. This is the hardest part of the soundness proof. We would like to start by arguing that, just as for the finite case, if the target program took an infinite number of steps, then the proof of the refinement triple must give a corresponding infinite number of steps in the source program. Unfortunately, this argument is not so simple because of step-indexing.
In Iris, Hoare triples are themselves step-indexed sets. We write n |= {P } e {Q} to say that the triple holds at step-index n. Then, when we say we have proved a Hoare triple, we mean the triple holds for all step-indices n and all resources satisfying the precondition. As is usual with step-indexing, when a triple {P } e {Q} holds for step-index n, that means when the precondition is satisfied, execution of e is safe for up-to n steps, and if it terminates within those n steps, the postcondition holds. In our case, it also means that each step of the target program gives a step of the source program, for up to n target steps. This restriction to only hold "up to n steps" arises due to the way Hoare triples are defined in the model: when proving the Hoare triple at step-index n, if e steps to e ′ , we are only required to show (n − 1) |= {P ′ } e ′ {Q} for some P ′ .
The restriction to a finite number of steps did not bother us for Lemma 2 and Lemma 3. Since they only deal with finite executions, and the Hoare triple holds for all starting indices n, we can simply pick n to be greater than the finite execution we are considering. But we cannot do this when we want to prove something about a diverging execution of the target. Whatever n we start with, it is not big enough to get the infinite source execution we need.
Bounded non-determinism, infinite executions, and step-indexing. Our insight is that when the source language has only bounded non-determinism, we can set up a more careful inductive argument. By bounded non-determinism, we mean that each configuration ([E , ...], Σ) only has finitely many possible successor configurations. The key result is the following quantifier inversion lemma: Lemma 5. Let R be a step-indexed predicate on a finite set X. Then: Proof. By assumption, for each n, there exists x n ∈ X such that n |= R(x n ). Since X is finite, by the pigeon-hole principle, there must be some x ∈ X such that m |= R(x) for infinitely many values of m. Now, given arbitrary n, this means there exists m > n such that m |= R(x). Since step-indexed predicates are downward-closed, n |= R(x). Hence ∀n. n |= R(x).
Ignoring delay steps for the moment, we apply this lemma to our setting to get: Lemma 6. Suppose e steps to e ′ and ∀n. ∃P n . n |= {source(i, E) * P n } e {Q}. Then, ∃E ′ such that E steps to E ′ and ∀n. ∃P ′ n . n |= {source(i, E ′ ) * P ′ n } e ′ {Q}. Proof. Let X by the set of E ′ that E can step to, which we know to be finite. 9 Consider the step-indexed predicate R on X defined by n |= R( . By assumption, for each n > 0, n |= {source(i, E) * P n } e {Q} for some P n . The definition of Hoare triples implies that there exists some E ′ such that (n − 1) |= R(E ′ ). Thus, ∀n.∃E ′ . n |= R(E ′ ), so we can apply Lemma 5 to get the desired result.
Notice that in the conclusion of Lemma 6, if e ′ takes another step, we can apply Lemma 6 again to the triples for e ′ . So, given some initial triple {source(i, E)} e {Q} and a diverging execution of e, by induction we can repeatedly apply Lemma 6 to construct an infinite execution of the source program. Finally, we prove that if the execution of e was fair, this source execution will be fair as well, giving us Lemma 4. Of course, for the full mechanized proof we have to take into account the delay steps and consider the case where the target thread multiple source threads. But all of these are finite additional possibilities, they do not fundamentally change the argument sketched above.

Proof of Compiler Correctness
We now give a brief overview of our proof of Theorem 1. Recall that we want to show that if E is a well-typed source expression, then E ⊑ E.
Our proof is a binary logical relations argument. We interpret each type τ as a relation on values from the target and source language, writing v ≃ V V : τ to say that v and V are related at type τ . However, following the example of [25,24], these are relations in our refinement logic, which means we can use all of the constructs of the logic to describe the meaning of types. We then prove a fundamental lemma showing that well-typed expressions are logically related to their translation. Next, we show that our logical relation implies the triple used in Ht-refine. Theorem 1 is then a direct consequence of these two lemmas.
Details of these proofs can be found in the appendix; here we focus on the definition of the logical relation itself. For most types, the interpretation is straightforward and fairly standard. For instance, v ≃ V V : Int holds exactly when v = V = n, for some integer n. The important exception, of course, is the interpretation of session types, in which we need to relate the encoding of channels as linked-lists to the source language's primitive buffers.
Sessions as an STS. To interpret session types, we generalize the state transition system from the example in §3 to handle the more complicated "protocols" that session types represent.
What should the states of this STS be? In the STS used in §3, we had three states: init, in which the message had not been sent; sent, where a message had been sent from the left end-point, but not received; and received, where the message had now been received at the right end-point. In the general case, we will have more than one message, so our states need to track how many messages have been sent/received on each end-point. We also need to know the "current" type of the end-points, but notice that if we know the starting type of an end-point, and how many messages have been sent/received on it, we can always recover these current types. We write S n for the type after n messages have been sent/received starting from S.
We also need to know which heap locations l l and l r currently represent the end-points of the channel. All together then, the states will be tuples (n l , n r , l l , l r ) describing how many messages have been sent/received on each end-point, and the corresponding heap locations.
Remember that we also need to define the tokens and transitions associated with each state of our STS. The transitions are simple: we can either advance the left end-point, incrementing n l and updating l l , and similarly for the right end-point. For the tokens, recall that in our example proof, we had [S] and [R] tokens used by each thread to advance the state when they had interacted with their respective end-points. In general, the threads will now use the endpoints multiple times, so we need a token for each of these uses on both sides. Concretely, we will have two kinds of tokens, [Left n] and [Right n], which are used when advancing the left and right end-point counter to n, respectively.
To complete the description of the STS, we have to talk about the interpretation of the states. This interpretation has to relate the messages in the source channel's current buffers to the nodes in the linked list on the target heap. The individual messages should, of course, be related by our logical relation (≃ V ). We lift this relation to lists of messages (≃ L ) as follows: For now, ignore the ⊲ symbol. The left rule says that two empty lists are equivalent at any session type. The right rule says two lists are related at a receive type ?τ. S, if their heads are related under τ , and the remainders of each list are related at S. It is important that this is a receive type: if the current type of the end-point is a send type, then there should not be any messages in its receive buffer, so the rule for empty lists is the only one that applies.
We can now give our state interpretation, ϕ, which is parameterized by (a) the starting type S of the left end-point (the right end-point's starting type is by necessity dual so there is no need to track it), and (b) the name c of the channel: Let us explain this piece by piece. To start, we have that there exists a list of source values L c and a list of target values L h , representing the messages that are stored in the buffer right now. We then distinguish between two cases: either the first buffer is empty or the second buffer is empty. We omit the second case (corresponding to the second disjunct) because it is symmetric. In the first case, the channel's first buffer contains L c and the second buffer is empty (10, left). On the target side, the buffer is represented as a linked list from l l to l r containing the values L h (10, right). Of course, the lists of values need to be related according to the end-point's current type S n l (11, left). Finally, the number of messages sent/received through the left end-point, plus the number of messages still in the buffer, should equal the total number of messages sent/received through the right end-point (11, right). Therefore, when these remaining messages are received by the left end-point, the two types will again be dual.
Informally then, the value relation at session types l ≃ V c s : S says that there exists an appropriate STS and tokens for the session S which relates l and c s . We can then prove Hoare triples for the message-passing primitives that manipulate this STS. For instance, for heapRecv we have (omitting delay steps): This triple closely corresponds to the typing rule Recv (Figure 1): typing judgments in the premise become value relations in the pre-condition, and the conclusion is analogously transformed into the postconditon. Indeed, the proof of the fundamental lemma for the logical relation essentially just appeals to these triples.
There is something we have glossed over: when we defined the logical relation, we used the STS, but the STS interpretation used the logical relation! This circularity is the reason for the ⊲ symbol guarding the recursive occurrence of (≃ V ) in L-cons. The details are spelled out in the appendix.

Conclusion and Related Work
We have presented a logic for establishing fair, termination-preserving refinement of higher-order, concurrent languages. To our knowledge, this is the first logic combining higher-order reasoning (and in particular, step-indexing) with reasoning for termination-sensitive concurrent refinement. Moreover, we applied this logic to verify the correctness of a compiler that translates a session-typed source language with channels into an ML-like language with a shared heap.
All of these results have been fully mechanized in Coq. Our mechanization builds on the Coq development described in Jung et al. [22] and the proof-mode from Krebbers et al. [24]. The proofs use the axioms of excluded middle and indefinite description. The proof scripts can be found online [1].
Second Case Study. Our logic is not tied to this source language and translation: we have used it to mechanize a proof that the Craig-Landin-Hagersten queue lock [11, 31] refines a ticket lock. Further details can be found in the appendix.
Linearity. Linearity has been used in separation logics to verify the absence of memory leaks: if heap assertions like l ֒→ v are linear, and the only way to "dispose" of them is by freeing the location l, then post conditions must mention all memory that persists after a command completes [20]. Our treatment of linearity has limitations that make it unsuitable for tracking resources like the heap. First, in our logic, only affine assertions can be framed (see Ht-frame), because framing could hide the obligation to perform steps on source threads. Of course, for resources like the heap this would be irrelevant, and this rule could be generalized. Second, linear resources cannot be put in STS interpretations, so they cannot be shared between threads. Since STSs are implemented in terms of a more primitive feature in Iris called invariants, which are affine, allowing linear resources to be put inside would circumvent the precise accounting that motivates linearity in the first place. Thus, we would need to extend Iris with a useful form of "linear" shared invariants, which we leave to future work. give logical relations for session-typed languages, which they use to prove strong normalization and contextual equivalence results. Their logical relation is defined "directly", instead of translating into an intermediary logic. Early versions of another session-typed system [43] used a ring-buffer to represent channels instead of linked lists, which would be interesting to verify.
Logics for Concurrency, Termination, and Refinement. There is a vast literature on program logics for concurrency [34,8,40,23,22,14,37,12,36,33,15,41,16,29,30,28,18]. Indeed, the reason for constructing a logical relation on top of a program logic, as in , is so that we can take advantage of the many ideas that have proliferated in this community.
Focusing on logics for refinement and termination properties: Benton [4] pioneered the use of a relational Hoare logic for showing the correctness of compiler transformations in the sequential setting. Yang [44] generalized this to relational separation logic. We have already described [40], which developed a higher-order concurrent separation logic for termination-insensitive refinement. Liang et al.
[29] also allow non-terminating programs to refine terminating ones. This was extended in [30] for a termination-preserving refinement, but this deals with termination-preservation without fairness. Most recently Liang and Feng [28] addressed fair termination-preserving refinement. In their logic, threads can explicitly reason about how their actions may or may not further delay other threads, which is more general than our approach and may be needed for verifying some of the examples they consider. It would be interesting to adapt this more explicit fairness reasoning to the higher-order setting.
Hoffmann et al.
[18] features a concurrent separation logic for total correctness. Threads own resources called "tokens", which must be "used up" every time a thread repeats a while loop. This "using up" of tokens inspired our step shifts. Later, da Rocha Pinto et al. [36] generalized this by using ordinals instead of tokens: threads decrease the ordinal they own as they repeat a loop. This is useful for languages with unbounded non-determinism. Our technique for coping with step-indexing in §4 relied on bounded non-determinism. It may be possible to remove this limitation by using transfinite step-indexing [5,38] instead.  Disclaimer: The Coq development of the logic is taken to be authoritative. Any discrepancies between this document and the Coq code should therefore be regarded as errors. Some important rules developed in the Coq proof may have been left out. Moreover, any mistakes in this document may have been introduced by the present authors: readers interested in the original Iris should consult its documentation. Also, the reader should be aware that the latest version of Iris has departed significantly from the version with which we began our extensions. The key intuition behind COFEs is that elements x and y are n-equivalent, notation x n = y, if they are equivalent for n steps of computation, i.e., if they cannot be distinguished by a program running for no more than n steps. In other words, as n increases, n = becomes more and more refined (cofe-mono)and in the limit, it agrees with plain equality (cofe-limit). In order to solve the recursive domain equation in §A.6 it is also essential that COFEs are complete, i.e., that any chain has a limit (cofe-compl).

Contents of Appendices
Intuitively, applying a non-expansive function to some data will not suddenly introduce differences between seemingly equal data. Elements that cannot be distinguished by programs within n steps remain indistinguishable after applying f . The reason that contractive functions are interesting is that for every contractive f : T → T with T inhabited, there exists a unique fixed-point fix(f ) such that fix(f ) = f (fix(f )).
Definition 11. The category COF E consists of COFEs as objects, and nonexpansive functions as arrows.
Note that COF E is cartesian closed. In particular: Definition 12. Given two COFEs T and U , the set of non-expansive functions Definition 13. A (bi)functor F : COF E → COF E is called locally non-expansive if its action F 1 on arrows is itself a non-expansive map. Similarly, F is called locally contractive if F 1 is a contractive map.
The function space (−) ne − → (−) is a locally non-expansive bifunctor. Note that the composition of non-expansive (bi)functors is non-expansive, and the composition of a non-expansive and a contractive (bi)functor is contractive. The reason contractive (bi)functors are interesting is that by America and Rutten's theorem [2,7], they have a unique 10 fixed-point.
RAs are closely related to Partial Commutative Monoids (PCMs), with two key differences: 1. The composition operation on RAs is total (as opposed to the partial composition operation of a PCM), but there is a specific subset V of valid elements that is compatible with the composition operation (ra-valid-op). This take on partiality is necessary when defining the structure of higherorder ghost state, CMRAs, in the next subsection. 2. Instead of a single unit that is an identity to every element, we allow for an arbitrary number of units, via a function |−| assigning to an element a its (duplicable) core |a|, as demanded by ra-core-id. We further demand that |−| is idempotent (ra-core-idem) and monotone (ra-core-mono) with respect to the extension order, defined similarly to that for PCMs (ra-incl).
Notice that the domain of the core is M ? , a set that adds a dummy element ⊤ to M . Thus, the core can be partial : not all elements need to have a unit. We use the metavariable a ? to indicate elements of M ? . We also lift the composition (·) to M ? . Partial cores help us to build interesting composite RAs from smaller primitives. Notice also that the core of an RA is a strict generalization of the unit that any PCM must provide, since |−| can always be picked as a constant function. 3. We add an aditional relation that captures "taking a step" on a resource. In most cases this will be the full relation, as we have no useful notion of "stepping" such resources.But, for resources used for establishing refinements, this will correspond to taking some kind of step in the source program.
Definition 15. It is possible to do a frame-preserving update from a ∈ M to The assertion a B says that every element a ? f compatible with a (we also call such elements frames), must also be compatible with some b ∈ B. Notice that a ? f could be ⊤, so the frame-preserving update can also be applied to elements that have no frame. Intuitively, this means that whatever assumptions the rest of the program is making about the state of γ, if these assumptions are compatible with a, then updating to b will not invalidate any of these assumptions. Since Iris ensures that the global ghost state is valid, this means that we can soundly update the ghost state from a to a non-deterministically picked b ∈ B. Definition 16. It is possible to do a frame-preserving step update from We can regard this as a transformation of two compatible resources a and b in which we do a frame-preserving update on the first component a and a step on the second component b.

CMRA
This is a natural generalization of RAs over COFEs. All operations have to be non-expansive, and the validity predicate V can now also depend on the step-index. We define the plain V as the "limit" of the V n : The extension axiom ( cmra-extend). Notice that the existential quantification in this axiom is constructive, i.e., it is a sigma type in Coq. The purpose of this axiom is to compute a 1 , a 2 completing the following square: where the n-equivalence at the bottom is meant to apply to the pairs of elements, i.e., we demand a 1 n = b 1 and a 2 n = b 2 . In other words, extension carries the decomposition of b into b 1 and b 2 over the n-equivalence of a and b, and yields a corresponding decomposition of a into a 1 and a 2 . This operation is needed to prove that ⊲ commutes with separating conjunction: ⊲(P * Q) ⇔ ⊲P * ⊲Q Definition 18. An element ε of a CMRA M is called the unit of M if it satisfies the following conditions: 1. ε is valid: ∀n. ε ∈ V n 2. ε is a left-identity of the operation: ∀a ∈ M. ε · a = a 3. ε is a discrete COFE element 4. ε is its own core: |ε| = ε Lemma 19. If M has a unit ε, then the core |−| is total, i.e., ∀a. |a| ∈ M .
Definition 20. It is possible to do a frame-preserving update from a ∈ M to Definition 21. It is possible to do a frame-preserving step update from Note that for RAs, this and the RA-based definition of a frame-preserving update and frame-preserving step update coincide.

Definition 22.
A CMRA M is discrete if it satisfies the following conditions: 1. M is a discrete COFE 2. V ignores the step-index: ∀a ∈ M. a ∈ V 0 ⇒ ∀n, a ∈ V n Note that every RA is a discrete CMRA, by picking the discrete COFE for the equivalence relation. Furthermore, discrete CMRAs can be turned into RAs by ignoring their COFE structure, as well as the step-index of V. 1. f is non-expansive 2. f preserves validity: Definition 24. The category CMRA consists of CMRAs as objects, and monotone functions as arrows.
Note that every object/arrow in CMRA is also an object/arrow of COF E. The notion of a locally non-expansive (or contractive) bifunctor naturally generalizes to bifunctors between these categories.

A.2 COFE constructions
Next (type-level later) Given a COFE T , we define ◮T as follows (using a datatype-like notation to define the type): ◮T next(x : T ) Note that in the definition of the carrier ◮T , next is a constructor (like the constructors in Coq), i.e., this is short for {next(x) | x ∈ T }. ◮(−) is a locally contractive functor from COF E to COF E.
Uniform Predicates Given a CMRA M , we define the COFE UPred(M ) of uniform predicates over M as follows: One way to understand this definition is to re-write it a little. We start by defining the COFE of step-indexed propositions: For every step-index, the proposition either holds or does not hold.
Notice that this notion of SProp is already hidden in the validity predicate V n of a CMRA: We could equivalently require every CMRA to define V − (−) : M ne − → SProp, replacing cmra-valid-ne and cmra-valid-mono. Now we can rewrite UPred(M ) as step-indexed predicates over pairs of M eleements, which is "monotone" in a certain sense with respect to the first element:

A.3 RA and CMRA constructions
When describing a CMRA construction, unless specified otherwise, the step relation is taken to be the full relation.
Product Given a family (M i ) i∈I of CMRAs (I finite), we construct a CMRA for the product i∈I M i by lifting everything pointwise. Frame-preserving updates on the M i lift to the product: Finite partial function Given some infinite countable K and some CMRA M , the set of finite partial functions K fin − ⇀ M is equipped with a COFE and CMRA structure by lifting everything pointwise.
We obtain the following frame-preserving updates: Above, V refers to the validity of M . K fin − ⇀ (−) is a locally non-expansive functor from CMRA to CMRA.
Agreement Given some COFE T , we define Ag(T ) as follows: Ag(−) is a locally non-expansive functor from COF E to CMRA. You can think of the c as a chain of elements of T that has to converge only for n ∈ V steps. The reason we store a chain, rather than a single element, is that Ag(T ) needs to be a COFE itself, so we need to be able to give a limit for every chain of Ag(T ). However, given such a chain, we cannot constructively define its limit: Clearly, the V of the limit is the limit of the V of the chain. But what to pick for the actual data, for the element of T ? Only if V = N we have a chain of T that we can take a limit of; if the V is smaller, the chain "cancels", i.e., stops converging as we reach indices n / ∈ V . To mitigate this, we apply the usual construction to close a set; we go from elements of T to chains of T .
We define an injection ag into Ag(T ) as follows: There are no interesting frame-preserving updates for Ag(T ), but we can show the following: Exclusive CMRA Given a COFE T equipped with a step-indexed relation ( n ), we define a CMRA Ex(T ) such that at most one x ∈ T can be owned: All cases of composition go to ⊥.

|ex(x)| ⊤ |⊥| ⊥
Remember that ⊤ is the "dummy" element in M ? indicating (in this case) that ex(x) has no core. The step-indexed equivalence is inductively defined as follows: is a locally non-expansive functor from COF E to CMRA. We obtain the following frame-preserving update: We lift the stepping relation to: x n y ex(x) n ex(y) STS with tokens Given a state-transition system (STS, i.e., a directed graph) (S, → ⊆ S × S), a set of tokens T , and a labeling L : S → ℘(T ) of protocolowned tokens for each state, we construct an RA modeling an authoritative current state and permitting transitions given a bound on the current state and a set of locally-owned tokens. The construction follows the idea of STSs as described in CaReSL [40]. We first lift the transition relation to S × ℘(T ) (implementing a law of token conservation) and define a stepping relation for the frame of a given token set: We further define closed sets of states (given a particular set of tokens) as well as the closure of a set: The remaining cases are all ⊥.
We will need the following frame-preserving update: At the moment we do not make use of the non-trivial step structure on STS's -all instances of STS's that are used in our present proofs are wrapped in another construction that makes the step structure trivial.
The core is not a homomorphism. The core of the STS construction is only satisfying the RA axioms because we are not demanding the core to be a homomorphism-all we demand is for the core to be monotone with respect to the ra-incl and have ra-core-distrib property. This last rule is kind of like homomorphism for elements that are already cores, which is weaker than normal homomorphism.

A.4 Language
A language Λ consists of a set Expr of expressions (metavariable e), a set Val of values (metavariable v), and a set State of states (metvariable σ) such that -There exist functions val2expr : Val → Expr and expr2val : Expr ⇀ val (notice the latter is partial), such that We will write e 1 , σ 1 → e 2 , σ 2 for e 1 , σ 1 → e 2 , σ 2 , ⊥.
A reduction e 1 , σ 1 → e 2 , σ 2 , e f indicates that, when e 1 reduces to e 2 , a new thread e f is forked off.

K does not turn non-values into values:
∀e. expr2val(e) = ⊥ ⇒ expr2val(K(e)) = ⊥ 2. One can perform reductions below K: ∀e 1 , σ 1 , e 2 , σ 2 , e f . e 1 , σ 1 → e 2 , σ 2 , e f ⇒ K(e 1 ), σ 1 → K(e 2 ), σ 2 , e f 3. Reductions stay below K until there is a value in the hole: Concurrent language For any language Λ, we define the corresponding threadpool semantics. The step relation for thread pool configurations is indexed by the number of the thread that performed a step. Definition 30. We say that thread index i is eventually always enabled in a diverging execution F if there exists N such that ∀n ≥ N , i is enabled in π 1 (F (n)).

Machine syntax T ∈ ThreadPool
Definition 31. We say that thread index i always eventually steps in a diverging execution F if for all n, there exists n ′ ≥ n such that π 2 (F (n ′ )) = i.
Definition 32. A diverging execution is (weakly) fair if for all i, if i is eventually always enabled in F , then i always eventually steps in F .

A.5 Logic
To instantiate Iris, you need to define the following parameters: -A language Λ, and a locally contractive bifunctor Σ : COF E → CMRA defining the ghost state, such that for all COFEs A, the CMRA Σ(A) has a unit. (By Lemma 19, this means that the core of Σ(A) is a total function.) As usual for higher-order logics, you can furthermore pick a signature S = (T , F , A) to add more types, symbols and axioms to the language. You have to make sure that T includes the base types: T ⊇ {Val, Expr, State, M, InvName, InvMask, Prop} Elements of T are ranged over by T . Each function symbol in F has an associated arity comprising a natural number n and an ordered list of n + 1 types τ (the grammar of τ is defined below, and depends only on T ). We write F : τ 1 , ... , τ n → τ n+1 ∈ F to express that F is a function symbol with the indicated arity.
Furthermore, A is a set of axioms, that is, terms t of type Prop. Again, the grammar of terms and their typing rules are defined below, and depends only on T and F , not on A. Elements of A are ranged over by A.

Grammar
Syntax. Iris syntax is built up from a signature S and a countably infinite set Var of variables (ranged over by metavariables x, y, z): Recursive predicates must be guarded : in µx. t, the variable x can only appear under the later ⊲ modality. Note that , ⊲ bind more tightly than * , - * , ∧, ∨, and ⇒. We will write |⇛ t P for |⇛ t t P , and similarly for |⇛ ⇛ t P . If we omit the mask, then it is ⊤ for weakest precondition wp e {x. P } and ∅ for primitive view shifts |⇛P and primitive step shifts |⇛ ⇛P .
Some propositions are timeless, which intuitively means that step-indexing does not affect them. This is a meta-level assertion about propositions, defined as follows: Similarly, some propositions are affine timeless, which means that step-indexing does not affect them when under an affine modality: Types Iris terms are simply-typed. The judgment Γ ⊢ t : τ expresses that, in variable context Γ , the term t has type τ . A variable context, Γ = x 1 : τ 1 , ... , x n : τ n , declares a list of variables and their types. In writing Γ, x : τ , we presuppose that x is not already declared in Γ .

Well-typed terms
Proof rules The judgment Γ | Θ ⊢ P says that with free variables Γ , proposition P holds whenever all assumptions Θ hold. We implicitly assume that an arbitrary variable context, Γ , is added to every constituent of the rules. Furthermore, an arbitrary boxed assertion context Θ may be added to every constituent. Axioms Γ | P ⊣⊢ Q indicate that both Γ | P ⊢ Q and Γ | Q ⊢ P can be derived.
Laws of intuitionistic higher-order logic with equality. This is entirely standard.
Furthermore, we have the usual η and β laws for projections, λ and µ.
Similar rules hold for a L .
Laws for the later modality.
a is a discrete COFE element timeless( a ) a is an element of a discrete CMRA timeless(V(a)) timeless(Phy(σ)) a is an element of a discrete CMRA atimeless(V(a)) atimeless(Phy(σ)) Laws for the always/relevant modality.
Laws of primitive view shifts.

pvs-intro
Laws of primitive step shifts.
Laws of weakest preconditions. wp-value Lifting of operational semantics. wp-lift-step Notice that primitive view shifts cover everything to their right, i.e., |⇛P * Q |⇛(P * Q), and similarly for primitive step shifts.
Here we define wp E e f {x. P } Emp if e f = ⊥ (remember that our stepping relation can, but does not have to, define a forked-off expression).

Adequacy
Finite Executions and Safety. The adequacy statement concerning functional correctness reads as follows: where ϕ is a meta-level predicate over values, i.e., it can mention neither resources nor invariants. Furthermore, the following adequacy statement shows that our weakest preconditions imply that the execution never gets stuck : Every expression in the thread pool either is a value, or can reduce further.
Notice that this is stronger than saying that the thread pool can reduce; we actually assert that every non-finished thread can take a step.
Diverging Executions. Remember that our goal is to show that if we have proved wp e {x. Q} and e has a fair diverging execution, then there is a fair diverging execution of some corresponding source program. Of course, there is no such notion of a "source program" baked into the logic at this point yet.
All we have is the step relation n on CMRA elements. The rules above for wp e {x. Q} suggest that 12 for each step e takes, we are required to perform a step-shift, thereby performing reduction steps on CMRA resources.
We can lift the n relation from CMRA elements to lists of CMRA elements, much as we lift the per-thread step relation to an indexed relation on threadpools: In general we shall use A and B as metavariables for such lists of CMRA elements, and write * A to represent the product of the elements of A.
Definition 33. We say index i is n-enabled in A if there exists B such that A n i B.
Somehow, we want to connect up these CMRA steps to steps in some source language, for a suitably chosen CMRA. Still working a bit more abstractly than that for the moment, let U be some COFE equipped with a family of relations ( i →: U ? ×U ? ) i∈N . We can adapt all of our definitions about fairness to the setting of this reduction on U ? , e.g.: Definition 35. A diverging execution of a is a function F : N → U ? × N such that: 1. F (0) = (a, i) for some i.
Definition 36. We say H : N → List M → U ? is a step-preserving map if the following conditions hold: 1. If i is enabled in H(n, A) then i is n-enabled in A.
2. If * A ∈ V n , * B ∈ V n , A n i B and H(n, A) ∈ U , then H(n, B) ∈ U and H(n, A) i → H(n, B) 12 We shall see that this is indeed the case when we examine the definition of weakest precondition in the model.

If H(n, A)
i → H(n, B) then ∀n ′ ≤ n, H(n ′ , A) i → H(n ′ , B) Definition 37. U has bounded non-determinism if ∀a ∈ U , the set {b |∃i. a i → b} is finite.
We are now able to state the infinite adequacy theorem: Theorem 38. Assume U has bounded non-determinism under a step relation ( i →: U ? × U ? ) i∈N . Let H be a step-preserving map to U . If [e]; σ has a diverging execution, and all of the following hold:

A.6 Model and semantics
The semantics closely follows the ideas laid out in [6].
Generic model of base logic The base logic including equality, later, always, and a notion of ownership is defined on UPred(M ) for any CMRA M .

Interpretation of base assertions
We are thus going to define the assertions as mapping pairs of CMRA elements to sets of step-indices.
We introduce an additional logical connective Own(a) and OwnL(a), which will later be used to encode all of P ι , a , a L and Phy(σ).
Note: There are slight differences between the definition here and the version in the Coq development. For instance, Own(a) in the Coq development does not stipulate that the second component is in fact equivalent to ε, which makes it non-affine; but in practice we almost always use A(Own(a)), so here we just present a version equivalent to that.
For every definition, we have to show all the side-conditions: The maps have to be non-expansive and monotone.

Iris model
Semantic domain of assertions. The first complicated task in building a model of full Iris is defining the semantic model of Prop. We start by defining the functor that assembles the CMRAs we need to the global resource CMRA: Above, M ? is the monoid obtained by adding a unit to M . (It's not a coincidence that we used the same notation for the range of the core; it's the same type either way: M + 1.) Remember that Σ is the user-chosen bifunctor from COF E to CMRA (see §A.5). ResF(T op , T ) is a CMRA by lifting the individual CMRAs pointwise. Furthermore, since Σ is locally contractive, so is ResF. Now we can write down the recursive domain equation: iPreProp is a COFE defined as the fixed-point of a locally contractive bifunctor. This fixed-point exists and is unique by America and Rutten's theorem [2,7]. We do not need to consider how the object is constructed. We only need the isomorphism, given by We then pick Prop as the interpretation of Prop:

Prop Prop
Interpretation of assertions. Prop is a UPred, and hence the definitions from §A.6 apply. We only have to define the interpretation of the missing connectives, the most interesting bits being primitive view shifts and weakest preconditions.

World satisfaction
Notice that the assertion P corresponding to the world ι must be affine, in the sense that n ∈ P (R(ι), ε). Without this stipulation, threads would be able to put linear resources inside invariants and STS interpretations. We prevent this in the current formulation of the logic because otherwise the rules for dealing with invariants would have to be stricter if we still wanted to establish fair refinements.
wp is defined as the fixed-point of a contractive function.
Interpretation of program logic assertions Γ ⊢ t : a and Phy(σ) are just syntactic sugar for forms of Own(−).

Expr ∆Expr
State ∆State For the remaining base types τ defined by the signature S, we pick an object X τ in COF E and define τ X τ For each function symbol F : τ 1 , ... , τ n → τ n+1 ∈ F , we pick a function F : Interpretation of non-propositional terms An environment Γ is interpreted as the set of finite partial functions ρ, with dom(ρ) = dom(Γ ) and ρ(x) ∈ Γ (x) .
Logical entailment. We can now define semantic logical entailment.

Interpretation of entailment
The soundness statement of the logic reads

A.7 Derived proof rules and other constructions
We will below abuse notation, using the term meta-variables like v to range over (bound) variables of the corresponding type. We omit type annotations in binders and equality, when the type is clear from context. We assume that the signature S embeds all the meta-level concepts we use, and their properties, into the logic. (The Coq formalization is a shallow embedding of the logic, so we have direct access to all meta-level notions within the logic anyways.) Persistent/Relevant assertions.
Definition 39. An assertion P is persistent or relevant if P ⊢ P .
Of course, P is persistent for any P . Furthermore, by the proof rules given in §A.5, t = t ′ as well as |a| , V(a) and P ι are persistent. Persistence is preserved by conjunction, disjunction, separating conjunction as well as universal and existential quantification. In our proofs, we will implicitly add and remove from persistent assertions as necessary.

Affine assertions.
Definition 40. An assertion P is affine if P ⊢ A(P ).
In our proofs, we will implicitly add and remove A(−) from persistent assertions as necessary.
Timeless assertions. We can show that the following additional closure properties hold for timeless assertions: Some similar rules apply for atimeless(-).
Program logic Hoare triples and view shifts are syntactic sugar for weakest (liberal) preconditions and primitive view shifts, respectively: We write just one mask for a view shift when E 1 = E 2 . Clearly, all of these assertions are persistent. The convention for omitted masks is similar to the base logic: An omitted E is ⊤ for Hoare triples and ∅ for view shifts.
Derived Rules We omit many of the derived rules for Hoare triples, view shifts, and step shifts. The interested reader can consult the Coq mechanization.
Global functor, ghost ownership, and namespaces For composability reasons, Iris makes it possible to combine a collection of CMRAs to get a larger "global" CMRA. This makes it possible to combine proofs that are done using a certain CMRA M with ones that are done doing another CMRA M ′ . We do omit the descriptions of these mechanisms; the interested reader should consult the original Iris 2.0 documentation.

A.8 Refinement RA
We now briefly describe the RA used to model source assetions. This entire section is new. Fix a source language Λ. We say that a list of configurations, C is compatible with a list of thread indices, L, written compat(C, L)L, if: We define an RA Refine(Λ): where max(v, v ′ ) is master if either v or v ′ is master, and the maximum of two lists is just the longer of the two. We have an additional proviso stating that multiplication is only defined if all of the following hold: Intuitively, the second component of an element, S represents a set of thread ID's "owned" by this element, and the C and L are some prefix of an execution of a source program. Then, condition one for multiplication being defined says there can be at most one master. Condition two says that, among two snapshots, one can be longer than the other, but the longer one cannot contain any additional steps by threads owned by the other. Condition three and four say that a snapshot must be a prefix of master, subject to the constraint that the master cannot contain any extra steps by threads owned by the snapshot.
The definition of for this RA is somewhat complicated. Let us motivate it in words -a reader that wants details is advised to consult the Coq formalization. Only snapshots may take steps. Intuitively, the snapshot is obligated to step every thread it controls (i.e. every index in S) which can possibly take a step. But, since the snapshot is only a partial prefix of the program execution, other threads not controlled by this snapshot may have taken steps. Thus, we first non-deterministically speculate some steps performed by other threads and then perform all of the required steps for the owned threads. Finally, since performing those steps may fork off new threads, we add the thread ids of the new threads to S.
Of course, for extra flexibility, we are allowed to step each thread more than once. We do not bake delay steps into this monoid. Rather, if we want delay steps, we first transform Λ into a language Λ ′ that has additional "stutter" steps for delay.
Finally, we can interpret source as: We also get an assertion SPhy(σ) for talking about the state of the assertion: We can use this "large footprint" assertion about source programs to derive smaller assertions, just as we do for the Phy(σ) assertion in Iris.
Finally, with some effort we can use this CMRA with the infinite adequacy theorem to get the refinement results stated in the body of the paper.

B.1 Session-Typed Language Translation
In this appendix we develop the logical relation used for our compiler correctness proof. The body of the paper has already explained the meaning of session types. But it avoided the crucial issue of showing that this relation is well-defined. What actually happens is we develop a state transition system for sessions which is parameterized by an interpretation of types. As we'll see, we then take a fixed point which is defined using this construction.
In our actual proof though, we do not work with the Hoare triple versions of our rules. Instead, we work with a more primitive form called weakest precondition, since it is much easier to work with in a proof assistant. We first sketch the connection between these and Hoare triples.
Then, we give this parameterized STS construction and state the mechanized weakest precondition proof rules using this STS for the message passing primitives. This time around we will be more explicit about the delay constants at first, but then show why it is OK to hide them. Next, we describe some additional Iris features we'll need and use them to define the logical relation (in particular, the ⊲ modality we mentioned without explanation in the main text). We then prove that our logical relation is sound (that is, it implies refinement for closed terms). Finally, we prove the fundamental lemma, which shows that the logical relation holds between well-typed expressions and their translation. This completes the proof.
Weakest Precondition In Iris, Hoare triples are not a primitive form. Instead, they are defined in terms of a weakest pre-condition primitive as follows: The assertion wp e {x. Q} expresses ownership of resources that is strong enough to justify the safe execution of e, such that when e terminates, Q holds. This is an ephemeral assertion in the sense that, like e.g. l ֒→ v, it can be used at most once and is the invalidated.
The magic wand P - * wp e {x. Q} says that if we are given resources satisfying P , we have enough resources to satisfy the weakest pre-condition. The wand - * works like an implication, but is right adjoint to the separating conjunction * instead of plain conjunction ∧.
Notice that in the example in §3, when we summarized the current state of the proof, we often said things like "Our current resources are P and we have to verify the following code e (with post-condition Q)". This exactly corresponds to a proof-state where our current logical context is P , and the goal is wp e {Q}: It should not be surprising that in carrying out Iris proofs in Coq, we generally work with weakest pre-conditions. Next, we wrap the always modality around the wand. This is to enforce that proofs of Hoare triples be persistent, i.e., the modality makes sure that a Hoare triple, once established, will remain valid throughout the remaining verification. By default, assertions in Iris are ephemeral and hence can be used only once.
Finally, there is an affine modality wrapping the whole thing -there should be no other source hidden within such a Hoare triple. We only get to use ones in P .
The Session STS The states, tokens, and transitions we gave in the main text did not mention the logical relation, so there is no concern about circularity in their definition. The only problem was the definition of the state interpretation, which was given as: What we now do is have the lifting of lists take a parameter, Θ, which is a pre-existing interpretation of types (i.e., a map from types to a relation between values of the target and source): Then, ϕ will also take this parameter and pass it to the list relation: We write ↑ (n l , −, l, −) for the set of all states that have first component n l and third component l, and symmetrically for the right counts and heap pointer.
Finally, we can define an assertion Session Θ (l, c s , S) which asserts (1) existence of an STS governing l and c, (2) comes equpped with the tokens needed for manipulating the end-point indicated by s, and (3) ensures that the current type of the end-point for s has type S: Of course, we've now only deferred the problem -eventually we do need to plug in the desired logical relation for Θ. For now, the key is that we can still prove things about channels which use this invariant; its just that the proof rules are also parameterized by Θ.
To show these rules, we need to be a bit more precise about delay constants for a moment. The triple about the receive primitive mentioned in the body of the paper omitted delay constants, and in general we have not been explicit about such constants in the main text. Let us first be a bit more precise about this, so that we can justify why it is safe to ignore them subsequently.
As we said when explaing the source assertion when we do a proof we need to fix a number D that will be an upper bound throughout for all delay constants. In the Coq development, we somewhat profligately proved things involving the above STS assuming that this upper bound was at least ≥ 100. So for concreteness, let us just fix this D now to be 100. Then we have proved the following rules (written in the weakest precondition style instead of Hoare triples): In addition, to the explicit delays, we also have this business about ⊲P in the second rule, which we can ignore for now. Note that if 4 < k ≤ D − 2, then k satisfies all of the side conditions placed on the delay constants that we start with in each rule (i.e., d). Moreover, such a d satisfies all of the constraints placed on the ending delay constant (i.e., d ′ ). That means if we start with such a k, at the end we can continue with the same k. In particular, a choice of k = 50 works. It's also the case that 0 satisfies the conditions on the d ′ above; so whatever delay we start with, we can always end up with 0, if we wish.
Putting this together, we will define source(i, E) (that is, without the delay constant) as: That is, when we are working with an expression, we assume an implicit delay constant of 50; when the source thread is a value, it is 0'd out. Rewriting the rules above with this new form, we can ignore the delay constants: To see that these implicit rules follow from the explicit delay constant form, observe that if (1) K[E] is a value, E must in fact be a value, and (2) if K[V ] is a value, then for all V ′ , K[V ′ ] is a value. This means for each of the above rules, we first determine whether the evaluation K will be a value after we substitute the return values in the post-condition; if it is, we apply the corresponding original rule taking d ′ = 0. If not, we take d ′ = 50.
The reason we chose the "implicit" delay for values to be 0 is so that source(i, V ) ⊢ Stopped, and so that our refinement rule can also be written as: Logical Relation Now that we have the STS defined in this parameterized way, we can follow up by defining the logical relation in a non-circular way. We follow the standard set-up of defining an interpretation of types that relates values, then lifting this to a relation on closed expressions, and then using that to define a relation on open expressions. In general, given a function Θ which maps types to Iris relations on values of the target and source, we write v ≃ V Θ V : τ to say that v and V are related at the interpretation of τ under Θ.
Lifting relations on values to expressions. The expression lifting operation is generic with respect to the final interpretation on values, so let us first define that. Given Θ, we define its lifting between expressions of the target and source as: This is an assertion saying that for any choice of thread i and evaluation context K, if we are given source(i, K[E]) we can prove a weakest-precondition for e in which the executions end in related values according to Θ at the appropriate type. We wrap this wand in an affine modality to ensure there are no implicit other threads owned. Also, in the post-condition, the proof that the values are related must be affine for a similar reason.
Let us note that the standard way such lifting relations are defined (in for instance, the sequential case) is more or less to say that e and E are related if they evaluate to related values. Indeed, that's essentially what we are saying here, but using the weakest precondition and all of the other machinery we have built up so that we're implicitly talking about concurrent executions and fairness.
Note that so long as Logical relation on values. Iris has two important features which we did not explain in the main text. First, there is the modality ⊲P (called "later"), which we have asked the reader to ignore a few times. This describes resources which satisfy P at one lower step-index. So, P ⊢ ⊲P , but not conversely. Second, we can construct fixed-points of arbitrary recursive definition of a predicate, so long as all recursive occurences are under the "later" modality. Such recursive definitions are called "guarded". We will define our interpretation of types by taking a fixed point of a guarded recursive definition. First, we define the function F which we are going to take the fixed-point of. Given an interpretation of types, Θ (that is, a map from types to an Iris relation on values), we define F (Θ) as yet another interpretation of types, defined by structural induction on types: The first three rules are straight-forward. The third says that two values are related at τ ′ ⊸ τ , if, when we apply them to values related at the intepretation of τ ′ , the applications are related at τ . Since the applications are expressions and not values, we use the lifting of the type interpretation. 13 By ⊲Θ we mean the type interpretation which applies a later after applying Θ to its arguments. Note that each occurence of F (Θ) in a premise is at a smaller type, so F (Θ) is well-defined. Second, the only occurence of Θ is in the rule for session types, where it occurs guarded by a later modality. Thus, the fixed point of F existscall it Ω. Then, our logical relation at values is this − ≃ V Ω − : τ (which in the text we wrote without Ω annotation) The fact that Ω is a fixed point of F means that Note that v ≃ V Ω V : τ is affine for all v, V , and τ , and so is the lifting of Ω to expressions. Now we can explain the additional premise in the rule for receive. By default when we have l ≃ V Ω c s : ?τ. S, this would unfold to Session ⊲Ω (l, c s , recv(τ )S) -looking at the definition of state interpretation, we might be afraid that the returned message values v and V , might merely be related at ⊲ of Ω (τ ) in the postcondition, not at Ω (τ ). The key is that the premise above the line lets us "strip" off such a later: take P in that premise to be − ≃ V Ω − : τ . Then, the premise of the rule holds when , and so in the post condition we get out v ≃ V Ω V : τ without the later. This justifies the rule we presented in the paper (and which we use below in the proof of the fundamental lemma). We now lift this relation to one on open expressions in a given context. Given a map γ h from a finite domain of variables to closed expressions in the target language, we write [γ h ]e for the result of simultaneously substituting each variable in the domain of γ h for its image under γ h . [γ c ]E is the analogous thing for source expressions.
We define the relation Γ ⊢ e ≃ E : τ , where Γ is a typing context, by: where we take * over an empty set to be A(True). We now show that the logical relation is sound : Proof. By induction on τ : τ = Int: By assumption, we have that Emp ⊢ e ≃ E Ω E : Int. By the refinement rule, it suffices to prove: Since Emp is affine and persistent, we can clear the implicit modalities in the Hoare triple, and move the pre-condition to the context by using the wand intro rule, so that we need to show: By our assumption, we can rewrite this as: the definition of the lifting of Ω, instantiating it with i and [], clearing the afine modality, and then eliminating the resulting wand with source(i, e), we need By the rule of consequence of weakest precondition (i.e., , weakest precondition is covariant in the post condition), it suffices to show for aribtrary x, Which follows from the definition of ≈.
The other cases are the same: in each case, we take the assumption, apply the refinement proof rule; then the ownership we get in the pre-condition of the refinement triple is the antecedent of the wand in the definition of the lifting of the type relation to expressions; eliminating that gives a weakest precondition, where the post condition implies that values are logically related; our logical relation implies ≈, so we're done.
We now prove what is called the fundamental theorem: Proof. The proof is by induction on the derivation of Γ ⊢ E : τ .
-Case Var: x = x, so given closing subsitutions γ h and γ c , we need to show * and similarly for γ c , so this becomes * Note that Γ (x) = τ , so, manipulating * , this just becomes Since the interpretation is affine, we can throw away * x∈Γ \{x} and we are done. -Case Int: Again, n = n, and these are closed, so we just have to show, given substitutions: We can throw away the context, since it is affine and not needed. Then, our goal follows immediately from the fact that n ≃ V Ω n : Int, and we have already said that related values are related under the lifting, since Ω is affine.
-Case Fun-Intro: Once more, (λx. E) = λx. E. By our induction hypothesis, we have that Γ, Unfolding the definition on the right, we are given arbitrary v ′ , V ′ which are related at τ 1 , which we put in the context using the rule for for all introduction, affine introduction, and wand introduction; we then need to show: We step the source and target to do the beta reductions: We can then extend the substititons γ h and γ c to also map x to v ′ and V ′ respectively; call these γ ′ h and γ ′ c . Then, rewriting the above and regrouping our assertions to the left of the turnstile, we get: τ 2 } But now we can apply our induction hypothesis (suitably unrolling and instantiating everything).
-Case Fun-Elim: Our induction hypothesis says: Γ ⊢ E ≃ E : τ 1 ⊸ τ 2 and Γ ⊢ E ′ ≃ E ′ : τ 1 and we need to show, given closing substitutions γ h and γ c : Now, we unfold the lifting on the right and introduce the corresponding source ownership assertion: As in the previous case, we use the bind rule to focus on the left and then right subexpressions; applying our induction hypothesis about E 1 and E 2 then lets us trade our context assumptions to end up with some v 1 , V 1 , v 2 , V 2 for which it suffices to show: But this follows immediately from the unfolding of Ω at pair type. -Case Pair-Elim: The argument is similar to Fun-Intro, in the way that Pair-Intro corresponds to Fun-Elim, so we omit it. -Case Fork: Surprisingly, this too is similar to the cases for pair and function! The reader might have expected that this would in fact be a hard case; but it is not precisely because our lifting from value relation to expression relation is usiing the weakest precondition, so we'll be able to use the fork rule. To wit, we have by induction hypothesis that Doing the same routine of restricting the substitutions, splitting the context assumptions, unfolding the lifting relation, etc. we get that we need to show We start by applying the fork rule; we then do a step shift in the source to get source(j, [χ c ]E f ) for some new j, and the parent thread becomes source(i, E). We now split the context, passing the assumptions about Γ 1 the j source thread to a proof of weakest precondition for the child target thread; the rest is used in the target parent thread's proof. So we need to prove the following two entailments: τ } The latter follows from the induction hypothesis. For the former, using the induction hypothesis and the rule of consequence for weakest precondition means we just need to show, for all v, V : But the right side of the conjunction is affine, hence can be thrown away, and we have mentioned above that a source of a value entails Stopped.
-Case NewChTyp: At last we come to a case involving a channel. This expression is closed, it suffices to show: Unfolding the definition of value relation at pair type and session type, the left side matches the right side so we are done. -Case Send: Our induction hypothesis gives us that Γ ⊢ E 1 ≃ E 1 : !τ. S and Γ ⊢ E 2 ≃ E 2 : τ and we need to show, given closing substitutions γ h and γ c : Doing the usual routine of noting that the two subexpressions only have free variables in their respective contexts, taking restrictions, and unfolding everything: Notice that because the implementation of heapSend let-binds a pair containing the two "arguments", they are both evaluated first before substitution into the "body" of the send primitive. Hence, we first evaluate the left and then right subexpressions using our induction hypothesis, and then just have to show for all values v 1 , v 2 , V 1 , V 2 : But then, the relation of v 1 and V 1 unfolds to give us: We first evaluate the subexpression using our induction hypothesis, and then just to show for all values v, v: Again, the relation of v and V unfolds to give us: So we can use the proof rule for receive primitive on the left to get Applying the rule of consequence, and unfolding the interpretation at tensor and session type, we are done.
This completes the proof of the fundamental lemma. Then, Theorem 1 follows by combining the fundamental lemma and the soundness of the logical relation (Lemma 41): every well typed term is logically related to its translation, and the left side of a logically related pair refines the right side.

B.2 Craig-Landin-Hagersten Lock
In this part, we describe our second case study, which shows that the Craig-Landin-Hagersten queue lock[11, 31] refines a fair ticket lock [32]. Like the first case study, the results mentioned here have all been mechanized in Coq. Our goal here is simply to give a feel for what the result is about; we do not describe the actual proofs or the state transition systems we use. The interested reader should consult the Coq source.
Lock Implementations The code for the two types of locks appears in Figure 5. The FAI(−) operation is a fetch-and-increment: it takes a location as a parameter and atomically increments that location and returns the previous value. Meanwhile, swap(−, −) takes a location and a value and atomically loads the previous value of the location and stores the second parameter as the new value.
Each ticket lock consists of two references storing integers: the "owner" counter and the "next" counter, called o and n in the code, so ticketnew just allocates these two references. To acquire the lock, a thread atomically fetches and increments the next counter to get a number, which we call a "ticket" (ticketacq). It then spins on the owner counter waiting until the owner counter matches the thread's ticket number (ticketwait). Once it matches, the thread  enters the critical section. To release the lock, the thread increments the owner counter (ticketrel).
The lock is fair in the sense that once a thread calls ticketacq and completes its fetch-and-increment operation to get its ticket, it is guaranteed to enter the critical section before other threads that subsequently call ticketacq. Thus, if every thread which acquires the lock eventually releases it, every thread that tries to acquire the lock will eventually enter the critical section.
However, one drawback to this design is that every thread waiting to acquire the lock spins on the same owner counter location. Depending on the machine, this can cause poor performance for memory related reasons [32]. In contrast, in the CLH lock, every waiting thread spins on a different memory location. The rather extensive benchmarking done by David et al. [13] suggests that in some settings the CLH lock performs better than the ticket lock.
Conceptually, we can think of the CLH lock as consisting of a queue of threads, in the order that they tried to acquire the lock. The lock has two fields: a pointer to the head of the queue, and a pointer to the tail of the queue. Each node in the queue consists of a single boolean value. While this value is true, the node that owns that node is either (1) still waiting to enter the critical section, or (2) is in the critical section, but has not yet released the lock. When creating a new CLH lock, we create a dummy node in which this field is set to false, and set the head and tail to point to it (CLHnew). To acquire the lock, a thread allocates a new node and inserts itself at the back of the list by atomically swapping the location of the new node with the current tail (CLHacq) -the value returned by this atomic swap is the node of its predecessor in the list. The thread then spins on this node's boolean value until it is false -this indicates that the predecessor has released the lock, signalling that the thread is now at the head of the queue and may enter the critical section (CLHwait). Before entering the critical section, the thread therefore updates the head pointer to point to its node. To release the lock, the thread looks at the node pointed to by the head field, and sets that node to false (CLHrel).
Observe that, as claimed, each waiting thread spins on a different location: the node of its predecessor in the list.
There is one important difference between our implementation and typical versions. Usually, there is no head pointer, and the API is designed so that the acquire method take two parameters: (1) the lock, and (2) the new node to be added to the list, while the release method takes only the releaser's node. This means conventionally it is not a drop-in replacement for the ticket-lock, because in the ticket lock, both acquire/release take the lock structure as their only parameter. That said, the head pointer may have other uses and is included in some implementations [26].
Refinement Specification Note that the CLH lock is fair in the same sense as the ticket lock: once a thread completes its atomic swap to insert itself into the queue, it must enter the critical section before threads that later call CLHacq. If one ignores all the parts of the above specification that have to do with our extensions (delay constants, refinement resources, and the affine modality), this looks like a standard specification for a lock primitive in a higherorder concurrent separation logic (indeed, this kind of specification is proved about the ticket lock in the original Iris repository). Such a specification says that for an arbitrary assertion R, if one initially owns R, it can be given up to create a lock protecting R -in exchange, one gets an assertion isLock(−, −, −, −) which is duplicable. Then, a thread can use this assertion to call acquire, and afterward it back R, and an assertion locked(−, −, −) which signifies that it is the owner of the lock. Both R and locked(−, −, −) are needed to then call release. Thus this typical formulation of a lock specification rules out the kind of counter-examples we illustrated above. Re-reading the specification with the parts relevant to our extension, we see that each shows a refinement from the corresponding ticket lock primitive. Of course, one can use these rules, along with the rest of the logic, to prove that for a given program, if one replaces the ticket primitives with the CLH versions, the result is a refinement. If the reader is familiar with the "usual" specification of lock primitives in higher-order CSL, hopefully the above description is compelling evidence that this refinement specification is "good enough". In the next section, we describe a particular use of these proof rules to show that for a large class of well-typed programs, the desired refinement holds.
Type-directed translation We now describe a simple type-directed translation from programs using the ticket primitives to ones using the CLH primitives. We then construct a logical relation which uses the weakest precondition specification described above to show that the translated programs refine their sources.
The translation is shown in Figure 6. We write Γ ⊢ e e ′ : τ to indicate that in context Γ , the expression e translates to e ′ at type τ . The type system used in the translation is a standard simple type system for MiniML with references, extended with an abstract type Lock for locks. In contrast to the session-typed language, the type system here is fully structral, not affine. The primitive ticketnew translates to CLHnew and returns a value of type Lock (Lock-Intro). This lock can be used with the command ticketsync, which takes a ticket lock and a function of type Unit → τ and synchronizes execution of the function with the lock (Lock-Elim). This translates to CLHsync, which does the same thing but using the CLH lock implementation.
Because these "synchronize" commands properly acquire and then release the lock, a the type system rules out the kinds of bad programs we mentioned above. Of course, this is a very restricted way of using the lock. Our point is just to show that the weakest precondition specification supports this kind of use; it in fact is more flexible, but a type system that demonstrated this would be more complex (at which point, one might want to just appeal to the program logic directly to prove the refinement).
As usual, to state our refinement result, we need to give a notion of observational equivalence on values. Here, we restrict our attention to booleans and say that given two booleans b and b ′ , b ≈ b ′ if and only if b = b ′ . With this notion of value equivalence as our foundation for refinement, we have mechanized the following result: Theorem 43. If · ⊢ e e ′ : Bool then e ′ ⊑ e.
To prove this theorem, we once again construct a logical relation. 14 This is very much like the relation given for the session typed language, with two notable exceptions (1) the type system is not affine, so all the interpretations of the types in the relation are both affine and relevant propositions (meaning they can be duplicated and thrown away, freely), (2) we need to model reference and lock types. For references and locks we have: isLock(γ, lk, lk ′ , True) lk ≃ V lk ′ : Lock where the boxed assertion in the premise of the second rule is an Iris invariant. These were not described in the main text, so the reader unfamiliar with the original work on Iris can think of them as a single-state STS 15 . The first rule means that lock types are just interpreted as the isLock(−, −, −, −) assertion we saw before. The fourth parameter is True because for purposes of the type translation, we don't care what resource the programmer is intending to protect with the lock. The second says that two heap locations are related at reference 14 The logical relation in our Coq formalization is actually formulated generically with respect to a pair of lock implementations, assumed to satisfy weakest precondition specifications like the ones given above for the ticket and CLH lock. The mechanization then instantiates this generic formulation with the particular results about the ticket and CLH locks. 15 In fact, the STS construct is derived from invariants.
type Ref τ if there is an invariant enforcing that they must always point to values that are related at the interpretation of τ .
Using these definitions, we can prove a fundamental lemma showing that if · ⊢ e e ′ : τ , then e ≃ E e ′ : τ holds. Then, we show a soundness lemma that states that if e ≃ E e ′ : Bool, then e ⊑ e ′ . By composing these two results, we obtain Theorem 43.