add raw annotation system

chapters/4-Annotation-System.typ

@@ -1,4 +1,8 @@
 #import "../config/utils.typ": *
+#import "rules/base.typ": *
+#import "rules/relations.typ": *
+#import "rules/unification.typ": *
+#import "rules/statements.typ": *
 
 #pagebreak(to:"odd")
 = Annotation System
@@ -49,6 +53,148 @@ A unique design goal of this system is to improve the verification process with
   $
 )
 
+== General
+
+#display-rules(
+  M-Type, M-Args
+)
+
+== Context
+
+- The same variable/field cannot appear more than once in a context.
+- Contexts are always *finite*
+- If not present in the context, fields have a default annotation that is the one written in the class declaration
+
+#display-rules(
+  Not-In-Base, Not-In-Rec,
+  Ctx-Base, Ctx-Rec,
+  Root-Base, Root-Rec,
+  Lookup-Base, Lookup-Rec,
+  Lookup-Default, "",
+  Remove-Empty, Remove-Base,
+  Remove-Rec, "",
+)
+
+== SubPaths
+
+If $p_1 subset.sq p_2$ holds, we say that 
+- $p_1$ is a *sub*-path of $p_2$
+- $p_2$ is a *sup*-path of $p_1$
+
+#display-rules(
+  SubPath-Base, SubPath-Rec,
+  SubPath-Eq-1, SubPath-Eq-2,
+  Remove-SupPathsEq-Empty, Remove-SupPathsEq-Discard,
+  Remove-SupPathsEq-Keep, Replace,
+  Get-SupPaths-Empty, "",
+  Get-SupPaths-Discard, "",
+  Get-SupPaths-Keep, "",
+)
+
+== Annotations relations
+
+- $alpha beta rel alpha' beta'$ means that $alpha beta$ can be passed where $alpha' beta'$ is expected.
+
+- $alpha beta ~> alpha' beta' ~> alpha'' beta''$ means that after passing a reference annotated with $alpha beta$ as argument where $alpha' beta'$ is expected, the reference will be annotated with $alpha'' beta''$ right after the method call.
+
+#display-rules(
+  row-size: 3,
+  A-id, A-trans, A-bor-sh,
+  A-sh, A-bor-un, A-un-1,
+  A-un-2, Pass-Bor, Pass-Un,
+  Pass-Sh
+)
+
+#figure(image(width: 25%, "../images/lattice.svg"), caption: [Lattice obtained by annotations relations rules])<annotation-lattice>
+
+== Paths
+<cap:paths>
+
+- $Lub{alpha_0 beta_0, ..., alpha_n beta_n}$ identifies the least upper bound of the annotations based on the lattice in @annotation-lattice.
+- Note that even if $p.f$ is annotated as unique in the class declaration, $Delta(p.f)$ can be shared (or $top$) if $Delta(p) = shared$ (or $top$)
+- Note that fields of a borrowed parameter are borrowed too and they need to be treated carefully in order to avoid unsoundness. Specifically, borrowed fields:
+  - Can be passed as arguments to other functions (if relation rules are respected).
+  - Have to become `T` after being read (even if shared).
+  - Can only be reassigned with a `unique`.
+- Note that $(Delta(p) = alpha beta) => (Delta inangle(root(p)) = alpha' beta')$ i.e. the root is present in the context.
+- $Delta tr std(p, alpha beta)$ means that paths rooted in $p$ have the right permissions when passing $p$ where $alpha beta$ is expected. To understand better why these rules are necessary look at the example in /*@path-permissions*/.
+- Note that in the rule "Std-Rec-2" the premise $(x : alpha beta) (p') = alpha'' beta''$ means that the evaluation of $p'$ in a context in which there is only $x : alpha beta$ is $alpha'' beta''$
+
+#display-rules(
+  Get-Var, Get-Path,
+  Std-Empty, Std-Rec-1,
+  Std-Rec-2, "",
+)
+
+== Unification
+
+- $Delta_1 lub Delta_2$ is the pointwise lub of $Delta_1$ and $Delta_2$.
+  - If a variable $x$ is present in only one context, it will be annotated with $top$ in $Delta_1 lub Delta_2$.
+  - If a path $p.f$ is missing in one of the two contexts, we can just consider the annotation in the class declaration.
+- $Delta triangle.filled.small.l Delta_1$ is used to maintain the correct context when exiting a scope.
+  - $Delta$ represents the resulting context of the inner scope.
+  - $Delta_1$ represents the context at the beginning of the scope.
+  - The result of the operation is a context where paths rooted in variable locally declared inside the scope are removed.
+- $unify(Delta, Delta_1, Delta_2)$ means that we want to unify $Delta_1$ and $Delta_2$ starting from a parent environment $Delta$.
+  - A path $p$ contained in $Delta_1$ or $Delta_2$ such that $root(p) = x$ is not contained $Delta$ will not be included in the unfication.
+  - The annotation of variables contained in the unfication is the least upper bound of the annotation in $Delta_1$ and $Delta_2$.
+
+#display-rules(
+  // U-Empty, U-Sym,
+  // U-Local, U-Rec,
+  Ctx-Lub-Empty, Ctx-Lub-Sym,
+  Ctx-Lub-1, "",
+  Ctx-Lub-2, "",
+  Ctx-Lub-3, "",
+  Remove-Locals-Base, Remove-Locals-Keep,
+  Remove-Locals-Discard, "",
+  Unify, ""
+)
+
+== Normalization
+
+- Normalization takes a list of annotated $p$ and retruns a list in which duplicates are substituted with the least upper bound.
+- Normalization is required for method calls in which the same variable is passed more than once.
+
+```kt
+fun f(x: ♭ shared, y: shared)
+fun use_f(x: unique) {
+  // Δ = x: unique
+  f(x, x)
+  // Δ = normalize(x: unique, x:shared) = x: shared
+}
+```
+
+#display-rules(
+  N-Empty, "",
+  N-Rec, ""
+)
+
+== Statements
+
+#display-rules(
+  Begin, "",
+  Decl, Assign-Null,
+  Seq-Base, Seq-Rec,
+  If, "",
+  Assign-Unique, "",
+  Assign-Shared, "",
+  Assign-Borrowed-Field, "",
+  Assign-Call, "",
+  Call, "",
+  // Return-Null, "",
+  Return-p, "",
+  // Return-m, "",
+)
+
+*Note:* Since they can be easily desugared, there are no rules for returnning `null` or a method call.
+- `return null` $equiv$ `var fresh ; fresh = null ; return fresh`
+- `return m(...)` $equiv$ `var fresh ; fresh = m(...) ; return fresh`
+
+The same can be done for the guard of if statements:
+- `if (p1 == null) ...` $equiv$ `var p2 ; p2 = null ; if(p1 == p2) ...`
+- `if (p1 == m(...)) ...` $equiv$ `var p2 ; p2 = m(...) ; if(p1 == p2) ...`
+
 // TODO: put this in a separate chapter
 
 // == Aliasing control in Kotlin

