Challenge 23: Verify Vec Part1 safety with Kani

[v3risec]

Summary

This PR adds Kani verification for the Vec APIs listed in Challenge 23.

Coverage: 36 / 36 Challenge 23 entries targeted.

The verification combines:

• contracts for unsafe raw-parts, length, append, and spare-capacity APIs;

• executable harnesses for safe and internal Vec operations;

• symbolic Vec states with symbolic length, capacity, ranges, indices, and operation counts;

• loop contracts for operations that require induction;

• explicit panic-path and allocation-growth coverage.

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

Unbounded verification

Except for extend_desugared and extend_trusted, the Challenge 23 target harnesses do not impose a fixed element-count bound and do not use #[kani::unwind].

The main proofs therefore operate over symbolic logical lengths rather than small fixed-size Vecs. Loops are either verified directly or discharged with loop contracts.

Non-ZST allocations are restricted by MAX_ALLOCATION_BYTES so that one symbolic allocation remains representable in CBMC's object model. This is a verifier representation bound rather than a small semantic Vec-length bound. ZST logical lengths remain symbolic over usize.

The two exceptions are documented limitations:

• extend_desugared is verified by bounded unwinding of the exact shipped implementation. An unbounded loop-contract proof is currently blocked by reallocation/free/provenance state across induction and by Kani issue #4796 for method calls in loop invariants.

• extend_trusted is also verified by bounded unwinding of the exact shipped implementation. Its loop is hidden inside Iterator::for_each / fold; an explicit repeated-next proof requires a TrustedLen state relation that currently runs into the same loop-invariant limitations.

These two proofs intentionally prefer bounded verification of the shipped implementation over claiming an unbounded proof of a verification-only replacement.

Contracts

Contract-backed APIs 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

The raw-parts contracts cover length/capacity consistency, alignment, allocation size, writable capacity, allocation-base/provenance requirements, and the initialized prefix.

For from_raw_parts, from_parts, and from_parts_in, the exact one-past-allocation check requires kani::mem::is_inbounds. The tool-independent safety-contract API currently has no equivalent predicate, so only that clause uses kani::requires; the remaining preconditions use safety::requires.

set_len includes both documented safety requirements: new_len <= capacity and initialization/validity of the newly exposed prefix when growing.

Harness coverage

Harnesses cover:

• raw-parts reconstruction and decomposition;

• boxed-slice and array conversions;

• truncate, swap_remove, insert, remove, push, push_within_capacity, pop, and clear;

• append, drain, split_off, and extract_if;

• extend_from_within, extend_with, spec_extend_from_within, extend_desugared, and extend_trusted;

• spare_capacity_mut, split_at_spare_mut, and split_at_spare_mut_with_len;

• Deref, DerefMut, IntoIterator, and Drop;

• normal and representative panic/overflow paths.

The current revision also covers both existing-spare and allocation-growth paths where applicable instead of assuming reallocation away.

Kani-only loop reshaping

Most targets execute the shipped implementation directly. Two functions still contain narrowly scoped Kani-only reshaping needed for unbounded loop contracts:

• dedup_by predeclares scalar/raw-pointer loop temporaries so they can be named by loop_modifies. The same values are recomputed before use, and predicate calls, drops, copies, branches, and length updates remain unchanged.

• extend_with expresses the shipped for _ in 1..n clone loop as an explicit counter loop. Both forms execute the same n - 1 clone/write/length-update operations for n > 0, zero for n == 0, followed by the same final write.

These are intended as semantics-preserving proof reshaping, not abstract replacements of the target behavior. They are documented in the source together with the pinned-Kani limitations that require them.

If required, supplementary shipped-text evidence can be added for these transcriptions.

append_elements

append_elements is verified with a direct #[kani::proof] rather than #[kani::proof_for_contract].

Its call to reserve may replace the backing allocation and free the old buffer. The pinned Kani function-contract interface can express writable modifies regions, but cannot express the corresponding frees frame needed for reallocation. The direct harness therefore executes the real function while retaining both:

• no-growth executions; and

• growth/reallocation executions.

The explicit non-overlap assumption is the documented unsafe-call precondition.

Symbolic Vec model

verifier_nondet_vec generates valid symbolic Vec states with symbolic capacity and logical length.

Pre-existing element contents are intentionally treated as opaque and initialized with a shape-valid repeated byte pattern, avoiding another unbounded initialization loop before every target proof.

The verified Vec internals generally do not branch on those stored values. Predicate-driven APIs such as retain_mut, dedup_by, and extract_if use nondeterministic predicate outcomes, over-approximating possible keep/remove/equality decision sequences. Values supplied through API arguments and iterators remain independently symbolic.

Representative element shapes currently cover ZSTs, ordinary scalar layouts, validity-constrained bool, and fixed-size aggregates.

Generic T

Harness bodies are written generically but Kani proof entry points are instantiated over representative concrete shapes.

