[spec] Bugs / questions about `VLOAD` in Wasm 2.0

[zilinc]

In the Wasm 2.0 spectec specification, the instruction VLOAD can optionally take a vloadop: https://github.com/WebAssembly/spec/blob/main/specification/wasm-2.0/1-syntax.spectec#L510
but I can't find its counterpart in the manually written spec.
There isn't a relevant typing rule for the eps case, but there're reduction rules for it: https://github.com/WebAssembly/spec/blob/main/specification/wasm-2.0/8-reduction.spectec#L505-L511

So we'd like to get some clarification on this discrepancy.

Incidentally, I think the show hints in this block are all wrong---they all take one more argument marker %: https://github.com/WebAssembly/spec/blob/main/specification/wasm-2.0/1-syntax.spectec#L506-L513

(cc: @maximelegoupil)

[rossberg]

That's historic. I had to do various refactorings between 2.0 and 3.0 for the sake of both Relaxed SIMD and general clean-up, and then again for SpecTec. Later I created the SpecTec 2.0 version simply by erasing all new features from the 3.0 version. Hence, all those refactorings occur in SpecTec 2.0, but the official document predates them.

Not sure I follow what you mean by the "eps case". Can you clarify?

The show hints in the 2.0 SpecTec may well be off — they never got tested or fixed, because we never rendered a real document from it.

[zilinc]

That's historic. I had to do various refactorings between 2.0 and 3.0 for the sake of both Relaxed SIMD and general clean-up, and then again for SpecTec. Later I created the SpecTec 2.0 version simply by erasing all new features from the 3.0 version. Hence, all those refactorings occur in SpecTec 2.0, but the official document predates them.

The syntax in the SpecTec version is VLOAD vectype vloadop? memarg. The real question is, when vloadop? = eps, is it a mis-specification or is it a genuine feature that the language supports (and if so, what does it map to in the manual spec)?

Not sure I follow what you mean by the "eps case". Can you clarify?

There're reduction rules for VLOAD when vloadop? = eps, but there's no corresponding typing rule.

[rossberg]

Ah, I see. Yes, it looks like the Instr_ok/vload-val rule from 3.0 somehow got lost in the backport. And Instr_ok/vload should be Instr_ok/vload-pack.

In general, the SIMD load/store instructions shouldn't differ from 3.0.

Please feel free to fix! :)

[zilinc]

I had a loot at the manual Wasm 2, Wasm 3, and SpecTec Wasm 3 spec pdfs. My understanding is that in the manual ones, both the typing rule and the reduction rule for VLOAD V128 eps memarg are merged with those for LOAD numtype eps memarg (where in Wasm 3 they additionally both take a memidx argument). But in the SpecTec-generated spec, this pen-and-paper informal rule merging isn't possible. However, it seems that there's no reduction rule for VLOAD V128 eps memidx memarg in the generated spec (the rules are there in the source. they're just not spliced into the doc).