[paulocsanz]

Towards #281. Solves Challenge 17 with a VeriFast 26.10 proof of library/core/src/slice/{mod,raw,rotate}.rs, following the structure of the accepted VeriFast solutions for challenges 5 (linked_list) and 19 (RawVec): verifast-proofs/core/slice/mod.rs/{original,verified} with a three-step gate (verifast → refinement-checker → byte-diff against library/), wired into check-verifast-proofs.sh (runs in the existing verifast.yml CI job). A negative counterpart, verifast-proofs/core/slice/mod.rs-negative (the same proof with a deliberately wrong swap_unchecked), is wired into check-verifast-proofs-negative.sh (the verifast-negative.yml job) and must be rejected by both verifast and the refinement checker.

Success criteria

Criterion	Status
10 unsafe fns: contracts + verified no-UB under them	7 directly on the function (get_unchecked, get_unchecked_mut, swap_unchecked, split_at_unchecked, split_at_mut_unchecked, align_to, align_to_mut); 3 const-generic ones (as_chunks_unchecked, as_chunks_unchecked_mut, get_disjoint_unchecked_mut) on a runtime-n transcription of the body, see caveat 1
27 safe fns: verified no UB	10 directly on the function; 17 const-generic ones via transcriptions, see caveat 1
Unbounded (arbitrary length)	Met — no unwind bounds anywhere
Generic T (no monomorphization)	Met — proofs are polymorphic in T (and in n) at the tool level

The two criteria that Kani submissions to this challenge have marked "not literally met" (unbounded; generic T without monomorphization) are satisfied here by construction, so this submission does not depend on the pending committee ruling on the generic-T clause.

Kani harnesses for the const-generic functions

For the 20 const-generic functions, which VeriFast 26.10 can only verify through transcriptions (caveat 1), this PR also adds Kani verification of the exact shipped bodies, bounded and monomorphized, in library/core/src/slice/mod.rs: #[requires]/#[ensures] contracts on the three unsafe ones (as_chunks_unchecked, as_chunks_unchecked_mut: N != 0 && self.len().is_multiple_of(N); get_disjoint_unchecked_mut: get_disjoint_check_valid(&indices, self.len()).is_ok(), the check get_disjoint_mut performs) with #[kani::proof_for_contract] harnesses over u8/u32/() and N in 1..=4 (usize and Range<usize> indices for get_disjoint_unchecked_mut), and bounded harnesses (slice length ≤ 12, any_slice_of_array) for the 17 safe ones, asserting the shapes of the results. The two tools are complementary here: VeriFast gives the unbounded, generic-T argument; Kani runs the real bodies. The contract macros are no-ops outside cfg(kani_host) and the harness module is cfg(kani), so the VeriFast gate is unchanged (patch-verifast-proofs.sh re-syncs the proof copies). With the repository's pinned Kani (tool_config/kani-version.toml), kani verify-std on the 22 harnesses reports Complete - 22 successfully verified harnesses, 0 failures (the CI partitions of this PR ran all 22).

Coverage (all 37 functions)

