#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$

= 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'')$

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)}
$

#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.
]