Challenge 26: verify Rc/Weak safety in alloc::rc with Kani

README.md

@@ -50,7 +50,7 @@ These are the challenges:
 | [23: Verify the safety of Vec functions part 1](https://model-checking.github.io/verify-rust-std/challenges/0023-vec-pt1.html) | 15,000 USD | Open | |
 | [24: Verify the safety of Vec functions part 2](https://model-checking.github.io/verify-rust-std/challenges/0024-vec-pt2.html) | 15,000 USD | Open | |
 | [25: Verify the safety of `VecDeque` functions](https://model-checking.github.io/verify-rust-std/challenges/0025-vecdeque.html) | 10,000 USD | Open | |
-| [26: Verify reference-counted Cell implementation](https://model-checking.github.io/verify-rust-std/challenges/0026-rc.html) | 10,000 USD | Open | |
+| [26: Verify reference-counted Cell implementation](https://model-checking.github.io/verify-rust-std/challenges/0026-rc.html) | 10,000 USD | [Resolved](https://github.com/model-checking/verify-rust-std/pull/582) | [Kani](https://github.com/model-checking/verify-rust-std/blob/main/library/alloc/src/rcs/rc.rs) |
 | [27: Verify atomically reference-counted Cell implementation](https://model-checking.github.io/verify-rust-std/challenges/0027-arc.html) | 10,000 USD | Open | |
 | [28: Verify float to decimal conversion module](https://model-checking.github.io/verify-rust-std/challenges/0028-flt2dec.html) | 5,000 USD | Open | |
 | [29: Safety of `boxed`](https://model-checking.github.io/verify-rust-std/challenges/0029-boxed.html) | 15,000 USD | Open | |

doc/src/challenges/0026-rc.md

@@ -1,10 +1,11 @@
 # Challenge 26: Verify reference-counted Cell implementation
 
-- **Status:** Open
-- **Solution:** *Option field to point to the PR that solved this challenge.*
+- **Status:** Resolved
+- **Winning Solution:** [#582](https://github.com/model-checking/verify-rust-std/pull/582)
 - **Tracking Issue:** [#382](https://github.com/model-checking/verify-rust-std/issues/382)
 - **Start date:** *2025/06/01*
 - **Reward:** *10,000 USD*
+- **Contributors:** [v3risec](https://github.com/v3risec) ([Mingzhi Gao](https://github.com/highhigh4), [Minghua Wang](https://github.com/MinghuaWang))
 
 -------------------
 

library/alloc/src/lib.rs

@@ -90,6 +90,7 @@
 // Library features:
 // tidy-alphabetical-start
 #![cfg_attr(kani, feature(kani))]
+#![cfg_attr(kani, feature(proc_macro_hygiene))]
 #![cfg_attr(not(no_global_oom_handling), feature(string_replace_in_place))]
 #![feature(allocator_ext)]
 #![feature(array_into_iter_constructors)]