389 lines
16 KiB
TeX
389 lines
16 KiB
TeX
{
|
|
\section{Soundness}
|
|
|
|
Before we can prove that our migration transformation is sound, we
|
|
must first define what soundness means for a partially typed system.
|
|
It cannot mean absence of runtime errors, since not all modules are
|
|
necessarily typed. All we can say instead is that the \emph{typed}
|
|
modules do not go wrong.
|
|
|
|
\subsection{Soundness for Mixed Programs}
|
|
\renewcommand\tau{a}
|
|
|
|
Soundness for interlanguage migration is a relation
|
|
between the program before and after migration.
|
|
Intuitively, this relation states that the two programs
|
|
agree when they both produce values and that the typed module never
|
|
produces a type error at runtime. We say that a program $P$ with exactly one typed module
|
|
named $a$, is \emph{partially typed at $a$}, or simply \emph{partially
|
|
typed} when the name of the typed module is not relevant.
|
|
|
|
\begin{definition}[Soundness]
|
|
$\related{P}{Q}$, where $Q$ is partially typed at $a$ iff:
|
|
\begin{enumerate}
|
|
\item If $P \dlsreduces v$ then there exists $v'$ where $Q \dlsreduces v'$ with $\similar{v}{v'}$ or $Q
|
|
\dlsreduces \blame{g}$ with $g \neq \tau$.
|
|
\item If $P \dlsreduces \blame{h}$ then there exists $g$ where $Q \dlsreduces \blame{g}$
|
|
with $g \neq \tau$.
|
|
\item If $P$ reduces forever, then $Q$ reduces forever or
|
|
there exists $g$ where $Q \dlsreduces \blame{g}$
|
|
with $g \neq \tau$.
|
|
\end{enumerate}
|
|
\end{definition}
|
|
|
|
\noindent
|
|
This definition relies on the \emph{similarity} relation $\similar{v}{v'}$, which
|
|
states that $v'$ is the same as $v$, with the possible addition of
|
|
types, contracts, and casts.
|
|
\begin{figure}
|
|
$$
|
|
\begin{array}{c}
|
|
\inferrule[Programs]{\overline{\similar{M}{M'}} \\
|
|
\similar{e}{e'}}{\similar{\overline{M}\ e}{\overline{M'}\ e'}} \vspace*{4mm}\\
|
|
\inferrule[Modules]{}{\similar{ \modu{f}{e}}{ \modu{f}{e} }}\\
|
|
\similar{ \modu{f}{e} }{\mc{f}{c}{e}} \vspace{1mm} \\
|
|
\inferrule{\similar e {e'}}{\similar{ \modu{f}{e} }{\mt{f}{t}{e'}}} \vspace{4mm} \\
|
|
\inferrule[Expressions]{}{\similar x x} \qquad {\similar f f} \qquad {\similar n n} \vspace{1mm} \\
|
|
\inferrule{\similar {\e{}}{ e'}}
|
|
{\similar{\e{}}{ \cast{c}{f}{e'}}} \qquad
|
|
\inferrule{\similar{\e1}{\e1'} \\ \similar{\e2}{\e2'}}{\similar{\comb{\e1}{\e2}}
|
|
{\comb{\e1'}{\e2'}}} \vspace{1mm} \\
|
|
\inferrule{\similar e e'}{\similar{\dlsabs{x}{e}}{\dlsabs{x}{e'}}} \qquad
|
|
\inferrule{\similar e e'}{\similar{\dlsabs{x}{e}}{\Tabs{x}{t}{e'}}} \vspace{1mm} \\
|
|
\inferrule{\similar{\e1}{\e1'} \\ \similar{\e2}{\e2'} \\\similar{\e3}{\e3'}}
|
|
{\similar{\ifz {e_1} {e_2} {e_3}}{\ifz {e_1'} {e_2'} {e_3'}}} \vspace{4mm}\\
|
|
|
|
\inferrule[Contexts]{\similar{e}{e'} \Rightarrow \similar{E[e]}{E'[e']}}{\similar{E}{E'}}
|
|
\end{array}
|
|
$$
|
|
\caption{Similarity} \label{fig:similarity}
|
|
\end{figure}
|
|
In figure~\ref{fig:similarity}, this relation is defined formally and
|
|
extended to modules and to programs. For programs,
|
|
$\similar{P}{Q}$ states that $P$ and $Q$ are syntactically identical,
|
|
ignoring casts, contracts and types.
|
|
|
|
We say that a system for typed migration is {\it sound} if
|
|
the migrated program is always in the $\trianglerighteq$ relation to
|
|
the original program. For the $MT$ transformation, this requires that
|
|
every element of $MT(P)$ is related to $P$.
|
|
|
|
This captures our intuition as to how typed migration should work:
|
|
that once we have migrated, we have proven the absence of errors in
|
|
the typed module. Further, if we get an answer, it is related to the
|
|
original answer. Since our reduction system tracks where errors occur, we are
|
|
able to express this statement formally.
|
|
|
|
\subsection{Soundness of our system}
|
|
|
|
Proving soundness for our system is a multi-step process. First, we
|
|
establish that the system resulting from the transformation agrees
|
|
with the original one, when
|
|
errors are ignored. This is established through a simple simulation relation
|
|
between programs. Second, we prove that programs in $MT(P)$ never
|
|
blame the typed module.
|
|
|
|
For the first of these steps, we again make use of the similarity property
|
|
mentioned above and defined in figure~\ref{fig:similarity}.
|
|
This relation between an untyped program (respectively, module or
|
|
expression) and a partially typed one, states syntactically that the
|
|
two programs $P$ and $Q$ are similar, written
|
|
$\similar{P}{Q}$, if they are identical ignoring contracts, types
|
|
and casts.
|
|
|
|
Similarity satisfies three lemmas:
|
|
|
|
\begin{lemma}
|
|
If $\similar{P}{Q}$ and $P \dlsreduces w$ and $Q \dlsreduces w'$ then $\similar{w}{w'}$.
|
|
\end{lemma}
|
|
|
|
\begin{lemma}
|
|
If $\similar{P}{Q}$ and $P$ reduces forever then $Q$ reduces
|
|
forever or $Q \dlsreduces \blame{f}$ for some $f$.
|
|
\end{lemma}
|
|
|
|
\begin{lemma}
|
|
If $\similar{P}{Q}$ and $P \dlsreduces \blame{f}$ for some $f$ then $Q
|
|
\dlsreduces \blame{g}$ for some $g$.\end{lemma}
|
|
|
|
\noindent\textbf{Proof Sketch}
|
|
These three lemmas all follow from similar simulation arguments. If
|
|
$\similar{e_1}{e_2}$, then there are three possibilities:
|
|
\begin{enumerate}
|
|
\item $e_2 = E[\cast{c}{f}{v}]$ Then either $e_2 \rightarrow
|
|
\blame{f}$ or $e_2 \rightarrow e_2'$ where $\similar{e_1}{e_2'}$.
|
|
This can be seen by simple inspection of the reduction rules for
|
|
casts.
|
|
\item $e_2 = E[\comb{\cast{\barrcnt{c_1}{c_2}}{f}{l}}{w}]$. Then $e_2
|
|
\rightarrow e_2'$ and $\similar{e_1}{e_2'}$
|
|
\item $e_1 = E[r_1]$ and $e_2 = E'[r_2]$ where $\similar{r_1}{r_2}$
|
|
and $\similar{E}{E'}$. Then $r_1
|
|
\rightarrow r_1'$ and $r_2 \rightarrow r_2'$ where
|
|
$\similar{r_1'}{r_2'}$ or $r_1 \rightarrow \blame{f}$ and $r_2
|
|
\rightarrow \blame{g}$. That the hypothesis holds is true from the
|
|
definition of similarity and the grammar for $E[]$. The fact that
|
|
the redexes reduce to similar terms or to errors can be seen from inspection of
|
|
the reduction rules where the redex is not a cast or the application
|
|
of a (blessed arrow) cast to a value.
|
|
|
|
Additionally, by the compositionality of similarity, placing
|
|
similar values into similar contexts produces similar terms.
|
|
Therefore, $\similar{E[r'_1]}{E'[r'_2]}$.
|
|
\end{enumerate}
|
|
Given this, similarity is consistently maintained by reduction, which
|
|
is all we need for the three lemmas. \qed
|
|
|
|
These lemmas are insufficient to establish soundness, since
|
|
they make no claim about who is blamed for an error. We therefore
|
|
introduce the notion of \emph{valid} expressions to prove that the
|
|
typed module is never blamed.
|
|
|
|
\paragraph{Validity}
|
|
Validity is a property of \emph{mixed} terms, those that combine code
|
|
from both typed and untyped modules (and the original main
|
|
expression). Before defining validity, we first present a new type
|
|
system for mixed terms which ensures that mixed terms use their typed subcomponents
|
|
appropriately. This type system has the judgement
|
|
$$
|
|
\mtypej{e}{t}
|
|
$$
|
|
which states that mixed expression $e$ has type $t$ in program $P$
|
|
and environment
|
|
$\Gamma$.
|
|
The rules of the type system are given in figure~\ref{fig:mixed-types}.
|
|
Note that untyped terms are not inspected by this judgement---instead,
|
|
their casts are simply trusted.
|
|
% Validity implies that
|
|
% there are no applications of numbers where the application is labeled
|
|
% with $\tau$, and also that every cast blaming $\tau$ is applied to a
|
|
% term that satisfies that cast.
|
|
|
|
|
|
\begin{figure*}[htbp]
|
|
$$
|
|
\inferrule[VT-Var]{}{\mtypej{x}{\Gamma(x)}} \qquad
|
|
\inferrule[VT-Cast]{e \mbox{\ closed}}{\mtypej{\cast{t}{f}{\e{}}}{t}} \qquad
|
|
$$
|
|
$$
|
|
\inferrule[VT-BlessedCast]{}{\mtypej{\cast{\barrcnt{t_1}{t_2}}{f}{v}}{\dlsproctype{t_1}{t_2}}} \qquad
|
|
\inferrule[VT-Int]{}{\mtypej{n}{\dlsint}}
|
|
$$
|
|
$$
|
|
\inferrule[VT-App]{{\mtypej{\e1}{\dlsproctype{t_1}{t_2}}} \\ % \\ separates premises
|
|
{\mtypej{\e2}{t_1}}}
|
|
{ {\mtypej {\comb{\e1}{\e2}} {t_2}}} \qquad
|
|
$$
|
|
$$
|
|
\inferrule[VT-If0]{{\mtypej{\e1}{t_1}} \\
|
|
{\mtypej{\e2}{t_2}} \\
|
|
{\mtypej{\e3}{t_2}}}
|
|
{ {\mtypej {\ifz{\e1}{\e2}{\e3}}{t_2}}}
|
|
$$
|
|
$$
|
|
\inferrule[VT-Abs]{\mtypejg{\Gamma,\hastype{x}{t}}{\e{}}{s}}
|
|
{\mtypej{\Tabs{x}{t}{\e{}}}{\dlsproctype t s}}
|
|
$$
|
|
$$
|
|
\inferrule[VT-TypeMod]{\mbox{$\mt{\tau}{t}{e} \in P$}}{\mtypej{\tau^{\tau}}{t}}
|
|
$$
|
|
\caption{Consistency Type System}\label{fig:mixed-types}
|
|
\end{figure*}
|
|
|
|
There a several rules to note in the type system. First, the rule
|
|
{\sc VT-Cast} does not ensure that its argument is well-typed.
|
|
Therefore, it applies even where the argument is an untyped term, and
|
|
the cast is protecting the context of the cast from its argument.
|
|
Second, the {\sc VT-BlessedCast} rule is necessary so that blessed
|
|
casts can appear during reduction, even though they are not part of
|
|
the syntax of types. Third, we allow the typed module to be used
|
|
without a cast in rule {\sc VT-TypeMod}. Such module references are
|
|
still protected from the untyped world, because they are within a
|
|
typed expression.
|
|
|
|
We now define two important properties of mixed terms.
|
|
|
|
\begin{definition}
|
|
A mixed term $e$ is \emph{consistent at $t$ in $P$} iff
|
|
$\mtypejg{\emptyset}{e}{t}$, or simply \emph{consistent} if there is
|
|
some $t$ such that $\mtypejg{\emptyset}{e}{t}$.
|
|
\end{definition}
|
|
\noindent
|
|
Terms may be consistent even if they do not originate in a typed module,
|
|
or even if some of their subterms are not consistent. For example,
|
|
$\mtypejg{\emptyset}{\cast{\dlsint}{f}{\dlsabs{x}{\comb{3}{x}}}}{\dlsint}$ for
|
|
any $f$ (including $\tau$), even
|
|
though the expression is patently erroneous.
|
|
|
|
Based on this definition, only some kinds of terms can be consistent:
|
|
typed abstractions, numbers, casts and applications of two consistent
|
|
terms.
|
|
|
|
\begin{definition}
|
|
A mixed term $e^f$ is \emph{originally typed in $P^\tau$} iff $f = \tau$.
|
|
\end{definition}
|
|
\noindent
|
|
This definition gives us a handle on those terms that came from the
|
|
original typed module. These are the terms that must not trigger errors
|
|
during the execution of the program. No guarantees are made about the
|
|
subterms of originally typed terms, however, in the case where they have a
|
|
different label.
|
|
|
|
With these definitions, we can define validity, the property that we use for our
|
|
central lemma. This property ensures both that numbers are
|
|
not in the operator position of a typed application, and that typed
|
|
terms satisfy any immediately surrounding casts. Maintenance of these
|
|
two properties is sufficient to ensure that $\tau$ is never blamed. The
|
|
third portion of the definition states that there is always a syntactic
|
|
barrier between consistent and inconsistent portions of the expression,
|
|
with the exception of numbers. This is the mechanism that is central
|
|
to maintaining the other two during reduction.
|
|
|
|
\begin{definition}
|
|
A closed mixed term $e_m$ is \emph{valid in program $P$} where $P$
|
|
has typed module $a$ iff all of the following hold:
|
|
\begin{enumerate}
|
|
\item every originally typed subexpression $d^\tau \in e_m$ is either consistent
|
|
or of the form ${\comb{\dlsabs{x}{e}}{e'}}^\tau$
|
|
\item for every subexpression of the form $\cast{t}{\tau}{e}$, $e$
|
|
is consistent at $t$.
|
|
\item every consistent term $d \in e_m$ is either a number, a cast, or the
|
|
immediate subterm of a consistent term or $d = e_m$.
|
|
\end{enumerate}
|
|
\end{definition}
|
|
|
|
Note that since the initial main expression $e$ in a program $P$ is
|
|
closed, it is also valid, since it does not contain any
|
|
originally typed subexpression or casts.
|
|
|
|
\begin{lemma}
|
|
\label{lem:central}
|
|
If a mixed term $e_m$ is valid in program $Q \in MT(P)$ (where $Q$
|
|
has typed module $a$) for
|
|
some $P$, and $e_m \rightarrow e_m'$ then $e_m'$
|
|
is valid in program $Q$.
|
|
\end{lemma}
|
|
|
|
\noindent\textbf{Proof Sketch}
|
|
This proof proceeds by cases on the reduction rule that takes $e_m$ to
|
|
$e_m'$. The important cases are {\sc Split}, {\sc Subst}, {\sc
|
|
TypedSubst} and {\sc LookupTyped}. We show two of these here.
|
|
|
|
Consider case {\sc Split}. Then $r =
|
|
{\comb{\cast{\barrcnt{c_1}{c_2}}{g}{v}}{w}}^f$ and $r' =
|
|
\cast{c_2}{g}{\comb{v}{\cast{c_1}{f}{w}}^f}$. We consider the three
|
|
components of validity in turn.
|
|
\begin{enumerate}
|
|
\item Originally-typed
|
|
subexpressions of $r'$ occur only in $v$ and $w$, or if the
|
|
resulting application has label $\tau$ (that is, that $f = \tau$).
|
|
|
|
If $v$ or $w$ contain
|
|
originally typed subexpression, these subexpressions must have been
|
|
originally typed in $r$, and so by
|
|
hypothesis they are still consistent.
|
|
|
|
Since $v$ is the argument to a blessed function cast, it must be an
|
|
abstraction, and therefore the application satisfies condition 1 (if
|
|
$f = a$).
|
|
|
|
If the redex is part of
|
|
a larger originally typed expression, then $r$ must have been consistent, and
|
|
must have had type $c_2$. But $\mtypejg[Q]{\emptyset}{r'}{c_2}$, so this
|
|
property is maintained.
|
|
|
|
|
|
\item Consider first the inner cast.
|
|
If $w$ is originally typed, then it must have been consistent (since the only
|
|
other possibility is not a value). Therefore, the whole application
|
|
must have been consistent, and thus $\mtypejg[Q]{\emptyset}{w}{c_1}$, which is
|
|
precisely the desired type.
|
|
|
|
If $g = \tau$, then we must also show that
|
|
$\mtypejg[Q]{\emptyset}{{\comb{v}{\cast{c_1}{f}{w}}^f}}{c_2}$. But then by
|
|
assumption, $\mtypejg[Q]{\emptyset}{v}{\dlsproctype{c_1}{c_2}}$ and
|
|
$\cast{c_1}{f}{w}$ trivially has type $c_1$.
|
|
|
|
If $r$ is the argument to a cast, we merely
|
|
must show that the type is preserved by reduction. But the original
|
|
type of $r$ must have been $c_2$, which is also the type of $r'$.
|
|
|
|
|
|
\item Both casts trivially satisfy this case. Thus we have to
|
|
consider $v$, $w$, and the application. Both the application and
|
|
$w$ are immediate arguments to a cast. If $v$ is consistent, then it
|
|
must be been a typed abstraction, since it is the argument of a
|
|
blessed arrow contract, and untyped abstractions are not consistent.
|
|
If it is a type-annotated abstraction, it must have label $\tau$,
|
|
as required by the grammar.
|
|
Thus, by hypothesis, it must satisfy its cast, and have type
|
|
$\dlsproctype{c_1}{c_2}$. Therefore, since the operand is a cast to
|
|
$c_2$, $\mtypejg{}{\comb{v}{\cast{c_1}{f}{w}}}{c_2}$.
|
|
\end{enumerate}
|
|
This concludes the case.
|
|
|
|
Consider case {\sc Subst}. Then $r = \comb{\dlsabs{x}{e}}{v}$ and $r'
|
|
= [v/x]e$. We again consider the three components of validity.
|
|
First, note that references to $x$ in $e$ cannot be either originally
|
|
typed or part of a consistent expression (without an intervening
|
|
cast), since $x$ is bound by an untyped abstraction.
|
|
\begin{enumerate}
|
|
\item First, any
|
|
originally typed and consistent expressions in $v$ remain so in
|
|
$r'$. This leaves the originally typed expressions in $e$. Choose
|
|
one of these, $d^a$. By hypothesis, either \mtypej{d^a}{t} or $d^a
|
|
= \comb{\dlsabs{y}{e_1}}{e_2}$. In the former case, $x$
|
|
is not in the free variables of $d^a$, since it cannot occur outside
|
|
of a cast, and {\sc VT-Cast} requires that the cast argument be
|
|
closed. Thus, $[v/x]d^a = d^a$. In the latter case, $[v/x]d^a =
|
|
\comb{\dlsabs{y}{[v/x]e_1}}{[v/x]e_2}$ which is of the appropriate
|
|
form.
|
|
\item By a similar argument, if $e$ has a subexpression of the form
|
|
$\cast{t}{a}{e'}$, then $e'$ is consistent and $[v/x]e' = e'$.
|
|
\item First, note that neither $v$ nor $e$ is consistent unless they are numbers or
|
|
casts, since they are not immediate subterms of consistent terms.
|
|
Thus consistent subterms of $v$ and $e$ that are not numbers or
|
|
casts must be proper subterms. The consistent subterms of $v$ are
|
|
preserved in $r'$. Further, since no reference to $x$ in the body
|
|
of $e'$ is consistent, the consistent subterms of of $e$ are
|
|
maintained.
|
|
\end{enumerate}
|
|
|
|
|
|
This concludes the case. The others are proved in a similar way. \qed
|
|
|
|
Given this lemma, we can now show that blame is never assigned to the
|
|
typed module.
|
|
|
|
\begin{lemma}[MT never blames the typed module]
|
|
If $P^\tau \in MT(P)$, and $P^\tau \dlsreduces \blame{g}$ then $g \neq
|
|
\tau$.
|
|
\label{lem:no-blame}
|
|
\end{lemma}
|
|
|
|
\noindent\textbf{Proof Sketch}
|
|
The only way we could ever reduce to \blame{\tau} is if
|
|
${\comb{n}{v}}^\tau$ is the redex or if a cast fails and blames $\tau$.
|
|
However, since the main expression is originally untyped, and thus
|
|
valid, and remains valid by lemma~\ref{lem:central}, this is impossible. \qed
|
|
|
|
We can now conclude the main theorem of this chapter.
|
|
|
|
\begin{theorem}[Soundness of MT]
|
|
\label{thm:dlsmain}
|
|
If $P^\tau \in MT(P)$ then $\related{P}{P^\tau}$.
|
|
\end{theorem}
|
|
|
|
\noindent\textbf{Proof Sketch}
|
|
First, note that if $\ttgproves{e}{t}{e'}$ then
|
|
$\similar{e}{e'}$. Therefore, if $P^\tau \in MT(P)$, then
|
|
$\similar{P}{P^\tau}$.
|
|
%
|
|
From this, if $P \dlsreduces v$ and $P^\tau \dlsreduces v'$ then
|
|
$\similar{v}{v'}$.
|
|
Similarly, if $P$ reduces forever, then $P^\tau \not\dlsreduces v$ for any
|
|
$v$. Therefore, lemma~\ref{lem:no-blame}, stating that if an error occurs,
|
|
the blame is assigned to one of the untyped modules, suffices for the
|
|
proof. \qed
|
|
|
|
}
|