Use byte-wise memchr under Kani to cut symbolic execution cost

[tautschnig]

Profiling ffi::c_str::verify::check_to_bytes (via CBMC --program-only SSA attribution) showed that a third of all SSA steps came from a single function: slice::memchr::memchr_aligned's runtime arm — the word-at-a-time scan behind slice contains, which CStr's safety invariant and contract clauses evaluate repeatedly. Symbolically, the word-optimized scan is ~13× more expensive than the semantically equivalent byte-wise memchr_naive loop while providing zero benefit: there is no word-level parallelism in symbolic execution.

This PR routes memchr to memchr_naive under cfg(kani). Measured effect (Kani 152c6a8c + CBMC 6.10.0, --jobs=4): the full ffi::c_str suite runs 12/12 in 2:13 wall; check_to_bytes alone drops from 3:28 wall / 170 s CBMC solve to 14.6 s solve, and from 606 s to 21 s solve when dependency contracts are asserted. check_from_bytes_until_nul needs its unwind bound raised from 32 to 33 (the byte-wise loop needs one more iteration than the word scan); it now solves in 3.1 s where the old bound's comment recorded 33.1 s.

Since the CStr harnesses were the only indirect verification coverage of memchr_aligned's unsafe word-sized reads, the PR adds an equivalence harness checking memchr_aligned against memchr_naive on all inputs up to 24 bytes (documenting the len >= 2*USIZE_BYTES precondition its caller establishes), so the optimized implementation stays verified. All str:: and slice::memchr harnesses (15 + 13) pass with this change.

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

[Copilot]

Pull request overview

This PR reduces symbolic execution cost under Kani by routing core::slice::memchr::memchr to the byte-wise memchr_naive implementation when cfg(kani) is enabled, while preserving verification coverage of the optimized word-at-a-time implementation via a new equivalence proof.

Changes:

• Under cfg(kani), make memchr always use memchr_naive to avoid expensive symbolic execution of the word-scan path.
• Add a Kani proof harness in core::slice::memchr that checks memchr_aligned is equivalent to memchr_naive for slices up to 24 bytes (with the caller-established length precondition).
• Increase the unwind bound for the CStr::from_bytes_until_nul harness from 32 to 33.

Reviewed changes

Copilot reviewed 2 out of 2 changed files in this pull request and generated 1 comment.

File	Description
library/core/src/slice/memchr.rs	Route memchr to the naive loop under Kani and add an equivalence proof for memchr_aligned vs memchr_naive.
library/core/src/ffi/c_str.rs	Adjust Kani unwind bound for from_bytes_until_nul harness to match the new execution profile under Kani.