Strip the crate prefix from scanner names so contract metrics match again

[Tianshu-Huang]

All *_under_contract metrics have read 0 since #685: core dropped from 313 to 0 unsafe functions under contract in one run while its contract count didn't change.

Since the nightly-2026-02-05 update (#613), the scanner reports crate-prefixed names (core::ptr::align_offset) but kani list reports ptr::align_offset, so nothing matches. Kani itself strips the prefix (strip_local_crate_prefix); the scanner doesn't.

This applies the same stripping in kani_std_analysis.py, so the metrics are correct regardless of Kani version. Core now reads 307 / 281 / 323 (unsafe / safe-abstraction / safe under contract) instead of 0.

Fixing it in Kani's scanner is another option, happy to do that instead if preferred.

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

[feliperodri]

Merge this, with one addition — and yes, also fix the scanner, but not instead of this.

The scanner is where the bug is: kani list strips the crate prefix and the scanner doesn't, so two Kani outputs disagree. I filed that as model-checking/kani#4868 and tagged you, since you offered.

This PR is still worth keeping permanently, because it solves a different problem. We pin Kani by commit and that pin moves in both directions, so a Kani-side fix leaves metrics wrong on every older pin, including the one on main today. Your shim is correct on both prefixed and already-stripped input, so it does not need reverting once the scanner is fixed.

The one thing to add: unit tests. This is a hand-ported non-trivial algorithm with no test and no way to notice if it drifts from Kani's copy. I ran it against the cases that matter:

core   '<char as core::ascii::AsciiExt>::is_ascii'  -> '<char as ascii::AsciiExt>::is_ascii'   ok
core   'core::core_simd::vector::Simd'              -> 'core_simd::vector::Simd'                ok
core   'ptr::align_offset'                          -> 'ptr::align_offset'                      ok, no-op
core   'alloc::vec::Vec'                            -> 'alloc::vec::Vec'                        ok, other crate
main   'main::main::{closure#0}'                    -> 'main::{closure#0}'                      not idempotent
core   'core::core::foo'                            -> 'core::foo'                              not idempotent

The port is faithful — including the qualifier case, which is why the char scan is needed rather than a removeprefix. The last two are not idempotent, matching Kani's own behaviour, and that is fine today because there is exactly one call site. Please pin all six so it stays that way; the last two are the ones that would break quietly if this ever gets applied twice.