Resolve an external fn by its declaration rather than its bare name

CHANGELOG.md

@@ -9,6 +9,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 
 ### Breaking
 
+- An `external fn`'s identity is now the **declaration** (the declaring `DefId`), resolved in the scope the call is written in — the declaring file, and the `spec` block within it — rather than the bare name looked up program-wide. Two shapes now compile that did not: two files may each declare `external fn f` and bind it to a different module, with each file's calls reaching its own binding; and a file's own bound extern is no longer broken by an unrelated same-named declaration elsewhere in the program. Two now error that did not: a `use … from` clause no longer reaches across files to bind another file's declaration, so one naming an extern its own file does not declare is the dangling-import error `ExternImportNotDeclared`; and a free function and an `external fn` sharing one bare name is the new `ExternFunctionNameCollision`, whether the two sit in one file or in different files: one bare name may not denote both a local function and an external declaration in one program. Each call in such a program resolves — to the declaration its own file names — and the pair is rejected as a rule about the spelling, because a call site does not say whether its callee is compiled here or linked in. `AmbiguousExternModule` is correspondingly a within-file rule — one name, one module, per file — and `extern_origins()` deduplicates on `(logical_module, export_field, decl)` rather than on `(module, field)`, so every declaration is still validated against the library's signature instead of only the first per `(module, field)` pair. Migration: rename either half of a colliding free-function/`external fn` pair, and give each file the `use … from` clause binding its own declaration; a program that does not reuse an extern name across files is unaffected ([#423])
 - A specification may now call a **bound** `external fn`, so a linked external `.wasm` is reasonable about in proof mode: the call becomes a `T_app`/`HA_app_ok` naming the body the static-merge linker splices in (`mathlib.double` for `use { double } from mathlib;`), which is the symbol the merge writes into the name section, and `wasm-to-v` resolves it against the **linked** module. Previously every extern call in a spec was **P005** ("external functions carry no verified body"), which made the linker envelope unusable for its stated purpose — an external could be linked and executed but nothing could be claimed about it. The declaration is resolved by `DefId`, not by name: two `external fn`s may share a name across scopes (a bound one at file scope, an unbound one inside a `spec`) and only the declaration the call site actually names decides whether it has a linked body, so a name-keyed lookup would hand a spec-inner declaration the top-level one's origin and name a merged body the call does not reach (`A024` resolves unbound-extern calls through the same scope walk and rejects such a call first, so this is defense in depth everywhere except a pipeline that skips analysis — which the proof-mode test gates are). An **unbound** extern keeps **P005**, with a message naming the missing `use … from` binding rather than the extern; through `infc`/`infs` that message is not what a user sees, since **A024** fires on the same call first — P005 is what an embedder or an analysis-skipping pipeline gets. Two `wasm-to-v` rejections come with it, both of which could previously produce a well-formed but meaningless `.v`: an obligation whose application arity differs from the resolved function's parameter count is now a hard error (`T_app`'s arguments are a `seq term`, so a wrong-width application elaborates and passes `coqc` while describing a different function), and an obligation naming a function the module *imports* now says the merge has not run instead of reporting the symbol as unknown. Unaffected: every obligation that names no extern is byte-identical, and no committed `.wasm`/`.wat`/`.v` golden moves. Known limitation, unchanged and now pinned by a test that asserts it: a **cross-file** `T_app` symbol still does not resolve, because code generation writes bare item names into the name section while the obligation writes the file-qualified `FnKey::Display` ([#363])
 - Proof mode now compiles `exists`- and `unique`-quantified spec functions end to end instead of rejecting them as **P001**. The body is *reachability-lowered*: compiled to vanilla WASM with one hidden trailing choice parameter per scalar `@` (name-section label `__choice{k}`; narrow-type domain normalization kept) and `assume`/`assert` as trap-on-false filters; the function is *retained* in the emitted `.v` module record — `forall`/plain spec functions stay omitted, and every executable reference to a retained function is rejected (it is the subject of a judgment, not a callable) — and its obligation is emitted as a `reachability_spec` record (`reach_func`/`reach_entry_arity`/`reach_visible_locs`/`reach_payload`) under a kind-selected theorem: `ValidExistsSpec` for `exists`, `ValidUniqueSpec` for `unique`, with the preamble import gaining ` Exists` only in reachability-bearing modules. The payload binds each `@` to its choice parameter's frame slot — no `HA_ex` binder, no `HA_has_type` guard: the judgment runs the retained body, so the frame supplies value and typing — while `_specs`/`ValidSpec` stays unconditional per spec name and forall-only output is byte-identical. The quantifier kind travels in `inference.hspecs` wire **v2** (per-entry kind byte plus reachability metadata; encode is always v2, decode rejects v1 — the section is proof-mode intermediate data, so recompile rather than migrate). **P001** narrows to standalone `assume` bodies, with a message explaining why an `assume` body states no property; new fatal diagnostics **P011** (any spec body calling an `exists`/`unique` spec function — the callee's compiled form carries hidden choice parameters no call site supplies) and **P012** (an anonymous `@` in a `unique` body — a choice nothing names cannot distinguish source-visible exit states; bind it first with `let c: i32 = @;`). Compound `@` in a reachability body keeps **P008** with a reachability-specific message; reachability bodies must be void and `return`-free (contract-forced: the downstream judgment reduces the retained body without an activation frame, so a `return` could never take a step), enforced by a codegen pre-scan even on analysis-skipping pipelines. `unique` compares source-visible exit states — entry parameters plus named `let x = @` choices, declared in `reach_visible_locs`; a `unique`-quantified *body* is a deliberate extension ahead of the language-spec amendment, while nested `unique` *blocks* stay **P002**. Reachability translation hard-depends on the WASM name section, and the obligations are dischargeable only for import-free modules (the always-link pipeline satisfies this). Also fixes the A002/A005 message article (`a 'exists' block` → `an 'exists' block`). Full contract in `core/wasm-to-v/ROCQ_CONTRACT.md` ([#354])
 - New fatal proof-mode diagnostic **P010**: a spec function whose obligation collapses to the vacuous `HA_true` now aborts code generation instead of being emitted. Such an obligation is discharged by any proof without reading the program, so a green `Qed` over it carried zero verification content and no warning said so — `spec Caller { fn caller() -> i32 { return helper(); } }` emitted `Definition …_hspec1 : hassert := HA_true.` and the meaning the author wrote ("caller equals helper") was simply dropped. The check is the translated result, not the body shape: `HAssert::and`/`imp`/`or`/`ex` absorb `⊤`, so every vacuity path collapses to exactly `HA_true` and one equality catches them all — an empty or assert-free body, a body that only computes (`return`, pure `let`/`const`), a trailing `assume` (`Imp(p, ⊤) = ⊤`), and an `if` whose branches all vacuate, several of which look like they contribute. The message names what the body claimed and what to write instead. A spec function may still `return` — a body that also asserts is unaffected. Consequence: a helper that only computes can no longer live inside a `spec` block; move it to file scope, where a spec function still applies it as a `T_app`. A plain spec *method* keeps its helper exemption because it produces no obligation either way, so the same helper wrapped in a spec-inner struct still compiles — but a plain method that *states* a property — one carrying an `assert` at any depth, a non-deterministic block that asserts nothing excluded — now raises **P009** rather than being dropped with no output at all, which is the widening that closes the worst silent path in the area. Unaffected: compile mode, which has no obligations; every spec function that already stated a property, whose obligation is byte-identical. Migration: give the spec function an `assert`, or move it out of the `spec` block ([#356])
@@ -621,3 +622,4 @@ Initial tagged release.
 [#416]: https://github.com/Inferara/inference/issues/416
 [#355]: https://github.com/Inferara/inference/issues/355
 [#420]: https://github.com/Inferara/inference/issues/420
+[#423]: https://github.com/Inferara/inference/issues/423

apps/infs/tests/cli_integration.rs

@@ -2384,15 +2384,23 @@ fn logged_probes(log: &std::path::Path) -> Vec<String> {
 /// what these tests link must be what `infc` emits today, or a change to the
 /// module shape would leave them linking a stale fixture.
 fn build_arith_library(infc_path: &std::path::Path) -> Vec<u8> {
+    build_library(infc_path, "arith", ARITH_LIB_SRC)
+}
+
+/// Compiles `source` on its own with the real `infc` and returns the `.wasm`
+/// bytes, for vendoring into a dependent project as a `[wasm-dependencies]`
+/// entry.
+fn build_library(infc_path: &std::path::Path, name: &str, source: &str) -> Vec<u8> {
     let lib = assert_fs::TempDir::new().unwrap();
-    lib.child("arith.inf").write_str(ARITH_LIB_SRC).unwrap();
+    let entry = format!("{name}.inf");
+    lib.child(&entry).write_str(source).unwrap();
 
     let mut cmd = Command::new(infc_path);
-    cmd.current_dir(lib.path()).arg("arith.inf");
+    cmd.current_dir(lib.path()).arg(&entry);
     cmd.assert().success();
 
-    std::fs::read(lib.child("out").child("arith.wasm").path())
-        .expect("infc must produce out/arith.wasm for the library")
+    std::fs::read(lib.child("out").child(format!("{name}.wasm")).path())
+        .unwrap_or_else(|e| panic!("infc must produce out/{name}.wasm for the library: {e}"))
 }
 
 /// Scaffolds a project that binds the `arith` external: the manifest declares the
@@ -2800,6 +2808,76 @@ fn project_run_executes_a_linked_manifest_dependency() {
     );
 }
 
+/// Two files of one project each declare `external fn scale` and bind it to a
+/// *different* library. Executed end to end through the project front end.
+///
+/// The project route is the one seam where the merged arena is built from a real
+/// source tree rather than assembled in a test, and the whole program is one
+/// `infc` invocation — so both files' `scale` calls pass through a single
+/// compilation with a single import table. Nothing before execution distinguishes
+/// a per-file resolution from a program-wide one: the declarations agree on name
+/// and signature, so either wiring type-checks, links and validates. Only the
+/// value says which library ran. `libA` multiplies by 999 and `libB` by 7, and
+/// `main` reports both at once as `1998 * 100 + 14`.
+#[test]
+fn project_run_resolves_a_same_named_extern_per_file() {
+    let Some(infc_path) = require_infc_and_wasmtime() else {
+        return;
+    };
+
+    let lib_a = build_library(
+        &infc_path,
+        "libA",
+        "pub fn scale(a: i32) -> i32 {\n    return a * 999;\n}\n",
+    );
+    let lib_b = build_library(
+        &infc_path,
+        "libB",
+        "pub fn scale(a: i32) -> i32 {\n    return a * 7;\n}\n",
+    );
+
+    let temp = assert_fs::TempDir::new().unwrap();
+    scaffold_project_with_manifest(
+        &temp,
+        "demo",
+        "use sib;\n\n\
+         external fn scale(a: i32) -> i32;\n\
+         use { scale } from libA;\n\n\
+         pub fn main() -> i32 {\n    return scale(2) * 100 + sib::via_b(2);\n}\n",
+        "[wasm-dependencies]\n\
+         libA = { path = \"libs/libA.wasm\" }\n\
+         libB = { path = \"libs/libB.wasm\" }\n",
+    );
+    temp.child("src")
+        .child("sib.inf")
+        .write_str(
+            "external fn scale(a: i32) -> i32;\n\
+             use { scale } from libB;\n\n\
+             pub fn via_b(x: i32) -> i32 {\n    return scale(x);\n}\n",
+        )
+        .unwrap();
+    temp.child("libs")
+        .child("libA.wasm")
+        .write_binary(&lib_a)
+        .unwrap();
+    temp.child("libs")
+        .child("libB.wasm")
+        .write_binary(&lib_b)
+        .unwrap();
+
+    let mut cmd = Command::new(assert_cmd::cargo::cargo_bin!("infs"));
+    cmd.env("INFC_PATH", &infc_path)
+        .env_remove("INFERENCE_WASM_LIB_PATH")
+        .current_dir(temp.path())
+        .arg("run");
+    let stdout = stdout_of(&cmd.assert().success());
+    assert!(
+        stdout.contains("199814"),
+        "each file's `scale` must reach its own library (1998 via libA, 14 via libB); \
+         201798 would mean both calls funnelled into libA, got:\n{stdout}"
+    );
+}
+
 /// Scaffolds a throwaway project with a logging `infc` stub, runs `infs run`
 /// with `args` from the project root, and returns the argv the stub recorded.
 ///

book/src/external-functions-and-wasm-linking.md

@@ -99,8 +99,12 @@ example above produces:
 
 Imported functions occupy the lowest WASM function indices. The local `add_three`
 is shifted to index 1 (after the one import at index 0). The call target `call 0`
-is the import index, resolved statically from the `extern_name_to_idx` table built
-during the pre-scan phase.
+is the import index, resolved statically during the pre-scan phase: the compiler
+resolves the callee name to the `external fn` declaration in scope where the call
+is written — its file, and the `spec` block enclosing it — and takes the import
+that declaration reserved. Identity is the declaration, not the name, so two files
+may each declare `scale` and bind it to a different module, and each file's calls
+reach its own.
 
 ## The Link Step
 

core/analysis/README.md

@@ -91,7 +91,7 @@ These rules cover constructs that are valid in the type system but cannot yet be
 | A019 | `ArrayIndex64Bit` | error | 64-bit integer used as an array index |
 | A022 | `LiteralOutOfRange` | error | numeric literal is outside the valid range for the type its position gave it |
 | A023 | `UzumakiInReassignment` | error | uzumaki (`@`) used in a variable reassignment (only `let` initializers are supported) |
-| A024 | `ExternFunctionCall` | error | call to an external (`extern`) function (not yet implemented in codegen) |
+| A024 | `ExternFunctionCall` | error | call to an **unbound** `external fn` — one no `use … from` clause binds to a source module |
 | A026 | `NestedCompoundDepth` | error | struct field is itself a nested compound type beyond one level of nesting |
 | A027 | `UzumakiOnNestedStruct` | error | uzumaki (`@`) assigned to a struct whose fields include another struct or an array of structs |
 | A028 | `UzumakiOnStructInArray` | error | uzumaki (`@`) assigned to an array whose element type is a struct |
@@ -178,7 +178,7 @@ A045 rejects *values* of a struct with no fields. Such a struct occupies zero by
 
 Rejecting a field-less struct as the type of a *field* is what closes the hole: a struct all of whose fields are zero-sized would itself be zero-sized, so forbidding a zero-sized field collapses that composition into the base case. In an accepted program a struct is therefore zero-sized if and only if it has no fields, which lets the predicate be `fields.is_empty()` plus array recursion — no transitive size computation, no visited set, no cycle handling. With every value-introducing position rejected, assignments, reads, and method calls on such values need no checks of their own (each requires a binding, parameter, or field that is already rejected), so a program reports one diagnostic per offending declaration rather than one per use. A module-scope `const` is checked here in its own right rather than left to A032, which rejects *every* top-level `const` as not yet implemented: A032 is a gate on an unimplemented feature, and a closure resting on it would go silently incomplete the day that feature lands. Both fire on such a declaration; there is no cross-rule suppression.
 
-*Declaring* a field-less struct stays legal. A field-less struct with associated functions is the supported method-namespace idiom (`E::helper()`) and compiles unchanged; the `self` receiver is rejected because once no value of the struct can exist the method is uncallable by construction, and the fix — dropping `self` — produces exactly that idiom. `external fn` signatures are checked for their ABI surface rather than for the closure (A024 rejects every call to an extern function, so no value can flow through one). Two documented non-scopes: generics, since a type parameter never resolves to a struct, so a generic signature (`fn id T'(x: T) -> T`) is outside the predicate — nothing is missed by that today, because the compiler does not monomorphize and codegen rejects a generic type outright, so there is no instantiation at a field-less struct to check; and local type aliases, which are non-transparent in Inference and so are a dead end rather than a route to a value.
+*Declaring* a field-less struct stays legal. A field-less struct with associated functions is the supported method-namespace idiom (`E::helper()`) and compiles unchanged; the `self` receiver is rejected because once no value of the struct can exist the method is uncallable by construction, and the fix — dropping `self` — produces exactly that idiom. `external fn` signatures are checked for their ABI surface rather than for the closure (A024 rejects a call to an *unbound* extern outright, and a bound extern's declared parameter and return types are themselves in scope above, so no field-less value flows through either). Two documented non-scopes: generics, since a type parameter never resolves to a struct, so a generic signature (`fn id T'(x: T) -> T`) is outside the predicate — nothing is missed by that today, because the compiler does not monomorphize and codegen rejects a generic type outright, so there is no instantiation at a field-less struct to check; and local type aliases, which are non-transparent in Inference and so are a dead end rather than a route to a value.
 
 ### Spaced Negative Literals (errors)