Tree Borrows update

Big Tree Borrows update.

The read-read reordering proofs against the sequential semantics now live in their own folder. (see: theories/tree_borrows/read_read_reorder/README.md)

Some examples from the paper now have their own proof, notably examples/protected/shared_insert_read.v and examples/protected/mutable_reorder_write_up_activated_paper.v.

Removed spurious header comments about how "This file has been adapted from the Stacked Borrows development". At that point the files have gone through SB -> SB+simuliris -> TB and several refactoring rounds. They are no longer recognizable and it makes no sense to keep this reference.

Outdated FIXMEs have been removed. Outdated comments in general too, including still some references to nonatomics, field accesses, syscalls, bitwise operators, etc. that have not been relevant for a long time (even before we started TB, these were already commented out in SB).

Expanded on theories/tree_borrows/README.md

Sizeable effort to document and comment the TCB and the WF invariants.

Got rid of poison semantics for failed reads.