Fix type ambiguity in spec generation for shadowed type names

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.

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.

Author: nnunley

anneal/src/aeneas.rs

@@ -346,8 +346,20 @@ pub fn generate_lean_workspace(roots: &LockedRoots, artifacts: &[AnnealArtifact]
         let slug = artifact.artifact_slug();
         let output_dir = lean_generated_root.join(&slug);
 
+        // Parse parameter types from Aeneas-generated Funs.lean to use
+        // fully-qualified type names in spec generation. We undo the
+        // `show` -> `show1` patch so parameter names match the Rust source.
+        let funs_path = output_dir.join("Funs.lean");
+        let funs_types = if funs_path.exists() {
+            let content = std::fs::read_to_string(&funs_path)
+                .with_context(|| format!("Failed to read {}", funs_path.display()))?;
+            crate::funs_types::parse_funs_types(&content)
+        } else {
+            crate::funs_types::FunsTypeMap::new()
+        };
+
         // Generate Anneal specs
-        let generated = generate::generate_artifact(artifact);
+        let generated = generate::generate_artifact_with_funs_types(artifact, &funs_types);
         let specs_path = output_dir.join(artifact.lean_spec_file_name());
         let map_path = output_dir.join(format!("{}.lean.map", artifact.artifact_slug()));
 

anneal/src/funs_types.rs

@@ -0,0 +1,157 @@
+//! Parses Aeneas-generated `Funs.lean` to extract fully-qualified parameter types.
+//!
+//! Anneal's spec generator re-derives types from the Rust AST, losing qualification
+//! for `use`-imported names (e.g., `Ordering` instead of `core.sync.atomic.Ordering`).
+//! This module provides a lookup table from the Aeneas output as a corrective.
+
+use std::collections::HashMap;
+
+/// Function name → `[(param_name, lean_type)]`.
+pub type FunsTypeMap = HashMap<String, Vec<(String, String)>>;
+
+/// Parses `def` signatures from `Funs.lean`, extracting explicit parameter types.
+/// Skips implicit `{}` parameters. Returns an empty map on parse failure.
+pub fn parse_funs_types(content: &str) -> FunsTypeMap {
+    let mut map = FunsTypeMap::new();
+    let lines: Vec<&str> = content.lines().collect();
+
+    for i in 0..lines.len() {
+        let Some(rest) = lines[i].trim().strip_prefix("def ") else { continue };
+        let name = rest.split([' ', '(', '{', ':']).next().unwrap_or("");
+        if name.is_empty() {
+            continue;
+        }
+
+        // Collect signature lines until `:=`
+        let mut sig = String::from(rest);
+        for j in (i + 1)..lines.len() {
+            if sig.contains(":=") {
+                break;
+            }
+            sig.push(' ');
+            sig.push_str(lines[j].trim());
+        }
+
+        let params = extract_params(&sig);
+        if !params.is_empty() {
+            // patch_funs renames `show` → `show1` to avoid a Lean keyword clash;
+            // undo that so param names match the Rust source during lookup.
+            let params = params
+                .into_iter()
+                .map(|(n, t)| (if n == "show1" { "show".to_string() } else { n }, t))
+                .collect();
+            map.insert(name.to_string(), params);
+        }
+    }
+    map
+}
+
+/// Extracts `(name : type)` bindings, skipping `{implicit}` params and stopping at `:`.
+fn extract_params(sig: &str) -> Vec<(String, String)> {
+    let mut params = Vec::new();
+    let mut chars = sig.chars().peekable();
+
+    while let Some(&c) = chars.peek() {
+        match c {
+            '(' => {
+                chars.next();
+                if let Some(pair) = parse_binding(&collect_delimited(&mut chars, ')')) {
+                    params.push(pair);
+                }
+            }
+            '{' => {
+                chars.next();
+                collect_delimited(&mut chars, '}');
+            }
+            ':' => break,
+            _ => {
+                chars.next();
+            }
+        }
+    }
+    params
+}
+
+/// Reads chars until the matching `close` delimiter, handling nesting.
+fn collect_delimited(chars: &mut std::iter::Peekable<std::str::Chars>, close: char) -> String {
+    let open = if close == ')' { '(' } else { '{' };
+    let mut depth = 1u32;
+    let mut buf = String::new();
+    for c in chars.by_ref() {
+        if c == open {
+            depth += 1;
+        } else if c == close {
+            depth -= 1;
+            if depth == 0 {
+                return buf;
+            }
+        }
+        buf.push(c);
+    }
+    buf
+}
+
+/// Splits `"name : type"` on the first ` : `.
+fn parse_binding(s: &str) -> Option<(String, String)> {
+    let s = s.trim();
+    let i = s.find(" : ")?;
+    let (name, ty) = (s[..i].trim(), s[i + 3..].trim());
+    (!name.is_empty() && !ty.is_empty()).then(|| (name.to_string(), ty.to_string()))
+}
+
+#[cfg(test)]
+mod tests {
+    use super::*;
+
+    #[test]
+    fn simple() {
+        let m = parse_funs_types("def hash_key (k : Std.Usize) : Result Std.Usize := do\n");
+        assert_eq!(m["hash_key"], [("k".into(), "Std.Usize".into())]);
+    }
+
+    #[test]
+    fn multiline() {
+        let m = parse_funs_types(
+            "def frame.AtomicFrameState.load\n\
+             \x20 (self : frame.AtomicFrameState) (order : core.sync.atomic.Ordering) :\n\
+             \x20 Result frame.FrameState\n\
+             \x20 := do\n",
+        );
+        let p = &m["frame.AtomicFrameState.load"];
+        assert_eq!(p[0], ("self".into(), "frame.AtomicFrameState".into()));
+        assert_eq!(p[1], ("order".into(), "core.sync.atomic.Ordering".into()));
+    }
+
+    #[test]
+    fn skips_implicits() {
+        let m = parse_funs_types(
+            "def HashMap.alloc {T : Type} (slots : alloc.vec.Vec T) (n : Std.Usize) :\n\
+             \x20 Result Unit := do\n",
+        );
+        let p = &m["HashMap.alloc"];
+        assert_eq!(p.len(), 2);
+        assert_eq!(p[0].0, "slots");
+        assert_eq!(p[1], ("n".into(), "Std.Usize".into()));
+    }
+
+    #[test]
+    fn multiple_ordering_params() {
+        let m = parse_funs_types(
+            "def f.compare_exchange\n\
+             \x20 (self : f.T) (expected : f.S)\n\
+             \x20 (success : core.sync.atomic.Ordering)\n\
+             \x20 (failure : core.sync.atomic.Ordering) :\n\
+             \x20 Result Unit := do\n",
+        );
+        let p = &m["f.compare_exchange"];
+        assert_eq!(p.len(), 4);
+        assert_eq!(p[2].1, "core.sync.atomic.Ordering");
+        assert_eq!(p[3].1, "core.sync.atomic.Ordering");
+    }
+
+    #[test]
+    fn trait_instance_no_params() {
+        let m = parse_funs_types("def Foo.Clone : core.clone.Clone Foo := {\n  clone := x\n}\n");
+        assert!(m.get("Foo.Clone").map_or(true, |p| p.is_empty()));
+    }
+}

anneal/src/generate.rs

@@ -236,11 +236,19 @@ pub fn generate_item(
     item: &crate::parse::ParsedLeanItem<crate::parse::hkd::Safe>,
     builder: &mut LeanBuilder,
     naming_context: &NamingContext,
+    funs_types: &crate::funs_types::FunsTypeMap,
 ) {
+    let namespace = naming_context.item_namespace(item);
     match &item.item {
-        ParsedItem::Function(func) => {
-            generate_function(&func.item, &func.anneal, builder, &item.source_file, naming_context)
-        }
+        ParsedItem::Function(func) => generate_function_with_funs_types(
+            &func.item,
+            &func.anneal,
+            builder,
+            &item.source_file,
+            naming_context,
+            funs_types,
+            &namespace,
+        ),
         ParsedItem::Type(ty) => {
             generate_type(&ty.item, &ty.anneal, builder, &item.source_file, naming_context)
         }
@@ -259,6 +267,13 @@ pub fn generate_item(
 /// 3. Iterates over all items in the artifact, generating code for each.
 /// 4. Wraps items in their respective module namespaces.
 pub fn generate_artifact(artifact: &crate::scanner::AnnealArtifact) -> GeneratedArtifact {
+    generate_artifact_with_funs_types(artifact, &Default::default())
+}
+
+pub fn generate_artifact_with_funs_types(
+    artifact: &crate::scanner::AnnealArtifact,
+    funs_types: &crate::funs_types::FunsTypeMap,
+) -> GeneratedArtifact {
     let mut builder = LeanBuilder::new();
     builder.push_str("-- This file is automatically generated by Anneal.\n");
     builder.push_str("-- Do not edit manually.\n\n");
@@ -293,7 +308,7 @@ pub fn generate_artifact(artifact: &crate::scanner::AnnealArtifact) -> Generated
             builder.push_str(&format!("namespace {}\n\n", namespace));
         }
 
-        generate_item(item, &mut builder, &naming_context);
+        generate_item(item, &mut builder, &naming_context, funs_types);
         builder.push('\n');
 
         if !namespace.is_empty() {
@@ -571,6 +586,26 @@ fn generate_function(
     builder: &mut LeanBuilder,
     source_file: &std::path::Path,
     naming_context: &NamingContext,
+) {
+    generate_function_with_funs_types(
+        func,
+        block,
+        builder,
+        source_file,
+        naming_context,
+        &Default::default(),
+        "",
+    )
+}
+
+fn generate_function_with_funs_types(
+    func: &FunctionItem<crate::parse::hkd::Safe>,
+    block: &FunctionAnnealBlock<crate::parse::hkd::Safe>,
+    builder: &mut LeanBuilder,
+    source_file: &std::path::Path,
+    naming_context: &NamingContext,
+    funs_types: &crate::funs_types::FunsTypeMap,
+    item_namespace: &str,
 ) {
     let (fn_name, fn_span, impl_struct_name, generic_params, generic_bounds, dict_args) = match func
     {
@@ -599,7 +634,30 @@ fn generate_function(
             (n.inner.sig.ident.clone(), n.inner.sig.name_span, None, p, b, d)
         }
     };
-    let args = extract_args_metadata(func, &impl_struct_name);
+    let mut args = extract_args_metadata(func, &impl_struct_name);
+
+    // Override parameter types from Aeneas-generated Funs.lean when available.
+    // This ensures fully-qualified type names are used, preventing ambiguity
+    // with Lean builtins (e.g., `Ordering` vs `core.sync.atomic.Ordering`).
+    if !funs_types.is_empty() {
+        // Build the Aeneas function name: namespace.fn_name
+        let aeneas_fn_name = if item_namespace.is_empty() {
+            fn_name.to_string()
+        } else {
+            format!("{}.{}", item_namespace, fn_name)
+        };
+
+        if let Some(aeneas_params) = funs_types.get(&aeneas_fn_name) {
+            for arg in args.iter_mut() {
+                if let Some((_, aeneas_type)) =
+                    aeneas_params.iter().find(|(name, _)| *name == arg.name)
+                {
+                    arg.lean_type = aeneas_type.clone();
+                }
+            }
+        }
+    }
+
     let has_return_value = !is_unit_return(func);
 
     builder.push_str(&format!("namespace {}\n\n", fn_name));

anneal/src/main.rs

@@ -2,6 +2,7 @@ mod aeneas;
 mod charon;
 mod diagnostics;
 mod errors;
+mod funs_types;
 mod generate;
 mod parse;
 mod resolve;