11institutetext: 1Inria Paris, France 2UAIC Iaşi, Romania 3MPI-SWS,
Saarbrücken, Germany 4Stanford University, Stanford, USA
5CISPA, Saarbrücken, Germany 6University of Chile, Santiago, Chile

# Trace-Relating Compiler Correctness
and Secure Compilation

Carmine Abate1 Roberto Blanco1 Stefan Ciobâcă2 Adrien Durier1
Deepak Garg3 Cătălin Hritcu1 Marco Patrignani4,5 Éric Tanter6,1 Jérémy
Thibault1

###### Abstract

Compiler correctness is, in its simplest form, defined as the inclusion of the
set of traces of the compiled program into the set of traces of the original
program, which is equivalent to the preservation of all trace properties. Here
traces collect, for instance, the externally observable events of each
execution. This definition requires, however, the set of traces of the source
and target languages to be exactly the same, which is not the case when the
languages are far apart or when observations are fine-grained. To overcome
this issue, we study a generalized compiler correctness definition, which uses
source and target traces drawn from potentially different sets and connected
by an arbitrary relation. We set out to understand what guarantees this
generalized compiler correctness definition gives us when instantiated with a
non-trivial relation on traces. When this trace relation is not equality, it
is no longer possible to preserve the trace properties of the source program
unchanged. Instead, we provide a generic characterization of the target trace
property ensured by correctly compiling a program that satisfies a given
source property, and dually, of the source trace property one is required to
show in order to obtain a certain target property for the compiled code. We
show that this view on compiler correctness can naturally account for
undefined behavior, resource exhaustion, different source and target values,
side-channels, and various abstraction mismatches. Finally, we show that the
same generalization also applies to many secure compilation definitions, which
characterize the protection of a compiled program against linked adversarial
code.

##  1 Introduction

Compiler correctness is an old idea [38, 41, 42] that has seen a significant
revival in recent times. This new wave was started by the creation of the
CompCert verified C compiler [34] and continued by the proposal of many
significant extensions and variants of CompCert [61, 43, 63, 31, 30, 8, 67,
23, 56, 12, 9] and the success of many other milestone compiler verification
projects, including Vellvm [70], Pilsner [46], CakeML [64], CertiCoq [4], etc.
Yet, even for these verified compilers, the precise statement of correctness
matters. Since proof assistants are used to conduct the verification, an
external observer does not have to understand the proofs in order to trust
them, but one still has to deeply understand the statement that was proved.
And this is true not just for correct compilation, but also for secure
compilation, which is the more recent idea that our compilation chains should
do more to also ensure security of our programs [26, 3].

Basic Compiler Correctness. The gold standard for compiler correctness is
semantic preservation, which intuitively says that the semantics of a compiled
program (in the target language) is compatible with the semantics of the
original program (in the source language). For practical verified compilers,
such as CompCert [34] and CakeML [64], semantic preservation is stated
extrinsically, by referring to traces. In these two settings, a trace is an
ordered sequence of events—such as inputs from and outputs to an external
environment—that are produced by the execution of a program.

A basic definition of compiler correctness can be given by the set inclusion
of the traces of the compiled program into the traces of the original program.
Formally [34]:

######  Definition 1 (Basic Compiler Correctness ($\mathsf{CC}$))

A compiler $\downarrow$ is correct iff

$\forall\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{W}}}~{}t.~{}\mathbf{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\left.\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{W}}}\right\downarrow}}}}}\mathbf{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}{\bm{\rightsquigarrow}}}}t\Rightarrow\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{W}}}\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>
This definition says that for any whole111For simplicity, for now we ignore
separate compilation and linking, returning to it in § 5.  source program
$\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>if we compile it (denoted
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\left.\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{W}}}\right\downarrow}}$),
execute it with respect to the semantics of the target language, and observe a
trace $t$, then the original
$\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>can produce the same trace $t$ with respect to the semantics of the source
language.222Typesetting convention [50]: we use a
$\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>$\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>font for
$\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>elements, an
$\mathbf{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color<EMAIL_ADDRESS>$\mathbf{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color<EMAIL_ADDRESS>font for
$\mathbf{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color<EMAIL_ADDRESS>ones and a
$\mathit{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{black}}}$,
$\mathit{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{italic}}}$
font for elements common to both languages.  This definition is simple and
easy to understand, since it only references a few familiar concepts: a
compiler between a source and a target language, each equipped with a trace-
producing semantics (usually nondeterministic).

Beyond Basic Compiler Correctness. This basic compiler correctness definition
assumes that any trace produced by a compiled program can be produced by the
source program. This is a very strict requirement, and in particular implies
that the source and target traces are drawn from the same set and that the
same source trace corresponds to a given target trace. These assumptions are
often too strong, and hence in practice verified compiler efforts use
different formulations of compiler correctness:

CompCert [34]

The original compiler correctness theorem of CompCert [34] can be seen as an
instance of basic compiler correctness, but it does not provide any guarantees
for programs that can exhibit undefined behavior [57]. As allowed by the C
standard, such unsafe programs are not even considered to be in the source
language, so are not quantified over. This has important practical
implications, since undefined behavior often leads to exploitable security
vulnerabilities [25, 13, 24] and serious confusion even among experienced C
and C++ developers [57, 33, 66, 65]. As such, since 2010, CompCert provides an
additional top-level correctness theorem333Stated at the top of the CompCert
file driver/Complements.v and discussed by Regehr [57]. that better accounts
for the presence of unsafe programs by providing guarantees for them up to the
point when they encounter undefined behavior [57]. This new theorem goes
beyond the basic correctness definition above, as a target trace need only
correspond to a source trace _up to the occurrence_ of undefined behavior in
the source trace.

CakeML [64]

Compiler correctness for CakeML accounts for memory exhaustion in target
executions. Crucially, memory exhaustion events cannot occur in source traces,
only in target traces. Hence, dually to CompCert, compiler correctness only
requires source and target traces to coincide up to the occurrence of a memory
exhaustion event in the target trace.

Trace-Relating Compiler Correctness. Generalized formalizations of compiler
correctness like the ones above can be naturally expressed as instances of a
uniform definition, which we call trace-relating compiler correctness. This
generalizes basic compiler correctness by (a) considering that source and
target traces belong to possibly distinct sets
$\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>and
$\mathbf{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color<EMAIL_ADDRESS>and (b) being parameterized by an arbitrary trace relation $\sim$.

######  Definition 2 (Trace-Relating Compiler Correctness
($\mathsf{CC^{\sim}}$))

A compiler $\downarrow$ is correct with respect to a trace relation
$\sim\,\subseteq\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{Trace_{S}}}}\times\mathbf{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color<EMAIL_ADDRESS>iff

$\forall\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{W}}}.\forall\mathbf{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}{t}}}.~{}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\left.\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{W}}}\right\downarrow}}\mathbf{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}{\bm{\rightsquigarrow}}}}\mathbf{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}{t}}}\Rightarrow\mathrel{\exists\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{s}}}\sim\mathbf{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}{t}}}}\ldotp\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{W}}}\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{\bm{\rightsquigarrow}}}}\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>
This definition requires that, for any target trace
$\mathbf{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color<EMAIL_ADDRESS>produced by the compiled program
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\left.\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>there exist a source trace
$\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>that can be produced by the original program
$\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>and is related to
$\mathbf{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color<EMAIL_ADDRESS>according to $\sim$ (i.e.,
$\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{s}}}\sim\mathbf{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}{t}}}$).
By choosing the trace relation appropriately, one can recover the different
notions of compiler correctness presented above:

Basic CC