• Unsafe, direct contracts: get_unchecked, get_unchecked_mut, swap_unchecked, split_at_unchecked, split_at_mut_unchecked, align_to, align_to_mut
• Unsafe (const-generic, via runtime-n wrappers — see caveats): as_chunks_unchecked, as_chunks_unchecked_mut, get_disjoint_unchecked_mut
• Safe, direct: reverse, split_at_checked, split_at_mut_checked, binary_search_by, partition_dedup_by, rotate_left, rotate_right, copy_from_slice, copy_within, swap_with_slice
• GetDisjointMutIndex::{is_in_bounds, is_overlapping}: verified against the region model for usize only (2 of the 10 impl methods). The Range<usize> impls read fields through &Range<usize>, which VeriFast 26.10 routes through a share interpretation of Range that its std specs do not define; RangeInclusive<usize> and core::range::* cannot be named in ghost code. Those 8 methods have no specification and are skipped, so the model is not checked against them
• Safe (const-generic, via wrappers): first_chunk, first_chunk_mut, split_first_chunk, split_first_chunk_mut, split_last_chunk, split_last_chunk_mut, last_chunk, last_chunk_mut, as_chunks, as_chunks_mut, as_rchunks, as_simd, as_simd_mut, as_flattened, as_flattened_mut, get_disjoint_mut, get_disjoint_check_valid. The as_simd/as_simd_mut wrappers additionally take valid_slice_transmute::<T, Simd<T, N>>() (the # Safety condition of align_to, justified by Simd's #[repr(simd)] layout) as an explicit, unchecked precondition

The tour of the proof, the ownership discipline (RustBelt-style share/full_borrow encoding), and every caveat are documented in verifast-proofs/core/slice/mod.rs/README.md.

Caveats (summary; full list in the proof README)

1. Const-generic functions. VeriFast 26.10 cannot attach specs to <const N: usize> functions (error: Todo: ConstKind::Param, vf_mir_translator.ml:1787), and passing N from the const fn into a wrapper aborts the refinement checker (Clause kind not supported, refinement_checker.ml:2338, ClauseKind::ConstArgHasType). Each const-generic function therefore has a *_proof__VeriFast_wrapper transcription that is generic in Chunk and takes n: usize at runtime, with a concrete layout predicate fix is_array_of<T, Chunk>(n: usize) -> bool { 0 <= n && size_of::<Chunk>() == n * size_of::<T>() && align_of::<Chunk>() == align_of::<T>() } as the layout bridge (used to prove e.g. flatten_non_zst_no_overflow mechanically). One proof covers every N, unbounded. To be explicit: VeriFast does not verify these 20 bodies. They carry no specification and -skip_specless_fns skips them; the refinement checker only confirms that they are identical to the original, which says nothing about the transcriptions. The correspondence between each body and its wrapper is by inspection only. The Kani harnesses below verify the bodies themselves, bounded and monomorphized. A VeriFast change that lifts this limitation is proposed in [Rust] Support const generic parameters in specified functions verifast/verifast#1048. This submission does not depend on it, but we are prepared to replace the 20 wrappers by direct specifications on the unchanged bodies as soon as a VeriFast release supports that.
2. Axioms (assume(false) lemmas), all with closed specifications. Contiguous borrow splitting (split_at_unchecked by induction on array_share, split_at_mut_unchecked and the reusable slice_full_borrow_split via open_full_borrow_strong_ + full_borrow_split), slice_full_borrow_inv, flatten_non_zst_no_overflow, gcd (including divisibility of its result), align_to_offsets (including byte-exact coverage of the middle slice; proved on its *_proof__VeriFast_wrapper transcription, since the method's const { gcd(..) } block and nested fn gcd are not translated, and the method itself carries the proved postcondition as a trusted assume_correct spec, see the README) and the whole get_disjoint_* bookkeeping (region carving and borrow conversion) are proved mechanically. What remains axiomatized is listed by name in the README: tuple/Range own closing, [T]↔[T; N]-chunk and stack-buffer reinterpretation under an abstract "Chunk is [T; n]" predicate (with its layout facts as an axiom), RustBelt's Copy rules (gated by a T: Copy witness function, so rustc rejects any use for a non-Copy type), the [T]→[U] reinterpretation of an aligned, byte-exactly covering prefix in align_to (alignment comes from ptr::align_offset's spec, coverage and the split are proved), the region model of the five sealed GetDisjointMutIndex impls (4 generic lemmas: the interval meaning of is_in_bounds/is_overlapping and the ownership meaning of get_unchecked_mut's result; plus the model's definition at usize and Range<usize>, against which the two interval lemmas are proved and the usize impls are verified; the carving of the regions out of the array and their restoration are proved by induction), the Range<usize> instance of get_unchecked's bounds precondition, and associativity of multiplication. No axiom produces ownership of pointers unrelated to its inputs or duplicates a borrow, and there are no inline assume statements. Each axiom that stands in for a missing prelude rule or prover fact is linked, at the assume(false) and in the README, to a VeriFast issue with a minimal reproducer: tuple/Range closing [Rust] No way to close <(T1, T2)>.own / <(T1, T2, T3)>.own / <Range<Idx>>.own from the components verifast/verifast#1049, slice validity facts $PATH for running compiletest.exe is not correct on windows rust-lang/rust#1050, Copy rules Bare functions, typesafe spawn, function subtyping rust-lang/rust#1051, mul_assoc Rewrite spawn again rust-lang/rust#1052, tuple layout Make a decision about fn@/lambda and fn&/block rust-lang/rust#1053 (and the chunk reinterpretation lemmas to the [T; N] ownership of Non-boxed recursive tag constructor fails to compile with "Out of stack space" rust-lang/rust#1048).
3. assume_correct on external/MIR-unsupported wrappers (slice::range, call_f_binary_search__VeriFast_wrapper, call_same_bucket__VeriFast_wrapper, empty_slice__VeriFast_wrapper, …; the full list is in the README). Two of them sit inside the get_disjoint_unchecked_mut transcription and are its only unsafe operations: clone_disjoint_index__VeriFast_wrapper (indices.get_unchecked(i).clone()) and write_disjoint_mut_elem__VeriFast_wrapper (arr_ptr.add(i).write(&mut *slice.get_unchecked_mut(idx)), whose trusted spec is the raw-pointer semantics of the sealed SliceIndex::get_unchecked_mut impls expressed in the region model, not the SliceIndex contract of core.rsspec), so what VeriFast proves for that function is the ownership bookkeeping over that model. external functions referencing Option, Range, or MaybeUninit cannot be placed in core.rsspec because vf_mir_translator.ml:418 restricts -extern_spec header dependencies to prelude.rsspec only ([Rust] -extern_spec files can only depend on prelude.rsspec, so they cannot mention std types (Option, Range, MaybeUninit) verifast/verifast#1056). The std functions whose signatures allow it (ptr::metadata, ptr::swap, ptr::swap_nonoverlapping) are specified in core.rsspec as extern specifications, like VeriFast's own std/lib.rsspec, and proposed upstream in [Rust] Specs for ptr::replace, ptr::swap, ptr::swap_nonoverlapping, ptr::slice_from_raw_parts; tuple_2/tuple_3 own lemmas verifast/verifast#1057; align_offset (a raw-pointer method) and slice_from_raw_parts{,_mut}/ptr::copy (whose specs use crate-local definitions) remain local forwarding functions in verified/lib.rs. Note that [T]::len is verified directly against ptr::metadata in core.rsspec, and T::IS_ZST branches are discharged mechanically via VeriFast's built-in std::mem::IS_ZST translation (vf_mir_translator.ml:2220) and std::alloc::is_valid_layout_size_of_align_of without inline assume statements.
4. Single local macro vf_revswap! in reverse (the verified copy omits revswap's two compiled-out debug_assert!s and indexes through element pointers; details in the README): vf_mir_exporter (lib.rs:434,940) ignores inline specs on nested functions inside a statement block, and rust_parser.ml:1036 rejects impl<T> [T] in .rsspec files; therefore revswap is verified as the top-level function revswap_proof__VeriFast_wrapper and invoked via vf_revswap!. Nested-fn specifications are proposed in [Rust] Support specifications on fn items nested inside a function body verifast/verifast#1058.
5. Flags: -skip_specless_fns -ignore_unwind_paths -allow_assume -allow_ignore_ref_creation. The 10 ignore_ref_creation directives (each checked to be necessary) suppress the aliasing-rule check at 10 sites: four &[T; N] created from raw pointers in the chunk wrappers (a shared reference to a type-parameter pointee from share ownership: init_ref_share needs type_interp, which 26.10 only provides inside lemma-pointer bodies), one &I::Output in get_unchecked, three &Ordering auto-references in binary_search_by and two &[_; 0] literals in align_to (temporaries inside expressions of directly verified bodies, where the protocol's ghost statements cannot be placed); the &I references of the get_disjoint_check_valid wrapper are created under the protocol; slice references created from raw pointers need no directive in 26.10 because the translator does not apply the protocol to them ([Rust] Aliasing model: reference-creation lemmas require a Sized pointee, so a &[T] created from a raw pointer cannot be verified verifast/verifast#1059); results are per target architecture (LP64); VeriFast is not foundational and has known unsoundnesses (pointer-aliasing rules, variance) as documented at https://github.com/verifast/verifast/issues?q=is%3Aissue+is%3Aopen+label%3Aunsoundness
6. Sysroot core. Since core::slice lives in core, verify.sh builds a libcore_noslice.rlib (a core without the slice inherent impls under test). It is built from the rust-src of the toolchain VeriFast 26.10 targets (nightly-2026-09-25), because VeriFast's rustc frontend cannot compile the repository's newer library/core subtree (nightly-2026-10-12 adds abort_immediate/type_id_* intrinsics and drops the optimize_attribute gate). The slice sources under verification are the repository's, byte-for-byte (enforced by the diff step); only the surrounding core comes from VeriFast's toolchain, as the linked_list and raw_vec proofs already do with VeriFast's own std specs. This also decouples the proof from subtree bumps such as Merge subtree update for toolchain nightly-2026-10-22 #737. The four visibility/attribute edits applied to that core are a reviewable core-sysroot.patch (a diff -ru), applied with patch -p1 by verify.sh.

Complements (not required by the challenge)

• The proof verifies the three rotation algorithms in slice/rotate.rs (ptr_rotate_memmove, ptr_rotate_gcd, ptr_rotate_swap) against the ptr_rotate contract used by rotate_left/rotate_right.
• from_raw_parts/from_raw_parts_mut (slice/raw.rs) are verified.
• We would be happy to upstream the slice borrow lemmas (such as array_share_split, slice_full_borrow_inv, and tuple/range ownership closing lemmas) into the VeriFast Rust prelude in a follow-up, so future proofs don't need to re-declare them; the gaps are filed as [Rust] No way to close <(T1, T2)>.own / <(T1, T2, T3)>.own / <Range<Idx>>.own from the components verifast/verifast#1049–Get rid of iterators rust-lang/rust#1056 and the const-generic support as [Rust] Support const generic parameters in specified functions verifast/verifast#1048.