Skip to content
This repository was archived by the owner on Apr 25, 2025. It is now read-only.

Commit b7065d8

Browse files
rossbergrossberg
authored
[spec] New instructions (#52)
1 parent 1a421a0 commit b7065d8

File tree

9 files changed

+569
-368
lines changed

9 files changed

+569
-368
lines changed

‎document/core/appendix/gen-index-instructions.py‎

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -81,7 +81,7 @@ def Instruction(name, opcode, type=None, validation=None, execution=None, operat
8181
Instruction(r'\CALLINDIRECT~x~y', r'\hex{11}', r'[t_1^\ast~\I32] \to [t_2^\ast]', r'valid-call_indirect', r'exec-call_indirect'),
8282
Instruction(None, r'\hex{12}'),
8383
Instruction(None, r'\hex{13}'),
84-
Instruction(None, r'\hex{14}'),
84+
Instruction(r'\CALLREF', r'\hex{14}', r'[t_1^\ast~(\REF~\NULL~x)] \to [t_2^\ast]', r'valid-call_ref', r'exec-call_ref'),
8585
Instruction(None, r'\hex{15}'),
8686
Instruction(None, r'\hex{16}'),
8787
Instruction(None, r'\hex{17}'),
@@ -269,13 +269,13 @@ def Instruction(name, opcode, type=None, validation=None, execution=None, operat
269269
Instruction(None, r'\hex{CD}'),
270270
Instruction(None, r'\hex{CE}'),
271271
Instruction(None, r'\hex{CF}'),
272-
Instruction(r'\REFNULL~t', r'\hex{D0}', r'[] \to [t]', r'valid-ref.null', r'exec-ref.null'),
273-
Instruction(r'\REFISNULL', r'\hex{D1}', r'[t] \to [\I32]', r'valid-ref.is_null', r'exec-ref.is_null'),
272+
Instruction(r'\REFNULL~\X{ht}', r'\hex{D0}', r'[] \to [(\REF~\NULL~\X{ht})]', r'valid-ref.null', r'exec-ref.null'),
273+
Instruction(r'\REFISNULL', r'\hex{D1}', r'[(\REF~\NULL~\X{ht})] \to [\I32]', r'valid-ref.is_null', r'exec-ref.is_null'),
274274
Instruction(r'\REFFUNC~x', r'\hex{D2}', r'[] \to [\FUNCREF]', r'valid-ref.func', r'exec-ref.func'),
275-
Instruction(None, r'\hex{D3}'),
276-
Instruction(None, r'\hex{D4}'),
275+
Instruction(r'\REFASNONNULL', r'\hex{D3}', r'[(\REF~\NULL~\X{ht})] \to [(\REF~\X{ht})]', r'valid-ref.as_non_null', r'exec-ref.as_non_null'),
276+
Instruction(r'\BRONNULL~l', r'\hex{D4}', r'[t^\ast~(\REF~\NULL~\X{ht})] \to [t^\ast~(\REF~\X{ht})]', r'valid-br_on_null', r'exec-br_on_null'),
277277
Instruction(None, r'\hex{D5}'),
278-
Instruction(None, r'\hex{D6}'),
278+
Instruction(r'\BRONNONNULL~l', r'\hex{D6}', r'[t^\ast~(\REF~\NULL~\X{ht})] \to [t^\ast]', r'valid-br_on_non_null', r'exec-br_on_non_null'),
279279
Instruction(None, r'\hex{D7}'),
280280
Instruction(None, r'\hex{D8}'),
281281
Instruction(None, r'\hex{D9}'),

‎document/core/appendix/index-instructions.rst‎

Lines changed: 274 additions & 274 deletions
Large diffs are not rendered by default.

‎document/core/binary/instructions.rst‎

Lines changed: 10 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -34,8 +34,11 @@ Control Instructions
3434
.. _binary-br:
3535
.. _binary-br_if:
3636
.. _binary-br_table:
37+
.. _binary-br_on_null:
38+
.. _binary-br_on_non_null:
3739
.. _binary-return:
3840
.. _binary-call:
41+
.. _binary-call_ref:
3942
.. _binary-call_indirect:
4043

4144
.. math::
@@ -62,7 +65,10 @@ Control Instructions
6265
&\Rightarrow& \BRTABLE~l^\ast~l_N \\ &&|&
6366
\hex{0F} &\Rightarrow& \RETURN \\ &&|&
6467
\hex{10}~~x{:}\Bfuncidx &\Rightarrow& \CALL~x \\ &&|&
65-
\hex{11}~~y{:}\Btypeidx~~x{:}\Btableidx &\Rightarrow& \CALLINDIRECT~x~y \\
68+
\hex{11}~~y{:}\Btypeidx~~x{:}\Btableidx &\Rightarrow& \CALLINDIRECT~x~y \\ &&|&
69+
\hex{14}~~x{:}\Bfuncidx &\Rightarrow& \CALLREF \\ &&|&
70+
\hex{D4}~~x{:}\Bfuncidx &\Rightarrow& \BRONNULL \\ &&|&
71+
\hex{D6}~~x{:}\Bfuncidx &\Rightarrow& \BRONNONNULL \\
6672
\end{array}
6773
6874
.. note::
@@ -84,13 +90,15 @@ Reference Instructions
8490
.. _binary-ref.null:
8591
.. _binary-ref.func:
8692
.. _binary-ref.is_null:
93+
.. _binary-ref.as_non_null:
8794

8895
.. math::
8996
\begin{array}{llclll}
9097
\production{instruction} & \Binstr &::=& \dots \\ &&|&
9198
\hex{D0}~~t{:}\Bheaptype &\Rightarrow& \REFNULL~t \\ &&|&
9299
\hex{D1} &\Rightarrow& \REFISNULL \\ &&|&
93-
\hex{D2}~~x{:}\Bfuncidx &\Rightarrow& \REFFUNC~x \\
100+
\hex{D2}~~x{:}\Bfuncidx &\Rightarrow& \REFFUNC~x \\ &&|&
101+
\hex{D3} &\Rightarrow& \REFASNONNULL \\
94102
\end{array}
95103
96104

‎document/core/exec/instructions.rst‎

Lines changed: 110 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -192,15 +192,35 @@ Reference Instructions
192192

193193
.. _exec-ref.null:
194194

195-
:math:`\REFNULL~t`
196-
..................
195+
:math:`\REFNULL~\X{ht}`
196+
.......................
197197

198-
1. Push the value :math:`\REFNULL~t` to the stack.
198+
1. Push the value :math:`\REFNULL~\X{ht}` to the stack.
199199

200200
.. note::
201201
No formal reduction rule is required for this instruction, since the |REFNULL| instruction is already a :ref:`value <syntax-val>`.
202202

203203

204+
.. _exec-ref.func:
205+
206+
:math:`\REFFUNC~x`
207+
..................
208+
209+
1. Let :math:`F` be the :ref:`current <exec-notation-textual>` :ref:`frame <syntax-frame>`.
210+
211+
2. Assert: due to :ref:`validation <valid-ref.func>`, :math:`F.\AMODULE.\MIFUNCS[x]` exists.
212+
213+
3. Let :math:`a` be the :ref:`function address <syntax-funcaddr>` :math:`F.\AMODULE.\MIFUNCS[x]`.
214+
215+
4. Push the value :math:`\REFFUNCADDR~a` to the stack.
216+
217+
.. math::
218+
\begin{array}{lcl@{\qquad}l}
219+
F; \REFFUNC~x &\stepto& F; \REFFUNCADDR~a
220+
& (\iff a = F.\AMODULE.\MIFUNCS[x]) \\
221+
\end{array}
222+
223+
204224
.. _exec-ref.is_null:
205225

206226
:math:`\REFISNULL`
@@ -210,7 +230,7 @@ Reference Instructions
210230

211231
2. Pop the value :math:`\val` from the stack.
212232

213-
3. If :math:`\val` is :math:`\REFNULL~t`, then:
233+
3. If :math:`\val` is :math:`\REFNULL~\X{ht}`, then:
214234

215235
a. Push the value :math:`\I32.\CONST~1` to the stack.
216236

@@ -221,29 +241,33 @@ Reference Instructions
221241
.. math::
222242
\begin{array}{lcl@{\qquad}l}
223243
\val~\REFISNULL &\stepto& \I32.\CONST~1
224-
& (\iff \val = \REFNULL~t) \\
244+
& (\iff \val = \REFNULL~\X{ht}) \\
225245
\val~\REFISNULL &\stepto& \I32.\CONST~0
226246
& (\otherwise) \\
227247
\end{array}
228248
229249
230-
.. _exec-ref.func:
250+
.. _exec-ref.as_non_null:
231251

232-
:math:`\REFFUNC~x`
233-
..................
252+
:math:`\REFASNONNULL`
253+
.....................
234254

235-
1. Let :math:`F` be the :ref:`current <exec-notation-textual>` :ref:`frame <syntax-frame>`.
255+
1. Assert: due to :ref:`validation <valid-ref.is_null>`, a :ref:`reference value <syntax-ref>` is on the top of the stack.
236256

237-
2. Assert: due to :ref:`validation <valid-ref.func>`, :math:`F.\AMODULE.\MIFUNCS[x]` exists.
257+
2. Pop the value :math:`\val` from the stack.
238258

239-
3. Let :math:`a` be the :ref:`function address <syntax-funcaddr>` :math:`F.\AMODULE.\MIFUNCS[x]`.
259+
3. If :math:`\val` is :math:`\REFNULL~\X{ht}`, then:
240260

241-
4. Push the value :math:`\REFFUNCADDR~a` to the stack.
261+
a. Trap.
262+
263+
4. Push the value :math:`\val` back to the stack.
242264

243265
.. math::
244266
\begin{array}{lcl@{\qquad}l}
245-
F; \REFFUNC~x &\stepto& F; \REFFUNCADDR~a
246-
& (\iff a = F.\AMODULE.\MIFUNCS[x]) \\
267+
\val~\REFASNONNULL &\stepto& \TRAP
268+
& (\iff \val = \REFNULL~\X{ht}) \\
269+
\val~\REFASNONNULL &\stepto& \val
270+
& (\otherwise) \\
247271
\end{array}
248272
249273
@@ -1722,6 +1746,60 @@ Control Instructions
17221746
\end{array}
17231747
17241748
1749+
.. _exec-br_on_null:
1750+
1751+
:math:`\BRONNULL~l`
1752+
...................
1753+
1754+
1. Assert: due to :ref:`validation <valid-ref.is_null>`, a :ref:`reference value <syntax-ref>` is on the top of the stack.
1755+
1756+
2. Pop the value :math:`\val` from the stack.
1757+
1758+
3. If :math:`\val` is :math:`\REFNULL~\X{ht}`, then:
1759+
1760+
a. :ref:`Execute <exec-br>` the instruction :math:`(\BR~l)`.
1761+
1762+
4. Else:
1763+
1764+
a. Push the value :math:`\val` back to the stack.
1765+
1766+
.. math::
1767+
\begin{array}{lcl@{\qquad}l}
1768+
\val~(\BRONNULL~l) &\stepto& (\BR~l)
1769+
& (\iff \val = \REFNULL~\X{ht}) \\
1770+
\val~(\BRONNULL~l) &\stepto& \val
1771+
& (\otherwise) \\
1772+
\end{array}
1773+
1774+
1775+
.. _exec-br_on_non_null:
1776+
1777+
:math:`\BRONNONNULL~l`
1778+
......................
1779+
1780+
1. Assert: due to :ref:`validation <valid-ref.is_null>`, a :ref:`reference value <syntax-ref>` is on the top of the stack.
1781+
1782+
2. Pop the value :math:`\val` from the stack.
1783+
1784+
3. If :math:`\val` is :math:`\REFNULL~\X{ht}`, then:
1785+
1786+
a. Do nothing.
1787+
1788+
4. Else:
1789+
1790+
a. Push the value :math:`\val` back to the stack.
1791+
1792+
b. :ref:`Execute <exec-br>` the instruction :math:`(\BR~l)`.
1793+
1794+
.. math::
1795+
\begin{array}{lcl@{\qquad}l}
1796+
\val~(\BRONNONNULL~l) &\stepto& \epsilon
1797+
& (\iff \val = \REFNULL~\X{ht}) \\
1798+
\val~(\BRONNONNULL~l) &\stepto& \val~(\BR~l)
1799+
& (\otherwise) \\
1800+
\end{array}
1801+
1802+
17251803
.. _exec-return:
17261804

17271805
:math:`\RETURN`
@@ -1776,6 +1854,23 @@ Control Instructions
17761854
\end{array}
17771855
17781856
1857+
.. _exec-call_ref:
1858+
1859+
:math:`\CALLREF`
1860+
................
1861+
1862+
1. Assert: due to :ref:`validation <valid-call_ref>`, a :ref:`function reference <syntax-ref>` is on the top of the stack.
1863+
1864+
2. Pop the value :math:`\REFFUNCADDR~a` from the stack.
1865+
1866+
3. :ref:`Invoke <exec-invoke>` the function instance at address :math:`a`.
1867+
1868+
.. math::
1869+
\begin{array}{lcl@{\qquad}l}
1870+
F; (\REFFUNCADDR~a)~\CALLREF &\stepto& F; (\INVOKE~a)
1871+
\end{array}
1872+
1873+
17791874
.. _exec-call_indirect:
17801875

17811876
:math:`\CALLINDIRECT~x~y`
@@ -1805,7 +1900,7 @@ Control Instructions
18051900

18061901
11. Let :math:`r` be the :ref:`reference <syntax-ref>` :math:`\X{tab}.\TIELEM[i]`.
18071902

1808-
12. If :math:`r` is :math:`\REFNULL~t`, then:
1903+
12. If :math:`r` is :math:`\REFNULL~\X{ht}`, then:
18091904

18101905
a. Trap.
18111906

‎document/core/syntax/instructions.rst‎

Lines changed: 11 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -174,8 +174,9 @@ Occasionally, it is convenient to group operators together according to the foll
174174
.. index:: ! reference instruction, reference, null
175175
pair: abstract syntax; instruction
176176
.. _syntax-ref.null:
177-
.. _syntax-ref.is_null:
178177
.. _syntax-ref.func:
178+
.. _syntax-ref.is_null:
179+
.. _syntax-ref.as_non_null:
179180
.. _syntax-instr-ref:
180181

181182
Reference Instructions
@@ -188,11 +189,13 @@ Instructions in this group are concerned with accessing :ref:`references <syntax
188189
\production{instruction} & \instr &::=&
189190
\dots \\&&|&
190191
\REFNULL~\reftype \\&&|&
192+
\REFFUNC~\funcidx \\&&|&
191193
\REFISNULL \\&&|&
192-
\REFFUNC~\funcidx \\
194+
\REFASNONNULL \\
193195
\end{array}
194196
195-
These instruction produce a null value, check for a null value, or produce a reference to a given function, respectively.
197+
The first three of these instruction produce a :ref:`null <syntax-null>` value, produce a reference to a given function, or check for a null value, respectively.
198+
The |REFASNONNULL| casts a :ref:`nullable <syntax-reftype>` to a non-null one, and :ref:`traps <trap>` if it encounters null.
196199

197200

198201
.. index:: ! parametric instruction, value type
@@ -389,8 +392,11 @@ Instructions in this group affect the flow of control.
389392
\BR~\labelidx \\&&|&
390393
\BRIF~\labelidx \\&&|&
391394
\BRTABLE~\vec(\labelidx)~\labelidx \\&&|&
395+
\BRONNULL~\labelidx \\&&|&
396+
\BRONNONNULL~\labelidx \\&&|&
392397
\RETURN \\&&|&
393398
\CALL~\funcidx \\&&|&
399+
\CALLREF \\&&|&
394400
\CALLINDIRECT~\tableidx~\typeidx \\
395401
\end{array}
396402
@@ -427,13 +433,15 @@ Branch instructions come in several flavors:
427433
|BR| performs an unconditional branch,
428434
|BRIF| performs a conditional branch,
429435
and |BRTABLE| performs an indirect branch through an operand indexing into the label vector that is an immediate to the instruction, or to a default target if the operand is out of bounds.
436+
The |BRONNULL| and |BRONNONNULL| instructions check whether a reference operand is :ref:`null <syntax-null>` and branch if that is the case or not the case, respectively.
430437
The |RETURN| instruction is a shortcut for an unconditional branch to the outermost block, which implicitly is the body of the current function.
431438
Taking a branch *unwinds* the operand stack up to the height where the targeted structured control instruction was entered.
432439
However, branches may additionally consume operands themselves, which they push back on the operand stack after unwinding.
433440
Forward branches require operands according to the output of the targeted block's type, i.e., represent the values produced by the terminated block.
434441
Backward branches require operands according to the input of the targeted block's type, i.e., represent the values consumed by the restarted block.
435442

436443
The |CALL| instruction invokes another :ref:`function <syntax-func>`, consuming the necessary arguments from the stack and returning the result values of the call.
444+
The |CALLREF| instruction invokes a function indirectly through a :ref:`function reference <syntax-reftype>` operand.
437445
The |CALLINDIRECT| instruction calls a function indirectly through an operand indexing into a :ref:`table <syntax-table>` that is denoted by a :ref:`table index <syntax-tableidx>` and must contain :ref:`function references <syntax-reftype>`.
438446
Since it may contain functions of heterogeneous type,
439447
the callee is dynamically checked against the :ref:`function type <syntax-functype>` indexed by the instruction's second immediate, and the call is aborted with a :ref:`trap <trap>` if it does not match.

‎document/core/text/instructions.rst‎

Lines changed: 10 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -95,8 +95,11 @@ However, the special case of a type use that is syntactically empty or consists
9595
.. _text-br:
9696
.. _text-br_if:
9797
.. _text-br_table:
98+
.. _text-br_on_null:
99+
.. _text-br_on_non_null:
98100
.. _text-return:
99101
.. _text-call:
102+
.. _text-call_ref:
100103
.. _text-call_indirect:
101104

102105
All other control instruction are represented verbatim.
@@ -110,8 +113,11 @@ All other control instruction are represented verbatim.
110113
\text{br\_if}~~l{:}\Tlabelidx_I &\Rightarrow& \BRIF~l \\ &&|&
111114
\text{br\_table}~~l^\ast{:}\Tvec(\Tlabelidx_I)~~l_N{:}\Tlabelidx_I
112115
&\Rightarrow& \BRTABLE~l^\ast~l_N \\ &&|&
116+
\text{br\_on\_null}~~l{:}\Tlabelidx_I &\Rightarrow& \BRONNULL~l \\ &&|&
117+
\text{br\_on\_non\_null}~~l{:}\Tlabelidx_I &\Rightarrow& \BRONNONNULL~l \\ &&|&
113118
\text{return} &\Rightarrow& \RETURN \\ &&|&
114119
\text{call}~~x{:}\Tfuncidx_I &\Rightarrow& \CALL~x \\ &&|&
120+
\text{call\_ref} &\Rightarrow& \CALLREF \\ &&|&
115121
\text{call\_indirect}~~x{:}\Ttableidx~~y,I'{:}\Ttypeuse_I &\Rightarrow& \CALLINDIRECT~x~y
116122
& (\iff I' = \{\ILOCALS~(\epsilon)^\ast\}) \\
117123
\end{array}
@@ -152,15 +158,17 @@ Reference Instructions
152158
~~~~~~~~~~~~~~~~~~~~~~
153159

154160
.. _text-ref.null:
155-
.. _text-ref.is_null:
156161
.. _text-ref.func:
162+
.. _text-ref.is_null:
163+
.. _text-ref.as_non_null:
157164

158165
.. math::
159166
\begin{array}{llclll}
160167
\production{instruction} & \Tplaininstr_I &::=& \dots \\ &&|&
161168
\text{ref.null}~~t{:}\Theaptype &\Rightarrow& \REFNULL~t \\ &&|&
162-
\text{ref.is\_null} &\Rightarrow& \REFISNULL \\ &&|&
163169
\text{ref.func}~~x{:}\Tfuncidx &\Rightarrow& \REFFUNC~x \\ &&|&
170+
\text{ref.is\_null} &\Rightarrow& \REFISNULL \\ &&|&
171+
\text{ref.as\_non\_null} &\Rightarrow& \REFASNONNULL \\
164172
\end{array}
165173
166174

‎document/core/util/macros.def‎

Lines changed: 9 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -351,8 +351,11 @@
351351
.. |BR| mathdef:: \xref{syntax/instructions}{syntax-instr-control}{\K{br}}
352352
.. |BRIF| mathdef:: \xref{syntax/instructions}{syntax-instr-control}{\K{br\_if}}
353353
.. |BRTABLE| mathdef:: \xref{syntax/instructions}{syntax-instr-control}{\K{br\_table}}
354+
.. |BRONNULL| mathdef:: \xref{syntax/instructions}{syntax-instr-control}{\K{br\_on\_null}}
355+
.. |BRONNONNULL| mathdef:: \xref{syntax/instructions}{syntax-instr-control}{\K{br\_on\_non\_null}}
354356
.. |RETURN| mathdef:: \xref{syntax/instructions}{syntax-instr-control}{\K{return}}
355357
.. |CALL| mathdef:: \xref{syntax/instructions}{syntax-instr-control}{\K{call}}
358+
.. |CALLREF| mathdef:: \xref{syntax/instructions}{syntax-instr-control}{\K{call\_ref}}
356359
.. |CALLINDIRECT| mathdef:: \xref{syntax/instructions}{syntax-instr-control}{\K{call\_indirect}}
357360

358361
.. |DROP| mathdef:: \xref{syntax/instructions}{syntax-instr-parametric}{\K{drop}}
@@ -383,8 +386,9 @@
383386
.. |DATADROP| mathdef:: \xref{syntax/instructions}{syntax-instr-memory}{\K{data.drop}}
384387

385388
.. |REFNULL| mathdef:: \xref{syntax/instructions}{syntax-instr-ref}{\K{ref{.}null}}
386-
.. |REFISNULL| mathdef:: \xref{syntax/instructions}{syntax-instr-ref}{\K{ref{.}is\_null}}
387389
.. |REFFUNC| mathdef:: \xref{syntax/instructions}{syntax-instr-ref}{\K{ref{.}func}}
390+
.. |REFISNULL| mathdef:: \xref{syntax/instructions}{syntax-instr-ref}{\K{ref{.}is\_null}}
391+
.. |REFASNONNULL| mathdef:: \xref{syntax/instructions}{syntax-instr-ref}{\K{ref{.}as\_non\_null}}
388392

389393
.. |CONST| mathdef:: \xref{syntax/instructions}{syntax-instr-numeric}{\K{const}}
390394
.. |EQZ| mathdef:: \xref{syntax/instructions}{syntax-instr-numeric}{\K{eqz}}
@@ -789,8 +793,8 @@
789793
.. |matchestabletype| mathdef:: \xref{valid/matching}{match-tabletype}{\leq}
790794
.. |matchesmemtype| mathdef:: \xref{valid/matching}{match-memtype}{\leq}
791795
.. |matchesglobaltype| mathdef:: \xref{valid/matching}{match-globaltype}{\leq}
792-
.. |matchesexterntype| mathdef:: \xref{exec/matching}{match-externtype}{\leq}
793-
.. |matcheslimits| mathdef:: \xref{exec/matching}{match-limits}{\leq}
796+
.. |matchesexterntype| mathdef:: \xref{valid/matching}{match-externtype}{\leq}
797+
.. |matcheslimits| mathdef:: \xref{valid/matching}{match-limits}{\leq}
794798

795799

796800
.. Contexts
@@ -832,8 +836,8 @@
832836
.. |vdashtabletypematch| mathdef:: \xref{valid/matching}{match-tabletype}{\vdash}
833837
.. |vdashmemtypematch| mathdef:: \xref{valid/matching}{match-memtype}{\vdash}
834838
.. |vdashglobaltypematch| mathdef:: \xref{valid/matching}{match-globaltype}{\vdash}
835-
.. |vdashexterntypematch| mathdef:: \xref{exec/matching}{match-externtype}{\vdash}
836-
.. |vdashlimitsmatch| mathdef:: \xref{exec/matching}{match-limits}{\vdash}
839+
.. |vdashexterntypematch| mathdef:: \xref{valid/matching}{match-externtype}{\vdash}
840+
.. |vdashlimitsmatch| mathdef:: \xref{valid/matching}{match-limits}{\vdash}
837841

838842
.. |vdashinstr| mathdef:: \xref{valid/instructions}{valid-instr}{\vdash}
839843
.. |vdashinstrseq| mathdef:: \xref{valid/instructions}{valid-instr-seq}{\vdash}

0 commit comments

Comments
 (0)