Take
$\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{s}}}\sim\mathbf{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color<EMAIL_ADDRESS>to be
$\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{s}}}=\mathbf{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color<EMAIL_ADDRESS>Trivially, the basic CC of 1 is $\mathsf{CC^{=}}$.

CompCert

Undefined behavior is modeled in CompCert as a trace-terminating event
$\mathit{Goes\\_wrong}$ that can occur in any of its languages (source,
target, and all intermediate languages), so for a given phase (or composition
thereof), we have
$\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{Trace_{S}}}}=\mathbf{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color<EMAIL_ADDRESS>Nevertheless, the relation between source and target traces with which to
instantiate $\mathsf{CC^{\sim}}$ to obtain CompCert’s current theorem is:

$\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{s}}}\sim\mathbf{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}{t}}}\quad\equiv\quad\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{s}}}=\mathbf{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}{t}}}\vee(\exists
m\leq\mathbf{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}{t}}}.~{}\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{s}}}=m{\cdot}\mathit{Goes\\_wrong}).$

A compiler satisfying $\mathsf{CC^{\sim}}$ for this trace relation can turn a
source trace ending in undefined behavior $m{\cdot}\mathit{Goes\\_wrong}$
(where “${\cdot}$” is concatenation) either into the same trace in the target
(first disjunct), or into a target trace that starts with the prefix $m$ but
then continues arbitrarily (second disjunct, “${\leq}$” is the prefix
relation).

CakeML

Here, target traces are sequences of symbols from an alphabet
$\mathbf{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color<EMAIL_ADDRESS>that has a specific trace-terminating event,
$\mathbf{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color<EMAIL_ADDRESS>which is not available in the source alphabet
$\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>(i.e.,
$\mathbf{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}{\Sigma_{T}}}}=\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{\Sigma_{S}}}}\cup\\{\mathbf{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color<EMAIL_ADDRESS>Then, the compiler correctness theorem of CakeML can be obtained by
instantiating $\mathsf{CC^{\sim}}$ with the following $\sim$ relation:

$\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{s}}}\sim\mathbf{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}{t}}}\quad\equiv\quad\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{s}}}=\mathbf{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}{t}}}\vee(\exists
m.~{}m\leq\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{s}}}.~{}\mathbf{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}{t}}}=m{\cdot}\mathbf{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}{Resource\\_limit\\_hit}}}).$

The resulting $\mathsf{CC^{\sim}}$ instance relates a target trace ending in
$\mathbf{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color<EMAIL_ADDRESS>after executing $m$ to a source trace that first produces $m$ and then
continues in a way given by the semantics of the source program.

Beyond undefined behavior and resource exhaustion, there are many other
practical uses for $\mathsf{CC^{\sim}}$: in this paper we show that it also
accounts for differences between source and target values, for a single source
output being turned into a series of target outputs, and for side-channels.

On the flip side, the compiler correctness statement and its implications can
be more difficult to understand for $\mathsf{CC^{\sim}}$ than for
$\mathsf{CC^{=}}$. The full implications of choosing a particular $\sim$
relation can be subtle. In fact, using a bad relation can make the compiler
correctness statement trivial or unexpected. For instance, it should be easy
to see that if one uses the total relation, which relates all source traces to
all target ones, the $\mathsf{CC^{\sim}}$ property holds for every compiler,
yet it might take one a bit more effort to understand that the same is true
even for the following relation:

$\displaystyle\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{s}}}\sim\mathbf{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}{t}}}\quad\equiv\quad\exists\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{W}}}.\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{W}}}\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{\bm{\rightsquigarrow}}}}\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{s}}}\wedge{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\left.\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{W}}}\right\downarrow}}\mathbf{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}{\bm{\rightsquigarrow}}}}\mathbf{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color<EMAIL_ADDRESS>
Reasoning About Trace Properties. To understand more about a particular
$\mathsf{CC^{\sim}}$ instance, we propose to also look at how it preserves
trace properties—defined as sets of allowed traces [32]—from the source to the
target. For instance, it is well known that $\mathsf{CC^{=}}$ is equivalent to
the preservation of all trace properties (where $W\models\pi$ reads “$W$
satisfies $\pi$” and stands for $\forall
t.~{}W{\bm{\rightsquigarrow}}t\Rightarrow t\in\pi$):

$\mathsf{CC^{=}}\quad\equiv\quad\forall\pi\in
2^{\text{Trace}}~{}\forall\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{W}}}.~{}\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{W}}}\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{\models}}}\pi\Rightarrow{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\left.\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{W}}}\right\downarrow}}\bm{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color<EMAIL_ADDRESS>
However, to the best of our knowledge, similar results have not been
formulated for trace relations beyond equality, when it is no longer possible
to preserve the trace properties of the source program unchanged. For trace-
relating compiler correctness, where source and target traces can be drawn
from different sets and related by an arbitrary trace relation, there are two
crucial questions to ask:

  1. 1.

For a source trace property
$\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>of a program—established for instance by formal verification—what is the
strongest target property that any $\mathsf{CC^{\sim}}$ compiler is guaranteed
to ensure for the produced target program?

  2. 2.

For a target trace property
${\bm{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color<EMAIL_ADDRESS>what is the weakest source property we need to show of the original source
program to obtain
$\bm{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color<EMAIL_ADDRESS>for the result of any $\mathsf{CC^{\sim}}$ compiler?

Far from being mere hypothetical questions, they can help the developer of a
verified compiler to better understand the compiler correctness theorem they
are proving, and we expect that any user of such a compiler will need to ask
either one or the other if they are to make use of that theorem. In this work
we provide a simple and natural answer to these questions, for any instance of
$\mathsf{CC^{\sim}}$. Building upon a bijection between relations and Galois
connections [20, 5, 44], we observe that any trace relation $\sim$ corresponds
to two property mappings $\tilde{\tau}$ and $\tilde{\sigma}$, which are
functions mapping source properties to target ones ($\tilde{\tau}$ standing
for “to target”) and target properties to source ones ($\tilde{\sigma}$
standing for “to source”):

$\tilde{\tau}(\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{\pi_{S}}}})=\left\\{\mathbf{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}{t}}}\,\mathrel{}\middle|\mathrel{}\,\exists\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{s}}}\ldotp\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{s}}}\sim\mathbf{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}{t}}}\wedge\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{s}}}\in\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{\pi_{S}}}}\right\\};\qquad\tilde{\sigma}(\bm{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}{\pi_{\mathrm{T}}}}})=\left\\{\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{s}}}\,\mathrel{}\middle|\mathrel{}\,\forall\mathbf{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}{t}}}\ldotp\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{s}}}\sim\mathbf{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}{t}}}\Rightarrow\mathbf{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}{t}}}\in\bm{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color<EMAIL_ADDRESS>
The _existential image_ of $\sim$, $\tilde{\tau}$, answers the first question
above by mapping a given source property
$\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>to the target property that contains all target traces for which there exists
a related source trace that satisfies
$\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>Dually, the _universal image_ of $\sim$, $\tilde{\sigma}$, answers the second
question by mapping a given target property
$\bm{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color<EMAIL_ADDRESS>to the source property that contains all source traces for which all related
target traces satisfy
$\bm{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color<EMAIL_ADDRESS>We introduce two new correct compilation definitions in terms of trace
property preservation ($\mathsf{TP}$): $\mathsf{TP^{\tilde{\tau}}}$ quantifies
over all source trace properties and uses $\tilde{\tau}$ to obtain the
corresponding target properties. $\mathsf{TP}^{\tilde{\sigma}}$ quantifies
over all target trace properties and uses $\tilde{\sigma}$ to obtain the
corresponding source properties. We prove that these two definitions are
equivalent to $\mathsf{CC^{\sim}}$, yielding a novel trinitarian view of
compiler correctness (Figure 1).

$\sim$
$\mathsf{CC^{\sim}}$$\mathsf{TP^{\tilde{\tau}}}$$\mathsf{TP^{\tilde{\sigma}}}$$\forall\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{W}}}.~{}\forall\mathbf{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}{t}}}.~{}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\left.\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{W}}}\right\downarrow}}\mathbf{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}{\bm{\rightsquigarrow}}}}\mathbf{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}{t}}}\Rightarrow\mathrel{\exists\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{s}}}\sim\mathbf{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}{t}}}}\ldotp\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{W}}}\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{\bm{\rightsquigarrow}}}}\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>$\begin{aligned}
&\forall\bm{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}{\pi_{\mathrm{T}}}}}.~{}\forall\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{W}}}.~{}\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{W}}}~{}\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{\models}}}~{}\tilde{\sigma}(\bm{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}{\pi_{\mathrm{T}}}}})\\\
&\
\Rightarrow{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\left.\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{W}}}\right\downarrow}}~{}\bm{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}{\models}}}~{}\bm{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color<EMAIL_ADDRESS>$\equiv\begin{aligned}
&\forall\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{\pi_{S}}}}.~{}\forall\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{W}}}.~{}\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{W}}}~{}\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{\models}}}~{}\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>&\
\Rightarrow{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\left.\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{W}}}\right\downarrow}}~{}\bm{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}{\models}}}~{}\tilde{\tau}(\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{\pi_{S}}}})\end{aligned}$
$\equiv$ Figure 1: The equivalent compiler correctness definitions forming our
trinitarian view.