chapters/rules/base.typ

@@ -0,0 +1,180 @@
+#import "../../config/proof-tree.typ": *
+#import "../../config/utils.typ": *
+
+// ****************** General ******************
+
+#let M-Type = prooftree(
+  axiom($m(alpha_0 beta_0 x_0, ..., alpha_n beta_n x_n): alpha {begin_m; overline(s); ret_m e}$),
+  rule(label: "M-Type", $mtype(m) = alpha_0 beta_0, ..., alpha_n beta_n -> alpha$),
+)
+
+#let M-Args = prooftree(
+  axiom($m(alpha_0 beta_0 x_0, ..., alpha_n beta_n x_n): alpha {begin_m; overline(s); ret_m e}$),
+  rule(label: "M-Args", $args(m) = x_0, ..., x_n$),
+)
+
+// ****************** Context ******************
+
+#let Not-In-Base = prooftree(
+  axiom(""),
+  rule(label: "Not-In-Base", $p in.not dot$),
+)
+
+#let Not-In-Rec = prooftree(
+  axiom($p != p'$),
+  axiom($p in.not Delta$),
+  rule(n:2, label: "Not-In-Rec", $p in.not (p' : alpha beta, Delta)$),
+)
+
+#let Root-Base = prooftree(
+  axiom(""),
+  rule(label: "Root-Base", $root(x) = x$),
+)
+
+#let Root-Rec = prooftree(
+  axiom($root(p) = x$),
+  rule(label: "Root-Rec", $root(p.f) = x$),
+)
+
+#let Ctx-Base = prooftree(
+  axiom(""),
+  rule(label: "Ctx-Base", $dot ctx$),
+)
+
+#let Ctx-Rec = prooftree(
+  axiom($Delta ctx$),
+  axiom($p in.not Delta$),
+  rule(n:2, label: "Ctx-Rec", $p: alpha beta, Delta ctx$),
+)
+
+#let Lookup-Base = prooftree(
+  axiom($(p: alpha beta, Delta) ctx$),
+  rule(label: "Lookup-Base", $(p: alpha beta, Delta) inangle(p) = alpha beta$),
+)
+
+#let Lookup-Rec = prooftree(
+  axiom($(p: alpha beta, Delta) ctx$),
+  axiom($p != p'$),
+  axiom($Delta inangle(p') = alpha' beta'$),
+  rule(n:3, label: "Lookup-Rec", $(p: alpha beta, Delta) inangle(p') = alpha' beta'$),
+)
+
+#let Lookup-Default = prooftree(
+  axiom($type(p) = C$),
+  axiom($class C(overline(f': alpha'_f), f: alpha, overline(f'': alpha''_f))$),
+  rule(n:2, label: "Lookup-Default", $dot inangle(p.f) = alpha$),
+)
+
+// #let In = prooftree(
+//   axiom($root(p) = x$),
+//   axiom($Delta inangle(x) = alpha beta$),
+//   rule(n:2, label: "In", $p in Delta$),
+// )
+
+#let Remove-Empty = prooftree(
+  axiom(""),
+  rule(label: "Remove-Empty", $dot without p = dot$),
+)
+
+#let Remove-Base = prooftree(
+  axiom(""),
+  rule(label: "Remove-Base", $(p: alpha beta, Delta) without p = Delta$),
+)
+
+#let Remove-Rec = prooftree(
+  axiom($Delta without p = Delta'$),
+  axiom($p != p'$),
+  rule(n:2, label: "Remove-Rec", $(p': alpha beta, Delta) without p = p': alpha beta, Delta'$),
+)
+
+#let SubPath-Base = prooftree(
+  axiom(""),
+  rule(label: "SubPath-Base", $p subset.sq p.f$),
+)
+
+#let SubPath-Rec = prooftree(
+  axiom($p subset.sq p'$),
+  rule(label: "SubPath-Rec", $p subset.sq p'.f$),
+)
+
+#let SubPath-Eq-1 = prooftree(
+  axiom($p = p'$),
+  rule(label: "SubPath-Eq-1", $p subset.sq.eq p'$),
+)
+
+#let SubPath-Eq-2 = prooftree(
+  axiom($p subset.sq p'$),
+  rule(label: "SubPath-Eq-2", $p subset.sq.eq p'$),
+)
+
+#let Remove-SupPathsEq-Empty = prooftree(
+  axiom(""),
+  rule(label: "Remove-SupPathsEq-Empty", $dot minus.circle p = dot$),
+)
+
+#let Remove-SupPathsEq-Discard = prooftree(
+  axiom($p subset.sq.eq p'$),
+  axiom($Delta minus.circle p = Delta'$),
+  rule(n:2, label: "Remove-SupPathsEq-Discard", $(p': alpha beta, Delta) minus.circle p = Delta'$),
+)
+
+#let Remove-SupPathsEq-Keep = prooftree(
+  axiom($p subset.not.sq.eq p'$),
+  axiom($Delta minus.circle p = Delta'$),
+  rule(n:2, label: "Remove-SupPathsEq-Keep", $(p': alpha beta, Delta) minus.circle p = (p': alpha beta, Delta')$),
+)
+
+#let Replace = prooftree(
+  axiom($Delta minus.circle p = Delta'$),
+  rule(label: "Replace", $Delta[p |-> alpha beta] = Delta', p: alpha beta$),
+)
+
+#let Get-SupPaths-Empty = prooftree(
+  axiom(""),
+  rule(label: "Get-SupPaths-Empty", $dot tr sp(p) = dot$),
+)
+
+#let Get-SupPaths-Discard = prooftree(
+  axiom($not (p subset.sq p')$),
+  axiom($Delta tr sp(p) = p_0 : alpha_0 beta_0, ..., p_n : alpha_n beta_n$),
+  rule(n: 2, label: "Get-SupPaths-Discard", $p': alpha beta, Delta tr sp(p) = p_0 : alpha_0 beta_0, ..., p_n : alpha_n beta_n$),
+)
+
+#let Get-SupPaths-Keep = prooftree(
+  axiom($p subset.sq p'$),
+  axiom($Delta tr sp(p) = p_0 : alpha_0 beta_0, ..., p_n : alpha_n beta_n$),
+  rule(n: 2, label: "Get-SupPaths-Keep", $p': alpha beta, Delta tr sp(p) = p': alpha beta, p_0 : alpha_0 beta_0, ..., p_n : alpha_n beta_n$),
+)
+
+// ************ Get ************
+
+#let Get-Var = prooftree(
+  axiom($Delta inangle(x) = alpha beta$),
+  rule(label: "Get-Var", $Delta(x) = alpha beta$)
+)
+
+#let Get-Path = prooftree(
+  axiom($Delta(p) = alpha beta$),
+  axiom($Delta inangle(p.f) = alpha'$),
+  rule(n: 2, label: "Get-Path", $Delta(p.f) = Lub{alpha beta, alpha'}$)
+)
+
+#let Std-Empty = prooftree(
+  axiom(""),
+  rule(label: "Std-Empty", $dot tr std(p, alpha beta)$),
+)
+
+#let Std-Rec-1 = prooftree(
+  axiom($not (p subset.sq p')$),
+  axiom($Delta tr std(p, alpha beta)$),
+  rule(n:2, label: "Std-Rec-1", $p' : alpha beta, Delta tr std(p, alpha beta)$),
+)
+
+#let Std-Rec-2 = prooftree(
+  axiom($p subset.sq p'$),
+  axiom($root(p) = x$),
+  axiom($(x : alpha beta) (p') = alpha'' beta''$),
+  axiom($alpha' beta' rel alpha'' beta''$),
+  axiom($Delta tr std(p, alpha beta)$),
+  rule(n:5, label: "Std-Rec-2", $p' : alpha' beta', Delta tr std(p, alpha beta)$),
+)

chapters/rules/relations.typ

@@ -0,0 +1,57 @@
+#import "../../config/proof-tree.typ": *
+#import "../../config/utils.typ": *
+
+// ************** Annotations Relations **************
+
+#let A-id = prooftree(
+  axiom($$),
+  rule(label: "A-Id", $alpha beta rel alpha beta$),
+)
+
+#let A-trans = prooftree(
+  axiom($alpha beta rel alpha' beta'$),
+  axiom($alpha' beta' rel alpha'' beta''$),
+  rule(n:2, label: "A-Trans", $alpha beta rel alpha'' beta''$),
+)
+
+#let A-bor-sh = prooftree(
+  axiom($$),
+  rule(label: "A-Bor-Sh", $shared borrowed rel top$),
+)
+
+#let A-sh = prooftree(
+  axiom($$),
+  rule(label: "A-Sh", $shared rel shared borrowed$),
+)
+
+#let A-bor-un = prooftree(
+  axiom($$),
+  rule(label: "A-Bor-Un", $unique borrowed rel shared borrowed$),
+)
+
+#let A-un-1 = prooftree(
+  axiom($$),
+  rule(label: "A-Un-1", $unique rel shared$),
+)
+
+#let A-un-2 = prooftree(
+  axiom($$),
+  rule(label: "A-Un-2", $unique rel unique borrowed$),
+)
+
+// ************** Parameters Passing **************
+
+#let Pass-Bor = prooftree(
+  axiom($alpha beta rel alpha' borrowed$),
+  rule(label: "Pass-Bor", $alpha beta ~> alpha' borrowed ~> alpha beta$)
+)
+
+#let Pass-Un = prooftree(
+  axiom($$),
+  rule(label: "Pass-Un", $unique ~> unique ~> top$)
+)
+
+#let Pass-Sh = prooftree(
+  axiom($alpha rel shared$),
+  rule(label: "Pass-Sh", $alpha ~> shared ~> shared$)
+)