diff --git a/document/core/syntax/instructions.rst b/document/core/syntax/instructions.rst index 516e02a67..b850737e1 100644 --- a/document/core/syntax/instructions.rst +++ b/document/core/syntax/instructions.rst @@ -61,6 +61,8 @@ If missing, the operands must be of :ref:`numeric ` or :ref:`vec .. _syntax-br_on_non_null: .. _syntax-br_on_cast: .. _syntax-br_on_cast_fail: +.. _syntax-br_on_cast_desc_eq: +.. _syntax-br_on_cast_desc_eq_fail: .. _syntax-call: .. _syntax-call_ref: .. _syntax-call_indirect: @@ -113,6 +115,7 @@ ${:BR_IF} performs a conditional branch, and ${:BR_TABLE} performs an indirect branch through an operand indexing into the label list that is an immediate to the instruction, or to a default target if the operand is out of bounds. The ${:BR_ON_NULL} and ${:BR_ON_NON_NULL} instructions check whether a reference operand is :ref:`null ` and branch if that is the case or not the case, respectively. Similarly, ${:BR_ON_CAST} and ${:BR_ON_CAST_FAIL} attempt a downcast on a reference operand and branch if that succeeds, or fails, respectively. +The ${:BR_ON_CAST_DESC_EQ} and ${:BR_ON_CAST_DESC_EQ_FAIL} instructions perform a similar cast check but compare the operand's descriptor against a given descriptor value. The ${:RETURN} instruction is a shortcut for an unconditional branch to the outermost block, which implicitly is the body of the current function. Taking a branch *unwinds* the operand stack up to the height where the targeted structured control instruction was entered. @@ -234,6 +237,7 @@ The ${:DATA.DROP} instruction prevents further use of a passive data segment. Th .. _syntax-ref.get_desc: .. _syntax-ref.test: .. _syntax-ref.cast: +.. _syntax-ref.cast_desc_eq: .. _syntax-instr-ref: Reference Instructions @@ -255,10 +259,12 @@ The instruction ${:REF.GET_DESC} gets the :ref:`descriptor ` of The instructions ${:REF.TEST} and ${:REF.CAST} test the :ref:`dynamic type ` of a reference operand. The former merely returns the result of the test, while the latter performs a downcast and :ref:`traps ` if the operand's type does not match. +The instruction ${:REF.CAST_DESC_EQ} performs a similar downcast but checks the operand's descriptor against a given descriptor value instead of checking its dynamic type. .. note:: The ${:BR_ON_NULL} and ${:BR_ON_NON_NULL} instructions provide versions of ${:REF.AS_NON_NULL} that branch depending on the success or failure of a null test instead of trapping. - Similarly, the ${:BR_ON_CAST} and ${:BR_ON_CAST_FAIL} instructions provides versions of ${:REF.CAST} that branch depending on the success of the downcast instead of trapping. + Similarly, the ${:BR_ON_CAST} and ${:BR_ON_CAST_FAIL} instructions provides versions of ${:REF.CAST} that branch depending on the success of the downcast instead of trapping, + and ${:BR_ON_CAST_DESC_EQ} and ${:BR_ON_CAST_DESC_EQ_FAIL} provide branching versions of ${:REF.CAST_DESC_EQ}. An additional instruction operating on function references is the :ref:`control instruction ` ${:CALL_REF}. diff --git a/document/core/util/macros.def b/document/core/util/macros.def index c4b0ccabb..419cfdf0f 100644 --- a/document/core/util/macros.def +++ b/document/core/util/macros.def @@ -493,6 +493,8 @@ .. |BRONNONNULL| mathdef:: \xref{syntax/instructions}{syntax-instr-control}{\K{br\_on\_non\_null}} .. |BRONCAST| mathdef:: \xref{syntax/instructions}{syntax-instr-control}{\K{br\_on\_cast}} .. |BRONCASTFAIL| mathdef:: \xref{syntax/instructions}{syntax-instr-control}{\K{br\_on\_cast\_fail}} +.. |BRONCASTDESCEQ| mathdef:: \xref{syntax/instructions}{syntax-instr-control}{\K{br\_on\_cast\_desc\_eq}} +.. |BRONCASTDESCEQFAIL| mathdef:: \xref{syntax/instructions}{syntax-instr-control}{\K{br\_on\_cast\_desc\_eq\_fail}} .. |RETURN| mathdef:: \xref{syntax/instructions}{syntax-instr-control}{\K{return}} .. |CALL| mathdef:: \xref{syntax/instructions}{syntax-instr-control}{\K{call}} @@ -552,6 +554,7 @@ .. |REFGETDESC| mathdef:: \xref{syntax/instructions}{syntax-instr-ref}{\K{ref.get\_desc}} .. |REFTEST| mathdef:: \xref{syntax/instructions}{syntax-instr-ref}{\K{ref{.}test}} .. |REFCAST| mathdef:: \xref{syntax/instructions}{syntax-instr-ref}{\K{ref{.}cast}} +.. |REFCASTDESCEQ| mathdef:: \xref{syntax/instructions}{syntax-instr-ref}{\K{ref{.}cast\_desc\_eq}} .. |STRUCTNEW| mathdef:: \xref{syntax/instructions}{syntax-instr-struct}{\K{struct{.}new}} .. |STRUCTNEWDEFAULT| mathdef:: \xref{syntax/instructions}{syntax-instr-struct}{\K{struct{.}new\_default}} diff --git a/document/core/valid/instructions.rst b/document/core/valid/instructions.rst index 7dc05b840..8b1db1a79 100644 --- a/document/core/valid/instructions.rst +++ b/document/core/valid/instructions.rst @@ -252,6 +252,32 @@ $${rule: Instr_ok/br_on_cast_fail} The existence of a common supertype ${:rt_3} means that ${:rt_1} and ${:rt_2} must be in the same heap subtyping hierarchy. +.. _valid-br_on_cast_desc_eq: + +:math:`\BRONCASTDESCEQ~l~\X{rt}_1~\X{rt}_2` +........................................... + +$${rule-prose: Instr_ok/br_on_cast_desc_eq} + +$${rule: Instr_ok/br_on_cast_desc_eq} + +.. note:: + The existence of a common supertype ${:rt_3} means that ${:rt_1} and ${:rt_2} must be in the same heap subtyping hierarchy. + + +.. _valid-br_on_cast_desc_eq_fail: + +:math:`\BRONCASTDESCEQFAIL~l~\X{rt}_1~\X{rt}_2` +................................................ + +$${rule-prose: Instr_ok/br_on_cast_desc_eq_fail} + +$${rule: Instr_ok/br_on_cast_desc_eq_fail} + +.. note:: + The existence of a common supertype ${:rt_3} means that ${:rt_1} and ${:rt_2} must be in the same heap subtyping hierarchy. + + .. _valid-call: :math:`\CALL~x` @@ -839,6 +865,16 @@ $${rule: Instr_ok/ref.cast} The liberty to pick a supertype ${:rt'} allows typing the instruction with the least precise super type of ${:rt} as input, that is, the top type in the corresponding heap subtyping hierarchy. +.. _valid-ref.cast_desc_eq: + +:math:`\REFCASTDESCEQ~\X{rt}` +............................. + +$${rule-prose: Instr_ok/ref.cast_desc_eq} + +$${rule: Instr_ok/ref.cast_desc_eq} + + .. index:: aggregate reference Aggregate Reference Instructions diff --git a/specification/wasm-latest/1.3-syntax.instructions.spectec b/specification/wasm-latest/1.3-syntax.instructions.spectec index 3a586db75..add01ba2f 100644 --- a/specification/wasm-latest/1.3-syntax.instructions.spectec +++ b/specification/wasm-latest/1.3-syntax.instructions.spectec @@ -234,6 +234,8 @@ syntax instr/br hint(desc "branch instruction") = ... | BR_ON_NON_NULL labelidx | BR_ON_CAST labelidx reftype reftype | BR_ON_CAST_FAIL labelidx reftype reftype + | BR_ON_CAST_DESC_EQ labelidx reftype reftype + | BR_ON_CAST_DESC_EQ_FAIL labelidx reftype reftype | ... syntax instr/call hint(desc "function instruction") = ... @@ -309,6 +311,7 @@ syntax instr/ref hint(desc "reference instruction") = ... | REF.GET_DESC typeidx | REF.TEST reftype | REF.CAST reftype + | REF.CAST_DESC_EQ reftype | ... syntax instr/func hint(desc "function reference instruction") = ... @@ -448,6 +451,10 @@ def $free_instr(BR_ON_CAST labelidx reftype_1 reftype_2) = $free_labelidx(labelidx) ++ $free_reftype(reftype_1) ++ $free_reftype(reftype_2) def $free_instr(BR_ON_CAST_FAIL labelidx reftype_1 reftype_2) = $free_labelidx(labelidx) ++ $free_reftype(reftype_1) ++ $free_reftype(reftype_2) +def $free_instr(BR_ON_CAST_DESC_EQ labelidx reftype_1 reftype_2) = + $free_labelidx(labelidx) ++ $free_reftype(reftype_1) ++ $free_reftype(reftype_2) +def $free_instr(BR_ON_CAST_DESC_EQ_FAIL labelidx reftype_1 reftype_2) = + $free_labelidx(labelidx) ++ $free_reftype(reftype_1) ++ $free_reftype(reftype_2) def $free_instr(CALL funcidx) = $free_funcidx(funcidx) def $free_instr(CALL_REF typeuse) = $free_typeuse(typeuse) @@ -501,6 +508,7 @@ def $free_instr(REF.AS_NON_NULL) = {} def $free_instr(REF.EQ) = {} def $free_instr(REF.TEST reftype) = $free_reftype(reftype) def $free_instr(REF.CAST reftype) = $free_reftype(reftype) +def $free_instr(REF.CAST_DESC_EQ reftype) = $free_reftype(reftype) def $free_instr(REF.FUNC funcidx) = $free_funcidx(funcidx) def $free_instr(REF.I31) = {} diff --git a/specification/wasm-latest/2.3-validation.instructions.spectec b/specification/wasm-latest/2.3-validation.instructions.spectec index bb380f13b..3bfb63578 100644 --- a/specification/wasm-latest/2.3-validation.instructions.spectec +++ b/specification/wasm-latest/2.3-validation.instructions.spectec @@ -115,6 +115,28 @@ rule Instr_ok/br_on_cast_fail: -- Reftype_sub: C |- rt_2 <: rt_3 -- Reftype_sub: C |- $diffrt(rt_1, rt_2) <: rt +rule Instr_ok/br_on_cast_desc_eq: + C |- BR_ON_CAST_DESC_EQ l rt_1 (REF null? (_HT exact? _IDX x)) : t* rt_1 (REF NULL (_HT exact? _IDX y)) -> t* ($diffrt(rt_1, (REF null? (_HT exact? _IDX x)))) + -- if C.LABELS[l] = t* rt + -- ExpandDesc: C.TYPES[x] ~~ describestype? (DESCRIPTOR (_IDX y)) ct + -- Reftype_ok: C |- rt_1 : OK + -- Reftype_ok: C |- rt_3 : OK + ---- + -- Reftype_sub: C |- rt_1 <: rt_3 + -- Reftype_sub: C |- (REF null? (_HT exact? _IDX x)) <: rt_3 + -- Reftype_sub: C |- (REF null? (_HT exact? _IDX x)) <: rt + +rule Instr_ok/br_on_cast_desc_eq_fail: + C |- BR_ON_CAST_DESC_EQ_FAIL l rt_1 (REF null? (_HT exact? _IDX x)) : t* rt_1 (REF NULL (_HT exact? _IDX y)) -> t* (REF null? (_HT exact? _IDX x)) + -- if C.LABELS[l] = t* rt + -- ExpandDesc: C.TYPES[x] ~~ describestype? (DESCRIPTOR (_IDX y)) ct + -- Reftype_ok: C |- rt_1 : OK + -- Reftype_ok: C |- rt_3 : OK + ---- + -- Reftype_sub: C |- rt_1 <: rt_3 + -- Reftype_sub: C |- (REF null? (_HT exact? _IDX x)) <: rt_3 + -- Reftype_sub: C |- $diffrt(rt_1, (REF null? (_HT exact? _IDX x))) <: rt + ;; Function instructions @@ -246,6 +268,12 @@ rule Instr_ok/ref.cast: -- Reftype_ok: C |- rt' : OK -- Reftype_sub: C |- rt <: rt' +rule Instr_ok/ref.cast_desc_eq: + C |- REF.CAST_DESC_EQ (REF null? (_HT exact? _IDX x)) : (REF NULL ht) (REF NULL (_HT exact? _IDX y)) -> (REF null? (_HT exact? _IDX x)) + -- Heaptype_ok: C |- ht : OK + -- ExpandDesc: C.TYPES[x] ~~ describestype? (DESCRIPTOR (_IDX y)) ct + -- Heaptype_sub: C |- (_HT exact? _IDX x) <: ht + ;; Scalar reference instructions diff --git a/spectec/test-frontend/TEST.md b/spectec/test-frontend/TEST.md index 59c39e951..574a07d3f 100644 --- a/spectec/test-frontend/TEST.md +++ b/spectec/test-frontend/TEST.md @@ -2128,6 +2128,8 @@ syntax instr = | BR_ON_NON_NULL{labelidx : labelidx}(labelidx : labelidx) | BR_ON_CAST{labelidx : labelidx, reftype : reftype}(labelidx : labelidx, reftype : reftype, reftype) | BR_ON_CAST_FAIL{labelidx : labelidx, reftype : reftype}(labelidx : labelidx, reftype : reftype, reftype) + | BR_ON_CAST_DESC_EQ{labelidx : labelidx, reftype : reftype}(labelidx : labelidx, reftype : reftype, reftype) + | BR_ON_CAST_DESC_EQ_FAIL{labelidx : labelidx, reftype : reftype}(labelidx : labelidx, reftype : reftype, reftype) | CALL{funcidx : funcidx}(funcidx : funcidx) | CALL_REF{typeuse : typeuse}(typeuse : typeuse) | CALL_INDIRECT{tableidx : tableidx, typeuse : typeuse}(tableidx : tableidx, typeuse : typeuse) @@ -2170,6 +2172,7 @@ syntax instr = | REF.GET_DESC{typeidx : typeidx}(typeidx : typeidx) | REF.TEST{reftype : reftype}(reftype : reftype) | REF.CAST{reftype : reftype}(reftype : reftype) + | REF.CAST_DESC_EQ{reftype : reftype}(reftype : reftype) | REF.FUNC{funcidx : funcidx}(funcidx : funcidx) | REF.I31 | I31.GET{sx : sx}(sx : sx) @@ -2267,227 +2270,233 @@ def $free_blocktype(blocktype : blocktype) : free ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec rec { -;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:575.1-575.44 +;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:583.1-583.44 def $shift_labelidxs(labelidx*) : labelidx* - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:576.1-576.32 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:584.1-584.32 def $shift_labelidxs([]) = [] - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:577.1-577.66 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:585.1-585.66 def $shift_labelidxs{`labelidx'*` : labelidx*}([`%`_labelidx(0)] ++ labelidx'*{labelidx' <- `labelidx'*`}) = $shift_labelidxs(labelidx'*{labelidx' <- `labelidx'*`}) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:578.1-578.91 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:586.1-586.91 def $shift_labelidxs{labelidx : labelidx, `labelidx'*` : labelidx*}([labelidx] ++ labelidx'*{labelidx' <- `labelidx'*`}) = [`%`_labelidx((((labelidx!`%`_labelidx.0 : nat <:> int) - (1 : nat <:> int)) : int <:> nat))] ++ $shift_labelidxs(labelidx'*{labelidx' <- `labelidx'*`}) } ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec rec { -;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:420.1-420.30 +;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:423.1-423.30 def $free_instr(instr : instr) : free - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:431.1-431.26 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:434.1-434.26 def $free_instr(NOP_instr) = {TYPES [], FUNCS [], GLOBALS [], TABLES [], MEMS [], ELEMS [], DATAS [], LOCALS [], LABELS []} - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:432.1-432.34 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:435.1-435.34 def $free_instr(UNREACHABLE_instr) = {TYPES [], FUNCS [], GLOBALS [], TABLES [], MEMS [], ELEMS [], DATAS [], LOCALS [], LABELS []} - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:433.1-433.27 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:436.1-436.27 def $free_instr(DROP_instr) = {TYPES [], FUNCS [], GLOBALS [], TABLES [], MEMS [], ELEMS [], DATAS [], LOCALS [], LABELS []} - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:434.1-434.86 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:437.1-437.86 def $free_instr{`valtype*?` : valtype*?}(SELECT_instr(valtype*{valtype <- `valtype*`}?{`valtype*` <- `valtype*?`})) = $free_opt($free_list($free_valtype(valtype)*{valtype <- `valtype*`})?{`valtype*` <- `valtype*?`}) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:436.1-436.92 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:439.1-439.92 def $free_instr{blocktype : blocktype, `instr*` : instr*}(BLOCK_instr(blocktype, instr*{instr <- `instr*`})) = $free_blocktype(blocktype) +++ $free_block(instr*{instr <- `instr*`}) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:437.1-437.91 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:440.1-440.91 def $free_instr{blocktype : blocktype, `instr*` : instr*}(LOOP_instr(blocktype, instr*{instr <- `instr*`})) = $free_blocktype(blocktype) +++ $free_block(instr*{instr <- `instr*`}) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:438.1-439.79 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:441.1-442.79 def $free_instr{blocktype : blocktype, `instr_1*` : instr*, `instr_2*` : instr*}(`IF%%ELSE%`_instr(blocktype, instr_1*{instr_1 <- `instr_1*`}, instr_2*{instr_2 <- `instr_2*`})) = $free_blocktype(blocktype) +++ $free_block(instr_1*{instr_1 <- `instr_1*`}) +++ $free_block(instr_2*{instr_2 <- `instr_2*`}) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:441.1-441.56 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:444.1-444.56 def $free_instr{labelidx : labelidx}(BR_instr(labelidx)) = $free_labelidx(labelidx) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:442.1-442.59 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:445.1-445.59 def $free_instr{labelidx : labelidx}(BR_IF_instr(labelidx)) = $free_labelidx(labelidx) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:443.1-444.69 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:446.1-447.69 def $free_instr{`labelidx*` : labelidx*, labelidx' : labelidx}(BR_TABLE_instr(labelidx*{labelidx <- `labelidx*`}, labelidx')) = $free_list($free_labelidx(labelidx)*{labelidx <- `labelidx*`}) +++ $free_labelidx(labelidx') - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:445.1-445.64 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:448.1-448.64 def $free_instr{labelidx : labelidx}(BR_ON_NULL_instr(labelidx)) = $free_labelidx(labelidx) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:446.1-446.68 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:449.1-449.68 def $free_instr{labelidx : labelidx}(BR_ON_NON_NULL_instr(labelidx)) = $free_labelidx(labelidx) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:447.1-448.83 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:450.1-451.83 def $free_instr{labelidx : labelidx, reftype_1 : reftype, reftype_2 : reftype}(BR_ON_CAST_instr(labelidx, reftype_1, reftype_2)) = $free_labelidx(labelidx) +++ $free_reftype(reftype_1) +++ $free_reftype(reftype_2) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:449.1-450.83 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:452.1-453.83 def $free_instr{labelidx : labelidx, reftype_1 : reftype, reftype_2 : reftype}(BR_ON_CAST_FAIL_instr(labelidx, reftype_1, reftype_2)) = $free_labelidx(labelidx) +++ $free_reftype(reftype_1) +++ $free_reftype(reftype_2) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:452.1-452.55 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:454.1-455.83 + def $free_instr{labelidx : labelidx, reftype_1 : reftype, reftype_2 : reftype}(BR_ON_CAST_DESC_EQ_instr(labelidx, reftype_1, reftype_2)) = $free_labelidx(labelidx) +++ $free_reftype(reftype_1) +++ $free_reftype(reftype_2) + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:456.1-457.83 + def $free_instr{labelidx : labelidx, reftype_1 : reftype, reftype_2 : reftype}(BR_ON_CAST_DESC_EQ_FAIL_instr(labelidx, reftype_1, reftype_2)) = $free_labelidx(labelidx) +++ $free_reftype(reftype_1) +++ $free_reftype(reftype_2) + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:459.1-459.55 def $free_instr{funcidx : funcidx}(CALL_instr(funcidx)) = $free_funcidx(funcidx) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:453.1-453.59 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:460.1-460.59 def $free_instr{typeuse : typeuse}(CALL_REF_instr(typeuse)) = $free_typeuse(typeuse) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:454.1-455.53 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:461.1-462.53 def $free_instr{tableidx : tableidx, typeuse : typeuse}(CALL_INDIRECT_instr(tableidx, typeuse)) = $free_tableidx(tableidx) +++ $free_typeuse(typeuse) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:456.1-456.29 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:463.1-463.29 def $free_instr(RETURN_instr) = {TYPES [], FUNCS [], GLOBALS [], TABLES [], MEMS [], ELEMS [], DATAS [], LOCALS [], LABELS []} - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:457.1-457.62 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:464.1-464.62 def $free_instr{funcidx : funcidx}(RETURN_CALL_instr(funcidx)) = $free_funcidx(funcidx) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:458.1-458.66 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:465.1-465.66 def $free_instr{typeuse : typeuse}(RETURN_CALL_REF_instr(typeuse)) = $free_typeuse(typeuse) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:459.1-460.53 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:466.1-467.53 def $free_instr{tableidx : tableidx, typeuse : typeuse}(RETURN_CALL_INDIRECT_instr(tableidx, typeuse)) = $free_tableidx(tableidx) +++ $free_typeuse(typeuse) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:462.1-462.63 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:469.1-469.63 def $free_instr{numtype : numtype, numlit : num_(numtype)}(CONST_instr(numtype, numlit)) = $free_numtype(numtype) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:463.1-463.60 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:470.1-470.60 def $free_instr{numtype : numtype, unop : unop_(numtype)}(UNOP_instr(numtype, unop)) = $free_numtype(numtype) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:464.1-464.62 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:471.1-471.62 def $free_instr{numtype : numtype, binop : binop_(numtype)}(BINOP_instr(numtype, binop)) = $free_numtype(numtype) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:465.1-465.64 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:472.1-472.64 def $free_instr{numtype : numtype, testop : testop_(numtype)}(TESTOP_instr(numtype, testop)) = $free_numtype(numtype) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:466.1-466.62 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:473.1-473.62 def $free_instr{numtype : numtype, relop : relop_(numtype)}(RELOP_instr(numtype, relop)) = $free_numtype(numtype) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:467.1-468.55 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:474.1-475.55 def $free_instr{numtype_1 : numtype, numtype_2 : numtype, cvtop : cvtop__(numtype_2, numtype_1)}(CVTOP_instr(numtype_1, numtype_2, cvtop)) = $free_numtype(numtype_1) +++ $free_numtype(numtype_2) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:470.1-470.64 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:477.1-477.64 def $free_instr{vectype : vectype, veclit : vec_(vectype)}(VCONST_instr(vectype, veclit)) = $free_vectype(vectype) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:471.1-471.64 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:478.1-478.64 def $free_instr{vectype : vectype, vvunop : vvunop}(VVUNOP_instr(vectype, vvunop)) = $free_vectype(vectype) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:472.1-472.66 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:479.1-479.66 def $free_instr{vectype : vectype, vvbinop : vvbinop}(VVBINOP_instr(vectype, vvbinop)) = $free_vectype(vectype) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:473.1-473.68 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:480.1-480.68 def $free_instr{vectype : vectype, vvternop : vvternop}(VVTERNOP_instr(vectype, vvternop)) = $free_vectype(vectype) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:474.1-474.68 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:481.1-481.68 def $free_instr{vectype : vectype, vvtestop : vvtestop}(VVTESTOP_instr(vectype, vvtestop)) = $free_vectype(vectype) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:475.1-475.56 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:482.1-482.56 def $free_instr{shape : shape, vunop : vunop_(shape)}(VUNOP_instr(shape, vunop)) = $free_shape(shape) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:476.1-476.58 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:483.1-483.58 def $free_instr{shape : shape, vbinop : vbinop_(shape)}(VBINOP_instr(shape, vbinop)) = $free_shape(shape) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:477.1-477.60 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:484.1-484.60 def $free_instr{shape : shape, vternop : vternop_(shape)}(VTERNOP_instr(shape, vternop)) = $free_shape(shape) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:478.1-478.60 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:485.1-485.60 def $free_instr{shape : shape, vtestop : vtestop_(shape)}(VTESTOP_instr(shape, vtestop)) = $free_shape(shape) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:479.1-479.58 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:486.1-486.58 def $free_instr{shape : shape, vrelop : vrelop_(shape)}(VRELOP_instr(shape, vrelop)) = $free_shape(shape) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:480.1-480.64 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:487.1-487.64 def $free_instr{ishape : ishape, vshiftop : vshiftop_(ishape)}(VSHIFTOP_instr(ishape, vshiftop)) = $free_shape(ishape!`%`_ishape.0) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:481.1-481.55 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:488.1-488.55 def $free_instr{ishape : ishape}(VBITMASK_instr(ishape)) = $free_shape(ishape!`%`_ishape.0) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:482.1-482.66 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:489.1-489.66 def $free_instr{bshape : bshape, vswizzlop : vswizzlop_(bshape)}(VSWIZZLOP_instr(bshape, vswizzlop)) = $free_shape(bshape!`%`_bshape.0) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:483.1-483.64 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:490.1-490.64 def $free_instr{bshape : bshape, `laneidx*` : laneidx*}(VSHUFFLE_instr(bshape, laneidx*{laneidx <- `laneidx*`})) = $free_shape(bshape!`%`_bshape.0) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:484.1-485.49 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:491.1-492.49 def $free_instr{ishape_1 : ishape, ishape_2 : ishape, vextunop : vextunop__(ishape_2, ishape_1)}(VEXTUNOP_instr(ishape_1, ishape_2, vextunop)) = $free_shape(ishape_1!`%`_ishape.0) +++ $free_shape(ishape_2!`%`_ishape.0) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:486.1-487.49 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:493.1-494.49 def $free_instr{ishape_1 : ishape, ishape_2 : ishape, vextbinop : vextbinop__(ishape_2, ishape_1)}(VEXTBINOP_instr(ishape_1, ishape_2, vextbinop)) = $free_shape(ishape_1!`%`_ishape.0) +++ $free_shape(ishape_2!`%`_ishape.0) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:488.1-489.49 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:495.1-496.49 def $free_instr{ishape_1 : ishape, ishape_2 : ishape, vextternop : vextternop__(ishape_2, ishape_1)}(VEXTTERNOP_instr(ishape_1, ishape_2, vextternop)) = $free_shape(ishape_1!`%`_ishape.0) +++ $free_shape(ishape_2!`%`_ishape.0) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:490.1-491.49 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:497.1-498.49 def $free_instr{ishape_1 : ishape, ishape_2 : ishape, sx : sx}(VNARROW_instr(ishape_1, ishape_2, sx)) = $free_shape(ishape_1!`%`_ishape.0) +++ $free_shape(ishape_2!`%`_ishape.0) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:492.1-493.47 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:499.1-500.47 def $free_instr{shape_1 : shape, shape_2 : shape, vcvtop : vcvtop__(shape_2, shape_1)}(VCVTOP_instr(shape_1, shape_2, vcvtop)) = $free_shape(shape_1) +++ $free_shape(shape_2) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:494.1-494.51 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:501.1-501.51 def $free_instr{shape : shape}(VSPLAT_instr(shape)) = $free_shape(shape) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:495.1-495.70 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:502.1-502.70 def $free_instr{shape : shape, `sx?` : sx?, laneidx : laneidx}(VEXTRACT_LANE_instr(shape, sx?{sx <- `sx?`}, laneidx)) = $free_shape(shape) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:496.1-496.66 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:503.1-503.66 def $free_instr{shape : shape, laneidx : laneidx}(VREPLACE_LANE_instr(shape, laneidx)) = $free_shape(shape) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:498.1-498.62 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:505.1-505.62 def $free_instr{heaptype : heaptype}(REF.NULL_instr(heaptype)) = $free_heaptype(heaptype) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:499.1-499.34 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:506.1-506.34 def $free_instr(REF.IS_NULL_instr) = {TYPES [], FUNCS [], GLOBALS [], TABLES [], MEMS [], ELEMS [], DATAS [], LOCALS [], LABELS []} - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:500.1-500.38 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:507.1-507.38 def $free_instr(REF.AS_NON_NULL_instr) = {TYPES [], FUNCS [], GLOBALS [], TABLES [], MEMS [], ELEMS [], DATAS [], LOCALS [], LABELS []} - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:501.1-501.29 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:508.1-508.29 def $free_instr(REF.EQ_instr) = {TYPES [], FUNCS [], GLOBALS [], TABLES [], MEMS [], ELEMS [], DATAS [], LOCALS [], LABELS []} - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:502.1-502.59 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:509.1-509.59 def $free_instr{reftype : reftype}(REF.TEST_instr(reftype)) = $free_reftype(reftype) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:503.1-503.59 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:510.1-510.59 def $free_instr{reftype : reftype}(REF.CAST_instr(reftype)) = $free_reftype(reftype) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:504.1-504.59 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:511.1-511.67 + def $free_instr{reftype : reftype}(REF.CAST_DESC_EQ_instr(reftype)) = $free_reftype(reftype) + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:512.1-512.59 def $free_instr{funcidx : funcidx}(REF.FUNC_instr(funcidx)) = $free_funcidx(funcidx) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:505.1-505.30 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:513.1-513.30 def $free_instr(REF.I31_instr) = {TYPES [], FUNCS [], GLOBALS [], TABLES [], MEMS [], ELEMS [], DATAS [], LOCALS [], LABELS []} - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:507.1-507.33 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:515.1-515.33 def $free_instr{sx : sx}(I31.GET_instr(sx)) = {TYPES [], FUNCS [], GLOBALS [], TABLES [], MEMS [], ELEMS [], DATAS [], LOCALS [], LABELS []} - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:509.1-509.41 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:517.1-517.41 def $free_instr{typeidx : typeidx}(STRUCT.NEW_instr(typeidx)) = {TYPES [], FUNCS [], GLOBALS [], TABLES [], MEMS [], ELEMS [], DATAS [], LOCALS [], LABELS []} - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:510.1-510.69 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:518.1-518.69 def $free_instr{typeidx : typeidx}(STRUCT.NEW_DEFAULT_instr(typeidx)) = $free_typeidx(typeidx) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:511.1-511.69 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:519.1-519.69 def $free_instr{`sx?` : sx?, typeidx : typeidx, u32 : u32}(STRUCT.GET_instr(sx?{sx <- `sx?`}, typeidx, u32)) = $free_typeidx(typeidx) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:512.1-512.65 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:520.1-520.65 def $free_instr{typeidx : typeidx, u32 : u32}(STRUCT.SET_instr(typeidx, u32)) = $free_typeidx(typeidx) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:514.1-514.60 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:522.1-522.60 def $free_instr{typeidx : typeidx}(ARRAY.NEW_instr(typeidx)) = $free_typeidx(typeidx) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:515.1-515.68 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:523.1-523.68 def $free_instr{typeidx : typeidx}(ARRAY.NEW_DEFAULT_instr(typeidx)) = $free_typeidx(typeidx) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:516.1-516.70 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:524.1-524.70 def $free_instr{typeidx : typeidx, u32 : u32}(ARRAY.NEW_FIXED_instr(typeidx, u32)) = $free_typeidx(typeidx) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:517.1-518.51 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:525.1-526.51 def $free_instr{typeidx : typeidx, dataidx : dataidx}(ARRAY.NEW_DATA_instr(typeidx, dataidx)) = $free_typeidx(typeidx) +++ $free_dataidx(dataidx) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:519.1-520.51 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:527.1-528.51 def $free_instr{typeidx : typeidx, elemidx : elemidx}(ARRAY.NEW_ELEM_instr(typeidx, elemidx)) = $free_typeidx(typeidx) +++ $free_elemidx(elemidx) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:521.1-521.64 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:529.1-529.64 def $free_instr{`sx?` : sx?, typeidx : typeidx}(ARRAY.GET_instr(sx?{sx <- `sx?`}, typeidx)) = $free_typeidx(typeidx) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:522.1-522.60 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:530.1-530.60 def $free_instr{typeidx : typeidx}(ARRAY.SET_instr(typeidx)) = $free_typeidx(typeidx) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:523.1-523.32 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:531.1-531.32 def $free_instr(ARRAY.LEN_instr) = {TYPES [], FUNCS [], GLOBALS [], TABLES [], MEMS [], ELEMS [], DATAS [], LOCALS [], LABELS []} - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:524.1-524.61 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:532.1-532.61 def $free_instr{typeidx : typeidx}(ARRAY.FILL_instr(typeidx)) = $free_typeidx(typeidx) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:525.1-526.55 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:533.1-534.55 def $free_instr{typeidx_1 : typeidx, typeidx_2 : typeidx}(ARRAY.COPY_instr(typeidx_1, typeidx_2)) = $free_typeidx(typeidx_1) +++ $free_typeidx(typeidx_2) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:527.1-528.51 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:535.1-536.51 def $free_instr{typeidx : typeidx, dataidx : dataidx}(ARRAY.INIT_DATA_instr(typeidx, dataidx)) = $free_typeidx(typeidx) +++ $free_dataidx(dataidx) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:529.1-530.51 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:537.1-538.51 def $free_instr{typeidx : typeidx, elemidx : elemidx}(ARRAY.INIT_ELEM_instr(typeidx, elemidx)) = $free_typeidx(typeidx) +++ $free_elemidx(elemidx) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:532.1-532.41 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:540.1-540.41 def $free_instr(EXTERN.CONVERT_ANY_instr) = {TYPES [], FUNCS [], GLOBALS [], TABLES [], MEMS [], ELEMS [], DATAS [], LOCALS [], LABELS []} - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:533.1-533.41 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:541.1-541.41 def $free_instr(ANY.CONVERT_EXTERN_instr) = {TYPES [], FUNCS [], GLOBALS [], TABLES [], MEMS [], ELEMS [], DATAS [], LOCALS [], LABELS []} - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:535.1-535.63 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:543.1-543.63 def $free_instr{localidx : localidx}(LOCAL.GET_instr(localidx)) = $free_localidx(localidx) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:536.1-536.63 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:544.1-544.63 def $free_instr{localidx : localidx}(LOCAL.SET_instr(localidx)) = $free_localidx(localidx) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:537.1-537.63 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:545.1-545.63 def $free_instr{localidx : localidx}(LOCAL.TEE_instr(localidx)) = $free_localidx(localidx) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:539.1-539.67 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:547.1-547.67 def $free_instr{globalidx : globalidx}(GLOBAL.GET_instr(globalidx)) = $free_globalidx(globalidx) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:540.1-540.67 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:548.1-548.67 def $free_instr{globalidx : globalidx}(GLOBAL.SET_instr(globalidx)) = $free_globalidx(globalidx) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:542.1-542.63 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:550.1-550.63 def $free_instr{tableidx : tableidx}(TABLE.GET_instr(tableidx)) = $free_tableidx(tableidx) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:543.1-543.63 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:551.1-551.63 def $free_instr{tableidx : tableidx}(TABLE.SET_instr(tableidx)) = $free_tableidx(tableidx) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:544.1-544.64 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:552.1-552.64 def $free_instr{tableidx : tableidx}(TABLE.SIZE_instr(tableidx)) = $free_tableidx(tableidx) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:545.1-545.64 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:553.1-553.64 def $free_instr{tableidx : tableidx}(TABLE.GROW_instr(tableidx)) = $free_tableidx(tableidx) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:546.1-546.64 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:554.1-554.64 def $free_instr{tableidx : tableidx}(TABLE.FILL_instr(tableidx)) = $free_tableidx(tableidx) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:547.1-548.59 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:555.1-556.59 def $free_instr{tableidx_1 : tableidx, tableidx_2 : tableidx}(TABLE.COPY_instr(tableidx_1, tableidx_2)) = $free_tableidx(tableidx_1) +++ $free_tableidx(tableidx_2) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:549.1-550.53 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:557.1-558.53 def $free_instr{tableidx : tableidx, elemidx : elemidx}(TABLE.INIT_instr(tableidx, elemidx)) = $free_tableidx(tableidx) +++ $free_elemidx(elemidx) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:551.1-551.60 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:559.1-559.60 def $free_instr{elemidx : elemidx}(ELEM.DROP_instr(elemidx)) = $free_elemidx(elemidx) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:553.1-554.49 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:561.1-562.49 def $free_instr{numtype : numtype, `loadop?` : loadop_(numtype)?, memidx : memidx, memarg : memarg}(LOAD_instr(numtype, loadop?{loadop <- `loadop?`}, memidx, memarg)) = $free_numtype(numtype) +++ $free_memidx(memidx) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:555.1-556.49 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:563.1-564.49 def $free_instr{numtype : numtype, `storeop?` : storeop_(numtype)?, memidx : memidx, memarg : memarg}(STORE_instr(numtype, storeop?{storeop <- `storeop?`}, memidx, memarg)) = $free_numtype(numtype) +++ $free_memidx(memidx) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:557.1-558.49 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:565.1-566.49 def $free_instr{vectype : vectype, `vloadop?` : vloadop_(vectype)?, memidx : memidx, memarg : memarg}(VLOAD_instr(vectype, vloadop?{vloadop <- `vloadop?`}, memidx, memarg)) = $free_vectype(vectype) +++ $free_memidx(memidx) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:559.1-560.49 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:567.1-568.49 def $free_instr{vectype : vectype, sz : sz, memidx : memidx, memarg : memarg, laneidx : laneidx}(VLOAD_LANE_instr(vectype, sz, memidx, memarg, laneidx)) = $free_vectype(vectype) +++ $free_memidx(memidx) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:561.1-562.49 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:569.1-570.49 def $free_instr{vectype : vectype, memidx : memidx, memarg : memarg}(VSTORE_instr(vectype, memidx, memarg)) = $free_vectype(vectype) +++ $free_memidx(memidx) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:563.1-564.49 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:571.1-572.49 def $free_instr{vectype : vectype, sz : sz, memidx : memidx, memarg : memarg, laneidx : laneidx}(VSTORE_LANE_instr(vectype, sz, memidx, memarg, laneidx)) = $free_vectype(vectype) +++ $free_memidx(memidx) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:565.1-565.59 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:573.1-573.59 def $free_instr{memidx : memidx}(MEMORY.SIZE_instr(memidx)) = $free_memidx(memidx) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:566.1-566.59 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:574.1-574.59 def $free_instr{memidx : memidx}(MEMORY.GROW_instr(memidx)) = $free_memidx(memidx) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:567.1-567.59 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:575.1-575.59 def $free_instr{memidx : memidx}(MEMORY.FILL_instr(memidx)) = $free_memidx(memidx) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:568.1-569.51 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:576.1-577.51 def $free_instr{memidx_1 : memidx, memidx_2 : memidx}(MEMORY.COPY_instr(memidx_1, memidx_2)) = $free_memidx(memidx_1) +++ $free_memidx(memidx_2) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:570.1-571.49 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:578.1-579.49 def $free_instr{memidx : memidx, dataidx : dataidx}(MEMORY.INIT_instr(memidx, dataidx)) = $free_memidx(memidx) +++ $free_dataidx(dataidx) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:572.1-572.60 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:580.1-580.60 def $free_instr{dataidx : dataidx}(DATA.DROP_instr(dataidx)) = $free_dataidx(dataidx) -;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:421.1-421.31 +;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:424.1-424.31 def $free_block(instr*) : free - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:580.1-581.47 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:588.1-589.47 def $free_block{`instr*` : instr*, free : free}(instr*{instr <- `instr*`}) = free[LABELS_free = $shift_labelidxs(free.LABELS_free)] -- if (free = $free_list($free_instr(instr)*{instr <- `instr*`})) } @@ -3526,31 +3535,53 @@ 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-124.37 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:118.1-127.61 + rule br_on_cast_desc_eq{C : context, l : labelidx, rt_1 : reftype, `null?` : null?, `exact?` : exact?, x : idx, `t*` : valtype*, y : idx, rt : reftype, `describestype?` : describestype?, ct : comptype, rt_3 : reftype}: + `%|-%:%`(C, BR_ON_CAST_DESC_EQ_instr(l, rt_1, REF_reftype(null?{null <- `null?`}, _HT_heaptype(exact?{exact <- `exact?`}, _IDX_typeuse(x)))), `%->_%%`_instrtype(`%`_resulttype(t*{t <- `t*`} ++ [(rt_1 : reftype <: valtype) REF_valtype(?(NULL_null), _HT_heaptype(exact?{exact <- `exact?`}, _IDX_typeuse(y)))]), [], `%`_resulttype(t*{t <- `t*`} ++ [($diffrt(rt_1, REF_reftype(null?{null <- `null?`}, _HT_heaptype(exact?{exact <- `exact?`}, _IDX_typeuse(x)))) : reftype <: valtype)]))) + -- if (C.LABELS_context[l!`%`_labelidx.0] = `%`_resulttype(t*{t <- `t*`} ++ [(rt : reftype <: valtype)])) + -- ExpandDesc: `%~~%`(C.TYPES_context[x!`%`_idx.0], `%%%`_desctype(describestype?{describestype <- `describestype?`}, ?(DESCRIPTOR_descriptortype(_IDX_typeuse(y))), ct)) + -- Reftype_ok: `%|-%:OK`(C, rt_1) + -- Reftype_ok: `%|-%:OK`(C, rt_3) + -- Reftype_sub: `%|-%<:%`(C, rt_1, rt_3) + -- Reftype_sub: `%|-%<:%`(C, REF_reftype(null?{null <- `null?`}, _HT_heaptype(exact?{exact <- `exact?`}, _IDX_typeuse(x))), rt_3) + -- Reftype_sub: `%|-%<:%`(C, REF_reftype(null?{null <- `null?`}, _HT_heaptype(exact?{exact <- `exact?`}, _IDX_typeuse(x))), rt) + + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:129.1-138.76 + rule br_on_cast_desc_eq_fail{C : context, l : labelidx, rt_1 : reftype, `null?` : null?, `exact?` : exact?, x : idx, `t*` : valtype*, y : idx, rt : reftype, `describestype?` : describestype?, ct : comptype, rt_3 : reftype}: + `%|-%:%`(C, BR_ON_CAST_DESC_EQ_FAIL_instr(l, rt_1, REF_reftype(null?{null <- `null?`}, _HT_heaptype(exact?{exact <- `exact?`}, _IDX_typeuse(x)))), `%->_%%`_instrtype(`%`_resulttype(t*{t <- `t*`} ++ [(rt_1 : reftype <: valtype) REF_valtype(?(NULL_null), _HT_heaptype(exact?{exact <- `exact?`}, _IDX_typeuse(y)))]), [], `%`_resulttype(t*{t <- `t*`} ++ [REF_valtype(null?{null <- `null?`}, _HT_heaptype(exact?{exact <- `exact?`}, _IDX_typeuse(x)))]))) + -- if (C.LABELS_context[l!`%`_labelidx.0] = `%`_resulttype(t*{t <- `t*`} ++ [(rt : reftype <: valtype)])) + -- ExpandDesc: `%~~%`(C.TYPES_context[x!`%`_idx.0], `%%%`_desctype(describestype?{describestype <- `describestype?`}, ?(DESCRIPTOR_descriptortype(_IDX_typeuse(y))), ct)) + -- Reftype_ok: `%|-%:OK`(C, rt_1) + -- Reftype_ok: `%|-%:OK`(C, rt_3) + -- Reftype_sub: `%|-%<:%`(C, rt_1, rt_3) + -- Reftype_sub: `%|-%<:%`(C, REF_reftype(null?{null <- `null?`}, _HT_heaptype(exact?{exact <- `exact?`}, _IDX_typeuse(x))), rt_3) + -- Reftype_sub: `%|-%<:%`(C, $diffrt(rt_1, REF_reftype(null?{null <- `null?`}, _HT_heaptype(exact?{exact <- `exact?`}, _IDX_typeuse(x)))), rt) + + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:143.1-146.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*`}))) -- 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:126.1-128.45 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:148.1-150.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:130.1-134.45 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:152.1-156.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:136.1-139.42 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:158.1-161.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:142.1-148.42 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:164.1-170.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*`}))) -- if (C.FUNCS_context[x!`%`_idx.0] = _HT_heaptype(exact?{exact <- `exact?`}, (dt : deftype <: typeuse))) @@ -3559,7 +3590,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:151.1-156.42 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:173.1-178.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*`}))) @@ -3567,7 +3598,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:159.1-167.42 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:181.1-189.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)) @@ -3577,495 +3608,502 @@ 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:174.1-177.42 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:196.1-199.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:179.1-181.42 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:201.1-203.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:183.1-187.34 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:205.1-209.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:210.1-212.31 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:232.1-234.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:214.1-217.20 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:236.1-239.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:219.1-220.34 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:241.1-242.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:222.1-224.31 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:244.1-246.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:226.1-228.31 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:248.1-250.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:230.1-231.51 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:252.1-253.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:233.1-235.71 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:255.1-257.71 rule ref.get_desc{C : context, x : idx, `exact?` : exact?, y : idx, `describestype?` : describestype?, ct : comptype}: `%|-%:%`(C, REF.GET_DESC_instr(x), `%->_%%`_instrtype(`%`_resulttype([REF_valtype(?(NULL_null), _HT_heaptype(exact?{exact <- `exact?`}, _IDX_typeuse(x)))]), [], `%`_resulttype([REF_valtype(?(), _HT_heaptype(exact?{exact <- `exact?`}, _IDX_typeuse(y)))]))) -- ExpandDesc: `%~~%`(C.TYPES_context[x!`%`_idx.0], `%%%`_desctype(describestype?{describestype <- `describestype?`}, ?(DESCRIPTOR_descriptortype(_IDX_typeuse(y))), ct)) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:237.1-241.33 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:259.1-263.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:243.1-247.33 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:265.1-269.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:252.1-253.42 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:271.1-275.50 + rule ref.cast_desc_eq{C : context, `null?` : null?, `exact?` : exact?, x : idx, ht : heaptype, y : idx, `describestype?` : describestype?, ct : comptype}: + `%|-%:%`(C, REF.CAST_DESC_EQ_instr(REF_reftype(null?{null <- `null?`}, _HT_heaptype(exact?{exact <- `exact?`}, _IDX_typeuse(x)))), `%->_%%`_instrtype(`%`_resulttype([REF_valtype(?(NULL_null), ht) REF_valtype(?(NULL_null), _HT_heaptype(exact?{exact <- `exact?`}, _IDX_typeuse(y)))]), [], `%`_resulttype([REF_valtype(null?{null <- `null?`}, _HT_heaptype(exact?{exact <- `exact?`}, _IDX_typeuse(x)))]))) + -- Heaptype_ok: `%|-%:OK`(C, ht) + -- ExpandDesc: `%~~%`(C.TYPES_context[x!`%`_idx.0], `%%%`_desctype(describestype?{describestype <- `describestype?`}, ?(DESCRIPTOR_descriptortype(_IDX_typeuse(y))), ct)) + -- Heaptype_sub: `%|-%<:%`(C, _HT_heaptype(exact?{exact <- `exact?`}, _IDX_typeuse(x)), ht) + + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:280.1-281.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:258.1-260.68 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:286.1-288.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(?(EXACT_exact), _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:262.1-265.48 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:290.1-293.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(?(EXACT_exact), _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:267.1-269.88 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:295.1-297.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:271.1-274.48 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:299.1-302.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:279.1-283.41 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:307.1-311.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:285.1-288.24 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:313.1-316.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:293.1-295.43 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:321.1-323.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(?(EXACT_exact), _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:297.1-300.45 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:325.1-328.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(?(EXACT_exact), _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:302.1-304.43 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:330.1-332.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(?(EXACT_exact), _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:306.1-309.40 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:334.1-337.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(?(EXACT_exact), _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:311.1-315.24 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:339.1-343.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(?(EXACT_exact), _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:317.1-320.39 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:345.1-348.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:322.1-324.42 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:350.1-352.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:326.1-327.43 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:354.1-355.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:329.1-331.42 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:357.1-359.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:333.1-337.40 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:361.1-365.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:339.1-342.44 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:367.1-370.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:344.1-348.24 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:372.1-376.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:353.1-355.26 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:381.1-383.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:357.1-359.26 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:385.1-387.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:364.1-366.28 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:392.1-394.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:368.1-370.29 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:396.1-398.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:372.1-374.29 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:400.1-402.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:379.1-381.30 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:407.1-409.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:383.1-385.29 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:411.1-413.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:390.1-392.32 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:418.1-420.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:394.1-396.32 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:422.1-424.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:398.1-400.32 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:426.1-428.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:402.1-404.32 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:430.1-432.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:406.1-408.32 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:434.1-436.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:410.1-414.36 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:438.1-442.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:416.1-420.36 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:444.1-448.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:422.1-424.24 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:450.1-452.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:437.1-439.32 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:465.1-467.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:441.1-443.32 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:469.1-471.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:445.1-447.32 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:473.1-475.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:449.1-452.38 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:477.1-480.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:454.1-457.24 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:482.1-485.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:459.1-461.24 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:487.1-489.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:472.1-475.44 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:500.1-503.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:477.1-480.36 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:505.1-508.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:491.1-494.44 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:519.1-522.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:496.1-499.36 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:524.1-527.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:501.1-504.47 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:529.1-532.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:506.1-509.41 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:534.1-537.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:511.1-514.36 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:539.1-542.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:516.1-519.36 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:544.1-547.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:521.1-525.21 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:549.1-553.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:527.1-530.47 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:555.1-558.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:532.1-536.21 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:560.1-564.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:541.1-542.33 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:569.1-570.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:544.1-545.34 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:572.1-573.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:547.1-548.39 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:575.1-576.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:550.1-551.39 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:578.1-579.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:553.1-554.40 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:581.1-582.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:556.1-557.44 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:584.1-585.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:562.1-563.35 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:590.1-591.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:565.1-566.41 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:593.1-594.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:568.1-569.48 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:596.1-597.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:571.1-572.55 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:599.1-600.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:574.1-575.44 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:602.1-603.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:577.1-578.37 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:605.1-606.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:580.1-581.44 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:608.1-609.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:583.1-584.51 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:611.1-612.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:586.1-587.40 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:614.1-615.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:589.1-590.44 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:617.1-618.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:592.1-593.47 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:620.1-621.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:595.1-596.33 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:623.1-624.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:598.1-599.50 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:626.1-627.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:601.1-603.29 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:629.1-631.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:605.1-606.44 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:633.1-634.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:608.1-610.21 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:636.1-638.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:612.1-614.21 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:640.1-642.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:616.1-617.50 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:644.1-645.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:619.1-620.57 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:647.1-648.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:622.1-623.64 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:650.1-651.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:625.1-626.48 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:653.1-654.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:628.1-629.46 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:656.1-657.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:634.1-635.24 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:662.1-663.24 rule empty{C : context}: `%|-%:%`(C, [], `%->_%%`_instrtype(`%`_resulttype([]), [], `%`_resulttype([]))) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:638.1-642.82 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:666.1-670.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:644.1-648.33 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:672.1-676.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:651.1-654.33 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:679.1-682.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*`})))