Name section can carry duplicate entries: struct name equal to a bound logical module

[0xGeorgii]

Summary

Two different schemes compose names into the WebAssembly name section over the same . separator:

• methods, as {StructName}.{method}
• merged external bodies, as {logical_module}.{export_field}

When a struct's name equals a bound logical module name, the two collide and the linked module ships a name section with two entries spelling the same name.

Reproduction

external fn double(x: i32) -> i32;
use { double } from mathlib;

struct mathlib {
    v: i32;
    fn double(a: i32) -> i32 { return a * 3; }
}

pub fn entry(x: i32) -> i32 { return mathlib::double(x) + double(x); }

Compiles and links clean. The emitted name-section payload contains mathlib.double twice; wasm-tools print renders the second as $"#func2 mathlib.double" (@name "mathlib.double").

Impact

Compile mode ships the non-injective section with no diagnostic. The Rocq translator sanitizes . to _, so both would render as mathlib_double, and the translator's index-suffix disambiguation is index-dependent and shifts across merges.

Proof mode does fail closed, but only when an obligation actually applies the ambiguous symbol:

obligation applies function symbol `mathlib.double`, which 2 defined functions share; the target is ambiguous

So the guard is the resolution-time ambiguity arm, not the naming scheme — a program that merely defines the collision and never asserts over it is accepted in both modes.

Suggested direction

Either reserve a separator (or a prefix) that the method scheme cannot produce, or reject a bound logical module name that collides with a struct name at the point the binding is resolved, where the diagnostic can name both.

Scope

Pre-existing. Found during the #363 linker-envelope work while auditing the merged-name producers, which are now collocated in core/fn-key so this namespace is enumerable in one place.