Contributions.

  * $\blacktriangleright$

We propose a new trinitarian view of compiler correctness that accounts for
non-trivial trace relations. While, as discussed above, specific instances of
the $\mathsf{CC^{\sim}}$ definition have already been used in practice, we
seem to be the first to propose assessing the meaningfulness of
$\mathsf{CC^{\sim}}$ instances in terms of how properties are preserved
between the source and the target, and in particular by looking at the
property mappings $\tilde{\sigma}$ and $\tilde{\tau}$ induced by the trace
relation $\sim$. We prove that $\mathsf{CC^{\sim}}$,
$\mathsf{TP^{\tilde{\sigma}}}$, and $\mathsf{TP^{\tilde{\tau}}}$ are
equivalent for any trace relation (§ 2.2), as illustrated in Figure 1. In the
opposite direction, we show that for every trace relation corresponding to a
given Galois connection [20], an analogous equivalence holds. Finally, we
extend these results (§ 2.3) from the preservation of trace properties to the
larger class of subset-closed hyperproperties (e.g., noninterference).

  * $\blacktriangleright$

We use $\mathsf{CC^{\sim}}$ compilers of various complexities to illustrate
that our view on compiler correctness naturally accounts for undefined
behavior (§ 3.1), resource exhaustion (§ 3.2), different source and target
values (§ 3.3), and differences in the granularity of data and observable
events (§ 3.4). We expect these ideas to apply to any other discrepancies
between source and target traces. For each compiler we show how to choose the
relation between source and target traces and how the induced property
mappings preserve interesting trace properties and subset-closed
hyperproperties. We look at the way particular $\tilde{\sigma}$ and
$\tilde{\tau}$ work on different kinds of properties and how the produced
properties can be expressed for different kinds of traces.

  * $\blacktriangleright$

We analyze the impact of correct compilation on noninterference [22], showing
what can still be preserved (and thus also what is lost) when target
observations are finer than source ones, e.g., side-channel observations (§
4). We formalize the guarantee obtained by correct compilation of a
noninterfering program as abstract noninterference [21], a weakening of target
noninterference. Dually, we identify a family of declassifications of target
noninterference for which source reasoning is possible.

  * $\blacktriangleright$

Finally, we show that the trinitarian view also extends to a large class of
secure compilation definitions [2], formally characterizing the protection of
the compiled program against linked adversarial code (§ 5). For each secure
compilation definition we again propose both a property-free characterization
in the style of $\mathsf{CC^{\sim}}$, and two characterizations in terms of
preserving a class of source or target properties satisfied against arbitrary
adversarial contexts. The additional quantification over contexts allows for
finer distinctions when considering different property classes, so we study
mapping classes not only of trace properties and hyperproperties, but also of
relational hyperproperties [2]. An example secure compiler accounting for a
target that can produce additional trace events that are not possible in the
source illustrates this approach.

The paper closes with discussions of related (§ 6) and future work (§ 7). The
appendix contains omitted technical details.

The traces considered in our examples are structured, usually as sequences of
events. We notice however that unless explicitly mentioned, all our
definitions and results are more general and make no assumption whatsoever
about the structure of traces. Most of the theorems formally or informally
mentioned in the paper were mechanized in the Coq proof assistant and are
marked with  . This development has around 10k lines of code, is described in
the online appendix, and is available at the following address:
https://github.com/secure-compilation/different_traces.

##  2 Trace-Relating Compiler Correctness

In this section, we start by generalizing the trace property preservation
definitions at the end of the introduction to $\mathsf{TP^{\sigma}}$ and
$\mathsf{TP^{\tau}}$, which depend on two arbitrary mappings $\sigma$ and
$\tau$ (§ 2.1). We prove that, whenever $\sigma$ and $\tau$ form a Galois
connection, $\mathsf{TP^{\sigma}}$ and $\mathsf{TP^{\tau}}$ are equivalent
(Theorem 2.1). We then exploit a bijective correspondence between trace
relations and Galois connections to close the trinitarian view (§ 2.2), with
two main benefits: first, it helps us assess the meaningfulness of a given
trace relation by looking at the property mappings it induces; second, it
allows us to construct new compiler correctness definitions starting from a
desired mapping of properties. Finally, we generalize the classic result that
compiler correctness (i.e., $\mathsf{CC^{=}}$) is enough to preserve not just
trace properties but also all subset-closed hyperproperties [14]. For this, we
show that $\mathsf{CC^{\sim}}$ is also equivalent to subset-closed
hyperproperty preservation, for which we also define both a version in terms
of $\tilde{\sigma}$ and a version in terms of $\tilde{\tau}$ (§ 2.3).

###  2.1 Property Mappings

As explained in § 1, trace-relating compiler correctness $\mathsf{CC^{\sim}}$,
by itself, lacks a crisp description of which trace properties are preserved
by compilation. Since even the syntax of traces can differ between source and
target, one can either look at trace properties of the source (but then one
needs to interpret them in the target), or at trace properties of the target
(but then one needs to interpret them in the source). Formally we need two
property mappings,
$\tau:2^{\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>2^{\mathbf{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color<EMAIL_ADDRESS>and
$~{}\sigma:2^{\mathbf{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color<EMAIL_ADDRESS>2^{\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>which lead us to the following generalization of trace property preservation
($\mathsf{TP}$).

######  Definition 3 ($\mathsf{TP^{\sigma}}$ and $\mathsf{TP^{\tau}}$)

Given two property mappings,
$\tau:2^{\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>2^{\mathbf{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color<EMAIL_ADDRESS>and
$\sigma:2^{\mathbf{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color<EMAIL_ADDRESS>2^{\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>for a compilation chain
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\left.\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>we define:

$\mathsf{TP^{\tau}}\equiv\forall\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{\pi_{S}}}}.~{}\forall\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{W}}}.~{}\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{W}}}~{}\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{\models}}}~{}\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{\pi_{S}}}}\Rightarrow{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\left.\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{W}}}\right\downarrow}}~{}\bm{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}{\models}}}~{}\tau(\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{\pi_{S}}}});\;\;\;\mathsf{TP^{\sigma}}\equiv\forall\bm{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}{\pi_{\mathrm{T}}}}}.~{}\forall\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{W}}}.~{}\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{W}}}~{}\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{\models}}}~{}\sigma(\bm{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}{\pi_{\mathrm{T}}}}})\Rightarrow{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\left.\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{W}}}\right\downarrow}}~{}\bm{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}{\models}}}~{}\bm{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color<EMAIL_ADDRESS>
For an arbitrary source program
$\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>$\tau$ interprets a source property
$\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>as the _target guarantee_ for
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\left.\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>Dually, $\sigma$ defines a _source obligation_ sufficient for the satisfaction
of a target property
$\bm{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color<EMAIL_ADDRESS>after compilation. Ideally:

  * •

Given
$\bm{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color<EMAIL_ADDRESS>the target interpretation of the source obligation
$\sigma(\bm{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}{\pi_{\mathrm{T}}}}})$
should actually guarantee that
$\bm{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color<EMAIL_ADDRESS>holds, i.e.,
$\tau(\sigma(\bm{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}{\pi_{\mathrm{T}}}}}))\subseteq\bm{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color<EMAIL_ADDRESS>
  * •

Dually for
$\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>we would not want the source obligation for
$\tau(\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{\pi_{S}}}})$
to be harder than
$\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>itself, i.e.,
$\sigma(\tau(\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{\pi_{S}}}}))\supseteq\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>
These requirements are satisfied when the two maps form a Galois connection
between the posets of source and target properties ordered by inclusion. We
briefly recall the definition and the characteristic property of Galois
connections [16, 39].

