[rominf]

• If this PR fixes a bug, searched tests/e2e-cucumber/expectations.toml for the fixed ticket ID and removed/narrowed any now-stale xfail rows. — N/A, test-only.
• If this PR adds a new subcommand or subsystem, its domain implementation lives in its own file per docs/architecture.md. — N/A.
• Every new or changed user-facing message was read against the code path that runs after it, and its test asserts the resulting state — not only the wording — per AGENTS.md §3. — N/A, no message changes.

Summary

rocm examine judges the driver side of a host with a few small text readers. Each one now has a property whose oracle is stated independently of the code:

Reader	Property	Oracle
distro_clears_wsl_floor	a newer Ubuntu release is never less supported than an older one	monotonicity
mode_access	read/write access comes from the owner, else group, else other class of a stat -c %A string (with or without the ACL +)	POSIX class precedence, read independently from the string
line_blacklists_amdgpu	blacklist amdgpu is recognized, but not when commented out and not for amdgpu_foo, amdgpufoo, amdgpu2, radeon or amdkfd	modprobe.d grammar
parse_iommu_param	iommu= is read from its own token, never from amd_iommu= or intel_iommu=	whitespace-separated cmdline tokens
normalize_therock_family	every spelling of a reported gfx target (case, :xnack- suffix, trailing whitespace) normalizes to a family in known_therock_families(), and normalizing again changes nothing	the recognized-family set

None of them found a defect, so they are regression guards. They extend the existing example tests (iommu_param_parsed_from_cmdline, blacklist_amdgpu_detection, mode_access_owner_group_other_precedence, known_therock_families_all_round_trip) from a few hand-picked inputs to the whole input alphabet.

The iommu= generator deliberately never produces two iommu= tokens. Which one takes effect is the kernel's decision, not a tokenization property, and pinning the current first-match behaviour would make a correct change look like a regression.

Reach

inputs_reach_every_region draws 2048 inputs from each strategy with a deterministic RNG and requires each region to appear in at least 5% of draws:

• WSL floor: pairs straddling the floor 999, both above it 755
• mode_access: owner class 1034, group class 478 (other is the rest)
• blacklist: real blacklist 259, not a blacklist 1789
• iommu: iommu= present 1053, only look-alike parameters 749
• targets: with a feature suffix 554, upper case 989

Mutation testing

Each mutant turned its property red and was then restored:

Mutation	Result
mode_access checks the group before the owner	fails
parse_iommu_param matches iommu= anywhere in a token	fails (amd_iommu=… read as iommu=)
line_blacklists_amdgpu accepts any module starting with amdgpu	fails (shrinks to blacklist amdgpu_foo)
WSL floor stops clearing at Ubuntu 30	fails ((24, 4) clears the floor but the newer (30, 4) does not)

Ignored reproducer, tied to #506

blacklistamdgpu (no whitespace after the directive) is read as a blacklist. That is #506. The blacklist property's separator alphabet therefore excludes the empty separator. A separate test, a_blacklist_directive_needs_whitespace_before_the_module, is #[ignore]d with (#506) in the reason; it still fails on this base. The fix for #506 should un-ignore it and can then let the property draw an empty separator.

Relationship to #521

This comes from a property-testing pass over GPU classification. Everything in that pass about APU classification — the lspci/marketing-name/rocminfo/Windows-row properties, the corpus sweeps, the Raphael + RX 7900 XTX diagnose test and the vram_capacity_is_meaningful test — is already in #521 and was dropped from here. What remains is the driver-side readers, which #521 does not touch.

The new module is examine_driver_proptests.rs (#521 adds examine_proptests.rs), declared at the end of examine.rs, so the two PRs do not overlap. examine.rs merges cleanly with #521. The family property also holds after #521, which adds gfx90c as its own family in both normalize_therock_family and known_therock_families().

Determinism, runtime, platforms

• The reach test is deterministic. The properties use proptest's default seeding; any failure is saved to proptest-regressions/ as usual. PROPTEST_CASES raises the case count (default 256).
• The whole module runs in under 0.5 s.
• Platform-independent pure functions; no filesystem access.

AGENTS.md §3

This is a test-only change: it changes no CLI output, exit code, file layout or runtime selection, so no Gherkin scenario is needed.

Verification

• cargo test --locked -p rocm-core: exit 0 (478 passed, 1 ignored)
• cargo clippy --locked --workspace --all-targets -- -D warnings: exit 0
• cargo clippy --locked -p e2e-cucumber --test e2e -- -D warnings: exit 0
• cargo fmt --all --check, cargo xtask manifest --check, cargo xtask tpn --check, cargo xtask check-crate-edges: exit 0

[jussielo-amd]

Nice, careful piece of work. Traced each property (mode_access owner/group/other precedence, the blacklist grammar, iommu= tokenization, the WSL floor, and the gfx-family normalize/round-trip) against the actual implementation by hand, and the oracles all check out independently of the code — no vacuous generators, no off-by-one in the permission-class indices, and the inputs_reach_every_region hit-rate math holds up with real margin. Ran the suite plus clippy and fmt locally and everything's clean, matching the PR description. The #506 pin and the #521 scoping note both check out against the live issue/PR too.

One small nice-to-have: GFX_TARGETS doesn't include a gfx125x example, so that branch of normalize_therock_family isn't exercised by this property test (the existing example test still covers it, so no real gap). Not blocking.

Approving.

[rominf]

Following up the non-blocking note on the review: #628 adds gfx1250 to GFX_TARGETS, so the family property now reaches the gfx125* arm of normalize_therock_family. Deleting that arm now fails the property with minimal input "gfx1250"; before, the same mutation passed it.