From 2ca8cdd96bcd3db89f33ca8ca86ae4ca7625988a Mon Sep 17 00:00:00 2001 From: Thomas Lively Date: Tue, 7 Jul 2026 18:35:22 -0700 Subject: [PATCH 1/3] Exact func externtypes types Update the syntax of func externtypes and func types in the typing context to include exactness. This allows specifying exact function imports and properly typing ref.func as exact for exact imports and defined functions and otherwise as inexact. --- document/core/util/macros.def | 3 +++ .../wasm-latest/1.2-syntax.types.spectec | 22 ++++++++++++++----- .../2.0-validation.contexts.spectec | 2 +- .../wasm-latest/2.1-validation.types.spectec | 2 +- .../2.2-validation.subtyping.spectec | 4 ++-- .../2.3-validation.instructions.spectec | 16 ++++++++++---- .../2.4-validation.modules.spectec | 12 +++++----- .../wasm-latest/4.1-execution.values.spectec | 2 +- .../wasm-latest/5.2-binary.types.spectec | 3 ++- .../wasm-latest/6.2-text.types.spectec | 3 ++- 10 files changed, 48 insertions(+), 21 deletions(-) diff --git a/document/core/util/macros.def b/document/core/util/macros.def index 35413fb95..8676c91fe 100644 --- a/document/core/util/macros.def +++ b/document/core/util/macros.def @@ -239,6 +239,7 @@ .. |NULL| mathdef:: \xref{syntax/types}{syntax-reftype}{\K{null}} .. |EXACT| mathdef:: \xref{syntax/types}{syntax-heaptype}{\K{exact}} +.. |INEXACT| mathdef:: {} .. |ANY| mathdef:: \xref{syntax/types}{syntax-heaptype}{\K{any}} .. |EQT| mathdef:: \xref{syntax/types}{syntax-heaptype}{\K{eq}} .. |I31| mathdef:: \xref{syntax/types}{syntax-heaptype}{\K{i\scriptstyle31}} @@ -309,6 +310,7 @@ .. |subtype| mathdef:: \xref{syntax/types}{syntax-subtype}{\X{subtype}} .. |rectype| mathdef:: \xref{syntax/types}{syntax-rectype}{\X{rectype}} .. |deftype| mathdef:: \xref{valid/conventions}{syntax-deftype}{\X{deftype}} +.. |exact| mathdef:: \X{exact} .. |globaltype| mathdef:: \xref{syntax/types}{syntax-globaltype}{\X{globaltype}} .. |tabletype| mathdef:: \xref{syntax/types}{syntax-tabletype}{\X{tabletype}} @@ -349,6 +351,7 @@ .. |unrollht| mathdef:: \xref{appendix/properties}{aux-unroll-heaptype}{\F{unroll}} .. |unpack| mathdef:: \xref{syntax/types}{aux-unpack}{\F{unpack}} +.. |exactheaptype| mathdef:: \F{exactheaptype} .. |funcsxt| mathdef:: \xref{syntax/types}{syntax-externtype}{\F{funcs}} .. |tablesxt| mathdef:: \xref{syntax/types}{syntax-externtype}{\F{tables}} diff --git a/specification/wasm-latest/1.2-syntax.types.spectec b/specification/wasm-latest/1.2-syntax.types.spectec index 25990998e..0502851e4 100644 --- a/specification/wasm-latest/1.2-syntax.types.spectec +++ b/specification/wasm-latest/1.2-syntax.types.spectec @@ -7,6 +7,9 @@ ;; TODO(3, rossberg): add ability to do this inline syntax null hint(show NULL) hint(macro "%" "%") = NULL +syntax exact hint(desc "exactness") = + | EXACT | INEXACT + syntax addrtype hint(desc "address type") = | I32 | I64 @@ -32,6 +35,8 @@ syntax rectype hint(desc "recursive type") ;; forward decl syntax deftype hint(desc "defined type") = | _DEF rectype n hint(show %.%) +syntax exactdeftype hint(show (exact deftype)) = exact deftype + syntax typeuse/syn hint(desc "type use") = | _IDX typeidx | ... syntax typeuse/sem = @@ -85,6 +90,12 @@ def $NULLEXNREF = (REF NULL NOEXN) def $NULLEXTERNREF = (REF NULL NOEXTERN) +def $exactheaptype(exact, typeuse) : heaptype + +def $exactheaptype(EXACT, typeuse) = EXACT typeuse +def $exactheaptype(INEXACT, typeuse) = typeuse + + ;; Packed types syntax packtype hint(desc "packed type") = I8 | I16 @@ -141,7 +152,7 @@ syntax datatype hint(desc "data type") = OK hint(macro "%data") syntax elemtype hint(desc "element type") = reftype syntax externtype hint(desc "external type") hint(macro "%" "XT%") = - | TAG tagtype | GLOBAL globaltype | MEM memtype | TABLE tabletype | FUNC typeuse + | TAG tagtype | GLOBAL globaltype | MEM memtype | TABLE tabletype | FUNC exact typeuse syntax moduletype hint(desc "module type") = externtype* -> externtype* hint(macro "toM") @@ -156,6 +167,7 @@ var at : addrtype ;; var bt : blocktype ;; defined below var ct : comptype var dt : deftype +var edt : exactdeftype var et : elemtype var ft : fieldtype var gt : globaltype @@ -315,7 +327,7 @@ def $tagsxt(externtype*) : tagtype* hint(show $tags(%)) hint(macro "ta def $globalsxt(externtype*) : globaltype* hint(show $globals(%)) hint(macro "globalsxt") def $memsxt(externtype*) : memtype* hint(show $mems(%)) hint(macro "memsxt") def $tablesxt(externtype*) : tabletype* hint(show $tables(%)) hint(macro "tablesxt") -def $funcsxt(externtype*) : deftype* hint(show $funcs(%)) hint(macro "funcsxt") +def $funcsxt(externtype*) : exactdeftype* hint(show $funcs(%)) hint(macro "funcsxt") def $tagsxt(eps) = eps def $tagsxt((TAG jt) xt*) = jt $tagsxt(xt*) @@ -334,7 +346,7 @@ def $tablesxt((TABLE tt) xt*) = tt $tablesxt(xt*) def $tablesxt(externtype xt*) = $tablesxt(xt*) -- otherwise def $funcsxt(eps) = eps -def $funcsxt((FUNC dt) xt*) = dt $funcsxt(xt*) +def $funcsxt((FUNC exact dt) xt*) = (exact dt) $funcsxt(xt*) def $funcsxt(externtype xt*) = $funcsxt(xt*) -- otherwise @@ -436,7 +448,7 @@ def $subst_externtype((TAG jt), tv*, tu*) = TAG $subst_tagtype(jt, tv*, tu*) def $subst_externtype((GLOBAL gt), tv*, tu*) = GLOBAL $subst_globaltype(gt, tv*, tu*) def $subst_externtype((TABLE tt), tv*, tu*) = TABLE $subst_tabletype(tt, tv*, tu*) def $subst_externtype((MEM mt), tv*, tu*) = MEM $subst_memtype(mt, tv*, tu*) -def $subst_externtype((FUNC dt), tv*, tu*) = FUNC $subst_deftype(dt, tv*, tu*) +def $subst_externtype((FUNC exact dt), tv*, tu*) = FUNC exact $subst_deftype(dt, tv*, tu*) def $subst_moduletype(xt_1* -> xt_2*, tv*, tu*) = $subst_externtype(xt_1, tv*, tu*)* -> $subst_externtype(xt_2, tv*, tu*)* @@ -598,7 +610,7 @@ def $free_externtype(TAG tagtype) = $free_tagtype(tagtype) def $free_externtype(GLOBAL globaltype) = $free_globaltype(globaltype) def $free_externtype(MEM memtype) = $free_memtype(memtype) def $free_externtype(TABLE tabletype) = $free_tabletype(tabletype) -def $free_externtype(FUNC typeuse) = $free_typeuse(typeuse) +def $free_externtype(FUNC exact typeuse) = $free_typeuse(typeuse) def $free_moduletype(externtype_1* -> externtype_2*) = $free_list($free_externtype(externtype_1)*) ++ diff --git a/specification/wasm-latest/2.0-validation.contexts.spectec b/specification/wasm-latest/2.0-validation.contexts.spectec index e9205fa2b..a48d50338 100644 --- a/specification/wasm-latest/2.0-validation.contexts.spectec +++ b/specification/wasm-latest/2.0-validation.contexts.spectec @@ -28,7 +28,7 @@ syntax context hint(desc "context") hint(macro "%" "C%") = GLOBALS globaltype* hint(desc "global"), MEMS memtype* hint(desc "memory"), TABLES tabletype* hint(desc "table"), - FUNCS deftype* hint(desc "function"), + FUNCS exactdeftype* hint(desc "function"), DATAS datatype* hint(desc "data segment"), ELEMS elemtype* hint(desc "element segment"), LOCALS localtype* hint(desc "local"), diff --git a/specification/wasm-latest/2.1-validation.types.spectec b/specification/wasm-latest/2.1-validation.types.spectec index ddb81eb2f..c1089a135 100644 --- a/specification/wasm-latest/2.1-validation.types.spectec +++ b/specification/wasm-latest/2.1-validation.types.spectec @@ -265,6 +265,6 @@ rule Externtype_ok/table: -- Tabletype_ok: C |- tabletype : OK rule Externtype_ok/func: - C |- FUNC typeuse : OK + C |- FUNC exact typeuse : OK -- Typeuse_ok: C |- typeuse : OK -- Expand_use: typeuse ~~_C $($(FUNC t_1* -> t_2*)) diff --git a/specification/wasm-latest/2.2-validation.subtyping.spectec b/specification/wasm-latest/2.2-validation.subtyping.spectec index 9bd60602f..3c7fd4bf2 100644 --- a/specification/wasm-latest/2.2-validation.subtyping.spectec +++ b/specification/wasm-latest/2.2-validation.subtyping.spectec @@ -260,5 +260,5 @@ rule Externtype_sub/table: -- Tabletype_sub: C |- tabletype_1 <: tabletype_2 rule Externtype_sub/func: - C |- FUNC deftype_1 <: FUNC deftype_2 - -- Deftype_sub: C |- deftype_1 <: deftype_2 + C |- FUNC exact_1 deftype_1 <: FUNC exact_2 deftype_2 + -- Heaptype_sub: C |- $exactheaptype(exact_1, deftype_1) <: $exactheaptype(exact_2, deftype_2) diff --git a/specification/wasm-latest/2.3-validation.instructions.spectec b/specification/wasm-latest/2.3-validation.instructions.spectec index 2e042e76f..0da536a45 100644 --- a/specification/wasm-latest/2.3-validation.instructions.spectec +++ b/specification/wasm-latest/2.3-validation.instructions.spectec @@ -120,7 +120,8 @@ rule Instr_ok/br_on_cast_fail: rule Instr_ok/call: C |- CALL x : t_1* -> t_2* - -- Expand: C.FUNCS[x] ~~ FUNC t_1* -> t_2* + -- if C.FUNCS[x] = exact dt + -- Expand: dt ~~ FUNC t_1* -> t_2* rule Instr_ok/call_ref: C |- CALL_REF (_IDX x) : t_1* (REF NULL (_IDX x)) -> t_2* @@ -140,7 +141,8 @@ rule Instr_ok/return: ;; TODO(3, rossberg): enable t_2* <: C.RETURN rule Instr_ok/return_call: C |- RETURN_CALL x : t_3* t_1* -> t_4* - -- Expand: C.FUNCS[x] ~~ FUNC t_1* -> t_2* + -- if C.FUNCS[x] = exact dt + -- Expand: dt ~~ FUNC t_1* -> t_2* -- if C.RETURN = (t'_2*) -- Resulttype_sub: C |- t_2* <: t'_2* -- Instrtype_ok: C |- t_3* -> t_4* : OK @@ -210,8 +212,14 @@ rule Instr_ok/ref.null: -- Heaptype_ok: C |- ht : OK rule Instr_ok/ref.func: - C |- REF.FUNC x : eps -> (REF dt) - -- if C.FUNCS[x] = dt + C |- REF.FUNC x : eps -> (REF ht) + -- if C.FUNCS[x] = exact dt + -- if ht = $exactheaptype(exact, dt) + -- if x <- C.REFS + +rule Instr_ok/ref.func-exact: + C |- REF.FUNC x : eps -> (REF (EXACT dt)) + -- if C.FUNCS[x] = EXACT dt -- if x <- C.REFS rule Instr_ok/ref.i31: diff --git a/specification/wasm-latest/2.4-validation.modules.spectec b/specification/wasm-latest/2.4-validation.modules.spectec index a78814662..2d021afe2 100644 --- a/specification/wasm-latest/2.4-validation.modules.spectec +++ b/specification/wasm-latest/2.4-validation.modules.spectec @@ -90,7 +90,8 @@ rule Elemmode_ok/active: rule Start_ok: C |- START x : OK - -- Expand: C.FUNCS[x] ~~ FUNC eps -> eps + -- if C.FUNCS[x] = exact dt + -- Expand: dt ~~ FUNC eps -> eps ;; Im/exports @@ -125,8 +126,8 @@ rule Externidx_ok/table: -- if C.TABLES[x] = tt rule Externidx_ok/func: - C |- FUNC x : FUNC dt - -- if C.FUNCS[x] = dt + C |- FUNC x : FUNC exact dt + -- if C.FUNCS[x] = exact dt ;; Modules @@ -159,14 +160,15 @@ rule Module_ok: ---- -- if C = C' ++ {TAGS jt_I* jt*, GLOBALS gt*, MEMS mt_I* mt*, TABLES tt_I* tt*, DATAS ok*, ELEMS rt*} ---- - -- if C' = {TYPES dt'*, GLOBALS gt_I*, FUNCS dt_I* dt*, REFS x*} + -- if C' = {TYPES dt'*, GLOBALS gt_I*, FUNCS edt_I* edt*, REFS x*} + -- if edt* = (EXACT dt)* -- if x* = $funcidx_nonfuncs(global* mem* table* elem*) ---- -- if jt_I* = $tagsxt(xt_I*) -- if gt_I* = $globalsxt(xt_I*) -- if mt_I* = $memsxt(xt_I*) -- if tt_I* = $tablesxt(xt_I*) - -- if dt_I* = $funcsxt(xt_I*) + -- if edt_I* = $funcsxt(xt_I*) rule Types_ok/empty: diff --git a/specification/wasm-latest/4.1-execution.values.spectec b/specification/wasm-latest/4.1-execution.values.spectec index 1b38a0623..03cef8d5a 100644 --- a/specification/wasm-latest/4.1-execution.values.spectec +++ b/specification/wasm-latest/4.1-execution.values.spectec @@ -102,7 +102,7 @@ rule Externaddr_ok/table: -- if s.TABLES[a] = tableinst rule Externaddr_ok/func: - s |- FUNC a : FUNC funcinst.TYPE + s |- FUNC a : FUNC EXACT funcinst.TYPE -- if s.FUNCS[a] = funcinst rule Externaddr_ok/sub: diff --git a/specification/wasm-latest/5.2-binary.types.spectec b/specification/wasm-latest/5.2-binary.types.spectec index 743ff8785..c44cdb5b6 100644 --- a/specification/wasm-latest/5.2-binary.types.spectec +++ b/specification/wasm-latest/5.2-binary.types.spectec @@ -100,7 +100,8 @@ grammar Btabletype : tabletype = grammar Bexterntype : externtype = - | 0x00 x:Btypeidx => FUNC (_IDX x) + | 0x00 x:Btypeidx => FUNC INEXACT (_IDX x) + | 0x20 x:Btypeidx => FUNC EXACT (_IDX x) | 0x01 tt:Btabletype => TABLE tt | 0x02 mt:Bmemtype => MEM mt | 0x03 gt:Bglobaltype => GLOBAL gt diff --git a/specification/wasm-latest/6.2-text.types.spectec b/specification/wasm-latest/6.2-text.types.spectec index 2afedafc9..ee285b8fa 100644 --- a/specification/wasm-latest/6.2-text.types.spectec +++ b/specification/wasm-latest/6.2-text.types.spectec @@ -152,7 +152,8 @@ grammar Texterntype_(I) : (externtype, idctxt) = | "(" "global" id?:Tid? gt:Tglobaltype_(I) ")" => (GLOBAL gt, {GLOBALS (id?)}) | "(" "memory" id?:Tid? mt:Tmemtype_(I) ")" => (MEM mt, {MEMS (id?)}) | "(" "table" id?:Tid? tt:Ttabletype_(I) ")" => (TABLE tt, {TABLES (id?)}) - | "(" "func" id?:Tid? (x,I'):Ttypeuse_(I) ")" => (FUNC $($(_IDX x)), {FUNCS (id?)}) + | "(" "func" id?:Tid? (x,I'):Ttypeuse_(I) ")" => (FUNC INEXACT $($(_IDX x)), {FUNCS (id?)}) + | "(" "func" id?:Tid? "(" "exact" (x,I'):Ttypeuse_(I) ")" ")" => (FUNC EXACT $($(_IDX x)), {FUNCS (id?)}) ;; Type uses From ca049ee91d58f8eb202fb51b51169f0288390cef Mon Sep 17 00:00:00 2001 From: Thomas Lively Date: Wed, 8 Jul 2026 19:07:55 -0700 Subject: [PATCH 2/3] cleanup old Instr_ok/ref.func-exact --- .../wasm-latest/2.3-validation.instructions.spectec | 5 ----- 1 file changed, 5 deletions(-) diff --git a/specification/wasm-latest/2.3-validation.instructions.spectec b/specification/wasm-latest/2.3-validation.instructions.spectec index 0da536a45..a41160bf6 100644 --- a/specification/wasm-latest/2.3-validation.instructions.spectec +++ b/specification/wasm-latest/2.3-validation.instructions.spectec @@ -217,11 +217,6 @@ rule Instr_ok/ref.func: -- if ht = $exactheaptype(exact, dt) -- if x <- C.REFS -rule Instr_ok/ref.func-exact: - C |- REF.FUNC x : eps -> (REF (EXACT dt)) - -- if C.FUNCS[x] = EXACT dt - -- if x <- C.REFS - rule Instr_ok/ref.i31: C |- REF.I31 : I32 -> (REF I31) From e4fd1bd622ab5cec1273f0265d43318e5e741489 Mon Sep 17 00:00:00 2001 From: Thomas Lively Date: Tue, 14 Jul 2026 03:25:46 -0700 Subject: [PATCH 3/3] update tests --- spectec/test-frontend/TEST.md | 280 +++++++++++++++++----------------- 1 file changed, 144 insertions(+), 136 deletions(-) diff --git a/spectec/test-frontend/TEST.md b/spectec/test-frontend/TEST.md index 24fe9b19c..d24c3f457 100644 --- a/spectec/test-frontend/TEST.md +++ b/spectec/test-frontend/TEST.md @@ -849,7 +849,7 @@ syntax externtype = | GLOBAL{globaltype : globaltype}(globaltype : globaltype) | MEM{memtype : memtype}(memtype : memtype) | TABLE{tabletype : tabletype}(tabletype : tabletype) - | FUNC{typeuse : typeuse}(typeuse : typeuse) + | FUNC{heaptype : heaptype}(heaptype : heaptype) ;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec syntax moduletype = @@ -1123,11 +1123,11 @@ def $tablesxt(externtype*) : tabletype* rec { ;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:320.1-320.88 -def $funcsxt(externtype*) : deftype* +def $funcsxt(externtype*) : heaptype* ;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:338.1-338.24 def $funcsxt([]) = [] ;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:339.1-339.47 - def $funcsxt{dt : deftype, `xt*` : externtype*}([FUNC_externtype((dt : deftype <: typeuse))] ++ xt*{xt <- `xt*`}) = [dt] ++ $funcsxt(xt*{xt <- `xt*`}) + def $funcsxt{ht : heaptype, `xt*` : externtype*}([FUNC_externtype(ht)] ++ xt*{xt <- `xt*`}) = [ht] ++ $funcsxt(xt*{xt <- `xt*`}) ;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:340.1-340.59 def $funcsxt{externtype : externtype, `xt*` : externtype*}([externtype] ++ xt*{xt <- `xt*`}) = $funcsxt(xt*{xt <- `xt*`}) -- otherwise @@ -1302,7 +1302,7 @@ def $subst_externtype(externtype : externtype, typevar*, typeuse*) : externtype ;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec def $subst_externtype{mt : memtype, `tv*` : typevar*, `tu*` : typeuse*}(MEM_externtype(mt), tv*{tv <- `tv*`}, tu*{tu <- `tu*`}) = MEM_externtype($subst_memtype(mt, tv*{tv <- `tv*`}, tu*{tu <- `tu*`})) ;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec - def $subst_externtype{dt : deftype, `tv*` : typevar*, `tu*` : typeuse*}(FUNC_externtype((dt : deftype <: typeuse)), tv*{tv <- `tv*`}, tu*{tu <- `tu*`}) = FUNC_externtype(($subst_deftype(dt, tv*{tv <- `tv*`}, tu*{tu <- `tu*`}) : deftype <: typeuse)) + def $subst_externtype{ht : heaptype, `tv*` : typevar*, `tu*` : typeuse*}(FUNC_externtype(ht), tv*{tv <- `tv*`}, tu*{tu <- `tu*`}) = FUNC_externtype($subst_heaptype(ht, tv*{tv <- `tv*`}, tu*{tu <- `tu*`})) ;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec def $subst_moduletype(moduletype : moduletype, typevar*, typeuse*) : moduletype @@ -1578,7 +1578,7 @@ def $free_externtype(externtype : externtype) : free ;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec def $free_externtype{tabletype : tabletype}(TABLE_externtype(tabletype)) = $free_tabletype(tabletype) ;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec - def $free_externtype{typeuse : typeuse}(FUNC_externtype(typeuse)) = $free_typeuse(typeuse) + def $free_externtype{heaptype : heaptype}(FUNC_externtype(heaptype)) = $free_heaptype(heaptype) ;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec def $free_moduletype(moduletype : moduletype) : free @@ -2672,7 +2672,7 @@ syntax context = GLOBALS{`globaltype*` : globaltype*} globaltype*, MEMS{`memtype*` : memtype*} memtype*, TABLES{`tabletype*` : tabletype*} tabletype*, - FUNCS{`deftype*` : deftype*} deftype*, + FUNCS{`heaptype*` : heaptype*} heaptype*, DATAS{`datatype*` : datatype*} datatype*, ELEMS{`elemtype*` : elemtype*} elemtype*, LOCALS{`localtype*` : localtype*} localtype*, @@ -3263,8 +3263,8 @@ relation Externtype_ok: `%|-%:OK`(context, externtype) -- Tabletype_ok: `%|-%:OK`(C, tabletype) ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec - rule func{C : context, typeuse : typeuse, `t_1*` : valtype*, `t_2*` : valtype*}: - `%|-%:OK`(C, FUNC_externtype(typeuse)) + rule func{C : context, `exact?` : exact?, typeuse : typeuse, `t_1*` : valtype*, `t_2*` : valtype*}: + `%|-%:OK`(C, FUNC_externtype(_HT_heaptype(exact?{exact <- `exact?`}, typeuse))) -- Typeuse_ok: `%|-%:OK`(C, typeuse) -- Expand_use: `%~~_%%`(typeuse, C, `FUNC%->%`_comptype(`%`_resulttype(t_1*{t_1 <- `t_1*`}), `%`_resulttype(t_2*{t_2 <- `t_2*`}))) @@ -3351,9 +3351,9 @@ relation Externtype_sub: `%|-%<:%`(context, externtype, externtype) -- Tabletype_sub: `%|-%<:%`(C, tabletype_1, tabletype_2) ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec - rule func{C : context, deftype_1 : deftype, deftype_2 : deftype}: - `%|-%<:%`(C, FUNC_externtype((deftype_1 : deftype <: typeuse)), FUNC_externtype((deftype_2 : deftype <: typeuse))) - -- Deftype_sub: `%|-%<:%`(C, deftype_1, deftype_2) + rule func{C : context, heaptype_1 : heaptype, heaptype_2 : heaptype}: + `%|-%<:%`(C, FUNC_externtype(heaptype_1), FUNC_externtype(heaptype_2)) + -- Heaptype_sub: `%|-%<:%`(C, heaptype_1, heaptype_2) ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec relation Blocktype_ok: `%|-%:%`(context, blocktype, instrtype) @@ -3525,38 +3525,40 @@ relation Instr_ok: `%|-%:%`(context, instr, instrtype) -- Reftype_sub: `%|-%<:%`(C, rt_2, rt_3) -- Reftype_sub: `%|-%<:%`(C, $diffrt(rt_1, rt_2), rt) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:121.1-123.45 - rule call{C : context, x : idx, `t_1*` : valtype*, `t_2*` : valtype*}: + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:121.1-124.37 + rule call{C : context, x : idx, `t_1*` : valtype*, `t_2*` : valtype*, `exact?` : exact?, dt : deftype}: `%|-%:%`(C, CALL_instr(x), `%->_%%`_instrtype(`%`_resulttype(t_1*{t_1 <- `t_1*`}), [], `%`_resulttype(t_2*{t_2 <- `t_2*`}))) - -- Expand: `%~~%`(C.FUNCS_context[x!`%`_idx.0], `FUNC%->%`_comptype(`%`_resulttype(t_1*{t_1 <- `t_1*`}), `%`_resulttype(t_2*{t_2 <- `t_2*`}))) + -- if (C.FUNCS_context[x!`%`_idx.0] = _HT_heaptype(exact?{exact <- `exact?`}, (dt : deftype <: typeuse))) + -- Expand: `%~~%`(dt, `FUNC%->%`_comptype(`%`_resulttype(t_1*{t_1 <- `t_1*`}), `%`_resulttype(t_2*{t_2 <- `t_2*`}))) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:125.1-127.45 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:126.1-128.45 rule call_ref{C : context, x : idx, `t_1*` : valtype*, `t_2*` : valtype*}: `%|-%:%`(C, CALL_REF_instr(_IDX_typeuse(x)), `%->_%%`_instrtype(`%`_resulttype(t_1*{t_1 <- `t_1*`} ++ [REF_valtype(?(NULL_null), _HT_heaptype(?(), _IDX_typeuse(x)))]), [], `%`_resulttype(t_2*{t_2 <- `t_2*`}))) -- Expand: `%~~%`(C.TYPES_context[x!`%`_idx.0], `FUNC%->%`_comptype(`%`_resulttype(t_1*{t_1 <- `t_1*`}), `%`_resulttype(t_2*{t_2 <- `t_2*`}))) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:129.1-133.45 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:130.1-134.45 rule call_indirect{C : context, x : idx, y : idx, `t_1*` : valtype*, at : addrtype, `t_2*` : valtype*, lim : limits, rt : reftype}: `%|-%:%`(C, CALL_INDIRECT_instr(x, _IDX_typeuse(y)), `%->_%%`_instrtype(`%`_resulttype(t_1*{t_1 <- `t_1*`} ++ [(at : addrtype <: valtype)]), [], `%`_resulttype(t_2*{t_2 <- `t_2*`}))) -- if (C.TABLES_context[x!`%`_idx.0] = `%%%`_tabletype(at, lim, rt)) -- Reftype_sub: `%|-%<:%`(C, rt, REF_reftype(?(NULL_null), FUNC_heaptype)) -- Expand: `%~~%`(C.TYPES_context[y!`%`_idx.0], `FUNC%->%`_comptype(`%`_resulttype(t_1*{t_1 <- `t_1*`}), `%`_resulttype(t_2*{t_2 <- `t_2*`}))) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:135.1-138.42 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:136.1-139.42 rule return{C : context, `t_1*` : valtype*, `t*` : valtype*, `t_2*` : valtype*}: `%|-%:%`(C, RETURN_instr, `%->_%%`_instrtype(`%`_resulttype(t_1*{t_1 <- `t_1*`} ++ t*{t <- `t*`}), [], `%`_resulttype(t_2*{t_2 <- `t_2*`}))) -- if (C.RETURN_context = ?(`%`_resulttype(t*{t <- `t*`}))) -- Instrtype_ok: `%|-%:OK`(C, `%->_%%`_instrtype(`%`_resulttype(t_1*{t_1 <- `t_1*`}), [], `%`_resulttype(t_2*{t_2 <- `t_2*`}))) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:141.1-146.42 - rule return_call{C : context, x : idx, `t_3*` : valtype*, `t_1*` : valtype*, `t_4*` : valtype*, `t_2*` : valtype*, `t'_2*` : valtype*}: + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:142.1-148.42 + rule return_call{C : context, x : idx, `t_3*` : valtype*, `t_1*` : valtype*, `t_4*` : valtype*, `exact?` : exact?, dt : deftype, `t_2*` : valtype*, `t'_2*` : valtype*}: `%|-%:%`(C, RETURN_CALL_instr(x), `%->_%%`_instrtype(`%`_resulttype(t_3*{t_3 <- `t_3*`} ++ t_1*{t_1 <- `t_1*`}), [], `%`_resulttype(t_4*{t_4 <- `t_4*`}))) - -- Expand: `%~~%`(C.FUNCS_context[x!`%`_idx.0], `FUNC%->%`_comptype(`%`_resulttype(t_1*{t_1 <- `t_1*`}), `%`_resulttype(t_2*{t_2 <- `t_2*`}))) + -- if (C.FUNCS_context[x!`%`_idx.0] = _HT_heaptype(exact?{exact <- `exact?`}, (dt : deftype <: typeuse))) + -- Expand: `%~~%`(dt, `FUNC%->%`_comptype(`%`_resulttype(t_1*{t_1 <- `t_1*`}), `%`_resulttype(t_2*{t_2 <- `t_2*`}))) -- if (C.RETURN_context = ?(`%`_resulttype(t'_2*{t'_2 <- `t'_2*`}))) -- Resulttype_sub: `%|-%<:%`(C, `%`_resulttype(t_2*{t_2 <- `t_2*`}), `%`_resulttype(t'_2*{t'_2 <- `t'_2*`})) -- Instrtype_ok: `%|-%:OK`(C, `%->_%%`_instrtype(`%`_resulttype(t_3*{t_3 <- `t_3*`}), [], `%`_resulttype(t_4*{t_4 <- `t_4*`}))) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:149.1-154.42 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:151.1-156.42 rule return_call_ref{C : context, x : idx, `t_3*` : valtype*, `t_1*` : valtype*, `t_4*` : valtype*, `t_2*` : valtype*, `t'_2*` : valtype*}: `%|-%:%`(C, RETURN_CALL_REF_instr(_IDX_typeuse(x)), `%->_%%`_instrtype(`%`_resulttype(t_3*{t_3 <- `t_3*`} ++ t_1*{t_1 <- `t_1*`} ++ [REF_valtype(?(NULL_null), _HT_heaptype(?(), _IDX_typeuse(x)))]), [], `%`_resulttype(t_4*{t_4 <- `t_4*`}))) -- Expand: `%~~%`(C.TYPES_context[x!`%`_idx.0], `FUNC%->%`_comptype(`%`_resulttype(t_1*{t_1 <- `t_1*`}), `%`_resulttype(t_2*{t_2 <- `t_2*`}))) @@ -3564,7 +3566,7 @@ relation Instr_ok: `%|-%:%`(context, instr, instrtype) -- Resulttype_sub: `%|-%<:%`(C, `%`_resulttype(t_2*{t_2 <- `t_2*`}), `%`_resulttype(t'_2*{t'_2 <- `t'_2*`})) -- Instrtype_ok: `%|-%:OK`(C, `%->_%%`_instrtype(`%`_resulttype(t_3*{t_3 <- `t_3*`}), [], `%`_resulttype(t_4*{t_4 <- `t_4*`}))) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:157.1-165.42 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:159.1-167.42 rule return_call_indirect{C : context, x : idx, y : idx, `t_3*` : valtype*, `t_1*` : valtype*, at : addrtype, `t_4*` : valtype*, lim : limits, rt : reftype, `t_2*` : valtype*, `t'_2*` : valtype*}: `%|-%:%`(C, RETURN_CALL_INDIRECT_instr(x, _IDX_typeuse(y)), `%->_%%`_instrtype(`%`_resulttype(t_3*{t_3 <- `t_3*`} ++ t_1*{t_1 <- `t_1*`} ++ [(at : addrtype <: valtype)]), [], `%`_resulttype(t_4*{t_4 <- `t_4*`}))) -- if (C.TABLES_context[x!`%`_idx.0] = `%%%`_tabletype(at, lim, rt)) @@ -3574,490 +3576,490 @@ relation Instr_ok: `%|-%:%`(context, instr, instrtype) -- Resulttype_sub: `%|-%<:%`(C, `%`_resulttype(t_2*{t_2 <- `t_2*`}), `%`_resulttype(t'_2*{t'_2 <- `t'_2*`})) -- Instrtype_ok: `%|-%:OK`(C, `%->_%%`_instrtype(`%`_resulttype(t_3*{t_3 <- `t_3*`}), [], `%`_resulttype(t_4*{t_4 <- `t_4*`}))) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:172.1-175.42 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:174.1-177.42 rule throw{C : context, x : idx, `t_1*` : valtype*, `t*` : valtype*, `t_2*` : valtype*}: `%|-%:%`(C, THROW_instr(x), `%->_%%`_instrtype(`%`_resulttype(t_1*{t_1 <- `t_1*`} ++ t*{t <- `t*`}), [], `%`_resulttype(t_2*{t_2 <- `t_2*`}))) -- Expand: `%~~%`($as_deftype(C.TAGS_context[x!`%`_idx.0]), `FUNC%->%`_comptype(`%`_resulttype(t*{t <- `t*`}), `%`_resulttype([]))) -- Instrtype_ok: `%|-%:OK`(C, `%->_%%`_instrtype(`%`_resulttype(t_1*{t_1 <- `t_1*`}), [], `%`_resulttype(t_2*{t_2 <- `t_2*`}))) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:177.1-179.42 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:179.1-181.42 rule throw_ref{C : context, `t_1*` : valtype*, `t_2*` : valtype*}: `%|-%:%`(C, THROW_REF_instr, `%->_%%`_instrtype(`%`_resulttype(t_1*{t_1 <- `t_1*`} ++ [REF_valtype(?(NULL_null), EXN_heaptype)]), [], `%`_resulttype(t_2*{t_2 <- `t_2*`}))) -- Instrtype_ok: `%|-%:OK`(C, `%->_%%`_instrtype(`%`_resulttype(t_1*{t_1 <- `t_1*`}), [], `%`_resulttype(t_2*{t_2 <- `t_2*`}))) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:181.1-185.34 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:183.1-187.34 rule try_table{C : context, bt : blocktype, `catch*` : catch*, `instr*` : instr*, `t_1*` : valtype*, `t_2*` : valtype*, `x*` : idx*}: `%|-%:%`(C, TRY_TABLE_instr(bt, `%`_list(catch*{catch <- `catch*`}), instr*{instr <- `instr*`}), `%->_%%`_instrtype(`%`_resulttype(t_1*{t_1 <- `t_1*`}), [], `%`_resulttype(t_2*{t_2 <- `t_2*`}))) -- Blocktype_ok: `%|-%:%`(C, bt, `%->_%%`_instrtype(`%`_resulttype(t_1*{t_1 <- `t_1*`}), [], `%`_resulttype(t_2*{t_2 <- `t_2*`}))) -- Instrs_ok: `%|-%:%`({TYPES [], RECS [], TAGS [], GLOBALS [], MEMS [], TABLES [], FUNCS [], DATAS [], ELEMS [], LOCALS [], LABELS [`%`_resulttype(t_2*{t_2 <- `t_2*`})], RETURN ?(), REFS []} +++ C, instr*{instr <- `instr*`}, `%->_%%`_instrtype(`%`_resulttype(t_1*{t_1 <- `t_1*`}), x*{x <- `x*`}, `%`_resulttype(t_2*{t_2 <- `t_2*`}))) -- (Catch_ok: `%|-%:OK`(C, catch))*{catch <- `catch*`} - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:208.1-210.31 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:210.1-212.31 rule ref.null{C : context, ht : heaptype}: `%|-%:%`(C, REF.NULL_instr(ht), `%->_%%`_instrtype(`%`_resulttype([]), [], `%`_resulttype([REF_valtype(?(NULL_null), ht)]))) -- Heaptype_ok: `%|-%:OK`(C, ht) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:212.1-215.20 - rule ref.func{C : context, x : idx, dt : deftype}: - `%|-%:%`(C, REF.FUNC_instr(x), `%->_%%`_instrtype(`%`_resulttype([]), [], `%`_resulttype([REF_valtype(?(), _HT_heaptype(?(), (dt : deftype <: typeuse)))]))) - -- if (C.FUNCS_context[x!`%`_idx.0] = dt) + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:214.1-217.20 + rule ref.func{C : context, x : idx, ht : heaptype}: + `%|-%:%`(C, REF.FUNC_instr(x), `%->_%%`_instrtype(`%`_resulttype([]), [], `%`_resulttype([REF_valtype(?(), ht)]))) + -- if (C.FUNCS_context[x!`%`_idx.0] = ht) -- if (x <- C.REFS_context) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:217.1-218.34 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:219.1-220.34 rule ref.i31{C : context}: `%|-%:%`(C, REF.I31_instr, `%->_%%`_instrtype(`%`_resulttype([I32_valtype]), [], `%`_resulttype([REF_valtype(?(), I31_heaptype)]))) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:220.1-222.31 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:222.1-224.31 rule ref.is_null{C : context, ht : heaptype}: `%|-%:%`(C, REF.IS_NULL_instr, `%->_%%`_instrtype(`%`_resulttype([REF_valtype(?(NULL_null), ht)]), [], `%`_resulttype([I32_valtype]))) -- Heaptype_ok: `%|-%:OK`(C, ht) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:224.1-226.31 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:226.1-228.31 rule ref.as_non_null{C : context, ht : heaptype}: `%|-%:%`(C, REF.AS_NON_NULL_instr, `%->_%%`_instrtype(`%`_resulttype([REF_valtype(?(NULL_null), ht)]), [], `%`_resulttype([REF_valtype(?(), ht)]))) -- Heaptype_ok: `%|-%:OK`(C, ht) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:228.1-229.51 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:230.1-231.51 rule ref.eq{C : context}: `%|-%:%`(C, REF.EQ_instr, `%->_%%`_instrtype(`%`_resulttype([REF_valtype(?(NULL_null), EQ_heaptype) REF_valtype(?(NULL_null), EQ_heaptype)]), [], `%`_resulttype([I32_valtype]))) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:231.1-235.33 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:233.1-237.33 rule ref.test{C : context, rt : reftype, rt' : reftype}: `%|-%:%`(C, REF.TEST_instr(rt), `%->_%%`_instrtype(`%`_resulttype([(rt' : reftype <: valtype)]), [], `%`_resulttype([I32_valtype]))) -- Reftype_ok: `%|-%:OK`(C, rt) -- Reftype_ok: `%|-%:OK`(C, rt') -- Reftype_sub: `%|-%<:%`(C, rt, rt') - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:237.1-241.33 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:239.1-243.33 rule ref.cast{C : context, rt : reftype, rt' : reftype}: `%|-%:%`(C, REF.CAST_instr(rt), `%->_%%`_instrtype(`%`_resulttype([(rt' : reftype <: valtype)]), [], `%`_resulttype([(rt : reftype <: valtype)]))) -- Reftype_ok: `%|-%:OK`(C, rt) -- Reftype_ok: `%|-%:OK`(C, rt') -- Reftype_sub: `%|-%<:%`(C, rt, rt') - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:246.1-247.42 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:248.1-249.42 rule i31.get{C : context, sx : sx}: `%|-%:%`(C, I31.GET_instr(sx), `%->_%%`_instrtype(`%`_resulttype([REF_valtype(?(NULL_null), I31_heaptype)]), [], `%`_resulttype([I32_valtype]))) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:252.1-254.68 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:254.1-256.68 rule struct.new{C : context, x : idx, `zt*` : storagetype*, `describestype?` : describestype?, `mut?*` : mut?*}: `%|-%:%`(C, STRUCT.NEW_instr(x), `%->_%%`_instrtype(`%`_resulttype($unpack(zt)*{zt <- `zt*`}), [], `%`_resulttype([REF_valtype(?(), _HT_heaptype(?(), _IDX_typeuse(x)))]))) -- ExpandDesc: `%~~%`(C.TYPES_context[x!`%`_idx.0], `%%%`_desctype(describestype?{describestype <- `describestype?`}, ?(), STRUCT_comptype(`%`_list(`%%`_fieldtype(mut?{mut <- `mut?`}, zt)*{`mut?` <- `mut?*`, zt <- `zt*`})))) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:256.1-259.48 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:258.1-261.48 rule struct.new_default{C : context, x : idx, `describestype?` : describestype?, `mut?*` : mut?*, `zt*` : storagetype*}: `%|-%:%`(C, STRUCT.NEW_DEFAULT_instr(x), `%->_%%`_instrtype(`%`_resulttype([]), [], `%`_resulttype([REF_valtype(?(), _HT_heaptype(?(), _IDX_typeuse(x)))]))) -- ExpandDesc: `%~~%`(C.TYPES_context[x!`%`_idx.0], `%%%`_desctype(describestype?{describestype <- `describestype?`}, ?(), STRUCT_comptype(`%`_list(`%%`_fieldtype(mut?{mut <- `mut?`}, zt)*{`mut?` <- `mut?*`, zt <- `zt*`})))) -- (Defaultable: `|-%DEFAULTABLE`($unpack(zt)))*{zt <- `zt*`} - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:261.1-263.88 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:263.1-265.88 rule struct.new_desc{C : context, x : idx, `zt*` : storagetype*, y : idx, `describestype?` : describestype?, `mut?*` : mut?*}: `%|-%:%`(C, STRUCT.NEW_DESC_instr(x), `%->_%%`_instrtype(`%`_resulttype($unpack(zt)*{zt <- `zt*`} ++ [REF_valtype(?(NULL_null), _HT_heaptype(?(EXACT_exact), _IDX_typeuse(y)))]), [], `%`_resulttype([REF_valtype(?(), _HT_heaptype(?(EXACT_exact), _IDX_typeuse(x)))]))) -- ExpandDesc: `%~~%`(C.TYPES_context[x!`%`_idx.0], `%%%`_desctype(describestype?{describestype <- `describestype?`}, ?(DESCRIPTOR_descriptortype(_IDX_typeuse(y))), STRUCT_comptype(`%`_list(`%%`_fieldtype(mut?{mut <- `mut?`}, zt)*{`mut?` <- `mut?*`, zt <- `zt*`})))) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:265.1-268.48 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:267.1-270.48 rule struct.new_default_desc{C : context, x : idx, y : idx, `describestype?` : describestype?, `mut?*` : mut?*, `zt*` : storagetype*}: `%|-%:%`(C, STRUCT.NEW_DEFAULT_DESC_instr(x), `%->_%%`_instrtype(`%`_resulttype([REF_valtype(?(NULL_null), _HT_heaptype(?(EXACT_exact), _IDX_typeuse(y)))]), [], `%`_resulttype([REF_valtype(?(), _HT_heaptype(?(EXACT_exact), _IDX_typeuse(x)))]))) -- ExpandDesc: `%~~%`(C.TYPES_context[x!`%`_idx.0], `%%%`_desctype(describestype?{describestype <- `describestype?`}, ?(DESCRIPTOR_descriptortype(_IDX_typeuse(y))), STRUCT_comptype(`%`_list(`%%`_fieldtype(mut?{mut <- `mut?`}, zt)*{`mut?` <- `mut?*`, zt <- `zt*`})))) -- (Defaultable: `|-%DEFAULTABLE`($unpack(zt)))*{zt <- `zt*`} - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:273.1-277.41 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:275.1-279.41 rule struct.get{C : context, `sx?` : sx?, x : idx, i : u32, zt : storagetype, `ft*` : fieldtype*, `mut?` : mut?}: `%|-%:%`(C, STRUCT.GET_instr(sx?{sx <- `sx?`}, x, i), `%->_%%`_instrtype(`%`_resulttype([REF_valtype(?(NULL_null), _HT_heaptype(?(), _IDX_typeuse(x)))]), [], `%`_resulttype([$unpack(zt)]))) -- Expand: `%~~%`(C.TYPES_context[x!`%`_idx.0], STRUCT_comptype(`%`_list(ft*{ft <- `ft*`}))) -- if (ft*{ft <- `ft*`}[i!`%`_u32.0] = `%%`_fieldtype(mut?{mut <- `mut?`}, zt)) -- if ((sx?{sx <- `sx?`} =/= ?()) <=> $is_packtype(zt)) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:279.1-282.24 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:281.1-284.24 rule struct.set{C : context, x : idx, i : u32, zt : storagetype, `ft*` : fieldtype*}: `%|-%:%`(C, STRUCT.SET_instr(x, i), `%->_%%`_instrtype(`%`_resulttype([REF_valtype(?(NULL_null), _HT_heaptype(?(), _IDX_typeuse(x))) $unpack(zt)]), [], `%`_resulttype([]))) -- Expand: `%~~%`(C.TYPES_context[x!`%`_idx.0], STRUCT_comptype(`%`_list(ft*{ft <- `ft*`}))) -- if (ft*{ft <- `ft*`}[i!`%`_u32.0] = `%%`_fieldtype(?(MUT_mut), zt)) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:287.1-289.43 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:289.1-291.43 rule array.new{C : context, x : idx, zt : storagetype, `mut?` : mut?}: `%|-%:%`(C, ARRAY.NEW_instr(x), `%->_%%`_instrtype(`%`_resulttype([$unpack(zt) I32_valtype]), [], `%`_resulttype([REF_valtype(?(), _HT_heaptype(?(), _IDX_typeuse(x)))]))) -- Expand: `%~~%`(C.TYPES_context[x!`%`_idx.0], ARRAY_comptype(`%%`_fieldtype(mut?{mut <- `mut?`}, zt))) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:291.1-294.45 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:293.1-296.45 rule array.new_default{C : context, x : idx, `mut?` : mut?, zt : storagetype}: `%|-%:%`(C, ARRAY.NEW_DEFAULT_instr(x), `%->_%%`_instrtype(`%`_resulttype([I32_valtype]), [], `%`_resulttype([REF_valtype(?(), _HT_heaptype(?(), _IDX_typeuse(x)))]))) -- Expand: `%~~%`(C.TYPES_context[x!`%`_idx.0], ARRAY_comptype(`%%`_fieldtype(mut?{mut <- `mut?`}, zt))) -- Defaultable: `|-%DEFAULTABLE`($unpack(zt)) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:296.1-298.43 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:298.1-300.43 rule array.new_fixed{C : context, x : idx, n : n, zt : storagetype, `mut?` : mut?}: `%|-%:%`(C, ARRAY.NEW_FIXED_instr(x, `%`_u32(n)), `%->_%%`_instrtype(`%`_resulttype($unpack(zt)^n{}), [], `%`_resulttype([REF_valtype(?(), _HT_heaptype(?(), _IDX_typeuse(x)))]))) -- Expand: `%~~%`(C.TYPES_context[x!`%`_idx.0], ARRAY_comptype(`%%`_fieldtype(mut?{mut <- `mut?`}, zt))) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:300.1-303.40 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:302.1-305.40 rule array.new_elem{C : context, x : idx, y : idx, `mut?` : mut?, rt : reftype}: `%|-%:%`(C, ARRAY.NEW_ELEM_instr(x, y), `%->_%%`_instrtype(`%`_resulttype([I32_valtype I32_valtype]), [], `%`_resulttype([REF_valtype(?(), _HT_heaptype(?(), _IDX_typeuse(x)))]))) -- Expand: `%~~%`(C.TYPES_context[x!`%`_idx.0], ARRAY_comptype(`%%`_fieldtype(mut?{mut <- `mut?`}, (rt : reftype <: storagetype)))) -- Reftype_sub: `%|-%<:%`(C, C.ELEMS_context[y!`%`_idx.0], rt) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:305.1-309.24 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:307.1-311.24 rule array.new_data{C : context, x : idx, y : idx, `mut?` : mut?, zt : storagetype, numtype : numtype, vectype : vectype}: `%|-%:%`(C, ARRAY.NEW_DATA_instr(x, y), `%->_%%`_instrtype(`%`_resulttype([I32_valtype I32_valtype]), [], `%`_resulttype([REF_valtype(?(), _HT_heaptype(?(), _IDX_typeuse(x)))]))) -- Expand: `%~~%`(C.TYPES_context[x!`%`_idx.0], ARRAY_comptype(`%%`_fieldtype(mut?{mut <- `mut?`}, zt))) -- if (($unpack(zt) = (numtype : numtype <: valtype)) \/ ($unpack(zt) = (vectype : vectype <: valtype))) -- if (C.DATAS_context[y!`%`_idx.0] = OK_datatype) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:311.1-314.39 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:313.1-316.39 rule array.get{C : context, `sx?` : sx?, x : idx, zt : storagetype, `mut?` : mut?}: `%|-%:%`(C, ARRAY.GET_instr(sx?{sx <- `sx?`}, x), `%->_%%`_instrtype(`%`_resulttype([REF_valtype(?(NULL_null), _HT_heaptype(?(), _IDX_typeuse(x))) I32_valtype]), [], `%`_resulttype([$unpack(zt)]))) -- Expand: `%~~%`(C.TYPES_context[x!`%`_idx.0], ARRAY_comptype(`%%`_fieldtype(mut?{mut <- `mut?`}, zt))) -- if ((sx?{sx <- `sx?`} = ?()) <=> $is_packtype(zt)) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:316.1-318.42 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:318.1-320.42 rule array.set{C : context, x : idx, zt : storagetype}: `%|-%:%`(C, ARRAY.SET_instr(x), `%->_%%`_instrtype(`%`_resulttype([REF_valtype(?(NULL_null), _HT_heaptype(?(), _IDX_typeuse(x))) I32_valtype $unpack(zt)]), [], `%`_resulttype([]))) -- Expand: `%~~%`(C.TYPES_context[x!`%`_idx.0], ARRAY_comptype(`%%`_fieldtype(?(MUT_mut), zt))) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:320.1-321.43 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:322.1-323.43 rule array.len{C : context}: `%|-%:%`(C, ARRAY.LEN_instr, `%->_%%`_instrtype(`%`_resulttype([REF_valtype(?(NULL_null), ARRAY_heaptype)]), [], `%`_resulttype([I32_valtype]))) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:323.1-325.42 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:325.1-327.42 rule array.fill{C : context, x : idx, zt : storagetype}: `%|-%:%`(C, ARRAY.FILL_instr(x), `%->_%%`_instrtype(`%`_resulttype([REF_valtype(?(NULL_null), _HT_heaptype(?(), _IDX_typeuse(x))) I32_valtype $unpack(zt) I32_valtype]), [], `%`_resulttype([]))) -- Expand: `%~~%`(C.TYPES_context[x!`%`_idx.0], ARRAY_comptype(`%%`_fieldtype(?(MUT_mut), zt))) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:327.1-331.40 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:329.1-333.40 rule array.copy{C : context, x_1 : idx, x_2 : idx, zt_1 : storagetype, `mut?` : mut?, zt_2 : storagetype}: `%|-%:%`(C, ARRAY.COPY_instr(x_1, x_2), `%->_%%`_instrtype(`%`_resulttype([REF_valtype(?(NULL_null), _HT_heaptype(?(), _IDX_typeuse(x_1))) I32_valtype REF_valtype(?(NULL_null), _HT_heaptype(?(), _IDX_typeuse(x_2))) I32_valtype I32_valtype]), [], `%`_resulttype([]))) -- Expand: `%~~%`(C.TYPES_context[x_1!`%`_idx.0], ARRAY_comptype(`%%`_fieldtype(?(MUT_mut), zt_1))) -- Expand: `%~~%`(C.TYPES_context[x_2!`%`_idx.0], ARRAY_comptype(`%%`_fieldtype(mut?{mut <- `mut?`}, zt_2))) -- Storagetype_sub: `%|-%<:%`(C, zt_2, zt_1) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:333.1-336.44 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:335.1-338.44 rule array.init_elem{C : context, x : idx, y : idx, zt : storagetype}: `%|-%:%`(C, ARRAY.INIT_ELEM_instr(x, y), `%->_%%`_instrtype(`%`_resulttype([REF_valtype(?(NULL_null), _HT_heaptype(?(), _IDX_typeuse(x))) I32_valtype I32_valtype I32_valtype]), [], `%`_resulttype([]))) -- Expand: `%~~%`(C.TYPES_context[x!`%`_idx.0], ARRAY_comptype(`%%`_fieldtype(?(MUT_mut), zt))) -- Storagetype_sub: `%|-%<:%`(C, (C.ELEMS_context[y!`%`_idx.0] : reftype <: storagetype), zt) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:338.1-342.24 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:340.1-344.24 rule array.init_data{C : context, x : idx, y : idx, zt : storagetype, numtype : numtype, vectype : vectype}: `%|-%:%`(C, ARRAY.INIT_DATA_instr(x, y), `%->_%%`_instrtype(`%`_resulttype([REF_valtype(?(NULL_null), _HT_heaptype(?(), _IDX_typeuse(x))) I32_valtype I32_valtype I32_valtype]), [], `%`_resulttype([]))) -- Expand: `%~~%`(C.TYPES_context[x!`%`_idx.0], ARRAY_comptype(`%%`_fieldtype(?(MUT_mut), zt))) -- if (($unpack(zt) = (numtype : numtype <: valtype)) \/ ($unpack(zt) = (vectype : vectype <: valtype))) -- if (C.DATAS_context[y!`%`_idx.0] = OK_datatype) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:347.1-349.26 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:349.1-351.26 rule extern.convert_any{C : context, `null_1?` : null?, `null_2?` : null?}: `%|-%:%`(C, EXTERN.CONVERT_ANY_instr, `%->_%%`_instrtype(`%`_resulttype([REF_valtype(null_1?{null_1 <- `null_1?`}, ANY_heaptype)]), [], `%`_resulttype([REF_valtype(null_2?{null_2 <- `null_2?`}, EXTERN_heaptype)]))) -- if (null_1?{null_1 <- `null_1?`} = null_2?{null_2 <- `null_2?`}) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:351.1-353.26 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:353.1-355.26 rule any.convert_extern{C : context, `null_1?` : null?, `null_2?` : null?}: `%|-%:%`(C, ANY.CONVERT_EXTERN_instr, `%->_%%`_instrtype(`%`_resulttype([REF_valtype(null_1?{null_1 <- `null_1?`}, EXTERN_heaptype)]), [], `%`_resulttype([REF_valtype(null_2?{null_2 <- `null_2?`}, ANY_heaptype)]))) -- if (null_1?{null_1 <- `null_1?`} = null_2?{null_2 <- `null_2?`}) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:358.1-360.28 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:360.1-362.28 rule local.get{C : context, x : idx, t : valtype}: `%|-%:%`(C, LOCAL.GET_instr(x), `%->_%%`_instrtype(`%`_resulttype([]), [], `%`_resulttype([t]))) -- if (C.LOCALS_context[x!`%`_idx.0] = `%%`_localtype(SET_init, t)) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:362.1-364.29 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:364.1-366.29 rule local.set{C : context, x : idx, t : valtype, init : init}: `%|-%:%`(C, LOCAL.SET_instr(x), `%->_%%`_instrtype(`%`_resulttype([t]), [x], `%`_resulttype([]))) -- if (C.LOCALS_context[x!`%`_idx.0] = `%%`_localtype(init, t)) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:366.1-368.29 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:368.1-370.29 rule local.tee{C : context, x : idx, t : valtype, init : init}: `%|-%:%`(C, LOCAL.TEE_instr(x), `%->_%%`_instrtype(`%`_resulttype([t]), [x], `%`_resulttype([t]))) -- if (C.LOCALS_context[x!`%`_idx.0] = `%%`_localtype(init, t)) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:373.1-375.30 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:375.1-377.30 rule global.get{C : context, x : idx, t : valtype, `mut?` : mut?}: `%|-%:%`(C, GLOBAL.GET_instr(x), `%->_%%`_instrtype(`%`_resulttype([]), [], `%`_resulttype([t]))) -- if (C.GLOBALS_context[x!`%`_idx.0] = `%%`_globaltype(mut?{mut <- `mut?`}, t)) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:377.1-379.29 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:379.1-381.29 rule global.set{C : context, x : idx, t : valtype}: `%|-%:%`(C, GLOBAL.SET_instr(x), `%->_%%`_instrtype(`%`_resulttype([t]), [], `%`_resulttype([]))) -- if (C.GLOBALS_context[x!`%`_idx.0] = `%%`_globaltype(?(MUT_mut), t)) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:384.1-386.32 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:386.1-388.32 rule table.get{C : context, x : idx, at : addrtype, rt : reftype, lim : limits}: `%|-%:%`(C, TABLE.GET_instr(x), `%->_%%`_instrtype(`%`_resulttype([(at : addrtype <: valtype)]), [], `%`_resulttype([(rt : reftype <: valtype)]))) -- if (C.TABLES_context[x!`%`_idx.0] = `%%%`_tabletype(at, lim, rt)) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:388.1-390.32 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:390.1-392.32 rule table.set{C : context, x : idx, at : addrtype, rt : reftype, lim : limits}: `%|-%:%`(C, TABLE.SET_instr(x), `%->_%%`_instrtype(`%`_resulttype([(at : addrtype <: valtype) (rt : reftype <: valtype)]), [], `%`_resulttype([]))) -- if (C.TABLES_context[x!`%`_idx.0] = `%%%`_tabletype(at, lim, rt)) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:392.1-394.32 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:394.1-396.32 rule table.size{C : context, x : idx, at : addrtype, lim : limits, rt : reftype}: `%|-%:%`(C, TABLE.SIZE_instr(x), `%->_%%`_instrtype(`%`_resulttype([]), [], `%`_resulttype([(at : addrtype <: valtype)]))) -- if (C.TABLES_context[x!`%`_idx.0] = `%%%`_tabletype(at, lim, rt)) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:396.1-398.32 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:398.1-400.32 rule table.grow{C : context, x : idx, rt : reftype, at : addrtype, lim : limits}: `%|-%:%`(C, TABLE.GROW_instr(x), `%->_%%`_instrtype(`%`_resulttype([(rt : reftype <: valtype) (at : addrtype <: valtype)]), [], `%`_resulttype([I32_valtype]))) -- if (C.TABLES_context[x!`%`_idx.0] = `%%%`_tabletype(at, lim, rt)) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:400.1-402.32 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:402.1-404.32 rule table.fill{C : context, x : idx, at : addrtype, rt : reftype, lim : limits}: `%|-%:%`(C, TABLE.FILL_instr(x), `%->_%%`_instrtype(`%`_resulttype([(at : addrtype <: valtype) (rt : reftype <: valtype) (at : addrtype <: valtype)]), [], `%`_resulttype([]))) -- if (C.TABLES_context[x!`%`_idx.0] = `%%%`_tabletype(at, lim, rt)) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:404.1-408.36 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:406.1-410.36 rule table.copy{C : context, x_1 : idx, x_2 : idx, at_1 : addrtype, at_2 : addrtype, lim_1 : limits, rt_1 : reftype, lim_2 : limits, rt_2 : reftype}: `%|-%:%`(C, TABLE.COPY_instr(x_1, x_2), `%->_%%`_instrtype(`%`_resulttype([(at_1 : addrtype <: valtype) (at_2 : addrtype <: valtype) ($minat(at_1, at_2) : addrtype <: valtype)]), [], `%`_resulttype([]))) -- if (C.TABLES_context[x_1!`%`_idx.0] = `%%%`_tabletype(at_1, lim_1, rt_1)) -- if (C.TABLES_context[x_2!`%`_idx.0] = `%%%`_tabletype(at_2, lim_2, rt_2)) -- Reftype_sub: `%|-%<:%`(C, rt_2, rt_1) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:410.1-414.36 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:412.1-416.36 rule table.init{C : context, x : idx, y : idx, at : addrtype, lim : limits, rt_1 : reftype, rt_2 : reftype}: `%|-%:%`(C, TABLE.INIT_instr(x, y), `%->_%%`_instrtype(`%`_resulttype([(at : addrtype <: valtype) I32_valtype I32_valtype]), [], `%`_resulttype([]))) -- if (C.TABLES_context[x!`%`_idx.0] = `%%%`_tabletype(at, lim, rt_1)) -- if (C.ELEMS_context[y!`%`_idx.0] = rt_2) -- Reftype_sub: `%|-%<:%`(C, rt_2, rt_1) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:416.1-418.24 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:418.1-420.24 rule elem.drop{C : context, x : idx, rt : reftype}: `%|-%:%`(C, ELEM.DROP_instr(x), `%->_%%`_instrtype(`%`_resulttype([]), [], `%`_resulttype([]))) -- if (C.ELEMS_context[x!`%`_idx.0] = rt) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:431.1-433.32 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:433.1-435.32 rule memory.size{C : context, x : idx, at : addrtype, lim : limits}: `%|-%:%`(C, MEMORY.SIZE_instr(x), `%->_%%`_instrtype(`%`_resulttype([]), [], `%`_resulttype([(at : addrtype <: valtype)]))) -- if (C.MEMS_context[x!`%`_idx.0] = `%%PAGE`_memtype(at, lim)) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:435.1-437.32 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:437.1-439.32 rule memory.grow{C : context, x : idx, at : addrtype, lim : limits}: `%|-%:%`(C, MEMORY.GROW_instr(x), `%->_%%`_instrtype(`%`_resulttype([(at : addrtype <: valtype)]), [], `%`_resulttype([(at : addrtype <: valtype)]))) -- if (C.MEMS_context[x!`%`_idx.0] = `%%PAGE`_memtype(at, lim)) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:439.1-441.32 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:441.1-443.32 rule memory.fill{C : context, x : idx, at : addrtype, lim : limits}: `%|-%:%`(C, MEMORY.FILL_instr(x), `%->_%%`_instrtype(`%`_resulttype([(at : addrtype <: valtype) I32_valtype (at : addrtype <: valtype)]), [], `%`_resulttype([]))) -- if (C.MEMS_context[x!`%`_idx.0] = `%%PAGE`_memtype(at, lim)) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:443.1-446.38 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:445.1-448.38 rule memory.copy{C : context, x_1 : idx, x_2 : idx, at_1 : addrtype, at_2 : addrtype, lim_1 : limits, lim_2 : limits}: `%|-%:%`(C, MEMORY.COPY_instr(x_1, x_2), `%->_%%`_instrtype(`%`_resulttype([(at_1 : addrtype <: valtype) (at_2 : addrtype <: valtype) ($minat(at_1, at_2) : addrtype <: valtype)]), [], `%`_resulttype([]))) -- if (C.MEMS_context[x_1!`%`_idx.0] = `%%PAGE`_memtype(at_1, lim_1)) -- if (C.MEMS_context[x_2!`%`_idx.0] = `%%PAGE`_memtype(at_2, lim_2)) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:448.1-451.24 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:450.1-453.24 rule memory.init{C : context, x : idx, y : idx, at : addrtype, lim : limits}: `%|-%:%`(C, MEMORY.INIT_instr(x, y), `%->_%%`_instrtype(`%`_resulttype([(at : addrtype <: valtype) I32_valtype I32_valtype]), [], `%`_resulttype([]))) -- if (C.MEMS_context[x!`%`_idx.0] = `%%PAGE`_memtype(at, lim)) -- if (C.DATAS_context[y!`%`_idx.0] = OK_datatype) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:453.1-455.24 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:455.1-457.24 rule data.drop{C : context, x : idx}: `%|-%:%`(C, DATA.DROP_instr(x), `%->_%%`_instrtype(`%`_resulttype([]), [], `%`_resulttype([]))) -- if (C.DATAS_context[x!`%`_idx.0] = OK_datatype) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:466.1-469.44 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:468.1-471.44 rule `load-val`{C : context, nt : numtype, x : idx, memarg : memarg, at : addrtype, lim : limits}: `%|-%:%`(C, LOAD_instr(nt, ?(), x, memarg), `%->_%%`_instrtype(`%`_resulttype([(at : addrtype <: valtype)]), [], `%`_resulttype([(nt : numtype <: valtype)]))) -- if (C.MEMS_context[x!`%`_idx.0] = `%%PAGE`_memtype(at, lim)) -- Memarg_ok: `|-%:%->%`(memarg, at, $size(nt)) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:471.1-474.36 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:473.1-476.36 rule `load-pack`{C : context, Inn : Inn, M : M, sx : sx, x : idx, memarg : memarg, at : addrtype, lim : limits}: `%|-%:%`(C, LOAD_instr((Inn : Inn <: numtype), ?(`%_%`_loadop_(`%`_sz(M), sx)), x, memarg), `%->_%%`_instrtype(`%`_resulttype([(at : addrtype <: valtype)]), [], `%`_resulttype([(Inn : Inn <: valtype)]))) -- if (C.MEMS_context[x!`%`_idx.0] = `%%PAGE`_memtype(at, lim)) -- Memarg_ok: `|-%:%->%`(memarg, at, M) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:485.1-488.44 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:487.1-490.44 rule `store-val`{C : context, nt : numtype, x : idx, memarg : memarg, at : addrtype, lim : limits}: `%|-%:%`(C, STORE_instr(nt, ?(), x, memarg), `%->_%%`_instrtype(`%`_resulttype([(at : addrtype <: valtype) (nt : numtype <: valtype)]), [], `%`_resulttype([]))) -- if (C.MEMS_context[x!`%`_idx.0] = `%%PAGE`_memtype(at, lim)) -- Memarg_ok: `|-%:%->%`(memarg, at, $size(nt)) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:490.1-493.36 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:492.1-495.36 rule `store-pack`{C : context, Inn : Inn, M : M, x : idx, memarg : memarg, at : addrtype, lim : limits}: `%|-%:%`(C, STORE_instr((Inn : Inn <: numtype), ?(`%`_storeop_(`%`_sz(M))), x, memarg), `%->_%%`_instrtype(`%`_resulttype([(at : addrtype <: valtype) (Inn : Inn <: valtype)]), [], `%`_resulttype([]))) -- if (C.MEMS_context[x!`%`_idx.0] = `%%PAGE`_memtype(at, lim)) -- Memarg_ok: `|-%:%->%`(memarg, at, M) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:495.1-498.47 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:497.1-500.47 rule `vload-val`{C : context, x : idx, memarg : memarg, at : addrtype, lim : limits}: `%|-%:%`(C, VLOAD_instr(V128_vectype, ?(), x, memarg), `%->_%%`_instrtype(`%`_resulttype([(at : addrtype <: valtype)]), [], `%`_resulttype([V128_valtype]))) -- if (C.MEMS_context[x!`%`_idx.0] = `%%PAGE`_memtype(at, lim)) -- Memarg_ok: `|-%:%->%`(memarg, at, $vsize(V128_vectype)) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:500.1-503.41 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:502.1-505.41 rule `vload-pack`{C : context, M : M, N : N, sx : sx, x : idx, memarg : memarg, at : addrtype, lim : limits}: `%|-%:%`(C, VLOAD_instr(V128_vectype, ?(`SHAPE%X%_%`_vloadop_(`%`_sz(M), N, sx)), x, memarg), `%->_%%`_instrtype(`%`_resulttype([(at : addrtype <: valtype)]), [], `%`_resulttype([V128_valtype]))) -- if (C.MEMS_context[x!`%`_idx.0] = `%%PAGE`_memtype(at, lim)) -- Memarg_ok: `|-%:%->%`(memarg, at, (M * N)) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:505.1-508.36 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:507.1-510.36 rule `vload-splat`{C : context, N : N, x : idx, memarg : memarg, at : addrtype, lim : limits}: `%|-%:%`(C, VLOAD_instr(V128_vectype, ?(SPLAT_vloadop_(`%`_sz(N))), x, memarg), `%->_%%`_instrtype(`%`_resulttype([(at : addrtype <: valtype)]), [], `%`_resulttype([V128_valtype]))) -- if (C.MEMS_context[x!`%`_idx.0] = `%%PAGE`_memtype(at, lim)) -- Memarg_ok: `|-%:%->%`(memarg, at, N) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:510.1-513.36 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:512.1-515.36 rule `vload-zero`{C : context, N : N, x : idx, memarg : memarg, at : addrtype, lim : limits}: `%|-%:%`(C, VLOAD_instr(V128_vectype, ?(ZERO_vloadop_(`%`_sz(N))), x, memarg), `%->_%%`_instrtype(`%`_resulttype([(at : addrtype <: valtype)]), [], `%`_resulttype([V128_valtype]))) -- if (C.MEMS_context[x!`%`_idx.0] = `%%PAGE`_memtype(at, lim)) -- Memarg_ok: `|-%:%->%`(memarg, at, N) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:515.1-519.21 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:517.1-521.21 rule vload_lane{C : context, N : N, x : idx, memarg : memarg, i : laneidx, at : addrtype, lim : limits}: `%|-%:%`(C, VLOAD_LANE_instr(V128_vectype, `%`_sz(N), x, memarg, i), `%->_%%`_instrtype(`%`_resulttype([(at : addrtype <: valtype) V128_valtype]), [], `%`_resulttype([V128_valtype]))) -- if (C.MEMS_context[x!`%`_idx.0] = `%%PAGE`_memtype(at, lim)) -- Memarg_ok: `|-%:%->%`(memarg, at, N) -- if ((i!`%`_laneidx.0 : nat <:> rat) < ((128 : nat <:> rat) / (N : nat <:> rat))) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:521.1-524.47 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:523.1-526.47 rule vstore{C : context, x : idx, memarg : memarg, at : addrtype, lim : limits}: `%|-%:%`(C, VSTORE_instr(V128_vectype, x, memarg), `%->_%%`_instrtype(`%`_resulttype([(at : addrtype <: valtype) V128_valtype]), [], `%`_resulttype([]))) -- if (C.MEMS_context[x!`%`_idx.0] = `%%PAGE`_memtype(at, lim)) -- Memarg_ok: `|-%:%->%`(memarg, at, $vsize(V128_vectype)) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:526.1-530.21 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:528.1-532.21 rule vstore_lane{C : context, N : N, x : idx, memarg : memarg, i : laneidx, at : addrtype, lim : limits}: `%|-%:%`(C, VSTORE_LANE_instr(V128_vectype, `%`_sz(N), x, memarg, i), `%->_%%`_instrtype(`%`_resulttype([(at : addrtype <: valtype) V128_valtype]), [], `%`_resulttype([]))) -- if (C.MEMS_context[x!`%`_idx.0] = `%%PAGE`_memtype(at, lim)) -- Memarg_ok: `|-%:%->%`(memarg, at, N) -- if ((i!`%`_laneidx.0 : nat <:> rat) < ((128 : nat <:> rat) / (N : nat <:> rat))) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:535.1-536.33 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:537.1-538.33 rule const{C : context, nt : numtype, c_nt : num_(nt)}: `%|-%:%`(C, CONST_instr(nt, c_nt), `%->_%%`_instrtype(`%`_resulttype([]), [], `%`_resulttype([(nt : numtype <: valtype)]))) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:538.1-539.34 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:540.1-541.34 rule unop{C : context, nt : numtype, unop_nt : unop_(nt)}: `%|-%:%`(C, UNOP_instr(nt, unop_nt), `%->_%%`_instrtype(`%`_resulttype([(nt : numtype <: valtype)]), [], `%`_resulttype([(nt : numtype <: valtype)]))) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:541.1-542.39 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:543.1-544.39 rule binop{C : context, nt : numtype, binop_nt : binop_(nt)}: `%|-%:%`(C, BINOP_instr(nt, binop_nt), `%->_%%`_instrtype(`%`_resulttype([(nt : numtype <: valtype) (nt : numtype <: valtype)]), [], `%`_resulttype([(nt : numtype <: valtype)]))) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:544.1-545.39 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:546.1-547.39 rule testop{C : context, nt : numtype, testop_nt : testop_(nt)}: `%|-%:%`(C, TESTOP_instr(nt, testop_nt), `%->_%%`_instrtype(`%`_resulttype([(nt : numtype <: valtype)]), [], `%`_resulttype([I32_valtype]))) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:547.1-548.40 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:549.1-550.40 rule relop{C : context, nt : numtype, relop_nt : relop_(nt)}: `%|-%:%`(C, RELOP_instr(nt, relop_nt), `%->_%%`_instrtype(`%`_resulttype([(nt : numtype <: valtype) (nt : numtype <: valtype)]), [], `%`_resulttype([I32_valtype]))) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:550.1-551.44 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:552.1-553.44 rule cvtop{C : context, nt_1 : numtype, nt_2 : numtype, cvtop : cvtop__(nt_2, nt_1)}: `%|-%:%`(C, CVTOP_instr(nt_1, nt_2, cvtop), `%->_%%`_instrtype(`%`_resulttype([(nt_2 : numtype <: valtype)]), [], `%`_resulttype([(nt_1 : numtype <: valtype)]))) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:556.1-557.35 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:558.1-559.35 rule vconst{C : context, c : vec_(V128_Vnn)}: `%|-%:%`(C, VCONST_instr(V128_vectype, c), `%->_%%`_instrtype(`%`_resulttype([]), [], `%`_resulttype([V128_valtype]))) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:559.1-560.41 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:561.1-562.41 rule vvunop{C : context, vvunop : vvunop}: `%|-%:%`(C, VVUNOP_instr(V128_vectype, vvunop), `%->_%%`_instrtype(`%`_resulttype([V128_valtype]), [], `%`_resulttype([V128_valtype]))) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:562.1-563.48 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:564.1-565.48 rule vvbinop{C : context, vvbinop : vvbinop}: `%|-%:%`(C, VVBINOP_instr(V128_vectype, vvbinop), `%->_%%`_instrtype(`%`_resulttype([V128_valtype V128_valtype]), [], `%`_resulttype([V128_valtype]))) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:565.1-566.55 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:567.1-568.55 rule vvternop{C : context, vvternop : vvternop}: `%|-%:%`(C, VVTERNOP_instr(V128_vectype, vvternop), `%->_%%`_instrtype(`%`_resulttype([V128_valtype V128_valtype V128_valtype]), [], `%`_resulttype([V128_valtype]))) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:568.1-569.44 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:570.1-571.44 rule vvtestop{C : context, vvtestop : vvtestop}: `%|-%:%`(C, VVTESTOP_instr(V128_vectype, vvtestop), `%->_%%`_instrtype(`%`_resulttype([V128_valtype]), [], `%`_resulttype([I32_valtype]))) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:571.1-572.37 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:573.1-574.37 rule vunop{C : context, sh : shape, vunop : vunop_(sh)}: `%|-%:%`(C, VUNOP_instr(sh, vunop), `%->_%%`_instrtype(`%`_resulttype([V128_valtype]), [], `%`_resulttype([V128_valtype]))) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:574.1-575.44 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:576.1-577.44 rule vbinop{C : context, sh : shape, vbinop : vbinop_(sh)}: `%|-%:%`(C, VBINOP_instr(sh, vbinop), `%->_%%`_instrtype(`%`_resulttype([V128_valtype V128_valtype]), [], `%`_resulttype([V128_valtype]))) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:577.1-578.51 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:579.1-580.51 rule vternop{C : context, sh : shape, vternop : vternop_(sh)}: `%|-%:%`(C, VTERNOP_instr(sh, vternop), `%->_%%`_instrtype(`%`_resulttype([V128_valtype V128_valtype V128_valtype]), [], `%`_resulttype([V128_valtype]))) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:580.1-581.40 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:582.1-583.40 rule vtestop{C : context, sh : shape, vtestop : vtestop_(sh)}: `%|-%:%`(C, VTESTOP_instr(sh, vtestop), `%->_%%`_instrtype(`%`_resulttype([V128_valtype]), [], `%`_resulttype([I32_valtype]))) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:583.1-584.44 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:585.1-586.44 rule vrelop{C : context, sh : shape, vrelop : vrelop_(sh)}: `%|-%:%`(C, VRELOP_instr(sh, vrelop), `%->_%%`_instrtype(`%`_resulttype([V128_valtype V128_valtype]), [], `%`_resulttype([V128_valtype]))) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:586.1-587.47 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:588.1-589.47 rule vshiftop{C : context, sh : ishape, vshiftop : vshiftop_(sh)}: `%|-%:%`(C, VSHIFTOP_instr(sh, vshiftop), `%->_%%`_instrtype(`%`_resulttype([V128_valtype I32_valtype]), [], `%`_resulttype([V128_valtype]))) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:589.1-590.33 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:591.1-592.33 rule vbitmask{C : context, sh : ishape}: `%|-%:%`(C, VBITMASK_instr(sh), `%->_%%`_instrtype(`%`_resulttype([V128_valtype]), [], `%`_resulttype([I32_valtype]))) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:592.1-593.50 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:594.1-595.50 rule vswizzlop{C : context, sh : bshape, vswizzlop : vswizzlop_(sh)}: `%|-%:%`(C, VSWIZZLOP_instr(sh, vswizzlop), `%->_%%`_instrtype(`%`_resulttype([V128_valtype V128_valtype]), [], `%`_resulttype([V128_valtype]))) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:595.1-597.29 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:597.1-599.29 rule vshuffle{C : context, sh : bshape, `i*` : laneidx*}: `%|-%:%`(C, VSHUFFLE_instr(sh, i*{i <- `i*`}), `%->_%%`_instrtype(`%`_resulttype([V128_valtype V128_valtype]), [], `%`_resulttype([V128_valtype]))) -- (if (i!`%`_laneidx.0 < (2 * $dim(sh!`%`_bshape.0)!`%`_dim.0)))*{i <- `i*`} - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:599.1-600.44 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:601.1-602.44 rule vsplat{C : context, sh : shape}: `%|-%:%`(C, VSPLAT_instr(sh), `%->_%%`_instrtype(`%`_resulttype([($unpackshape(sh) : numtype <: valtype)]), [], `%`_resulttype([V128_valtype]))) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:602.1-604.21 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:604.1-606.21 rule vextract_lane{C : context, sh : shape, `sx?` : sx?, i : laneidx}: `%|-%:%`(C, VEXTRACT_LANE_instr(sh, sx?{sx <- `sx?`}, i), `%->_%%`_instrtype(`%`_resulttype([V128_valtype]), [], `%`_resulttype([($unpackshape(sh) : numtype <: valtype)]))) -- if (i!`%`_laneidx.0 < $dim(sh)!`%`_dim.0) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:606.1-608.21 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:608.1-610.21 rule vreplace_lane{C : context, sh : shape, i : laneidx}: `%|-%:%`(C, VREPLACE_LANE_instr(sh, i), `%->_%%`_instrtype(`%`_resulttype([V128_valtype ($unpackshape(sh) : numtype <: valtype)]), [], `%`_resulttype([V128_valtype]))) -- if (i!`%`_laneidx.0 < $dim(sh)!`%`_dim.0) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:610.1-611.50 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:612.1-613.50 rule vextunop{C : context, sh_1 : ishape, sh_2 : ishape, vextunop : vextunop__(sh_2, sh_1)}: `%|-%:%`(C, VEXTUNOP_instr(sh_1, sh_2, vextunop), `%->_%%`_instrtype(`%`_resulttype([V128_valtype]), [], `%`_resulttype([V128_valtype]))) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:613.1-614.57 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:615.1-616.57 rule vextbinop{C : context, sh_1 : ishape, sh_2 : ishape, vextbinop : vextbinop__(sh_2, sh_1)}: `%|-%:%`(C, VEXTBINOP_instr(sh_1, sh_2, vextbinop), `%->_%%`_instrtype(`%`_resulttype([V128_valtype V128_valtype]), [], `%`_resulttype([V128_valtype]))) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:616.1-617.64 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:618.1-619.64 rule vextternop{C : context, sh_1 : ishape, sh_2 : ishape, vextternop : vextternop__(sh_2, sh_1)}: `%|-%:%`(C, VEXTTERNOP_instr(sh_1, sh_2, vextternop), `%->_%%`_instrtype(`%`_resulttype([V128_valtype V128_valtype V128_valtype]), [], `%`_resulttype([V128_valtype]))) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:619.1-620.48 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:621.1-622.48 rule vnarrow{C : context, sh_1 : ishape, sh_2 : ishape, sx : sx}: `%|-%:%`(C, VNARROW_instr(sh_1, sh_2, sx), `%->_%%`_instrtype(`%`_resulttype([V128_valtype V128_valtype]), [], `%`_resulttype([V128_valtype]))) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:622.1-623.46 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:624.1-625.46 rule vcvtop{C : context, sh_1 : shape, sh_2 : shape, vcvtop : vcvtop__(sh_2, sh_1)}: `%|-%:%`(C, VCVTOP_instr(sh_1, sh_2, vcvtop), `%->_%%`_instrtype(`%`_resulttype([V128_valtype]), [], `%`_resulttype([V128_valtype]))) ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:6.1-6.96 relation Instrs_ok: `%|-%:%`(context, instr*, instrtype) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:628.1-629.24 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:630.1-631.24 rule empty{C : context}: `%|-%:%`(C, [], `%->_%%`_instrtype(`%`_resulttype([]), [], `%`_resulttype([]))) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:632.1-636.82 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:634.1-638.82 rule seq{C : context, instr_1 : instr, `instr_2*` : instr*, `t_1*` : valtype*, `x_1*` : idx*, `x_2*` : idx*, `t_3*` : valtype*, `t_2*` : valtype*, `init*` : init*, `t*` : valtype*}: `%|-%:%`(C, [instr_1] ++ instr_2*{instr_2 <- `instr_2*`}, `%->_%%`_instrtype(`%`_resulttype(t_1*{t_1 <- `t_1*`}), x_1*{x_1 <- `x_1*`} ++ x_2*{x_2 <- `x_2*`}, `%`_resulttype(t_3*{t_3 <- `t_3*`}))) -- Instr_ok: `%|-%:%`(C, instr_1, `%->_%%`_instrtype(`%`_resulttype(t_1*{t_1 <- `t_1*`}), x_1*{x_1 <- `x_1*`}, `%`_resulttype(t_2*{t_2 <- `t_2*`}))) -- (if (C.LOCALS_context[x_1!`%`_idx.0] = `%%`_localtype(init, t)))*{init <- `init*`, t <- `t*`, x_1 <- `x_1*`} -- Instrs_ok: `%|-%:%`($with_locals(C, x_1*{x_1 <- `x_1*`}, `%%`_localtype(SET_init, t)*{t <- `t*`}), instr_2*{instr_2 <- `instr_2*`}, `%->_%%`_instrtype(`%`_resulttype(t_2*{t_2 <- `t_2*`}), x_2*{x_2 <- `x_2*`}, `%`_resulttype(t_3*{t_3 <- `t_3*`}))) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:638.1-642.33 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:640.1-644.33 rule sub{C : context, `instr*` : instr*, it' : instrtype, it : instrtype}: `%|-%:%`(C, instr*{instr <- `instr*`}, it') -- Instrs_ok: `%|-%:%`(C, instr*{instr <- `instr*`}, it) -- Instrtype_sub: `%|-%<:%`(C, it, it') -- Instrtype_ok: `%|-%:OK`(C, it') - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:645.1-648.33 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:647.1-650.33 rule frame{C : context, `instr*` : instr*, `t*` : valtype*, `t_1*` : valtype*, `x*` : idx*, `t_2*` : valtype*}: `%|-%:%`(C, instr*{instr <- `instr*`}, `%->_%%`_instrtype(`%`_resulttype(t*{t <- `t*`} ++ t_1*{t_1 <- `t_1*`}), x*{x <- `x*`}, `%`_resulttype(t*{t <- `t*`} ++ t_2*{t_2 <- `t_2*`}))) -- Instrs_ok: `%|-%:%`(C, instr*{instr <- `instr*`}, `%->_%%`_instrtype(`%`_resulttype(t_1*{t_1 <- `t_1*`}), x*{x <- `x*`}, `%`_resulttype(t_2*{t_2 <- `t_2*`}))) @@ -4272,9 +4274,10 @@ relation Elem_ok: `%|-%:%`(context, elem, elemtype) ;; ../../../../specification/wasm-latest/2.4-validation.modules.spectec relation Start_ok: `%|-%:OK`(context, start) ;; ../../../../specification/wasm-latest/2.4-validation.modules.spectec - rule _{C : context, x : idx}: + rule _{C : context, x : idx, `exact?` : exact?, dt : deftype}: `%|-%:OK`(C, START_start(x)) - -- Expand: `%~~%`(C.FUNCS_context[x!`%`_idx.0], `FUNC%->%`_comptype(`%`_resulttype([]), `%`_resulttype([]))) + -- if (C.FUNCS_context[x!`%`_idx.0] = _HT_heaptype(exact?{exact <- `exact?`}, (dt : deftype <: typeuse))) + -- Expand: `%~~%`(dt, `FUNC%->%`_comptype(`%`_resulttype([]), `%`_resulttype([]))) ;; ../../../../specification/wasm-latest/2.4-validation.modules.spectec relation Import_ok: `%|-%:%`(context, import, externtype) @@ -4306,9 +4309,9 @@ relation Externidx_ok: `%|-%:%`(context, externidx, externtype) -- if (C.TABLES_context[x!`%`_idx.0] = tt) ;; ../../../../specification/wasm-latest/2.4-validation.modules.spectec - rule func{C : context, x : idx, dt : deftype}: - `%|-%:%`(C, FUNC_externidx(x), FUNC_externtype((dt : deftype <: typeuse))) - -- if (C.FUNCS_context[x!`%`_idx.0] = dt) + rule func{C : context, x : idx, ht : heaptype}: + `%|-%:%`(C, FUNC_externidx(x), FUNC_externtype(ht)) + -- if (C.FUNCS_context[x!`%`_idx.0] = ht) ;; ../../../../specification/wasm-latest/2.4-validation.modules.spectec relation Export_ok: `%|-%:%%`(context, export, name, externtype) @@ -4320,13 +4323,13 @@ relation Export_ok: `%|-%:%%`(context, export, name, externtype) ;; ../../../../specification/wasm-latest/2.4-validation.modules.spectec rec { -;; ../../../../specification/wasm-latest/2.4-validation.modules.spectec:136.1-136.100 +;; ../../../../specification/wasm-latest/2.4-validation.modules.spectec:137.1-137.100 relation Globals_ok: `%|-%:%`(context, global*, globaltype*) - ;; ../../../../specification/wasm-latest/2.4-validation.modules.spectec:180.1-181.17 + ;; ../../../../specification/wasm-latest/2.4-validation.modules.spectec:182.1-183.17 rule empty{C : context}: `%|-%:%`(C, [], []) - ;; ../../../../specification/wasm-latest/2.4-validation.modules.spectec:183.1-186.54 + ;; ../../../../specification/wasm-latest/2.4-validation.modules.spectec:185.1-188.54 rule cons{C : context, global_1 : global, `global*` : global*, gt_1 : globaltype, `gt*` : globaltype*}: `%|-%:%`(C, [global_1] ++ global*{global <- `global*`}, [gt_1] ++ gt*{gt <- `gt*`}) -- Global_ok: `%|-%:%`(C, global_1, gt_1) @@ -4336,13 +4339,13 @@ relation Globals_ok: `%|-%:%`(context, global*, globaltype*) ;; ../../../../specification/wasm-latest/2.4-validation.modules.spectec rec { -;; ../../../../specification/wasm-latest/2.4-validation.modules.spectec:135.1-135.98 +;; ../../../../specification/wasm-latest/2.4-validation.modules.spectec:136.1-136.98 relation Types_ok: `%|-%:%`(context, type*, deftype*) - ;; ../../../../specification/wasm-latest/2.4-validation.modules.spectec:172.1-173.17 + ;; ../../../../specification/wasm-latest/2.4-validation.modules.spectec:174.1-175.17 rule empty{C : context}: `%|-%:%`(C, [], []) - ;; ../../../../specification/wasm-latest/2.4-validation.modules.spectec:175.1-178.49 + ;; ../../../../specification/wasm-latest/2.4-validation.modules.spectec:177.1-180.49 rule cons{C : context, type_1 : type, `type*` : type*, `dt_1*` : deftype*, `dt*` : deftype*}: `%|-%:%`(C, [type_1] ++ type*{type <- `type*`}, dt_1*{dt_1 <- `dt_1*`} ++ dt*{dt <- `dt*`}) -- Type_ok: `%|-%:%`(C, type_1, dt_1*{dt_1 <- `dt_1*`}) @@ -4361,7 +4364,7 @@ def $funcidx_nonfuncs(nonfuncs : nonfuncs) : funcidx* ;; ../../../../specification/wasm-latest/2.4-validation.modules.spectec relation Module_ok: `|-%:%`(module, moduletype) ;; ../../../../specification/wasm-latest/2.4-validation.modules.spectec - rule _{`type*` : type*, `import*` : import*, `tag*` : tag*, `global*` : global*, `mem*` : mem*, `table*` : table*, `func*` : func*, `data*` : data*, `elem*` : elem*, `start?` : start?, `export*` : export*, C : context, `xt_I*` : externtype*, `xt_E*` : externtype*, `dt'*` : deftype*, C' : context, `jt*` : tagtype*, `gt*` : globaltype*, `mt*` : memtype*, `tt*` : tabletype*, `dt*` : deftype*, `ok*` : datatype*, `rt*` : reftype*, `nm*` : name*, `jt_I*` : tagtype*, `mt_I*` : memtype*, `tt_I*` : tabletype*, `gt_I*` : globaltype*, `dt_I*` : deftype*, `x*` : idx*}: + rule _{`type*` : type*, `import*` : import*, `tag*` : tag*, `global*` : global*, `mem*` : mem*, `table*` : table*, `func*` : func*, `data*` : data*, `elem*` : elem*, `start?` : start?, `export*` : export*, C : context, `xt_I*` : externtype*, `xt_E*` : externtype*, `dt'*` : deftype*, C' : context, `jt*` : tagtype*, `gt*` : globaltype*, `mt*` : memtype*, `tt*` : tabletype*, `dt*` : deftype*, `ok*` : datatype*, `rt*` : reftype*, `nm*` : name*, `jt_I*` : tagtype*, `mt_I*` : memtype*, `tt_I*` : tabletype*, `gt_I*` : globaltype*, `ht_I*` : heaptype*, `ht*` : heaptype*, `x*` : idx*}: `|-%:%`(MODULE_module(type*{type <- `type*`}, import*{import <- `import*`}, tag*{tag <- `tag*`}, global*{global <- `global*`}, mem*{mem <- `mem*`}, table*{table <- `table*`}, func*{func <- `func*`}, data*{data <- `data*`}, elem*{elem <- `elem*`}, start?{start <- `start?`}, export*{export <- `export*`}), $clos_moduletype(C, `%->%`_moduletype(xt_I*{xt_I <- `xt_I*`}, xt_E*{xt_E <- `xt_E*`}))) -- Types_ok: `%|-%:%`({TYPES [], RECS [], TAGS [], GLOBALS [], MEMS [], TABLES [], FUNCS [], DATAS [], ELEMS [], LOCALS [], LABELS [], RETURN ?(), REFS []}, type*{type <- `type*`}, dt'*{dt' <- `dt'*`}) -- (Import_ok: `%|-%:%`({TYPES dt'*{dt' <- `dt'*`}, RECS [], TAGS [], GLOBALS [], MEMS [], TABLES [], FUNCS [], DATAS [], ELEMS [], LOCALS [], LABELS [], RETURN ?(), REFS []}, import, xt_I))*{import <- `import*`, xt_I <- `xt_I*`} @@ -4376,13 +4379,14 @@ relation Module_ok: `|-%:%`(module, moduletype) -- (Export_ok: `%|-%:%%`(C, export, nm, xt_E))*{export <- `export*`, nm <- `nm*`, xt_E <- `xt_E*`} -- if $disjoint_(syntax name, nm*{nm <- `nm*`}) -- if (C = C' +++ {TYPES [], RECS [], 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 []}) - -- if (C' = {TYPES dt'*{dt' <- `dt'*`}, RECS [], 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*`}}) + -- if (C' = {TYPES dt'*{dt' <- `dt'*`}, RECS [], TAGS [], GLOBALS gt_I*{gt_I <- `gt_I*`}, MEMS [], TABLES [], FUNCS ht_I*{ht_I <- `ht_I*`} ++ ht*{ht <- `ht*`}, DATAS [], ELEMS [], LOCALS [], LABELS [], RETURN ?(), REFS x*{x <- `x*`}}) + -- if (ht*{ht <- `ht*`} = _HT_heaptype(?(EXACT_exact), (dt : deftype <: typeuse))*{dt <- `dt*`}) -- if (x*{x <- `x*`} = $funcidx_nonfuncs(`%%%%`_nonfuncs(global*{global <- `global*`}, mem*{mem <- `mem*`}, table*{table <- `table*`}, elem*{elem <- `elem*`}))) -- if (jt_I*{jt_I <- `jt_I*`} = $tagsxt(xt_I*{xt_I <- `xt_I*`})) -- if (gt_I*{gt_I <- `gt_I*`} = $globalsxt(xt_I*{xt_I <- `xt_I*`})) -- if (mt_I*{mt_I <- `mt_I*`} = $memsxt(xt_I*{xt_I <- `xt_I*`})) -- if (tt_I*{tt_I <- `tt_I*`} = $tablesxt(xt_I*{xt_I <- `xt_I*`})) - -- if (dt_I*{dt_I <- `dt_I*`} = $funcsxt(xt_I*{xt_I <- `xt_I*`})) + -- if (ht_I*{ht_I <- `ht_I*`} = $funcsxt(xt_I*{xt_I <- `xt_I*`})) ;; ../../../../specification/wasm-latest/3.0-numerics.relaxed.spectec syntax relaxed2 = @@ -6015,7 +6019,7 @@ relation Externaddr_ok: `%|-%:%`(store, externaddr, externtype) ;; ../../../../specification/wasm-latest/4.1-execution.values.spectec:104.1-106.30 rule func{s : store, a : addr, funcinst : funcinst}: - `%|-%:%`(s, FUNC_externaddr(a), FUNC_externtype((funcinst.TYPE_funcinst : deftype <: typeuse))) + `%|-%:%`(s, FUNC_externaddr(a), FUNC_externtype(_HT_heaptype(?(EXACT_exact), (funcinst.TYPE_funcinst : deftype <: typeuse)))) -- if (s.FUNCS_store[a] = funcinst) ;; ../../../../specification/wasm-latest/4.1-execution.values.spectec:108.1-111.37 @@ -7734,7 +7738,9 @@ grammar Btabletype : tabletype ;; ../../../../specification/wasm-latest/5.2-binary.types.spectec grammar Bexterntype : externtype ;; ../../../../specification/wasm-latest/5.2-binary.types.spectec - prod{x : idx} {{0x00} {x:Btypeidx}} => FUNC_externtype(_IDX_typeuse(x)) + prod{x : idx} {{0x00} {x:Btypeidx}} => FUNC_externtype(_HT_heaptype(?(), _IDX_typeuse(x))) + ;; ../../../../specification/wasm-latest/5.2-binary.types.spectec + prod{x : idx} {{0x20} {x:Btypeidx}} => FUNC_externtype(_HT_heaptype(?(EXACT_exact), _IDX_typeuse(x))) ;; ../../../../specification/wasm-latest/5.2-binary.types.spectec prod{tt : tabletype} {{0x01} {tt:Btabletype}} => TABLE_externtype(tt) ;; ../../../../specification/wasm-latest/5.2-binary.types.spectec @@ -9804,7 +9810,9 @@ grammar Texterntype_(I : I) : (externtype, idctxt) ;; ../../../../specification/wasm-latest/6.2-text.types.spectec prod{`id?` : char?, tt : tabletype} {{"("} {"table"} {?(`%`_name(lift(id?{id <- `id?`}))):Tid?{}} {tt:Ttabletype_(I)} {")"}} => (TABLE_externtype(tt), {TYPES [], TAGS [], GLOBALS [], MEMS [], TABLES [?(`%`_name(lift(id?{id <- `id?`})))], FUNCS [], DATAS [], ELEMS [], LOCALS [], LABELS [], FIELDS [], TYPEDEFS []}) ;; ../../../../specification/wasm-latest/6.2-text.types.spectec - prod{`id?` : char?, x : idx, I' : I} {{"("} {"func"} {?(`%`_name(lift(id?{id <- `id?`}))):Tid?{}} {(x, I'):Ttypeuse_(I)} {")"}} => (FUNC_externtype(_IDX_typeuse(x)), {TYPES [], TAGS [], GLOBALS [], MEMS [], TABLES [], FUNCS [?(`%`_name(lift(id?{id <- `id?`})))], DATAS [], ELEMS [], LOCALS [], LABELS [], FIELDS [], TYPEDEFS []}) + prod{`id?` : char?, x : idx, I' : I} {{"("} {"func"} {?(`%`_name(lift(id?{id <- `id?`}))):Tid?{}} {(x, I'):Ttypeuse_(I)} {")"}} => (FUNC_externtype(_HT_heaptype(?(), _IDX_typeuse(x))), {TYPES [], TAGS [], GLOBALS [], MEMS [], TABLES [], FUNCS [?(`%`_name(lift(id?{id <- `id?`})))], DATAS [], ELEMS [], LOCALS [], LABELS [], FIELDS [], TYPEDEFS []}) + ;; ../../../../specification/wasm-latest/6.2-text.types.spectec + prod{`id?` : char?, x : idx, I' : I} {{"("} {"func"} {?(`%`_name(lift(id?{id <- `id?`}))):Tid?{}} {"("} {"exact"} {(x, I'):Ttypeuse_(I)} {")"} {")"}} => (FUNC_externtype(_HT_heaptype(?(EXACT_exact), _IDX_typeuse(x))), {TYPES [], TAGS [], GLOBALS [], MEMS [], TABLES [], FUNCS [?(`%`_name(lift(id?{id <- `id?`})))], DATAS [], ELEMS [], LOCALS [], LABELS [], FIELDS [], TYPEDEFS []}) ;; ../../../../specification/wasm-latest/6.3-text.instructions.spectec grammar Tlabel_(I : I) : (name?, I)