######  Definition 4 (Galois connection)

Let $(X,\preceq)$ and $(Y,\sqsubseteq)$ be two posets. A pair of maps,
$\alpha:X\to Y$, $\gamma:Y\to X$ is a Galois connection $\mathit{iff}$ it
satisfies the _adjunction law_ : $\forall x\in X.~{}\forall y\in
Y.~{}\alpha(x)\sqsubseteq y\iff x\preceq\gamma(y)$. $\alpha$ (resp. $\gamma$)
is the lower (upper) adjoint or abstraction (concretization) function and $Y$
($X$) the abstract (concrete) domain.

We will often write $\alpha:(X,\preceq)\leftrightarrows(Y,\sqsubseteq):\gamma$
to denote a Galois connection, or simply $\alpha:X\leftrightarrows Y:\gamma$,
or even $\alpha\leftrightarrows\gamma$ when the involved posets are clear from
context.

######  Lemma 1 (Characteristic property of Galois connections)

If $\alpha{:}(X,\preceq)\leftrightarrows{(Y,\sqsubseteq){:}\gamma}$ is a
Galois connection, then $\alpha,\gamma$ are monotone and they satisfy these
properties:

$\displaystyle i)$ $\displaystyle\quad\forall x\in
X.~{}x\preceq\gamma(\alpha(x));$ $\displaystyle ii)$
$\displaystyle\quad\forall y\in Y.~{}\alpha(\gamma(y))\sqsubseteq y.$

If $X,Y$ are complete lattices, then $\alpha$ is continuous, i.e., $\forall
F\subseteq X.~{}\alpha(\bigsqcup F)=\bigsqcup\alpha(F)$.

If two property mappings, $\tau$ and $\sigma$, form a Galois connection on
trace properties ordered by set inclusion, 1 (with $\alpha=\tau$ and
$\gamma=\sigma$) tells us that they satisfy the ideal conditions we discussed
above, i.e.,
$\tau(\sigma(\bm{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}{\pi_{\mathrm{T}}}}}))\subseteq\bm{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color<EMAIL_ADDRESS>and
$\sigma(\tau(\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{\pi_{S}}}}))\supseteq\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>target traces are often _“more concrete”_ than source ones, trace properties
$2^{\text{Trace}}$ (which in Coq we represent as the function type
$\text{Trace}{\to}\text{Prop}$) are contravariant in Trace and thus target
properties correspond to the _abstract domain_.

The two ideal conditions on $\tau$ and $\sigma$ are sufficient to show the
equivalence of the criteria they define, respectively $\mathsf{TP^{\tau}}$ and
$\mathsf{TP^{\sigma}}$.

######  Theorem 2.1 ($\mathsf{TP^{\tau}}$ and $\mathsf{TP^{\sigma}}$ coincide
)

Let
$\tau:2^{\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>2^{\mathbf{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}{{Trace}_{T}}}}}:\sigma$
be a Galois connection, with $\tau$ and $\sigma$ the lower and upper adjoints
(resp.). Then $\mathsf{TP^{\tau}}\iff\mathsf{TP^{\sigma}}$.

###  2.2 Trace Relations and Property Mappings

We now investigate the relation between $\mathsf{CC^{\sim}}$,
$\mathsf{TP^{\tau}}$ and $\mathsf{TP^{\sigma}}$. We show that for a trace
relation and its corresponding Galois connection (2), the three criteria are
equivalent (Theorem 2.3). This equivalence offers interesting insights for
both verification and design of a correct compiler. For a $\mathsf{CC^{\sim}}$
compiler, the equivalence makes explicit both the guarantees one has after
compilation ($\tilde{\tau}$) and source proof obligations to ensure the
satisfaction of a given target property ($\tilde{\sigma}$). On the other hand,
a compiler designer might first determine the target guarantees the compiler
itself must provide, i.e., $\tau$, and then prove an equivalent statement,
$\mathsf{CC^{\sim}}$, for which more convenient proof techniques exist in the
literature [7, 64].

######  Definition 5 (Existential and Universal Image [20])

Given any two sets $X$ and $Y$ and a relation ${\sim}\subseteq A\times B$,
define its existential or direct image, $\tilde{\tau}:2^{X}\to 2^{Y}$ and its
universal image, $\tilde{\sigma}:2^{Y}\to 2^{X}$ as follows:

$\tilde{\tau}=\lambda~{}\pi\in
2^{X}.~{}\left\\{y\,\mathrel{}\middle|\mathrel{}\,\exists x\ldotp x\sim
y\wedge x\in\pi\right\\};\tilde{\sigma}=\lambda~{}\pi\in
2^{Y}.~{}\left\\{x\,\mathrel{}\middle|\mathrel{}\,\forall y\ldotp x\sim
y\Rightarrow y\in\pi\right\\}.$

When trace relations are considered, the existential and universal images can
be used to instantiate 3 leading to the trinitarian view already mentioned in
§ 1.

######  Theorem 2.2 (Trinitarian View  )

For any trace relation $\sim$ and its existential and universal images
$\tilde{\tau}$ and $\tilde{\sigma}$, we have:
$\mathsf{TP^{\tilde{\tau}}}\iff\mathsf{CC^{\sim}}\iff\mathsf{TP^{\tilde{\sigma}}}$.

This result relies both on Theorem 2.1 and on the fact that the existential
and universal images of a trace relation form a Galois connection ( ). Below
we further generalize this result (Theorem 2.3) relying on a bijective
correspondence between trace relations and Galois connections on properties.

######  Lemma 2 (Trace relations $\cong$ Galois connections on trace
properties)

The function $\sim\;\mapsto\tilde{\tau}\leftrightarrows\tilde{\sigma}$ that
maps a trace relation to its existential and universal images is a bijection
between trace relations
$2^{\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{Trace_{S}}}}\times\mathbf{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color<EMAIL_ADDRESS>and Galois connections on trace properties
$2^{\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>2^{\mathbf{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color<EMAIL_ADDRESS>Its inverse is $\tau\leftrightarrows\sigma\mapsto\hat{\sim}$, where
$\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{s}}}\,\hat{\sim}\,\mathbf{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}{t}}}\equiv\mathbf{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}{t}}}\in\tau(\\{\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{s}}}\\})$.

###### Proof

Gardiner et al. [20] show that the existential image is a functor from the
category of sets and relations to the category of predicate transformers,
mapping a set $X\mapsto 2^{X}$ and a relation $\sim\;\subseteq X\times
Y\mapsto\tilde{\tau}:2^{X}\to 2^{Y}$. They also show that such a functor is an
isomorphism – hence bijective – when one considers only monotonic predicate
transformers that have a – unique – upper adjoint. The universal image of
$\sim$, $\tilde{\sigma}$, is the unique adjoint of $\tilde{\tau}$ ( ), hence
$\sim\;\mapsto\tilde{\tau}\leftrightarrows\tilde{\sigma}$ is itself bijective.
∎