Therefore this PR does not claim to literally satisfy the Challenge wording of "generic T (no monomorphization)". This is the same tool-level/project-policy question discussed for Challenge 25 / #681 and other generic collection challenges.

Challenge 23 naming

Some Challenge 23 names differ from the current repository API. This PR follows the checked-in source:

• from_nonnull → Vec::from_parts

• from_nonnull_in → Vec::from_parts_in

Private targets 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.

Verification

All added Challenge 23 harnesses pass locally with the pinned Kani configuration.

The remaining documented limitations are primarily:

1. literal generic-T / no-monomorphization support;

2. bounded shipped-code proofs for extend_desugared and extend_trusted;

3. the two narrowly scoped Kani-only loop reshaping cases described above.

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

[feliperodri]

Thanks @v3risec. Reviewed Challenge 23 with our vacuity tooling. Broad coverage (35/35), but soundness issues block acceptance:

1. 5 cfg(kani) body swaps (T1) — critical. Kani verifies alternate bodies for spec_extend_from_within, extend_desugared, extend_trusted, extend_with, and dedup_by. The verified artifact is not the shipped code.
2. Pervasive kani::assume(false) cutoffs. In extend_desugared the reserve/grow path is short-circuited with if len == cur_cap { kani::assume(false); } and the iteration bound is capped (if raw_max_write > 8 { assume(false); }); extend_trusted uses assume(false) on TrustedLen-yields-None early. Plus overflow branches for checked_add and layout representability. These skip the interesting failure branches rather than verifying them.
3. Assume-the-conclusion inside verified bodies: kani::assume(kani::mem::can_write(len_ptr)) and can_write(spare_write_set) are placed inside the fn being verified — assumes the memory-access safety property.
4. set_len contract is under-specified: #[requires(new_len <= self.capacity())] omits the initialized-prefix requirement the safety docstring calls out.
5. Fails unbounded+generic-T universally (monomorphized ~14 concrete types; retain_mut/dedup_by/extend_desugared etc. bounded MAX_VEC_LEN=4).
6. verifier_nondet_vec fills the buffer with a single symbolic byte pattern (ptr::write_bytes(..., kani::any::<u8>(), size_of::<T>() * sz)), so all elements share the same byte value — swap_remove/dedup_by/retain_mut can't exercise element-to-element differentiation.

Between the two open Challenge 23 solutions we're prioritizing #569 as the sounder shell (no body swaps), though it too is incomplete (hardcoded ARRAY_LEN=3, monomorphized i32). Please replace the body swaps with loop contracts on the real bodies and drop the assume(false)s.

[v3risec]

@feliperodri Thanks for the detailed review. I have substantially reworked this PR.

Changes since the previous review

The main soundness issues have been addressed:

• All kani::assume(false) cutoffs have been removed.

• Memory-safety conclusions such as can_write(...) are no longer assumed inside verified implementations; they are asserted when needed.

• set_len now requires the grown prefix to contain initialized valid Ts, and its harness covers grow / shrink / unchanged cases.

• append_elements no longer assumes enough spare capacity; both no-growth and reallocation paths are covered.

• split_off's panic harness now uses the strict at > len boundary.

• from_parts / from_parts_in require alignment unconditionally.

• extend_desugared, extend_trusted, and spec_extend_from_within now execute the shipped implementation under Kani rather than a verification-only replacement.

The raw-parts contracts also now encode the allocation base, writable capacity, exact allocation size/end, and initialized prefix requirements.

Unbounded verification

A major improvement in the current revision is that all Challenge 23 target families except extend_desugared and extend_trusted are verified without an explicit element-count bound and without #[kani::unwind].

Lengths, capacities, indices, ranges, and operation counts remain symbolic, and loops that require induction are discharged using loop contracts. Non-ZST allocations are restricted by a CBMC object-model limit (MAX_ALLOCATION_BYTES). This is a verifier representation bound rather than a small fixed Vec-length bound.

The two exceptions are currently:

extend_desugared: bounded shipped-code proof
extend_trusted:   bounded shipped-code proof

I am intentionally documenting these as limitations rather than claiming they satisfy the unbounded requirement.

Remaining cfg(not(kani)) reshaping

After the changes above, only dedup_by and extend_with still contain meaningful Kani-only source reshaping.

dedup_by

This is not an alternate deduplication algorithm. Kani only extends the storage lifetime of several usize / bool / raw-pointer loop temporaries so that they can be named by loop_modifies.

Each value is recomputed from the same expression before use, and the actual operations remain unchanged:

• same_bucket,

• drop_in_place,

• copy_nonoverlapping,

• index updates,

• and FillGapOnDrop.

This is required because the pinned loop-contract implementation cannot express body-local mutable temporaries in the loop frame.

extend_with

The shipped code uses:

for _ in 1..n {
    ptr::write(ptr, value.clone());
    ptr = ptr.add(1);
    local_len.increment_len(1);
}

The Kani branch exposes the same iteration as an explicit counter loop so that a loop contract can be attached.

