Skip to content

Commit 24a7a71

Browse files
zilinczilinc
authored
[spec] Partly revert #2162: ignore start for func refs (#2201)
1 parent bd4633a commit 24a7a71

6 files changed

Lines changed: 31 additions & 31 deletions

File tree

‎specification/wasm-3.0/2.4-validation.modules.spectec‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -138,10 +138,10 @@ relation Types_ok: context |- type* : deftype* hint(name "T-types") hin
138138
relation Globals_ok: context |- global* : globaltype* hint(name "T-globals") hint(macro "%globals")
139139

140140
;; HACK for notation
141-
syntax nonfuncs = global* mem* table* elem* start? export*
141+
syntax nonfuncs = global* mem* table* elem* export*
142142
def $funcidx_nonfuncs(nonfuncs) : funcidx* hint(show $funcidx(%)) hint(macro "freefuncidx")
143-
def $funcidx_nonfuncs(global* mem* table* elem* start? export*) =
144-
$funcidx_module(MODULE eps eps eps global* mem* table* eps eps elem* start? export*)
143+
def $funcidx_nonfuncs(global* mem* table* elem* export*) =
144+
$funcidx_module(MODULE eps eps eps global* mem* table* eps eps elem* eps export*)
145145

146146
rule Module_ok:
147147
|- MODULE type* import* tag* global* mem* table* func* data* elem* start? export* : $clos_moduletype(C, xt_I* -> xt_E*)
@@ -163,7 +163,7 @@ rule Module_ok:
163163
-- if C = C' ++ {TAGS jt_I* jt*, GLOBALS gt*, MEMS mt_I* mt*, TABLES tt_I* tt*, DATAS ok*, ELEMS rt*}
164164
----
165165
-- if C' = {TYPES dt'*, GLOBALS gt_I*, FUNCS dt_I* dt*, REFS x*}
166-
-- if x* = $funcidx_nonfuncs(global* mem* table* elem* start? export*)
166+
-- if x* = $funcidx_nonfuncs(global* mem* table* elem* export*)
167167
----
168168
-- if jt_I* = $tagsxt(xt_I*)
169169
-- if gt_I* = $globalsxt(xt_I*)

‎specification/wasm-latest/2.4-validation.modules.spectec‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -138,10 +138,10 @@ relation Types_ok: context |- type* : deftype* hint(name "T-types") hin
138138
relation Globals_ok: context |- global* : globaltype* hint(name "T-globals") hint(macro "%globals")
139139

140140
;; HACK for notation
141-
syntax nonfuncs = global* mem* table* elem* start? export*
141+
syntax nonfuncs = global* mem* table* elem* export*
142142
def $funcidx_nonfuncs(nonfuncs) : funcidx* hint(show $funcidx(%)) hint(macro "freefuncidx")
143-
def $funcidx_nonfuncs(global* mem* table* elem* start? export*) =
144-
$funcidx_module(MODULE eps eps eps global* mem* table* eps eps elem* start? export*)
143+
def $funcidx_nonfuncs(global* mem* table* elem* export*) =
144+
$funcidx_module(MODULE eps eps eps global* mem* table* eps eps elem* eps export*)
145145

146146
rule Module_ok:
147147
|- MODULE type* import* tag* global* mem* table* func* data* elem* start? export* : $clos_moduletype(C, xt_I* -> xt_E*)
@@ -163,7 +163,7 @@ rule Module_ok:
163163
-- if C = C' ++ {TAGS jt_I* jt*, GLOBALS gt*, MEMS mt_I* mt*, TABLES tt_I* tt*, DATAS ok*, ELEMS rt*}
164164
----
165165
-- if C' = {TYPES dt'*, GLOBALS gt_I*, FUNCS dt_I* dt*, REFS x*}
166-
-- if x* = $funcidx_nonfuncs(global* mem* table* elem* start? export*)
166+
-- if x* = $funcidx_nonfuncs(global* mem* table* elem* export*)
167167
----
168168
-- if jt_I* = $tagsxt(xt_I*)
169169
-- if gt_I* = $globalsxt(xt_I*)

