Challenge 23: Verify Vec Part1 safety with Kani

[v3risec]

Summary

This PR adds Kani-based verification artifacts for Vec APIs in library/alloc/src/vec/mod.rs for Challenge 23.

The change introduces:

• Kani contracts for unsafe raw reconstruction, length mutation, append, and spare-capacity splitting APIs
• proof harness modules under #[cfg(kani)] for all Challenge 23 listed Vec entries
• reusable symbolic Vec helpers for allocated, ZST, bounded, and reserve-sensitive cases
• Kani loop contracts and Kani-only loop structure for retain, dedup, extend, and trusted-iterator paths

No non-verification runtime behavior is changed in normal builds.

Notes on Challenge 23 Function Signatures

Several Challenge 23 names do not exactly match the current repository source. This PR follows the checked-in API definitions.

Notable alignments include:

• from_nonnull is verified as Vec::from_parts, the current NonNull<T> raw-parts constructor.
• from_nonnull_in is verified as Vec::from_parts_in.
• Internal listed entries such as append_elements, split_at_spare_mut_with_len, extend_with, spec_extend_from_within, extend_desugared, and extend_trusted are verified from inside vec::mod, where those private paths are accessible.

Verification Coverage Report

Coverage: 36 / 36 Challenge 23 entries targeted

Contract-backed unsafe/API groups include:

• Vec::from_raw_parts
• Vec::from_parts
• Vec::from_parts_in
• Vec::set_len
• Vec::append_elements
• Vec::split_at_spare_mut_with_len

Harness-backed coverage includes:

• raw-parts decomposition and boxed-slice conversion
• length and element operations: truncate, swap_remove, insert, remove, push, push_within_capacity, pop, clear
• bulk and iterator-related operations: append, drain, split_off, extend_from_within, extend_with, spec_extend_from_within, extend_desugared, extend_trusted, extract_if
• spare-capacity APIs: spare_capacity_mut, split_at_spare_mut, split_at_spare_mut_with_len
• trait paths: Deref, DerefMut, IntoIterator, Drop, and [T; N]::try_from(Vec<T>)
• panic-path harnesses for representative out-of-bounds and capacity-overflow cases

Approach

The verification strategy combines function contracts with executable harnesses:

1. Add kani::requires, kani::ensures, and kani::modifies clauses for unsafe pointer/length APIs where the source safety requirements can be expressed.
2. Add #[kani::proof_for_contract] harnesses for contract targets and #[kani::proof] harnesses for safe and internal APIs.
3. Use representative concrete instantiations across integer types, usize/isize, unit/ZSTs, fixed arrays, nested arrays, and a clone-only type.
4. Add Kani loop invariants and modifies sets for paths that manipulate initialized prefixes, spare capacity, and panic-safe length guards.
5. Keep verification-only helper accessors in SetLenOnDrop under cfg(kani) so normal builds preserve the original behavior.

Scope assumptions

• Generic T is represented through a broad set of concrete instantiations used by the harness macros.
• Raw pointer provenance is constrained with Kani memory predicates where currently expressible.

Verification

All added Challenge 23 harnesses pass locally with Kani.

Resolves #284

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

Adds Kani verification artifacts for Challenge 23’s Vec safety targets.

Changes:

• Adds contracts and proof harnesses for Vec APIs.
• Introduces Kani-specific loop invariants and helper accessors.
• Updates verification dependencies and compiler features.

Reviewed changes

Copilot reviewed 2 out of 4 changed files in this pull request and generated 11 comments.

File	Description
library/Cargo.lock	Records safety-contract dependencies.
library/alloc/src/lib.rs	Enables proc-macro hygiene.
library/alloc/src/vec/mod.rs	Adds contracts, loop models, and harnesses.
library/alloc/src/vec/set_len_on_drop.rs	Adds Kani-only pointer accessors.

Suppressed comments (1)

library/alloc/src/vec/set_len_on_drop.rs:34

• As with local_len_ptr, this pub(super) verification helper should not add an inline hint under the repository's inline policy. Remove #[inline].

    #[inline]

---

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

[feliperodri]

Review: PR #598 — Challenge 23 (Vec pt1)

1. The 11 #[cfg(not(kani))] blocks — NOT fatal (credit given)

