Summary
No multi-file program whose spec calls a function defined in another file can produce a .v at all. The proof obligation records the callee with FnKey::Display, while the name section records the bare name, so symbol resolution finds no match and wasm_to_v fails.
Reproduction
Committed fixture, current main:
against tests/test_data/multi_file_golden/proof_specs/, which fails with:
obligation applies function symbol `lib.checks.lib_value`, which no defined function in the module carries
The obligation writes the structured FnKey rendering; the name section writes lib_value.
Why it is filed separately
Aligning the two moves every multi-file .wasm golden, and it needs a collision rule decided first: the bare name is not unique across files, which is why the qualified form exists on the obligation side. Picking the qualified form for the name section instead changes the emitted names every downstream Rocq proof refers to.
Scope
Pre-existing; not introduced by the linker-envelope work on #363. Found while adding a linked-external proof fixture there, and reproduced at that branch point with the base binary on a committed fixture.
Summary
No multi-file program whose
speccalls a function defined in another file can produce a.vat all. The proof obligation records the callee withFnKey::Display, while the name section records the bare name, so symbol resolution finds no match andwasm_to_vfails.Reproduction
Committed fixture, current
main:against
tests/test_data/multi_file_golden/proof_specs/, which fails with:The obligation writes the structured
FnKeyrendering; the name section writeslib_value.Why it is filed separately
Aligning the two moves every multi-file
.wasmgolden, and it needs a collision rule decided first: the bare name is not unique across files, which is why the qualified form exists on the obligation side. Picking the qualified form for the name section instead changes the emitted names every downstream Rocq proof refers to.Scope
Pre-existing; not introduced by the linker-envelope work on #363. Found while adding a linked-external proof fixture there, and reproduced at that branch point with the base binary on a committed fixture.