The bijection just introduced allows us to generalize Theorem 2.2 and switch
between the three views of compiler correctness described earlier at will.

######  Theorem 2.3 (Correspondence of Criteria)

For any trace relation $\sim$ and corresponding Galois connection
$\tau\leftrightarrows\sigma$, we have:
$\mathsf{TP^{\tau}}\iff\mathsf{CC^{\sim}}\iff\mathsf{TP^{\sigma}}$.

###### Proof

For a trace relation $\sim$ and the Galois connection
$\tilde{\tau}\leftrightarrows\tilde{\sigma}$, the result follows from Theorem
2.2. For a Galois connection $\tau\leftrightarrows\sigma$ and $\hat{\sim}$,
use 2 to conclude that the existential and universal images of $\hat{\sim}$
coincide with $\tau$ and $\sigma$, respectively; the goal then follows from
Theorem 2.2. ∎

We conclude by explicitly noting that sometimes the lifted properties may be
trivial: the target guarantee can be the true property (the set of all
traces), or the source obligation the false property (the empty set of
traces). This might be the case when source observations abstract away too
much information (§ 3.2 presents an example).

###  2.3 Preservation of Subset-Closed Hyperproperties

A $\mathsf{CC^{=}}$ compiler ensures the preservation not only of trace
properties, but also of all subset-closed hyperproperties, which are known to
be preserved by refinement [14]. An example of a subset-closed hyperproperty
is noninterference [14]; a $\mathsf{CC^{=}}$ compiler thus guarantees that if
$\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>is noninterfering with respect to the inputs and outputs in the trace then so
is
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\left.\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>To be able to talk about how (hyper)properties such as noninterference are
preserved, in this section we propose another trinitarian view involving
$\mathsf{CC^{\sim}}$ and preservation of subset-closed hyperproperties
(Theorem 2.4), slightly weakened in that source and target property mappings
will need to be closed under subsets.

First, recall that a program satisfies a hyperproperty when its complete set
of traces, which from now on we will call its behavior, is a member of the
hyperproperty [14].

######  Definition 6 (Hyperproperty Satisfaction)

A program $W$ satisfies a hyperproperty $H$, written $W\models H$, iff
$\mathit{beh}(W)\in H$, where
$\mathit{beh}(W)=\left\\{t\,\mathrel{}\middle|\mathrel{}\,W{\rightsquigarrow}t\right\\}$.

Hyperproperty preservation is a strong requirement in general. Fortunately,
many interesting hyperproperties are subset-closed ($\mathit{SCH}$ for short),
which simplifies their preservation since it suffices to show that the
behaviors of the compiled program refine the behaviors of the source one,
which coincides with the statement of $\mathsf{CC^{=}}$.

To talk about hyperproperty preservation in the trace-relating setting, we
need an interpretation of source hyperproperties into the target and vice
versa. The one we consider builds on top of the two trace property mappings
$\tau$ and $\sigma$, which are naturally lifted to hyperproperty mappings.
This way we are able to extract two hyperproperty mappings from a trace
relation similarly to § 2.2:

######  Definition 7 (Lifting property mappings to hyperproperty mappings)

Let
$\tau:2^{\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>2^{\mathbf{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color<EMAIL_ADDRESS>and
$\sigma:2^{\mathbf{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color<EMAIL_ADDRESS>2^{\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>be arbitrary property mappings. The images of
$\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>2^{2^{\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{{Trace}_{S}}}}}},\mathbf{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color<EMAIL_ADDRESS>2^{2^{\mathbf{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color<EMAIL_ADDRESS>under $\tau$ and $\sigma$ are, respectively:

$\displaystyle\tau(\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{H_{S}}}})$
$\displaystyle=\left\\{\tau(\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{\pi_{S}}}})\,\mathrel{}\middle|\mathrel{}\,\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{\pi_{S}}}}\in\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{H_{S}}}}\right\\};$
$\displaystyle\sigma(\mathbf{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}{H_{T}}}})$
$\displaystyle=\left\\{\sigma(\bm{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}{\pi_{\mathrm{T}}}}})\,\mathrel{}\middle|\mathrel{}\,\bm{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}{\pi_{\mathrm{T}}}}}\in\mathbf{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color<EMAIL_ADDRESS>
Formally we are defining two new mappings, this time on hyperproperties, but
by a small abuse of notation we still denote them by $\tau$ and $\sigma$.

Interestingly, it is not possible to apply the argument used for
$\mathsf{CC^{=}}$ to show that a $\mathsf{CC^{\sim}}$ compiler guarantees
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\left.\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{W}}}\right\downarrow}}~{}\bm{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}{\models}}}~{}\tilde{\tau}(\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{H_{S}}}})$
whenever
$\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{W}}}~{}\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{\models}}}~{}\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>This is in fact not true because direct images do not necessarily preserve
subset-closure [37, 45]. To fix this we close the image of $\tilde{\tau}$ and
$\tilde{\sigma}$ under subsets (denoted as $\mathit{Cl_{\subseteq}}$) and
obtain:

######  Theorem 2.4 (Preservation of Subset-Closed Hyperproperties  )

For any trace relation $\sim$ and its existential and universal images lifted
to hyperproperties, $\tilde{\tau}$ and $\tilde{\sigma}$, and for
$\mathit{Cl}_{\subseteq}(H)=\\{\pi\mid\exists\pi^{\prime}\in
H.~{}\pi\subseteq\pi^{\prime}\\}$, we have:

$\mathsf{SCHP^{\mathit{Cl}_{\subseteq}\circ\tilde{\tau}}}\iff\mathsf{CC^{\sim}}\iff\mathsf{SCHP^{\mathit{Cl}_{\subseteq}\circ\tilde{\sigma}}},\text{
where}$
$\displaystyle\mathsf{SCHP^{\mathit{Cl}_{\subseteq}\circ\tilde{\tau}}}$
$\displaystyle\equiv\forall\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{W}}}\forall\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{H_{S}}}}\in\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{SCH_{S}}}}.\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{W}}}~{}\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{\models}}}~{}\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{H_{S}}}}\Rightarrow{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\left.\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{W}}}\right\downarrow}}~{}\bm{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}{\models}}}~{}\mathit{Cl}_{\subseteq}(\tilde{\tau}(\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{H_{S}}}}));$
$\displaystyle\mathsf{SCHP^{\mathit{Cl}_{\subseteq}\circ\tilde{\sigma}}}$
$\displaystyle\equiv\forall\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{W}}}\forall\mathbf{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}{H_{T}}}}\in\mathbf{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}{SCH_{T}}}}.\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{W}}}~{}\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{\models}}}~{}\mathit{Cl}_{\subseteq}(\tilde{\sigma}(\mathbf{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}{H_{T}}}}))\Rightarrow{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\left.\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{W}}}\right\downarrow}}~{}\bm{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}{\models}}}~{}\mathbf{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color<EMAIL_ADDRESS>
Theorem 2.4 makes us aware of the potential loss of precision when interested
in preserving subset-closed hyperproperties through compilation. In § 4 we
focus on a security relevant subset-closed hyperproperty, noninterference, and
show that such a loss of precision can be intended as a declassification of
noninterference.

##  3 Instances of Trace-Relating Compiler Correctness

The trace-relating view of compiler correctness above can serve as a unifying
framework for studying a range of interesting compilers. This section provides
several representative instantiations of the framework: source languages with
undefined behavior that compilation can turn into arbitrary target behavior (§
3.1), target languages with resource exhaustion that cannot happen in the
source (§ 3.2), changes in the representation of values (§ 3.3), and
differences in the granularity of data and observable events (§ 3.4).

###  3.1 Undefined Behavior

We start by expanding upon the discussion of undefined behavior in § 1. We
first study the model of CompCert, where source and target alphabets are the
same, including the event for undefined behavior. The trace relation weakens
equality by allowing undefined behavior to be replaced with an arbitrary
sequence of events.

######  Example 1 (CompCert-like Undefined Behavior Relation)

Source and target traces are sequences of events drawn from $\Sigma$, where
$\mathit{Goes\\_wrong}\in\Sigma$ is a terminal event that represents an
undefined behavior. We then use the trace relation from the introduction:

$\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{s}}}\sim\mathbf{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}{t}}}\quad\equiv\quad\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{s}}}=\mathbf{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color<EMAIL_ADDRESS>m\leq\mathbf{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}{t}}}.~{}\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>
Each trace of a target program produced by a $\mathsf{CC^{\sim}}$ compiler is
either also a trace of the original source program or it has a finite prefix
that the source program also produces, immediately before encountering
undefined behavior. As explained in § 1, one of the correctness theorems in
CompCert can be rephrased as this variant of $\mathsf{CC^{\sim}}$.

