diff --git a/theories/tree_borrows/README.md b/theories/tree_borrows/README.md
index 83d9d1ddde5bb1a7ec5eeb55bd671f5724e1b862..3b57584d544fe80fa4610f674a424252d1dac59e 100644
--- a/theories/tree_borrows/README.md
+++ b/theories/tree_borrows/README.md
@@ -53,6 +53,49 @@ In addition, `read_read_reorder/` provides proofs of simple reorderings
 directly against the operational semantics.
 You can find more details in the associated `README.md`.
 
+## Correspondence with Sections 2 and 3
+
+Here, we describe how we formalized the semantics of Tree Borrows described in the paper.
+We start with the formalization of trees given in `tree.v`, which defines n-ary trees where each node is indexed by an integer, called a `tag`.
+
+Next, `lang_base.v` defines the type of permission, notably defining `Inductive permission` in line 83, which corresponds to the states of the state machine.
+Like in Miri, we actually have two kinds of protectors (line 113), with `ProtStrong` corresponding to regular protectors and `ProtWeak` not being used in the paper.
+(It is used to model `Box` aliasing rules, something not touched upon in the paper and also something that might be removed in future versions of Rust.)
+
+Next, `bor_semantics.v` defines the main Tree Borrows semantics.
+In line 224-291, we define the notions of "relatedness" in a tree (parent/child/local/foreign etc.).
+This culminates in `rel_dec`, which decides the relation between two tags in a tree.
+
+The main state machine is defined in line 340, the function `apply_access_perm_inner`.
+This depends on the access kind (read/write), the relatedness (foreign/local) and on whether the current node is protected.
+It returns the new permission, or `None` which indicates UB.
+
+This is used in `apply_access_perm`, which also tracks "initialization" which is part of lazy range detection.
+It is used to cause UB when a protected, already locally accessed node becomes disabled.
+Compare to the description around line 545 in the paper.
+
+The function `item_apply_access` lifts this from one permission to a tree item, which contains the entire range, accounting for every offset in a block in the block-based memory model.
+Then, `tree_apply_access` lifts this to an entire tree, and `trees_apply_access` lifts it to the entire memory.
+
+The function `memory_deallocate` ensures that no deallocation happens while a protector exists. This is not described in the paper, but this behavior is inherited from Stacked Borrows.
+It is also present in the Miri implementation.
+
+After some basic proofs about the definitions, we contine in line 780 with the definition of retags.
+A retag is the core operation creating a new reference, which is parameterized by a "pointer kind" defining if this is to be a shared/mutable reference with(out) interior mutability.
+Further it defines whether there are to be protectors.
+The function `create_child` is the main function used during a retag.
+
+Finally, the protector end semantics are defined starting at lien 841, with the function `tree_get_all_protected_tags_initialized_locs` and `tree_access_all_protected_initialized`.
+
+To put all the definitions together, the inductive `bor_step` is defined.
+It is coupled to the main operational semantics by a series of "events".
+For example, a read (called "copy" here) causes a `CopyEvt`, which is picked up by the `CopyIS` rule.
+This will ensure the tag exists, and then cause a read event.
+
+Also of interests to reviewers is like 1000-1038. This defines a "unit test" for the `rel_dec` and `create_child` functions.
+Since `rel_dec` is not commutative, it can be difficult to remember which node is which and whether an output of e.g. "Child" means that the first node is a child of the second or the other way around.
+The "unit test" makes it clear that an output of "Child" indeed means that the first node is a child of the second.
+
 ## Correspondence with Section 5
 
 Section 5 has three examples, one for deleting reads, one for deleting writes, and one for reordering reads.