Minor errors in 3.0 binary format

[conrad-watt]

1. The third (recursive) case of the binary definition of sN should have i:s instead of i:u

• 3.0: https://webassembly.github.io/spec/core/binary/values.html#integers
• 2.0 for comparison: https://www.w3.org/TR/wasm-core-2/#integers%E2%91%A4

---

2. (arguable?) The module binary definition uses * everywhere for all the section lists, but the typeid and code sections should have a distinguished arity to make in unambiguous that they must have the same number of entries as each other (while other sections are allowed to have different sizes) - 2.0 used n.

• 3.0: https://webassembly.github.io/spec/core/binary/modules.html#binary-module
• 2.0 for comparison: https://www.w3.org/TR/wasm-core-2/#modules%E2%91%A0%E2%93%AA

---

These were found while hand-mechanising part of the binary format in Isabelle.

[rossberg]

Ah thanks. (1) is fixed in 6e4c4bc.

Re (2), that should actually be working as intended, since the side condition (𝑓𝑢𝑛𝑐 = func 𝑡𝑦𝑝𝑒𝑖𝑑𝑥 𝑙𝑜𝑐𝑎𝑙* 𝑒𝑥𝑝𝑟)* already implies the constraint |𝑡𝑦𝑝𝑒𝑖𝑑𝑥*| = |𝑙𝑜𝑐𝑎𝑙**| = |𝑒𝑥𝑝𝑟*|, otherwise it wouldn't be defined. But admittedly that's subtle.