We proved that the property mappings induced by the relation can be written as
( ):

$\displaystyle\tilde{\sigma}(\bm{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}{\pi_{\mathrm{T}}}}})=$
$\displaystyle\
\left\\{\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{s}}}\,\mathrel{}\middle|\mathrel{}\,\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{s}}}{\in}\bm{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}{\pi_{\mathrm{T}}}}}\wedge\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>m{\cdot}\mathit{Goes\\_wrong}\right\\}\cup\left\\{{m}{\cdot}\mathit{Goes\\_wrong}\,\mathrel{}\middle|\mathrel{}\,\forall\mathbf{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}{t}}}.~{}m{\leq}\mathbf{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}{t}}}{\implies}\mathbf{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}{t}}}{\in}\bm{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}{\pi_{\mathrm{T}}}}}\right\\};$
$\displaystyle\tilde{\tau}(\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{\pi_{S}}}})=$
$\displaystyle\
\left\\{\mathbf{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}{t}}}\,\mathrel{}\middle|\mathrel{}\,\mathbf{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}{t}}}{\in}\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{\pi_{S}}}}\right\\}\cup\left\\{\mathbf{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}{t}}}\,\mathrel{}\middle|\mathrel{}\,\exists
m\leq\mathbf{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}{t}}}.~{}{m}{\cdot}\mathit{Goes\\_wrong}\in\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>
These two mappings explain what a $\mathsf{CC^{\sim}}$ compiler ensures for
the $\sim$ relation above. The target-to-source mapping $\tilde{\sigma}$
states that to prove that a compiled program has a property
$\bm{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color<EMAIL_ADDRESS>using source-level reasoning, one has to prove that any trace produced by the
source program must either be a target trace satisfying
$\bm{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color<EMAIL_ADDRESS>or have undefined behavior, but only provided that any continuation of the
trace substituted for the undefined behavior satisfies
$\bm{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color<EMAIL_ADDRESS>The source-to-target mapping $\tilde{\tau}$ states that by compiling a program
satisfying a property
$\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>we obtain a program that produces traces that satisfy the same property or
that extend a source trace that ends in undefined behavior.

These definitions can help us reason about programs. For instance,
$\tilde{\sigma}$ specifies that, to prove that an event does not happen in the
target, it is not enough to prove that it does not happen in the source: it is
also necessary to prove that the source program is does not have any undefined
behavior (second disjunct). Indeed, if it had an undefined behavior, its
continuations could exhibit the unwanted event.  $\boxdot$

This relation can be easily generalized to other settings. For instance,
consider the setting in which we compile down to a low-level language like
machine code. Target traces can now contain new events that cannot occur in
the source: indeed, in modern architectures like x86 a compiler typically uses
only a fraction of the available instruction set. Some instructions might even
perform dangerous operations, such as writing to the hard drive. Formally, the
source and target do not have the same events any more. Thus, we consider a
source alphabet
$\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{\Sigma_{S}}}}=\Sigma\cup\\{\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>and a target alphabet
$\mathbf{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color<EMAIL_ADDRESS>The trace relation is defined in the same way and we obtain the same property
mappings as above, except that since target traces now have more events (some
of which may be dangerous), and the arbitrary continuations of target traces
get more interesting. For instance, consider a new event that represents
writing data on the hard drive, and suppose we want to prove that this event
cannot happen for a compiled program. Then, proving this property requires
exactly proving that the source program exhibits no undefined behavior [11].
More generally, what one can prove about target-only events can only be either
that they cannot appear (because there is no undefined behavior) or that any
of them can appear (in the case of undefined behavior).

In § 5.2 we study a similar example, showing that even in a safe language
linked adversarial contexts can cause dangerous target events that have no
source correspondent.

###  3.2 Resource Exhaustion

Let us return to the discussion about resource exhaustion in § 1.

######  Example 2 (Resource Exhaustion)

We consider traces made of events drawn from
$\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>in the source, and
$\mathbf{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}{\Sigma_{T}}}}=\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{\Sigma_{S}}}}\cup\\{\mathbf{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color<EMAIL_ADDRESS>in the target. Recall the trace relation for resource exhaustion:

$\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{s}}}\sim\mathbf{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}{t}}}\quad\equiv\quad\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{s}}}=\mathbf{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}{t}}}\vee\exists{m}\leq\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{s}}}.~{}\mathbf{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}{t}}}={m}\cdot\mathbf{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color<EMAIL_ADDRESS>
Formally, this relation is similar to the one for undefined behavior, except
this time it is the target trace that is allowed to end early instead of the
source trace.

The induced trace property mappings $\tilde{\sigma}$ and $\tilde{\tau}$ are
the following ( ):

$\displaystyle\tilde{\sigma}(\bm{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}{\pi_{T}}}})$
$\displaystyle=\\{\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{s}}}\mid\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{s}}}\in\bm{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}{\pi_{T}}}}\\}\cap\\{\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{s}}}\mid\forall{m}\leq\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{s}}}.~{}{m}\cdot\mathbf{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}{Resource\\_Limit\\_Hit}}}\in\bm{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}{\pi_{T}}}}\\};$
$\displaystyle\tilde{\tau}(\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{\pi_{S}}}})$
$\displaystyle=\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{\pi_{S}}}}\cup\\{{m}\cdot\mathbf{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}{Resource\\_Limit\\_Hit}}}\mid\exists\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{s}}}\in\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{\pi_{S}}}}.~{}{m}\leq\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>
These capture the following intuitions. The target-to-source mapping
$\tilde{\sigma}$ states that to prove a property of the compiled program one
has to show that the traces of the source program satisfy two conditions: (1)
they must also satisfy the target property; and (2) the termination of every
one of their prefixes by a resource exhaustion error must be allowed by the
target property. This is rather restrictive: any property that prevents
resource exhaustion cannot be proved using source-level reasoning. Indeed, if
$\bm{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color<EMAIL_ADDRESS>does not allow resource exhaustion, then
$\tilde{\sigma}(\bm{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}{\pi_{\mathrm{T}}}}})=\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>This is to be expected since resource exhaustion is simply not accounted for
at the source level. The other mapping $\tilde{\tau}$ states that a compiled
program produces traces that either belong to the same properties as the
traces of the source program or end early due to resource exhaustion.

In this example, safety properties [32] are mapped (in both directions) to
other safety properties ( ). This can be desirable for a relation: since
safety properties are usually easier to reason about, one interested only in
safety properties at the target can reason about them using source-level
reasoning tools for safety properties. § 0.B.1 provides a detailed account of
safety properties and how one can restrict the notion of compiler correctness
if one is only interested in them.

The compiler correctness theorem in CakeML is an instance of
$\mathsf{CC^{\sim}}$ for the $\sim$ relation above. We have also implemented
two small compilers that are correct for this relation. The full details can
be found in the Coq development in the supplementary materials. The first
compiler ( ) goes from a simple expression language (similar to the one in §
3.3 but without inputs) to the same language except that execution is bounded
by some amount of fuel: each execution step consumes some amount of fuel and
execution immediately halts when it runs out of fuel. The compiler is the
identity.

