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.

[feliperodri]

Static review (no local Kani run this time). This introduces a deliberate cfg(kani) path in memchr that routes callers through memchr_naive, which I scrutinized closely as a potential body-swap (verifier sees a different body than ships). It is soundly mitigated: the shipped word-at-a-time memchr_aligned remains verified directly by the new check_memchr_aligned_equiv_naive harness, which is non-vacuous — the aligned scanning loop is reachable for len in [16, 24], and assume(slice.len() >= 2*USIZE_BYTES) matches the real implicit precondition established by memchr's only call site — and checks both functional equivalence to the naive path and the UB of the unsafe word-sized reads. Callers therefore verify an equivalent but much cheaper path.

Minor: the equivalence is bounded (MAX_SIZE = 24) and the stack-array pointer may limit the align_offset values exercised; acceptable for a scanning-routine equivalence proof. The check_from_bytes_until_nul unwind bump 32 -> 33 is consistent with the changed reachable code. No major concerns.