Skip to content

Commit

Permalink
Tweak layout
Browse files Browse the repository at this point in the history
  • Loading branch information
@rossberg
rossberg committed Jun 13, 2024
1 parent 92182ac commit dd3c8d4
Show file tree
Hide file tree
Showing 8 changed files with 69 additions and 105 deletions.
55 changes: 0 additions & 55 deletions document/core/binary/modules.rst
View file
Original file line number Diff line number Diff line change
Expand Up @@ -383,61 +383,6 @@ Furthermore, it must be present if any :ref:`data index <syntax-dataidx>` occurs

$${grammar: {Bmagic Bversion Bmodule}}

.. math::
\begin{array}{llcllll}
\production{magic} & \Bmagic &::=&
\hex{00}~\hex{61}~\hex{73}~\hex{6D} \\
\production{version} & \Bversion &::=&
\hex{01}~\hex{00}~\hex{00}~\hex{00} \\
\production{module} & \Bmodule &::=&
\Bmagic \\ &&&
\Bversion \\ &&&
\Bcustomsec^\ast \\ &&&
\rectype^\ast{:\,}\Btypesec \\ &&&
\Bcustomsec^\ast \\ &&&
\import^\ast{:\,}\Bimportsec \\ &&&
\Bcustomsec^\ast \\ &&&
\typeidx^n{:\,}\Bfuncsec \\ &&&
\Bcustomsec^\ast \\ &&&
\table^\ast{:\,}\Btablesec \\ &&&
\Bcustomsec^\ast \\ &&&
\mem^\ast{:\,}\Bmemsec \\ &&&
\Bcustomsec^\ast \\ &&&
\global^\ast{:\,}\Bglobalsec \\ &&&
\Bcustomsec^\ast \\ &&&
\export^\ast{:\,}\Bexportsec \\ &&&
\Bcustomsec^\ast \\ &&&
\start^?{:\,}\Bstartsec \\ &&&
\Bcustomsec^\ast \\ &&&
\elem^\ast{:\,}\Belemsec \\ &&&
\Bcustomsec^\ast \\ &&&
m^?{:\,}\Bdatacntsec \\ &&&
\Bcustomsec^\ast \\ &&&
\X{code}^n{:\,}\Bcodesec \\ &&&
\Bcustomsec^\ast \\ &&&
\data^m{:\,}\Bdatasec \\ &&&
\Bcustomsec^\ast
\quad\Rightarrow\quad \{~
\begin{array}[t]{@{}l@{}}
\MTYPES~\rectype^\ast, \\
\MFUNCS~\func^n, \\
\MTABLES~\table^\ast, \\
\MMEMS~\mem^\ast, \\
\MGLOBALS~\global^\ast, \\
\MELEMS~\elem^\ast, \\
\MDATAS~\data^m, \\
\MSTART~\start^?, \\
\MIMPORTS~\import^\ast, \\
\MEXPORTS~\export^\ast ~\} \\
\end{array} \\ &&&
(\iff m^? \neq \epsilon \vee \freedataidx(\X{code}^n) = \emptyset) \\
\end{array}
where for each :math:`t_i^\ast, e_i` in :math:`\X{code}^n`,

.. math::
\func^n[i] = \{ \FTYPE~\typeidx^n[i], \FLOCALS~t_i^\ast, \FBODY~e_i \} \\
.. note::
The version of the WebAssembly binary format may increase in the future
if backward-incompatible changes have to be made to the format.
Expand Down
4 changes: 2 additions & 2 deletions document/core/util/macros.def
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1331,7 +1331,7 @@
.. |TIREFS| mathdef:: \xref{exec/runtime}{syntax-tableinst}{\K{elem}}

.. |MITYPE| mathdef:: \xref{exec/runtime}{syntax-meminst}{\K{type}}
.. |MIBYTES| mathdef:: \xref{exec/runtime}{syntax-meminst}{\K{data}}
.. |MIBYTES| mathdef:: \xref{exec/runtime}{syntax-meminst}{\K{bytes}}

