Skip to content

[spec] Fix instr sequence typing rules to actually be composable #2197

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
rossberg merged 2 commits into from
Jun 23, 2026
Merged

[spec] Fix instr sequence typing rules to actually be composable #2197

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
7fe9619
[spec] Fix instr sequence typing rules to actually be composable
rossberg Jun 23, 2026
f2b8e6b
Fix variable name
rossberg Jun 23, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
18 changes: 12 additions & 6 deletions document/core/valid/instructions.rst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1358,22 +1358,28 @@ $${rule-prose: Instrs_ok}

$${rule: Instrs_ok/empty}

$${rule: Instrs_ok/instr}

$${rule: Instrs_ok/seq}

$${rule: {Instrs_ok/sub Instrs_ok/frame}}
$${rule: Instrs_ok/sub}

.. note::
In combination with the previous rule,
subsumption allows to compose instructions whose types would not directly fit otherwise.
This *subsumption rule* allows to weaken the type of an instruction sequence to a supertype,
which includes the ability to drop init variables ${:x*} from the instruction type in a context where they are not needed, for example, at the end of the body of a :ref:`block <valid-block>`.

$${rule: Instrs_ok/frame}

.. note::
In combination with the previous two rules,
this *frame rule* allows to compose instructions whose types would not directly fit otherwise.
For example, consider the instruction sequence

$${instr*: (CONST I32 1) (CONST I32 2) (BINOP I32 ADD)}

To type this sequence, its subsequence ${instr*: (CONST I32 2) (BINOP I32 ADD)} needs to be valid with an intermediate type.
But the direct type of ${instr: (CONST I32 2)} is ${instrtype: eps -> I32}, not matching the two inputs expected by ${instr: $($(BINOP I32 ADD))}.
The subsumption rule allows to weaken the type of ${instr: (CONST I32 2)} to the supertype ${instrtype: I32 -> I32 I32}, such that it can be composed with ${instr: $($(BINOP I32 ADD))} and yields the intermediate type ${instrtype: I32 -> I32 I32} for the subsequence. That can in turn be composed with the first constant.

Furthermore, subsumption allows to drop init variables ${:x*} from the instruction type in a context where they are not needed, for example, at the end of the body of a :ref:`block <valid-block>`.
The rule allows to weaken the type of ${instr: (CONST I32 2)} to the supertype ${instrtype: I32 -> I32 I32}, such that it can be composed with ${instr: $($(BINOP I32 ADD))} and yields the intermediate type ${instrtype: I32 -> I32 I32} for the subsequence. That can in turn be composed with the first constant.


.. index:: expression, result type
Expand Down
8 changes: 6 additions & 2 deletions specification/wasm-1.0/6-typing.spectec
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -134,9 +134,13 @@ rule Expr_ok:
rule Instrs_ok/empty:
C |- eps : eps -> eps

rule Instrs_ok/instr:
C |- instr : t_1* -> t_2*
-- Instr_ok: C |- instr : t_1* -> t_2*

@raoxiaojia raoxiaojia Jun 23, 2026

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Oh, I am amazed that this can be correctly parsed by the backends, as at first glance it really looks like a self-referential rule; but actually it says instr_ok C instr : t1* -> ts2* constructs instrs_ok C [instr].

@rossberg rossberg Jun 23, 2026

Copy link
Copy Markdown
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Well, the frontend does the resolution. There is nothing specific to do in the after elaboration.

@raoxiaojia raoxiaojia Jun 23, 2026

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Then I'll praise the frontend to have handled this cleanly!


rule Instrs_ok/seq:
C |- instr_1 instr_2* : t_1* -> t_3*
-- Instr_ok: C |- instr_1 : t_1* -> t_2*
C |- instr_1* instr_2* : t_1* -> t_3*
-- Instrs_ok: C |- instr_1* : t_1* -> t_2*

@raoxiaojia raoxiaojia Jun 23, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Hmm, this formulation will allow derivations of arbitrary lengths now, since either instruction list can be empty. I thought it would be better to preserve the original cons form of the rule and leave the general list append as a lemma (not too difficult to prove). Or did I overlook anything here?

Same for the 2.0/3.0 changes below.

-- Instrs_ok: C |- instr_2* : t_2* -> t_3*

rule Instrs_ok/frame:
Expand Down
8 changes: 6 additions & 2 deletions specification/wasm-2.0/6-typing.spectec
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -151,9 +151,13 @@ rule Expr_ok:
rule Instrs_ok/empty:
C |- eps : eps -> eps

rule Instrs_ok/instr:
C |- instr : t_1* -> t_2*
-- Instr_ok: C |- instr : t_1* -> t_2*

rule Instrs_ok/seq:
C |- instr_1 instr_2* : t_1* -> t_3*
-- Instr_ok: C |- instr_1 : t_1* -> t_2*
C |- instr_1* instr_2* : t_1* -> t_3*
-- Instrs_ok: C |- instr_1* : t_1* -> t_2*
-- Instrs_ok: C |- instr_2* : t_2* -> t_3*

