Skip to content

Commit bd4633a

Browse files
rossbergrossberg
authored
[spec] Fix instr sequence typing rules to actually be composable (#2197)
1 parent 9979256 commit bd4633a

10 files changed

Lines changed: 185 additions & 67 deletions

File tree

‎document/core/valid/instructions.rst‎

Lines changed: 12 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -1358,22 +1358,28 @@ $${rule-prose: Instrs_ok}
13581358

13591359
$${rule: Instrs_ok/empty}
13601360

1361+
$${rule: Instrs_ok/instr}
1362+
13611363
$${rule: Instrs_ok/seq}
13621364

1363-
$${rule: {Instrs_ok/sub Instrs_ok/frame}}
1365+
$${rule: Instrs_ok/sub}
13641366

13651367
.. note::
1366-
In combination with the previous rule,
1367-
subsumption allows to compose instructions whose types would not directly fit otherwise.
1368+
This *subsumption rule* allows to weaken the type of an instruction sequence to a supertype,
1369+
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>`.
1370+
1371+
$${rule: Instrs_ok/frame}
1372+
1373+
.. note::
1374+
In combination with the previous two rules,
1375+
this *frame rule* allows to compose instructions whose types would not directly fit otherwise.
13681376
For example, consider the instruction sequence
13691377

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

13721380
To type this sequence, its subsequence ${instr*: (CONST I32 2) (BINOP I32 ADD)} needs to be valid with an intermediate type.
13731381
But the direct type of ${instr: (CONST I32 2)} is ${instrtype: eps -> I32}, not matching the two inputs expected by ${instr: $($(BINOP I32 ADD))}.
1374-
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.
1375-
1376-
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>`.
1382+
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.
13771383

13781384

13791385
.. index:: expression, result type

‎specification/wasm-1.0/6-typing.spectec‎

Lines changed: 6 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -134,9 +134,13 @@ rule Expr_ok:
134134
rule Instrs_ok/empty:
135135
C |- eps : eps -> eps
136136

137+
rule Instrs_ok/instr:
138+
C |- instr : t_1* -> t_2*
139+
-- Instr_ok: C |- instr : t_1* -> t_2*
140+
137141
rule Instrs_ok/seq:
138-
C |- instr_1 instr_2* : t_1* -> t_3*
139-
-- Instr_ok: C |- instr_1 : t_1* -> t_2*
142+
C |- instr_1* instr_2* : t_1* -> t_3*
143+
-- Instrs_ok: C |- instr_1* : t_1* -> t_2*
140144
-- Instrs_ok: C |- instr_2* : t_2* -> t_3*
141145

142146
rule Instrs_ok/frame:

‎specification/wasm-2.0/6-typing.spectec‎

Lines changed: 6 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -151,9 +151,13 @@ rule Expr_ok:
151151
rule Instrs_ok/empty:
152152
C |- eps : eps -> eps
153153

154+
rule Instrs_ok/instr:
155+
C |- instr : t_1* -> t_2*
156+
-- Instr_ok: C |- instr : t_1* -> t_2*
157+
154158
rule Instrs_ok/seq:
155-
C |- instr_1 instr_2* : t_1* -> t_3*
156-
-- Instr_ok: C |- instr_1 : t_1* -> t_2*
159+
C |- instr_1* instr_2* : t_1* -> t_3*
160+
-- Instrs_ok: C |- instr_1* : t_1* -> t_2*
157161
-- Instrs_ok: C |- instr_2* : t_2* -> t_3*
158162

159163
rule Instrs_ok/sub:

‎specification/wasm-3.0/2.3-validation.instructions.spectec‎

Lines changed: 6 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -613,10 +613,14 @@ rule Instr_ok/vcvtop:
613613
rule Instrs_ok/empty:
614614
C |- eps : eps -> eps
615615

616+
rule Instrs_ok/instr:
617+
C |- instr : t_1* ->_(x*) t_2*
618+
-- Instr_ok: C |- instr : t_1* ->_(x*) t_2*
619+
616620
;; TODO(3, rossberg): enable x_1*#x_2* to avoid space
617621
rule Instrs_ok/seq:
618-
C |- instr_1 instr_2* : t_1* ->_(x_1* x_2*) t_3*
619-
-- Instr_ok: C |- instr_1 : t_1* ->_(x_1*) t_2*
622+
C |- instr_1* instr_2* : t_1* ->_(x_1* x_2*) t_3*
623+
-- Instrs_ok: C |- instr_1* : t_1* ->_(x_1*) t_2*
620624
-- (if C.LOCALS[x_1] = init t)*
621625
-- Instrs_ok: $with_locals(C, x_1*, (SET t)*) |- instr_2* : t_2* ->_(x_2*) t_3*
622626

‎specification/wasm-latest/2.3-validation.instructions.spectec‎

Lines changed: 6 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -613,10 +613,14 @@ rule Instr_ok/vcvtop:
613613
rule Instrs_ok/empty:
614614
C |- eps : eps -> eps
615615

616+
rule Instrs_ok/instr:
617+
C |- instr : t_1* ->_(x*) t_2*
618+
-- Instr_ok: C |- instr : t_1* ->_(x*) t_2*
619+
616620
;; TODO(3, rossberg): enable x_1*#x_2* to avoid space
617621
rule Instrs_ok/seq:
618-
C |- instr_1 instr_2* : t_1* ->_(x_1* x_2*) t_3*
619-
-- Instr_ok: C |- instr_1 : t_1* ->_(x_1*) t_2*
622+
C |- instr_1* instr_2* : t_1* ->_(x_1* x_2*) t_3*
623+
-- Instrs_ok: C |- instr_1* : t_1* ->_(x_1*) t_2*
620624
-- (if C.LOCALS[x_1] = init t)*
621625
-- Instrs_ok: $with_locals(C, x_1*, (SET t)*) |- instr_2* : t_2* ->_(x_2*) t_3*
622626

‎spectec/test-frontend/TEST.md‎

Lines changed: 11 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -4463,21 +4463,26 @@ relation Instrs_ok: `%|-%:%`(context, instr*, instrtype)
44634463
rule empty{C : context}:
44644464
`%|-%:%`(C, [], `%->_%%`_instrtype(`%`_resulttype([],), [], `%`_resulttype([],)))
44654465

4466-
;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:617.1-621.82
4467-
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*}:
4468-
`%|-%:%`(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*`},)))
4469-
-- 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*`},)))
4466+
;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:616.1-618.46
4467+
rule instr{C : context, instr : instr, `t_1*` : valtype*, `x*` : idx*, `t_2*` : valtype*}:
4468+
`%|-%:%`(C, [instr], `%->_%%`_instrtype(`%`_resulttype(t_1*{t_1 <- `t_1*`},), x*{x <- `x*`}, `%`_resulttype(t_2*{t_2 <- `t_2*`},)))
4469+
-- Instr_ok: `%|-%:%`(C, instr, `%->_%%`_instrtype(`%`_resulttype(t_1*{t_1 <- `t_1*`},), x*{x <- `x*`}, `%`_resulttype(t_2*{t_2 <- `t_2*`},)))
4470+
4471+
;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:621.1-625.82
4472+
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*}:
4473+
`%|-%:%`(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*`},)))
4474+
-- 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*`},)))
44704475
-- (if (C.LOCALS_context[x_1!`%`_idx.0] = `%%`_localtype(init, t)))*{init <- `init*`, t <- `t*`, x_1 <- `x_1*`}
44714476
-- 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*`},)))
44724477

4473-
;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:623.1-627.33
4478+
;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:627.1-631.33
44744479
rule sub{C : context, `instr*` : instr*, it' : instrtype, it : instrtype}:
44754480
`%|-%:%`(C, instr*{instr <- `instr*`}, it')
44764481
-- Instrs_ok: `%|-%:%`(C, instr*{instr <- `instr*`}, it)
44774482
-- Instrtype_sub: `%|-%<:%`(C, it, it')
44784483
-- Instrtype_ok: `%|-%:OK`(C, it')
44794484

4480-
;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:630.1-633.33
4485+
;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:634.1-637.33
44814486
rule frame{C : context, `instr*` : instr*, `t*` : valtype*, `t_1*` : valtype*, `x*` : idx*, `t_2*` : valtype*}:
44824487
`%|-%:%`(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*`},)))
44834488
-- Instrs_ok: `%|-%:%`(C, instr*{instr <- `instr*`}, `%->_%%`_instrtype(`%`_resulttype(t_1*{t_1 <- `t_1*`},), x*{x <- `x*`}, `%`_resulttype(t_2*{t_2 <- `t_2*`},)))