The second compiler ( ) is more interesting: we proved this
$\mathsf{CC^{\sim}}$ instance for a variant of a compiler from a while
language to a simple stack machine by Xavier Leroy [36]. We enriched the two
languages with outputs and modified the semantics of the stack machine so that
it falls into an error state if the stack reaches a certain size. The proof
uses a standard forward simulation modified to account for failure.  $\boxdot$

We conclude this subsection by noting that the resource exhaustion relation
and the undefined behavior relation from the previous subsection can easily be
combined. Indeed, given a relation $\sim_{\text{UB}}$ and a relation
$\sim_{\text{RE}}$ defined as above on the same sets of traces, we can build a
new relation $\sim$ that allows both refinement of undefined behavior and
resource exhaustion by taking their union:
$\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{s}}}\sim\mathbf{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}{t}}}\equiv\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{s}}}\sim_{\text{UB}}\mathbf{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}{t}}}\vee\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{s}}}\sim_{\text{RE}}\mathbf{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color<EMAIL_ADDRESS>A compiler that is $\mathsf{CC^{\sim_{\text{UB}}}}$ or
$\mathsf{CC^{\sim_{\text{RE}}}}$ is trivially $\mathsf{CC^{\sim}}$, though the
converse is not true.

###  3.3 Different Source and Target Values

We now illustrate trace-relating compilation for a translation mapping source-
level booleans to target-level natural numbers. Given the simplicity of this
compiler, most of the details of the formalization are deferred to the online
appendix.

The source language is a pure, statically typed expression language whose
expressions
$\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>include naturals
$\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>booleans
$\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>conditionals, arithmetic and relational operations, boolean inputs
$\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>and natural inputs
$\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>A trace
$\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>is a list of inputs
$\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>paired with a result
$\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>which can be a natural, a boolean, or an error. Well-typed programs never
produce error ( ). Types
$\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>are either
$\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>(naturals) or
$\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>(booleans); typing is standard. The source language has a standard big-step
operational semantics
($\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>is,r\right\rangle}}}$) which tells how an expression
$\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>generates a trace
$\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>is,r\right\rangle}}}$. The target language is analogous, except that it is
untyped, only has naturals
$\mathbf{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color<EMAIL_ADDRESS>and its only inputs are naturals
$\mathbf{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color<EMAIL_ADDRESS>The semantics of the target language is also given in big-step style. Since we
only have naturals and all expressions operate on them, no error result is
possible in the target.

The compiler is homomorphic, translating a source expression to the same
target expression; the only differences are natural numbers (and
conditionals), as noted below.

$\displaystyle{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\left.\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>$\displaystyle\
\mathbf{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color<EMAIL_ADDRESS>$\displaystyle{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\left.\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>$\displaystyle\
\mathbf{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color<EMAIL_ADDRESS>$\displaystyle{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\left.\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>e_{2}}}}\right\downarrow}}=$ $\displaystyle\
\mathbf{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}{{if}~{}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\left.\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{e_{1}}}}\right\downarrow}}~{}\bm{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}{\leq}}}~{}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\left.\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>$\displaystyle{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\left.\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>$\displaystyle\
\mathbf{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color<EMAIL_ADDRESS>$\displaystyle{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\left.\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>$\displaystyle\
\mathbf{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color<EMAIL_ADDRESS>$\displaystyle{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\left.\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>$\displaystyle\
\mathbf{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}{{if}~{}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\left.\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{e_{1}}}}\right\downarrow}}~{}\bm{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}{\leq}}}~{}0~{}{then}~{}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\left.\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{e_{3}}}}\right\downarrow}}~{}{else}~{}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\left.\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>
When compiling an _if-then-else_ the target condition
$\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\left.\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>$\bm{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color<EMAIL_ADDRESS>$\mathbf{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color<EMAIL_ADDRESS>is used to check that
$\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>is false, and therefore the _then_ and _else_ branches of the source are
swapped in the target.

Relating Traces. We relate basic values (naturals and booleans) in a non-
injective fashion as noted below. Then, we extend the relation to lists of
inputs pointwise (Sections 3.3 and 3.3) and lift that relation to traces
(Sections 3.3 and 3.3).

$\displaystyle\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>$\displaystyle\
\mathbf{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color<EMAIL_ADDRESS>$\displaystyle\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>$\displaystyle\
\mathbf{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color<EMAIL_ADDRESS>$\mathbf{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color<EMAIL_ADDRESS>$\displaystyle\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>$\displaystyle\
\mathbf{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color<EMAIL_ADDRESS>
$\begin{array}[]{c}\textsf{\scriptsize({Empty})}\\\
\inference{}{\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{\varnothing}}}\sim\mathbf{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color<EMAIL_ADDRESS>$\begin{array}[]{c}\textsf{\scriptsize({Cons})}\\\
\inference{\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{i}}}\sim\mathbf{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}{i}}}&\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{is}}}\sim\mathbf{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}{is}}}}{\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>is}}}\sim\mathbf{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color<EMAIL_ADDRESS>is}}}}\end{array}$ $\begin{array}[]{c}\textsf{\scriptsize({Nat})}\\\
\inference{\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{is}}}\sim\mathbf{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}{is}}}&\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{n}}}\sim\mathbf{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}{n}}}}{\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>is,n\right\rangle}}}\sim\mathbf{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color<EMAIL_ADDRESS>is,n\right\rangle}}}}\end{array}$
$\begin{array}[]{c}\textsf{\scriptsize({Bool})}\\\
\inference{\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{is}}}\sim\mathbf{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}{is}}}&\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{b}}}\sim\mathbf{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}{n}}}}{\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>is,b\right\rangle}}}\sim\mathbf{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color<EMAIL_ADDRESS>is,n\right\rangle}}}}\end{array}$

Property mappings. The property mappings $\tilde{\sigma}$ and $\tilde{\tau}$
induced by the trace relation $\sim$ defined above capture the intuition
behind encoding booleans as naturals:

  * •

the source-to-target mapping allows
$\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>to be encoded by any non-zero number;

  * •

