Nested transparent wrapper pointer casts produce incorrect projection chains

Problem

Pointer casts involving nested transparent wrappers around arrays (e.g., *const [u8; 2] → *const W2(W1([u8; 2]))) produce incorrect projection chains that get stuck during traversal.

The #pointeeProjection function's source-first strategy correctly handles single-layer wrappers via the lookupTy(FIELD) ==K SRC guard, but for nested wrappers the immediate inner type doesn't match the source array, so the guard fails and the array unwrap fires first, producing an uncancelable projectionElemSingletonArray tail.

Reproducer

#[derive(Clone, Copy)]
struct W1([u8; 2]);

#[derive(Clone, Copy)]
struct W2(W1);

fn main() {
    let arr: [u8; 2] = [11, 22];
    let w: W2 = unsafe { *((&arr) as *const [u8; 2] as *const W2) };
    assert_eq!((w.0).0, [11, 22]);
}

Running kmir prove on this program produces 2 stuck nodes (one from the alignment check ND branch per #638, and one from the bad projection chain).

Root Cause

In types.md, the specialized rule:

rule #pointeeProjection(SRC:TypeInfo, typeInfoStructType(_NAME, _ADTDEF, FIELD .Tys, LAYOUT))
    => maybeConcatProj(projectionElemWrapStruct, #pointeeProjection(SRC, lookupTy(FIELD)))
    requires #isArrayType(SRC) andBool #zeroFieldOffset(LAYOUT) andBool lookupTy(FIELD) ==K SRC
    [priority(42)]

Only matches when the struct's immediate inner type equals the source. For W2(W1([u8;2])), lookupTy(FIELD) returns W1_info ≠ [u8;2]_info, so the guard fails.

The correct projection for this cast would be WrapStruct + WrapStruct (wrap into W1, then into W2), which requires multi-level lookahead that the current one-step guard cannot provide.

Status

This is a pre-existing bug — it also fails on master (before PR #988's source-first refactoring). The source-first strategy did not introduce this regression.

Related

• #638 (alignment check ND branch — the other stuck node)
• PR #988 (source-first #pointeeProjection refactoring)

Read types.md and trace #pointeeProjection, especially the source-first rule and its lookupTy(FIELD) guard. Run kmir prove on the nested W1/W2 reproducer and verify that the projection chain contains two struct wraps and no bad array tail; the separate alignment-check node from #638 may remain.