References to wasm spec are incorrect in several ways

[lars-t-hansen]

Ref https://webassembly.github.io/spec/core/exec/modules.html#exec-instantiation

The prose for memory.init references the wasm spec for instantiation "step 11" but this is incorrect now, the step is probably 14 (for memories) and 13 (for tables). However, those steps presuppose that range checking already has been done in steps 9 (for tables) and 10 (for memories), so the prose for this cross-reference in the bulkmem spec must be rewritten until we have proper formal semantics.

Worse, in steps 9 and 10 of those algorithms, we fail instantiation without writing anything if a data/elem segment would write past the end of the memory/table, meaning there would be no writing-up-until-the-bounds-check-fails, as we have for memory.init / table.init by recent agreement. Thus active and passive segments don't behave the same, or if you like, the operations at module start are not really the same as a memory.init+data.drop or table.init+elem.drop, which is counter to what we're stating.

It's not 100% backwards compatible to fix this by changing the handling of active segments, since imported memories/tables that are targeted by oob active segments are now unchanged when the module instantiation fails, but would be partially and observably changed if we change the semantics of active segments. But I doubt it would break any real code to fix it this way.

[lars-t-hansen]

Thanks.

One issue outstanding: now that we can have partial writes, whether we do memory initialization or table initialization first becomes observable. The MVP spec has tables before memory, and I'm happy with that; @binji, @rossberg, any particular reasons to alter this?

[rossberg]

I can't think of a good argument either way, so it seems fine leaving it as is.