‎spectec/test-frontend/TEST.md‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -4770,12 +4770,12 @@ relation Types_ok: `%|-%:%`(context, type*, deftype*)
47704770

47714771
;; ../../../../specification/wasm-latest/2.4-validation.modules.spectec
47724772
syntax nonfuncs =
4773-
| `%%%%%%`(`global*` : global*, `mem*` : mem*, `table*` : table*, `elem*` : elem*, `start?` : start?, `export*` : export*)
4773+
| `%%%%%`(`global*` : global*, `mem*` : mem*, `table*` : table*, `elem*` : elem*, `export*` : export*)
47744774

47754775
;; ../../../../specification/wasm-latest/2.4-validation.modules.spectec
47764776
def $funcidx_nonfuncs(nonfuncs : nonfuncs) : funcidx*
47774777
;; ../../../../specification/wasm-latest/2.4-validation.modules.spectec
4778-
def $funcidx_nonfuncs{`global*` : global*, `mem*` : mem*, `table*` : table*, `elem*` : elem*, `start?` : start?, `export*` : export*}(`%%%%%%`_nonfuncs(global*{global <- `global*`}, mem*{mem <- `mem*`}, table*{table <- `table*`}, elem*{elem <- `elem*`}, start?{start <- `start?`}, export*{export <- `export*`})) = $funcidx_module(MODULE_module(`%`_list([],), `%`_list([],), `%`_list([],), `%`_list(global*{global <- `global*`},), `%`_list(mem*{mem <- `mem*`},), `%`_list(table*{table <- `table*`},), `%`_list([],), `%`_list([],), `%`_list(elem*{elem <- `elem*`},), start?{start <- `start?`}, `%`_list(export*{export <- `export*`},)))
4778+
def $funcidx_nonfuncs{`global*` : global*, `mem*` : mem*, `table*` : table*, `elem*` : elem*, `export*` : export*}(`%%%%%`_nonfuncs(global*{global <- `global*`}, mem*{mem <- `mem*`}, table*{table <- `table*`}, elem*{elem <- `elem*`}, export*{export <- `export*`})) = $funcidx_module(MODULE_module(`%`_list([],), `%`_list([],), `%`_list([],), `%`_list(global*{global <- `global*`},), `%`_list(mem*{mem <- `mem*`},), `%`_list(table*{table <- `table*`},), `%`_list([],), `%`_list([],), `%`_list(elem*{elem <- `elem*`},), ?(), `%`_list(export*{export <- `export*`},)))
47794779

