Repository navigation
Description
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) 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)]
pub struct Month(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:
| niche_probe | days_left_in_year | Missing Arbitrary implementation for argument(s) s: Schedule |
| niche_probe | signed_niche | Missing Arbitrary implementation for argument(s) p: PosI8 |
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_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 with kani::any, assume scalar_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_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).
Activity
feliperodri commentedon Aug 25, 2026
Surfaced by #4760 (the
nightly-2026-06-01upgrade), which converts the affected tests to pattern types and pins the reduced reach intests/script-based-pre/autoharness_nicheso it cannot regress further unnoticed.Upgrade Rust toolchain to nightly-2026-06-01 (model-checking#4760)
Autoharness: support pattern types (RigidTy::Pat)
Autoharness: support pattern types (RigidTy::Pat)
Autoharness: support pattern types (RigidTy::Pat) (model-checking#4780)