Friday, August 24, 2012

Type Safety in Five Easy Lemmas

A language is type safe if running a program in the language cannot result in an untrapped error. A trapped error is something like an exception or a message-not-found error, that is, it's an error that is part of the defined behavior of the language. An untrapped error is something like a segmentation fault, that is, the program has run into an undefined state in which the language doesn't define what should happen. A segmentation fault is the underlying operating system catching the error, not the language itself. It is the untrapped errors that hackers take advantage of to break into computer systems. If you want to run untrusted code without getting into trouble, then it's a good idea to only run code that is in a type safe language!

Wright and Felleisen pioneered what has become the most flexible approach to proving that a language is type safe in their 1992 paper A Syntactic Approach to Type Soundness. The general idea is to define a small-step operational semantics for the language and show that if a program is well typed, then it is either done reducing or it can reduce to another well-typed program. The safety of an entire sequence of reductions can then be proved by induction. It is now common practice for language designers to prove type safety for new language designs, or at least for interesting subsets of the languages of interest. Proving type safety does not require advanced mathematics and isn't particularly challenging, except that it is often rather tedious, requiring many technical lemmas in which it is easy to make a mistake.

It turns out that the choice in formulation of the operational semantics can make a significant difference regarding how many lemmas, and how tedious, the proof of type safety becomes. In this blog post, I present an operational semantics that removes the need for many of the standard lemmas. The semantics is based on an abstract machine. The language will be the simply-typed lambda calculus in A-normal form, extended with recursive functions and a few primitive operators. Despite its small size, this language is Turing complete. This language is roughly equivalent to the target language discussed in my previous posts about Structural Induction and the ECD Machine. In the following I present the syntax, operational semantics, and type system of this language. Then I give the proof of type safety. The proof will rely on five lemmas, one lemma for each function or relation used in the operational semantics: the variable partial function, the partial function that defines the behavior of the primitive operators, the partial function for evaluating expression, the transition relation for the abstract machine, and the multi-transition relation . The lemma for the transition relation is the main event.

Syntax

Operational Semantics

We use the notation for the empty list. Given a list , the notation is a larger list with as the first element and the rest of the elements are the same as . We use lists of key-value pairs (association lists) to represent mapping from variables to types (type environments) and variables to values (environments). The following lookup (partial) function finds the thing associated with a given key in an association list. Next we define the function, which gives meaning to the primitive operators. The function maps expressions to values, using environment . The values of this language are constants and closures, as defined below. The definition of uses the function for variables, the function for primitive operations, and turns functions to closures. A stack is a list of statement-environment pairs. The state of the machine is simply a stack. The top of the stack contains the actively-executing statement and its environment. The relation defines transitions between states. There are only three transition rules, for primitive operators, calling functions, and returning from functions. We define in the usual way, as follows. The semantics of this language is given by the following function. A state is final if it is of the form and for some .

Type System

The types for the constants is given by the function. The function maps a primitive operator and argument types to the return type. The following presents the type rules for expressions, definitions, and statements. Our proof of type safety will require that we define notions of well-typed values, well-typed environments, well-typed stacks, and well-typed states.

Proof of Type Safety

The first lemma proves that when an operator is applied to values of the expected type, the result is a value whose type matches the return type of the operator.

Lemma ( is safe)
If and for , then and , for some .

Proof. We proceed by cases on the operator .

  1. If the operator is , then we have and . Then because , we know that for . Then and we have .
  2. If the operator is , then we have and . Then because , we know that for some . Then and we have .
  3. If the operator is , then we have and . Then because , we know that for . Then and we have .
QED.

The second lemma says that if you have an environment that is well-typed with respect to the type environment, and if a variable x is associated with type T in the type environment, then looking up x in the environment produces a value that has type T.

Lemma ( is safe)
If and , then and for some .
Proof. We proceed by induction on .
  1. Case
    But then we have a contradition with the premise , so this case is vacuously true.
  2. Case :
    Next we consider two cases, whether or not.
    1. Case : Then and , so we conclude that .
    2. Case : Then and . By the induction hypothesis, we have and for some , which completes this case.
QED.

The next lemma proves that a well-typed expression evaluates to a value of the expected type.

Lemma ( is safe)
If and , then and for some .
Proof. We proceed by cases on the expression .
  1. Case :
    From we have and therefore . Also, we have , which completes this case.
  2. Case :
    From we have . We then apply the lookup is safe lemma to obtain and for some . Thus, we have and this case is complete.
  3. Case :
    We have . From we have , with . Together with , we conclude that .
QED.

Now for the fourth and most important lemma. This lemma states that if a state is well typed, then either the state is a final state or the state can transition to a new state of the same type. In the literature, this lemma is often split into two lemmas called progress and preservation. In the setting of an abstract machine, it's convenient to merge these two lemmas into one lemma. Note that the conclusion of this lemmas includes two alternatives: the state is final or it can take a step. The power of this lemma is that it rules out the third alternative, that the state is not final and can't take a step. Such a situation is referred to as "stuck" and corresponds to untrapped errors.

Lemma ( is safe)
If , then either is a final state or and .
Proof. Because we know that , , , and . We proceed by cases on because the transition rule that will apply depends primarily on .
  1. Case :
    We have and . So and for . Because is safe, we have and for . Because is safe, we have and for some . Thus, the current state takes the following transition. We have
    and therefore
  2. Case :
    From we have and . Thus, we also have and . Because is safe, there exist and such that , , , and . The only way for to be true is for to be a closure. That is, . This closure is well typed, so we have and . We have what we need to know that the current state transitions as follows. We can deduce
    and
    so we have everything necessary to conclude
  3. Case :
    If the stack is empty, then is a final state and this case is complete. If the stack is not empty, we have . Then, because , we have , , , and . Because , we have and therefore and for some (because is safe). So the current state takes the following transition: We have , which is the last thing we needed to conclude that .
QED.

Lemma ( is safe)
If and , then .
Proof. The proof is by induction on .
  1. Case : We already have .
  2. Case : Because is safe and deterministic (the three transition rules obviously do not overlap), we have . Then by the induction hypothesis, we conclude that .
QED.

Theorem (Type Safety)
If , then either
  1. and , or
  2. and for some , or
  3. (the program does not terminate).

Proof. Suppose that the program terminates. We have for some and . Because is safe, we have . Then because is safe, we know that either is final or it can take a step. But we know it can't take a step, so it must be final. So and . Then because is safe, we have and . If , then we have and . If , then , , and .
QED.

That's it! Type safety in just five easy lemmas.

2 comments:

  1. In the transition rule Call, I think v_2 should equal to V(e_2, /rho), instead of V(e_1, /rho).

    ReplyDelete