the target-to-source mapping requires that
$\mathbf{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color<EMAIL_ADDRESS>be replaceable by _both_
$\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>and
$\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>
Compiler correctness. With the relation above, the compiler is proven to
satisfy $\mathsf{CC^{\sim}}$.

######  Theorem 3.1
(${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\left.\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>is correct  )

${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\left.\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>is $\mathsf{CC^{\sim}}$.

Simulations with different traces. The difficulty in proving Theorem 3.1
arises from the trace-relating compilation setting: For compilation chains
that have the same source and target traces, it is customary to prove compiler
correctness using a forward simulation (i.e., a simulation between source and
target transition system); then, using determinacy [18, 40] of the target
language and input totality [69, 19] (aka receptiveness) of the source, this
forward simulation is flipped into a backward simulation (a simulation between
target and source transition system), as described by Beringer et al. [7],
Leroy [35]. This flipping is useful because forward simulations are often much
easier to prove (by induction on the transitions of the source) than backward
ones, as it is the case here.

We first give the main idea of the flipping proof, when the inputs are the
same in the source and the target [7, 35]. We only consider inputs, as it is
the most interesting case, since with determinacy, nondeterminism only occurs
on inputs. Given a forward simulation $\mathcal{R}$, and a target program
$\mathbf{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color<EMAIL_ADDRESS>that simulates a source program
$\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>$\mathbf{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color<EMAIL_ADDRESS>is able to perform an input iff so is
$\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>otherwise, say for instance that
$\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>performs an output, by forward simulation
$\mathbf{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color<EMAIL_ADDRESS>would also perform an output, which is impossible because of determinacy. By
input totality of the source,
$\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>must be able to perform the exact same input as
$\mathbf{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color<EMAIL_ADDRESS>using forward simulation and determinacy, the resulting programs must be
related.

$\textstyle{\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{W_{S}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{i_{1}}}}}$$\textstyle{=\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{W_{S}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{i_{2}}}}}$$\textstyle{\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\mathcal{R}}$$\textstyle{\mathbf{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}{W_{T}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\mathbf{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color<EMAIL_ADDRESS>By input totality By contradiction, using forward simulation and determinacy
$\textstyle{\exists\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>By forward simulation and determinacy
$\textstyle{\cdot}$$\textstyle{\mathbf{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color<EMAIL_ADDRESS>
However, our trace relation is not injective (both
$\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>and
$\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>are mapped to
$\mathbf{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}{0}}}$),
therefore these arguments do not apply: not all possible inputs of target
programs are accounted for in the forward simulation. We thus have to
strengthen the forward simulation assumption, requiring the following
additional property to hold, for any source program
$\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>and target program
$\mathbf{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color<EMAIL_ADDRESS>related by the forward simulation $\mathcal{R}$.

$\textstyle{\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{W_{S}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{{i_{S}}_{1}}}}}$$\scriptstyle{\exists\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{{i_{S}}_{2}}}}}$$\textstyle{\ignorespaces\ignorespaces\ignorespaces\ignorespaces\mathcal{R}}$$\textstyle{\mathbf{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}{W_{T}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\mathbf{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}{{i_{T}}_{1}}}}}$$\scriptstyle{\mathbf{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}{{i_{T}}_{2}}}}}$$\textstyle{\exists\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{{W_{S}}_{2}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\mathcal{R}}$$\textstyle{\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{{W_{S}}_{1}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\ignorespaces\ignorespaces\ignorespaces\ignorespaces\mathcal{R}}$$\textstyle{\mathbf{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}{{W_{T}}_{1}}}}}$$\textstyle{\mathbf{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color<EMAIL_ADDRESS>
where
$\displaystyle\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{{i_{S}}_{1}}}}\sim\mathbf{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color<EMAIL_ADDRESS>$\displaystyle\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{{i_{S}}_{1}}}}\sim\mathbf{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color<EMAIL_ADDRESS>$\displaystyle\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{{i_{S}}_{2}}}}\sim\mathbf{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color<EMAIL_ADDRESS>
We say that a forward simulation for which this property holds is _flippable_.
For our example compiler, a flippable forward simulation works as follows:
whenever a boolean input occurs in the source, the target program must perform
every strictly positive input
$\mathbf{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color<EMAIL_ADDRESS>(and not just
$\mathbf{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color<EMAIL_ADDRESS>as suggested by the compiler). Using this property, determinacy of the target,
input totality of the source, as well as the fact that any target input has an
inverse image through the relation, we can indeed show that the forward
simulation can be turned into a backward one: starting from
$\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{W_{S}}}}\mathrel{\mathcal{R}}\mathbf{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color<EMAIL_ADDRESS>and an input
$\mathbf{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color<EMAIL_ADDRESS>we show that there is
$\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>and
$\mathbf{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color<EMAIL_ADDRESS>as in the diagram above, using the same arguments as when the inputs are the
same; because the simulation is flippable, we can close the diagram, and
obtain the existence of an adequate
$\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>From this we obtain $\mathsf{CC^{\sim}}$.

In fact, we have proven a completely general ‘flipping theorem’, with this
flippable hypothesis on the forward simulation ( ). We have also shown that if
the relation $\sim$ defines a bijection between the inputs of the source and
the target, then any forward simulation is flippable, hence reobtaining the
usual proof technique [7, 35] as a special case. This flipping theorem is
further discussed in the online appendix.

###  3.4 Abstraction Mismatches

We now consider how to relate traces where a single source action is compiled
to multiple target ones. To illustrate this, we take a pure, statically-typed
source language that can output (nested) pairs of arbitrary size, and a pure,
_untyped_ target language where sent values have a fixed size. Concretely, the
source is analogous to the language of § 3.3, except that it does not have
inputs or booleans and it has an expression
$\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>which can emit a (nested) pair
$\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>of values in a single action. That is, given that
$\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>reduces to a pair, e.g.,
$\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>v1,\left\langle v2,v3\right\rangle\right\rangle}}}$, expression
$\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{send~{}\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>v1,\left\langle v2,v3\right\rangle\right\rangle}}}}}}$ emits action
$\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>v1,\left\langle v2,v3\right\rangle\right\rangle}}}$. That expression is
compiled into a sequence of individual sends in the target language
$\mathbf{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color<EMAIL_ADDRESS>;
$\mathbf{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color<EMAIL_ADDRESS>;
$\mathbf{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color<EMAIL_ADDRESS>since in the target,
$\mathbf{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color<EMAIL_ADDRESS>sends the value that
$\mathbf{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color<EMAIL_ADDRESS>reduces to, but the language has no pairs.

Due to space constraints we omit the full formalization of these simple
languages and of the homomorphic compiler
(${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\left.\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{\left(\cdot\right)}}}\right\downarrow}}:\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{e}}}\to\mathbf{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}{e}}}$).
The only interesting bit is the compilation of the
$\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>expression, which relies on the
${{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\mathtt{gensend}\left(\cdot\right)}}}$
function below. That function takes a source expression of a given type and
returns a sequence of target
$\mathbf{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color<EMAIL_ADDRESS>instructions that send each element of the expression.

$\displaystyle{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\mathtt{gensend}\left(\vdash\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{e:\tau}}}\right)}}}=\begin{cases}\mathbf{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}{\mathbf{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}{send~{}{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\left.\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{\left(\vdash\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{{e}}}}:N\right)}}}\right\downarrow}}}}}}}}}&\text{
if
}\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{\tau}}}=\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>\mathbf{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}{{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\mathtt{gensend}\left(\vdash\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{e.1:\tau^{\prime}}}}\right)}}};{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\mathtt{gensend}\left(\vdash\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{e.2:\tau^{\prime\prime}}}}\right)}}}}}}&\text{
if
}\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{\tau}}}=\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>
Relating Traces. We start with the trivial relation between numbers:
$\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{n}}}\operatorname{\sim^{0}}\mathbf{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color<EMAIL_ADDRESS>i.e., numbers are related when they are the same. We cannot build a relation
between single actions since a single source action is related to multiple
target ones. Therefore, we define a relation between a source action
$\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>and a target trace
$\mathbf{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color<EMAIL_ADDRESS>(a list of numbers), inductively on the structure of
$\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>(which is a pair of values, and values are natural numbers or pairs).

$\begin{array}[]{c}\textsf{\scriptsize({Trace-Rel-N-N})}\\\
\inference{\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{n}}}\operatorname{\sim^{0}}\mathbf{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}{n}}}&\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{n^{\prime}}}}\operatorname{\sim^{0}}\mathbf{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}{n^{\prime}}}}}{\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>n,n^{\prime}\right\rangle}}}\operatorname{\sim}\mathbf{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color<EMAIL_ADDRESS>n^{\prime}}}}}\end{array}$ $\begin{array}[]{c}\textsf{\scriptsize({Trace-Rel-
N-M})}\\\
\inference{\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{n}}}\operatorname{\sim^{0}}\mathbf{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}{n}}}&\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color@cmyk@fill{1}{0.50}{0}{0}{M}}}\operatorname{\sim}\mathbf{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color@cmyk@fill{0}{0.77}{0.87}{0}{t}}}}{\mathsf{{\color[rgb]{0,0.5,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,1}\pgfsys@color@cmyk@stroke{1}{0.50}{0}{0}\pgfsys@color<EMAIL_ADDRESS>n,M\right\rangle}}}\operatorname{\sim}\mathbf{{\color[rgb]{1,0.23,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.23,0.13}\pgfsys@color@cmyk@stroke{0}{0.77}{0.87}{0}\pgfsys@color<EMAIL_ADDRESS>t}}}}\end{array}$ $\begin{array}[]{c}\textsf{\scriptsize({Trace-Rel-M-N})}\\\