recursive descend will come later

[web.git] / ralf / _drafts / stacked-borrows-implementation.md

diff --git a/ralf/_drafts/stacked-borrows-implementation.md b/ralf/_drafts/stacked-borrows-implementation.md
index 17c8d27c4be198149808f696d5618ea7750650cf..e5dae22eb914a79dd40f21d067668c7c34720375 100644 (file)
--- a/ralf/_drafts/stacked-borrows-implementation.md
+++ b/ralf/_drafts/stacked-borrows-implementation.md
@@ -33,8 +33,10 @@ changed a bit, but also because I think I understand the model better myself
 now.
 
 Ready?  Let's get started.  I hope you brought some time, because this is a
 now.
 
 Ready?  Let's get started.  I hope you brought some time, because this is a

-rather lengthy post.  If you are not interested in the details, you can skip
-right to section 4.  If you only want to know how to help, go to section 6.
+rather lengthy post.  If you are not interested in a detailed description of
+Stacked Borrows, you can skip most of this post and go right to
+[section 4](#4-differences-to-the-original-proposal).  If you only want to know
+how to help, jump to [section 6](#6-evaluation-and-how-you-can-help).

 
 ## 1 Enforcing Uniqueness
 
 
 ## 1 Enforcing Uniqueness
 


@@ -437,8 +439,10 @@ references are copied: At the beginning of every function, all inputs of
 reference type get retagged.  On every assignment, if the assigned value is of
 reference type, it gets retagged.  Moreover, we do this even when the reference
 value is inside the field of a `struct` or `enum`, to make sure we really cover
 reference type get retagged.  On every assignment, if the assigned value is of
 reference type, it gets retagged.  Moreover, we do this even when the reference
 value is inside the field of a `struct` or `enum`, to make sure we really cover

-all references.  However, we do *not* descend recursively through references:
-Retagging a `&mut &mut u8` will only retag the *outer* reference.
+all references.  (This recursive descend is already implemented, but the
+implementation has not landed yet.)  However, we do *not* descend recursively
+through references: Retagging a `&mut &mut u8` will only retag the *outer*
+reference.

 
 Retagging is the *only* operation that generates fresh tags.  Taking a reference
 simply forwards the tag of the pointer we are basing this reference on.
 
 Retagging is the *only* operation that generates fresh tags.  Taking a reference
 simply forwards the tag of the pointer we are basing this reference on.


@@ -782,7 +786,7 @@ implement in miri because dereferences can happen any time a path is evaluated,
 but it is nevertheless interesting and might be useful in a "lower-level MIR"
 that does not permit dereferences in paths.
 
 but it is nevertheless interesting and might be useful in a "lower-level MIR"
 that does not permit dereferences in paths.
 

-## Evaluation, and How You Can Help
+## 6 Evaluation, and How You Can Help

 
 I have implemented both the validity invariant and the model as described above
 in miri. This [uncovered](https://github.com/rust-lang/rust/issues/54908) two
 
 I have implemented both the validity invariant and the model as described above
 in miri. This [uncovered](https://github.com/rust-lang/rust/issues/54908) two