Scanner CSVs report crate-prefixed names while kani list does not #4868

Summary

Kani now emits two different names for the same function. kani list reports ptr::align_offset; the scanner's CSVs report core::ptr::align_offset. Anything that joins the two artifacts silently matches nothing.

Cause

rust-lang/rust#149401 changed CrateDef::name() to include the crate prefix. kani-compiler compensates — strip_local_crate_prefix in kani_middle/mod.rs:66 — so kani list is unaffected. tools/scanner calls item.name() / def.name() / fn_item.name() directly and inherited the prefix without anyone choosing it.

Impact

model-checking/verify-rust-std joins these two artifacts to compute contract coverage. Every *_under_contract metric there has read 0 since the divergence: core went from 313 unsafe functions under contract to 0 in a single run, with no change to the contracts themselves.

Suggested fix

Strip the prefix where the names are created, not per-CSV — the names reach at least five dump_csv calls (analysis.rs:84, 140, 167, 219, 230), so fixing one output would leave the others inconsistent.

The wrinkle is that strip_local_crate_prefix lives in kani-compiler and tools/scanner does not depend on it, so the helper needs extracting into a crate both can reach. Please don't hand-port it: the algorithm has a non-obvious rule distinguishing a crate-root qualifier (droppable) from a path continuation segment that merely shares the crate's name, and it must handle the prefix appearing inside a type qualifier such as <char as core::ascii::AsciiExt>::is_ascii. A second copy will drift.

Not urgent for verify-rust-std

They are landing a defensive shim on their side (model-checking/verify-rust-std#696), because they pin Kani by commit and need older pins to keep producing correct metrics. That shim is a no-op on already-stripped names, so it stays correct after this is fixed and does not need reverting. This issue is about Kani's own two outputs disagreeing, which will bite the next consumer that joins them.

@Tianshu-Huang offered to fix this on the Kani side in that PR — flagging for them.