‎spectec/test-latex/TEST.md‎

Lines changed: 13 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -7332,13 +7332,24 @@ $$
73327332
$$
73337333
\begin{array}{@{}c@{}}\displaystyle
73347334
\frac{
7335-
C \vdash {\mathit{instr}}_1 : {t_1^\ast} \rightarrow_{{x_1^\ast}} {t_2^\ast}
7335+
C \vdash {\mathit{instr}} : {t_1^\ast} \rightarrow_{{x^\ast}} {t_2^\ast}
7336+
}{
7337+
C \vdash {\mathit{instr}} : {t_1^\ast} \rightarrow_{{x^\ast}} {t_2^\ast}
7338+
} \, {[\textsc{\scriptsize T{-}instr*{-}instr}]}
7339+
\qquad
7340+
\end{array}
7341+
$$
7342+
7343+
$$
7344+
\begin{array}{@{}c@{}}\displaystyle
7345+
\frac{
7346+
C \vdash {{\mathit{instr}}_1^\ast} : {t_1^\ast} \rightarrow_{{x_1^\ast}} {t_2^\ast}
73367347
\qquad
73377348
(C{.}\mathsf{locals}{}[x_1] = {\mathit{init}}~t)^\ast
73387349
\qquad
73397350
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}
73407351
}{
7341-
C \vdash {\mathit{instr}}_1~{{\mathit{instr}}_2^\ast} : {t_1^\ast} \rightarrow_{{x_1^\ast}~{x_2^\ast}} {t_3^\ast}
7352+
C \vdash {{\mathit{instr}}_1^\ast}~{{\mathit{instr}}_2^\ast} : {t_1^\ast} \rightarrow_{{x_1^\ast}~{x_2^\ast}} {t_3^\ast}
73427353
} \, {[\textsc{\scriptsize T{-}instr*{-}seq}]}
73437354
\qquad
73447355
\end{array}