.. |GITYPE| mathdef:: \xref{exec/runtime}{syntax-globalinst}{\K{type}}
.. |GIVALUE| mathdef:: \xref{exec/runtime}{syntax-globalinst}{\K{value}}
Expand All @@ -1340,7 +1340,7 @@
.. |EIREFS| mathdef:: \xref{exec/runtime}{syntax-eleminst}{\K{elem}}

.. |DITYPE| mathdef:: \xref{exec/runtime}{syntax-datainst}{\K{data}}
.. |DIBYTES| mathdef:: \xref{exec/runtime}{syntax-datainst}{\K{data}}
.. |DIBYTES| mathdef:: \xref{exec/runtime}{syntax-datainst}{\K{bytes}}

.. |EINAME| mathdef:: \xref{exec/runtime}{syntax-exportinst}{\K{name}}
.. |EIVALUE| mathdef:: \xref{exec/runtime}{syntax-exportinst}{\K{value}}
Expand Down
10 changes: 5 additions & 5 deletions spectec/spec/wasm-3.0/2-syntax-aux.watsup
View file
Original file line number Diff line number Diff line change
Expand Up @@ -17,22 +17,22 @@ def $setminus1(x, y_1 y*) = $setminus1(x, y*) -- otherwise

;; Free indices

def $dataidx_instr(instr) : dataidx* hint(show $dataidx(%))
def $dataidx_instr(instr) : dataidx* hint(show $dataidx(%)) hint(macro "freedataidx")
def $dataidx_instr(MEMORY.INIT x y) = y
def $dataidx_instr(DATA.DROP x) = x
def $dataidx_instr(in) = eps

def $dataidx_instrs(instr*) : dataidx* hint(show $dataidx(%))
def $dataidx_instrs(instr*) : dataidx* hint(show $dataidx(%)) hint(macro "freedataidx")
def $dataidx_instrs(eps) = eps
def $dataidx_instrs(instr instr'*) = $dataidx_instr(instr) $dataidx_instrs(instr'*)

def $dataidx_expr(expr) : dataidx* hint(show $dataidx(%))
def $dataidx_expr(expr) : dataidx* hint(show $dataidx(%)) hint(macro "freedataidx")
def $dataidx_expr(in*) = $dataidx_instrs(in*)

def $dataidx_func(func) : dataidx* hint(show $dataidx(%))
def $dataidx_func(func) : dataidx* hint(show $dataidx(%)) hint(macro "freedataidx")
def $dataidx_func(FUNC x loc* e) = $dataidx_expr(e)

def $dataidx_funcs(func*) : dataidx* hint(show $dataidx(%))
def $dataidx_funcs(func*) : dataidx* hint(show $dataidx(%)) hint(macro "freedataidx")
def $dataidx_funcs(eps) = eps
def $dataidx_funcs(func func'*) = $dataidx_func(func) $dataidx_funcs(func'*)

Expand Down
34 changes: 20 additions & 14 deletions spectec/spec/wasm-3.0/A-binary.watsup
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1067,6 +1067,7 @@ grammar Bexportsec : export* hint(desc "export section") =

;; Start section

;; TODO: should return start?
grammar Bstart : start* =
| x:Bfuncidx => (START x)

Expand Down Expand Up @@ -1132,6 +1133,7 @@ grammar Bdatasec : data* hint(desc "data section") =

;; Data count section

;; TODO: should return u32?
grammar Bdatacnt : u32* hint(desc "data count") =
| n:Bu32 => n

Expand All @@ -1141,61 +1143,65 @@ grammar Bdatacntsec : u32* hint(desc "data count section") =

;; Modules

;; TODO: avoid double empty lines
grammar Bmagic : () = 0x00 0x61 0x73 0x6D => ()
grammar Bversion : () = 0x01 0x00 0x00 0x00 => ()
grammar Bmodule : module =
| Bmagic
Bversion
Bcustomsec*


type*:Btypesec
Bcustomsec*
type*:Btypesec


import*:Bimportsec
Bcustomsec*
import*:Bimportsec


typeidx^n:Bfuncsec
Bcustomsec*
typeidx^n:Bfuncsec


table*:Btablesec
Bcustomsec*
table*:Btablesec


