Add a comment for PrePasses.remove_shallow_borrows

1 files changed, 87 insertions, 2 deletions

diff --git a/compiler/PrePasses.ml b/compiler/PrePasses.ml
index a0c01384..8b193ee2 100644
--- a/compiler/PrePasses.ml
+++ b/compiler/PrePasses.ml
@@ -267,9 +267,94 @@ let remove_loop_breaks (crate : A.crate) (f : A.fun_decl) : A.fun_decl =
 
     In practice, this is not a soundness issue.
 
+    **Soundness**:
+    ==============
+    For instance, let's consider the following Rust code:
+    {[
+      match ls : &mut List<u32> {
+        Nil => return None,
+        Cons(hd, tl) if *hd > 0 => return Some(hd),
+        Cons(hd, tl) => ...,
+      }
+    ]}
+
+    The Rust compiler enforces the fact that the guard doesn't modify the
+    variant of [ls]. It does so by compiling to (approximately) the following
+    MIR code:
+    {[
+      let d = discriminant( *ls);
+      switch d {
+        0 => ... // Nil case
+        1 => { // Cons case
+          // Introduce hd and tl
+          hd := &mut ( *ls as Cons).0;
+          tl := &mut ( *ls as Cons).1;
+
+          // Evaluate the guard
+          tmp := &shallow *ls; // Create a shallow borrow of ls
+          b := *hd > 0;
+          fake_read(tmp); // Make sure the shallow borrow lives until the end of the guard
+
+          // We evaluated the guard: go to the proper branch
+          if b then {
+            ... // First Cons branch
+          }
+          else {
+            ... // Second Cons branch
+          }
+        }
+      }
+    ]}
+
+    Shallow borrows are a bit like shared borrows but with the following
+    difference:
+    - they do forbid modifying the value directly below the loan
+    - but they allow modifying a strict subvalue
+    For instance, above, for as long as [tmp] lives:
+    - we can't change the variant of [*ls]
+    - but we can update [hd] and [tl]
+
+    On our side, we have to pay attention to two things:
+    - Removing shallow borrows don't modify the behavior of the program.
+      In practice, adding shallow borrows can lead to a MIR program being
+      rejected, but it doesn't change this program's behavior.
+
+      Regarding this, there is something important. At the top-level AST,
+      if the guard modifies the variant (say, to [Nil]) and evaluates to [false],
+      then we go to the second [Cons] branch, which doesn't really make sense
+      (though it is not a soundness issue - for soundness, see next point).
+
+      At the level of MIR, as the match has been desugared, there is no issue
+      in modifying the variant of the scrutinee.
+
+    - We have to make sure the evaluation in sound. In particular, modifying
+      the variant of [*ls] should invalidate [hd] and [tl]. This is important
+      for the Rust compiler to enforce this on its side. In the case of LLBC,
+      we don't need additional constraints because modifying [*ls] will
+      indeed invalidate [hd] and [tl].
+
+      More specifically, at the beginning of the [Cons] branch and just after
+      we introduced [hd] and [tl] we have the following environment:
+      {[
+        ... // l0 comes from somewhere - we omit the corresponding loan
+        ls -> MB l0 (Cons (ML l1) (ML l2))
+        hd -> MB l1 s1
+        tl -> MB l2 s2
+      ]}
+
+      If we evaluate: [*ls := Nil], we get:
+      {[
+        ... // l0 comes from somewhere - we omit the corresponding loan
+        ls -> MB l0 Nil
+        hd -> ⊥ // invalidated
+        tl -> ⊥ // invalidated
+      ]}
+
+    **Implementation**:
+    ===================
     The pass is implemented as follows:
-    - we look for all the variables which appear in pattern of the form and
-      remove them:
+    - we look for all the variables which appear in pattern of the following
+      shape and remove them:
       {[
         let x = &shallow ...;
         ...