I classified each against the fatal pattern from #537/#538/#557/#558 (replacing a verified body with a #[cfg(kani)] nondeterministic stub that assumes its own safety). None of them do this. Every one is a loop-contract rewrite that faithfully reproduces the real logic, only rebinding locals into pre-declared mut variables so kani::loop_modifies can name them, or splitting the original body from a Kani variant that adds loop_invariant/loop_modifies. The real writes (ptr::write, same_bucket, drop_in_place, increment_len, clone()) are preserved.

#	Diff line	Function	Classification
1	367	dedup_by loop 1	Benign — kani block (356-366) recomputes found_duplicate into tracked vars; logic identical
2-4	420,422,426	dedup_by loop 2	Benign — kani block (410-419) rebinds read/prev ptr + found_duplicate; real drop/copy branch unchanged
5	439	dedup_by write_ptr	Benign — rebinds write_ptr only
6	516	extend_with	Benign swap — kani block (546-620) reproduces clone loop + last-write via SetLenOnDrop with invariants
7	676	spec_extend_from_within	Benign swap — kani block (634-674) is manual MaybeUninit::write loop, semantically equal to iter::zip
8	758,770	extend_desugared	Concern (not fatal): kani replaces if len==cap { reserve } with if len==cur_cap { kani::assume(false) } — see §3
9	777	extend_desugared dst	Benign — rebinds dst
10	805	extend_trusted	Benign swap — kani block (814-885) reproduces for_each as manual loop with invariants

Conclusion: no cfg-swap vacuity. This is materially better than the rejected PRs and I credit the author for structuring the rewrites correctly.

2. Contract-liveness (T7) — PASS (correcting the triage note)

The triage note "6 proof_for_contract, 0 added contracts" is incorrect. All 6 proof_for_contract targets have contracts added in this diff:

• from_raw_parts (diff 187-217), from_parts (225-246), from_parts_in (254-275): kani::requires
• set_len (283-284): requires + modifies
• append_elements (447-472): requires + modifies
• split_at_spare_mut_with_len (480-495): ensures

No orphaned contract harnesses. T7 is satisfied.

3. BLOCKING — both mandatory Challenge-23 criteria are violated

The spec states verbatim: "The verification must be unbounded---it must hold for slices of arbitrary length" and "The verification must hold for generic type T (no monomorphization)."

(a) Monomorphization — violated for 100% of harnesses. Every harness is macro-generated over a fixed concrete type list (u8..i128, usize/isize, (), [u8;4]). There is not a single generic-T harness. verifier_nondet_bounded_vec even requires T: kani::Arbitrary. Concrete primitives cannot discharge the obligation for T with validity/drop invariants. (Copilot: mod.rs:5000.) This alone fails the mandatory criterion.

(b) Bounded length — violated for several required functions. verifier_nondet_bounded_vec (diff 937-946) caps at MAX_VEC_LEN = 4, and is used by retain_mut, dedup_by, append_elements, extend_desugared, extend_trusted (lengths 0–4 only). Additionally extend_with is bounded len<=8, n<=8 (diff 2006-2007), extend_desugared's max_write is clamped <=8 with kani::assume(false) otherwise (diff 699-704), and the *_clone_only harnesses assume <=4/<=8. These directly contradict "arbitrary length." (Copilot: mod.rs:4845, 4169.)

Note: many other harnesses are properly unbounded via verifier_nondet_vec (symbolic cap/len with len<=cap) — good. But the mixed picture still fails the criterion for the bounded subset, and monomorphization fails it globally.

4. Additional soundness gaps (would block independently)

