memory.init/copy/fill discard their memory-index immediates

[0xGeorgii]

Summary

memory.init, memory.copy and memory.fill discard their memory-index immediates and unconditionally emit the memory-0 constructor, so a multi-memory module translates to a .v describing a machine the .wasm is not. The neighbouring memory.size/memory.grow arms get this right and reject mem > 0.

Found while auditing coqc-gate coverage for #401.

Reproduction

(module
  (memory 1)
  (memory 1)
  (func (memory.copy 1 1)))

translates successfully and emits BI_memory_copy — the constructor for memory 0. The obligation is then about the wrong memory, silently.

Cause

In core/wasm-to-v/src/translator.rs, the three arms match mem: _ / mem_dst: _, mem_src: _ and drop the immediate:

Operator::MemoryInit { data_index, mem: _ } => ...
Operator::MemoryCopy { dst_mem: _, src_mem: _ } => "BI_memory_copy".to_string(),
Operator::MemoryFill { mem: _ } => "BI_memory_fill".to_string(),

Compare MemorySize/MemoryGrow in the same file, which check the index and reject a non-zero one as multi-memory.

Suggested fix

Reject mem > 0 in all three arms as WasmToVError::UnsupportedFeature, matching what memory.size/memory.grow already do — the proof contract has no multi-memory constructor, so failing closed is the only faithful option. The same memory64/shared guards elsewhere in that function exist for exactly this reason.

Reachability

Not reachable from Inference codegen, which emits a single memory. Reachable from a foreign or statically-linked .wasm. Multi-memory is a post-1.0 feature, so exposure is limited today — but the failure is silent, which is the part worth fixing.

Not fixed by the #401 coverage work: giving BI_memory_copy a producer only needs a single-memory fixture, so the audit does not force this. Filing it separately.