Convert binary modules

document/core/appendix/changes.rst

@@ -99,7 +99,7 @@ Added instructions that modify ranges of memory or table entries. [#proposal-ref
 
 * New :ref:`passive <syntax-elemmode>` form of :ref:`element segment <syntax-elem>`
 
-* New :ref:`data count section <binary-datacountsec>` in binary format
+* New :ref:`data count section <binary-datacntsec>` in binary format
 
 * Active data and element segments boundaries are no longer checked at compile time but may trap instead
 

document/core/binary/types.rst

@@ -1,6 +1,5 @@
 .. index:: type
    pair: binary format; type
-.. _binary-type:
 
 Types
 -----
@@ -181,3 +180,15 @@ Global Types
 :ref:`Global types <syntax-globaltype>` are encoded by their :ref:`value type <binary-valtype>` and a flag for their :ref:`mutability <syntax-mut>`.
 
 $${grammar: Bglobaltype}
+
+
+.. index:: external type
+   pair: binary format; external type
+.. _binary-externtype:
+
+External Types
+~~~~~~~~~~~~~~
+
+:ref:`External types <syntax-externtype>` are encoded by a distiguishing byte followed by an encoding of the respective form of type.
+
+$${grammar: Bexterntype}

document/core/util/macros.def

@@ -824,6 +824,7 @@
 .. |Bmemtype| mathdef:: \xref{binary/types}{binary-memtype}{\B{memtype}}
 .. |Blimits| mathdef:: \xref{binary/types}{binary-limits}{\B{limits}}
 .. |Bmut| mathdef:: \xref{binary/types}{binary-mut}{\B{mut}}
+.. |Bexterntype| mathdef:: \xref{binary/types}{binary-externtype}{\B{externtype}}
 
 
 .. Indices, non-terminals
@@ -840,6 +841,8 @@
 .. |Blabelidx| mathdef:: \xref{binary/modules}{binary-labelidx}{\B{labelidx}}
 .. |Bfieldidx| mathdef:: \xref{binary/modules}{binary-fieldidx}{\B{fieldidx}}
 
+.. |Bexternidx| mathdef:: \xref{binary/modules}{binary-externidx}{\B{externidx}}
+
 
 .. Modules, non-terminals
 
@@ -860,10 +863,10 @@
 .. |Belemsec| mathdef:: \xref{binary/modules}{binary-elemsec}{\B{elemsec}}
 .. |Bdatasec| mathdef:: \xref{binary/modules}{binary-datasec}{\B{datasec}}
 .. |Bstartsec| mathdef:: \xref{binary/modules}{binary-startsec}{\B{startsec}}
-.. |Bdatacountsec| mathdef:: \xref{binary/modules}{binary-datacountsec}{\B{datacountsec}}
+.. |Bdatacntsec| mathdef:: \xref{binary/modules}{binary-datacntsec}{\B{datacntsec}}
 
 .. |Bcustom| mathdef:: \xref{binary/modules}{binary-customsec}{\B{custom}}
-.. |Btype| mathdef:: \xref{binary/modules}{binary-typedef}{\B{type}}
+.. |Btype| mathdef:: \xref{binary/modules}{binary-type}{\B{type}}
 .. |Bfunc| mathdef:: \xref{binary/modules}{binary-func}{\B{func}}
 .. |Btable| mathdef:: \xref{binary/modules}{binary-table}{\B{table}}
 .. |Bmem| mathdef:: \xref{binary/modules}{binary-mem}{\B{mem}}
@@ -879,6 +882,7 @@
 .. |Blocals| mathdef:: \xref{binary/modules}{binary-local}{\B{locals}}
 .. |Bdata| mathdef:: \xref{binary/modules}{binary-data}{\B{data}}
 .. |Bstart| mathdef:: \xref{binary/modules}{binary-start}{\B{start}}
+.. |Bdatacnt| mathdef:: \xref{binary/modules}{binary-datacnt}{\B{datacnt}}
 
 
 .. Instructions, non-terminals

spectec/spec/wasm-3.0/A-binary.watsup

@@ -78,7 +78,7 @@ grammar Bmemidx : memidx = x:Bu32 => x
 grammar Belemidx : elemidx = x:Bu32 => x
 grammar Bdataidx : dataidx = x:Bu32 => x
 grammar Blocalidx : localidx = x:Bu32 => x
-grammar Blabelidx : labelidx = x:Bu32 => x
+grammar Blabelidx : labelidx = l:Bu32 => l
 
 grammar Bexternidx : externidx =
   | 0x00 x:Bfuncidx => FUNC x
@@ -1031,7 +1031,8 @@ grammar Bfuncsec : typeidx* hint(desc "function section") =
 ;; Table section
 
 grammar Btable : table =
-  | tt:Btabletype e:Bexpr => TABLE tt e
+  | tt:Btabletype => TABLE tt (REF.NULL ht)  -- if tt = lim (REF NULL? ht)
+  | 0x40 0x00 tt:Btabletype e:Bexpr => TABLE tt e
 
 grammar Btablesec : table* hint(desc "table section") =
   | tab*:Bsection_(4, Blist(Btable)) => tab*
@@ -1058,7 +1059,7 @@ grammar Bglobalsec : global* hint(desc "global section") =
 ;; Export section
 
 grammar Bexport : export =
-  | nm:Bname ux:Bexternidx => EXPORT nm ux
+  | nm:Bname xx:Bexternidx => EXPORT nm xx
 
 grammar Bexportsec : export* hint(desc "export section") =
   | ex*:Bsection_(7, Blist(Bexport)) => ex*
@@ -1080,19 +1081,19 @@ grammar Belemkind : reftype hint(desc "element kind") =
 
 grammar Belem : elem =
   | 0:Bu32 e_o:Bexpr y*:Blist(Bfuncidx) =>
-      ELEM (REF NULL FUNC) (REF.FUNC y)* (ACTIVE 0 e_o)
+      ELEM (REF FUNC) (REF.FUNC y)* (ACTIVE 0 e_o)
   | 1:Bu32 rt:Belemkind y*:Blist(Bfuncidx) =>
       ELEM rt (REF.FUNC y)* PASSIVE
-  | 2:Bu32 x:Btableidx expr:Bexpr rt:Belemkind y*:Blist(Bfuncidx) =>
-      ELEM rt (REF.FUNC y)* (ACTIVE x expr)
+  | 2:Bu32 x:Btableidx e:Bexpr rt:Belemkind y*:Blist(Bfuncidx) =>
+      ELEM rt (REF.FUNC y)* (ACTIVE x e)
   | 3:Bu32 rt:Belemkind y*:Blist(Bfuncidx) =>
       ELEM rt (REF.FUNC y)* DECLARE
-  | 4:Bu32 e_o:Bexpr e*:Blist(Bexpr) =>
-      ELEM (REF NULL FUNC) e* (ACTIVE 0 e_o)
+  | 4:Bu32 e_O:Bexpr e*:Blist(Bexpr) =>
+      ELEM (REF NULL FUNC) e* (ACTIVE 0 e_O)
   | 5:Bu32 rt:Breftype e*:Blist(Bexpr) =>
       ELEM rt e* PASSIVE
-  | 6:Bu32 x:Btableidx expr:Bexpr e*:Blist(Bexpr) =>
-      ELEM (REF NULL FUNC) e* (ACTIVE x expr)
+  | 6:Bu32 x:Btableidx e_O:Bexpr e*:Blist(Bexpr) =>
+      ELEM (REF NULL FUNC) e* (ACTIVE x e_O)
   | 7:Bu32 rt:Breftype e*:Blist(Bexpr) =>
       ELEM rt e* DECLARE
 
@@ -1102,13 +1103,14 @@ grammar Belemsec : elem* hint(desc "element section") =
 
 ;; Code section
 
-syntax code = (local*, expr)
+syntax code hint(macro none) = (local*, expr)
 
 grammar Blocals : local* hint(desc "local") =
   | n:Bu32 t:Bvaltype => (LOCAL t)^n
 
 grammar Bfunc : code =
-  | local**:Blist(Blocals) expr:Bexpr => ($concat_(local, local**), expr)
+  | loc**:Blist(Blocals) e:Bexpr => ($concat_(local, loc**), e)
+    -- if $(|$concat_(local, loc**)| < 2^32)
 
 grammar Bcode : code =
   | len:Bu32 code:Bfunc => code  -- if len = ||Bfunc||
@@ -1139,8 +1141,11 @@ grammar Bdatacntsec : u32* hint(desc "data count section") =
 
 ;; Modules
 
+grammar Bmagic : () = 0x00 0x61 0x73 0x6D => ()
+grammar Bversion : () = 0x01 0x00 0x00 0x00 => ()
 grammar Bmodule : module =
-  | 0x00 0x61 0x73 0x6D 1:Bu32
+  | Bmagic
+    Bversion
     Bcustomsec*
 
 

spectec/spec/wasm-3.0/C-conventions.watsup

@@ -109,5 +109,4 @@ def $allocXs2(syntax X, syntax Y, s*[0], X^n, Y^n) = (s*[n], a^n)
 grammar Btypewriter : () hint(macro none) = 0x00 => ()
 
 def $symdots : A hint(show `...) hint(macro none)
-grammar Bsym : A hint(macro none) =
-  $(B_1) => A_1 | $($symdots) | $(B_n) => A_n
+grammar Bsym : A hint(macro none) = $(B_1) => A_1 | $($symdots) | $(B_n) => A_n

spectec/src/backend-latex/render.ml

@@ -1241,8 +1241,11 @@ and render_syms sep env gs =
 
 and render_prod arrow env prod =
   let (g, e, prems) = prod.it in
-  render_sym env g ^ " " ^ arrow ^ " " ^
-    render_conditions env (render_exp env e) "&&&&&" prems
+  match e.it, prems with
+  | (TupE [] | ParenE ({it = SeqE []; _}, _)), [] -> render_sym env g
+  | _ ->
+    render_sym env g ^ " " ^ arrow ^ " " ^
+      render_conditions env (render_exp env e) "&&&&&" prems
 
 and render_gram arrow env gram =
   let (dots1, prods, dots2) = gram.it in
@@ -1323,17 +1326,21 @@ let render_typdeco env id =
 
 let render_typdef env d =
   match d.it with
-  | TypD (id1, _id2, args, t, _) ->
+  | TypD (id1, _id2, args, t, _hints) ->
     render_typdeco env id1 ^
     render_apply render_typid render_exp env env.show_typ env.macro_typ id1 args ^
     " &::=& " ^ render_typ env t
   | _ -> assert false
 
 let render_gramdef env d =
   match d.it with
-  | GramD (id1, _id2, ps, _t, ({it = (_, prods, _); _} as gram), _) ->
+  | GramD (id1, _id2, ps, _t, gram, _hints) ->
     let args = List.map arg_of_param ps in
-    let arrow = if has_nl prods then "&\\quad\\Rightarrow&\\quad" else "~\\Rightarrow~" in
+    let arrow =
+      if env.config.display && has_nl (let _, prods, _ = gram.it in prods)
+      then "&\\quad\\Rightarrow&\\quad"
+      else "~\\Rightarrow~"
+    in
     "& " ^ render_apply render_gramid render_exp_as_sym
       env env.show_gram env.macro_gram id1 args ^
       " &::=& " ^ render_gram arrow env gram

spectec/test-latex/TEST.md

@@ -8214,7 +8214,7 @@ $$
 & {\mathtt{elemidx}} &::=& x{:}{\mathtt{u32}} ~\Rightarrow~ x \\
 & {\mathtt{dataidx}} &::=& x{:}{\mathtt{u32}} ~\Rightarrow~ x \\
 & {\mathtt{localidx}} &::=& x{:}{\mathtt{u32}} ~\Rightarrow~ x \\
-& {\mathtt{labelidx}} &::=& x{:}{\mathtt{u32}} ~\Rightarrow~ x \\
+& {\mathtt{labelidx}} &::=& l{:}{\mathtt{u32}} ~\Rightarrow~ l \\
 & {\mathtt{externidx}} &::=& \mathtt{0x00}~~x{:}{\mathtt{funcidx}} &\quad\Rightarrow&\quad \mathsf{func}~x \\ &&|&
 \mathtt{0x01}~~x{:}{\mathtt{tableidx}} &\quad\Rightarrow&\quad \mathsf{table}~x \\ &&|&
 \mathtt{0x02}~~x{:}{\mathtt{memidx}} &\quad\Rightarrow&\quad \mathsf{mem}~x \\ &&|&
@@ -8920,8 +8920,8 @@ $$
 
 $$
 \begin{array}{@{}l@{}rrl@{}l@{}l@{}l@{}}
-& {\mathtt{custom}} &::=& {\mathtt{name}}~~{{\mathtt{byte}}^\ast} ~\Rightarrow~ () \\
-& {\mathtt{customsec}} &::=& {{\mathtt{section}}}_{0}({\mathtt{custom}}) ~\Rightarrow~ () \\
+& {\mathtt{custom}} &::=& {\mathtt{name}}~~{{\mathtt{byte}}^\ast} \\
+& {\mathtt{customsec}} &::=& {{\mathtt{section}}}_{0}({\mathtt{custom}}) \\
 \end{array}
 $$
 
@@ -8955,7 +8955,9 @@ $$
 
 $$
 \begin{array}{@{}l@{}rrl@{}l@{}l@{}l@{}}
-& {\mathtt{table}} &::=& {\mathit{tt}}{:}{\mathtt{tabletype}}~~e{:}{\mathtt{expr}} ~\Rightarrow~ \mathsf{table}~{\mathit{tt}}~e \\
+& {\mathtt{table}} &::=& {\mathit{tt}}{:}{\mathtt{tabletype}} &\quad\Rightarrow&\quad \mathsf{table}~{\mathit{tt}}~(\mathsf{ref{.}null}~{\mathit{ht}})
+  &\qquad \mbox{if}~{\mathit{tt}} = {\mathit{lim}}~(\mathsf{ref}~{\mathsf{null}^?}~{\mathit{ht}}) \\ &&|&
+\mathtt{0x40}~~\mathtt{0x00}~~{\mathit{tt}}{:}{\mathtt{tabletype}}~~e{:}{\mathtt{expr}} &\quad\Rightarrow&\quad \mathsf{table}~{\mathit{tt}}~e \\
 & {\mathtt{tablesec}} &::=& {{\mathit{tab}}^\ast}{:}{{\mathtt{section}}}_{4}({\mathtt{list}}({\mathtt{table}})) ~\Rightarrow~ {{\mathit{tab}}^\ast} \\
 \end{array}
 $$
@@ -8982,7 +8984,7 @@ $$
 
 $$
 \begin{array}{@{}l@{}rrl@{}l@{}l@{}l@{}}
-& {\mathtt{export}} &::=& {\mathit{nm}}{:}{\mathtt{name}}~~{\mathit{ux}}{:}{\mathtt{externidx}} ~\Rightarrow~ \mathsf{export}~{\mathit{nm}}~{\mathit{ux}} \\
+& {\mathtt{export}} &::=& {\mathit{nm}}{:}{\mathtt{name}}~~{\mathit{xx}}{:}{\mathtt{externidx}} ~\Rightarrow~ \mathsf{export}~{\mathit{nm}}~{\mathit{xx}} \\
 & {\mathtt{exportsec}} &::=& {{\mathit{ex}}^\ast}{:}{{\mathtt{section}}}_{7}({\mathtt{list}}({\mathtt{export}})) ~\Rightarrow~ {{\mathit{ex}}^\ast} \\
 \end{array}
 $$
@@ -9001,13 +9003,13 @@ $$
 $$
 \begin{array}{@{}l@{}rrl@{}l@{}l@{}l@{}}
 & {\mathtt{elemkind}} &::=& \mathtt{0x00} ~\Rightarrow~ \mathsf{ref}~\mathsf{null}~\mathsf{func} \\
-& {\mathtt{elem}} &::=& 0{:}{\mathtt{u32}}~~e_o{:}{\mathtt{expr}}~~{y^\ast}{:}{\mathtt{list}}({\mathtt{funcidx}}) &\quad\Rightarrow&\quad \mathsf{elem}~(\mathsf{ref}~\mathsf{null}~\mathsf{func})~{(\mathsf{ref{.}func}~y)^\ast}~(\mathsf{active}~0~e_o) \\ &&|&
+& {\mathtt{elem}} &::=& 0{:}{\mathtt{u32}}~~e_o{:}{\mathtt{expr}}~~{y^\ast}{:}{\mathtt{list}}({\mathtt{funcidx}}) &\quad\Rightarrow&\quad \mathsf{elem}~(\mathsf{ref}~\mathsf{func})~{(\mathsf{ref{.}func}~y)^\ast}~(\mathsf{active}~0~e_o) \\ &&|&
 1{:}{\mathtt{u32}}~~{\mathit{rt}}{:}{\mathtt{elemkind}}~~{y^\ast}{:}{\mathtt{list}}({\mathtt{funcidx}}) &\quad\Rightarrow&\quad \mathsf{elem}~{\mathit{rt}}~{(\mathsf{ref{.}func}~y)^\ast}~\mathsf{passive} \\ &&|&
-2{:}{\mathtt{u32}}~~x{:}{\mathtt{tableidx}}~~{\mathit{expr}}{:}{\mathtt{expr}}~~{\mathit{rt}}{:}{\mathtt{elemkind}}~~{y^\ast}{:}{\mathtt{list}}({\mathtt{funcidx}}) &\quad\Rightarrow&\quad \mathsf{elem}~{\mathit{rt}}~{(\mathsf{ref{.}func}~y)^\ast}~(\mathsf{active}~x~{\mathit{expr}}) \\ &&|&
+2{:}{\mathtt{u32}}~~x{:}{\mathtt{tableidx}}~~e{:}{\mathtt{expr}}~~{\mathit{rt}}{:}{\mathtt{elemkind}}~~{y^\ast}{:}{\mathtt{list}}({\mathtt{funcidx}}) &\quad\Rightarrow&\quad \mathsf{elem}~{\mathit{rt}}~{(\mathsf{ref{.}func}~y)^\ast}~(\mathsf{active}~x~e) \\ &&|&
 3{:}{\mathtt{u32}}~~{\mathit{rt}}{:}{\mathtt{elemkind}}~~{y^\ast}{:}{\mathtt{list}}({\mathtt{funcidx}}) &\quad\Rightarrow&\quad \mathsf{elem}~{\mathit{rt}}~{(\mathsf{ref{.}func}~y)^\ast}~\mathsf{declare} \\ &&|&
-4{:}{\mathtt{u32}}~~e_o{:}{\mathtt{expr}}~~{e^\ast}{:}{\mathtt{list}}({\mathtt{expr}}) &\quad\Rightarrow&\quad \mathsf{elem}~(\mathsf{ref}~\mathsf{null}~\mathsf{func})~{e^\ast}~(\mathsf{active}~0~e_o) \\ &&|&
+4{:}{\mathtt{u32}}~~e_{\mathsf{o}}{:}{\mathtt{expr}}~~{e^\ast}{:}{\mathtt{list}}({\mathtt{expr}}) &\quad\Rightarrow&\quad \mathsf{elem}~(\mathsf{ref}~\mathsf{null}~\mathsf{func})~{e^\ast}~(\mathsf{active}~0~e_{\mathsf{o}}) \\ &&|&
 5{:}{\mathtt{u32}}~~{\mathit{rt}}{:}{\mathtt{reftype}}~~{e^\ast}{:}{\mathtt{list}}({\mathtt{expr}}) &\quad\Rightarrow&\quad \mathsf{elem}~{\mathit{rt}}~{e^\ast}~\mathsf{passive} \\ &&|&
-6{:}{\mathtt{u32}}~~x{:}{\mathtt{tableidx}}~~{\mathit{expr}}{:}{\mathtt{expr}}~~{e^\ast}{:}{\mathtt{list}}({\mathtt{expr}}) &\quad\Rightarrow&\quad \mathsf{elem}~(\mathsf{ref}~\mathsf{null}~\mathsf{func})~{e^\ast}~(\mathsf{active}~x~{\mathit{expr}}) \\ &&|&
+6{:}{\mathtt{u32}}~~x{:}{\mathtt{tableidx}}~~e_{\mathsf{o}}{:}{\mathtt{expr}}~~{e^\ast}{:}{\mathtt{list}}({\mathtt{expr}}) &\quad\Rightarrow&\quad \mathsf{elem}~(\mathsf{ref}~\mathsf{null}~\mathsf{func})~{e^\ast}~(\mathsf{active}~x~e_{\mathsf{o}}) \\ &&|&
 7{:}{\mathtt{u32}}~~{\mathit{rt}}{:}{\mathtt{reftype}}~~{e^\ast}{:}{\mathtt{list}}({\mathtt{expr}}) &\quad\Rightarrow&\quad \mathsf{elem}~{\mathit{rt}}~{e^\ast}~\mathsf{declare} \\
 & {\mathtt{elemsec}} &::=& {{\mathit{elem}}^\ast}{:}{{\mathtt{section}}}_{9}({\mathtt{list}}({\mathtt{elem}})) ~\Rightarrow~ {{\mathit{elem}}^\ast} \\
 \end{array}
@@ -9024,7 +9026,8 @@ $$
 $$
 \begin{array}{@{}l@{}rrl@{}l@{}l@{}l@{}}
 & {\mathtt{locals}} &::=& n{:}{\mathtt{u32}}~~t{:}{\mathtt{valtype}} ~\Rightarrow~ {(\mathsf{local}~t)^{n}} \\
-& {\mathtt{func}} &::=& {{{\mathit{local}}^\ast}^\ast}{:}{\mathtt{list}}({\mathtt{locals}})~~{\mathit{expr}}{:}{\mathtt{expr}} ~\Rightarrow~ ({\mathrm{concat}}({{{\mathit{local}}^\ast}^\ast}), {\mathit{expr}}) \\
+& {\mathtt{func}} &::=& {{{\mathit{loc}}^\ast}^\ast}{:}{\mathtt{list}}({\mathtt{locals}})~~e{:}{\mathtt{expr}} ~\Rightarrow~ ({\mathrm{concat}}({{{\mathit{loc}}^\ast}^\ast}), e)
+  &\qquad \mbox{if}~{|{\mathrm{concat}}({{{\mathit{loc}}^\ast}^\ast})|} < {2^{32}} \\
 & {\mathtt{code}} &::=& {\mathit{len}}{:}{\mathtt{u32}}~~{\mathit{code}}{:}{\mathtt{func}} ~\Rightarrow~ {\mathit{code}}
   &\qquad \mbox{if}~{\mathit{len}} = ||{\mathtt{func}}|| \\
 & {\mathtt{codesec}} &::=& {{\mathit{code}}^\ast}{:}{{\mathtt{section}}}_{10}({\mathtt{list}}({\mathtt{code}})) ~\Rightarrow~ {{\mathit{code}}^\ast} \\
@@ -9055,7 +9058,9 @@ $$
 
 $$
 \begin{array}{@{}l@{}rrl@{}l@{}l@{}l@{}}
-& {\mathtt{module}} &::=& \mathtt{0x00}~~\mathtt{0x61}~~\mathtt{0x73}~~\mathtt{0x6D}~~1{:}{\mathtt{u32}}~~{{\mathtt{customsec}}^\ast} \\ &&&\quad {{\mathit{type}}^\ast}{:}{\mathtt{typesec}}~~{{\mathtt{customsec}}^\ast} \\ &&&\quad {{\mathit{import}}^\ast}{:}{\mathtt{importsec}}~~{{\mathtt{customsec}}^\ast} \\ &&&\quad {{\mathit{typeidx}}^{n}}{:}{\mathtt{funcsec}}~~{{\mathtt{customsec}}^\ast} \\ &&&\quad {{\mathit{table}}^\ast}{:}{\mathtt{tablesec}}~~{{\mathtt{customsec}}^\ast} \\ &&&\quad {{\mathit{mem}}^\ast}{:}{\mathtt{memsec}}~~{{\mathtt{customsec}}^\ast} \\ &&&\quad {{\mathit{global}}^\ast}{:}{\mathtt{globalsec}}~~{{\mathtt{customsec}}^\ast} \\ &&&\quad {{\mathit{export}}^\ast}{:}{\mathtt{exportsec}}~~{{\mathtt{customsec}}^\ast} \\ &&&\quad {{\mathit{start}}^\ast}{:}{\mathtt{startsec}}~~{{\mathtt{customsec}}^\ast} \\ &&&\quad {{\mathit{elem}}^\ast}{:}{\mathtt{elemsec}}~~{{\mathtt{customsec}}^\ast} \\ &&&\quad {{m'}^\ast}{:}{\mathtt{datacntsec}}~~{{\mathtt{customsec}}^\ast} \\ &&&\quad {({{\mathit{local}}^\ast}, {\mathit{expr}})^{n}}{:}{\mathtt{codesec}}~~{{\mathtt{customsec}}^\ast} \\ &&&\quad {{\mathit{data}}^{m}}{:}{\mathtt{datasec}}~~{{\mathtt{customsec}}^\ast} ~\Rightarrow~ \mathsf{module}~{{\mathit{type}}^\ast}~{{\mathit{import}}^\ast}~{{\mathit{func}}^{n}}~{{\mathit{global}}^\ast}~{{\mathit{table}}^\ast}~{{\mathit{mem}}^\ast}~{{\mathit{elem}}^\ast}~{{\mathit{data}}^{m}}~{{\mathit{start}}^\ast}~{{\mathit{export}}^\ast}
+& {\mathtt{magic}} &::=& \mathtt{0x00}~~\mathtt{0x61}~~\mathtt{0x73}~~\mathtt{0x6D} \\
+& {\mathtt{version}} &::=& \mathtt{0x01}~~\mathtt{0x00}~~\mathtt{0x00}~~\mathtt{0x00} \\
+& {\mathtt{module}} &::=& {\mathtt{magic}}~~{\mathtt{version}}~~{{\mathtt{customsec}}^\ast} \\ &&&\quad {{\mathit{type}}^\ast}{:}{\mathtt{typesec}}~~{{\mathtt{customsec}}^\ast} \\ &&&\quad {{\mathit{import}}^\ast}{:}{\mathtt{importsec}}~~{{\mathtt{customsec}}^\ast} \\ &&&\quad {{\mathit{typeidx}}^{n}}{:}{\mathtt{funcsec}}~~{{\mathtt{customsec}}^\ast} \\ &&&\quad {{\mathit{table}}^\ast}{:}{\mathtt{tablesec}}~~{{\mathtt{customsec}}^\ast} \\ &&&\quad {{\mathit{mem}}^\ast}{:}{\mathtt{memsec}}~~{{\mathtt{customsec}}^\ast} \\ &&&\quad {{\mathit{global}}^\ast}{:}{\mathtt{globalsec}}~~{{\mathtt{customsec}}^\ast} \\ &&&\quad {{\mathit{export}}^\ast}{:}{\mathtt{exportsec}}~~{{\mathtt{customsec}}^\ast} \\ &&&\quad {{\mathit{start}}^\ast}{:}{\mathtt{startsec}}~~{{\mathtt{customsec}}^\ast} \\ &&&\quad {{\mathit{elem}}^\ast}{:}{\mathtt{elemsec}}~~{{\mathtt{customsec}}^\ast} \\ &&&\quad {{m'}^\ast}{:}{\mathtt{datacntsec}}~~{{\mathtt{customsec}}^\ast} \\ &&&\quad {({{\mathit{local}}^\ast}, {\mathit{expr}})^{n}}{:}{\mathtt{codesec}}~~{{\mathtt{customsec}}^\ast} \\ &&&\quad {{\mathit{data}}^{m}}{:}{\mathtt{datasec}}~~{{\mathtt{customsec}}^\ast} ~\Rightarrow~ \mathsf{module}~{{\mathit{type}}^\ast}~{{\mathit{import}}^\ast}~{{\mathit{func}}^{n}}~{{\mathit{global}}^\ast}~{{\mathit{table}}^\ast}~{{\mathit{mem}}^\ast}~{{\mathit{elem}}^\ast}~{{\mathit{data}}^{m}}~{{\mathit{start}}^\ast}~{{\mathit{export}}^\ast}
   &\qquad \mbox{if}~{{m'}^\ast} = \epsilon \lor {\mathrm{dataidx}}({{\mathit{func}}^{n}}) = \epsilon \\
   &&&&&&\qquad {\land}~m = {\mathrm{sum}}({{m'}^\ast}) \\
   &&&&&&\qquad {\land}~(({\mathit{func}} = \mathsf{func}~{\mathit{typeidx}}~{{\mathit{local}}^\ast}~{\mathit{expr}}))^{n} \\
@@ -9180,7 +9185,7 @@ $$
 
 $$
 \begin{array}{@{}l@{}rrl@{}l@{}l@{}l@{}}
-& {\mathtt{typewriter}} &::=& \mathtt{0x00} ~\Rightarrow~ () \\
+& {\mathtt{typewriter}} &::=& \mathtt{0x00} \\
 \end{array}
 $$
 

spectec/test-splice/TEST.md

@@ -643,6 +643,7 @@ warning: grammar `Blimits` was never spliced
 warning: grammar `Blist` was never spliced
 warning: grammar `Blocalidx` was never spliced
 warning: grammar `Blocals` was never spliced
+warning: grammar `Bmagic` was never spliced
 warning: grammar `Bmem` was never spliced
 warning: grammar `Bmemarg` was never spliced
 warning: grammar `Bmemidx` was never spliced
@@ -677,6 +678,7 @@ warning: grammar `Bu64` was never spliced
 warning: grammar `BuN` was never spliced
 warning: grammar `Bvaltype` was never spliced
 warning: grammar `Bvectype` was never spliced
+warning: grammar `Bversion` was never spliced
 warning: rule `Blocktype_ok/valtype` was never spliced
 warning: rule `Blocktype_ok/typeidx` was never spliced
 warning: rule `Comptype_ok/struct` was never spliced