[srivatsansamraj]

Resolves #4954.

In the nightly-2026-09-25 library that model-checking/verify-rust-std#687 syncs to, core's is_ascii has an aarch64 NEON path (is_ascii_neon) that calls vmaxvq_u8, which lowers to simd_reduce_max. Kani reports that intrinsic as unsupported, so slice::ascii::verify::check_is_ascii fails on the macOS runners for that sync and the ones after it.

This adds simd_reduce_max and simd_reduce_min for integer lanes, next to simd_reduce_all: the lanes are folded into a temporary that keeps the larger (or smaller) value at each step, with signedness taken from the lane type. Non-integer lanes are reported as unsupported: both intrinsics take integer vectors only, and portable SIMD's float reductions do not call them. The intrinsics table in the docs gets the two rows.

The new kani test checks both reductions against Iterator::max and Iterator::min over symbolic u8x16 and i32x4 lanes (the signed lanes catch an unsigned comparison), and the new expected test checks that the float lanes fail verification as unsupported. Both fail without this change. The aarch64 path itself does not build on x86_64, so the end-to-end check is verify-rust-std's macOS job.

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

[srivatsansamraj]

@CYJ904 @Tianshu-Huang @wodex1nhaoIeng @acearyanarun for review. Kani could not handle simd_reduce_max, the vector operation that returns the largest lane. The library we now sync to uses it in the ARM (NEON) version of is_ascii, so check_is_ascii fails on the macOS CI runners, which are ARM. This adds max and min reductions for integer lanes the same way Kani already does simd_reduce_all; float lanes stay reported as unsupported. The new tests compare against Rust's own max()/min() on symbolic lanes. What moves: check_is_ascii on macOS for model-checking/verify-rust-std#687 and later syncs, once a Kani with this is pinned.

[Copilot]

Warning

Copilot couldn't run its full agentic review because it didn't start before the timeout. Make sure your repository has a runner available, or add a copilot-code-review.yml file specifying one with the runs-on attribute. See the docs for more details.

Copilot review overview

Review effort: Lite
Findings: 1 · 1

Open (2)

• This expected-output file looks malformed: the trailing \\ on the Status: FAILURE\\ lines and… · New
• Unlike SimdReduceAll, this writes acc to place without casting to the CBMC return type. Even… · New

What changed in this PR

Adds Kani support for the Rust SIMD reduction intrinsics simd_reduce_max and simd_reduce_min on integer lanes, unblocking verification of core paths (e.g., aarch64 NEON is_ascii) that lower to these intrinsics, while explicitly rejecting float-lane reductions due to unmodeled NaN semantics.

Changes:

• Implement codegen for simd_reduce_max / simd_reduce_min over integer SIMD lanes and mark float-lane usage as unsupported.
• Extend intrinsic classification (parsing, points-to, uninit checks) to recognize the new intrinsics.
• Add Kani regression tests for integer-lane behavior and expected-failure tests for float lanes; document partial support.

File	Description
tests/​kani/​Intrinsics/​SIMD/​Reduction/​reduce_min_max.rs	Adds Kani proofs validating integer-lane reduce max/min behavior against iterator max/min.
tests/​expected/​intrinsics/​simd-reduce-float/​main.rs	Adds harnesses that intentionally invoke float-lane reduce max/min to ensure they’re rejected.
tests/​expected/​intrinsics/​simd-reduce-float/​expected	Captures expected failure output for unsupported float-lane reduce max/min.
kani-compiler/​src/​kani_middle/​transform/​check_uninit/​ptr_uninit/​uninit_visitor.rs	Treats new reduce intrinsics as safe to skip for uninit pointer checking.
kani-compiler/​src/​kani_middle/​points_to/​points_to_analysis.rs	Treats new reduce intrinsics as identity-aliasing for points-to analysis.
kani-compiler/​src/​intrinsics.rs	Adds new intrinsic variants and matches simd_reduce_max / simd_reduce_min.
kani-compiler/​src/​codegen_cprover_gotoc/​codegen/​intrinsic.rs	Implements integer-lane folding codegen and rejects float-lane reductions.
docs/​src/​rust-feature-support/​intrinsics.md	Documents partial support for the two new intrinsics (integer lanes only).

---

💡 Add a code-review agent skill or configure MCP servers for context-aware, tailored reviews. Learn more in the docs.

[feliperodri]

Requesting changes for one small bug; the approach is right. Integer reductions are correct for every lane width I tried (i8–u64, 1 to 16 lanes), and the aarch64 is_ascii shape (max of bytes < 0x80 ⇔ all ASCII) verifies. usize/isize lanes crash codegen on a type mismatch, which is reachable through portable SIMD's reduce_max. The cast suggested inline fixes it, and a usize harness would pin it; with that, this is an approve.

[srivatsansamraj]

Rebased onto main. fa17f395c lists both reductions in simd_vector_operand from #4927, with a scalar harness in simd-scalar-operand: before it, simd_reduce_max::<i32, i32> crashed the compiler.

[feliperodri]

Thanks for the quick turnaround. Removing the cast brings the usize/isize crash back, and the new harnesses catch it. I also checked your float-lane reply against rustc: its LLVM backend only accepts integer lanes for these two intrinsics, so reporting floats as unsupported is the right call and there's nothing to track. Portable SIMD's reduce_max/reduce_min on usize and i64, a single-lane vector, and the is_ascii shape all verify.

One non-blocking point inline: a return type that isn't the lane type is accepted silently. rustc rejects it, and the comparisons already report it as unsupported. A follow-up is fine.

The NEON path itself only runs on verify-rust-std's macOS job, so that's the end-to-end check once this lands.

[feliperodri]

@srivatsansamraj ready to merge?

[srivatsansamraj]

Yes, ready once CI passes; I'll open the return-type check as a follow-up, matching simd_mask_problem.