Challenge 20: remove two tool workarounds once Kani and CBMC are fixed #748

#740 (Challenge 20) carries two workarounds that can go once the tools are fixed.

1. The next_match stub in ffi::c_str::verify::check_from_ptr_contract (library/core/src/ffi/c_str.rs, with its any_match model). The harness reaches CharSearcher::next_match only through panic formatting, where it never runs. The loop contract of next_match makes Kani apply loop contracts to the whole harness, and CBMC 6.11 then rejects the contract-less loop of its built-in strlen ("Check that len is assignable"). Fixed by DFCC: scope skipped inner-loop locals to their enclosing scope diffblue/cbmc#9164 (merged 2026-09-16, in no release yet). Remove the stub once Kani ships a CBMC that includes it.

2. slice::Iter::kani_loop_raw_parts (library/core/src/slice/iter.rs), a copy of kani_raw_parts that only the loop invariants in str::pattern call. When a loop invariant calls a function that other code also calls, Kani lowers the invariant's call without its write-set argument and substitutes a nondeterministic value (#[kani::loop_invariant] with a method call lowers the call with "not enough arguments", substituting a non-deterministic value kani#4796). Merge it back into kani_raw_parts once #[kani::loop_invariant] with a method call lowers the call with "not enough arguments", substituting a non-deterministic value kani#4796 is fixed. kani_raw_parts itself stays: the invariants need the private fields of Iter.

After each removal, rerun str::pattern::verify_char_searcher::* and ffi::c_str::verify::check_from_ptr_contract.