• set_len only verifies shrinking. The harness constrains non-ZST new_len <= initialized_len (diff 1255), and the contract is only new_len <= self.capacity() (diff 283). The safety-sensitive half — growing len over uninitialized spare — is never exercised, and the contract omits the "elements in old_len..new_len initialized" precondition. (Copilot: mod.rs:2055, 5232.)
• append_elements assumes away reallocation. Contract requires count <= spare (diff 449-450), making the function's own self.reserve(count) a no-op; the grow path is never verified. Spare capacity is not a precondition of this function. (Copilot: mod.rs:2999.)
• extend_desugared assumes the Vec is never full (if len==cur_cap { kani::assume(false) }, diff 755-757), excluding every reserve/realloc path. (Copilot: mod.rs:4169, 4183.)
• split_off should_panic harness includes a non-panicking case. harness_vec_split_off_out_of_bounds uses at >= vec.len() (diff 1732), but at == len is valid for split_off and does not panic; the panic claim is not valid on every path. Should be at > len. (Copilot: mod.rs:5709.)
• from_parts/from_parts_in accept a misaligned NonNull when ZST or capacity==0 (alignment requirement gated away, diff 260-271). (Copilot: mod.rs:797, 1242.)
• spec_extend_from_within_clone_only (diff 2090-2107) omits the count <= cap - len assumption that the macro variant has, so the body's internal kani::assume(can_write(...)) silently discards invalid states instead of surfacing them. (Copilot: mod.rs:6080.)

Minor (non-blocking): #[inline] on pub(super) Kani-only helpers in set_len_on_drop.rs:29,34 violates the repo inline policy (Copilot).

Required direction to reach APPROVE

1. Replace all monomorphized macro harnesses with generic-T harnesses (no concrete-type expansion), per the mandatory no-monomorphization criterion.
2. Remove the MAX_VEC_LEN=4 / <=8 bounds; drive length symbolically and unbounded via loop contracts for retain_mut, dedup_by, append_elements, extend_desugared, extend_trusted, extend_with.
3. Make set_len verify the growth path (symbolic initialized prefix beyond old len) and strengthen its contract with the initialization precondition.
4. Cover the reallocation paths in append_elements and extend_desugared rather than assuming spare capacity.
5. Fix the split_off panic-harness boundary (at > len) and add the unconditional alignment requirement to from_parts/from_parts_in.

The loop-contract engineering here is solid and free of the body-swap vacuity that sank prior PRs, but it does not yet meet the two mandatory criteria, so changes are required.

[v3risec]

Notes on the Vec::set_len Initialization Precondition and the split_off Verification Issue

While addressing the reviewer feedback on Vec::set_len, we added the second Safety Requirement of set_len.

The Safety Requirement of Vec::set_len states:

The elements at old_len..new_len must already be initialized.

In other words, when set_len is used to increase the logical length of a Vec, the newly added elements within the new len range must already have been initialized before calling set_len.

To express this requirement, we added the following contract to set_len:

#[cfg_attr(
    kani,
    kani::requires(kani::mem::can_dereference(
        core::ptr::slice_from_raw_parts(
            self.as_ptr().wrapping_add(self.len),
            new_len.saturating_sub(self.len),
        )
    ))
)]

This precondition checks whether the region from the original self.len to the new new_len can be accessed as a valid [T], thereby expressing the Safety Requirement that old_len..new_len must already be initialized.

At the same time, we found that adding this contract alone is not sufficient. In order for Kani to actually track and check uninitialized memory, we need to pass the following option to run-kani.sh during verification:

-Z uninit-checks

Issue Found in split_off

While further examining Vec::split_off, we noticed that it contains two calls to set_len. The relevant logic is approximately:

let other_len = self.len - at;
let mut other =
    Vec::with_capacity_in(other_len, self.allocator().clone());

unsafe {
    self.set_len(at);
    other.set_len(other_len);

    ptr::copy_nonoverlapping(
        self.as_ptr().add(at),
        other.as_mut_ptr(),
        other.len(),
    );
}

The first call:

self.set_len(at);

shrinks the original Vec, so it does not introduce any newly exposed logical elements and therefore does not involve the initialization requirement for new elements.

However, the second call:

other.set_len(other_len);

is different.

Immediately after:

Vec::with_capacity(other_len)

the state of other is:

len = 0
capacity >= other_len

Although the underlying memory has already been allocated, the elements in 0..other_len are still uninitialized at this point.

However, the current implementation first calls:

other.set_len(other_len);

and only afterwards calls:

ptr::copy_nonoverlapping(...)

to copy the elements from the source Vec into other.

Therefore, at the point where other.set_len(other_len) is called, the range 0..other_len has not yet been initialized. According to the second documented Safety Requirement of Vec::set_len, this call does not satisfy:

