Auto merge of #3415 - JoJoDeveloping:tree-borrows-initialized-root, r=RalfJung

Tree Borrows: Make tree root always be initialized

This PR fixes a slight annoyance we discovered while formally proving that certain optimizations are sound with Tree Borrows. In particular... (copied from the commit message):

There should never be an `Active` but not initialized node in the borrow tree. If such a node exists, and if it has a protector, then on a foreign read, it could become disabled. This leads to some problems when formally proving that read moving optimizations are sound.

The root node is the only node for which this can happen, since all other nodes can only become `Active` when actually used. But special-casing the root node here is annoying to reason about, everything becomes much nicer if we can simply say that *all* `Active` nodes must be initialized. This requires making the root node default-initialized.

This is also more intuitive, since the root arguably becomes initialized during the allocation, which can be considered a write.

0 files changed, 0 insertions, 0 deletions