The Wasm 1.0 Module_ok rule has the import external types ixt* and export external types xt* in its premises, but its conclusion returns only OK.
Current rule:
relation Module_ok: |- module : OK hint(show "T-module")
The WebAssembly Specification, Release 1.0 PDF, Section 3.4:
“Then the module is valid with external types it* → et*.”
The conclusion of the formal rule is:
⊢ {types functype*, funcs func*, tables table*, mems mem*, globals global*,
elem elem*, data data*, start start?, imports import*, exports export*}
: it* → et*
The Wasm 1.0
Module_okrule has the import external typesixt*and export external typesxt*in its premises, but its conclusion returns onlyOK.Current rule:
The WebAssembly Specification, Release 1.0 PDF, Section 3.4:
The conclusion of the formal rule is: