188             // INVARIANT: There are no nodes in the tree, so the invariant holds vacuously.  in new()
198             // INVARIANT:  in iter()
213             // INVARIANT:  in iter_mut()
245             // INVARIANT:  in cursor_front()
260             // INVARIANT:  in cursor_back()
378 …       // SAFETY: By the type invariant of `Self`, all non-null `rb_node` pointers stored in `self`  in get()
425 …       // SAFETY: By the type invariant of `Self`, all non-null `rb_node` pointers stored in `self`  in cursor_lower_bound()
465             // INVARIANT:  in cursor_lower_bound()
486         // INVARIANT: The loop invariant is that all tree nodes from `next` in postorder are valid.  in drop()
495             // INVARIANT: This is the destructor, so we break the type invariant during clean-up,  in drop()
496             // but it is not observable. The loop invariant is still maintained.  in drop()
498             // SAFETY: `this` is valid per the loop invariant.  in drop()
762         // SAFETY: By the type invariant of `Self`, all non-null `rb_node` pointers stored in `self`  in remove_current()
769         // the tree cannot change. By the tree invariant, all nodes are valid.  in remove_current()
781             // INVARIANT:  in remove_current()
805             // the tree cannot change. By the tree invariant, all nodes are valid.  in remove_neighbor()
807 …       // SAFETY: By the type invariant of `Self`, all non-null `rb_node` pointers stored in `self`  in remove_neighbor()
828         // INVARIANT:  in mv()
913         // SAFETY: By the type invariant of `Self`, all non-null `rb_node` pointers stored in `self`  in to_key_value_raw()
1022         // SAFETY: By the type invariant of `IterRaw`, `self.next` is a valid node in an `RBTree`,  in next()
1023 …// and by the type invariant of `RBTree`, all nodes point to the links field of `Node<K, V>` objec…  in next()
1175         // INVARIANT: We are linking in a new node, which is valid. It remains valid because we  in insert()
1237         // INVARIANT: The node is being returned and the caller may free it, however, it was  in remove_node()