panic: `-Z valid-value-checks` ICEs on any allocating function: fat-pointer pattern type in `NonNull<[u8]>`

[feliperodri]

Summary

Under -Z valid-value-checks, any function that allocates — anything touching Box, Vec, or String — panics the compiler. ty_validity_per_offset asserts that a pattern type always has a scalar ABI, but NonNull<[u8]>'s field is pattern_type!(*const [u8] is !null): a fat pointer, so its layout is ScalarPair, and the assertion fires. The allocation shims have taken NonNull<[u8]> since nightly-2026-03-21, so RawVec drags this in.

Reproduction

boxonly.rs, with no pattern types anywhere in it:

pub fn takes_box(b: Box<u32>) -> u32 { *b }

kani autoharness -Z autoharness -Z valid-value-checks boxonly.rs

thread 'rustc' panicked at kani-compiler/src/kani_middle/transform/check_values.rs:959:9:
expected pattern type to have a scalar ABI: Ty { id: 99, kind: RigidTy(Pat(Ty { id: 100,
kind: RigidTy(RawPtr(Ty { id: 46, kind: RigidTy(Slice(Ty { id: 29, kind: RigidTy(Uint(U8)) })) },
Not)) }, NotNull)) }

Kani unexpectedly panicked during compilation.

Kani 0.68.0 built from 80f3cc98a (current main), CBMC 6.10.0, nightly-2026-08-21. Also reproduces on #4780's head, whose check_values.rs is unmodified — this is not that PR's doing.

Where

kani-compiler/src/kani_middle/transform/check_values.rs:945-964. The Pat branch rejects char bases, then asserts:

assert!(
    matches!(layout.abi, ValueAbi::Scalar(..)),
    "expected pattern type to have a scalar ABI: {ty:?}"
);

The comment above it says "its base type is always a scalar", which does not hold for a raw pointer to an unsized pointee: *const [u8] and *const dyn Trait are ScalarPair (data pointer + metadata).

Impact

-Z valid-value-checks is unusable on essentially any real program, since allocating is enough to reach it. It is a panic rather than a diagnostic, so there is no way to work around it short of dropping the flag.

Suggested fix

Either handle the pair case — for !null over a fat pointer the constraint applies to the data-pointer half at offset 0, pointer-width — or, conservatively, return Err("Unsupported pattern type over a fat pointer") the way the char case does, so it degrades to a reported unsupported construct instead of an ICE.

Notes

Found while reviewing #4780, whose new test runs with -Z valid-value-checks; it does not hit this because its probe does not allocate. Likely blocks the NonNull autoharness follow-up described there, and may share a root cause with the assert_is_non_null_like failure reported in #4799 (comment).