47804780
;; ../../../../specification/wasm-latest/2.4-validation.modules.spectec
47814781
relation Module_ok: `|-%:%`(module, moduletype)
@@ -4796,7 +4796,7 @@ relation Module_ok: `|-%:%`(module, moduletype)
47964796
-- if $disjoint_(syntax name, nm*{nm <- `nm*`})
47974797
-- if (C = C' +++ {TYPES [], TAGS jt_I*{jt_I <- `jt_I*`} ++ jt*{jt <- `jt*`}, GLOBALS gt*{gt <- `gt*`}, MEMS mt_I*{mt_I <- `mt_I*`} ++ mt*{mt <- `mt*`}, TABLES tt_I*{tt_I <- `tt_I*`} ++ tt*{tt <- `tt*`}, FUNCS [], DATAS ok*{ok <- `ok*`}, ELEMS rt*{rt <- `rt*`}, LOCALS [], LABELS [], RETURN ?(), REFS [], RECS []})
47984798
-- if (C' = {TYPES dt'*{dt' <- `dt'*`}, TAGS [], GLOBALS gt_I*{gt_I <- `gt_I*`}, MEMS [], TABLES [], FUNCS dt_I*{dt_I <- `dt_I*`} ++ dt*{dt <- `dt*`}, DATAS [], ELEMS [], LOCALS [], LABELS [], RETURN ?(), REFS x*{x <- `x*`}, RECS []})
4799-
-- if (x*{x <- `x*`} = $funcidx_nonfuncs(`%%%%%%`_nonfuncs(global*{global <- `global*`}, mem*{mem <- `mem*`}, table*{table <- `table*`}, elem*{elem <- `elem*`}, start?{start <- `start?`}, export*{export <- `export*`})))
4799+
-- if (x*{x <- `x*`} = $funcidx_nonfuncs(`%%%%%`_nonfuncs(global*{global <- `global*`}, mem*{mem <- `mem*`}, table*{table <- `table*`}, elem*{elem <- `elem*`}, export*{export <- `export*`})))
48004800
-- if (jt_I*{jt_I <- `jt_I*`} = $tagsxt(xt_I*{xt_I <- `xt_I*`}))
48014801
-- if (gt_I*{gt_I <- `gt_I*`} = $globalsxt(xt_I*{xt_I <- `xt_I*`}))
48024802
-- if (mt_I*{mt_I <- `mt_I*`} = $memsxt(xt_I*{xt_I <- `xt_I*`}))

‎spectec/test-latex/TEST.md‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -7904,16 +7904,16 @@ $\boxed{{\mathit{context}} \vdash {{\mathit{global}}^\ast} : {{\mathit{globaltyp
79047904

79057905
$$
79067906
\begin{array}[t]{@{}lrrl@{}l@{}}
7907-
& {\mathit{nonfuncs}} & ::= & {{\mathit{global}}^\ast}~{{\mathit{mem}}^\ast}~{{\mathit{table}}^\ast}~{{\mathit{elem}}^\ast}~{{\mathit{start}}^?}~{{\mathit{export}}^\ast} \\
7907+
& {\mathit{nonfuncs}} & ::= & {{\mathit{global}}^\ast}~{{\mathit{mem}}^\ast}~{{\mathit{table}}^\ast}~{{\mathit{elem}}^\ast}~{{\mathit{export}}^\ast} \\
79087908
\end{array}
79097909
$$
79107910

79117911
$$
79127912
\begin{array}[t]{@{}lcl@{}l@{}}
7913-
{\mathrm{funcidx}}({{\mathit{global}}^\ast}~{{\mathit{mem}}^\ast}~{{\mathit{table}}^\ast}~{{\mathit{elem}}^\ast}~{{\mathit{start}}^?}~{{\mathit{export}}^\ast}) & = & & \\
7913+
{\mathrm{funcidx}}({{\mathit{global}}^\ast}~{{\mathit{mem}}^\ast}~{{\mathit{table}}^\ast}~{{\mathit{elem}}^\ast}~{{\mathit{export}}^\ast}) & = & & \\
79147914
\multicolumn{4}{@{}l@{}}{\quad
79157915
\begin{array}[t]{@{}l@{}}
7916-
{\mathrm{funcidx}}(\mathsf{module}~\epsilon~\epsilon~\epsilon~{{\mathit{global}}^\ast}~{{\mathit{mem}}^\ast}~{{\mathit{table}}^\ast}~\epsilon~\epsilon~{{\mathit{elem}}^\ast}~{{\mathit{start}}^?}~{{\mathit{export}}^\ast}) \\
7916+
{\mathrm{funcidx}}(\mathsf{module}~\epsilon~\epsilon~\epsilon~{{\mathit{global}}^\ast}~{{\mathit{mem}}^\ast}~{{\mathit{table}}^\ast}~\epsilon~\epsilon~{{\mathit{elem}}^\ast}~\epsilon~{{\mathit{export}}^\ast}) \\
79177917
\end{array}
79187918
} \\
79197919
\end{array}
@@ -7951,7 +7951,7 @@ C = {C'} \oplus \{ \mathsf{tags}~{{\mathit{jt}}_{\mathsf{i}}^\ast}~{{\mathit{jt}
79517951
\\
79527952
{C'} = \{ \mathsf{types}~{{\mathit{dt}'}^\ast},\;\allowbreak \mathsf{globals}~{{\mathit{gt}}_{\mathsf{i}}^\ast},\;\allowbreak \mathsf{funcs}~{{\mathit{dt}}_{\mathsf{i}}^\ast}~{{\mathit{dt}}^\ast},\;\allowbreak \mathsf{refs}~{x^\ast} \}
79537953
\qquad
7954-
{x^\ast} = {\mathrm{funcidx}}({{\mathit{global}}^\ast}~{{\mathit{mem}}^\ast}~{{\mathit{table}}^\ast}~{{\mathit{elem}}^\ast}~{{\mathit{start}}^?}~{{\mathit{export}}^\ast})
7954+
{x^\ast} = {\mathrm{funcidx}}({{\mathit{global}}^\ast}~{{\mathit{mem}}^\ast}~{{\mathit{table}}^\ast}~{{\mathit{elem}}^\ast}~{{\mathit{export}}^\ast})
79557955
\\
79567956
{{\mathit{jt}}_{\mathsf{i}}^\ast} = {\mathrm{tags}}({{\mathit{xt}}_{\mathsf{i}}^\ast})
79577957
\qquad

‎spectec/test-middlend/TEST.md‎

Lines changed: 9 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -4293,12 +4293,12 @@ relation Types_ok: `%|-%:%`(context, type*, deftype*)
42934293

42944294
;; ../../../../specification/wasm-latest/2.4-validation.modules.spectec
42954295
syntax nonfuncs =
4296-
| `%%%%%%`(`global*` : global*, `mem*` : mem*, `table*` : table*, `elem*` : elem*, `start?` : start?, `export*` : export*)
4296+
| `%%%%%`(`global*` : global*, `mem*` : mem*, `table*` : table*, `elem*` : elem*, `export*` : export*)
42974297

42984298
;; ../../../../specification/wasm-latest/2.4-validation.modules.spectec
42994299
def $funcidx_nonfuncs(nonfuncs : nonfuncs) : funcidx*
43004300
;; ../../../../specification/wasm-latest/2.4-validation.modules.spectec
4301-
def $funcidx_nonfuncs{`global*` : global*, `mem*` : mem*, `table*` : table*, `elem*` : elem*, `start?` : start?, `export*` : export*}(`%%%%%%`_nonfuncs(global*{global <- `global*`}, mem*{mem <- `mem*`}, table*{table <- `table*`}, elem*{elem <- `elem*`}, start?{start <- `start?`}, export*{export <- `export*`})) = $funcidx_module(MODULE_module(`%`_list([],), `%`_list([],), `%`_list([],), `%`_list(global*{global <- `global*`},), `%`_list(mem*{mem <- `mem*`},), `%`_list(table*{table <- `table*`},), `%`_list([],), `%`_list([],), `%`_list(elem*{elem <- `elem*`},), start?{start <- `start?`}, `%`_list(export*{export <- `export*`},)))
4301+
def $funcidx_nonfuncs{`global*` : global*, `mem*` : mem*, `table*` : table*, `elem*` : elem*, `export*` : export*}(`%%%%%`_nonfuncs(global*{global <- `global*`}, mem*{mem <- `mem*`}, table*{table <- `table*`}, elem*{elem <- `elem*`}, export*{export <- `export*`})) = $funcidx_module(MODULE_module(`%`_list([],), `%`_list([],), `%`_list([],), `%`_list(global*{global <- `global*`},), `%`_list(mem*{mem <- `mem*`},), `%`_list(table*{table <- `table*`},), `%`_list([],), `%`_list([],), `%`_list(elem*{elem <- `elem*`},), ?(), `%`_list(export*{export <- `export*`},)))
43024302

43034303
;; ../../../../specification/wasm-latest/2.4-validation.modules.spectec
43044304
relation Module_ok: `|-%:%`(module, moduletype)
@@ -4319,7 +4319,7 @@ relation Module_ok: `|-%:%`(module, moduletype)
43194319
-- if $disjoint_(syntax name, nm*{nm <- `nm*`})
43204320
-- if (C = C' +++ {TYPES [], TAGS jt_I*{jt_I <- `jt_I*`} ++ jt*{jt <- `jt*`}, GLOBALS gt*{gt <- `gt*`}, MEMS mt_I*{mt_I <- `mt_I*`} ++ mt*{mt <- `mt*`}, TABLES tt_I*{tt_I <- `tt_I*`} ++ tt*{tt <- `tt*`}, FUNCS [], DATAS ok*{ok <- `ok*`}, ELEMS rt*{rt <- `rt*`}, LOCALS [], LABELS [], RETURN ?(), REFS [], RECS []})
43214321
-- if (C' = {TYPES dt'*{dt' <- `dt'*`}, TAGS [], GLOBALS gt_I*{gt_I <- `gt_I*`}, MEMS [], TABLES [], FUNCS dt_I*{dt_I <- `dt_I*`} ++ dt*{dt <- `dt*`}, DATAS [], ELEMS [], LOCALS [], LABELS [], RETURN ?(), REFS x*{x <- `x*`}, RECS []})
4322-
-- if (x*{x <- `x*`} = $funcidx_nonfuncs(`%%%%%%`_nonfuncs(global*{global <- `global*`}, mem*{mem <- `mem*`}, table*{table <- `table*`}, elem*{elem <- `elem*`}, start?{start <- `start?`}, export*{export <- `export*`})))
4322+
-- if (x*{x <- `x*`} = $funcidx_nonfuncs(`%%%%%`_nonfuncs(global*{global <- `global*`}, mem*{mem <- `mem*`}, table*{table <- `table*`}, elem*{elem <- `elem*`}, export*{export <- `export*`})))
43234323
-- if (jt_I*{jt_I <- `jt_I*`} = $tagsxt(xt_I*{xt_I <- `xt_I*`}))
43244324
-- if (gt_I*{gt_I <- `gt_I*`} = $globalsxt(xt_I*{xt_I <- `xt_I*`}))
43254325
-- if (mt_I*{mt_I <- `mt_I*`} = $memsxt(xt_I*{xt_I <- `xt_I*`}))
@@ -16167,12 +16167,12 @@ relation Types_ok: `%|-%:%`(context, type*, deftype*)
1616716167

1616816168
;; ../../../../specification/wasm-latest/2.4-validation.modules.spectec
1616916169
syntax nonfuncs =
16170-
| `%%%%%%`(`global*` : global*, `mem*` : mem*, `table*` : table*, `elem*` : elem*, `start?` : start?, `export*` : export*)
16170+
| `%%%%%`(`global*` : global*, `mem*` : mem*, `table*` : table*, `elem*` : elem*, `export*` : export*)
1617116171

1617216172
;; ../../../../specification/wasm-latest/2.4-validation.modules.spectec
1617316173
def $funcidx_nonfuncs(nonfuncs : nonfuncs) : funcidx*
1617416174
;; ../../../../specification/wasm-latest/2.4-validation.modules.spectec
16175-
def $funcidx_nonfuncs{`global*` : global*, `mem*` : mem*, `table*` : table*, `elem*` : elem*, `start?` : start?, `export*` : export*}(`%%%%%%`_nonfuncs(global*{global <- `global*`}, mem*{mem <- `mem*`}, table*{table <- `table*`}, elem*{elem <- `elem*`}, start?{start <- `start?`}, export*{export <- `export*`})) = $funcidx_module(MODULE_module(`%`_list([],), `%`_list([],), `%`_list([],), `%`_list(global*{global <- `global*`},), `%`_list(mem*{mem <- `mem*`},), `%`_list(table*{table <- `table*`},), `%`_list([],), `%`_list([],), `%`_list(elem*{elem <- `elem*`},), start?{start <- `start?`}, `%`_list(export*{export <- `export*`},)))
16175+
def $funcidx_nonfuncs{`global*` : global*, `mem*` : mem*, `table*` : table*, `elem*` : elem*, `export*` : export*}(`%%%%%`_nonfuncs(global*{global <- `global*`}, mem*{mem <- `mem*`}, table*{table <- `table*`}, elem*{elem <- `elem*`}, export*{export <- `export*`})) = $funcidx_module(MODULE_module(`%`_list([],), `%`_list([],), `%`_list([],), `%`_list(global*{global <- `global*`},), `%`_list(mem*{mem <- `mem*`},), `%`_list(table*{table <- `table*`},), `%`_list([],), `%`_list([],), `%`_list(elem*{elem <- `elem*`},), ?(), `%`_list(export*{export <- `export*`},)))
1617616176

1617716177
;; ../../../../specification/wasm-latest/2.4-validation.modules.spectec
1617816178
relation Module_ok: `|-%:%`(module, moduletype)
@@ -16193,7 +16193,7 @@ relation Module_ok: `|-%:%`(module, moduletype)
1619316193
-- if $disjoint_(syntax name, nm*{nm <- `nm*`})
1619416194
-- if (C = C' +++ {TYPES [], TAGS jt_I*{jt_I <- `jt_I*`} ++ jt*{jt <- `jt*`}, GLOBALS gt*{gt <- `gt*`}, MEMS mt_I*{mt_I <- `mt_I*`} ++ mt*{mt <- `mt*`}, TABLES tt_I*{tt_I <- `tt_I*`} ++ tt*{tt <- `tt*`}, FUNCS [], DATAS ok*{ok <- `ok*`}, ELEMS rt*{rt <- `rt*`}, LOCALS [], LABELS [], RETURN ?(), REFS [], RECS []})
1619516195
-- if (C' = {TYPES dt'*{dt' <- `dt'*`}, TAGS [], GLOBALS gt_I*{gt_I <- `gt_I*`}, MEMS [], TABLES [], FUNCS dt_I*{dt_I <- `dt_I*`} ++ dt*{dt <- `dt*`}, DATAS [], ELEMS [], LOCALS [], LABELS [], RETURN ?(), REFS x*{x <- `x*`}, RECS []})
16196-
-- if (x*{x <- `x*`} = $funcidx_nonfuncs(`%%%%%%`_nonfuncs(global*{global <- `global*`}, mem*{mem <- `mem*`}, table*{table <- `table*`}, elem*{elem <- `elem*`}, start?{start <- `start?`}, export*{export <- `export*`})))
16196+
-- if (x*{x <- `x*`} = $funcidx_nonfuncs(`%%%%%`_nonfuncs(global*{global <- `global*`}, mem*{mem <- `mem*`}, table*{table <- `table*`}, elem*{elem <- `elem*`}, export*{export <- `export*`})))
1619716197
-- if (jt_I*{jt_I <- `jt_I*`} = $tagsxt(xt_I*{xt_I <- `xt_I*`}))
1619816198
-- if (gt_I*{gt_I <- `gt_I*`} = $globalsxt(xt_I*{xt_I <- `xt_I*`}))
1619916199
-- if (mt_I*{mt_I <- `mt_I*`} = $memsxt(xt_I*{xt_I <- `xt_I*`}))
@@ -28161,12 +28161,12 @@ relation Types_ok: `%|-%:%`(context, type*, deftype*)
2816128161

2816228162
;; ../../../../specification/wasm-latest/2.4-validation.modules.spectec
2816328163
syntax nonfuncs =
28164-
| `%%%%%%`(`global*` : global*, `mem*` : mem*, `table*` : table*, `elem*` : elem*, `start?` : start?, `export*` : export*)
28164+
| `%%%%%`(`global*` : global*, `mem*` : mem*, `table*` : table*, `elem*` : elem*, `export*` : export*)
2816528165

2816628166
;; ../../../../specification/wasm-latest/2.4-validation.modules.spectec
2816728167
def $funcidx_nonfuncs(nonfuncs : nonfuncs) : funcidx*
2816828168
;; ../../../../specification/wasm-latest/2.4-validation.modules.spectec
28169-
def $funcidx_nonfuncs{`global*` : global*, `mem*` : mem*, `table*` : table*, `elem*` : elem*, `start?` : start?, `export*` : export*}(`%%%%%%`_nonfuncs(global*{global <- `global*`}, mem*{mem <- `mem*`}, table*{table <- `table*`}, elem*{elem <- `elem*`}, start?{start <- `start?`}, export*{export <- `export*`})) = $funcidx_module(MODULE_module(`%`_list([],), `%`_list([],), `%`_list([],), `%`_list(global*{global <- `global*`},), `%`_list(mem*{mem <- `mem*`},), `%`_list(table*{table <- `table*`},), `%`_list([],), `%`_list([],), `%`_list(elem*{elem <- `elem*`},), start?{start <- `start?`}, `%`_list(export*{export <- `export*`},)))
28169+
def $funcidx_nonfuncs{`global*` : global*, `mem*` : mem*, `table*` : table*, `elem*` : elem*, `export*` : export*}(`%%%%%`_nonfuncs(global*{global <- `global*`}, mem*{mem <- `mem*`}, table*{table <- `table*`}, elem*{elem <- `elem*`}, export*{export <- `export*`})) = $funcidx_module(MODULE_module(`%`_list([],), `%`_list([],), `%`_list([],), `%`_list(global*{global <- `global*`},), `%`_list(mem*{mem <- `mem*`},), `%`_list(table*{table <- `table*`},), `%`_list([],), `%`_list([],), `%`_list(elem*{elem <- `elem*`},), ?(), `%`_list(export*{export <- `export*`},)))
2817028170

2817128171
;; ../../../../specification/wasm-latest/2.4-validation.modules.spectec
2817228172
relation Module_ok: `|-%:%`(module, moduletype)
@@ -28196,7 +28196,7 @@ relation Module_ok: `|-%:%`(module, moduletype)
2819628196
-- if $disjoint_(syntax name, nm*{nm <- `nm*`})
2819728197
-- if (C = C' +++ {TYPES [], TAGS jt_I*{jt_I <- `jt_I*`} ++ jt*{jt <- `jt*`}, GLOBALS gt*{gt <- `gt*`}, MEMS mt_I*{mt_I <- `mt_I*`} ++ mt*{mt <- `mt*`}, TABLES tt_I*{tt_I <- `tt_I*`} ++ tt*{tt <- `tt*`}, FUNCS [], DATAS ok*{ok <- `ok*`}, ELEMS rt*{rt <- `rt*`}, LOCALS [], LABELS [], RETURN ?(), REFS [], RECS []})
2819828198
-- if (C' = {TYPES dt'*{dt' <- `dt'*`}, TAGS [], GLOBALS gt_I*{gt_I <- `gt_I*`}, MEMS [], TABLES [], FUNCS dt_I*{dt_I <- `dt_I*`} ++ dt*{dt <- `dt*`}, DATAS [], ELEMS [], LOCALS [], LABELS [], RETURN ?(), REFS x*{x <- `x*`}, RECS []})
28199-
-- if (x*{x <- `x*`} = $funcidx_nonfuncs(`%%%%%%`_nonfuncs(global*{global <- `global*`}, mem*{mem <- `mem*`}, table*{table <- `table*`}, elem*{elem <- `elem*`}, start?{start <- `start?`}, export*{export <- `export*`})))
28199+
-- if (x*{x <- `x*`} = $funcidx_nonfuncs(`%%%%%`_nonfuncs(global*{global <- `global*`}, mem*{mem <- `mem*`}, table*{table <- `table*`}, elem*{elem <- `elem*`}, export*{export <- `export*`})))
2820028200
-- if (jt_I*{jt_I <- `jt_I*`} = $tagsxt(xt_I*{xt_I <- `xt_I*`}))
2820128201
-- if (gt_I*{gt_I <- `gt_I*`} = $globalsxt(xt_I*{xt_I <- `xt_I*`}))
2820228202
-- if (mt_I*{mt_I <- `mt_I*`} = $memsxt(xt_I*{xt_I <- `xt_I*`}))

0 commit comments

Comments
 (0)