ReLoC Reloaded: A Mechanized Relational Logic for Concurrency]ReLoC Reloaded: A Mechanized Relational Logic for Fine-Grained Concurrency and Logical Atomicity

Dan Frumina
aUniversity of Groningen and Radboud University

Robbert Krebbersb
bRadboud University and Delft University of Technology

Lars Birkedalc
cAarhus University

We present a new version of : a relational separation logic for proving refinements of programs with higher-order state, fine-grained concurrency, polymorphism and recursive types.
The core of is its refinement judgment $\logrel{}{\expr}{\expr'}{\type}$, which states that a program $\expr$ refines a program $\expr'$ at type $\type$.
provides type-directed structural rules and symbolic execution rules in separation-logic style for manipulating the judgment, whereas in prior work on refinements for languages with higher-order state and concurrency, such proofs were carried out by unfolding the judgment into its definition in the model.
's abstract proof rules make it simpler to carry out refinement proofs, and enable us to generalize the notion of logically atomic specifications to the relational case, which we call logically atomic relational specifications.

We build on top of the Iris framework for separation logic in Coq, allowing us
to leverage features of Iris to prove soundness of , and to carry out refinement proofs in .
We implement tactics for interactive proofs in , allowing us to mechanize several case studies in Coq, and thereby demonstrate the practicality of .

extends (LICS'18) with various technical improvements, a new Coq mechanization, and support for Iris's prophecy variables.
The latter allows us to carry out refinement proofs that involve reasoning about the program's future.
We also expand 's notion of logically atomic relational specifications with a new flavor based on the HOCAP pattern by Svendsen .

§ INTRODUCTION

A fundamental question in computer science is when two programs are equivalent?
The “golden standard” of program equivalence is contextual equivalence, stated directly in terms of the operational semantics.
Intuitively, expressions $\expr$ and $\expr'$ are contextually equivalent

if no well-typed client can distinguish them, which formally means that for all well-typed contexts $\pctx$, the expression $\fillctx\pctx[\expr]$ has same observable behaviors as $\fillctx\pctx[\expr']$.
Contextual equivalence can be further decomposed into contextual refinement.
An expression $\expr$ contextually refines $\expr'$
if, for all contexts $\pctx$, if $\fillctx\pctx[\expr]$ has some observable behavior, then so does $\fillctx\pctx[\expr']$.
Expressions $\expr$ and $\expr'$ are contextually equivalent iff $\expr$ contextually refines $\expr'$ and vice versa.

Contextual refinement and contextual equivalence have many applications in computer science.
One such application is to specify programs in terms of other programs.
For example, one can specify an implementation of a program module (say, a map) that internally uses an efficient but complicated data structure (say, a balanced search tree) by stating that it refines an implementation that internally uses an inefficient but easy to understand data structure (say, an unordered list).
In the context of a typed language that supports data abstraction, a specification of a program module in terms of refinement shows that clients of the program module cannot depend on the internal representation of data.
This can be seen as an instance of the representation independence principle [86, 72].

In the context of concurrency, contextual refinement is often used to specify a fine-grained concurrent program module by stating that it contextually refines a coarse-grained version.
This is similar to showing that a fine-grained program module is linearizable [52, 43], each fine-grained operation appears to take place instantaneously.
A simple example is the specification of a fine-grained concurrent counter by a coarse-grained one, see <Ref> for the code.
The increment operation of the fine-grained version, $\FGcounter$, takes an “optimistic” lock-free approach to incrementing the value using a compare-and-set operation inside a loop.
If the value of the counter has been changed (for instance, by some other thread), then the fine-grained counter reattempts the increment from the beginning.
The increment operation of the coarse-grained version, $\CGcounter$, is performed inside a critical section guarded by a lock.
We can state the desired refinement as follows:

\begin{equation*}
\FGcounter \ctxrel \CGcounter : (\tunit \to \tint) \times (\tunit \to \tint).
\end{equation*}

Due to the instrumentation of the coarse-grained version with locks, this refinement expresses that each operation of the fine-grained version takes place instantaneously.
We will use the counter as a simple running example throughout the paper.

Another application of contextual refinement and contextual equivalence is to state algebraic properties of program constructs.
For example, let us consider the non-deterministic choice operator $\expr_1 \orOp \expr_2$, which non-deterministically executes the expression $\expr_1$ or $\expr_2$.
Using contextual equivalence, we can state that this operator is
commutative (${\expr_1 \orOp \expr_2} \ctxequivsymb {\expr_2 \orOp \expr_1}$),
associative (${\expr_1 \orOp (\expr_2 \orOp \expr_3)} \ctxequivsymb {(\expr_1 \orOp \expr_2) \orOp \expr_3}$),
and that sequential composition distributes over the operator
$({(\expr_1 \orOp \expr_2) ; \expr_3} \ctxequivsymb {(\expr_1 ; \expr_3) \orOp (\expr_2 ; \expr_3)}$).

\begin{align*}
\intertext{\raggedright\textbf{Fine-grained grained version (\ie the implementation)}:}
\counterread \eqdef{}& \Lam \cntvar. \deref \cntvar \\
\FGincrement \eqdef{}& \Rec {\lvar{inc}} \cntvar =
\begin{array}[t]{@{} l}
\Let n = \deref \cntvar in \\
\If \CAS{\cntvar}{n}{1 + n} then n \Else \lvar{inc}\ \cntvar
\end{array} \\
\FGcounter \eqdef{}& \Let \cntvar = \Ref(0) in ((\Lam \unittt.\counterread\ \cntvar),(\Lam \unittt. \FGincrement\ \cntvar)) \\
\intertext{\raggedright\textbf{Coarse-grained version (\ie the specification)}:}
\CGincrement \eqdef{}& \Lam \cntvar\, l.
%\begin{array}[t]{@{} l}
\acquire\ l;\  %\\
\Let n = \deref \cntvar in \cntvar \gets (1 + n);\
\release\ l;\ n
\\
\CGcounter \eqdef{}& \Let l = \newlock\ \unittt in
\Let \cntvar = \Ref(0) in
((\Lam \unittt.\counterread\ \cntvar),(\Lam \unittt. \CGincrement\ \cntvar\ l))
\end{align*}

A fine-grained and coarse-grained concurrent counter.
(Note that the $\counterread$ operation is shared by both.)

§.§ Proving contextual refinement and contextual equivalence

Contextual refinement $\expr \ctxrel {\expr'} : \type$ (and contextual equivalence $\expr \ctxequivsymb {\expr'} : \type$) are very strong notions because they relate the expressions $\expr$ and $\expr'$ in any well-typed context $\pctx$ with a hole of type $\type$.
As a consequence, proving contextual refinement and equivalence directly is challenging—one has to consider arbitrary contexts $\pctx$, which are only known to be well-typed.
Contextual refinement and equivalence are therefore typically proved indirectly using approaches based on bisimulations ( [44, 81, 69, 93]) or logical relations ( [82, 6, 28, 23, 102]).
In the present paper we focus on approaches based on logical relations because they scale well to increasingly rich programming languages with features such as impredicative polymorphism, recursive types, higher-order state, and fine-grained concurrency.

In the approaches based on logical relations, the key is a notion of logical refinement, notation $\logrel {} \expr {\expr'} \type$.
Logical refinement is defined by structural recursion over the type $\type$, rather than by quantification over all contexts.
The soundness theorem of logical relations states that logical refinement implies contextual refinement, that $\logrel {} \expr {\expr'} \type$ implies $\expr \ctxrel {\expr'} : \type$.
As a result, proving contextual refinement can be reduced to proving logical refinement, which is generally much easier.

Unfortunately, it is difficult to construct a suitable notion of logical refinement when considering language features like recursive types and higher-order state.
In the presence of (general) recursive types, no structurally-recursive definition over the type exists, and in the presence of higher-order references, one needs some notion of recursively-defined worlds [22].
The technique of step-indexing [1, 5] has been used to stratify the definitions using recursion over a natural number, called the step-index, which corresponds to the number of computation steps performed by the program.

Step-indexing has shown to be very effective by a large body of work on step-indexed logical relations,  [77, 48, 23, 25, 87].
However, definitions and proofs are intricate because step-indices appear practically everywhere—they even appear in definitions and proofs related to language features (say, products or sums) for which step-indexing is orthogonal.
Dreyer thus proposed the “logical approach” to logical relations [28, 34] to hide step-indices by abstracting and internalizing them in a modal logic using the later modality ($\later$) [9].
Turon  [102, 97] further developed the logical approach by using separation logic [79, 78, 21] to abstract over program states and to handle (fine-grained) concurrency.

More recently, Krebbers  [68] and Timany [98] defined a logical relation for program refinement based on the work of Turon in the state-of-the-art higher-order concurrent separation logic Iris [58, 61, 57, 64].
Iris supports impredicative invariants [88] and used-defined ghost state, which can be used to streamline the definition of the logical relation, and to carry out proofs of challenging program refinements.
The meta theory of Iris is mechanized in the Coq proof assistant, and Iris comes equipped with a proof mode [68, 65]—an extensive set of Coq tactics for separation logic proofs—which allowed them to mechanize all their results in Coq.

§.§ Problem statement and key idea

To prove refinements of complicated program modules in a scalable fashion, it is important to decompose refinement proofs into smaller refinements that can be proved in isolation.
As a simple example, let us consider the refinement of the fine-grained and coarse-grained concurrent counter from <Ref>:

\begin{equation*}
\FGcounter \ctxrel \CGcounter : (\tunit \to \tint) \times (\tunit \to \tint).
\end{equation*}

We wish to decompose the proof of this refinement into refinements for the read and increment operations.
Naively, one might consider proving contextual refinements for these operations.
Unfortunately, such contextual refinements do not hold—they only hold conditionally under the assumption that the internal state in both of the implementations is related (including the state of the lock used by the coarse-grained version).

Instead of performing composition at the level of contextual refinement, our key idea is to perform composition at the level of logical refinement.
By generalizing logical refinement to become an internal (first-class) notion in (the Iris) separation logic, we can use the connectives of separation logic to express conditional refinements.
Logical refinements for the operations of the concurrent counter are as follows:

\begin{align*}
\knowInv{}{\counterinv} \wand{}&
\logrel{}{(\Lam \unittt. \counterread\ c_i)}{(\Lam \unittt. \counterread\ c_s)}{\tunit \to \tint}
\\
\knowInv{}{\counterinv} \wand{}&
\logrel{}{(\Lam \unittt.\FGincrement\ c_i)}{(\Lam \unittt.\CGincrement\ c_s\ \lkvar)}{\tunit \to \tint}.
\end{align*}

We use the magic wand ($\wand$, also known as separating implication) to make these refinements conditional under the invariant $\counterinv$ (expressed using Iris's invariant connective $\knowInv {} I$), which is defined as $\counterinv \eqdef \Exists n \in \nat. c_i \mapstoI n * c_s \mapstoS n * \isLock{\lkvar}{\<false>}$.
The invariant $\counterinv$ intuitively expresses that in between function calls, the values of both counters are equal, and the lock (used in the coarse-grained implementation) is in unlocked state.
With logical refinements for the individual operations at hand, we can compose them into the logical refinement ${\logrel {} \FGcounter \CGcounter {(\tunit \to \tint) \times (\tunit \to \tint)}}$, which using soundness gives us the desired contextual refinement ${\FGcounter \ctxrel \CGcounter : (\tunit \to \tint) \times (\tunit \to \tint)}$.

Treating logical refinement as an internal notion in separation logic succinctly distinguishes our work from prior work.
In prior work on refinements for rich languages, the aforementioned work by Turon  [102, 97], Krebbers  [68], and Timany [98], logical refinement is an external notion (a proposition in ordinary mathematics, rather than in separation logic), which means that one cannot concisely state refinements that are conditional on the program state.
To state and prove such refinements, one needs to unfold the definition of the logical refinement into the model.

Apart from being able to decompose refinement proofs, internalizing logical refinement gives us a number of other tangible benefits.
First, it allows us to develop type-directed structural rules and symbolic execution rules for proving logical refinements.
Our symbolic execution rules closely resemble the typical rules for symbolic execution in separation logic, but come in two forms: for the program on the left-hand side and right-hand side of the refinement, making it possible to write concise proofs.

Second, by internalizing logical refinement we can state logical refinements that apply to the situation when the expression on the one side of the refinement contains a program subject to specification, while the expression on the other side is arbitrary.
We call such specifications relational specifications.
Relational specifications take the ability to decompose refinement proofs one step further.
As a simple example, let us consider the example from <Ref>, where we proved that a fine-grained concurrent counter refines a coarse-grained version.
This refinement is insufficient if we want to prove that a program module that uses internally the fine-grained counter (say, a ticket lock) refines another module that does not use the coarse-grained counter (say, a spin lock).
However, we can instead formulate a relational specification for the program module that is proven just once, and derive different logical (and thus by soundness, contextual) refinements from it.

A key challenge in stating relational specifications for operations is to concisely capture that they behave as-if they were atomic, they appear to take place instantaneously.
There has been a long line of work on logically atomic specifications to reason about atomicity in the context of Hoare-style logics [60, 89, 36, 61, 59].
We show that such logically atomic specifications generalize to the relational case, and call them logically atomic relational specifications.
Concretely, we introduce relational specification patterns based on da Rocha Pinto 's TaDA-style [36] and Svendsen 's HOCAP-style [89] logically atomic specifications.

§.§ The logic

Based on the previously described key ideas, we develop a relational separation logic called .
is built on top of Iris, allowing the user to leverage the features of Iris such as invariants, (higher-order) ghost state, and prophecy variables.
Invariants and ghost state state are powerful mechanisms that support reasoning about concurrent programs through used-defined protocols.
Prophecy variables [7, 59] allow for speculative reasoning about the future state of concurrent programs.
In Iris they come in the form of ghost variables whose value can be referenced before they are specified, thus allowing one to “prophesize” their potential value.
We show how these features can be used in to prove challenging refinements.

We have implemented as a shallow embedding on top of Iris in Coq [68, 65].
In addition to mechanizing all meta-theoretic results of , like its soundness theorem, we have implemented new tactics that support mechanized interactive reasoning about program refinements in in a practical and modular way.
To our knowledge, is the first fully mechanized relational logic enabling reasoning about contextual refinements of programs in a fine-grained concurrent higher-order imperative programming language.
The mechanization can be found at [41].

§.§ Contributions and structure of the paper

* We present a relational logic  for reasoning about contextual refinements of fine-grained concurrent higher-order imperative programs.
We present our target programming language (<Ref>), an overview of (<Ref>), and a detailed description of its type-directed structural rules and symbolic execution rules (<Ref>).

* We introduce relational specification patterns based on TaDA [36] and  HOCAP-style [89] logically atomic specifications (<Ref>).

* We show how to integrate prophecy variables into ReLoC, thereby enabling speculative reasoning in proofs of program refinements (<Ref>).

* We describe the logical relations model of in Iris (<Ref>).

* We describe the mechanization of in Coq, and explain how we support mechanized interactive reasoning in in a practical and modular way (<Ref>).

We discuss further related work in <Ref> and conclude in <Ref>.

In addition to the case studies presented in this paper, we have also verified a collection of refinements of concurrent programs from the literature.
We give a brief overview of these examples in <Ref>; and the proofs can be found in the accompanying Coq sources.

§.§ Differences with the conference version of this paper

In the conference version of this paper [40] we described the first version of .
This paper extends the conference paper in two ways.
First, we introduce (in this paper referred to as just ), which has several new features, especially in terms its Coq mechanization.
Second, we have expanded the presentation of, as well as the material covered by, the paper significantly.
Concretely, has the following new features compared to its original version:

* 's primitive refinement judgment $\logrel{}{\expr}{\expr'}{\type}$ is defined for closed expressions (without free variables), and the version for open expressions (with free variables) is a derived notion (see <Ref>).

* 's underlying programming language is —the default language of Iris's Coq mechanization.
By having a tight integration of with Iris's Coq ecosystem we managed to reuse more Coq code and integrate novel Iris features.

* One such feature that we have integrated into is the support for prophecy
variables (<Ref>), which was recently added to Iris [59].

Compared to the conference paper, we have significantly expanded <Ref>, and added <Ref>, which are completely new.
We have extended <Ref> with HOCAP-style specifications, which we put into action by verifying a refinement between a ticket lock and a spin lock in <Ref>.

§ THE PROGRAMMING LANGUAGE

We consider a typed version of , the default language that is shipped with Iris's Coq development [54].
is a call-by-value $\lambda$-calculus, with higher-order references, fork-based unstructured concurrency, and atomic operations for fine-grained concurrency, equipped with System-$\mathsf{F}$-style types.
The syntax is shown in <Ref>.
We let $\tvar$ range over a countably infinite set $\TVar$ of type variables, which can be bound by the universal type $\tforall{\tvar. \type}$, existential type $\texists{\tvar . \type}$, and recursive type $\trec{\tvar. \type}$.
We omit the usual Boolean and arithmetic operations such as addition, multiplication, equality, negation.

\begin{align*}
\type \in \Type \bnfdef{}&
\tvar \ALT
\tunit \ALT
\tbool \ALT
\tint \ALT
\type_1 \times \type_2 \ALT
\type_1 + \type_2 \ALT
\type_1 \to \type_2 \ALT
\tforall{\tvar. \type} \ALT
\texists{\tvar. \type} \ALT
\trec{\tvar. \type} \ALT
\tref\ \type \\
\val \in \Val \bnfdef{}&
i \ALT
\loc \ALT
\<true> \ALT
\<false> \ALT
(\val_1, \val_2) \ALT
\<inl>(\val) \ALT
\<inr>(\val) \ALT
\Rec f \var = \expr \qquad i \in \mathbb{Z}, \loc \in \Loc \\ & \ALT
\tlam{\expr}\ALT
\<pack>\ \val \ALT
\<fold>\ \val \\
\expr \in \Expr \bnfdef{}&
\var \ALT
\val \ALT
\If \expr then \expr_1 \Else \expr_2 \ALT
(\expr_1, \expr_2) \ALT
\proj_i(\expr) \ALT
\<inl>(\expr) \ALT
\<inr>(\expr) \qquad i \in \{1, 2\} \\ & \ALT
(\Match \expr with \<inl>(\var) \to \expr_1 \mid \<inr>(\var) \to \expr_2) \ALT
\expr_1 (\expr_2) \ALT
\tapp{\expr} \\ & \ALT
\<pack>(\expr) \ALT
\unpack{\expr_1}{\Ret \var. \expr_2} \ALT
\<fold>\ \expr \ALT
\<unfold>\ \expr \\ & \ALT
\Ref(\expr) \ALT
\deref \expr \ALT
\expr_1 \gets \expr_2 \ALT
\CAS{\expr_1}{\expr_2}{\expr_3} \ALT
\Fork{\expr} \ALT
\dots
\end{align*}

The syntax of the language.

Most of the operations are standard, so we only discuss some subtleties.
Type abstraction $\tlam{\expr}$, type application $\tapp{\expr}$, and the $\<pack>$/$\<unpack>$ constructs for packing/unpacking existential types do not contain type annotations, following  [6].
The $\<fold>$/$\<unfold>$ constructs are used to fold/unfold iso-recursive types.
The language includes standard operation on references $\Ref(\expr)$ for allocation, $\deref\expr$ for dereferencing, and $\expr_1 \gets \expr_2$ for assignment.
The atomic compare-and-set operation $\CAS{\expr_1}{\expr_2}{\expr_3}$ checks if the value stored at the location $\expr_1$ is equal to $\expr_2$, and, if so, sets the value at $\expr_1$ to $\expr_3$.
The $\Fork\expr$ construct creates a new thread, which will execute the expression $\expr$.

Selected typing rules:

() =

_1 ×_2 i ∈{1, 2}
f x=_1 →_2
pack> .
, _1_2_2

_1. _2_2

fold> .
unfold> .

_1 _2

Selected rules of pure reduction
$\pureexec {\expr_1} {\expr_2}$
and thread-local call-by-value head-reduction
$(\expr,\stateS) \hstep (\expr',\stateS')$:

_i (_1, _2) _i
(f x = e)
exvff x = e
(pack> ).
unfold> (fold> )
_1 _2
(_1, ) (_2, )
() =
((), ) (, )
() =
(, ) (, )
() =
(', ) (, ')
() ≠_1
(_1_2, ) (false>, )
() = _1
(_1_2, ) (true>, _2)

Thread-pool reduction
\((\vec\expr,\stateS) \tpstep (\vec{\expr'},\stateS')\):

(,) (',')
(_⃗1⃗ [] _⃗2⃗, )
(_⃗1⃗ ['] _⃗2⃗, ')

(_⃗1⃗ [] _⃗2⃗, )
(_⃗1⃗ [] _⃗2⃗ , )

The type system and operational semantics of .

Syntactic sugar.
We use syntactic sugar to define non-recursive functions, let-bindings, and sequential composition.
We let $(\Lam \var. \expr) \eqdef (\Rec \_ \var = \expr)$ and
$(\Let \var = \expr_1 in \expr_2) \eqdef ((\Lam \var. \expr_2)\ \expr_1)$ and
$(\expr_1 ; \expr_2) \eqdef (\Let \_ = \expr_1 in \expr_2)$.
The underscore $\_$ denotes an anonymous binder, a fresh variable that is unused in the body of the binding expression.

Type system.
Typing judgments take the form \(\typed \tenv \vctx \expr \type\),
where \(\vctx\) is a context assigning types to program variables, and $\tenv$ is a context of type variables.
The inference rules for the typing judgments are standard; a selection of representative rules is given in <Ref>.
The typing rule for the compare-and-set ($\<CAS>$) operation has a side-condition $\EqType(\type)$, which ensures that a compare-and-set can only be performed on word-sized data types, the unit, Boolean, integer, and reference type.

Operational semantics.
The operational semantics involves three reduction relations:
pure head reduction $\ra_{\mathsf{pure}}$,
thread-local head reduction \(\hstep\), and thread-pool reduction \(\tpstep\), see
<Ref> for the rules.
Head reduction \(\hstep\) is lifted to thread-pool reduction \(\tpstep\) using standard call-by-value evaluation contexts (in the style of Felleisen and Hieb [39]):

\[
\lctx \in \Ectx \bnfdef{}
\hole \ALT
\expr_1(\lctx) \ALT
\lctx(\val_2) \ALT
\expr_1 \gets \lctx \ALT
\lctx \gets \val_2 \ALT \dots
\]

Thread-pool reduction \(\tpstep\) is defined on configurations \(\cfgg = (\vec\expr,\stateS)\)
consisting of a state \(\stateS\) (a finite partial map from locations to
values) and a thread-pool \(\vec\expr\) (a list of expressions corresponding to the
by interleaving, by picking a thread and executing it, thread-locally, for one step.
The only special case is \(\Fork{\expr}\),
which spawns a thread \(\expr\), and reduces itself to the unit value \(\unittt\).

Contextual refinement.
The notion of contextual refinement that we use is standard (see, [82] or <cit.>).
It formalizes the situation when the set of observations that can be made about the first program is a subset of observations that can be made about the second program.
An observation about a program are made using a program context $\pctx$, which is a program with a hole:

\begin{align*}
\pctx \in \Pctx \bnfdef{}&
\Box \ALT
\Rec f \var = \pctx \ALT
\pctx (\expr_2) \ALT
\expr_1 (\pctx) \ALT
\tlam\pctx \ALT
\tapp{\pctx} \ALT
\dots
\end{align*}

Since we are in a typed setting, we consider only typed contexts.
A program context is well-typed, denoted as $\typedctx{\pctx}{\tenv}{\vctx}{\type}{\tenv'}{\vctx'}{\type'}$, if
for any term $\typed{\tenv}{\vctx}{\term}{\type}$ we have $\typed{\tenv'}{\vctx'}{\fillctx\pctx[\term]}{\type'}$.
The typing relation on contexts is standard, and can be derived from the typing rules in <Ref>.

We then define contextual refinement as follows.
An expression $\expr_1$ contextually refines an expression $\expr_2$ at type $\type$, denoted as $\ctxref{\tenv \mid \vctx}{\expr_1}{\expr_2}{\type}$, if no well-typed program context $\pctx$ resulting in a closed program can distinguish the two:

\begin{align*}
\ctxref{\tenv \mid \vctx}{\expr_1}{\expr_2}{\type} \eqdef{}&
\All \type'\,
\val\; \vec{\expr_f}\; \stateS. \\& \qquad\qquad
(\fillctx\pctx[\expr_1], \emptyset) \tpstep^{\ast} (\conS{\val}{\efs}, \stateS) \implies \\ & \qquad\qquad
\Exists \val'\; {\vec{\expr'_{f}}}\; \stateS'. (\fillctx\pctx[\expr_2], \emptyset) \tpstep^{\ast} (\conS{\val'}{\vec{\expr'_{f}}}, \stateS').
\end{align*}

Contextual equivalence $\ctxequiv{\tenv \mid \vctx}{\expr_1}{\expr_2}{\type}$ is defined as the symmetric closure of contextual refinement, $(\ctxref{\tenv \mid \vctx}{\expr_1}{\expr_2}{\type}) \wedge (\ctxref{\tenv \mid \vctx}{\expr_2}{\expr_1}{\type})$.

Note that contextual refinement only takes termination into account, and does not require the resulting values $\val$ and $\val'$ to be equal.
Demanding the equality on the resulting values would make contextual refinement too strong.
For example, the terms $(\Lam x. x + 1)$ and $(\Lam x. 1 + x)$ of function type would not be deemed contextually equivalent, because they terminate to syntactically different values in the empty program context.

There are, however, equivalent formulations of contextual refinement which equate the resulting values $\val$ and $\val'$.
In order to do that, it is necessary to restrict the typed context $\typedctx{\pctx}{\tenv}{\vctx}{\type}{\emptyset}{\emptyset}{\type'}$ to those for which $\type'$ is a directly observable type, like Booleans or integers.
For example, we could have used the following equivalent[Proving that this definition is equivalent to the one presented earlier is not a very complicated, albeit laborious, task. See the Coq mechanization for the formal proof.] definition (a variation of $\<true>$-adequate contextual equivalence from <cit.>):

\begin{align*}
% \ctxref{\tenv \mid \vctx}{\expr_1}{\expr_2}{\type} \eqdef{}&
&  \All (\typedctx{\pctx}{\tenv}{\vctx}{\type}{\emptyset}{\emptyset}{\tbool})\;
\vec{\expr_f}\; \stateS. \\& \qquad\qquad
(\fillctx\pctx[\expr_1], \emptyset) \tpstep^{\ast} (\conS{\<true>}{\efs}, \stateS) \implies
\Exists {\vec{\expr'_{f}}}\; \stateS'. (\fillctx\pctx[\expr_2], \emptyset) \tpstep^{\ast} (\conS{\<true>}{{\vec{\expr'_{f}}}}, \stateS').
\end{align*}

§ A TOUR OF

This section gives a tour of by demonstrating its key logical connectives and proof rules.
We first describe 's grammar, soundness statement, and rule format (<Ref>).
After that, we put to action by proving contextual refinements of two program modules.
The first is a bit module, which demonstrates 's type-directed structural rules and symbolic execution rules for reasoning about pure programs (<Ref>).
The second is the concurrent counter module from <Ref>, which involves reasoning about internal state and concurrency.
Specifically we demonstrate how is used to reason about stateful programs
using symbolic execution (<Ref>),
concurrency using invariants (<Ref>),
and recursive functions and loops using Löb induction (<Ref>).

§.§ Grammar and soundness

is based on higher-order intuitionistic separation logic, and the grammar of its propositions is:

\begin{align*}
\propMV, \propMVB \in \Prop \bnfdef{}&
\TRUE \ALT \FALSE \ALT
\All \var.\propMV \ALT
\Exists \var.\propMV \ALT
\propMV \wedge \propMVB \ALT
\propMV \vee \propMVB \ALT
\propMV \implies \propMVB \\ & \ALT
\propMV * \propMVB \ALT
\propMV \wand \propMVB \ALT
\loc \mapstoI \val \ALT
\loc \mapstoS \val \ALT
(\logrel[\mask]{\Delta}{\expr_1}{\expr_2}{\type}) \\ & \ALT
\logrelV{\type}{\Delta}{\val_1}{\val_2} \ALT
\knowInv\namesp\propMV \ALT
\later \propMV \ALT
\always \propMV \ALT
\pvs[\mask_1][\mask_2] \propMV \ALT \dots
\end{align*}

is an extension of Iris and therefore includes all connectives of Iris, in particular, the later modality $\later$, persistence modality $\always$, update modality $\pvs[\mask_1][\mask_2]$, and invariant assertion $\knowInv \namesp \propMV$.
We introduce these connectives in passing throughout this section.
Some of these connectives are annotated by invariant masks $\mask \subseteq \InvName$ and invariant names $\namesp \in \InvName$, which are needed for bookkeeping related to Iris's invariant mechanism.
Until we introduce invariants in <Ref>, we will omit these annotations.
Similarly, we will ignore the later modality $\later$ until we explain it in <Ref>.

An essential difference to vanilla Iris is that has internal (or first-class) refinement judgments $\logrel{\Delta}{\expr_1}{\expr_2}{\type}$, which should be read as “the expression $\expr_1$ refines the expression $\expr_2$ at type $\type$”.
Just like contextual refinement, the refinement judgment in is indexed by a type $\type$.
The judgment contains an environment $\Delta$ which assigns interpretations to type variables.
These interpretations are given by an Iris relation of type
$\Val \times \Val \to \Prop$.
One such kind of relation, the value interpretation relation $\logrelV{\type}{\Delta}{-}{-} : \Val \times \Val \to \Prop$ (for each syntactic type $\type$ of ) will be discussed in <Ref>.
We elide the contexts $\Delta$ in refinement judgments whenever they are empty.

The intuitive meaning of $\logrel{\Delta}{\expr_1}{\expr_2}{\type}$ is that $\expr_1$ is safe, and all of its behaviors can be simulated by $\expr_2$.
It is a simulation in the sense that any execution step of $\expr_1$ can be matched by a (possibly empty) sequence of execution steps of $\expr_2$.
Borrowing the terminology from languages with non-determinism, we think of $\expr_1$ as being demonic and $\expr_2$ as being angelic.
That is, the non-deterministic choices of $\expr_1$ (scheduling of forked-off threads) are selected by an external demon; whereas for the non-deterministic choices of $\expr_2$, an angle blesses the person proving the refinement with an ability to select a choice themselves.

Since we often use refinement judgments to specify programs, we refer to the left-hand side $\expr_1$ as the implementation, and to right-hand side $\expr_2$ as the specification.
The intuitive meaning is formally reflected by the soundness theorem contextual refinement.

If the refinement judgment $\logrel{\emptyset}{\expr_1}{\expr_2}{\type}$ is derivable in , then $\ctxref{\emptyset \mid \emptyset}{\expr_1}{\expr_2}{\type}$.

In this section we only consider closed programs $\expr_1$ and $\expr_2$; we will see how (and its soundness theorem) generalize to open terms in <Ref>.

Like ordinary separation logic, has heap assertions.
Since is relational, these come in two forms: $\loc \mapstoI \val$ and , which signify ownership of a location $\loc$ with value $\val$ on the implementation and specification side, respectively.

Contrary to earlier work on logical refinements in Iris,  [68, 98], refinement judgments $\logrel{\Delta}{\expr_1}{\expr_2}{\type}$ in are first-class propositions.
As such, we can combine them in arbitrary ways with the other logical connectives, and state conditional refinements.
For example, the proposition

\begin{equation}
\label{reloc:eq:cond_refinement}
(\loc_1 \mapstoI \val_1 * \loc_2 \mapstoS \val_2 *
\logrel{\Delta}{\expr_1'}{\expr_2'}{\typeB})
\wand{}
\logrel{\Delta}{\expr_1}{\expr_2}{\type},
\end{equation}

states that the $\expr_1$ refines $\expr_2$, under the assumption of another refinement and that certain locations have specified values in the heap.
Having conditional refinements is crucial for modularity, as it allows us to formulate and prove refinements of individual methods of a data structure under the assumptions provided by the internal invariant of the data structure.
The fact that refinement judgments are first class also plays an important role in the presentation of 's proof rules.

§.§ Derivability and inference rules

As standard in logic, Iris/has a derivability relation $P \proves Q$.
We say that $Q$ is derivable if $\TRUE \proves Q$.
In many situations, we use magic wand $\wand$ instead of the derivability relation $\proves$, because we have the standard deduction property:

\[
P \proves Q \wand R \qquad\textnormal{iff}\qquad P \ast Q \proves R
\]

Most of the inference rules we present can be internalized as propositions by a magic wand or a derivability relation between the separating conjunction of the antecedents and the consequent.
We thus use the following notations:

\[
\begin{array}{c @{\quad \textnormal{is notation for}\quad} l}
\infer{P_1 \and \dotsb \and P_n}{Q} & (P_1 \ast \dotsb \ast P_n) \wand Q, \\[1.5em]
\inferB{P}{Q} & (P \wand Q) \wedge (Q \wand P).
\end{array}
\]

For instance, the conditional refinement in Formula (<ref>) is presented as the following inference rule:

\[
\infer
{\loc_1 \mapstoI \val_1 \and \loc_2 \mapstoS \val_2 \and
\logrel{\Delta}{\expr_1'}{\expr_2'}{\typeB}}
\]

In rules like this, it is useful to think of premises $\loc_1 \mapstoI \val_1$ and $\loc_2 \mapstoS \val_2$ as side conditions, and of the premise $\logrel{\Delta}{\expr_1'}{\expr_2'}{\typeB}$ as the new goal that you get when you apply the rule.
This backwards-style reasoning integrates well in the Coq proof assistant; we discuss it more in detail in <Ref>.

We use the derivability relation $\proves$ explicitly to state rules that cannot be internalized, $\infer{\vdash P}{\vdash Q}$ states that if $P$ is derivable, then $Q$ is derivable.
This is weaker than $\infer{P}{Q}$, which denotes that $Q$ can be derived from $P$, $P \vdash Q$.

§.§ Example: Contextual equivalance of a bit module

We demonstrate the basic usage of by using its type-directed structural and symbolic execution rules to prove contextual equivalence of two implementations of a simple program module (representation independence).
The module we consider represents a single bit data structure—it contains an initial value for the bit, an operation for flipping the bit, and an operation for converting the values of the abstract type to Booleans.
We use an existential type (abstract type) to hide the representation type and thus the type of the module:

\[
\tbit \eqdef \texists{\tvar. \tvar \times (\tvar \to \tvar) \times (\tvar \to \tbool)}.
\]

Perhaps the simplest implementation of the bit interface is the one that uses Booleans for the internal state:

\[
\bitbool : \tbit \eqdef \<pack>(\<true>, (\Lam b. \neg b), (\Lam b. b)).
\]

The second implementation models a bit by a number from the set $\{0, 1\}$:

\begin{align*}
\flipnat : \tint \to \tint \eqdef{}& \Lam n. \If (n = 0) then 1 \Else 0 \\
\bitnat : \tbit \eqdef{}& \<pack>(1, \flipnat, (\Lam n. n = 1)).
\end{align*}

Before we explain how the contextual equivalence of these two implementation is formally proved in , let us informally discuss why these implementations are equivalent.
Note that the underlying types ($\tint$ and $\tbool$) are not isomorphic.
This, however, is not going to be a problem, because the underlying types are hidden/existentially abstracted in the module signature.
As a consequence of that, a (well-typed) client has to be polymorphic in the type $\tvar$, and can thus only create and modify values of $\tvar$ through the functions provided by the module.
A client that uses the $\bitnat$ module can only construct integers $0$ and $1$ (using the initial value and applying the flip function a number of times).
Thus, requiring an isomorphism between the underlying types is too strict—for example, we do not care what Boolean value an integer $7$ might correspond to, because the number $7$ can never be constructed using the functions provided by $\bitnat$.

This intuitive reasoning signals the key idea behind the representation independence principle [72], which states that in order to prove that two modules are equivalent, it suffices to pick a relation between the underlying types and demonstrate that all the methods preserve this relation.
For this example, a sensible candidate for such a relation is
\set{ (\<true>, 1), (\<false>, 0) }
Note that our relation does not include any integers other than $0$ or $1$, because as we previously explained, a well-typed client of $\bitnat$ cannot construct other integers.
With the relation at hand, the informal proof is as follows.
The initial values offered by the modules are related.
The flip function preserves this relation.
The function that converts “bits” to Booleans sends related values to the same Boolean.

We will now demonstrate how to carry out this argument formally in .
Specifically, we prove the following refinement using the rules in <Ref>:

\[
\logrel{}{\bitbool}{\bitnat}{\tbit}
\]

The other direction can be proved in a similar way, which using soundness (<Ref>), gives us the contextual equivalence $\ctxequiv{}{\bitbool}{\bitnat}{\tbit}$.

From a high-level point of view, the proof of this example involves applying 's type-directed structural rules following the structure of $\tbit$.
At the leaves of the proof, we continue with 's symbolic execution rules to perform computation steps.

Since $\tbit$ is an existential type, and both $\bitbool$ and $\bitnat$ are $\<pack>$'s, we start off by applying the type-directed structural rule rel-pack.
For that we need to pick a relation $R$, which will be the interpretation for the type variable $\tvar$, and should link together the underlying representations of bits in $\bitbool$ and $\bitnat$.
We define the relation $R$ as follows:

\[
R(b, n) \eqdef (b = \<true> \wedge n = 1) \vee (b = \<false> \wedge n = 0).
\]

Starting with the initial goal $\logrel{}{\bitbool}{\bitnat}{\tbit}$, we apply rel-pack.
As a side-condition, we have to prove that $R$ is persistent for any $\val_1, \val_2$, written as $\persistent{R(\val_1,\val_2)}$, intuitively meaning that the proposition $R(\val_1, \val_2)$ does not assert ownership of any resources.
We discuss persistent propositions in more detail in <Ref>, and for now we just note that the relation $R$ is indeed persistent.
After application of the rel-pack rule the goal becomes:

\[
\logrel{\deltainsert{\tvar}{R}{}}
{(\<true>, (\Lam b. \neg b), (\Lam b.b))}
{(1, \flipnat, (\Lam n. n = 1))}
{\tvar \times (\tvar \to \tvar) \times (\tvar \to \tbool)}.
\]

By repeatedly applying the type-directed structural rule rel-pair we get three new goals:

* $\logrel{\deltainsert{\tvar}{R}{}}{\<true>}{1}{\tvar}$;

* $\logrel{\deltainsert{\tvar}{R}{}}{(\Lam b. \neg b)}{\flipnat}{\tvar \to \tvar}$;

* $\logrel{\deltainsert{\tvar}{R}{}}{(\Lam b. b)}{(\Lam n. n = 1)}{\tvar \to \tbool}$.

For the first goal, we can use the rules rel-return' and val-var', leaving us with the obligation $R(\<true>, 1)$, which holds by the definition of $R$.

For the second and the third goal we need to prove refinements of two closures,
for which we use the type-directed structural rule rel-rec.
Let us look at the third goal in detail.
After the application of rel-rec we have to show:

\[
\always \left( \All \val_1, \val_2. \logrelV{\tvar}{{\deltainsert{\tvar}{R}{}}}{\val_1}{\val_2} \wand
\logrel{{\deltainsert{\tvar}{R}{}}}{(\Lam b. b)\ \val_1}{(\Lam n. n = 1)\ \val_2}{\tbool}
\right).
\]

The goal is wrapped in Iris's persistence modality $\always$, which turns any proposition into a persistent one.
Once again, we postpone the details about the persistence modality until <Ref>, and only remark that here we are allowed to prove the goal without the $\always$ modality.
Using this information, and the rule val-var' we reduce our goal to show:

\[
R(\val_1, \val_2) \wand \logrel{{\deltainsert{\tvar}{R}{}}}{(\Lam b. b)\ \val_1}{(\Lam n. n = 1)\ \val_2}{\tbool},
\]

for arbitrary $\val_1, \val_2$.
We then unfold the definition of $R$ and observe that we need to distinguish two cases:

* $\val_1 = \<true>$ and $\val_2 = 1$;

* $\val_1 = \<false>$ and $\val_2 = 0$.

Suppose we are in the first case (the second case is similar).
We have to show:

\[
\logrel{{\deltainsert{\tvar}{R}{}}}{(\Lam b. b)\ \<true>}{(\Lam n. n = 1)\ 1}{\tbool}.
\]

At this point we apply 's symbolic execution rules: we symbolically reduce both the left-hand and the right-hand side of the refinement.
For this we use the rules rel-pure-l and rel-pure-r (the later modalities ($\later$) in these rules can be ignored for now, they will be explained in <Ref>).
These rules perform pure reductions, reductions that do not depend on the heaps.
In our case we have a $\beta$-reduction on the left-hand side, and a $\beta$-reduction and an evaluation of the binary operation (equality testing) on the right-hand side:

\[
\pureexec{(\Lam b. b)\ \<true>}{\<true>} \qquad
\pureexec{(\Lam n. n = 1)\ 1}{\pureexec{(1 = 1)}{\<true>}}.
\]

After the repeated application of the said rules we arrive at a goal

\[
\logrel{{\deltainsert{\tvar}{R}{}}}{\<true>}{\<true>}{\tbool},
\]

which we discharge by rel-return' and val-bool'.
This completes the proof of the refinement.

§.§ Example: Contextual refinement of a concurrent counter

The previous example showcased how can be used to show contextual refinement and equivalence of pure program modules.

In this subsection we prove contextual refinement of the fine-grained concurrent counter in <Ref> from <Ref> by showing that it refines the coarse-grained counter.
Specifically, we prove the following refinement:

\[
\ctxref{}{\FGcounter}{\CGcounter}
{(\tunit \to \tint) \times (\tunit \to \tint)}.
\]

Using soundness (<Ref>), this contextual refinement can be reduced to proving the refinement judgment $\logrel{}{\FGcounter}{\CGcounter}
{(\tunit \to \tint) \times (\tunit \to \tint)}$ in .

The previous example demonstrated the basic usage of symbolic execution rules of .
Those symbolic execution rules were confined to the pure fragment of the programming language.
In this example we show how to use 's symbolic execution rules for stateful computations and concurrency primitives.
In addition to the type-directed structural rules and symbolic execution rules, the proof will require the usage of invariants for linking together the values of the two counters.
We will use selected rules from <Ref>.
To symbolically execute the operations on locks that appear in $\CGcounter$, we will also make use of the relational specification for locks in <Ref>.
The lock specification
is stated in terms of an abstract predicate $\isLock{\lkvar}{\<false>}$ (resp., $\isLock{\lkvar}{\<true>}$) stating that $\lkvar$ is a lock which is unlocked (resp., locked).
The relational specification for locks can then be seen as consisting of symbolic execution rules that manipulate that abstract predicate.[Because this specification is for the “angelic” right-hand side, it does not express mutual exclusion as it is common for separation logic specifications. We explain this by contrasting the specification with the one for the left-hand side in <Ref>.]
We will see in <Ref> that these specifications can be proven for a simple spin lock.

. false> []Δ_1[]
[]Δ_1[ ]
false> true> []Δ_1[]
[]Δ_1[ ]
b false> []Δ_1[]
[]Δ_1[ ]

Right-hand side relational specification for locks.

§.§.§ Symbolic execution

Recall that performing symbolic execution means reducing the left-hand or right-hand side of the refinement according to the computational rules.
We have already seen the usage of rel-pure-l, which allows us to perform pure computations.
For this example we also use stateful symbolic execution rules in <Ref>.
To start with the refinement proof, we apply the stateful symbolic execution rule rel-alloc-l' to the left-hand side to obtain:

\[
c_i \mapstoI 0 \wand
\logrel{}{((\Lam \unittt. \counterread\ c_i),(\Lam \unittt. \FGincrement\ c_i))}{\CGcounter}{(\tunit \to \tint) \times (\tunit \to \tint)}.
\]

Note that after the application of the rule we gain access to the resource $c_i \mapstoI 0$ representing the value of the counter on the left-hand side.
Subsequently, using the symbolic execution rules rel-pure-r, rel-alloc-r and newlock-r on the right-hand side the goal becomes:

\begin{multline*}
c_i \mapstoI 0 * c_s \mapstoS 0 * \isLock{\lkvar}{\<false>}
\wand \\
\logrel{}{((\Lam \unittt. \counterread\;c_i),(\Lam \unittt.\FGincrement\ c_i))}
{(\Lam \unittt. \counterread\ c_s),(\Lam \unittt.\CGincrement\ c_s\ \lkvar))}
{(\tunit \to \tint) \times (\tunit \to \tint)}.
\end{multline*}

In addition to gaining the resource $c_s \mapstoS 0$, representing the value of the right-hand side counter, we get access to the abstract predicate $\isLock{\lkvar}{\<false>}$, which keeps track of the state of the lock $\lkvar$ on the right-hand side.

's symbolic execution rules are inspired by the “backwards”-style Hoare rules of [53] and the weakest-precondition rules in Iris [64, 58].

§.§.§ Invariants and persistent propositions

At this point we wish to prove a refinement of two closures.
By the rule rel-pair it would suffice to prove that both closures refine each other.
However, if we were to apply rel-pair, we would be forced to split our resources in two: the resources needed for the refinement proof of the read function, and the resources needed for the refinement proof of the increment function.
But both of those operations require access to the counter locations $c_i \mapstoI -$ and $c_s \mapstoS -$.
To circumvent this issue we put said resources in a global invariant $\knowInv{}{\propMV}$, which allows $\propMV$ to be shared between different parts of the program (and between different threads).
In our running example, we establish the invariant $\knowInv{\namesp}{\counterinv}$ (using rel-inv-alloc'), where:

\[
\counterinv \eqdef \Exists n \in \nat. c_i \mapstoI n * c_s \mapstoS n * \isLock{\lkvar}{\<false>}.
\]

The invariant $\knowInv{\namesp}{\counterinv}$ not only allows us to share access to $c_i$ and $c_s$, but also ensures that the values of the respective counters match up.
For our invariant we pick any fresh invariant name $\namesp \in \InvName$ (more on the invariant names below).

Invariants $\knowInv {} \propMV$ are persistent: once established, they will remain valid for the rest of the verification.
This differentiates them from ephemeral propositions like $\loc \mapstoI \val$ and $\loc \mapstoS \val$, which could be invalidated in the future by actions of the program or proof.

The notion of being persistent is expressed in (and Iris) by means of the persistence modality $\always$.
The purpose of $\always \propMV$ is to say that $\propMV$ holds without asserting any ephemeral propositions.
The most important rules for the $\always$ modality are $\always \propMV =  \always\propMV * \always\propMV$ and $\always\propMV \wand \propMV$, which allow to freely duplicate $\always \propMV$ and finally get $\propMV$ out.
We say that $\propMV$ is persistent, written as $\persistent{\propMV}$, if $\propMV \proves \always \propMV$; otherwise, we say that $\propMV$ is ephemeral.
To prove $\always \propMV$, one can only use persistent resources like $\knowInv{}{\propMV}$, and not ephemeral resources like $\loc \mapstoI \val$.
We refer to stripping off the persistence modality in the context of persistent hypotheses as introducing the $\always$ modality.
We make that precise and give rules for the $\always$ modality in <Ref>.

Once the invariant $\knowInv{}{\counterinv}$ for our running example has been established, we can duplicate it, and apply rel-pair to obtain two goals:

\begin{align*}
\knowInv{}{\counterinv} \wand{}&
\logrel{}{(\Lam \unittt. \counterread\ c_i)}{(\Lam \unittt. \counterread\ c_s)}{\tunit \to \tint}
\\
\knowInv{}{\counterinv} \wand{}&
\logrel{}{(\Lam \unittt.\FGincrement\ c_i)}{(\Lam \unittt.\CGincrement\ c_s\ \lkvar)}{\tunit \to \tint}.
\end{align*}

We first describe how to prove the refinement of $\counterread$.
As $\Lam x.e$ is syntactic sugar for $\Rec \_ x = e$, we can apply rel-rec at the function type $\tunit \to \tint$ and obtain the new goal:

\[
\knowInv{}{\counterinv} \wand
\always \big(
\All \val\, \val'. \logrelV{\tunit}{\Delta}{\val}{\val'} \wand
\logrel{}{(\Lam \unittt. \deref c_i)\ \val}{(\Lam \unittt.\deref c_s)\ \val'}{\tint} \big).
\]

By val-unit', we obtain that $\logrelV{\tunit}{\Delta}{\val}{\val'}$ implies $\val = \val' = \unittt$.
Moreover, since $\knowInv{}{\counterinv}$ is our only hypothesis, and it is persistent, we can strip off the $\always$ modality
, arriving at the following goal:

\[
\knowInv{}{\counterinv} \wand{} {\logrel{}{(\Lam \unittt. \deref c_i)\ \unittt}{(\Lam \unittt.\deref c_s)\ \unittt}{\tint}}.
\]

Accessing invariants.
The fact that invariants are persistent (and thus can be duplicated, $\knowInv {} \propMV \mathrel{=} \knowInv {} \propMV \mathrel{*} \knowInv {} \propMV$) comes with a cost—once a proposition $\propMV$ has been turned into an invariant $\knowInv {} \propMV$, one is only allowed to access $\propMV$ during a single atomic execution step on the left-hand side.
This restriction is crucial as the scheduling of threads on the left-hand side is demonic.
When proving a refinement, we have to consider all possible interleavings of threads.
If we were to be able to access an invariant for the duration of multiple steps, another thread could be scheduled in between, and observe that the invariant was temporarily broken.

Scheduling on the right-hand side, however, is angelic.
That is, when proving a refinement, we have the ability to select the choice of scheduling.
As a consequence, allows us to execute multiple steps on the right-hand side while accessing an invariant.

Let us take a look at the way accessing invariants in works.
We do so by continuing the proof of our running example (after introducing $\always$ and performing pure symbolic execution steps):

\[
\knowInv{}{\counterinv} \wand{}
\logrel{}{\deref c_i}{\deref c_s}{\tint}.
\]

At this point we would like to access the locations $c_i$ and $c_s$ stored in the invariant $\knowInv{}{\counterinv}$.
For this we use the rule rel-load-l-inv in <Ref>.

This rule is quite a mouthful, so let us first take a look at its shape before going into detail about the mask annotations and later modalities $\later$.
The essence of rel-load-l-inv is that it provides temporary access to the resources $\propMV$ guarded by the invariant.
In addition, it provides the invariant closing resource $\CLOSE{\namesp}{\propMV}$, which can restore the invariant (using the rule rel-inv-restore).
The resources $\propMV$ can be used to prove $\loc \mapstoI \val$, which is needed to justify the symbolic execution step on the left.
Afterwards, we are left with the goal $\logrel[\top \setminus \namesp]{\Delta}{\fillctx\lctx[\val]}{\expr_2}{\type}$.
We typically do not immediately restore the invariant (using rel-inv-restore), but first use the resources $\propMV$ to perform matching symbolic execution steps on the right.

In our example, by applying rel-load-l-inv, we obtain $c_i \mapstoI n$ and $c_s \mapstoS n$ and $\isLock{\lkvar}{\<false>}$, for some $n \in \nat$, reducing our goal to
\logrel[\top \setminus \counterN]{}{n}{\deref c_s}{\tint}
We then use rel-load-r to reduce our goal to
\logrel[\top \setminus \counterN]{}{n}{n}{\tint}.
Because these steps did not change the heap, rel-inv-restore's premises for closing the invariant are trivially met.
The refinement proof is then concluded by applying the structural rules rel-return' and val-int'.

Let us take a look at the rules rel-load-l-inv and rel-inv-restore in more detail.
A crucial aspect of these rules is that they ensure that access to the invariant $\knowInv {\namesp} \propMV$ is temporary, that $\propMV$ is only used during a single symbolic execution step on the left-hand side (but possibly several steps on the right), and that the same invariant cannot be opened twice.
This is achieved by tagging each invariant $\knowInv \namesp \propMV$ with a name $\namesp \in \InvName$, and by keeping track of which invariants have been accessed.
The latter is done in a way similar to Iris—like Iris's Hoare triples $\hoare \propMV \expr \propMVB[\mask]$, our refinement judgments $\logrel[\mask]{\Delta}{\expr_1}{\expr_2}{\type}$ are annotated with a mask $\mask \subseteq \InvName$ of accessible invariants.
By default all invariants are accessible, so we write $\logrel{\Delta}{\expr_1}{\expr_2}{\type}$ for $\logrel[\top]{\Delta}{\expr_1}{\expr_2}{\type}$, where $\top$ is the set of all invariant names.

An invariant namespace is a (non-empty) list of strings or values: $\InvName = \List(\textdom{String} + \Val)$.
When opening an invariant and removing it from a mask, we coerce an invariant namespace $\namesp$ into a mask by taking its upwards extension $\namecl{\namesp} = \{ \namesp.x_1.\dots.x_n \mid n \in \mathbb{N},\, x_i \in \textdom{String} + \Val \}$.
Abusing the notation, we write $\mask \setminus \namesp$ for $\mask \setminus \namecl{\namesp}$.

When accessing an invariant, using rel-load-l-inv or rel-cas-l-inv, its namespace is removed from the mask annotation of the judgment.
The removal of the namespace from the mask guarantees that invariants are only used for a single execution step on the left-hand side.
After all, all rules for symbolic execution on the left-hand side require a $\top$ mask, whereas those for the right-hand side allow for an arbitrary mask.
The only way of performing a subsequent step on the left-hand side is thus by first restoring the mask to $\top$, which can only be done by restoring the invariants that have been accessed (using the rule rel-inv-restore).

One may wonder why refinement judgments are annotated with a mask instead of a Boolean that indicates if an invariant has been opened.
As we will show in <Ref>, allows one to access multiple invariants simultaneously.
To avoid reentrancy—which means accessing the same invariant twice in a nested fashion—we need to know exactly which invariants are opened.

An additional aspect to note is that invariants $\knowInv \namesp \propMV$ in (and Iris) are impredicative [88, 58].
This means that $\propMV$ is allowed to contain other invariant assertions $\knowInv {\namesp'} \propMVB$ or even refinement judgments $\logrel{}{\expr}{\exprB}{\type}$.
As a consequence, to ensure soundness of the logic, all rules for invariants only provide access to $\later\propMV$, $\propMV$ “guarded” by the later modality $\later$.
When invariants are not used impredicatively (invariants over so called timeless propositions, which include connectives of first-order logic and heap assertions), these modalities can be soundly omitted.

§.§.§ Later modality and Löb induction

The later modality $\later$ is not only used for resolving the impredicativity issues, but also for handling general recursion.
As is custom in logics based on step-indexing [8], such as Iris, the later modality $\later$ and Löb induction are used to reason about recursive functions.
Specifically, Iris provides the following rules for $\later$:

P Q
P Q
P P

In our example, this means that by Löb induction (rule later-loeb), we may prove

$\logrel{} {\FGincrement\ c_i} {\CGincrement\ c_s\ \lkvar}{\tint}$,

under the assumption of the induction hypothesis

$\later (\logrel{} {\FGincrement\ c_i} {\CGincrement\ c_s\ \lkvar}{\tint})$.

The induction hypothesis is `guarded' by a $\later$, and can only be used after we have performed a step of symbolic execution on the left-hand side.
That is why the symbolic execution rules for the left-hand side contain the later modality in the premises.
Let us see how it works in the example.
We use rel-pure-l to arrive at:

\begin{align*}
&\later (\logrel{} {\FGincrement\ c_i} {\CGincrement\ c_s\ \lkvar}{\tint}) \wand \\
&\later (\logrel{}%
{\Let c = \deref c_i in \If \CAS{c_i}{c}{1 + c} then c \Else \FGincrement\,c_i}%
{\CGincrement\ c_s\ \lkvar}{\tint}).
\end{align*}

By monotonicity (rule later-mono), we can now remove $\later$ both from the induction hypothesis and from the goal.

Subsequently, we symbolically execute the load operation using the invariant, just like in the previous section, reaching the goal

\[
\logrel{}%
{\If \CAS{c_i}{n}{1 + n} then n \Else \FGincrement\,c_i}%
{\CGincrement\ c_s\ \lkvar}{\tint}
\]

for some $n \in \nat$.
To symbolically execute the compare-and-set ($\<CAS>$), we use rel-cas-l-inv.
By this rule, we have to consider two outcomes, depending on whether the original value of the counter has changed between the load and compare-and-set operations or not.

* Suppose that the value of the counter $c_i$ has changed.
In that case the compare-and-set operation fails and we are left with

\begin{align*}
& c_i \mapstoI m * c_s \mapstoS m * \isLock{\lkvar}{\<false>} \wand \\
& \logrel[\top \setminus \counterN]{}%
{\If \<false> then n \Else \FGincrement\,c_i}%
{\CGincrement\ c_s\ \lkvar}{\tint}
\end{align*}

for some $m \neq n$.
Because the symbolic heap has not been changed, we can easily restore the invariant and execute the $\If \<false> then \dots \Else \dots$ to obtain
$\logrel{}{\FGincrement\,c_i}{\CGincrement\ c_s\ \lkvar}{\tint}$,
which is exactly our induction hypothesis.

* If the value has not changed, then the compare-and-set succeeds and we are left with the new goal:

\begin{align*}
&c_i \mapstoI (1 + n) * c_s \mapstoS n * \isLock{\lkvar}{\<false>} \wand \\
&\logrel[\top \setminus \counterN]{}%
{\If \<true> then n \Else \FGincrement\,c_i}%
{\CGincrement\ c_s\ \lkvar}{\tint}.
\end{align*}

At this point we use the symbolic execution rules rel-store-r, rel-load-r and the lock specifications from <Ref> to symbolically execute the right-hand side of the refinement and update the resources to match:

\begin{align*}
&c_i \mapstoI (1 + n) * c_s \mapstoS (1 + n) * \isLock{\lkvar}{\<false>} \wand \\
&\logrel[\top \setminus \counterN]{}%
{\If \<true> then n \Else \FGincrement\,c_i}%
\end{align*}

We can then restore the invariant and symbolically execute the left-hand side to finish the proof.

Note that the point in the proof when we symbolically execute $\CGincrement\ c_s\ \lkvar$ on the right-hand side corresponds to the linearization point of $\FGincrement$.

This concludes the proof of the counter refinement.
For the purposes of the proof, we have used some derived rules and principles in .
In the next section we will present an overview of primitive rules—the very core of —and show how they can be used to recover the kind of intuitive reasoning we employed in this section.

§ A CLOSER LOOK AT

We now explain some of the more technical details of , and show how the principles that we have used in <Ref> can be obtained from 's primitive proof rules.
First, we describe how to work with invariants using Iris's update modality $\pvs$
Then we explain the role and rules of persistent propositions (<Ref>), and go through a selection of 's primitive proof rules and explain how the symbolic execution and structural rules can be derived from them (<Ref>).
Finally, we demonstrate how 's rules can be used to prove the fundamental property: if we can derive a typing judgment $\typed{}{}{\expr}{\type}$, then $\expr$ refines itself, $\logrel{}{\expr}{\expr}{\type}$.
To prove the fundamental property, we need to generalize the relational judgment to open terms, and prove the structural rules for open terms as well (<Ref>).

A selection of 's primitive proof rules are shown in <Ref>.

§.§ Invariants and the update modality

The rules for invariants in <Ref> in <Ref> are fairly restrictive, they allow us to open at most one invariant at the same time.
Moreover, several of those rules, rel-load-l-inv and rel-cas-l-inv, mix together symbolic execution and invariant manipulation.
We now present 's more primitive proof rules, which integrate Iris's flexible mechanism for invariants and ghost state, and which can be used to derive rules such as like rel-load-l-inv and rel-cas-l-inv.

Invariants and ghost state in Iris are controlled via the update modality $\pvs[\mask_1][\mask_2] \propMV$.
The intuition behind $\pvs[\mask_1][\mask_2] \propMV$ is to express that under the assumption that the invariants in $\mask_1$ are accessible initially, one can obtain $\propMV$, and end up in the situation where the invariants in $\mask_2$ are accessible.
Thus, for showing $P$ we can open the invariants from $\mask_1$ and have to restore the invariants from $\mask_2$ (the invariants from $\mask_1 \setminus \mask_2$ may remain open).
Furthermore, this modality allows one to perform changes to Iris's ghost state via frame preserving updates; for a description of those we refer the reader to [58].

The key rules of the update modality are:

$\pvs$-monoupd-mono⊢[_1][_2] ⊢[_1][_2]
$\pvs$-idempupd-idemp[_1][_2] [_2][_3] [_1][_3]
$\pvs$-sepupd-sep∗[_1][_2] [_1][_2] (∗)

These rules say that the update modality is a monad, which is indexed (due to the masks), and strong (due to rule upd-sep).
In (and Iris) proofs, we often need to eliminate update modalities in the proof context, which is allowed if the goal is an update modality with corresponding source mask.
This is expressed by the following derived rule:

[_1][_2] [_2][_3]

This rule is derivable from upd-mono, and upd-idemp.

Before we will describe the rules of the update modality related to invariants, let us describe some syntactic sugar that we inherit from Iris.
We write $\pvs[\mask] \propMV$ for $\pvs[\mask][\mask] \propMV$, and $\pvs \propMV$ for $\pvs[\top] \propMV$, where $\top$ is the set of all invariant names.
Moreover, since the update modality is often combined with the magic wand, we write $\propMV \vsW[\mask_1][\mask_2] \propMVB$ for $\propMV \wand \pvs[\mask_1][\mask_2] \propMVB$, and follow the same conventions for omitting masks on $\vsW$ as used for $\pvs$.

's main rule for interacting with the update modality is rel-upd.
It allows to eliminate an update modality around a refinement judgment.
To get an idea of how this rule is used, let us take a look at the primitive rule inv-alloc for allocating an invariant.
The derived rule rel-inv-alloc' in <Ref> is a composition of rel-upd with Iris's rules upd-elim and inv-alloc.

By combining rel-upd with Iris's rules upd-elim and inv-access for accessing invariants, one can turn an invariant $\knowInv \namesp \propMV$ into its content $\propMV$, together with a way of restoring the invariant $\later \propMV \vsW[\mask \setminus \namesp][\mask] \TRUE$.
It is important to notice that by using the combination of these rules, the mask on the refinement judgment changes from $\mask$ into $\mask \setminus \namesp$.
This prohibits access to the invariant $\namesp$ until it has been restored—thus preventing reentrancy.
Restoring the invariant is done by using the rule rel-upd with the premise $\later \propMV \vsW[\mask \setminus \namesp][\mask] \TRUE$.
This requires one to give up $\propMV$, and in turn transforms the mask of the judgment back into $\mask$.
Note that one can use inv-access multiple times to open multiple invariants.

Invariants and symbolic execution.
Opening invariants through rel-upd and inv-access as described above is fairly limited.
Once we open an invariant, the mask at the refinement judgment changes from $\top$ into $\top \setminus \namesp$, which prevents any symbolic execution on the left-hand side.
The rules for symbolic execution on that side require the mask to be $\top$.
As we discussed in <Ref> already, this restriction to the $\top$ mask on left-hand side rules is crucial.
It is unsound to perform multiple symbolic execution steps on the left while an invariant is open.
To see why this is the case, consider the following refinement:

\[
\logrel{}{(\Lam x. \Let n = \deref x  in x \gets n + 1; n)}{\FGincrement}{\tref\ {\tint} \to \tint}
\]

This refinement does not hold because the two programs can be distinguished by the context:

\[
\Let \cntvar = \Ref(0) in \Let f = \hole in \Fork{f\ \cntvar}; f \cntvar.
\]

The left-hand side is basically the coarse-grained increment operation $\CGincrement$ without the lock protection.
Thus, the function on the left-hand side does not guarantee thread-safety: the value of the passed reference can change unpredictably if the function is invoked in parallel with itself.
By contrast, the $\FGincrement$ always increments the counter monotonically.

If we were allowed to perform multiple symbolic execution rules on the left-hand side, then we could have proven the above refinement, using an invariant of $\knowInv{}{\Exists n. \cntvar_s \mapstoS n \ast \cntvar_i \mapstoI n}$.

In order to support symbolic execution with invariants, provides additional rules to simultaneously access an invariant and perform a single atomic symbolic execution step on the left-hand side.
Examples of such rules are rel-load-l, rel-store-l and rel-cas-l.

We can now explain the derived rule rel-load-l-inv in terms of the primitive rules.
The proposition $\later \propMV \vsW[\mask \setminus \namesp][\mask] \TRUE$ is used for closing the invariant $\namesp$ because it changes the mask from $\mask \setminus \namesp$ to $\mask$.
Thus $\CLOSE{\namesp}{\propMV} \eqdef (\later \propMV \vsW[\top \setminus \namesp][\top] \TRUE)$.
To prove rel-load-l-inv from <Ref>, we apply rel-load-l to obtain the goal:

\[
\pvs[\top][\top\setminus\namesp] {\left(
\Exists \val. \loc \mapstoI \val \mathrel{*}
\later \big(\loc \mapstoI \val \wand
\logrel[\top\setminus\namesp]{\Delta}{\fillctx\lctx [\val]}{\expr}{\type}\big)
\right) }.
\]

We then use inv-access and upd-elim to get the premise of rel-load-l-inv.
In the same way rel-cas-l-inv can be derived from rel-cas-l.
Finally, the closing rule rel-inv-restore is a consequence of the definition of $\CLOSE{\namesp}{\propMV}$ and rel-upd.

Using 's primitive symbolic execution rules such as rel-load-l, rel-store-l and rel-cas-l one can also derive the following weaker, but perhaps more intuitive, symbolic execution rule:

\[
\inferH{rel-store-l'}
{\loc \mapstoI \val \and
\later \big(\loc \mapstoI \valB \wand
\logrel{\Delta}{\fillctx\lctx [\unittt]}{\expr_2}{\type}\big)}
{\logrel{\Delta}{\fillctx\lctx [\loc \gets \valB]}{\expr_2}{\type}}
\]

Since these rules have a $\top$ mask, they can only be used when no invariants have been opened.
Recall that by contrast, the symbolic execution rules for the right-hand side, such as rel-load-r, rel-store-r in <Ref>, which are of a similar shape, can be performed even with invariants open because they allow the mask to be arbitrary.

§.§ The persistence modality

Recall from <Ref> that a proposition $\propMV$ is persistent, written as $\persistent{\propMV}$, if $\propMV \vdash \always \propMV$, where $\always$ is Iris's persistence modality.
The $\always$ modality plays an important role in because it makes it possible to express that if two expressions are related, they remain related forever.
For example, the persistence modality plays a crucial role in the rule rel-rec in <Ref>—it ensures that ephemeral resources (such as heap assertions) are not used for the verification of the closure's body.
After all, closures can be invoked arbitrarily many times at different points in time (possibly concurrently), and hence it is impossible to guarantee that ephemeral resources will still be available when the closure is called.
For example, without the $\always$ modality in the premise of rel-rec one would be able to prove the following unsound refinement:

\[
\logrel{}{\Let \loc = \Ref(0) in \Lam \unittt. \loc \gets 1 + \deref\loc;\,\deref \loc\ }{\ \Lam \unittt. 1\ }{\ \tunit \to \tint}.
\]

One would use rel-alloc-l' to obtain the heap assertion $\loc \mapstoI 0$, and subsequently use that assertion to verify the body of the closure.
Fortunately, the $\always$ modality in rel-rec prevails—$\loc \mapstoI 0$ is ephemeral, not persistent, so cannot be moved under a $\always$.

In <Ref> we gave an idea of the core rules of the persistence modality.
Let us now take a look at the rules in more detail:

The rules always-dup and always-elim say that the $\always \propMV$ is duplicable, and one can get $\propMV$ out.
The rule always-idemp says that $\always \propMV$ itself is persistent.
The rules always-elim, always-mono and always-idemp say that $\always$ is in fact a co-monad.
Finally, $\always$ commutes with most logical connectives, for example, the separating conjunction, as expressed by always-sep.

If we wish to prove $\always \propMVB$ under the assumptions $\propMV_1, \dots, \propMV_n$, where each $\propMV_i$ is persistent, then we can introduce the $\always$ modality and prove $\propMVB$ from $\propMV_1, \dots, \propMV_n$:

_1 …_n
_1 ∗…∗_n ⊢

_1 ∗…∗_n ⊢

This rule is derivable from the definition of $\persistent{-}$, always-sep, and always-mono.

Note that $\persistent{\propMV}$ is defined through the validity relation $\propMV \proves \always \propMV$; it is a meta-logical notion (in terms of the mechanization, $\persistent\propMV$ is a Coq-level predicate, not an Iris-level predicate).
As such, the rule above does not fit the description we have given to the inference rules in <Ref>.
Rather, it should be seen as a family of inference rules indexed by meta-level propositions $\persistent{\propMV_1}, \dots, \persistent{\propMV_n}$.

§.§ Value interpretation and monadic rules

In addition to the refinement judgment $\logrel{\Delta}{\expr_1}{\expr_2}{\type}$, which relates expressions $\expr_1$ and $\expr_2$, provides the value interpretation $\Sem{\type}_\Delta(\val_1,\val_2)$, which relates values $\val_1$ and $\val_2$.
The rule rel-return expresses that $\Sem{\type}_\Delta(\val_1,\val_2)$ implies $\logrel{\Delta}{\val_2}{\val_2}{\type}$.
However, the inverse direction does not hold, $\Sem{\type}_\Delta(\val_1,\val_2)$ is strictly stronger than $\logrel{\Delta}{\val_1}{\val_2}{\type}$ as its rules (in <Ref>) are bidirectional, whereas those for the expression judgment are unidirectional.
The bidirectionality is crucial for the rule rel-rec in <Ref>, as it contains $\Sem{\type}_\Delta(\val_1,\val_2)$ in negative position—as a client of rel-rec one gets $\Sem{\type}_\Delta(\val_1,\val_2)$ as an assumption and hence needs to eliminate it.

We want the value interpretation $\logrelV{\type}{\Delta}{\val_1}{\val_2}$ to be persistent, because our type system is not substructural, types denote knowledge, but not ownership of data.
For example, in typing the expression $\expr_1 \gets \expr_2$ with store-typed, we use the same context $\Gamma$ for type checking both $e_1$ and $e_2$.
In order to semantically validate such rules, we want the propositions $\logrelV{\type}{\Delta}{\val_1}{\val_2}$ to be duplicable.
To that end, we require all the interpretations in the context $\Delta$ to be persistent.
That is why the rule rel-pack in <Ref> has a side-condition $\All \val_1, \val_2. \persistent{R(\val_1, \val_2)}$.

The value interpretation also appears in the monadic rules rel-return and rel-bind in <Ref>.
These rules are used to derive all type-directed structural rules of , with the exception of rel-fork, which is the sole primitive type-directed structural rule.
As an example, consider the type-directed structural rule for the first projection $\pi_1$.

The following rule is derivable:

By rel-bind it suffices to show:

* $\logrel{\Delta}{\expr_1}{\expr_2}{\type \times \typeB}$, but this is exactly our assumption;

* for any $\val, \valB$: $\logrelV{\type \times \typeB}{\Delta}{\val}{\valB} \wand \logrel{\Delta}{\pi_1(\val)}{\pi_1(\valB)}{\type}$.

By val-prod we have values $\val_i, \valB_i$ for $i \in \{1,2\}$ such that $\val = (\val_1,\val_2)$ and $\valB = (\valB_1,\valB_2)$ and
$\logrelV{\type}{\Delta}{\val_1}{\valB_1} \ast \logrelV{\typeB}{\Delta}{\val_2}{\valB_2}$.
Using rel-pure-l and rel-pure-r we reduce the goal
$\logrel{\Delta}{\pi_1(\val_1,\val_2)}{\pi_1(\valB_1,\valB_2)}{\type}$ to
At this point we apply rel-return.

§.§ Fundamental theorem and refinements of open terms

The type-directed structural rules[Our type-directed structural rules are often called compatibility lemmas in the logical relation literature.] are also used for proving the following theorem, which is a standard result for logical relation models of type systems:

If expression $\expr$ is well typed, $\typed{}{}{\expr}{\type}$, then $\expr$ refines itself, the judgment $\logrel{}{\expr}{\expr}{\type}$ is derivable in .

We wish to prove this theorem by induction on the typing derivation.
But in order to make it work, we need to generalize the theorem to open terms (in order to deal with the rec-typed case).
Consequently, we need to generalize 's refinement judgment $\logrel{\Delta}[\vctx]{\expr_1}{\expr_2}{\type}$ to open terms $\expr_1$ and $\expr_2$ whose free variables are bound by the typing context $\vctx$.
To define the refinement judgment for open terms, we first define a standard notion of a closing substitution.

A mapping $\gamma : \Var \to \Val \times \Val$ is
a closing substitution the typing environment $\vctx$, notation
$\validSubst{\Delta}{\vctx}{\gamma}$, if

\[
\All (x, \type) \in \vctx. \logrelV{\type}{\Delta}{\gamma_1(x)}{\gamma_2(x)},
\]

where $\gamma_i(x) = \pi_i(\gamma(x))$ is the $i$-th projection of $\gamma(x)$.

The refinement judgment $\logrel{\Delta}[\vctx]{\expr_1}{\expr_2}{\type}$ for open
terms is defined as:

\[
\logrel{\Delta}[\vctx]{\expr_1}{\expr_2}{\type}
\All \gamma.
\validSubst{\Delta}{\vctx}{\gamma} \wand \logrel{\Delta}{\gamma_1(\expr_1)}{\gamma_2(\expr_2)}{\type}.
\]

Using the refinement judgment for open terms we can now state versions of the type-directed structural rules for open terms.
For example:

\[
\infer
{\logrel{\Delta}[\vctx]{\Lam x. \expr_1}{\Lam x. \expr_2}{\type \to \typeB}}
\]

This rule can be proven by unfolding the definition of the refinement judgment for open terms and proceeding as in <Ref>.
Finally, we can state and prove the generalized version of the fundamental theorem for open terms:

If $\typed{\tenv}{\vctx}{\expr}{\type}$, then $\logrel{\Delta}[\vctx]{\expr}{\expr}{\type}$ is derivable in , for all $\Delta$ which contain the variables from $\tenv$.

By induction on the typing derivation, using the versions of the type-directed structural rules for open terms.

With the refinement judgments generalized to open terms, we can state and the generalized version of <Ref> for open terms, which we prove in <Ref>.

Let $\tenv$ be a type environment.
Suppose that refinement judgment $\logrel{\Delta}[\vctx]{\expr_1}{\expr_2}{\type}$ is derivable in for all $\Delta$ which contain the variables from $\tenv$.
Then $\ctxref{\tenv \mid \vctx}{\expr_1}{\expr_2}{\type}$.

§ RELATIONAL SPECIFICATIONS IN

Due to its first-class refinement judgments, can be used to give relational specifications to programs.
Similar to Hoare triples, relational specifications abstract away from a program's implementation by expressing its behavior in terms of a pre- and postcondition.
Relational specifications apply to the situation when the expression on the one side of the refinement contains a program subject to specification, while the expression on the other side is arbitrary.
In <Ref> in <Ref> we saw an example of a right-hand side relational specifications for locks, which we then used to verify a counter module.

We start this section by describing the general format of non-atomic relational specifications (<Ref>).
Non-atomic relational specifications are sufficient to give strong specifications for the right-hand left, but due to the demonic nature of the left-hand side, we often need stronger specifications for the left-hand side (<Ref>).
We therefore introduce logically atomic relation specifications, which generalize da Rocha Pinto 's TaDA-style specifications [36] (<Ref>) and Svendsen 's HOCAP-style specifications [89] (<Ref>) from the Hoare-logic setting to the relational setting.
Finally, we show how to use logically atomic specifications to verify a ticket lock (<Ref>).

§.§ Non-atomic relational specifications

§.§.§ Right-hand side relational specifications

Consider the following implementation of a lock, which we refer to as a spin lock:

\begin{align*}
\newlock \eqdef{} & \Lam \unittt. \Ref(\<false>) \\
\acquire \eqdef{} & \Lam \loc. \If \CAS{\loc}{\<false>}{\<true>} then \unittt \Else
\acquire\ \loc \\
\release \eqdef{} & \Lam \loc. \loc \gets \<false>
\end{align*}

For this specific implementation, we can prove the rules in <Ref> in <Ref> by defining the lock predicates as follows:

\[
\isLock{\lkvar}{b} \eqdef \lkvar \in \Loc \ast \lkvar \mapstoS b.
\]

The rules for locks in <Ref> follow a certain pattern.
For an expression $\expr_2$ that, under precondition $\textcolor{precond}{\propMV}$, reduces to $\val$, with postcondition $\textcolor{postcond}{\propMVB(\var,\val)}$, we have the following rule:

\[
\infer
{{\color{precond}\propMV} \and
\All \var,\val. {\color{postcond}\propMVB(\var,\val)} \wand \logrel[\mask]{\Delta}{\expr_1}{\fillctx\lctx[\val]}{\type}}
\]

The postcondition $\propMVB : X \times \Val \to \Prop$ also depends on a type $X$, provided by the provider of the rule.
This rule pattern can be considered a relational version of a Hoare triple for a program on the right-hand side of the refinement judgment.

§.§.§ Left-hand side relational specifications

R ,  . (, , R) []_2
[ ]_2
(, , R)
(, , R)
(, , R) ( R []_2)
[ ]_2
(, , R)  R []_2
[ ]_2

Left-hand side relational specification for locks.

We can formulate a similar pattern for programs on the left-hand side of the refinement judgment:

\[
\infer
{{\color{precond}\propMV} \and
\All \var,\val. {\color{postcond}\propMVB(\var,\val)} \wand \logrel{\Delta}{\fillctx\lctx[\val]}{\expr_2}{\type}}
\]

Using this pattern we can state and prove a relational version of the standard separation logic specification for locks, which is shown in <Ref>.
This specification makes use of the lock predicate $\islockI(\gname, \lkvar, R)$, which states that $\lkvar$ protects the resources described by the proposition $R$.
When creating a lock using $\newlock$, the resources $R$ have to be given up, and the persistent lock predicate $\islockI(\gname, \lkvar, R)$ is given in return.
A thread that acquires a lock by calling $\acquire$ gets access to $R$ for the duration of the critical section, and has to give $R$ back when calling $\release$.
The token $\locked{\gname}$, where $\gname$ is a ghost name associated to the lock, makes sure that a lock can only be released when it has been acquired.
To prove the left-hand side specification for the spin lock, we define the lock predicate $\islockI(\gname, \lkvar, R)$ following the usual definition in Iris:

\[
\islockI(\gname, \lkvar, R) \eqdef
\lkvar \in \Loc \ast
\knowInv{\namesp_{\mathsf{lock}}}{
(\lkvar \mapstoI \<false> * \locked{\gname} * R) \lor
(\lkvar \mapstoI \<true>)
\]

This definition uses an Iris invariant to express that the lock is either unlocked ($\lkvar \mapstoI \<false>$), in which case it holds the token $\locked{\gname}$ and the resources $R$, or locked ($\lkvar \mapstoI \<true>$), in which case it holds no resources, since those are held by the thread that acquired the lock.
The token $\locked{\gname}$ is an exclusive resource that is obtained from Iris's ghost theory.

§.§.§ Left- versus right-hand side relational specifications

As we have seen in the specifications for the lock, there is an asymmetry between the left- and right-hand side specifications.
The left-hand side specification of $\acquire$ (acquire-l) can be used regardless of whether the lock is unlocked, whereas the right-hand specification (acquire-r) can be used solely if the lock is unlocked (if $\isLock{\lkvar}{\<false>}$).
This is due to the demonic nature of the left-hand side and the angelic nature of the right-hand side.
For $\acquire$ on the left-hand side, we have to consider an arbitrary execution, whereas for $\acquire$ on the right-hand side we have to provide an execution ourselves.
That is, for $\acquire$ on the right-hand side we have to show that it actually acquires the lock and reduces to $\unittt$,
which is only possible when the lock is unlocked.
For this reason we use the predicate $\isLock{\lkvar}{b}$, which tracks the state $b$ of the lock.

§.§ The need for logically atomic specifications

Recall from <Ref> that for any primitive (stateful) operation we have a symbolic execution rule that allows the client to access shared resourced stored in an invariant.
For example, the rule rel-store-l for the store operation is as follows:

[⊤][] (
- *

Concretely, the update modality $\pvs[\top][\mask]$ in the premise of this rule allows users to use inv-access to access an invariant for the duration of the operation.
The mask $\mask$ in the refinement judgment $\logrel[\mask]{\Delta}{\fillctx\lctx [\unittt]}{\expr_2}{\type}$ (that appears in the premise of the rule) forces the user to close the invariant at the end of the duration of the operation.
The ability to open an invariant is sound because operations such as store are physically atomic—they reduce in one step.
As a consequence of being physically atomic, other threads cannot observe that the invariant has been broken during the execution of the operation.

In contrast, methods of a concurrent program module are typically composed of several operations and hence they are not physically atomic.
For example, consider the increment function $\FGincrement$ of the fine-grained counter module from <Ref>:

\[
\FGincrement \eqdef{} \Rec {\lvar{inc}} \cntvar =
\begin{array}[t]{@{} l}
\Let n = \deref \cntvar in \\
\If \CAS{\cntvar}{n}{1 + n} then n \Else \lvar{inc}\ \cntvar
\end{array}
\]

This function is a compound expression that does not reduce to a value in a single step.
Nevertheless, during the execution of this function there is a single instant at which the whole operation actually appears to take the effect—namely the successful reduction of the compare-and-set operation ($\<CAS>$).
This instant is called the linearization point.
What it means is that, for an outside observer, the method $\FGincrement$ behaves as if it was atomic, and we wish to express that in this function's relational specification.

This phenomenon is called logical atomicity in the literature, and has been studied extensively in the context of Hoare-style logics [60, 36, 89, 61, 59].
In the upcoming subsections we will how to generalize the concept of logical atomicity to the relational setting, and how that gives rise to logically atomic relational specifications.
Concretely, we generalize da Rocha Pinto 's TaDA-style specifications [36] (<Ref>) and Svendsen 's HOCAP-style specifications [89] (<Ref>) from the Hoare-logic setting to the relational setting.
Establishing the formal comparison between the two styles is out of the scope of this paper.
Rather, we demonstrate that both approaches can be applied to the context of relational specifications.

§.§ TaDA-style relational specifications

§.§.§ Formulating TaDA-style specifications

We take inspiration from the encoding of TaDA-style logically atomic Hoare triples in Iris [61] and assign the following logically atomic relational specification to $\FGincrement$:

[⊤][] n. n *

(n [][⊤] )

((n + 1) [][n])

[ ]

Contrary to the non-atomic specification, we do not have $\cntvar \mapstoI n$ as a premise of the rule directly, but instead the premise contains a way of obtaining $\cntvar \mapstoI n$.
The typical way of obtaining $\cntvar \mapstoI n$ is by accessing an invariant, which is formally done by using the update modality $\pvs[\top][\mask]$ in the premise combined with inv-access from <Ref>.

To justify the remaining part of the premise of the rule we need to take a closer took at the behavior of $\FGincrement\ \cntvar$, whose implementation (<Ref>) we recall to be as follows:

\[
\FGincrement \eqdef{} \Rec {\lvar{inc}} \cntvar =
\begin{array}[t]{@{} l}
\Let n = \deref \cntvar in \\
\If \CAS{\cntvar}{n}{1 + n} then n \Else \lvar{inc}\ \cntvar
\end{array}
\]

The compare-and-set operation ($\<CAS>$) can either succeed or fail.
If it succeeds, then we have managed to update our resources to $\cntvar \mapstoI (n + 1)$, and we can proceed with proving $\logrel[\mask]{}{\fillctx\lctx[n]}{\expr}{\type}$ under that premise.
This explains the $(\cntvar \mapstoI (n + 1) \wand \logrel[\mask]{}{\fillctx\lctx[n]}{\expr}{\type})$ clause.
If, however, the compare-and-set fails, then we need to be able to restart the whole computation of $\FGincrement\ \cntvar$.
For that we must be able to return $\cntvar \mapstoI n$ to the invariant.
Hence the $(\cntvar \mapstoI n \vsW[\mask][\top] \TRUE)$ clause.
(The same clause is used for performing operations that do not modify the state, such as dereferencing.)

Finally, we know that the computation can either succeed or be restarted—but not both.
We have to accommodate for both situations, just not at the same time.
Hence the last two clauses described here are connected by an intuitionistic conjunction ($\wedge$), instead of the separating conjunction ($*$).

§.§.§ Using TaDA-style specifications

We use the logically atomic relational specification inc-i-l-tada to prove the refinement that we have seen in <Ref>.
The new proof is more modular since it does not appeal to the definition of $\FGincrement$.
The refinement that we want to prove is as follows:

\[
\knowInv{\counterN}{\counterinv} \wand{}
\logrel{}{\FGincrement\ c_i}{\CGincrement\ c_s\ l}{\tint}
\]

Recall that $\counterinv \eqdef {\Exists n \in \nat. c_i \mapstoI n * c_s \mapstoS n * \isLock{\lkvar}{\<false>}}$.
To prove this goal, we use inc-i-l-tada.
After introducing the persistence modality (using always-intro, which is allowed, because there are no ephemeral assumptions in our context), this gives the following new goal (under the assumption $\knowInv{\counterN}{\counterinv}$):

\begin{equation*}
\pvs[\top][\top \setminus \counterN] \Exists n. c_i \mapstoI n \ast
\left(
\begin{array}{@{} l @{}}
\big(c_i \mapstoI n \vsW[\top \setminus \counterN][\top] \TRUE\big)
\mathrel{\land} \\
\big(c_i \mapstoI (n + 1) \wand \logrel[\top \setminus \counterN]{}{n}{\CGincrement\ c_s\ l}{\tint}\big)
\end{array}
\right)
\end{equation*}

At this point we can open up the invariant $\counterinv$ (using inv-access), and thereby introduce the update modality.
The contents of the invariant provides us with a witness for the existential quantifier and allows us to discharge $\cntvar \mapstoI n$.
We are left with proving the conjunction:

\begin{equation*}
\big(c_i \mapstoI n \vsW[\top \setminus \counterN][\top] \TRUE\big)
\quad \land \quad
\big(c_i \mapstoI (n + 1) \wand \logrel[\top \setminus \counterN]{}{n}{\CGincrement\ c_s\ l}{\tint}\big)
\end{equation*}

under the assumption of the unused resources $\isLock{l}{\<false>}$ and $c_s \mapstoS n$ from the invariant, and the invariant closing resource $\later \counterinv \vsW[\top \setminus \counterN][\top] \TRUE$.

The first conjunct corresponds to the case in which we close the invariant without modifying anything in our current context (the compare-and-set has failed).
It follows directly from the invariant closing resource.
It thus remains to prove the second conjunct (the compare-and-set has succeeded), which means we should prove
\logrel[\top \setminus \counterN]{}{n}{\CGincrement\ c_s\ l}{\tint}
under the assumptions $c_i \mapstoI (n+1)$ and $\isLock{l}{\<false>}$ and $c_s \mapstoS n$ and $\later \counterinv \vsW[\top \setminus \counterN][\top] \TRUE$.
At this point we finish the proof by symbolically executing $\CGincrement\ c_s\ l$ on the right-hand side before closing the invariant using invariant closing resource.

§.§.§ General format of TaDA-style specifications

The general format of logically atomic rules for logical refinements is the following:

x. (x) *

((x) [][⊤] )

(x,) * [][]_2)

Here, $\propMV : X \to \Prop$ is a predicate describing consumed resources, and $\propMVB : X \times \Val \to \Prop$ is a predicate describing produced resources, both dependent on a type $X$ supplied by the provider of the rule (a library that exports the program $\expr_1$).
This parameter $X$ is selected on per-specification basis.
For example, for the counter module $X$ is going to be the type of natural numbers.

We include a frame $\propMVC$, which can be chosen by the client, for the following reason.
The second premise of the rule resides below a persistence modality.
Whenever we prove a goal of the form $\always P$ we must prove $P$ using only persistent resources, and thus have to throw all the ephemeral resources away (see always-intro in <Ref>).
However, we do not want to throw away all the ephemeral resources that we have for eternity (as they might be needed to close invariants afterwards or to proceed otherwise with the proof), so we give them up only temporarily, by collecting them in $\propMVC$.

§.§.§ Proving TaDA-style specifications

Following the general scheme, we now state and prove the TaDA-style specification of our increment function:

[⊤][] n. n *

(n [][⊤] )

((n + 1) ∗[][n])

[ ]

To prove this specification, we proceed by Löb induction and symbolic execution.
At the point when we need to symbolically dereference $\cntvar$ we apply rel-load-l.
We then use the update that we have as a premise of the specification to obtain $\cntvar \mapstoI n$ for some $n$.
After providing $\cntvar \mapstoI n$ for the load operation, we use the first conjunct
\cntvar \mapstoI n * \vsW[\mask][\top] \TRUE
to restore the mask on the refinement judgment.

After that we have to symbolically execute the compare-and-set operation; we apply rel-cas-l and use the update that we have as a premise again to obtain $\cntvar \mapstoI m$ for some $m$, as needed for rel-cas-l.
If $m \neq n$, then the compare-and-set operation has failed, and we can restart the proof first by restoring the mask on the refinement judgment (using the closing update), and then using the Löb induction hypothesis.
If $m = n$, then the compare-and-set operation has succeeded, and the points-to connective is updated to $\cntvar \mapstoI (n+1)$.
Then we can use the second conjunct
\cntvar \mapstoI (n + 1) \ast \propMVC \wand \logrel[\mask]{}{\fillctx\lctx[n]}{\expr}{\type}
to arrive at the exact conclusion that we need: $\logrel[\mask]{}{\fillctx\lctx[n]}{\expr}{\type}$.

§.§ HOCAP-style relational specifications

We now present another form of logically atomic relational specifications—HOCAP-style logical atomic relational specifications, which are based on the logically atomic specifications by Svendsen  [89] in the eponymous logic.
Contrary to TaDA-style specifications, which come in a precisely specified format (<Ref>), HOCAP-style specifications do not have a precise format.
This provides the flexibility that not only can they be used to represent linearization points, but they can also be used to represent arbitrary observable interactions with the abstract state.
This flexibility allows us to give strong specifications to non-linearizable methods (<Ref>), which we use in the ticket lock refinement proof (<Ref>).

§.§.§ Formulating HOCAP-style specifications

Rules for abstract predicates:

n qm
n = m
q_1n q_2m
n = m
q_1n ∗q_2n
q_1 + q_2n
n 1m
k ∗1k

Relational specification:

.  ∗1n  []_2
∩ = ∅

(n. n
n+1 ∗ [⊤∖][n]_2)
[ ]_2
∩ = ∅

(n. n
n ∗ [⊤∖][n]_2)
[ ]_2

HOCAP-style logically atomic relational specification for a fine-grained concurrent counter.

Let us consider the HOCAP-style specification in <Ref> for the fine-grained concurrent counter from <Ref> in <Ref>.
Contrary to the TaDA-style specification, the HOCAP-style specification does not expose the underlying state of the counter ($\loc \mapstoI n$) directly, but instead provides an abstract view of the state through abstract predicates.

The persistent predicate $\Cnt{\cntvar}{\gname}$ asserts that the value $\cntvar$ represents a counter.
The specification is parameterized by a namespace $\namesp$ for the internal invariants associated with the specification.
The ghost name $\gname$ is used to link $\cntvar$ with the predicates $\cnt{\gname}{q}{n}$ and $\cntAuth{\gname}{n}$, which describe the abstract state of the counter.
The predicate $\cnt{\gname}{q}{n}$ provides the client view of the abstract state of the counter.
It is similar to the fractional heap points-to connective from separation logic—it associates a value (a natural number $n$) to the counter, and can be split and combined according to the fractional component $q$ (cnt-agree', cnt-combine).
The predicate $\cntAuth{\gname}{m}$ provides the module view of the abstract state of the counter.
It agrees with the client view (cnt-agree) and can be used together with $\cnt{\gname}{1}{n}$ to update the value associated to the counter (cnt-update).

Ownership of the module view predicate $\cntAuth{\gname}{m}$ is given to the user only during the execution of the counter operations.
Consider, for example, the specification inc-i-l-hocap for the atomic increment function $\FGincrement$.
From the client's point of view, there is only one place where $\FGincrement$ observably interacts with the abstract state of the counter, namely during its linearization point.
For this point of access, the user has to provide the update:

\[
\cntAuth{\gname}{n}
\vsW[\top\setminus \namesp][\top\setminus  \namesp \setminus \mask]
\cntAuth{\gname}{n+1} \ast{} \logrel[\top\setminus\mask]{}{\fillctx\lctx[n]}{\expr_2}{\type}.
\]

The user is given the module view $\cntAuth{\gname}{n}$ of the counter, and has to update it to $\cntAuth{\gname}{n+1}$.
For that, the user has to appeal to cnt-update and has to provide $\cnt{\gname}{q}{n}$ themselves (either as an immediate resource or from an invariant in $\mask$, which can be opened thanks to the update modality).
After the abstract state is updated, the user has to prove the refinement judgment $\logrel[\top\setminus\mask]{}{\fillctx\lctx[n]}{\expr_2}{\type}$.
Similar to the TaDA-style specifications, the mask on the refinement is set to $\top\setminus\mask$, allowing the user to perform some reasoning on the right-hand side before closing all the invariants from $\mask$.

§.§.§ Using HOCAP-style specifications

We use the HOCAP-style logically atomic relational specification from <Ref> to prove the refinement that we have seen in <Ref>:

\[
\logrel{}{\FGcounter}{\CGcounter}
{(\tunit \to \tint) \times (\tunit \to \tint)}.
\]

Since the HOCAP-style specifications are stated in terms of abstract predicates, instead of the $\loc \mapstoI n$ connective, we need a slightly different invariant than the one we used for the proof using the TaDA-style specification in <Ref>, namely:

\[
\CntN{c_i}{\gname}{\namesp\!.{\mathsf{cnt}}} \ast
\knowInv{\namesp\!.{\mathsf{inv}}}{\Exists n \in \nat. \cnt{\gname}{1}{n} * c_s \mapstoS n * \isLock{\lkvar}{\<false>}}.
\]

After having established this invariant, the refinement proofs for the increment and read methods proceed similar to the corresponding TaDA-style proofs (<Ref>), except that in the increment case the user has to use cnt-update alongside inc-i-l-hocap in order to update the ghost state $\cnt{\gname}{1}{n}$ accordingly.
We do not give the proof here, and direct the reader to the accompanying Coq mechanization.

In <Ref> we will another example of a client using the HOCAP-style specification for the counter.

§.§.§ Proving HOCAP-style specifications

We discuss how to prove that the implementation of the fine-grained counter meets the HOCAP-style specifications.
To do so, we first use Iris's ghost theory to define the predicates $\cnt{\gname}{q}{n}$ and $\cntAuth{\gname}{n}$ (the details of this definition are omitted).
We then define the predicate $\Cnt{\cntvar}{\gname}$, which provides the internal invariant of the module:

\[
\Cnt{\cntvar}{\gname} \eqdef \cntvar \in \Loc \ast
\knowInv{\namesp}{\Exists n \in \mathbb{N}. \cntvar \mapstoI n \ast \cntAuth{\gname}{n}}
\]

This invariant states that the physical value $n$ of $\cntvar$ corresponds to the logical value $n$ of the predicate $\cntAuth{\gname}{n}$.
To see how this invariant is used, let us consider the proof of inc-i-l-hocap for the $\FGincrement$ operation.
Since $\FGincrement$ is defined recursively, we prove this rule by Löb induction.
We proceed by symbolically executing the left-hand side, accessing the invariant $\namesp$ to dereference $\cntvar$ for some value $n$.
It then remains to show:

\[
\logrel{}{\If \CAS{\cntvar}{n}{1 + n} then n \Else \FGincrement\ \cntvar}{\expr_2}{\type}.
\]

At this point we use the atomic symbolic execution rule for compare-and-set rel-cas-l (with $\mask = \namesp$).
We introduce the update modality $\pvs[\top][\top \setminus \namesp]$ we obtain by accessing the invariant $\namesp$ using Iris's strong invariant access rule inv-access-strong, which is needed because we need to access invariants in a non-well-bracketed way:

P [][∖]
P ∗('. P ['][' ∪] )

It remains to consider two cases.
If the compare-and-set ($\<CAS>$) has failed, we close the invariant (by setting $\mask' = \top \setminus \namesp$) and appeal to the induction hypothesis.
If the compare-and-set has succeeded, we are left to show the following:

\[
\dots \ast \cntvar \mapstoI (n+1) \ast \cntAuth{\gname}{n} \wand{} \logrel[\top \setminus  \namesp]{}{n}{\expr_2}{\type}.
\]

We first use the update $\vsW[\top\setminus \namesp][\top\setminus \namesp \setminus \mask]$ that is provided by the premise of the rule to update $\cntAuth{\gname}{n}$ into $\cntAuth{\gname}{n+1}$.
This moreover provides a proof of $\logrel[\top \setminus \mask]{}{n}{\expr_2}{\type}$.
At this point our goal becomes
\logrel[\top \setminus  \namesp \setminus \mask]{}{n}{\expr_2}{\type}
We close the invariant $\namesp$ (by setting $\mask' = \top \setminus  \namesp \setminus \mask$) and restore the mask on the refinement proposition in our goal, resulting in
\logrel[\top \setminus \mask]{}{n}{\expr_2}{\type}
$, which is exactly what we obtained from the update $\vsW[\top\setminus \namesp][\top\setminus \namesp \setminus \mask]$.

§.§.§ HOCAP-style specifications for non-linearizable operations

Using HOCAP-style specifications we can also specify operations that are not linearizable.
Consider the following “weak increment” function that we can add to the counter module:

\[
\wkincr \eqdef{} \Lam \cntvar. \cntvar \gets (\deref \cntvar + 1)
\]

The function increments the value in the location $\cntvar$ non-atomically.
What kind of specification can we give to $\wkincr$?
To answer this we have to examine what the update $\vsW$ represents in the HOCAP-style specifications.
In the previous examples with linearizable functions, the updates represented observations about the abstract state that the clients could make, and they corresponded to the linearization points.
But there is no reason why we should pin them to linearization points only.
Rather, we can let the update correspond to any operation that is observable through the abstract state.
In $\wkincr$ there are two points where such operations happen, which we can represent through two nested updates:

∩ = ∅

n. n [⊤∖]
n ∗

m [⊤∖][⊤∖∖]

n+1 ∗ [⊤∖][]_2)

[ ]_2

The first update binds the value $n$, which is obtained from the initial read operation $\deref \cntvar$.
In the conclusion of this update the client needs to return the $\cntAuth{\gname}{n}$ predicate, as in the specification read-i-l-hocap.
In addition to that predicate, the client has to provide the second update, in which $\cntAuth{\gname}{m}$ has to be updated to $\cntAuth{\gname}{n+1}$, corresponding to the assignment $\cntvar \gets n+1$.
The value $m$ corresponds to the intermediate state of the counter, which might have changed in between the dereferencing of $\cntvar$ and the assignment to it.
The presence of two updates differentiates methods that have a linearization point, such as $\FGincrement$, and non-linearizable methods, such as $\wkincr$.

In the next section we will see how a client might use the specification cnt-wk-incr-l.

§.§ Ticket lock refinement from HOCAP-style specs

§ SPECULATIVE REASONING USING PROPHECY VARIABLES

In addition to Iris's ordinary ghost state mechanism, which allows to reason about the history of a program, Iris has recently been extended with a mechanism for speculative reasoning based on prophecy variables, which allows to reason about the future of a program [7, 59].
A prophecy variable is a ghost variable that can reference a value that is determined in the future of a program's execution.
While the program that is subject to verification cannot make use of the value of a prophecy variable itself—they are ghost variables—the value can be used in proofs, to speculatively choose a reduction step in the right-hand program.
In this section we show how Iris's mechanism for prophecy variables is integrated into and can be put to action to prove challenging refinements.

We start this section by illustrating the need for prophecy variables with a motivational example (<Ref>).
We then introduce the proof rules for prophecy variables in (<Ref>), and use them to verify the motivational example (<Ref>).
We finish with another example demonstrating the applicability of prophecy variables to algebraic reasoning for concurrent programs (<Ref>).

§.§ Motivational example

The ghost state mechanism of Iris that we have seen so far has allowed us to reason about the history of the program's execution.
However, in some cases that is not enough, and it is required to take the future of the program's execution into account.
As a simple motivating example let, us consider the implementations $\newcoin$ and $\newcoinLazy$ of a coin module in <Ref>.
They both implement a virtual coin that can be flipped (using the first closure) and whose value can be read (using the second closure), but there is an important difference.
The eager version ($\newcoin$) calculates the flipped value in the $\flipcoin$ function immediately—using the $\rand$ function in <Ref>, which gives a non-deterministic Boolean value—and the $\readcoin$ function just reads that value.
In contrast, the lazy version ($\newcoinLazy$) does not perform any non-deterministic calculations in its flip operation $\flipcoinLazy$.
Instead, it sets the value of the coin to “undetermined” ($\NONE$), and postpones the actual calculation to the $\readcoinLazy$ function.

While these two implementations are rather different, they are contextually equivalent—for clients of the module it is not observable if the coin is flipped eagerly or lazily.
To prove that, we wish to establish the following refinements in :

\[
\logrel{}{\newcoin}{\newcoinLazy}{(\tunit \to \tunit) \times (\tunit \to \tbool)}
\]

\[
\logrel{}{\newcoinLazy}{\newcoin}{(\tunit \to \tunit) \times (\tunit \to \tbool)}
\]

The first refinement can be proved with the tools that we have already described.
We start by symbolically executing both implementations, obtaining references $c$ and $c_l$ to the internal state of the eager coin and lazy coin, respectively.
We then establish the following invariant linking together the two internal states:

\[
\knowInv{}{\Exists (b : \mathbb{B}). c \mapstoI b \ast (c_l \mapstoS \<None> \vee c_l \mapstoS \<Some>(b))}.
\]

This invariant can be easily shown to be preserved during the $\flipcoin \lrel \flipcoinLazy$ refinement proof.
During the $\readcoin \lrel \readcoinLazy$ refinement proof we can choose which value $\rand\ \unittt$ reduces to based on the current value of $c$, using rel-rand-r.

However, we cannot prove the second refinement with the same strategy.
The problem is that during the $\flipcoinLazy \lrel \flipcoin$ refinement we reset the value of $c_l$ (on the left-hand side) to $\<None>$, and then we have to establish a simulation on the right-hand side by picking a value for $\rand\ \unittt$ that will be assigned to $c$.
But this value has to be the same value that is picked by $\rand\ \unittt$ in $\readcoinLazy$.
Thus we have to pick a value “from the future”.

To facilitate this style of reasoning, prophecy variables have been introduced into Iris [59].
Originally, prophecy variables were used to prove refinements between state machines [7].
Lately they have been used in Iris for establishing linearizability of concurrent data structures without a fixed linearization point.
In the rest of this section we show how we integrated prophecy variables into .

§.§ Prophecy instructions and proof rules

v⃗ p. pv⃗ Δ[p]_2

v⃗. pv⃗ ∗
. (v⃗=) ∗p []Δ[]_2
p. ([]Δ_1[p])

The proof rules for prophecy variables.

While Iris's ordinary ghost state mechanism only appears at the level of the logic, prophecy variables appear as instrumented instructions in the source program.[The semantics of has to be instrumented to support prophecy variables, we refer the reader to <cit.> for details.]
The instruction $\newProph$ creates a new prophecy variable.
The instruction $\resolveProph{p}{v}$ resolves a prophecy variable $p$ to a value $v$.

The symbolic execution rules for the prophecy instructions are given in <Ref>.
In the right-hand side, the prophecy instructions are no-ops and therefore do not have any pre- or post-conditions.
Prophecy instructions that appear on the left-hand side, however, operate on additional ghost state, and thus have pre- and postconditions.
The ghost predicate $\Proph{p}{\vec{v}}$ says that the prophecy variable $p$ will be resolved, in the future, with values from the vector $\vec{v}$.
Initially, a prophecy variable created with $\newProph$ has an arbitrary vector $\vec{v}$ associated with it.
Only after symbolically executing $\resolveProph{p}{\valB}$ we learn that this vector $\vec{v}$ contains $\valB$ at the head position.
The trick behind the prophecy variables ghost state is that we can already refer to the head element of $\vec{v}$ before resolving it to some $\valB$.
We will see how to use this in establishing the refinement between the lazy coin and the eager coin in the next section.
Note that the rules for the left-hand side are written in logically atomic style: compare, for example, rel-resolveproph-l and rel-store-l.

To see how the instrumented instructions for prophecy variables are used, suppose we want to prove a contextual refinement $\ctxref{}{\expr_1}{\expr_2}{\type}$ that involves speculative reasoning.
We first prove a refinement $\hat \expr_1 \lrel \expr_2 : \type$, where $\hat \expr_1$ is a version of $\expr_1$ instrumented with prophecy variables, and then prove $\expr_1 \lrel \hat \expr_1 : \type$ to show that the prophecy variables can be erased.
By soundness of and transitivity of contextual refinement, this gives a contextual refinement $\ctxref{}{\expr_1}{\expr_2}{\type}$ that refers only to the original programs.

§.§ Proving the coin refinement

To prove the refinement $\logrel{}{\newcoinLazy}{\newcoin}{(\tunit \to \tunit) \times (\tunit \to \tbool)}$ from <Ref> we instrument the lazy implementation $\newcoinLazy$ with prophecy variables so we can speculate on the outcome of $\rand$ in $\readcoinLazy$.
The instrumented implementation $\newcoinLazyI$ is shown in <Ref>.
In addition to prophecy variables, we also instrumented the implementation with locks to ensure that there is no interference between updating the reference $c$ and resolving the prophecy variable $p$.
With the instrumented program at hand, we will prove the chain of refinements:

\begin{align*}
& \logrel{}{\newcoinLazy}{\newcoinLazyI}{(\tunit \to \tunit) \times (\tunit \to \tbool)}\\
& \logrel{}{\newcoinLazyI}{\newcoin}{(\tunit \to \tunit) \times (\tunit \to \tbool)}.
\label{reloc:eq:coin_instrumented_refinements}
\end{align*}

Via 's soundness theorem, we can compose these refinements at the level of contextual refinement to obtain:

\[
\ctxref{}{\newcoinLazy}{\newcoin}{(\tunit \to \tunit) \times (\tunit \to \tbool)}.
\]

Note that that we only use the instrumented implementation $\newcoinLazyI$ for the intermediate step, which means that prophecy variables and locks do not appear at all in the final statement above.
The approach of using prophecies as an intermediate step works not just for closed programs, but also for open programs, as it does not rely on an erasure theorem <cit.>.
Moreover, as the example demonstrates, it allows us to make use of locks in the instrumented program.[Atomic prophecy resolution was introduced in [59] as an alternative to locks to deal with atomicity of prophecy resolution.].

The first refinement ($\newcoinLazy \lrel \newcoinLazyI$) is easy to prove, we simply use the no-op symbolic execution rules for prophecies on the right-hand side (<Ref>).
The second refinement ($\newcoinLazyI \lrel \newcoin$) is where the mechanism of prophecy variables comes to help.
We symbolically execute the allocation parts of $\newcoinLazyI$ and $\newcoin$.
We then use the relational specification for locks (<Ref>) with the following lock invariant:

\[
\Exists \vec{v}. \Proph{p}{\vec{v}} \ast
\big(
(c_l \mapstoI \NONE \ast c \mapstoS (hd\ \vec{v}))
\vee \spac (\Exists (b : \mathbb{B}). c_l \mapstoI \SOME(b) \ast c \mapstoS b)
\big).
\]

This invariant says that if the value of the lazy coin is $\NONE$, then the value of the eager coin is determined by the prophecy variable $p$.
There are two main implications of this:

* In the refinement between $\flipcoinLazyI$ and $\flipcoin$, the invariant can be (re)established, because we can pick the value of $\rand\ \unittt$ on the right-hand side to be the head element of $\vec{v}$—the future value of the lazy coin is already bound at this point.

* In the refinement between $\readcoinLazyI$ and $\readcoin$ (specifically, in the $\NONE$ branch), we obtain a non-deterministic Boolean $x$ from symbolically executing $\rand\ \unittt$ on the left-hand side, and we update the value of $c_l$ to be $x$.
Moreover, we resolve the prophecy variable $p$ to $x$, which gives us much desired information: the head element of $\vec{v}$ was $x$ all along!
This information allows us to transition from the left disjunct to the right disjunct in the invariant and complete the proof.

§.§ Algebraic reasoning about non-deterministic choice

In this section we give another example of the use of prophecy variables: we verify several algebraic properties of non-deterministic choice modulo contextual equivalence.
(In)equational theories of the non-deterministic choice operator were previously considered in the context of domain theory, where non-determinism is usually modeled using power domains [83, 92], and in the context of algebraic effects [95, 62].
Power domains and the denotational semantics approach does not seem to scale easily to languages with concurrency and higher-order store.
An operational approach to equational theory of a programming language with non-determinism was considered in [12] using step-indexed logical relations.
There the authors show several contextual equivalences involving non-determinism, both finite (picking a Boolean) and countable (picking a natural number).
In this subsection, we provide conceptually simple proofs for contextual equivalences involving finite non-determinism only.
However, we were also able to prove that non-deterministic choice and sequential composition distribute over each other.
Proving this crucially relies on speculative reasoning which we formalize using prophecy variables.

We do not have a non-deterministic choice operation built-in the language, but we can define it using the $\rand$ function from <Ref>.
The operation $\orFn$ non-deterministically executes one of its thunked arguments:

\[
\orFn\spac \exprB_1\spac \exprB_2 \eqdef{}
\If \rand\ \unittt then \exprB_1\ \unittt \Else \exprB_2\ \unittt
\]

We write $\expr_1 \orOp \expr_2$ for $\orFn\ (\Lam \unittt. \expr_1)\ (\Lam \unittt. \expr_2)$.
The expression $\expr_1 \orOp \expr_2$ thus non-deterministically reduces to either $\expr_1$ or $\expr_2$.
From the rules for the $\rand$ function (<Ref>), we derive the following symbolic execution rules for $\orOp$:

Δ[_1 _2]

[]Δ[_1 _2]
[]Δ[_1 _2]

The rules for $\orOp$ are reminiscent of the rules for disjunction ($\vee$) in sequent calculus.
To symbolically execute $\orOp$ on the left-hand side (to eliminate $\vee$) it is necessary to establish refinements for both operands (to consider both disjuncts), and to symbolically execute $\orOp$ on the right-hand side (to introduce $\vee$) it suffices to establish a refinement for one of the operands (prove one of the disjuncts).

Assume that $\expr_1, \expr_2, \expr_3$ are closed programs of type $\type$.
Then using rel-or-r-1, rel-or-r-2, and rel-or-l, we prove the following equivalences:

_1_1 _1
_1 _2_2 _1
_1 (_2 _3)(_1 _2) _3
(_1 _2) ; _3(_1 ; _3) (_2 ; _3)

The equational theory that we obtain here is similar to the one obtained from the Hoare power domain, as ${\expr_1 \orOp \diverge}$ (where $\diverge$ is an infinite loop) is identified with $\expr_1$.
The last equation states that non-deterministic choice distributes over sequential composition, and is standard in, process calculi.
What is less standard is the following equation, which is not validated by models based on bisimulation:

\[
\ctxequiv{}{\expr_1 ; (\expr_2 \orOp \expr_3)}{(\expr_1 ; \expr_2) \orOp (\expr_1 ; \expr_3)}{\type}.
\]

This equation, however, holds in Kleene algebra-like models [50, 67].
If we think about proving this equation using the symbolic execution rules for $\orOp$, then we can observe that proving the refinement in right-to-left direction

\[
\logrel{}{(\expr_1 ; \expr_2) \orOp (\expr_1 ; \expr_3)}{\expr_1 ; (\expr_2 \orOp \expr_3)}{\type}
\]

is possible, and, by rel-or-l, it boils down to proving two refinements:

\[
\logrel{}{\expr_1 ; \expr_2}{\expr_1 ; (\expr_2 \orOp \expr_3)}{\type}
\qquad
\logrel{}{\expr_1 ; \expr_3}{\expr_1 ; (\expr_2 \orOp \expr_3)}{\type}.
\]

However, proving the refinement in left-to-right direction is harder:

\[
\logrel{}{\expr_1 ; (\expr_2 \orOp \expr_3)}{(\expr_1 ; \expr_2) \orOp (\expr_1 ; \expr_3)}{\type}.
\]

If we want to use the symbolic execution rules for $\orOp$, we have to “synchronize” both sides on $\expr_1$.
To do that, we have to pick a branch for $\orOp$ on the right-hand side before we get to use rel-or-l on the left-hand side, but we do not know ahead of time which branch to pick.
To resolve this dependency, we use a prophecy variable to speculate on which branch $\expr_2 \orOp \expr_3$ will be taken on the left-hand side, and use the value of this prophecy variable to choose the appropriate branch of ${(\expr_1 ; \expr_2) \orOp (\expr_1 ; \expr_3)}$ on the right-hand side.

The intermediate program that is instrumented with prophecy variables is as follows:

\begin{align*}
& \Let p {} = \newProph in \\
& \expr_1 ;\
\big((\resolveProph{p}{0}; \expr_2) \orOp (\resolveProph{p}{1}; \expr_3)\big)
\end{align*}

We can easily verify that the original program ${\expr_1 ; (\expr_2 \orOp \expr_3)}$ refines the instrumented one.
To verify that the instrumented program refines ${(\expr_1 ; \expr_2) \orOp (\expr_1 ; \expr_3)}$ we symbolically execute $\newProph$ and obtain a predicate $\Proph{p}{\vec{v}}$ associating a vector of future values $\vec{v}$ to the newly created prophecy variable $p$.
Then we examine the head element $\valB$ of the prophecy values $\vec{v}$.
If $\valB$ is $0$, then we apply rel-or-r-1, otherwise we apply rel-or-r-2.
Without loss of generality, suppose that $\valB$ is $0$; that is, $\vec{v} = \conS{0}{\vec{\valB}}$ for some tail $\vec{\valB}$.
First we “synchronize” the refinement proof on $\expr_1$ on both sides.
Then we apply rel-or-l.
Because the premises of rel-or-l are joined by intuitionistic conjunction $\wedge$, we can use the resource $\Proph{p}{\vec{v}}$ for verifying both refinements:

\begin{align*}
& \Proph{p}{\conS{0}{\vec{v'}}} \wand \logrel{}{\resolveProph{p}{0}; \expr_2}{\expr_2}{\type} \\
& \Proph{p}{\conS{0}{\vec{v'}}} \wand \logrel{}{\resolveProph{p}{1}; \expr_3}{\expr_2}{\type}
\end{align*}

The first refinement is reduced to $\logrel{}{\expr_2}{\expr_2}{\type}$, which follows from the fundamental property (<Ref>) and the assumption that $\expr_2$ is well-typed.
To prove the second refinement we symbolically execute $\resolveProph{p}{1}$ on the left-hand side, at which point we reach a contradiction $0=1$.

§ THE LOGICAL RELATIONS MODEL OF

extends Iris with logical connectives and corresponding proof rules for reasoning about refinements.
In this section we show how this is achieved by modeling the connectives of through a shallow embedding in Iris and proving the logical rules of as mere lemmas in Iris.
We describe how the refinement judgment $\logrel{}{\expr_1}{\expr_2}{\type}$ is modeled through Iris's weakest preconditions and a ghost thread pool construction (<Ref>) combined with a binary logical relation $\Sem{\type}_\Delta$ that describes when values are related (<Ref>).
We then summarize how the proof rules (<Ref>) and soundness theorem (<Ref>) are proved.
The key definitions of the model are shown in <Ref>.

The construction of our model generalizes prior work by Turon  [102, 97], which culminated in the CaReSL logic, and was subsequently mechanized in Iris by Krebbers  [68] and Timany [98].
We discuss the differences in <Ref>.

Refinement judgments:

\begin{align*}
\logrel[\mask]{\Delta & }{\expr_1}{\expr_2}{\type} \eqdef
\All i,\lctx.
\begin{array}[t]{@{} l}
\specctx \wand i \tpto \fillctx\lctx[\expr_2] \vsW[\mask][\top] \\
\wpre{\expr_1}{\Ret \val_1. \Exists \val_2. i \tpto \fillctx\lctx[\val_2] \ast \Sem{\type}_{\Delta}(\val_1, \val_2)}
\end{array}
\end{align*}

Interpretation of types:

\begin{align*}
\Sem{\tvar}_{\Delta} \eqdef{}& \Lam (\val_1, \val_2). \Delta(\tvar)(\val_1, \val_2) \\
\Sem{\tunit}_\Delta \eqdef{}& \Lam (\val_1, \val_2). \val_1 = \val_2 = \unittt \\
\Sem{\tbool}_\Delta \eqdef{}& \Lam (\val_1, \val_2). (\val_1 = \val_2 = \<true>) \vee (\val_1 = \val_2 = \<false>) \\
\Sem{\tint}_\Delta \eqdef{}& \Lam (\val_1, \val_2). \Exists n \in \mathbb{Z}. \val_1 = \val_2 = n \\
\Sem{\type \times \typeB}_\Delta \eqdef{}& \Lam (\val_1, \val_2).
\Exists \valB_1,\valB_2,\valB'_1,\valB'_2.
\begin{array}[t]{@{}l}
\val_1 = (\valB_1, \valB_2) \ast \val_2 = (\valB'_1, \valB'_2) \ast{} \\
\Sem{\type}_\Delta(\valB_1, \valB'_1) \ast
\Sem{\typeB}_\Delta(\valB_2, \valB'_2)
\end{array}\\
\Sem{\type + \typeB}_\Delta \eqdef{}& \Lam (\val_1, \val_2).
\Exists \valB_1,\valB_2.
\begin{array}[t]{@{}l}
\left( \val_1 = \<inl>(\valB_1) \ast \val_2 = \<inl>(\valB_2) \ast{}
\Sem{\type}_{\Delta}(\valB_1, \valB_2) \right) \vee{} \\
\left( \val_1 = \<inr>(\valB_1) \ast \val_2 = \<inr>(\valB_2) \ast
\Sem{\typeB}_{\Delta}(\valB_1, \valB_2) \right)
\end{array}\\
\Sem{\type \to \typeB}_\Delta \eqdef{}& \Lam (\val_1, \val_2).
\always \left(\All \valB_1,\valB_2. \Sem{\type}_{\Delta}(\valB_1, \valB_2) \wand
(\logrel{\Delta}{\val_1\ \valB_1}{\val_2\ \valB_2}{\typeB})\right) \\
\Sem{\tforall{\Ret \tvar.\type}}_\Delta \eqdef{}& \Lam (\val_1, \val_2).
\always \left(\All \pred \in \Val \times \Val \to \PersistentProp.
(\logrel{\deltainsert{\tvar}{\pred}{\Delta}}{\tapp{\val_1}}{\tapp{\val_2}}{\type})\right) \\
\Sem{\texists{\Ret \tvar.\type}}_\Delta \eqdef{}& \Lam (\val_1, \val_2).
\Exists \pred \in \Val \times \Val \to \PersistentProp. \Sem{\type}_{\deltainsert{\tvar}{\pred}{\Delta}}(\val_1, \val_2) \\
\Sem{\trec{\Ret \tvar.\type}}_{\Delta} \eqdef{}& \MU \pred. \Lam (\val_1, \val_2).
\Exists \valB_1,\valB_2. \val_1 = \<fold>(\valB_1) \ast
\val_2 = \<fold>(\valB_2) \ast
\later \Sem{\type}_{\deltainsert{\tvar}{\pred}{\Delta}}(\valB_1, \valB_2) \\[0.3em]
\Sem{\tref\ \type}_{\Delta} \eqdef{}& \Lam (\val_1, \val_2).
\Exists \loc_1,\loc_2 \in \Loc.
\begin{array}[t]{@{}l}
\val_1 = \loc_1 \ast \val_2 = \loc_2 \ast{} \\
\knowInv{(\loc_1, \loc_2)}
\Exists \valB_1,\valB_2. \loc_1 \mapstoI \valB_1 \ast \loc_2 \mapstoS \valB_2 \ast \Sem{\type}_{\Delta}(\valB_1, \valB_2)
\end{array}
\end{align*}

The model of in Iris.

§.§ The refinement judgment

Recall from <Ref> that the intuitive meaning of the refinement proposition $\logrel{}{\expr_1}{\expr_2}{\type}$ is that any behavior of $\expr_1$ can be simulated by some behavior of $\expr_2$.
This intuitive idea is modeled in Iris as follows:

\begin{align*}
\logrel[\mask]{\Delta & }{\expr_1}{\expr_2}{\type} \eqdef
\All i,\lctx.
\begin{array}[t]{@{} l}
\specctx \wand i \tpto \fillctx\lctx[\expr_2] \vsW[\mask][\top] \\
\wpre{\expr_1}{\Ret \val_1. \Exists \val_2. i \tpto \fillctx\lctx[\val_2] \ast \Sem{\type}_{\Delta}(\val_1, \val_2)}
\end{array}
\end{align*}

This definition is quite a mouthful, so let us go over it piece by piece.
First, it involves Iris's weakest precondition connective $\wpre {\expr} \pred$, which gives the weakest precondition under which execution of $\expr$ is safe, and when $\expr$ returns with value $\val$, the postcondition $\pred(\val)$ holds.
Second, it involves the ghost thread pool connective $i \tpto \expr$, which is defined through Iris's ghost theory, and states that the $i$-th ghost thread is executing a program $\expr$.
Putting these pieces together (ignoring $\specctx$ and $\vsW[\mask][\top]$ for now), this definition states that if a (ghost) thread $i$ is executing right-hand side $\expr_2$, and left-hand side $\expr_1$ reduces to some value $\val_1$, then a corresponding execution can be made so that (ghost) thread $i$ is executing right-hand side $\val_2$.
The result values $\val_1$ and $\val_2$ of the left-hand and right-hand side should be related via the value interpretation $\Sem{\type}_{\Delta}(\val_1, \val_2)$, which we model in <Ref> via a logical relation.
The quantification over $\lctx$ closes the definition under evaluation contexts.
The expression $\expr_1$ on the left-hand side does not need to be closed under evaluation contexts because weakest preconditions enjoy the rule: $\wpre \expr {\Ret \valB. \wpre {\fillctx\lctx[\valB]} \pred} \wand
\wpre {\fillctx\lctx[\expr]} \pred$.

The ghost thread pool predicates satisfy a number of symbolic execution rules corresponding to executions in the operational semantics.
A selection of these rules is given in <Ref>.
The $\specctx$ proposition is an Iris invariant that ties together the thread pool connectives $i \tpto \expr$ and the heap assertions $\loc \mapstoS \val$ with a matching execution on the right-hand side.
We will explain the role of $\specctx$ in <Ref>.

We should emphasize that the combination of the weakest precondition and the ghost thread pool in the definition of $\logrel[\mask]{\Delta}{\expr_1}{\expr_2}{\type}$ model the demonic nature of $\expr_1$ and the angelic nature of $\expr_2$.
To prove the weakest precondition $\wpre{\expr_1}{\Ret \val_1. \Exists \val_2. i \tpto \fillctx\lctx[\val_2] \ast \Sem{\type}_{\Delta}(\val_1, \val_2)}$ one has to consider all behaviors of $\expr_1$, but has to establish only a single matching execution for $\expr_2$ by using the appropriate rules for the ghost thread pool.

§.§ The logical relation

The interpretation of types $\Sem{\type}_{\Delta}(\val_1, \val_2)$, as defined in <Ref>, expresses when two values $\val_1$ and $\val_2$ are related at type $\type$ (in context $\Delta$).
The definition of $\Sem{\type}_{\Delta}(\val_1, \val_2)$ follows the usual structure of a logical relation, it is defined recursively on the structure of the type $\type$ and uses the corresponding logical connectives via the Curry-Howard isomorphism.
For example, products are defined via (separating) conjunction, sums are defined via disjunction, functions are defined via (separating) implication, universal types are defined via universal quantification,

The interpretation of recursive types and reference types are somewhat more interesting, as they make use of Iris-specific connectives.
The interpretation of the recursive type $\trec{\Ret \tvar.\type}$ makes use of Iris's guarded fixed point operator $\MU \var. \term$, which is used to define recursive predicates without a restriction of the variance of the recursive occurrence $\var$ in $\term$, but requires $\var$ to appear in guarded position, under the later modality $\later$ <cit.>.
To define the interpretation of the reference type $\tref\ \type$, we use the invariant

\[
\knowInv{(\loc_1, \loc_2)}
\Exists \valB_1,\valB_2. \loc_1 \mapstoI \valB_1 \ast \loc_2 \mapstoS \valB_2 \ast \Sem{\type}_{\Delta}(\valB_1, \valB_2)
\]

which states that whatever values are stored in $\loc_1$ and $\loc_2$ are always related at type $\Sem{\type}_{\Delta}$.

The persistence modality $\always$ in the interpretation for function types and universal types is used to ensure that the type interpretation is persistent and prevents the kind of issues described in <Ref>.
Similarly, in the interpretation of the universal and existential types we quantify over a persistent predicate $\pred \in \Val \times \Val \to \PersistentProp$, where $\PersistentProp$ is the subset of Iris propositions that is persistent.

§.§ Differences with prior work.

The definition of the refinement $\logrel[\mask]{\Delta}{\expr_1}{\expr_2}{\type}$ and value interpretation $\Sem{\type}_{\Delta}(\val_1, \val_2)$ generalize the versions by Krebbers  [68] and Timany  [98], which in turn adapted ghost thread pools by Turon  [102, 97] by modeling these in Iris.
The main novelty is that our refinement judgment $\logrel[\mask]{\Delta}{\expr_1}{\expr_2}{\type}$ is a first-class Iris proposition, instead of a meta-logical proposition.
As we have demonstrated throughout this paper, this modification is simple, albeit crucial for writing conditional refinements and to obtain high-level proof rules for refinements.

Furthermore, to obtain high-level proof rules for invariants, we have equipped the refinement judgment with a mask $\mask$, which keeps track of the invariants that may be opened.
To give the appropriate semantics to the mask $\mask$, our definition involves the update modality $\vsW[\mask][\top]$.
Note that the definition by Krebbers  [68] and Timany [98] is logically equivalent to $\vdash \logrel[\top]{\Delta}{\expr_1}{\expr_2}{\type}$, where the derivability relation $\proves$ of Iris is used to turn the judgment into a meta theoretical proposition, and the mask is set to $\top$.

§.§ Deriving the primitive rules

In <Ref> we have demonstrated that 's primitive monadic (rel-return and rel-bind) and symbolic execution rules can be used to derive 's high-level proof rules, such as its type-directed structural rules.
In this section, we indicate how 's primitive rules are proved by unfolding the definition of the refinement judgment.
We prove the symbolic execution rules through the following auxiliary rules, which allow us to lift Iris's rules for weakest preconditions and the ghost thread pool rules (<Ref>) to the refinement judgment:

_1[⊤]_1. [_1]_2
[⊤][] _1[]_1. [][_1]_2
j, '. ∗j '[[_2]]
[] _2. j '[[_2]] ∗