Both equivalence preservation and equivalence reflection (what make a compiler fully abstract) relate to how the compiler treats program equivalences, which in this case I’m considering observational equivalence. Two programs p1 and p2 are observationally equivalent if you cannot make any external observations that can distinguish them.
For example, if the only externally observable behavior about programs in your language that you can make is see what output they print, this means that the two programs print the same output, even if they are implemented in completely different ways. Observational equivalence is extremely useful, especially for compilers, which when optimizing may change how a particular program is implemented but should not change the observable behavior. But it is also useful for programmers, who commonly refactor code, which means they change how the code is implemented (to make it easier to maintain, or extend, or better support some future addition), without changing any functionality. Refactoring is an equivalence-preserving transformation. We write observational equivalence on programs formally as:
p1 ≈ p1But we often also want to compile not just whole programs, but particular modules, or expressions, or in the general sense, components, and in that case, we want an analogous notion of equivalence. Two components are contextually equivalent if in all program contexts they produce the same observable behavior. In other words, if you have two modules, but any way you combine those modules with the rest of a program (so the rest is the same, but the modules differ), the result is the same, then those two modules are contextually equivalent. We will write this, overloading the ≈ for both observational and contextual equivalence, as:
e1 ≈ e1As an example, if we consider a simple functional language and consider our components to be individual expressions, it should be clear that these two expressions are contextually equivalent:
@@ -44,18 +45,21 @@Would not be contextually equivalent, because there exists a program context that can distinguish them. What is that context? Well, if we imagine plugging in the functions above into the “hole” written as [·] below, the result will be different for the two functions! This is because the toString() method on functions in Javascript returns the source code of the function.
([·]).toString()From the perspective of optimizations, this is troublesome, as you can’t be sure that a transformation between the above programs was safe (assuming one was much faster than the other), as there could be code that relied upon the particular way that the source code had been written. There are more complicated things you can do (like optimizing speculatively and falling back to unoptimized versions when reflection was needed). In general though, languages with that kind of reflection are both harder to write fast compilers for and harder to write secure compilers for, and while it’s not the topic of this post, it’s always important to know what you mean by contextual equivalence, which usually means: what can program contexts determine about components.
+With that in mind, what does equivalence reflection and equivalence preservation for a compiler mean? Let’s start with equivalence reflection, as that’s the property that all your correct compilers already have. Equivalence reflection means that if two components, when compiled, are equivalent, then the source components must have been equivalent. We can write this more formally as (where we write s ↠ t to mean a component s is compiled to t):
∀ s1 s2 t1 t2. s1 ↠ t1 ∧ t2 ↠ s2 ∧ t1 ≈ t2 ⇒ s1 ≈ s2What are the consequences of this definition? And why do correct compilers have this property? Well, the contrapositive is actually easier to understand: it says that if the source components weren’t equivalent then the target components would have to be different, or more formally:
∀ s1 s2 t1 t2. s1 ↠ t1 ∧ t2 ↠ s2 ∧ s1 ≉ s2 ⇒ t1 ≉ t2If this didn’t hold, then the compiler could take different source components and compile them to the same target component! Which means you could have different source programs you wrote, which have observationally different behavior, and your compiler would produce the same target program! Any correct compiler has to preserve observational behavior, and it couldn’t do that in this case, as the target program only has one behavior, so it can’t have both the behavior of s1 and s2 (for pedants, not considering non-deterministic targets).
So equivalence reflection should be thought of as related to compiler correctness. Note, however, that equivalence reflection is not the same as compiler correctness: as long as your compiler produced different target programs for different source programs, all would be fine – your compiler could hash the source program and produce target programs that just printed the hash to the screen, and it would be equivalence reflecting, since it would produce different target programs not only for source programs that were observationally different, but even syntactically different! That would be a pretty bad compiler, and certainly not correct, but it would be equivalence reflecting.
+Equivalence preservation, on the other hand, is the hallmark of fully abstract compilers, and it is a property that even most correct compilers do not have, though it would certainly be great if they did. It says that if two source components are equivalent, then the compiled versions must still be equivalent. Or, more formally:
∀ s1 s2 t1 t2. s1 ↠ t1 ∧ t2 ↠ s2 ∧ s1 ≈ s2 ⇒ t1 ≈ t2(See, I just reversed the implication. Need trick! But now it means something totally different). One place where this has been studied extensively is by security researchers, because what it tells you is that observers in the target can’t make observations that aren’t possible to distinguish in the source. Let’s make that a lot more concrete, where we will also see why it’s not frequently true, even of proven correct compilers.
Say your language has some information hiding feature, like a private field, and you have two source components that are identical except they have different values stored in the private field. If the compiler does not preserve the fact that it is private (because, for example, it translates the higher level object structure into a C struct or just a pile of memory accessed by assembly), then other target code could read the private values, and these two components will no longer be equivalent.
This also has implications for programmer refactoring and compiler optimizations: I (or my compiler) might think that it is safe to replace one version of the program with another, because I know that in my language these are equivalent, but what I don’t know is that the compiler reveals distinguishing characteristics, and perhaps some target-level library that I’m linking with relies upon how the old code worked. If that’s the case, I can have a working program, and make a change that does not change the meaning of the component in my language, but the whole program can no longer work.
Proving a compiler fully abstract, therefore, is all about proving equivalence preservation. So how do we do it?
+Looking at what we have to prove, we see that given contextually equivalent source components s1 and s2, we need to show that t1 and t2 are contextually equivalent. We can expand this to explicitly quantify over the contexts that combine with the components to make whole programs:
∀ s1 s2 t1 t2. s1 ↠ t1 ∧ t2 ↠ s2 ∧ (∀Cs. Cs[s1] ≈ Cs[s2]) ⇒ (∀Ct. Ct[t1] ≈ Ct[t2])Noting that as mentioned above, I am overloading ≈ to now mean whole-program observational equivalence (so, running the program produces the same observations).
Cs'[s1] ≈ Cs'[s2]
≈ ≈
Ct[t1] ? Ct[t2]Let’s make this concrete with an example. This will be presented somewhat in english and some in Coq.
Our source language is arithmetic expressions over integers with addition and subtraction:
e ::= n
@@ -75,7 +80,7 @@ How to prove a compiler fully abstract
| Num : Z -> Expr
| Plus : Expr -> Expr -> Expr
| Minus : Expr -> Expr -> Expr.Evaluation is standard (if you wanted to parse this, you would need to deal with left/right associativity, and probably add parenthesis to disambiguate, but we consider the point where you already have a tree structure, so it is unambiguous). We can write this evaluation relation as:
+Evaluation is standard (if you wanted to parse this, you would need to deal with left/right associativity, and probably add parenthesis to disambiguate, but we consider the point where you already have a tree structure, so it is unambiguous). We can write the evaluation function as:
Fixpoint eval_Expr (e : Expr) : Z :=
match e with
| Num n => n
@@ -268,6 +273,7 @@ How to prove a compiler fully abstract
specialize (eqsource c'); simpl in *; congruence.
Qed.This was obviously a very tiny language and a very restrictive linker that only allowed very restrictive contexts, which was done primarily to make the proofs very short, but the general shape of the proof is the same as that used in more realistic languages published in research conferences today!
+So next time you see a result about a correct (or even hoped to be correct), ask if it is fully abstract! And if it’s not, are the violations of equivalences something that could be exploited? Or something that would invalidate optimizations?
diff --git a/drafts/how-to-prove-a-compiler-fully-abstract.md b/drafts/how-to-prove-a-compiler-fully-abstract.md index 1178f8d..825f722 100644 --- a/drafts/how-to-prove-a-compiler-fully-abstract.md +++ b/drafts/how-to-prove-a-compiler-fully-abstract.md @@ -37,6 +37,8 @@ programs formally as: p1 ≈ p1 ``` +### Contextual equivalence + But we often also want to compile not just whole programs, but particular modules, or expressions, or in the general sense, **components**, and in that case, we want an analogous notion of equivalence. Two components are **contextually equivalent** if in all program @@ -90,6 +92,8 @@ secure compilers for, and while it's not the topic of this post, it's always important to know what you mean by contextual equivalence, which usually means: _what can program contexts determine about components_. +### Part 1. Equivalence reflection + With that in mind, what does **equivalence reflection** and **equivalence preservation** for a compiler mean? Let's start with **equivalence reflection**, as that's the property that all your correct compilers already have. Equivalence @@ -131,6 +135,8 @@ different target programs not only for source programs that were observationally different, but even syntactically different! That would be a pretty bad compiler, and certainly not correct, but it would be equivalence reflecting. +### Part 2. Equivalence preservation + Equivalence preservation, on the other hand, is the hallmark of fully abstract compilers, and it is a property that even most correct compilers do not have, though it would certainly be great if they did. It says that if two source @@ -169,6 +175,8 @@ component _in my language_, but the whole program can no longer work. Proving a compiler fully abstract, therefore, is all about proving equivalence preservation. So how do we do it? +### How to prove equivalence preservation + Looking at what we have to prove, we see that given contextually equivalent source components `s1` and `s2`, we need to show that `t1` and `t2` are contextually equivalent. We can expand this to explicitly quantify over the @@ -207,6 +215,8 @@ Cs'[s1] ≈ Cs'[s2] Ct[t1] ? Ct[t2] ``` +### Concrete example of languages, compiler, & proof of full abstraction + Let's make this concrete with an example. This will be presented somewhat in english and some in Coq. Our source language is arithmetic expressions over integers with addition and @@ -230,7 +240,7 @@ Inductive Expr : Set := Evaluation is standard (if you wanted to parse this, you would need to deal with left/right associativity, and probably add parenthesis to disambiguate, but we consider the point where you already have a tree structure, so it is -unambiguous). We can write this evaluation relation as: +unambiguous). We can write the evaluation function as: ```coq Fixpoint eval_Expr (e : Expr) : Z := @@ -591,6 +601,11 @@ allowed very restrictive contexts, which was done primarily to make the proofs very short, but the general shape of the proof is the same as that used in more realistic languages published in research conferences today! +So next time you see a result about a correct (or even hoped to be correct), ask +if it is fully abstract! And if it's not, are the violations of equivalences +something that could be exploited? Or something that would invalidate +optimizations? + > As stated at the top of the post, all the code in this post is available at > [https://github.com/dbp/howtoprovefullabstraction](https://github.com/dbp/howtoprovefullabstraction).As stated at the top of the post, all the code in this post is available at https://github.com/dbp/howtoprovefullabstraction. If you have any trouble getting it going, open an issue on that repository.