simple formalization for most important nodes

src/CFG-based-system.typ

@@ -1,3 +1,5 @@
+#import "./proof-tree.typ": *
+#import "./vars.typ": *
 = CFG Based System
 
 Basic rules for Uniqueness and Borrowing won't change here,
@@ -7,6 +9,43 @@ The key gap between the CFG version and the type rules is at the function call.
 Type checking at function calls need adjustment so that it can be done in control flow order.
 The support for recursive function all is alse missing is previous typing rules.
 
+== Formalization
+
+We follow the original lattice for control flow analysis.
+#figure(image(width: 25%, "./img/lattice.svg"), caption: [Lattice in Control Flow Analysis])<CFA-lattice>
+
+The context for CFA $Gamma$ is defined as: a mapping from path to the lattice:
+$ Gamma : p -> U $, $U$ for uniqueness and borrowing level.
+
+In Kotlin CFG, $"$"i = "eval" e$, is a common pattern that appears everywhere, we distinguish this case with assignment statement when rhs is a path: define context $Delta$ for case $"$"i = "eval" p$ temp variables to the corresponding path and lattice, to make it simple here, we define it as a list:
+$ Delta : (i, p, U) $
+When the rhs is not a variable or path, we store $(i, *, U)$.
+
+Rule for CFA are as follows on different nodes in CFG:
+#prooftree(
+  axiom($Delta'= (i, p, Gamma(p)) :: Delta$),
+  rule(label: "Temp assignment path", $Gamma, Delta tack.r "$"i := p tack.l Gamma, Delta'$),
+)
+
+#prooftree(
+  axiom($Delta'= (i*, "Eval"(f)) :: Delta$),
+  rule(label: "Temp assignment non-path", $Gamma, Delta tack.r "$"i := f tack.l Gamma, Delta'$),
+)
+
+#prooftree(
+  axiom($Delta("$"i).3 <= "U"i$),
+  axiom("Do normalization with alias infomation in Delta"),
+  rule(n: 2, label: "Function call", $Gamma, Delta tack.r f("$"1: "U"1, ..., "$"n: "U"n) tack.l Gamma', Delta$),
+)
+
+#prooftree(
+  axiom($"Unification "Gamma_1, Gamma_2$),
+  axiom($Delta'= ("result", ("$"1, "$"2), Gamma("$"1) lub Gamma("$"2)) :: Delta$),
+  rule(n:2, label: "CFG Join Node for Expression(if/when)", $Gamma_1, Delta_1 tack.r "$result" := "$2" join Gamma_2, Delta_2 tack.r "$result" := "$2" tack.l Gamma', Delta'$),
+)
+
+Here $("$"1, "$"2)$ means we keep both alias, when one of them is $*$, we keep the other one.
+
 == Examples for recursive function call
 - Example with multiple call with unique
 ```kt