Fix type ambiguity in anneal spec generation for shadowed type names

[nnunley]

Summary

When a Rust function uses a type via use import (e.g., use std::sync::atomic::Ordering), the spec generator only sees the short name Ordering from the syn AST. This conflicts with Lean's native Ordering (core.cmp.Ordering) brought in by open Aeneas.Std, causing type mismatches in the generated Pre/Post structs.

Fix

After Aeneas generates Funs.lean (which contains fully-qualified type names in def signatures), parse those signatures and use the Aeneas types as overrides in spec generation. Falls back to the existing map_type behavior when no Aeneas type info is available.

Changes

• anneal/src/funs_types.rs (new): Parses Lean def signatures from Funs.lean to extract (param_name, lean_type) pairs. Handles single-line, multi-line, generic, and implicit-parameter signatures. Skips implicit {} params.
• anneal/src/generate.rs: Adds generate_artifact_with_types and generate_function_with_types that accept a FunsTypeMap. Original signatures preserved as backward-compatible wrappers. Override logic matches params by name and uses the item_namespace for correct Aeneas function name lookup.
• anneal/src/aeneas.rs: Reads Funs.lean after Aeneas runs, parses types, passes to spec generation. Undoes the show→show1 patch before parsing so param names match the Rust source.
• anneal/src/main.rs: Registers new module.

Testing

• 242 unit tests pass (including 6 new tests for the Funs.lean parser)
• Integration tests: 53 pass, 43 fail — identical results on main (pre-existing toolchain issue where LD_LIBRARY_PATH doesn't include the managed toolchain's rust/lib/ when ANNEAL_USE_PATH_FOR_TOOLS=1 is set)
• Verified on both macOS (aarch64) and Linux (x86_64, Ubuntu 24.04)

Example

Before (broken — Ordering resolves to Lean's core.cmp.Ordering):

structure Pre (self : AtomicFrameState) (order : Ordering) : Prop where

After (correct — uses Aeneas's fully-qualified name):

structure Pre (self : AtomicFrameState) (order : core.sync.atomic.Ordering) : Prop where

[google-cla]

Thanks for your pull request! It looks like this may be your first contribution to a Google open source project. Before we can look at your pull request, you'll need to sign a Contributor License Agreement (CLA).

View this failed invocation of the CLA check for more information.

For the most up to date status, view the checks section at the bottom of the pull request.

[codecov-commenter]

Codecov Report

✅ All modified and coverable lines are covered by tests.
✅ Project coverage is 91.88%. Comparing base (be6f199) to head (b36aba8).

Additional details and impacted files

@@           Coverage Diff           @@
##             main    #3345   +/-   ##
=======================================
  Coverage   91.88%   91.88%           
=======================================
  Files          20       20           
  Lines        6076     6076           
=======================================
  Hits         5583     5583           
  Misses        493      493           

☔ View full report in Codecov by Sentry.
📢 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.