old_len..new_len must already be initialized

where:

old_len = 0
new_len = other_len

Using a Separate Harness to Simulate the Call Sequence in split_off

To confirm whether Kani can detect this issue when uninitialized-memory checking is enabled, we wrote a harness that simulates the following call sequence in split_off:

with_capacity
→ set_len
→ copy_nonoverlapping

The harness is:

#[kani::proof_for_contract(Vec::<u8>::set_len)]
pub fn verify_seq_set_len() {
    let src_v = vec![0xffu8; 8];
    let at = 4;
    let other_len = src_v.len() - at;

    let mut other = Vec::<u8>::with_capacity(other_len);

    unsafe {
        other.set_len(other_len);

        core::ptr::copy_nonoverlapping(
            src_v.as_ptr(),
            other.as_mut_ptr(),
            other.len(),
        );
    };
}

We ran it with:

./scripts/run-kani.sh \
    --path . \
    --kani-args \
    --harness-timeout 1800 \
    --harness verify_seq_set_len \
    -Z uninit-checks

With -Z uninit-checks enabled, Kani reports a verification failure related to uninitialized memory:

Failed Checks:
Undefined Behavior: Reading from an uninitialized pointer

File:
".../library/core/src/lib.rs",
line 360,
in core::kani::mem::assert_is_initialized::<[u8]>

VERIFICATION:- FAILED

This shows that, with memory-initialization checking enabled, Kani is able to detect the problematic call ordering where set_len is called before the corresponding memory has been initialized.

Why Did We Not Get the Same Verification Failure Directly from the split_off Harness?

In principle, after adding the second Safety Requirement to set_len and enabling:

-Z uninit-checks

we would like to run the split_off harness directly and let Kani check the second call:

other.set_len(other_len);

However, in practice, Kani does not complete verification. Instead, it panics during compilation.

The relevant part of the error message is:

Kani was not able to resolve the instance of the function operand ...

Currently, memory initialization checks in presence of
function pointers and vtable calls are not supported.

For more information about planned support, see
model-checking/kani#3300.

Kani then reports:

error: internal compiler error: Kani unexpectedly panicked

Kani unexpectedly panicked during compilation
error: could not compile `alloc` (lib)

Therefore, this is neither a successful nor a failed verification of split_off under -Z uninit-checks. Instead, Kani is currently unable to complete the verification.

On the other hand, if we do not enable:

-Z uninit-checks

the original split_off harness reports:

VERIFICATION:- SUCCESSFUL

However, this result does not establish that the initialization Safety Requirement is satisfied, because the uninitialized-memory tracking required for this property is not enabled in that configuration.

Therefore, the current results can be summarized as follows:

split_off without -Z uninit-checks
    → verification succeeds
    → but the relevant initialization property is not checked

split_off with -Z uninit-checks
    → Kani compiler panics
    → verification is inconclusive

minimal split_off-like sequence with -Z uninit-checks
    → Kani reports an uninitialized-memory UB

Current Conclusion

We currently believe that there are two related issues here.

First, the contract of Vec::set_len should include the second Safety Requirement:

old_len..new_len must already be initialized

Otherwise, the growth case of set_len is not fully verified.

Second, the second call to set_len in Vec::split_off:

other.set_len(other_len);

is made before the destination memory has been initialized by the subsequent:

ptr::copy_nonoverlapping(...)

Therefore, it appears not to satisfy the initialization precondition of set_len.

Using a harness that simulates the call ordering in split_off, we can obtain the following result under -Z uninit-checks:

Undefined Behavior: Reading from an uninitialized pointer

This confirms that Kani's initialization checking is able to detect this class of issue.

However, for the actual split_off harness, we cannot currently obtain a final verification result because enabling -Z uninit-checks causes the Kani compiler to panic.

Therefore, in summary:

The second set_len call in split_off appears to violate the documented initialization precondition of set_len. A minimal harness reproducing the same call sequence is reported by Kani as an uninitialized-memory UB under -Z uninit-checks, while verification of the actual split_off harness cannot currently be completed because the Kani compiler panics.

We would like to confirm how the relationship between the public safety contract of set_len and the internal implementation of Vec should be handled in Challenge 23. @feliperodri