diff --git a/document/core/syntax/instructions.rst b/document/core/syntax/instructions.rst index 7a93f1d59..516e02a67 100644 --- a/document/core/syntax/instructions.rst +++ b/document/core/syntax/instructions.rst @@ -231,6 +231,7 @@ The ${:DATA.DROP} instruction prevents further use of a passive data segment. Th .. _syntax-ref.is_null: .. _syntax-ref.as_non_null: .. _syntax-ref.eq: +.. _syntax-ref.get_desc: .. _syntax-ref.test: .. _syntax-ref.cast: .. _syntax-instr-ref: @@ -247,7 +248,9 @@ The ${:REF.NULL} and ${:REF.FUNC} instructions produce a :ref:`null ` to a non-null one, and :ref:`traps ` if it encounters null. -The ${:REF.EQ} compares two references. +The instruction ${:REF.EQ} compares two references. + +The instruction ${:REF.GET_DESC} gets the :ref:`descriptor ` of an allocated value. 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, diff --git a/document/core/util/macros.def b/document/core/util/macros.def index bc05c7829..c4b0ccabb 100644 --- a/document/core/util/macros.def +++ b/document/core/util/macros.def @@ -549,6 +549,7 @@ .. |REFISNULL| mathdef:: \xref{syntax/instructions}{syntax-instr-ref}{\K{ref{.}is\_null}} .. |REFASNONNULL| mathdef:: \xref{syntax/instructions}{syntax-instr-ref}{\K{ref{.}as\_non\_null}} .. |REFEQ| mathdef:: \xref{syntax/instructions}{syntax-instr-ref}{\K{ref{.}eq}} +.. |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}} diff --git a/document/core/valid/instructions.rst b/document/core/valid/instructions.rst index c49fc727a..7dc05b840 100644 --- a/document/core/valid/instructions.rst +++ b/document/core/valid/instructions.rst @@ -803,6 +803,16 @@ $${rule-prose: Instr_ok/ref.eq} $${rule: Instr_ok/ref.eq} +.. _valid-ref.get_desc: + +:math:`\REFGETDESC~x` +..................... + +$${rule-prose: Instr_ok/ref.get_desc} + +$${rule: Instr_ok/ref.get_desc} + + .. _valid-ref.test: :math:`\REFTEST~\X{rt}` diff --git a/specification/wasm-latest/1.3-syntax.instructions.spectec b/specification/wasm-latest/1.3-syntax.instructions.spectec index 6228dce91..3a586db75 100644 --- a/specification/wasm-latest/1.3-syntax.instructions.spectec +++ b/specification/wasm-latest/1.3-syntax.instructions.spectec @@ -306,6 +306,7 @@ syntax instr/ref hint(desc "reference instruction") = ... | REF.IS_NULL | REF.AS_NON_NULL | REF.EQ + | REF.GET_DESC typeidx | REF.TEST reftype | REF.CAST reftype | ... diff --git a/specification/wasm-latest/2.3-validation.instructions.spectec b/specification/wasm-latest/2.3-validation.instructions.spectec index 317ca50b3..bb380f13b 100644 --- a/specification/wasm-latest/2.3-validation.instructions.spectec +++ b/specification/wasm-latest/2.3-validation.instructions.spectec @@ -230,6 +230,10 @@ rule Instr_ok/ref.as_non_null: rule Instr_ok/ref.eq: C |- REF.EQ : (REF NULL EQ) (REF NULL EQ) -> I32 +rule Instr_ok/ref.get_desc: + C |- REF.GET_DESC x : (REF NULL (_HT exact? _IDX x)) -> (REF (_HT exact? _IDX y)) + -- ExpandDesc: C.TYPES[x] ~~ describestype? (DESCRIPTOR (_IDX y)) ct + rule Instr_ok/ref.test: C |- REF.TEST rt : rt' -> I32 -- Reftype_ok: C |- rt : OK diff --git a/spectec/test-frontend/TEST.md b/spectec/test-frontend/TEST.md index c06e6b333..59c39e951 100644 --- a/spectec/test-frontend/TEST.md +++ b/spectec/test-frontend/TEST.md @@ -2167,6 +2167,7 @@ syntax instr = | REF.IS_NULL | REF.AS_NON_NULL | REF.EQ + | REF.GET_DESC{typeidx : typeidx}(typeidx : typeidx) | REF.TEST{reftype : reftype}(reftype : reftype) | REF.CAST{reftype : reftype}(reftype : reftype) | REF.FUNC{funcidx : funcidx}(funcidx : funcidx) @@ -2266,227 +2267,227 @@ def $free_blocktype(blocktype : blocktype) : free ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec rec { -;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:574.1-574.44 +;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:575.1-575.44 def $shift_labelidxs(labelidx*) : labelidx* - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:575.1-575.32 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:576.1-576.32 def $shift_labelidxs([]) = [] - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:576.1-576.66 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:577.1-577.66 def $shift_labelidxs{`labelidx'*` : labelidx*}([`%`_labelidx(0)] ++ labelidx'*{labelidx' <- `labelidx'*`}) = $shift_labelidxs(labelidx'*{labelidx' <- `labelidx'*`}) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:577.1-577.91 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:578.1-578.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:419.1-419.30 +;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:420.1-420.30 def $free_instr(instr : instr) : free - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:430.1-430.26 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:431.1-431.26 def $free_instr(NOP_instr) = {TYPES [], FUNCS [], GLOBALS [], TABLES [], MEMS [], ELEMS [], DATAS [], LOCALS [], LABELS []} - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:431.1-431.34 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:432.1-432.34 def $free_instr(UNREACHABLE_instr) = {TYPES [], FUNCS [], GLOBALS [], TABLES [], MEMS [], ELEMS [], DATAS [], LOCALS [], LABELS []} - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:432.1-432.27 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:433.1-433.27 def $free_instr(DROP_instr) = {TYPES [], FUNCS [], GLOBALS [], TABLES [], MEMS [], ELEMS [], DATAS [], LOCALS [], LABELS []} - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:433.1-433.86 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:434.1-434.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:435.1-435.92 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:436.1-436.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:436.1-436.91 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:437.1-437.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:437.1-438.79 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:438.1-439.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:440.1-440.56 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:441.1-441.56 def $free_instr{labelidx : labelidx}(BR_instr(labelidx)) = $free_labelidx(labelidx) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:441.1-441.59 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:442.1-442.59 def $free_instr{labelidx : labelidx}(BR_IF_instr(labelidx)) = $free_labelidx(labelidx) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:442.1-443.69 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:443.1-444.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:444.1-444.64 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:445.1-445.64 def $free_instr{labelidx : labelidx}(BR_ON_NULL_instr(labelidx)) = $free_labelidx(labelidx) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:445.1-445.68 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:446.1-446.68 def $free_instr{labelidx : labelidx}(BR_ON_NON_NULL_instr(labelidx)) = $free_labelidx(labelidx) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:446.1-447.83 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:447.1-448.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:448.1-449.83 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:449.1-450.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:451.1-451.55 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:452.1-452.55 def $free_instr{funcidx : funcidx}(CALL_instr(funcidx)) = $free_funcidx(funcidx) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:452.1-452.59 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:453.1-453.59 def $free_instr{typeuse : typeuse}(CALL_REF_instr(typeuse)) = $free_typeuse(typeuse) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:453.1-454.53 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:454.1-455.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:455.1-455.29 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:456.1-456.29 def $free_instr(RETURN_instr) = {TYPES [], FUNCS [], GLOBALS [], TABLES [], MEMS [], ELEMS [], DATAS [], LOCALS [], LABELS []} - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:456.1-456.62 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:457.1-457.62 def $free_instr{funcidx : funcidx}(RETURN_CALL_instr(funcidx)) = $free_funcidx(funcidx) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:457.1-457.66 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:458.1-458.66 def $free_instr{typeuse : typeuse}(RETURN_CALL_REF_instr(typeuse)) = $free_typeuse(typeuse) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:458.1-459.53 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:459.1-460.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:461.1-461.63 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:462.1-462.63 def $free_instr{numtype : numtype, numlit : num_(numtype)}(CONST_instr(numtype, numlit)) = $free_numtype(numtype) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:462.1-462.60 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:463.1-463.60 def $free_instr{numtype : numtype, unop : unop_(numtype)}(UNOP_instr(numtype, unop)) = $free_numtype(numtype) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:463.1-463.62 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:464.1-464.62 def $free_instr{numtype : numtype, binop : binop_(numtype)}(BINOP_instr(numtype, binop)) = $free_numtype(numtype) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:464.1-464.64 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:465.1-465.64 def $free_instr{numtype : numtype, testop : testop_(numtype)}(TESTOP_instr(numtype, testop)) = $free_numtype(numtype) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:465.1-465.62 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:466.1-466.62 def $free_instr{numtype : numtype, relop : relop_(numtype)}(RELOP_instr(numtype, relop)) = $free_numtype(numtype) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:466.1-467.55 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:467.1-468.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:469.1-469.64 - def $free_instr{vectype : vectype, veclit : vec_(vectype)}(VCONST_instr(vectype, veclit)) = $free_vectype(vectype) ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:470.1-470.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 def $free_instr{vectype : vectype, vvunop : vvunop}(VVUNOP_instr(vectype, vvunop)) = $free_vectype(vectype) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:471.1-471.66 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:472.1-472.66 def $free_instr{vectype : vectype, vvbinop : vvbinop}(VVBINOP_instr(vectype, vvbinop)) = $free_vectype(vectype) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:472.1-472.68 - def $free_instr{vectype : vectype, vvternop : vvternop}(VVTERNOP_instr(vectype, vvternop)) = $free_vectype(vectype) ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:473.1-473.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 def $free_instr{vectype : vectype, vvtestop : vvtestop}(VVTESTOP_instr(vectype, vvtestop)) = $free_vectype(vectype) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:474.1-474.56 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:475.1-475.56 def $free_instr{shape : shape, vunop : vunop_(shape)}(VUNOP_instr(shape, vunop)) = $free_shape(shape) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:475.1-475.58 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:476.1-476.58 def $free_instr{shape : shape, vbinop : vbinop_(shape)}(VBINOP_instr(shape, vbinop)) = $free_shape(shape) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:476.1-476.60 - def $free_instr{shape : shape, vternop : vternop_(shape)}(VTERNOP_instr(shape, vternop)) = $free_shape(shape) ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:477.1-477.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 def $free_instr{shape : shape, vtestop : vtestop_(shape)}(VTESTOP_instr(shape, vtestop)) = $free_shape(shape) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:478.1-478.58 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:479.1-479.58 def $free_instr{shape : shape, vrelop : vrelop_(shape)}(VRELOP_instr(shape, vrelop)) = $free_shape(shape) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:479.1-479.64 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:480.1-480.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:480.1-480.55 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:481.1-481.55 def $free_instr{ishape : ishape}(VBITMASK_instr(ishape)) = $free_shape(ishape!`%`_ishape.0) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:481.1-481.66 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:482.1-482.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:482.1-482.64 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:483.1-483.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:483.1-484.49 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:484.1-485.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:485.1-486.49 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:486.1-487.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:487.1-488.49 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:488.1-489.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:489.1-490.49 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:490.1-491.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:491.1-492.47 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:492.1-493.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:493.1-493.51 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:494.1-494.51 def $free_instr{shape : shape}(VSPLAT_instr(shape)) = $free_shape(shape) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:494.1-494.70 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:495.1-495.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:495.1-495.66 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:496.1-496.66 def $free_instr{shape : shape, laneidx : laneidx}(VREPLACE_LANE_instr(shape, laneidx)) = $free_shape(shape) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:497.1-497.62 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:498.1-498.62 def $free_instr{heaptype : heaptype}(REF.NULL_instr(heaptype)) = $free_heaptype(heaptype) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:498.1-498.34 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:499.1-499.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:499.1-499.38 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:500.1-500.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:500.1-500.29 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:501.1-501.29 def $free_instr(REF.EQ_instr) = {TYPES [], FUNCS [], GLOBALS [], TABLES [], MEMS [], ELEMS [], DATAS [], LOCALS [], LABELS []} - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:501.1-501.59 - def $free_instr{reftype : reftype}(REF.TEST_instr(reftype)) = $free_reftype(reftype) ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:502.1-502.59 - def $free_instr{reftype : reftype}(REF.CAST_instr(reftype)) = $free_reftype(reftype) + def $free_instr{reftype : reftype}(REF.TEST_instr(reftype)) = $free_reftype(reftype) ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:503.1-503.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 def $free_instr{funcidx : funcidx}(REF.FUNC_instr(funcidx)) = $free_funcidx(funcidx) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:504.1-504.30 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:505.1-505.30 def $free_instr(REF.I31_instr) = {TYPES [], FUNCS [], GLOBALS [], TABLES [], MEMS [], ELEMS [], DATAS [], LOCALS [], LABELS []} - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:506.1-506.33 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:507.1-507.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:508.1-508.41 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:509.1-509.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:509.1-509.69 - def $free_instr{typeidx : typeidx}(STRUCT.NEW_DEFAULT_instr(typeidx)) = $free_typeidx(typeidx) ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:510.1-510.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 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:511.1-511.65 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:512.1-512.65 def $free_instr{typeidx : typeidx, u32 : u32}(STRUCT.SET_instr(typeidx, u32)) = $free_typeidx(typeidx) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:513.1-513.60 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:514.1-514.60 def $free_instr{typeidx : typeidx}(ARRAY.NEW_instr(typeidx)) = $free_typeidx(typeidx) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:514.1-514.68 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:515.1-515.68 def $free_instr{typeidx : typeidx}(ARRAY.NEW_DEFAULT_instr(typeidx)) = $free_typeidx(typeidx) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:515.1-515.70 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:516.1-516.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:516.1-517.51 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:517.1-518.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:518.1-519.51 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:519.1-520.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:520.1-520.64 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:521.1-521.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:521.1-521.60 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:522.1-522.60 def $free_instr{typeidx : typeidx}(ARRAY.SET_instr(typeidx)) = $free_typeidx(typeidx) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:522.1-522.32 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:523.1-523.32 def $free_instr(ARRAY.LEN_instr) = {TYPES [], FUNCS [], GLOBALS [], TABLES [], MEMS [], ELEMS [], DATAS [], LOCALS [], LABELS []} - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:523.1-523.61 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:524.1-524.61 def $free_instr{typeidx : typeidx}(ARRAY.FILL_instr(typeidx)) = $free_typeidx(typeidx) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:524.1-525.55 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:525.1-526.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:526.1-527.51 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:527.1-528.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:528.1-529.51 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:529.1-530.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:531.1-531.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:532.1-532.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 def $free_instr(ANY.CONVERT_EXTERN_instr) = {TYPES [], FUNCS [], GLOBALS [], TABLES [], MEMS [], ELEMS [], DATAS [], LOCALS [], LABELS []} - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:534.1-534.63 - def $free_instr{localidx : localidx}(LOCAL.GET_instr(localidx)) = $free_localidx(localidx) ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:535.1-535.63 - def $free_instr{localidx : localidx}(LOCAL.SET_instr(localidx)) = $free_localidx(localidx) + def $free_instr{localidx : localidx}(LOCAL.GET_instr(localidx)) = $free_localidx(localidx) ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:536.1-536.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 def $free_instr{localidx : localidx}(LOCAL.TEE_instr(localidx)) = $free_localidx(localidx) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:538.1-538.67 - def $free_instr{globalidx : globalidx}(GLOBAL.GET_instr(globalidx)) = $free_globalidx(globalidx) ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:539.1-539.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 def $free_instr{globalidx : globalidx}(GLOBAL.SET_instr(globalidx)) = $free_globalidx(globalidx) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:541.1-541.63 - def $free_instr{tableidx : tableidx}(TABLE.GET_instr(tableidx)) = $free_tableidx(tableidx) ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:542.1-542.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 def $free_instr{tableidx : tableidx}(TABLE.SET_instr(tableidx)) = $free_tableidx(tableidx) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:543.1-543.64 - def $free_instr{tableidx : tableidx}(TABLE.SIZE_instr(tableidx)) = $free_tableidx(tableidx) ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:544.1-544.64 - def $free_instr{tableidx : tableidx}(TABLE.GROW_instr(tableidx)) = $free_tableidx(tableidx) + def $free_instr{tableidx : tableidx}(TABLE.SIZE_instr(tableidx)) = $free_tableidx(tableidx) ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:545.1-545.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 def $free_instr{tableidx : tableidx}(TABLE.FILL_instr(tableidx)) = $free_tableidx(tableidx) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:546.1-547.59 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:547.1-548.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:548.1-549.53 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:549.1-550.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:550.1-550.60 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:551.1-551.60 def $free_instr{elemidx : elemidx}(ELEM.DROP_instr(elemidx)) = $free_elemidx(elemidx) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:552.1-553.49 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:553.1-554.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:554.1-555.49 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:555.1-556.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:556.1-557.49 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:557.1-558.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:558.1-559.49 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:559.1-560.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:560.1-561.49 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:561.1-562.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:562.1-563.49 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:563.1-564.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:564.1-564.59 - def $free_instr{memidx : memidx}(MEMORY.SIZE_instr(memidx)) = $free_memidx(memidx) ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:565.1-565.59 - def $free_instr{memidx : memidx}(MEMORY.GROW_instr(memidx)) = $free_memidx(memidx) + def $free_instr{memidx : memidx}(MEMORY.SIZE_instr(memidx)) = $free_memidx(memidx) ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:566.1-566.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 def $free_instr{memidx : memidx}(MEMORY.FILL_instr(memidx)) = $free_memidx(memidx) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:567.1-568.51 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:568.1-569.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:569.1-570.49 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:570.1-571.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:571.1-571.60 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:572.1-572.60 def $free_instr{dataidx : dataidx}(DATA.DROP_instr(dataidx)) = $free_dataidx(dataidx) -;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:420.1-420.31 +;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:421.1-421.31 def $free_block(instr*) : free - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:579.1-580.47 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:580.1-581.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*`})) } @@ -3623,443 +3624,448 @@ relation Instr_ok: `%|-%:%`(context, instr, instrtype) 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-237.33 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:233.1-235.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 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:239.1-243.33 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:243.1-247.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:248.1-249.42 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:252.1-253.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:254.1-256.68 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:258.1-260.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:258.1-261.48 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:262.1-265.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:263.1-265.88 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:267.1-269.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:267.1-270.48 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:271.1-274.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:275.1-279.41 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:279.1-283.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:281.1-284.24 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:285.1-288.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:289.1-291.43 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:293.1-295.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:293.1-296.45 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:297.1-300.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:298.1-300.43 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:302.1-304.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:302.1-305.40 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:306.1-309.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:307.1-311.24 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:311.1-315.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:313.1-316.39 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:317.1-320.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:318.1-320.42 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:322.1-324.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:322.1-323.43 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:326.1-327.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:325.1-327.42 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:329.1-331.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:329.1-333.40 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:333.1-337.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:335.1-338.44 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:339.1-342.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:340.1-344.24 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:344.1-348.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:349.1-351.26 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:353.1-355.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:353.1-355.26 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:357.1-359.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:360.1-362.28 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:364.1-366.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:364.1-366.29 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:368.1-370.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:368.1-370.29 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:372.1-374.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:375.1-377.30 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:379.1-381.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:379.1-381.29 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:383.1-385.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:386.1-388.32 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:390.1-392.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:390.1-392.32 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:394.1-396.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:394.1-396.32 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:398.1-400.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:398.1-400.32 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:402.1-404.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:402.1-404.32 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:406.1-408.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:406.1-410.36 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:410.1-414.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:412.1-416.36 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:416.1-420.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:418.1-420.24 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:422.1-424.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:433.1-435.32 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:437.1-439.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:437.1-439.32 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:441.1-443.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:441.1-443.32 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:445.1-447.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:445.1-448.38 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:449.1-452.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:450.1-453.24 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:454.1-457.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:455.1-457.24 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:459.1-461.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:468.1-471.44 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:472.1-475.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:473.1-476.36 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:477.1-480.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:487.1-490.44 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:491.1-494.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:492.1-495.36 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:496.1-499.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:497.1-500.47 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:501.1-504.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:502.1-505.41 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:506.1-509.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:507.1-510.36 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:511.1-514.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:512.1-515.36 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:516.1-519.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:517.1-521.21 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:521.1-525.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:523.1-526.47 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:527.1-530.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:528.1-532.21 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:532.1-536.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:537.1-538.33 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:541.1-542.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:540.1-541.34 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:544.1-545.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:543.1-544.39 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:547.1-548.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:546.1-547.39 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:550.1-551.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:549.1-550.40 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:553.1-554.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:552.1-553.44 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:556.1-557.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:558.1-559.35 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:562.1-563.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:561.1-562.41 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:565.1-566.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:564.1-565.48 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:568.1-569.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:567.1-568.55 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:571.1-572.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:570.1-571.44 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:574.1-575.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:573.1-574.37 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:577.1-578.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:576.1-577.44 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:580.1-581.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:579.1-580.51 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:583.1-584.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:582.1-583.40 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:586.1-587.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:585.1-586.44 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:589.1-590.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:588.1-589.47 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:592.1-593.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:591.1-592.33 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:595.1-596.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:594.1-595.50 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:598.1-599.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:597.1-599.29 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:601.1-603.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:601.1-602.44 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:605.1-606.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:604.1-606.21 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:608.1-610.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:608.1-610.21 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:612.1-614.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:612.1-613.50 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:616.1-617.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:615.1-616.57 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:619.1-620.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:618.1-619.64 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:622.1-623.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:621.1-622.48 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:625.1-626.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:624.1-625.46 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:628.1-629.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:630.1-631.24 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:634.1-635.24 rule empty{C : context}: `%|-%:%`(C, [], `%->_%%`_instrtype(`%`_resulttype([]), [], `%`_resulttype([]))) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:634.1-638.82 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:638.1-642.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:640.1-644.33 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:644.1-648.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:647.1-650.33 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:651.1-654.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*`})))