Fix compiler crash on slice-modifies verified stubs (#4748)

[feliperodri]

Description

#[kani::modifies(x)] on a whole-slice argument (e.g. x: &mut [u8]) crashed the compiler when the contract was reused as a verified stub via #[kani::stub_verified]. Reachability collection panicked with:

Failed to resolve `FnDef(... "std::iter::IntoIterator::into_iter")`
with `GenericArgs([Ref(ReErased, Slice(Slice(Uint(U8))), Mut)])`

i.e. a doubled slice &mut [[u8]].

Context

AnyModifiesPass::replace_any_modifies rewrites the write_any marker into write_any_slim / write_any_slice / write_any_str based on the pointee type. write_any_slice<T>(slice: *mut [T]) is generic over the element type T, but the pass resolved it with the marker's instance_args, which hold the pointee type [T]. That produced write_any_slice::<[u8]>(*mut [[u8]]); its fill_with(T::any) body then iterated &mut [[u8]], and into_iter failed to resolve because [u8] is neither Sized nor Arbitrary.

This path is only reached in replace mode (stub_verified), which is why proof_for_contract harnesses were unaffected and the existing modifies_fat_pointer tests (all check-mode) did not catch it — removing the #[kani::stub_verified] line from the reproducer avoids the crash.

The fix resolves write_any_slice with the slice's element type instead of the pointee type.

Resolved issues

Resolves #4748

Testing

• Added tests/expected/function-contract/modifies_fat_pointer/slice_replace.rs, which exercises both proof_for_contract (check) and stub_verified (replace) on a &mut [u8] slice-modifies contract — the replace harness reproduces the crash before this change.
• Verified locally that the reproducer from the issue and the new test now complete codegen without panicking.

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