diff --git a/doc/src/SUMMARY.md b/doc/src/SUMMARY.md index 15b0f6f0da3a9..9a8023d63908a 100644 --- a/doc/src/SUMMARY.md +++ b/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) diff --git a/doc/src/challenges/0004-btree-node.md b/doc/src/challenges/0004-btree-node.md index 6f252e9bd4bfa..6f29ce23eba73 100644 --- a/doc/src/challenges/0004-btree-node.md +++ b/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,7 +36,6 @@ 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` @@ -45,6 +43,11 @@ The memory safety of all public functions (especially safe ones) containing unsa 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` @@ -52,8 +55,6 @@ The memory safety of all public functions (especially safe ones) containing unsa 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):