250 lines
6.9 KiB
Plaintext
250 lines
6.9 KiB
Plaintext
#import "@preview/prooftrees:0.1.0": *
|
|
#set page(width: 5in, height: 8in, margin: 0.4in)
|
|
|
|
#let ifthenelse(e, e1, e2) = $"if" #e "then" #e1 "else" #e2$
|
|
#let subst(x, v, e) = $#e [#v\/#x]$
|
|
#let isValue(x) = $#x "value"$
|
|
#let mapstostar = $op(arrow.r.long.bar)^*$
|
|
#let safe = $"safe"$
|
|
#let db(x) = $bracket.l.double #x bracket.r.double$
|
|
#let TODO = text(fill: red)[*TODO*]
|
|
|
|
= Mon. Jun 3 \@ 14:00
|
|
|
|
== 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
|
|
|
|
#let mapsto = $arrow.r.long.bar$
|
|
|
|
#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. |