loop_modifies over a Vec no longer establishes drop_in_place's new reference-creation precondition

[feliperodri]

Context

tests/expected/loop-contract/loop_assigns_for_vec.rs uses loop_modifies over a Vec<u8>, listing the buffer contents and the word holding v.len():

#[kani::loop_invariant(i <= 3)]
#[kani::loop_modifies(&i, slice_from_raw_parts(v.as_ptr(), 12), unsafe {(&v as *const Vec<u8>  as *const usize).add(2)})]
while i < 3 { .. }

Problem

As of nightly-2026-06-01 (#4760) this fails when v is dropped after the loop:

Check 80: std::ptr::drop_in_place::<[u8]>.safety_check.2
	 - Status: FAILURE
	 - Description: "dereference failure: pointer invalid"
	 - Location: core/src/ptr/mod.rs:820:24 in function std::ptr::drop_in_place::<[u8]>

plus a companion "misaligned pointer to reference cast" failure at the same location.

The cause is an upstream change to how drop glue is reached. core::ptr::drop_in_place used to be the lang item, with its body replaced wholesale by the compiler:

// nightly-2026-05-01
unsafe { drop_in_place(to_drop) }

It is now a wrapper around a new drop_glue lang item, and it takes a reference to get there:

// nightly-2026-06-01
unsafe { drop_glue(&mut *to_drop) }

Creating that &mut *to_drop asserts the pointee is aligned and valid. So dropping through a raw pointer now carries a precondition it did not before, and the loop contract has to establish it. loop_modifies havocs the word holding v.len() while the invariant only constrains i, so after the loop v has an unconstrained length and the reference creation fails.

Verified this is genuinely new behaviour rather than pre-existing fragility: the same test passes when the parent commit is rebuilt against nightly-2026-05-01. Also verified that Vec's internal layout is unchanged, so the test's hard-coded .add(2) offset for len is still correct (a probe confirms word 2 holds len and word 0 holds the capacity).

Why it is not fixed in #4760

The natural fix is to strengthen the invariant so it pins what the drop needs:

#[kani::loop_invariant(i <= 3 && v.len() == i * 3 + 3)]

That is rejected with Rust intrinsic assumption failed, so expressing the needed fact appears to be a loop-contracts limitation rather than something the toolchain upgrade can address. #4760 renames the test to loop_assigns_for_vec_fixme.rs so the upgrade is not blocked, with the analysis recorded in the file.

Suggested next steps

• Determine why v.len() (or an equivalent formulation over the havoced length word) cannot appear in a loop_invariant, and whether that is a fixable restriction.
• Once expressible, restore the test to loop_assigns_for_vec.rs.
• Worth checking whether other loop_modifies uses over heap containers have the same latent gap — this was the only failure in the expected suite, but the new drop_in_place precondition applies to every drop through a raw pointer.

[feliperodri]

Surfaced by #4760 (the nightly-2026-06-01 upgrade), which renames the test to loop_assigns_for_vec_fixme.rs so the upgrade is not blocked.