374 lines
No EOL
11 KiB
Text
374 lines
No EOL
11 KiB
Text
#import "../common.typ": *
|
|
#import "@preview/prooftrees:0.1.0": *
|
|
#show: doc => conf("Logical Relations", doc)
|
|
|
|
#let safe = $"safe"$
|
|
|
|
== Lecture 1
|
|
|
|
=== Logical relations
|
|
|
|
Logical relations are used to prove things about programs
|
|
|
|
- Unary equivalence
|
|
- Example: Prove termination of the STLC
|
|
- Example: Prove type soundness / safety (these lectures)
|
|
|
|
- Binary equivalence
|
|
- Example: are two programs going to behave the same when you put them in some different context? (*contextual equivalence*)
|
|
|
|
-
|
|
Representation independence
|
|
|
|
- Example: suppose u implement a stack and have 2 different implementations. Prove that it doesn't matter which implementation you use.
|
|
- Parametricity for existential types "there exists a stack such that these properties are true"
|
|
|
|
- Parametricity
|
|
- Security levels of data in a security programming language
|
|
- Establish that high-security data never flows to low-security observers (*non-interference*)
|
|
|
|
You can also relate source terms to target terms in different languages.
|
|
This can be used to prove compiler correctness.
|
|
|
|
=== Type safety / soundness
|
|
|
|
Unary realizability relations for FFI. "all well-behaved terms from language A can be used in language B without causing problems with either language"
|
|
|
|
=== STLC
|
|
|
|
Statics
|
|
|
|
- $tau ::= "bool" | tau_1 arrow.r tau_2$
|
|
- $e ::= x | "true" | "false" | ifthenelse(e, e_1, e_2) | lambda (x : tau) . e | e_1 " " e_2$
|
|
- $v ::= "true" | "false" | lambda (x:tau) . e$
|
|
- $E ::= [dot] | "if" E "then" e_1 "else" e_2 | E " " e_2 | v " " E$
|
|
|
|
Operational semantics
|
|
|
|
|
|
#rect[$e mapsto e'$]
|
|
|
|
#tree(
|
|
axi[],
|
|
uni[$ifthenelse("true", e_1, e_2) mapsto e_1$]
|
|
)
|
|
|
|
#tree(
|
|
axi[],
|
|
uni[$ifthenelse("false", e_1, e_2) mapsto e_2$]
|
|
)
|
|
|
|
#tree(
|
|
axi[],
|
|
uni[$(lambda (x:tau) e) v mapsto subst(x, v, e)$]
|
|
)
|
|
|
|
#tree(
|
|
axi[$e mapsto e'$],
|
|
uni[$E[e] mapsto E[e']$]
|
|
)
|
|
|
|
Contexts:
|
|
|
|
$Gamma ::= dot | Gamma , x : A$
|
|
|
|
#rect[$Gamma tack.r e : tau$]
|
|
|
|
#tree(
|
|
axi[],
|
|
uni[$Gamma tack.r "true" : "bool"$]
|
|
)
|
|
|
|
#tree(
|
|
axi[],
|
|
uni[$Gamma tack.r "false" : "bool"$]
|
|
)
|
|
|
|
#tree(
|
|
axi[$Gamma tack.r e : "bool"$],
|
|
axi[$Gamma tack.r e_1 : tau$],
|
|
axi[$Gamma tack.r e_2 : tau$],
|
|
tri[$Gamma tack.r ifthenelse(e, e_1, e_2) : tau$]
|
|
)
|
|
|
|
#tree(
|
|
axi[$Gamma(x) = tau$],
|
|
uni[$Gamma tack.r x : tau$]
|
|
)
|
|
|
|
#tree(
|
|
axi[$Gamma , x : tau tack.r e : tau_2$],
|
|
uni[$Gamma tack.r lambda (x : tau_1) . e : tau_1 arrow.r tau_2 $]
|
|
)
|
|
|
|
#tree(
|
|
axi[$Gamma tack.r e_1 : tau_2 arrow.r tau$],
|
|
axi[$Gamma tack.r e_2 : tau_2$],
|
|
bin[$Gamma tack.r e_1 e_2 : tau$],
|
|
)
|
|
|
|
#quote(block: true, attribution: [Milner])[
|
|
Well-typed programs do not go wrong
|
|
]
|
|
|
|
What does "going wrong" mean? It means getting stuck. You can't take another step and it's not a value.
|
|
|
|
*Definition (Type Soundness).* If $dot tack.r e : tau$, then
|
|
$forall(e' . e mapstostar e')$ either $isValue(e')$ or $exists e'' . e' mapsto e''$
|
|
|
|
*Definition (Progress).* If $dot tack.r e : tau$ then either $isValue(e)$ or $exists e' . (e mapsto e')$.
|
|
|
|
*Definition (Preservation).* If $dot tack.r e : tau$ and $e mapsto e'$ then $dot tack.r e' : tau$.
|
|
|
|
Progress and preservation are a _technique_ for proving type soundness, by just using the two functions over and over.
|
|
|
|
=== Logical relations
|
|
|
|
$ P_tau(e) $
|
|
|
|
A unary relation on any expression $e$ and its corresponding type $tau$.
|
|
(There are also binary relations $R_tau (e_1, e_2)$)
|
|
|
|
The property we're interested in is: $safe(e)$
|
|
|
|
- If $dot tack.r e:tau$ then $safe(e)$
|
|
|
|
*Definition (safe).* $safe(e) :equiv forall e' . (e mapstostar e') arrow.r.double isValue(e') or exists e'' . (e' mapsto e'')$
|
|
|
|
*Definition (Semantic Type Soundness).* $dot tack.r e : tau$ then $safe(e)$
|
|
|
|
Common technique:
|
|
|
|
- Focus on the values, when do values belong to the relation, when are they safe?
|
|
- Then check expressions. When do expressions belong to the relation, and when are they safe?
|
|
|
|
$ V db(tau_1) = { v | ... } \
|
|
V db("bool") = { "true" , "false" } \
|
|
V db(tau_1 arrow.r tau_2) = { lambda (x : tau_1) . e | ... }
|
|
$
|
|
|
|
Can't have just arbitrary $lambda (x : tau_1) . e$ under $V db(tau_1 arrow.r tau_2)$.
|
|
The body also needs to be well-typed.
|
|
|
|
$
|
|
V db(tau_1 arrow.r tau_2) = { lambda (x : tau_1) . e | forall v in V db(tau_1) . subst(x, v, e) in Epsilon db(tau_2) } \
|
|
Epsilon db(tau) = { e | forall e' . e mapstostar e' and "irreducible"(e') arrow.r.double e' in V db(tau)} \
|
|
"irreducible"(e) :equiv cancel(exists) e' . e mapsto e'
|
|
$
|
|
|
|
#rect[
|
|
*Example of code from Rust.*
|
|
Unsafe code blocks are an example of a something that may not be _syntactically well-formed_, but are still represented by logical relations because they behave the same at the boundary.
|
|
]
|
|
|
|
The difference between semantic soundness with logical relations vs. progress and preservation is that you don't need to prove anything about intermediate states of running programs.
|
|
|
|
Can't just work with closed terms because of this rule:
|
|
|
|
#tree(
|
|
axi[$Gamma , x : tau tack.r e : tau_2$],
|
|
uni[$Gamma tack.r lambda (x : tau_1) . e : tau_1 arrow.r tau_2 $]
|
|
)
|
|
|
|
(Slightly more general theorem)
|
|
|
|
#rect(width: 100%)[
|
|
*Definition (Fundamental property of logical relations).*
|
|
Theorem we are trying to prove
|
|
$
|
|
Gamma tack.r e : tau arrow.r.double Gamma tack.r.double e : tau
|
|
$
|
|
- "syntactically well typed means semantically well typed"
|
|
]
|
|
|
|
Focus on terms with open variables
|
|
|
|
Use $gamma$ as a substitution from variables to values.
|
|
|
|
#rect[$G db(Gamma)$]
|
|
|
|
- $G db(dot) = { emptyset }$
|
|
- $G #db[$Gamma , x : tau$] = { gamma[x mapsto v] | gamma in G db(Gamma) and v in V db(tau)}$
|
|
|
|
"sound inputs will give you sound outputs". This is the important case
|
|
|
|
Now define semantic soundness:
|
|
|
|
$ Gamma tack.r.double e : tau :equiv forall (gamma in G db(Gamma)) . gamma(e) in Epsilon db(tau) $
|
|
|
|
Prove:
|
|
|
|
#set enum(numbering: "a.")
|
|
|
|
1. $dot tack.r e : tau arrow.r.double e in Epsilon db(tau)$
|
|
- this cannot be proved by focusing on closed terms alone
|
|
- This is why the fundamental property must be used, in the case of $Gamma = dot$, then the substitution $gamma$ is empty and the result is $e in Epsilon db(tau)$
|
|
2. $e in Epsilon db(tau) arrow.r.double safe(e)$
|
|
|
|
#set enum(numbering: "1.")
|
|
|
|
To prove A:
|
|
|
|
_Proof._ By induction on typing derivations
|
|
|
|
-
|
|
Case example:
|
|
|
|
#tree(
|
|
axi[],
|
|
uni[$Gamma tack.r "true" : "bool"$]
|
|
)
|
|
|
|
Show $Gamma tack.r.double "true" : "bool"$. Suppose $gamma in G db(Gamma)$.
|
|
Show $gamma("true") in Epsilon db("bool") equiv "true" in Epsilon db("bool")$.
|
|
Suffices to show $"true" in V db("bool")$, which is true by definition.
|
|
|
|
False is proved similarly.
|
|
|
|
-
|
|
Case example:
|
|
|
|
#tree(
|
|
axi[$Gamma(x) = tau$],
|
|
uni[$Gamma tack.r x : tau$]
|
|
)
|
|
|
|
Show $Gamma tack.r.double x : tau$. #TODO
|
|
|
|
To prove B:
|
|
|
|
_Proof._ Suppose $e'$ s.t. $e mapstostar e'$ .
|
|
|
|
- Case : $not "irreducible" (e')$ then $exists e'' . e' mapsto e''$
|
|
- Case : $"irreducible" (e')$ then $isValue(e')$ trivially.
|
|
|
|
#pagebreak()
|
|
|
|
== Lecture 2
|
|
|
|
#set enum(numbering: "A.")
|
|
|
|
Recall the lemmas we're proving:
|
|
|
|
1. $dot tack.r e : tau arrow.r.double e in Epsilon db(tau)$
|
|
2. $e in Epsilon db(tau) arrow.r.double safe(e)$
|
|
|
|
#set enum(numbering: "1.")
|
|
|
|
To prove lemma A, we must prove the fundamental property: $Gamma tack.r e:tau arrow.r.double Gamma tack.r.double e:tau$. "Syntactically well-typed implies semantic well-typed"
|
|
|
|
$ Gamma tack.r.double e : tau :equiv forall (gamma in G db(Gamma)) . gamma(e) in Epsilon db(tau) $
|
|
|
|
==== Proving A case for $lambda$
|
|
|
|
Case:
|
|
|
|
#tree(
|
|
axi[$Gamma , x : tau tack.r e : tau_2$],
|
|
uni[$Gamma tack.r lambda (x : tau_1) . e : tau_1 arrow.r tau_2 $]
|
|
)
|
|
|
|
*Show:* $Gamma tack.r.double lambda (x : tau_1) . e : tau_1 arrow tau_2$.
|
|
|
|
Suppose $gamma in G db(Gamma)$. Then we ned to *show*:
|
|
|
|
$ &gamma (lambda (x : tau_1). e) in Epsilon db(tau_1 arrow tau_2) \
|
|
equiv &lambda (x:tau_1).gamma(e) in Epsilon db(tau_1 arrow tau_2)
|
|
$
|
|
|
|
Suffices to show: $lambda (x:tau_1) gamma(e) in V db(tau_1 arrow tau_2)$.
|
|
|
|
Suppose $v in V db(tau_1)$. Then we need to show:
|
|
|
|
$ &subst(x, v, gamma(e)) in Epsilon db(tau_2) \
|
|
equiv & gamma[x mapsto v] (e) in Epsilon db(tau_2)$
|
|
|
|
By the induction hypothesis, $Gamma,x:tau_1 tack.r e:tau_2$, so $Gamma,x:tau_1 tack.r.double e:tau_2$.
|
|
|
|
Because $gamma[x mapsto v] in G db(#[$Gamma, x : tau_1$])$, we can instantiate $Gamma,x:tau_1$ with $gamma[x mapsto v]$. (basically just translating it over to $gamma$)
|
|
|
|
Therefore, $gamma[x mapsto v](e) in Epsilon db(tau_2)$
|
|
|
|
#TODO Do the app case at home.
|
|
|
|
=== Adding recursive types
|
|
|
|
$ Omega :equiv (lambda x . x " " x) (lambda x . x " " x) $
|
|
|
|
Cannot be type-checked in STLC, but adding recursive types allows this to be typechecked.
|
|
|
|
$ tau ::= 1 | "bool" | tau_1 arrow tau_2 | alpha | mu alpha . tau $
|
|
|
|
For example:
|
|
|
|
- $"tree" = mu alpha . 1 + ("int" times alpha times alpha)$
|
|
- $"intlist" = mu alpha . 1 + ("int" times alpha)$
|
|
|
|
$ e ::= ... | "fold"(e) | "unfold"(e) $
|
|
|
|
#tree(
|
|
axi[$Gamma tack.r e : subst(alpha, mu alpha . tau, tau)$],
|
|
uni[$Gamma tack.r "fold"(e) : mu alpha . tau $],
|
|
)
|
|
|
|
#tree(
|
|
axi[$Gamma tack.r e : mu alpha . tau $],
|
|
uni[$Gamma tack.r "unfold"(e) : subst(alpha, mu alpha . tau, tau)$],
|
|
)
|
|
|
|
*NOTE*: Fold usually needs to be annotated with $mu alpha . tau$ in order to guide type checking.
|
|
|
|
=== Type-checking $Omega$
|
|
|
|
$ Omega :equiv (lambda (x : ?) . x " " x) (lambda (x : ?) . x " " x) $
|
|
|
|
With inductive types, we can give the second $x$ some type $alpha$.
|
|
Then the first $x$ that calls it would be $alpha arrow tau$ for some $tau$.
|
|
|
|
$ "SA" : (mu alpha . alpha arrow tau) arrow tau \
|
|
"SA" :equiv lambda (x : mu alpha . alpha arrow tau) . ("unfold" x) x$
|
|
|
|
Then re-define $Omega$ to be:
|
|
|
|
$ Omega' :equiv "SA" ("fold" "SA") $
|
|
|
|
=== Proving soundness for lambda calculus with recursive types with logical relations
|
|
|
|
$ v ::= ... | "fold"(v) $
|
|
|
|
*NOTE:* Unfold will not be a value.
|
|
|
|
$ E ::= ... | "fold" E $
|
|
|
|
New reduction rule:
|
|
|
|
$ "unfold"("fold" v) mapsto v $
|
|
|
|
$V db(mu alpha . tau) = { "fold"(v) | forall v in V db(subst(alpha, mu alpha. tau, tau)) }$
|
|
|
|
This is *not* a well-founded relation, because $V$ would depend on itself. This was an open problem (ATTAPL exercise) for a long time.
|
|
|
|
==== Step Indexing
|
|
|
|
This shows that this is well founded.
|
|
|
|
"If i were to run my program for $k$ steps, then I would not be able to tell that $V$ isn't well-founded"
|
|
|
|
#rect[$V_k db(tau)$]
|
|
|
|
$V_k db("bool") = {"true" , "false"}$
|
|
|
|
$V_k db(mu alpha . tau) = {"fold" v | v in V_(k-1) db(subst(alpha , mu alpha. tau , tau))}$
|
|
|
|
- Doing $"unfold"("fold" x) mapsto x$ "consumes" a step of $k$, so that's why $v$ already consumes a step.
|
|
|
|
$V_k db(tau_1 arrow tau_2) = {lambda (x : tau_1) . e | forall (j lt.eq k, v in V_j db(tau_1)) arrow.r.double subst(x, v, e) in Epsilon_j db(tau_2)}$
|
|
|
|
- Think of this as a timeline, starting with $k$ steps left
|
|
- $j+1$ is the number of steps left when you get to the application of the lambda
|
|
- Use 1 step to do the application, resulting in $j$ steps
|
|
- Eventually reach 0 steps left.
|
|
|
|
$Epsilon_k db(tau) = { e | forall (j < k, e') arrow.r.double e op(mapsto)^j e' and "irreducible"(e') arrow.r.double e' in V_(k-j) db(tau)}$
|
|
|
|
What $k$ doesn't matter because the entire relations are universally quantified over all $k$s. |