Possible discrepancy between wasmcert and official webassembly specification

[mkarup]

I have found something that might have been missed in the WasmCert-Coq mechanization related to left/ right shifts. In the official WebAssembly spec (both 1.0 and 2.0), the left/ right shift integer operators (ishl_N and ishr_u_N / ishr_s_N, where N is either 32 or 64) are defined to shift the first argument i₁ left, respectively right, by k bits, where k = i₂ mod N.
For example:

ishl₆₄(1, 65) = 1 << (65 mod 64) = 2

Apologies if I'm incorrect, but looking at the integer operations defined in WasmCert, it doesn't look like the second argument of the shift operators are taken modulo N before applying the shift.

The relevant section in the official specification is in Execution/Numerics/Integer operations.

[raoxiaojia]

I think you are right -- in fact, there's a TODO note on the definitions of ishl/ishr_u functions talking about the mistmach as well, and ishr_s was using Compcert's version of shr (which seems to perform the signed conversion but also needs the mod N treatment).

The rotations irotl and irotr are also using Compcert's version directly, but curiously Compcert has performed mod N in their implementation. Instead of simply posting a commit to add the modulos in, I'll check and compare the expected behaviours of Compcert numerics and Wasm's to make sure these several functions actually match.