Summary
translate_module_import and translate_export_module interpolate WASM import/export name bytes straight into a Gallina string literal without escaping, so a name containing " or a backslash emits Rocq that does not parse.
Found while fixing #402, which is the same "no fixture exercises it, so nothing caught it" story.
Cause
In core/wasm-to-v/src/translator.rs, both sites build the literal by direct interpolation:
format!("Mi \"{imp_module}\" \"{imp_name}\" …")A name of say"hi closes the literal early; a trailing backslash escapes the closing quote. Either way coqc fails to parse the module.
Why it matters more than the import case
Imports are stripped by the static-merge linker before -v runs, so the import site is only reachable through translate_bytes on a foreign .wasm. Exports are not — they are emitted by the normal pipeline, so an export name carrying a quote reaches coqc from ordinary Inference source.
WebAssembly export names are arbitrary UTF-8 byte sequences; nothing in the format forbids a quote.
Suggested fix
Either escape the bytes for Gallina's string-literal syntax, or fail closed the way translate_ref_type does and reject a name the contract cannot spell. Escaping is preferable — rejecting a legal export name because of the proof backend would be a surprising restriction — but failing closed is better than emitting a broken .v, so either is an improvement.
Worth pairing with a fixture so the coqc gate covers it, in the spirit of #401.
Summary
translate_module_importandtranslate_export_moduleinterpolate WASM import/export name bytes straight into a Gallina string literal without escaping, so a name containing"or a backslash emits Rocq that does not parse.Found while fixing #402, which is the same "no fixture exercises it, so nothing caught it" story.
Cause
In
core/wasm-to-v/src/translator.rs, both sites build the literal by direct interpolation:A name of
say"hicloses the literal early; a trailing backslash escapes the closing quote. Either waycoqcfails to parse the module.Why it matters more than the import case
Imports are stripped by the static-merge linker before
-vruns, so the import site is only reachable throughtranslate_byteson a foreign.wasm. Exports are not — they are emitted by the normal pipeline, so an export name carrying a quote reachescoqcfrom ordinary Inference source.WebAssembly export names are arbitrary UTF-8 byte sequences; nothing in the format forbids a quote.
Suggested fix
Either escape the bytes for Gallina's string-literal syntax, or fail closed the way
translate_ref_typedoes and reject a name the contract cannot spell. Escaping is preferable — rejecting a legal export name because of the proof backend would be a surprising restriction — but failing closed is better than emitting a broken.v, so either is an improvement.Worth pairing with a fixture so the
coqcgate covers it, in the spirit of #401.