Only one external fn per bare name can be bound across a multi-file program

[0xGeorgii]

Summary

collect_top_level_extern_decls builds a program-wide name -> DefId map with last-file-wins, so at most one external fn of a given bare name can be bound anywhere in a multi-file program. An unrelated, never-called declaration in a sibling file breaks a working call in another file, with the calling file's source unchanged.

Reproduction

1. main.inf declares external fn f(...) and binds it with use { f } from mathlib;, then calls it. A024 passes.
2. Add a sibling file containing an unrelated external fn f(...) that is never called and never bound.
3. main.inf's own call now fails A024, with byte-identical source in main.inf.

Why it matters

The failure is non-local and the diagnostic points at the calling file, which is correct in neither the cause nor the fix. It also makes the binding depend on file iteration order rather than on scope.

The natural fix is to key the map on the declaration's DefId (or on (module_path, name)) rather than the bare name — the same identity distinction #363 needed for resolving a bound extern in a spec obligation, where a name-keyed lookup would hand a spec-inner declaration the top-level one's origin.

Scope

Pre-existing and independent of the #363 linker-envelope work; found and reproduced while implementing it.

[0xGeorgii]

Reproduced by execution — this is a miscompile, not only a diagnostic problem

The bare-name extern map does not merely reject a valid program (the case in the description); it also silently binds a call to the wrong function.

Two-file project, built through infs project mode:

• entry file: defines its own fn scale(x) -> x * 10, and calls scale(x) from pub fn entry
• sibling file: declares external fn scale(x) and binds it with use { scale } from libA;, where libA.scale computes a + a

The entry file's call resolves through the program-wide extern_name_to_idx, so it reaches the external, not the local function defined in its own file. wasm-tools print on the linked output:

(func $scale    (;0;) ...)                     ; the entry file's own scale - dead
(func $entry    (;1;) ...) call $libA.scale
(func $use_side (;2;) ...) call $libA.scale
(func $libA.scale (;3;) ...)

Executed:

wasmtime run --invoke entry <module>.wasm 2
1998

entry(2) should be 2 * 10 = 20. It returns 1998, because the call landed on the external.

There is no diagnostic at any stage: type checking, analysis, code generation, linking, and validation all pass.

Note for whoever fixes this

The proof-obligation pass added for #363 resolves the same call scope-aware (spec-inner, then file-scope) and keyed on the declaration's DefId, so it names the local function here while code generation names the external. That divergence is documented at the ExternIndex type rather than silently relied upon. Fixing the code generation side should make the two agree; the obligation side is already the more precise of the two and is a reasonable model for the fix.