‎spectec/test-middlend/TEST.md‎

Lines changed: 33 additions & 18 deletions
Original file line numberDiff line numberDiff line change
@@ -3986,21 +3986,26 @@ relation Instrs_ok: `%|-%:%`(context, instr*, instrtype)
39863986
rule empty{C : context}:
39873987
`%|-%:%`(C, [], `%->_%%`_instrtype(`%`_resulttype([],), [], `%`_resulttype([],)))
39883988

3989-
;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:617.1-621.82
3990-
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*}:
3991-
`%|-%:%`(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*`},)))
3992-
-- 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*`},)))
3989+
;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:616.1-618.46
3990+
rule instr{C : context, instr : instr, `t_1*` : valtype*, `x*` : idx*, `t_2*` : valtype*}:
3991+
`%|-%:%`(C, [instr], `%->_%%`_instrtype(`%`_resulttype(t_1*{t_1 <- `t_1*`},), x*{x <- `x*`}, `%`_resulttype(t_2*{t_2 <- `t_2*`},)))
3992+
-- Instr_ok: `%|-%:%`(C, instr, `%->_%%`_instrtype(`%`_resulttype(t_1*{t_1 <- `t_1*`},), x*{x <- `x*`}, `%`_resulttype(t_2*{t_2 <- `t_2*`},)))
3993+
3994+
;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:621.1-625.82
3995+
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*}:
3996+
`%|-%:%`(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*`},)))
3997+
-- 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*`},)))
39933998
-- (if (C.LOCALS_context[x_1!`%`_idx.0] = `%%`_localtype(init, t)))*{init <- `init*`, t <- `t*`, x_1 <- `x_1*`}
39943999
-- 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*`},)))
39954000

3996-
;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:623.1-627.33
4001+
;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:627.1-631.33
39974002
rule sub{C : context, `instr*` : instr*, it' : instrtype, it : instrtype}:
39984003
`%|-%:%`(C, instr*{instr <- `instr*`}, it')
39994004
-- Instrs_ok: `%|-%:%`(C, instr*{instr <- `instr*`}, it)
40004005
-- Instrtype_sub: `%|-%<:%`(C, it, it')
40014006
-- Instrtype_ok: `%|-%:OK`(C, it')
40024007

4003-
;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:630.1-633.33
4008+
;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:634.1-637.33
40044009
rule frame{C : context, `instr*` : instr*, `t*` : valtype*, `t_1*` : valtype*, `x*` : idx*, `t_2*` : valtype*}:
40054010
`%|-%:%`(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*`},)))
40064011
-- Instrs_ok: `%|-%:%`(C, instr*{instr <- `instr*`}, `%->_%%`_instrtype(`%`_resulttype(t_1*{t_1 <- `t_1*`},), x*{x <- `x*`}, `%`_resulttype(t_2*{t_2 <- `t_2*`},)))
@@ -15855,21 +15860,26 @@ relation Instrs_ok: `%|-%:%`(context, instr*, instrtype)
1585515860
rule empty{C : context}:
1585615861
`%|-%:%`(C, [], `%->_%%`_instrtype(`%`_resulttype([],), [], `%`_resulttype([],)))
1585715862

