Separate list of functions that require unbounded verification

doc/src/SUMMARY.md

@@ -16,5 +16,5 @@
  - [Core Transmutation](./challenges/0001-core-transmutation.md)
  - [Memory safety of core intrinsics](./challenges/0002-intrinsics-memory.md)
  - [Pointer Arithmetic](./challenges/0003-pointer-arithmentic.md)
+ - [Memory safety of BTreeMap's `btree::node` module](./challenges/0004-btree-node.md)
  - [Inductive data type](./challenges/0005-linked-list.md)
- - [Memory safety of BTreeMap's `btree::node` module](./challenges/0006-btree-node.md)

doc/src/challenges/0004-btree-node.md

@@ -18,7 +18,6 @@ This is one of the main modules used for implementing the `BTreeMap` collection,
 The memory safety of all public functions (especially safe ones) containing unsafe code must be verified, e.g.:
 
 1. `LeafNode::new`
-1. `NodeRef::new_internal`
 1. `NodeRef::as_internal_mut`
 1. `NodeRef::len`
 1. `NodeRef::ascend`
@@ -37,23 +36,25 @@ The memory safety of all public functions (especially safe ones) containing unsa
 1. `Handle::right_edge`
 1. `Handle::left_kv`
 1. `Handle::right_kv`
-1. `Handle::insert_recursing`
 1. `Handle::descend`
 1. `Handle::into_kv`
 1. `Handle::key_mut`
 1. `Handle::into_val_mut`
 1. `Handle::into_kv_mut`
 1. `Handle::into_kv_valmut`
 1. `Handle::kv_mut`
+
+Verification must be unbounded for functions that use recursion or contain loops, e.g.
+
+1. `NodeRef::new_internal`
+1. `Handle::insert_recursing`
 1. `BalancingContext::do_merge`
 1. `BalancingContext::merge_tracking_child_edge`
 1. `BalancingContext::steal_left`
 1. `BalancingContext::steal_right`
 1. `BalancingContext::bulk_steal_left`
 1. `BalancingContext::bulk_steal_right`
 
-The verification must be unbounded for functions that are recursive or that contain loops (e.g. `Handle::insert_recursing`).
-
 ### List of UBs
 
 All proofs must automatically ensure the absence of the following [undefined behaviors](https://github.com/rust-lang/reference/blob/142b2ed77d33f37a9973772bd95e6144ed9dce43/src/behavior-considered-undefined.md):