Add function call encoding

chapters/6-Encoding.typ

@@ -72,20 +72,34 @@ Encoding the receiver of a method is straightforward since the receiver is consi
 - black-box Function
 - edge cases not supported at the moment
 
+== Predicates Unfolding<cap:unfolding>
+
+- easy for shared
+- inhaling -> only if there are no way to access the predicate
+- design choices for unique
+- EXAMPLES
+
 == Function Calls Encoding
 
-#figure(
-  caption: "TODO",
-  image("../images/calls-graph.svg", width: 60%)
-)
+Encoding method calls is straightforward for some cases, but requires attention for some others.
 
-- explain the call graph
+=== Functions with unique parameters
 
-- EXAMPLES
+Functions with a unique parameter, when called, do not need the inclusion of additional statements for their encoding, except for folding or unfolding statements, as detailed in @cap:unfolding.
 
-== Predicates Unfolding
+#code-compare("Function call with unique parameter encoding", .8fr, unique-call-kt, unique-call-vpr)
 
-- easy for shared
-- inhaling -> only if there are no way to access the predicate
-- design choices for unique
-- EXAMPLES
+=== Functions with shared parameters
+
+When functions with a shared parameter are called, their encoding may require the addition of `inhale` and `exhale` statements. The annotation system allows functions with shared parameters to be called by passing unique references. However, the function's conditions alone are not sufficient to properly encode these calls.
+
+For example, passing a unique reference to a function expecting a shared (non-borrowed) parameter will result in the loss of uniqueness for that reference, which is encoded by exhaling the unique predicate. Similarly, when a unique reference is passed to a function expecting a borrowed-shared parameter, the uniqueness is preserved, but any field of that reference can be modified. This is encoded by exhaling and then re-inhaling the unique predicate of that reference.
+
+@call-graph summarizes the `inhale` and `exhale` statements added during the encoding of a function call.
+
+#figure(
+  caption: "Extra statements added for functions call encoding",
+  image("../images/calls-graph.svg", width: 60%)
+)<call-graph>
+
+#code-compare("Function call with shared parameter encoding", .8fr, shared-call-kt, shared-call-vpr)

vars/kt-to-vpr-examples.typ

@@ -204,4 +204,85 @@ requires acc(SharedT(this), wildcard)
 requires acc(UniqueT(this), write)
 ensures acc(SharedT(this), wildcard)
 ensures acc(UniqueT(this), write)
+```
+
+#let unique-call-kt = ```kt
+fun uniqueParam(
+    @Unique t: T
+) {
+}
+
+fun uniqueBorrowedParam(
+    @Unique @Borrowed t: T
+) {
+}
+
+fun call(
+    @Unique @Borrowed t1: T,
+    @Unique t2: T
+) {
+    uniqueBorrowedParam(t1)
+    uniqueBorrowedParam(t2)
+    uniqueParam(t2)
+}
+```
+
+#let unique-call-vpr = ```java
+method uniqueParam(t: Ref)
+requires acc(UniqueT(t), write) && acc(SharedT(t), wildcard)
+ensures acc(SharedT(t), wildcard)
+
+method uniqueBorrowedParam(t: Ref)
+requires acc(UniqueT(t), write) && acc(SharedT(t), wildcard)
+ensures acc(UniqueT(t), write) && acc(SharedT(t), wildcard)
+
+method call(t1: Ref, t2: Ref)
+requires acc(UniqueT(t1), write) && acc(SharedT(t1), wildcard)
+requires acc(UniqueT(t2), write) && acc(SharedT(t2), wildcard)
+ensures acc(UniqueT(t1), write) && acc(SharedT(t1), wildcard)
+ensures acc(SharedT(t2), wildcard)
+{
+  uniqueBorrowedParam(t1)
+  uniqueBorrowedParam(t2)
+  uniqueParam(t2)
+}
+```
+
+#let shared-call-kt = ```kt
+fun sharedParam(
+    t: T
+) {
+}
+
+fun sharedBorrowedParam(
+    @Borrowed t: T
+) {
+}
+
+fun call(@Unique t: T) {
+    sharedBorrowedParam(t)
+    sharedParam(t)
+}
+```
+
+#let shared-call-vpr = ```java
+method sharedParam(t: Ref)
+requires acc(SharedT(t), wildcard)
+ensures acc(SharedT(t), wildcard)
+
+method sharedBorrowedParam(t: Ref)
+requires acc(SharedT(t), wildcard)
+ensures acc(SharedT(t), wildcard)
+
+method call(t: Ref)
+requires acc(UniqueT(t), write) && acc(SharedT(t), wildcard)
+ensures acc(SharedT(t), wildcard)
+{
+  exhale acc(UniqueT(t), write)
+  inhale acc(UniqueT(t), write)
+  sharedBorrowedParam(t)
+
+  exhale acc(UniqueT(t), write)
+  sharedParam(t)
+}
 ```