15858-
;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:617.1-621.82
15859-
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*}:
15860-
`%|-%:%`(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*`},)))
15861-
-- 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*`},)))
15863+
;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:616.1-618.46
15864+
rule instr{C : context, instr : instr, `t_1*` : valtype*, `x*` : idx*, `t_2*` : valtype*}:
15865+
`%|-%:%`(C, [instr], `%->_%%`_instrtype(`%`_resulttype(t_1*{t_1 <- `t_1*`},), x*{x <- `x*`}, `%`_resulttype(t_2*{t_2 <- `t_2*`},)))
15866+
-- Instr_ok: `%|-%:%`(C, instr, `%->_%%`_instrtype(`%`_resulttype(t_1*{t_1 <- `t_1*`},), x*{x <- `x*`}, `%`_resulttype(t_2*{t_2 <- `t_2*`},)))
15867+
15868+
;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:621.1-625.82
15869+
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*}:
15870+
`%|-%:%`(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*`},)))
15871+
-- 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*`},)))
1586215872
-- (if (C.LOCALS_context[x_1!`%`_idx.0] = `%%`_localtype(init, t)))*{init <- `init*`, t <- `t*`, x_1 <- `x_1*`}
1586315873
-- 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*`},)))
1586415874

15865-
;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:623.1-627.33
15875+
;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:627.1-631.33
1586615876
rule sub{C : context, `instr*` : instr*, it' : instrtype, it : instrtype}:
1586715877
`%|-%:%`(C, instr*{instr <- `instr*`}, it')
1586815878
-- Instrs_ok: `%|-%:%`(C, instr*{instr <- `instr*`}, it)
1586915879
-- Instrtype_sub: `%|-%<:%`(C, it, it')
1587015880
-- Instrtype_ok: `%|-%:OK`(C, it')
1587115881

15872-
;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:630.1-633.33
15882+
;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:634.1-637.33
1587315883
rule frame{C : context, `instr*` : instr*, `t*` : valtype*, `t_1*` : valtype*, `x*` : idx*, `t_2*` : valtype*}:
1587415884
`%|-%:%`(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*`},)))
1587515885
-- Instrs_ok: `%|-%:%`(C, instr*{instr <- `instr*`}, `%->_%%`_instrtype(`%`_resulttype(t_1*{t_1 <- `t_1*`},), x*{x <- `x*`}, `%`_resulttype(t_2*{t_2 <- `t_2*`},)))
@@ -27830,24 +27840,29 @@ relation Instrs_ok: `%|-%:%`(context, instr*, instrtype)
2783027840
rule empty{C : context}:
2783127841
`%|-%:%`(C, [], `%->_%%`_instrtype(`%`_resulttype([],), [], `%`_resulttype([],)))
2783227842

27833-
;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:617.1-621.82
27834-
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*}:
27835-
`%|-%:%`(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*`},)))
27836-
-- 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*`},)))
27843+
;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:616.1-618.46
27844+
rule instr{C : context, instr : instr, `t_1*` : valtype*, `x*` : idx*, `t_2*` : valtype*}:
27845+
`%|-%:%`(C, [instr], `%->_%%`_instrtype(`%`_resulttype(t_1*{t_1 <- `t_1*`},), x*{x <- `x*`}, `%`_resulttype(t_2*{t_2 <- `t_2*`},)))
27846+
-- Instr_ok: `%|-%:%`(C, instr, `%->_%%`_instrtype(`%`_resulttype(t_1*{t_1 <- `t_1*`},), x*{x <- `x*`}, `%`_resulttype(t_2*{t_2 <- `t_2*`},)))
27847+
27848+
;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:621.1-625.82
27849+
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*}:
27850+
`%|-%:%`(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*`},)))
27851+
-- 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*`},)))
2783727852
-- if (|`init*`| = |`t*`|)
2783827853
-- if (|`init*`| = |`x_1*`|)
2783927854
-- (if (x_1!`%`_idx.0 < |C.LOCALS_context|))*{x_1 <- `x_1*`}
2784027855
-- (if (C.LOCALS_context[x_1!`%`_idx.0] = `%%`_localtype(init, t)))*{init <- `init*`, t <- `t*`, x_1 <- `x_1*`}
2784127856
-- 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*`},)))
2784227857

27843-
;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:623.1-627.33
27858+
;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:627.1-631.33
2784427859
rule sub{C : context, `instr*` : instr*, it' : instrtype, it : instrtype}:
2784527860
`%|-%:%`(C, instr*{instr <- `instr*`}, it')
2784627861
-- Instrs_ok: `%|-%:%`(C, instr*{instr <- `instr*`}, it)
2784727862
-- Instrtype_sub: `%|-%<:%`(C, it, it')
2784827863
-- Instrtype_ok: `%|-%:OK`(C, it')
2784927864

27850-
;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:630.1-633.33
27865+
;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:634.1-637.33
2785127866
rule frame{C : context, `instr*` : instr*, `t*` : valtype*, `t_1*` : valtype*, `x*` : idx*, `t_2*` : valtype*}:
2785227867
`%|-%:%`(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*`},)))
2785327868
-- Instrs_ok: `%|-%:%`(C, instr*{instr <- `instr*`}, `%->_%%`_instrtype(`%`_resulttype(t_1*{t_1 <- `t_1*`},), x*{x <- `x*`}, `%`_resulttype(t_2*{t_2 <- `t_2*`},)))

0 commit comments

Comments
 (0)