Repository navigation
Minor errors in 3.0 binary format #2041
Description
- The third (recursive) case of the binary definition of
sNshould havei:sinstead ofi: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
- (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 usedn.
- 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.
Activity
rossberg commentedon Dec 8, 2025
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.