rule Instrs_ok/sub:
Expand Down
8 changes: 6 additions & 2 deletions specification/wasm-3.0/2.3-validation.instructions.spectec
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -613,10 +613,14 @@ rule Instr_ok/vcvtop:
rule Instrs_ok/empty:
C |- eps : eps -> eps

rule Instrs_ok/instr:
C |- instr : t_1* ->_(x*) t_2*
-- Instr_ok: C |- instr : t_1* ->_(x*) t_2*

;; TODO(3, rossberg): enable x_1*#x_2* to avoid space
rule Instrs_ok/seq:
C |- instr_1 instr_2* : t_1* ->_(x_1* x_2*) t_3*
-- Instr_ok: C |- instr_1 : t_1* ->_(x_1*) t_2*
C |- instr_1* instr_2* : t_1* ->_(x_1* x_2*) t_3*
-- Instrs_ok: C |- instr_1* : t_1* ->_(x_1*) t_2*
-- (if C.LOCALS[x_1] = init t)*
-- Instrs_ok: $with_locals(C, x_1*, (SET t)*) |- instr_2* : t_2* ->_(x_2*) t_3*

Expand Down
8 changes: 6 additions & 2 deletions specification/wasm-latest/2.3-validation.instructions.spectec
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -613,10 +613,14 @@ rule Instr_ok/vcvtop:
rule Instrs_ok/empty:
C |- eps : eps -> eps

rule Instrs_ok/instr:
C |- instr : t_1* ->_(x*) t_2*
-- Instr_ok: C |- instr : t_1* ->_(x*) t_2*

;; TODO(3, rossberg): enable x_1*#x_2* to avoid space
rule Instrs_ok/seq:
C |- instr_1 instr_2* : t_1* ->_(x_1* x_2*) t_3*
-- Instr_ok: C |- instr_1 : t_1* ->_(x_1*) t_2*
C |- instr_1* instr_2* : t_1* ->_(x_1* x_2*) t_3*
-- Instrs_ok: C |- instr_1* : t_1* ->_(x_1*) t_2*
-- (if C.LOCALS[x_1] = init t)*
-- Instrs_ok: $with_locals(C, x_1*, (SET t)*) |- instr_2* : t_2* ->_(x_2*) t_3*

Expand Down
17 changes: 11 additions & 6 deletions spectec/test-frontend/TEST.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4463,21 +4463,26 @@ relation Instrs_ok: `%|-%:%`(context, instr*, instrtype)
rule empty{C : context}:
`%|-%:%`(C, [], `%->_%%`_instrtype(`%`_resulttype([],), [], `%`_resulttype([],)))

;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:617.1-621.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*`},)))
;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:616.1-618.46
rule instr{C : context, instr : instr, `t_1*` : valtype*, `x*` : idx*, `t_2*` : valtype*}:
`%|-%:%`(C, [instr], `%->_%%`_instrtype(`%`_resulttype(t_1*{t_1 <- `t_1*`},), x*{x <- `x*`}, `%`_resulttype(t_2*{t_2 <- `t_2*`},)))
-- Instr_ok: `%|-%:%`(C, instr, `%->_%%`_instrtype(`%`_resulttype(t_1*{t_1 <- `t_1*`},), x*{x <- `x*`}, `%`_resulttype(t_2*{t_2 <- `t_2*`},)))

;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:621.1-625.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_1 <- `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*`},)))
-- Instrs_ok: `%|-%:%`(C, instr_1*{instr_1 <- `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:623.1-627.33
;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:627.1-631.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:630.1-633.33
;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:634.1-637.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*`},)))
Expand Down
15 changes: 13 additions & 2 deletions spectec/test-latex/TEST.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7332,13 +7332,24 @@ $$
$$
\begin{array}{@{}c@{}}\displaystyle
\frac{
C \vdash {\mathit{instr}}_1 : {t_1^\ast} \rightarrow_{{x_1^\ast}} {t_2^\ast}
C \vdash {\mathit{instr}} : {t_1^\ast} \rightarrow_{{x^\ast}} {t_2^\ast}
}{
C \vdash {\mathit{instr}} : {t_1^\ast} \rightarrow_{{x^\ast}} {t_2^\ast}
} \, {[\textsc{\scriptsize T{-}instr*{-}instr}]}
\qquad
\end{array}
$$

$$
\begin{array}{@{}c@{}}\displaystyle
\frac{
C \vdash {{\mathit{instr}}_1^\ast} : {t_1^\ast} \rightarrow_{{x_1^\ast}} {t_2^\ast}
\qquad
(C{.}\mathsf{locals}{}[x_1] = {\mathit{init}}~t)^\ast
\qquad
C{}[{.}\mathsf{local}{}[{x_1^\ast}] = {(\mathsf{set}~t)^\ast}] \vdash {{\mathit{instr}}_2^\ast} : {t_2^\ast} \rightarrow_{{x_2^\ast}} {t_3^\ast}
}{
C \vdash {\mathit{instr}}_1~{{\mathit{instr}}_2^\ast} : {t_1^\ast} \rightarrow_{{x_1^\ast}~{x_2^\ast}} {t_3^\ast}
C \vdash {{\mathit{instr}}_1^\ast}~{{\mathit{instr}}_2^\ast} : {t_1^\ast} \rightarrow_{{x_1^\ast}~{x_2^\ast}} {t_3^\ast}
} \, {[\textsc{\scriptsize T{-}instr*{-}seq}]}
\qquad
\end{array}
Expand Down
51 changes: 33 additions & 18 deletions spectec/test-middlend/TEST.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3986,21 +3986,26 @@ relation Instrs_ok: `%|-%:%`(context, instr*, instrtype)
rule empty{C : context}:
`%|-%:%`(C, [], `%->_%%`_instrtype(`%`_resulttype([],), [], `%`_resulttype([],)))

;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:617.1-621.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*`},)))
;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:616.1-618.46
rule instr{C : context, instr : instr, `t_1*` : valtype*, `x*` : idx*, `t_2*` : valtype*}:
`%|-%:%`(C, [instr], `%->_%%`_instrtype(`%`_resulttype(t_1*{t_1 <- `t_1*`},), x*{x <- `x*`}, `%`_resulttype(t_2*{t_2 <- `t_2*`},)))
-- Instr_ok: `%|-%:%`(C, instr, `%->_%%`_instrtype(`%`_resulttype(t_1*{t_1 <- `t_1*`},), x*{x <- `x*`}, `%`_resulttype(t_2*{t_2 <- `t_2*`},)))

