Preserve module paths in generated function names

[fallintoplace]

This fixes a namespace regression in Anneal's function generation.

Root cause:
generate_function rebuilt a temporary ParsedLeanItem with an empty module_path when it needed the Aeneas call name and namespace. For nested functions, that dropped the containing modules from the fully-qualified name used in generated proof tactics, so references could come out as _root_.crate.fn instead of _root_.crate.mod.fn.

What changed:

• make function generation consume the real ParsedLeanItem from the parser/generator pipeline
• derive the Aeneas function name, namespace, and spec name from the actual item instead of a synthetic one
• keep a small test-only helper for root-path function generation so the existing unit tests stay lightweight
• add a regression test that checks nested module paths are preserved in generated proof tactics

Impact:

• generated verify_is_valid and verify_user_bound calls now point at the correct nested function name
• nested functions no longer lose their module path during Lean generation
• future refactors have a direct regression test for this exact failure mode

Validation:

• cargo fmt --manifest-path /Users/hoangvu/Code/OSS/zerocopy/anneal/Cargo.toml --check
• cargo test --manifest-path /Users/hoangvu/Code/OSS/zerocopy/anneal/Cargo.toml generate::tests::

[codecov-commenter]

Codecov Report

✅ All modified and coverable lines are covered by tests.
✅ Project coverage is 91.85%. Comparing base (ed09d09) to head (5c545cd).

Additional details and impacted files

@@           Coverage Diff           @@
##             main    #3478   +/-   ##
=======================================
  Coverage   91.85%   91.85%           
=======================================
  Files          20       20           
  Lines        6093     6093           
=======================================
  Hits         5597     5597           
  Misses        496      496           

☔ View full report in Codecov by Harness.
📢 Have feedback on the report? Share it here.

🚀 New features to boost your workflow:

• ❄️ Test Analytics: Detect flaky tests, report on failures, and find test suite problems.