Table limits silently drop table64 and shared

[0xGeorgii]

Summary

translate_table_type_limits reads only initial/maximum and silently drops table64 and shared, so an i64-indexed or shared table is re-encoded as a 32-bit non-shared one. Its exact sibling translate_memory_type_limits rejects all three of the analogous cases.

Found while auditing coqc-gate coverage for #401.

The asymmetry

translate_memory_type_limits in core/wasm-to-v/src/translator.rs guards memory64, shared and a custom page size, with the rationale recorded in its own comment — such a module "would be silently re-encoded as a 32-bit, non-shared, default-page-size machine — a .v describing a machine the .wasm is not". The table helper next to it has no equivalent guard, although inf-wasmparser's TableType carries table64: bool and shared: bool and its initial/maximum are u64.

Reproduction

input	memory arm	table arm
(module (memory i64 1))	Err("unsupported WASM feature: memory64 (i64-addressed) linear memory")	—
(module (memory 1 1 shared))	Err("unsupported WASM feature: shared linear memory (threads proposal)")	—
(module (table i64 1 funcref))	—	Ok: Mt {|lim_min := 1%N; lim_max := None|} T_funcref
(module (table i64 5000000000 5000000000 funcref))	—	Ok: Mt {|lim_min := 5000000000%N; lim_max := Some(5000000000%N)|} T_funcref
(module (import "env" "t" (table i64 1 funcref)))	—	Ok: Mi "env" "t" (MID_table {|tt_limits := {|lim_min := 1%N; lim_max := None|}; tt_elem_type := T_funcref|})

The second row is the sharpest: a limit beyond u32::MAX is emitted verbatim into a field the contract types as a 32-bit table's N.

Suggested fix

Give translate_table_type_limits the same fail-closed guards its memory sibling has: reject table64 and shared as WasmToVError::UnsupportedFeature naming the construct. The proof contract has no constructor that can express either, so failing closed is the only faithful option.

Reachability

Not reachable from Inference codegen. Reachable from a foreign or statically-linked .wasm. Both are post-1.0 proposals so exposure is limited today; the failure is silent, which is the part worth fixing.

Related: #403 (the same silent-misdescription class, for the memory-index immediates of memory.init/copy/fill).