mem*:Bmemsec
Bcustomsec*
mem*:Bmemsec


global*:Bglobalsec
Bcustomsec*
global*:Bglobalsec


export*:Bexportsec
Bcustomsec*
export*:Bexportsec


start*:Bstartsec
Bcustomsec*
start*:Bstartsec


elem*:Belemsec
Bcustomsec*
elem*:Belemsec


m'*:Bdatacntsec
Bcustomsec*
m'*:Bdatacntsec ;; TODO: should be m'?


(local*, expr)^n:Bcodesec
Bcustomsec*
(local*, expr)^n:Bcodesec


Bcustomsec*
data^m:Bdatasec


Bcustomsec* =>
MODULE type* import* func^n global* table* mem* elem* data^m start* export*
-- if m'* = eps \/ $dataidx_funcs(func^n) = eps
----
-- if m'* =/= eps \/ $dataidx_funcs(func^n) = eps
-- if m = $sum(m'*)
-- if (func = FUNC typeidx local* expr)^n
-- (if func = FUNC typeidx local* expr)^n
8 changes: 6 additions & 2 deletions spectec/src/backend-latex/render.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1237,15 +1237,19 @@ and render_sym env g =
| UnparenG ({it = ParenG g1; _} | g1) -> render_sym env g1

and render_syms sep env gs =
altern_map_nl sep " \\\\ &&&\\quad " (render_sym env) gs
altern_map_nl sep " \\\\ &&& " (render_sym env) gs

and render_prod arrow env prod =
let (g, e, prems) = prod.it in
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
if g.at.right.line = e.at.left.line then
render_conditions env (render_exp env e) "&&&&&" prems
else
render_conditions env ("\\\\\n &&& \\multicolumn{3}{@{}l@{}}{\\qquad " ^
render_exp env e ^ " }") "&&&&&" prems

and render_gram arrow env gram =
let (dots1, prods, dots2) = gram.it in
Expand Down
4 changes: 2 additions & 2 deletions spectec/test-frontend/TEST.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1314,7 +1314,7 @@ def $dataidx_instr(instr : instr) : dataidx*
;; 2-syntax-aux.watsup
rec {

;; 2-syntax-aux.watsup:25.1-25.63
;; 2-syntax-aux.watsup:25.1-25.89
def $dataidx_instrs(instr*) : dataidx*
;; 2-syntax-aux.watsup:26.1-26.31
def $dataidx_instrs([]) = []
Expand All @@ -1335,7 +1335,7 @@ def $dataidx_func(func : func) : dataidx*
;; 2-syntax-aux.watsup
rec {

;; 2-syntax-aux.watsup:35.1-35.61
;; 2-syntax-aux.watsup:35.1-35.87
def $dataidx_funcs(func*) : dataidx*
;; 2-syntax-aux.watsup:36.1-36.30
def $dataidx_funcs([]) = []
Expand Down
39 changes: 24 additions & 15 deletions spectec/test-latex/TEST.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -8330,7 +8330,7 @@ $$
\mathtt{0x02}~~{\mathit{bt}}{:}{\mathtt{blocktype}}~~{({\mathit{in}}{:}{\mathtt{instr}})^\ast}~~\mathtt{0x0B} &\quad\Rightarrow&\quad \mathsf{block}~{\mathit{bt}}~{{\mathit{in}}^\ast} \\ &&|&
\mathtt{0x03}~~{\mathit{bt}}{:}{\mathtt{blocktype}}~~{({\mathit{in}}{:}{\mathtt{instr}})^\ast}~~\mathtt{0x0B} &\quad\Rightarrow&\quad \mathsf{loop}~{\mathit{bt}}~{{\mathit{in}}^\ast} \\ &&|&
\mathtt{0x04}~~{\mathit{bt}}{:}{\mathtt{blocktype}}~~{({\mathit{in}}{:}{\mathtt{instr}})^\ast}~~\mathtt{0x0B} &\quad\Rightarrow&\quad \mathsf{if}~{\mathit{bt}}~{{\mathit{in}}^\ast}~\mathsf{else}~\epsilon \\ &&|&
\mathtt{0x04}~~{\mathit{bt}}{:}{\mathtt{blocktype}}~~{({\mathit{in}}_1{:}{\mathtt{instr}})^\ast} \\ &&&\quad \mathtt{0x05}~~{({\mathit{in}}_2{:}{\mathtt{instr}})^\ast}~~\mathtt{0x0B} &\quad\Rightarrow&\quad \mathsf{if}~{\mathit{bt}}~{{\mathit{in}}_1^\ast}~\mathsf{else}~{{\mathit{in}}_2^\ast} \\ &&|&
\mathtt{0x04}~~{\mathit{bt}}{:}{\mathtt{blocktype}}~~{({\mathit{in}}_1{:}{\mathtt{instr}})^\ast} \\ &&& \mathtt{0x05}~~{({\mathit{in}}_2{:}{\mathtt{instr}})^\ast}~~\mathtt{0x0B} &\quad\Rightarrow&\quad \mathsf{if}~{\mathit{bt}}~{{\mathit{in}}_1^\ast}~\mathsf{else}~{{\mathit{in}}_2^\ast} \\ &&|&
\mathtt{0x0C}~~l{:}{\mathtt{labelidx}} &\quad\Rightarrow&\quad \mathsf{br}~l \\ &&|&
\mathtt{0x0D}~~l{:}{\mathtt{labelidx}} &\quad\Rightarrow&\quad \mathsf{br\_if}~l \\ &&|&
\mathtt{0x0E}~~{l^\ast}{:}{\mathtt{list}}({\mathtt{labelidx}})~~l_n{:}{\mathtt{labelidx}} &\quad\Rightarrow&\quad \mathsf{br\_table}~{l^\ast}~l_n \\ &&|&
Expand Down Expand Up @@ -8389,8 +8389,8 @@ $$
\mathtt{0xFB}~~21{:}{\mathtt{u32}}~~{\mathit{ht}}{:}{\mathtt{heaptype}} &\quad\Rightarrow&\quad \mathsf{ref{.}test}~(\mathsf{ref}~\mathsf{null}~{\mathit{ht}}) \\ &&|&
\mathtt{0xFB}~~22{:}{\mathtt{u32}}~~{\mathit{ht}}{:}{\mathtt{heaptype}} &\quad\Rightarrow&\quad \mathsf{ref{.}cast}~(\mathsf{ref}~{\mathit{ht}}) \\ &&|&
\mathtt{0xFB}~~23{:}{\mathtt{u32}}~~{\mathit{ht}}{:}{\mathtt{heaptype}} &\quad\Rightarrow&\quad \mathsf{ref{.}cast}~(\mathsf{ref}~\mathsf{null}~{\mathit{ht}}) \\ &&|&
\mathtt{0xFB}~~24{:}{\mathtt{u32}}~~({\mathsf{null}}{{{}_{1}^?}}, {\mathsf{null}}{{{}_{2}^?}}){:}{\mathtt{castop}} \\ &&&\quad l{:}{\mathtt{labelidx}}~~{\mathit{ht}}_1{:}{\mathtt{heaptype}}~~{\mathit{ht}}_2{:}{\mathtt{heaptype}} &\quad\Rightarrow&\quad \mathsf{br\_on\_cast}~l~(\mathsf{ref}~{\mathsf{null}}{{{}_{1}^?}}~{\mathit{ht}}_1)~(\mathsf{ref}~{\mathsf{null}}{{{}_{2}^?}}~{\mathit{ht}}_2) \\ &&|&
\mathtt{0xFB}~~25{:}{\mathtt{u32}}~~({\mathsf{null}}{{{}_{1}^?}}, {\mathsf{null}}{{{}_{2}^?}}){:}{\mathtt{castop}} \\ &&&\quad l{:}{\mathtt{labelidx}}~~{\mathit{ht}}_1{:}{\mathtt{heaptype}}~~{\mathit{ht}}_2{:}{\mathtt{heaptype}} &\quad\Rightarrow&\quad \mathsf{br\_on\_cast\_fail}~l~(\mathsf{ref}~{\mathsf{null}}{{{}_{1}^?}}~{\mathit{ht}}_1)~(\mathsf{ref}~{\mathsf{null}}{{{}_{2}^?}}~{\mathit{ht}}_2) \\ &&|&
\mathtt{0xFB}~~24{:}{\mathtt{u32}}~~({\mathsf{null}}{{{}_{1}^?}}, {\mathsf{null}}{{{}_{2}^?}}){:}{\mathtt{castop}} \\ &&& l{:}{\mathtt{labelidx}}~~{\mathit{ht}}_1{:}{\mathtt{heaptype}}~~{\mathit{ht}}_2{:}{\mathtt{heaptype}} &\quad\Rightarrow&\quad \mathsf{br\_on\_cast}~l~(\mathsf{ref}~{\mathsf{null}}{{{}_{1}^?}}~{\mathit{ht}}_1)~(\mathsf{ref}~{\mathsf{null}}{{{}_{2}^?}}~{\mathit{ht}}_2) \\ &&|&
\mathtt{0xFB}~~25{:}{\mathtt{u32}}~~({\mathsf{null}}{{{}_{1}^?}}, {\mathsf{null}}{{{}_{2}^?}}){:}{\mathtt{castop}} \\ &&& l{:}{\mathtt{labelidx}}~~{\mathit{ht}}_1{:}{\mathtt{heaptype}}~~{\mathit{ht}}_2{:}{\mathtt{heaptype}} &\quad\Rightarrow&\quad \mathsf{br\_on\_cast\_fail}~l~(\mathsf{ref}~{\mathsf{null}}{{{}_{1}^?}}~{\mathit{ht}}_1)~(\mathsf{ref}~{\mathsf{null}}{{{}_{2}^?}}~{\mathit{ht}}_2) \\ &&|&
\mathtt{0xFB}~~26{:}{\mathtt{u32}} &\quad\Rightarrow&\quad \mathsf{any{.}convert\_extern} \\ &&|&
\mathtt{0xFB}~~27{:}{\mathtt{u32}} &\quad\Rightarrow&\quad \mathsf{extern{.}convert\_any} \\ &&|&
\mathtt{0xFB}~~28{:}{\mathtt{u32}} &\quad\Rightarrow&\quad \mathsf{ref{.}i{\scriptstyle 31}} \\ &&|&
Expand Down Expand Up @@ -9003,14 +9003,22 @@ $$
$$
\begin{array}{@{}l@{}rrl@{}l@{}l@{}l@{}}
& {\mathtt{elemkind}} &::=& \mathtt{0x00} &\quad\Rightarrow&\quad \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{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}}~~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_{\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}}~~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{elem}} &::=& 0{:}{\mathtt{u32}}~~e_o{:}{\mathtt{expr}}~~{y^\ast}{:}{\mathtt{list}}({\mathtt{funcidx}}) &\quad\Rightarrow&\quad \\
&&& \multicolumn{3}{@{}l@{}}{\qquad \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 \\
&&& \multicolumn{3}{@{}l@{}}{\qquad \mathsf{elem}~{\mathit{rt}}~{(\mathsf{ref{.}func}~y)^\ast}~\mathsf{passive} } \\ &&|&
2{:}{\mathtt{u32}}~~x{:}{\mathtt{tableidx}}~~e{:}{\mathtt{expr}}~~{\mathit{rt}}{:}{\mathtt{elemkind}}~~{y^\ast}{:}{\mathtt{list}}({\mathtt{funcidx}}) &\quad\Rightarrow&\quad \\
&&& \multicolumn{3}{@{}l@{}}{\qquad \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 \\
&&& \multicolumn{3}{@{}l@{}}{\qquad \mathsf{elem}~{\mathit{rt}}~{(\mathsf{ref{.}func}~y)^\ast}~\mathsf{declare} } \\ &&|&
4{:}{\mathtt{u32}}~~e_{\mathsf{o}}{:}{\mathtt{expr}}~~{e^\ast}{:}{\mathtt{list}}({\mathtt{expr}}) &\quad\Rightarrow&\quad \\
&&& \multicolumn{3}{@{}l@{}}{\qquad \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 \\
&&& \multicolumn{3}{@{}l@{}}{\qquad \mathsf{elem}~{\mathit{rt}}~{e^\ast}~\mathsf{passive} } \\ &&|&
6{:}{\mathtt{u32}}~~x{:}{\mathtt{tableidx}}~~e_{\mathsf{o}}{:}{\mathtt{expr}}~~{e^\ast}{:}{\mathtt{list}}({\mathtt{expr}}) &\quad\Rightarrow&\quad \\
&&& \multicolumn{3}{@{}l@{}}{\qquad \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 \\
&&& \multicolumn{3}{@{}l@{}}{\qquad \mathsf{elem}~{\mathit{rt}}~{e^\ast}~\mathsf{declare} } \\
& {\mathtt{elemsec}} &::=& {{\mathit{elem}}^\ast}{:}{{\mathtt{section}}}_{9}({\mathtt{list}}({\mathtt{elem}})) &\quad\Rightarrow&\quad {{\mathit{elem}}^\ast} \\
\end{array}
$$
Expand Down Expand Up @@ -9060,10 +9068,11 @@ $$
\begin{array}{@{}l@{}rrl@{}l@{}l@{}l@{}}
& {\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} &\quad\Rightarrow&\quad \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} \\
& {\mathtt{module}} &::=& {\mathtt{magic}}~~{\mathtt{version}} \\ &&& {{\mathtt{customsec}}^\ast}~~{{\mathit{type}}^\ast}{:}{\mathtt{typesec}} \\ &&& {{\mathtt{customsec}}^\ast}~~{{\mathit{import}}^\ast}{:}{\mathtt{importsec}} \\ &&& {{\mathtt{customsec}}^\ast}~~{{\mathit{typeidx}}^{n}}{:}{\mathtt{funcsec}} \\ &&& {{\mathtt{customsec}}^\ast}~~{{\mathit{table}}^\ast}{:}{\mathtt{tablesec}} \\ &&& {{\mathtt{customsec}}^\ast}~~{{\mathit{mem}}^\ast}{:}{\mathtt{memsec}} \\ &&& {{\mathtt{customsec}}^\ast}~~{{\mathit{global}}^\ast}{:}{\mathtt{globalsec}} \\ &&& {{\mathtt{customsec}}^\ast}~~{{\mathit{export}}^\ast}{:}{\mathtt{exportsec}} \\ &&& {{\mathtt{customsec}}^\ast}~~{{\mathit{start}}^\ast}{:}{\mathtt{startsec}} \\ &&& {{\mathtt{customsec}}^\ast}~~{{\mathit{elem}}^\ast}{:}{\mathtt{elemsec}} \\ &&& {{\mathtt{customsec}}^\ast}~~{{m'}^\ast}{:}{\mathtt{datacntsec}} \\ &&& {{\mathtt{customsec}}^\ast}~~{({{\mathit{local}}^\ast}, {\mathit{expr}})^{n}}{:}{\mathtt{codesec}} \\ &&& {{\mathtt{customsec}}^\ast}~~{{\mathit{data}}^{m}}{:}{\mathtt{datasec}} \\ &&& {{\mathtt{customsec}}^\ast} &\quad\Rightarrow&\quad \\
&&& \multicolumn{3}{@{}l@{}}{\qquad \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} } \\
&&&&& \multicolumn{2}{l@{}}{\quad \mbox{if}~{{m'}^\ast} \neq \epsilon \lor {\mathrm{dataidx}}({{\mathit{func}}^{n}}) = \epsilon} \\
&&&&& \multicolumn{2}{l@{}}{\quad {\land}~m = {\mathrm{sum}}({{m'}^\ast})} \\
&&&&& \multicolumn{2}{l@{}}{\quad {\land}~({\mathit{func}} = \mathsf{func}~{\mathit{typeidx}}~{{\mathit{local}}^\ast}~{\mathit{expr}})^{n}} \\
\end{array}
$$

Expand Down
Loading

0 comments on commit dd3c8d4

Please sign in to comment.