fix(extract): derive RQN from SCIP module chain to resolve test/impl collisions

[mpenciak]

Summary

• RQN derivation: derive_rust_qualified_name now parses the module chain from the SCIP symbol instead of reconstructing it from the filesystem path. The path-based approach silently dropped inline mod tests and nested mod inner {} segments, so a #[test] fn foo() inside mod tests collapsed to the same RQN as an outer fn foo() in the same file.
• Charon match key: charon_names::make_match_key_from_atom used (file-derived module, bare display_name) as its key, re-introducing the same collision one layer down — a #[test] fn mul() and a Scalar52::mul impl in the same file shared a key, so the test atom silently inherited Charon's RQN for the real method. The key now derives from the atom's SCIP-correct RQN, preserving the ::test:: segment.
• Schema cleanup: the now-redundant pkg_name parameter is removed from derive_rust_qualified_name and convert_to_atoms_* (the SCIP symbol already carries the crate name).

Why this matters

probe-aeneas's strategy_rust_qualified_name (translate.rs:135) and enrich_with_aeneas_metadata (extract.rs:634) key on rust-qualified-name. With the collision:

• Both the test atom and the verified non-test atom mapped to the same RQN in funs_rust_names, so both got is-disabled: false / is-relevant: true — test atoms that should have been hidden leaked into downstream tooling.
• Strategy 1's disambiguator could route the Lean translation to the wrong atom, leaving the real verified function with no verification-status and showing up as unverified in the frontend.

End-to-end verification against curve25519-dalek

All 10 previously-colliding test atoms now have distinct, correct RQNs:

Atom	Before	After
backend/serial/u64/scalar/test/mul	...::scalar::{...Scalar52}::mul	...::scalar::test::mul
backend/serial/u64/scalar/test/add	...::scalar::{...Scalar52}::add	...::scalar::test::add
backend/serial/u64/scalar/test/sub	...::scalar::{...Scalar52}::sub	...::scalar::test::sub
backend/serial/u64/scalar/test/from_bytes_wide	...::scalar::{...Scalar52}::from_bytes_wide	...::scalar::test::from_bytes_wide
backend/serial/u64/scalar/test/montgomery_mul	...::scalar::{...Scalar52}::montgomery_mul	...::scalar::test::montgomery_mul
edwards/test/is_small_order	...::edwards::{...EdwardsPoint}::is_small_order	...::edwards::test::is_small_order
edwards/test/mul_base_clamped	...::edwards::{...EdwardsPoint}::mul_base_clamped	...::edwards::test::mul_base_clamped
montgomery/test/mul_base_clamped	...::montgomery::{...MontgomeryPoint}::mul_base_clamped	...::montgomery::test::mul_base_clamped
scalar/test/from_bytes_mod_order_wide	...::scalar::{...Scalar}::from_bytes_mod_order_wide	...::scalar::test::from_bytes_mod_order_wide
scalar/test/reduce	...::scalar::{...Scalar}::reduce	...::scalar::test::reduce

Non-test impl methods (Scalar52::mul, EdwardsPoint::is_small_order, Scalar::reduce, etc.) still resolve to their correct Charon-style RQNs.

Test plan

• cargo fmt --all
• cargo clippy --all-targets -- -D warnings
• cargo test (143 lib tests pass, up from 140 — added 3 new regression tests covering inline mod tests, inline submodules, and the Charon match-key collision)
• End-to-end re-extraction on curve25519-dalek-lean-verify confirms all 10 colliding atoms now get distinct RQNs while non-test impl methods retain their Charon-enriched RQNs
• Confirmed in curve25519-dalek-lean-verify that the 10 test probes now flip to is-disabled: true after running probe-aeneas

🤖 Generated with Claude Code