;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:621.1-625.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_1 <- `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*`},)))
-- Instrs_ok: `%|-%:%`(C, instr_1*{instr_1 <- `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:623.1-627.33
;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:627.1-631.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:630.1-633.33
;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:634.1-637.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*`},)))
Expand Down Expand Up @@ -15853,21 +15858,26 @@ relation Instrs_ok: `%|-%:%`(context, instr*, instrtype)
rule empty{C : context}:
`%|-%:%`(C, [], `%->_%%`_instrtype(`%`_resulttype([],), [], `%`_resulttype([],)))

;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:617.1-621.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*`},)))
;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:616.1-618.46
rule instr{C : context, instr : instr, `t_1*` : valtype*, `x*` : idx*, `t_2*` : valtype*}:
`%|-%:%`(C, [instr], `%->_%%`_instrtype(`%`_resulttype(t_1*{t_1 <- `t_1*`},), x*{x <- `x*`}, `%`_resulttype(t_2*{t_2 <- `t_2*`},)))
-- Instr_ok: `%|-%:%`(C, instr, `%->_%%`_instrtype(`%`_resulttype(t_1*{t_1 <- `t_1*`},), x*{x <- `x*`}, `%`_resulttype(t_2*{t_2 <- `t_2*`},)))

;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:621.1-625.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_1 <- `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*`},)))
-- Instrs_ok: `%|-%:%`(C, instr_1*{instr_1 <- `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:623.1-627.33
;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:627.1-631.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:630.1-633.33
;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:634.1-637.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*`},)))
Expand Down Expand Up @@ -27826,24 +27836,29 @@ relation Instrs_ok: `%|-%:%`(context, instr*, instrtype)
rule empty{C : context}:
`%|-%:%`(C, [], `%->_%%`_instrtype(`%`_resulttype([],), [], `%`_resulttype([],)))

;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:617.1-621.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*`},)))
;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:616.1-618.46
rule instr{C : context, instr : instr, `t_1*` : valtype*, `x*` : idx*, `t_2*` : valtype*}:
`%|-%:%`(C, [instr], `%->_%%`_instrtype(`%`_resulttype(t_1*{t_1 <- `t_1*`},), x*{x <- `x*`}, `%`_resulttype(t_2*{t_2 <- `t_2*`},)))
-- Instr_ok: `%|-%:%`(C, instr, `%->_%%`_instrtype(`%`_resulttype(t_1*{t_1 <- `t_1*`},), x*{x <- `x*`}, `%`_resulttype(t_2*{t_2 <- `t_2*`},)))

;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:621.1-625.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_1 <- `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*`},)))
-- Instrs_ok: `%|-%:%`(C, instr_1*{instr_1 <- `instr_1*`}, `%->_%%`_instrtype(`%`_resulttype(t_1*{t_1 <- `t_1*`},), x_1*{x_1 <- `x_1*`}, `%`_resulttype(t_2*{t_2 <- `t_2*`},)))
-- if (|`init*`| = |`t*`|)
-- if (|`init*`| = |`x_1*`|)
-- (if (x_1!`%`_idx.0 < |C.LOCALS_context|))*{x_1 <- `x_1*`}
-- (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:623.1-627.33
;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:627.1-631.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:630.1-633.33
;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:634.1-637.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*`},)))
Expand Down
Loading
Loading