Loop contracts: spurious dereference failures for `for (_, &x) in ...` ref-pattern loops since nightly-2025-10-13 (post rust-lang/rust#145513)

[tautschnig]

I tried this code:

#![feature(stmt_expr_attributes)]
#![feature(proc_macro_hygiene)]

const TABLE: [u8; 16] = [5, 2, 5, 1, 2, 5, 6, 2, 5, 3, 1, 2, 5, 1, 5, 6];

fn f(digits: &[u8; 16], num_digits: usize, a: usize, b: usize) -> usize {
    let num_new_digits: usize = 2;
    let pow5 = &TABLE[a..];

    #[kani::loop_invariant(num_new_digits > 1)]
    for (i, &p5) in pow5.iter().enumerate().take(b - a) {
        if i >= num_digits {
            return num_new_digits - 1;
        } else if digits[i] == p5 {
            continue;
        } else if digits[i] < p5 {
            return num_new_digits - 1;
        } else {
            return num_new_digits;
        }
    }
    num_new_digits
}

#[kani::proof]
fn check() {
    let digits: [u8; 16] = kani::any();
    let num_digits: usize = kani::any_where(|x| *x <= 16);
    let a: usize = kani::any_where(|x| *x < 8);
    let b: usize = kani::any_where(|x| *x >= a && *x <= 16);
    let n = f(&digits, num_digits, a, b);
    assert!(n <= 2);
}

using the following command line invocation:

kani repro.rs -Z loop-contracts

with Kani version: any version pinned to toolchain nightly-2025-10-13 or later, including current main.

I expected to see this happen: verification succeeds (as it does with Kani at commit 415ca50, toolchain nightly-2025-10-09).

Instead, this happened: spurious dereference failures on the for loop head:

Failed Checks: dereference failure: pointer NULL
 File: "repro.rs", line 12, in f
Failed Checks: dereference failure: pointer invalid
Failed Checks: dereference failure: deallocated dynamic object
Failed Checks: dereference failure: dead object
Failed Checks: dereference failure: pointer outside object bounds
Failed Checks: dereference failure: invalid integer address

VERIFICATION:- FAILED

This also breaks the num::dec2flt::decimal_seq harnesses in verify-rust-std once its Kani pin advances past nightly-2025-10-12 (observed in model-checking/verify-rust-std#530, number_of_digits_decimal_left_shift, decimal_seq.rs line 398).

Root cause (bisected to the nightly-2025-10-12 → nightly-2025-10-13 toolchain bump, i.e. rust-lang/rust#145513 "Validate CopyForDeref and DerefTemps better and remove them from runtime MIR"):

Destructuring patterns that go through a reference, like for (i, &p5) in ..., introduce a compiler-generated deref temporary in the pattern-binding block. Before rust-lang/rust#145513 that temporary was assigned via Rvalue::CopyForDeref:

_53 = deref_copy (_24.1: &u8);
_23 = copy (*_53);

LoopContractPass::replace_first_pat_by_nth_pat used the rvalue kind to tell pattern bindings apart from deref temporaries: Use(Copy) assignments sourced from the firstpat variable were paired with their nthpat counterparts and redirected to assign the nthpat projection local, while CopyForDeref assignments kept their left-hand side and only had their rvalue re-pointed at the nthpat variable.

Since rust-lang/rust#145513, the temporary is assigned via a plain copy:

_53 = copy (_24.1: &u8);
_23 = copy (*_53);

so it now takes the pattern-binding path: the map-building pairs _53 with the corresponding nthpat temporary _54 and the rewrite redirects the assignment to _54, leaving _53 uninitialized. The subsequent _23 = copy (*_53) then dereferences a dangling pointer, producing the failures above.

None of the existing tests/expected/loop-contract/for_loop_* tests destructure the iterator element through a reference (&x-style subpattern), which is why the test suite did not catch this.

Fix in preparation.