refine tree-borrows.md, fixing typos etc.

Author: JoJoDeveloping

wip/tree-borrows.md

@@ -7,13 +7,13 @@ This is not a guide! See the [Tree Borrows paper](https://plf.inf.ethz.ch/resear
 Changes since publication of the paper:
 
 * Interior-Mutable shared references are no longer treated like raw pointers, instead they use the new `Cell` permission. This permission allows all foreign and local accesses.
-* Mirroring Stacked Borrows, structs which contain an UnsafeCell now have that UnsafeCell's position tracked more finely-grained. It is no longer sufficient to just have an UnsafeCell somewhere in a struct to mark this as being interior-mutable everyhwere.
+* Mirroring Stacked Borrows, structs which contain an UnsafeCell now have that UnsafeCell's position tracked more finely-grained. It is no longer sufficient to just have an UnsafeCell somewhere in a struct to mark this as being interior-mutable everywhere.
 
 ## MiniRust
 
-Tree Borrows is documented in [MiniRust](https://github.com/minirust/minirust/tree/master/spec/mem/tree_borrows). MiniRust is written as literate code and should be readable without further explanation. 
+Tree Borrows is fully documented in [MiniRust](https://github.com/minirust/minirust/tree/master/spec/mem/tree_borrows). MiniRust is written as literate code and should be readable without further explanation. The MiniRust version of Tree Borrows is the authoritative version, and it will be updated to reflect future changes. MiniRust defines all of Tree Borrows, including the more obscure features.
 
-Instead of yet again defining Tree Borrows in prose here, we refer to this.
+Instead of yet again defining Tree Borrows in prose here, we refer to MiniRust. The information below is not normative and only a summary of what is already explained in MiniRust.
 
 
 ### High-level summary
@@ -26,27 +26,29 @@ These differences are not reflected in the state machines in the paper, we refer
 
 
 ### Differences between MiniRust and Miri
-MiniRust includes an idealized implementation of Tree Borrows. In particular, it models provenance/tags as tree addresses, which uniquely identify a node in the borrow tree. Miri however uses unique IDs, with the Tree being tracked more implicitly has relations between these IDs. This is an implementation detail and not relevant for understanding the semantics.
+MiniRust includes an idealized implementation of Tree Borrows, intended for easy readability.
+ In particular, it models provenance/tags as tree addresses, which uniquely identify a node in the borrow tree. Miri however uses unique integer IDs, with the Tree being tracked more implicitly as maps/relations between these nodes. The precise implementation of the tree is an implementation detail and not relevant for the semantics.
+
 Besides this representation difference, Miri also includes a number of optimizations that make Tree Borrows have acceptable performance. These include
 * skipping nodes based on past foreign accesses, exploiting idempotence properties in the state machine
 * garbage collection of unused references, which allows shrinking trees
-* skipping nodes based on the permissions found there
+* skipping nodes based on the permissions found therein
 
 ## Concepts Inherited From Stacked Borrows
 
 ### Retags
 Tree Borrows has retags happen in the same place as Stacked Borrows. But note that Tree Borrows treats raw pointer retags as NOPs, i.e. it does not attempt to track these.
 
 ### Protectors
-Like Stacked Borrows, Tree Borrows has protectors. These serve to ensure that references remain live throughout a function. Like Stacked Borrows, Tree Borrows has strong and weak protectors, and it protects the same values the same way.
+Like Stacked Borrows, Tree Borrows has protectors. These serve to ensure that references remain live throughout a function. Protectors are strong and weak, as in SB, and they protect the same places in the same way.
 
 ### Implicit Reads and Writes
 Like Stacked Borrows, Tree Borrows performs implicit accesses as part of retags. Unlike Stacked Borrows, these are always reads, even for `&mut` references.
 
-Also unlike Stacked Borrows, Tree Borrows has implicit accesses happen on protector end. These can be writes. See the section on "protector end semantics" in the paper for more info.
+A new concept in TB are protector end accesses. These can be writes. See the section on "protector end semantics" in the paper for more info.
 
 ### UnsafeCell tracking
-Like Stacked Borrows, Tree Borrows tracks where there are UnsafeCells, and treats these offsets differently from other offsets. UnsafeCells are tracked in structs and tuple fields, but enums are not inspected further.
+Like Stacked Borrows, Tree Borrows tracks where there are UnsafeCells, and treats these bytes differently from other bytes. UnsafeCells are tracked in structs and tuple fields, but enums are not inspected further.
 
 ### Accesses
 Besides for the aforementioned differences in the handling of retags, what counted as a read or write in Stacked Borrows also counts as a read or write in Tree Borrows. These places are not surprising.
@@ -60,4 +62,4 @@ The following is a list of things that are _not_ UB in Tree Borrows. Some people
 
 ## Other problems
 * The interaction of protector end writes with the data race model is not fully thought out.
-* Finding a good model of exposed provenance in Tree Borrows (that does not use angelic nondeterminism) is an open research question. Until then, Tree Borrows does not support `-Zmiri-permissive-provenance`
+* Finding a good model of exposed provenance in Tree Borrows (that does not use angelic nondeterminism) is an open research question. Until then, Tree Borrows does not support `-Zmiri-permissive-provenance`.