For n > 0, both execute exactly n - 1 clone/write/length-update steps; for n == 0, both execute zero. The final write of the original value is shared.

The reason is the pinned Kani lowering of contracted for ranges into verifier iterator/index state, which makes the 1..n case and its loop frame problematic.

I can add supplementary bounded shipped-text harnesses if the reviewer wants machine evidence in addition to this structural equivalence argument.

Why the other two targets are bounded

extend_desugared

The real loop can call reserve, so an unbounded loop-contract proof must preserve allocation identity/provenance across possible reallocation and freeing of the old buffer. At the current Kani pin, loop abstraction does not preserve enough of this state to prove the next iteration reliably.

The natural invariant also needs accessors such as capacity(), but method calls in loop invariants are affected by model-checking/kani#4796, where calls may be lowered with missing arguments and replaced by nondeterministic values.

For that reason, the current harness uses bounded unwinding but executes the exact shipped implementation, including reserve/reallocation paths.

extend_trusted

The shipped loop is hidden inside Iterator::for_each / fold, so there is no source-level loop where a loop contract can be attached.

An explicit repeated-next() transcription requires preserving:

remaining iterator length == additional - written

through induction. Expressing that naturally requires iterator methods such as size_hint(), which again runs into #4796.

Rather than use assume(false) or claim an alternate loop is the shipped implementation, the current proof executes the actual for_each path with bounded unwinding.

Reviewer guidance requested

If a narrowly scoped, semantics-preserving cfg(kani) transcription is acceptable when:

• normal builds retain the shipped implementation,

• no safety conclusion is assumed,

• the operation order and memory effects are preserved,

• the Kani limitation is documented,

• and bounded shipped-text evidence can be added,

then I can continue pursuing unbounded proofs for these two targets.

Otherwise, I would prefer to keep the current bounded proofs of the real implementation and document the limitation explicitly.

kani::mem::is_inbounds contracts

from_raw_parts, from_parts, and from_parts_in need to prove that ptr + capacity is the exact one-past endpoint of the allocation.

The tool-independent safety::requires predicates can express the allocation-base, same-allocation, writability, alignment, size, and initialized-prefix requirements, but currently have no equivalent for:

kani::mem::is_inbounds(...)

Therefore only this exact-endpoint clause uses kani::requires; the rest of the contracts remain tool-independent.

Why append_elements uses #[kani::proof]

append_elements calls reserve, which may replace the backing allocation and free the old one. The pinned Kani function-contract interface can express writable modifies regions, but not the corresponding frees behavior needed to model reallocation soundly. Using proof_for_contract would therefore either give an incomplete frame or require excluding the growth path.

The direct proof instead executes the real implementation and covers both no-growth and reallocation paths. The explicit non-overlap assumption is the documented unsafe-call precondition, not a safety conclusion of the implementation.

verifier_nondet_vec

Pre-existing values are intentionally treated as opaque. The generator uses a shape-valid repeated byte pattern instead of adding another unbounded initialization loop before every target proof. This does not represent every possible per-element value combination.

However, the verified Vec internals generally do not branch on existing element values. Predicate-driven APIs such as:

• retain_mut,

• dedup_by,

• extract_if

use nondeterministic predicate results, which over-approximate possible keep/remove/equality decision sequences. Values supplied as API inputs or iterator items remain independently symbolic.

Generic T

As with #681, the harness bodies are instantiated over representative element shapes because Kani proof entry points are monomorphized.

I do not claim that this literally satisfies the Challenge wording of "generic T (no monomorphization)". I believe this is the same project-level question already raised for Challenge 25 and the other generic collection challenges.

Items requiring reviewer guidance

The remaining questions are therefore:

1. Are the narrowly scoped dedup_by / extend_with Kani reshaping cases acceptable with the documented equivalence argument, optionally supplemented by shipped-text machine evidence?

2. If so, can the same approach be used to continue pursuing unbounded proofs for extend_desugared and extend_trusted, where the shipped source currently cannot carry a sound usable loop contract at this Kani pin?

Thanks again for the detailed review and guidance.

[v3risec]

A small follow-up to my previous comment: I have also strengthened the representative-type coverage.

I added a non-Copy, needs_drop WithDrop shape to exercise ownership- and drop-sensitive paths, including removal, retain/dedup, append/split, iterator ownership transfer, flattening, and the bounded extend targets. Compiler-generated slice-drop paths such as Vec::drop, truncate, clear, and Drain::drop are covered separately with supplementary bounded harnesses.

I also added a CloneOnly shape to force spec_extend_from_within / extend_from_within through the default per-element Clone implementation rather than only the TrivialClone / copy_nonoverlapping specialization. That default iterator path currently uses bounded supplementary evidence because its loop is hidden inside zip / map / for_each.

These additions do not change the unbounded status described in my previous comment; they are supplementary coverage for needs_drop, non-Copy, and default-specialization behavior.