Compiler correctness is an old idea [37,40,41] that has seen a significant revival in re-cent times. This new wave was started by the creation of the CompCert verified C com-piler [33] and continued by the proposal of many significant extensions and variants ofCompCert [8,9,12,23,29,30,42,52,56,57,61] and the success of many other mile-stone compiler verification projects, including Vellvm [64], Pilsner [45], CakeML [58],CertiCoq [4], etc. Yet, even for these verified compilers, the precise statement of cor-rectness matters. Since proof assistants are used to conduct the verification, an externalobserver does not have to understand the proofs in order to trust them, but one still hasto deeply understand the statement that was proved. And this is true not just for correctcompilation, but also for secure compilation, which is the more recent idea that ourcompilation chains should do more to also ensure security of our programs [3,26].Basic Compiler Correctness.The gold standard for compiler correctness issemanticpreservation, which intuitively says that the semantics of a compiled program (in thetarget language) is compatible with the semantics of the original program (in the source anguage). For practical verified compilers, such as CompCert [33] and CakeML [58],semantic preservation is stated extrinsically, by referring totraces. In these two settings,a trace is an ordered sequence of events—such as inputs from and outputs to an externalenvironment—that are produced by the execution of a program. This definition says that for any whole1source programW, if we compile it (denotedW?), execute it with respect to the semantics of the target language, and observe a tracet, then the originalWcan producethe sametracetwith respect to the semantics ofthe source language.2This definition is simple and easy to understand, since it onlyreferences a few familiar concepts: a compiler between a source and a target language,each equipped with a trace-producing semantics (usually nondeterministic).