You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
#4716 added an assumption of a type's layout niche after each nondeterministically generated value, so that autoharness stops producing language-level-invalid values for ranged scalar types (e.g. a date type packing a validated ordinal) and stops reporting the resulting false alarms.
The toolchain upgrade to nightly-2026-06-01 (#4757) removed rustc_layout_scalar_valid_range_start/_end in favour of pattern types — the same move core::num::niche_types made upstream. A ranged scalar newtype is now written as:
#[repr(transparent)]pubstructMonth(std::pat::pattern_type!(u8 is 1..=12));
Problem
A pattern type is not an ADT and has no Arbitrary implementation, so can_derive_arbitrary cannot synthesize a struct that has one as a field. Every locally-defined ranged newtype is therefore skipped rather than harnessed:
So the niche assumption, which is the thing #4716 added, no longer applies to the user-defined types it was aimed at. It still works end to end for std::time::Duration, whose Nanoseconds field carries the same kind of range and which does get harnessed — that is the motivating real-world case from the #3832 triage, so the feature is not dead, just much narrower than intended.
tests/script-based-pre/autoharness_niche pins both halves (the working Duration/NonZeroU8 cases and the skipped local ones) so this limitation is asserted by a test rather than silently regressing further.
Proposed fix
Teach autoharness to generate values for pattern-type fields. The pieces already exist:
scalar_niche (added in Autoharness: assume layout niches of generated scalar values #4716, kani-compiler/src/kani_middle/mod.rs) already computes the (bits, start, end) valid range from the layout, and a pattern type's layout carries exactly that restricted range.
call_kani_any_for_ty already knows how to generate a base integer and how to emit kani::assume for a niche.
So generating a pattern_type!(u8 is 1..=12) is: generate the base integer with kani::any, assume scalar_niche's range, and transmute. Concretely that means:
can_derive_arbitrary accepting RigidTy::Pat whose base type is generatable.
call_kani_any_for_ty gaining a RigidTy::Pat arm that generates the base type and applies assume_scalar_niche to the result.
Both are sound in the same sense #4716 argued: the assumed range is a necessary condition of the pattern type's validity, so no valid value is excluded.
Acceptance
tests/script-based-pre/autoharness_niche should move its local ranged types (Month, Schedule, PosI8, and check_monthly::<Month>) out of the skipped table and back into the verified table, with the cover checks still confirming the range extremes remain reachable (i.e. no over-constraining).
Context
#4716 added an assumption of a type's layout niche after each nondeterministically generated value, so that autoharness stops producing language-level-invalid values for ranged scalar types (e.g. a date type packing a validated ordinal) and stops reporting the resulting false alarms.
The toolchain upgrade to
nightly-2026-06-01(#4757) removedrustc_layout_scalar_valid_range_start/_endin favour of pattern types — the same movecore::num::niche_typesmade upstream. A ranged scalar newtype is now written as:Problem
A pattern type is not an ADT and has no
Arbitraryimplementation, socan_derive_arbitrarycannot synthesize a struct that has one as a field. Every locally-defined ranged newtype is therefore skipped rather than harnessed:So the niche assumption, which is the thing #4716 added, no longer applies to the user-defined types it was aimed at. It still works end to end for
std::time::Duration, whoseNanosecondsfield carries the same kind of range and which does get harnessed — that is the motivating real-world case from the #3832 triage, so the feature is not dead, just much narrower than intended.tests/script-based-pre/autoharness_nichepins both halves (the workingDuration/NonZeroU8cases and the skipped local ones) so this limitation is asserted by a test rather than silently regressing further.Proposed fix
Teach autoharness to generate values for pattern-type fields. The pieces already exist:
scalar_niche(added in Autoharness: assume layout niches of generated scalar values #4716,kani-compiler/src/kani_middle/mod.rs) already computes the(bits, start, end)valid range from the layout, and a pattern type's layout carries exactly that restricted range.call_kani_any_for_tyalready knows how to generate a base integer and how to emitkani::assumefor a niche.So generating a
pattern_type!(u8 is 1..=12)is: generate the base integer withkani::any, assumescalar_niche's range, and transmute. Concretely that means:can_derive_arbitraryacceptingRigidTy::Patwhose base type is generatable.call_kani_any_for_tygaining aRigidTy::Patarm that generates the base type and appliesassume_scalar_nicheto the result.Both are sound in the same sense #4716 argued: the assumed range is a necessary condition of the pattern type's validity, so no valid value is excluded.
Acceptance
tests/script-based-pre/autoharness_nicheshould move its local ranged types (Month,Schedule,PosI8, andcheck_monthly::<Month>) out of the skipped table and back into the verified table, with the cover checks still confirming the range extremes remain reachable (i.e. no over-constraining).