Skip to content
This repository was archived by the owner on Nov 3, 2021. It is now read-only.

[spec] Document execution #19

Closed
binji wants to merge 8 commits into from
Closed

[spec] Document execution #19

Show file tree
Hide file tree
Changes from 2 commits
Commits
Show all changes
8 commits
Select commit Hold shift + click to select a range
1f65aa1
[spec] Document execution
binji May 22, 2018
6c73ce1
Capitalize some headings
binji May 22, 2018
94e91c4
Address some comments
binji Jun 7, 2018
9bbfe24
Add memory.{drop,copy} exec
binji Jun 13, 2018
af0622b
Add Table instructions
binji Jun 20, 2018
4fd2b5b
Init all segments, move initdata/initelem into instructions section
binji Jun 20, 2018
526575e
Some instruction fixes
binji Jun 20, 2018
d058cd0
Address some comments
binji Jul 9, 2018
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
70 changes: 70 additions & 0 deletions document/core/exec/instructions.rst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -618,6 +618,76 @@ Memory Instructions
In practice, the choice depends on the :ref:`resources <impl-exec>` available to the :ref:`embedder <embedder>`.


.. _exec-memory.init:

:math:`\MEMORYINIT~x`
.....................

1. Let :math:`F` be the :ref:`current <exec-notation-textual>` :ref:`frame <syntax-frame>`.

2. Assert: due to :ref:`validation <valid-memory.init>`, :math:`F.\AMODULE.\MIMEMS[0]` exists.

3. Let :math:`ma` be the :ref:`memory address <syntax-memaddr>` :math:`F.\AMODULE.\MIMEMS[0]`.

4. Assert: due to :ref:`validation <valid-memory.init>`, :math:`S.\SMEMS[ma]` exists.

5. Let :math:`\X{mem}` be the :ref:`memory instance <syntax-meminst>` :math:`S.\SMEMS[ma]`.

6. Let :math:`msz` be the length of :math:`\X{mem}.\MIDATA`.

7. Assert: due to :ref:`validation <valid-memory.init>`, :math:`F.\AMODULE.\MIDATAS[x]` exists.

8. Let :math:`da` be the :ref:`data segment address <syntax-dataaddr>` :math:`F.\AMODULE.\MIDATAS[x]`.

9. If :math:`S.\SDATA[da]` does not exist, then:

a. Trap.

10. Let :math:`\X{data}` be the :ref:`data segment instance <syntax-datainst>` :math:`S.\SDATA[da]`.

11. Assert: due to :ref:`validation <valid-memory.init>`, three values of :ref:`value type <syntax-valtype>` |I32| are on the top of the stack.

12. Pop the value :math:`\I32.\CONST~s` from the stack.

13. Pop the value :math:`\I32.\CONST~t` from the stack.

@rossberg rossberg Jun 1, 2018

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

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

Nit: the spec convention is to use t for value types, and i,j,k,m,n for integers, at least if they are single-letter. So either use those or somewhat longer names.


14. Pop the value :math:`\I32.\CONST~n` from the stack.

15. Let :math:`dsz` be the length of :math:`\X{data}.\DSIINIT`.

16. If :math:`s + n > dsz`, then:

a. Trap.

17. If :math:`t + n > msz`, then:

a. Trap.

18. Let :math:`y` be the byte sequence :math:`\X{mem}.\DSIINIT[s \slice n]`.

@rossberg rossberg Jun 1, 2018

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

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

Nit: Use b^\ast instead of y.


19. :ref:`Initialize <initdata>` the memory instance at address :math:`ma` starting from offset :math:`t` with the byte sequence :math:`y`.

.. math::
~\\[-1ex]
\begin{array}{l}
\begin{array}{lcl@{\qquad}l}
S; F; (\I32.\CONST~n)~(\I32.\CONST~t)~(\I32.\CONST~s)~(\MEMORYINIT~x) &\stepto& S; F; (\INITDATA~ma~t~y)
\end{array}
\\ \qquad
\begin{array}[t]{@{}r@{~}l@{}}
(\iff & F.\AMODULE.\MIMEMS[0] = ma \\

@rossberg rossberg Jul 9, 2018

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

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

It seems like ma isn't needed (similarly in prose).

\wedge & F.\AMODULE.\MIDATAS[x] = da \\
\wedge & (s + n \leq |S.\SDATA[da].\DSIINIT|) \\
\wedge & (t + n \leq |S.\SMEMS[ma].\MIDATA|) \\
\wedge & y = S.\SDATA[da].\DSIINIT[s \slice n]) \\
\end{array}
\\[1ex]
\begin{array}{lcl@{\qquad}l}
S; F; (\I32.\CONST~n)~(\I32.\CONST~t)~(\I32.\CONST~s)~(\MEMORYINIT~x) &\stepto& S; F; \TRAP

@rossberg rossberg Jun 1, 2018

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

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

This needs an "otherwise" as a side conditione, else it would always be allowed non-deterministically.

\end{array}
\end{array}


.. index:: control instructions, structured control, label, block, branch, result type, label index, function index, type index, vector, address, table address, table instance, store, frame
pair: execution; instruction
single: abstract syntax; instruction
Expand Down
176 changes: 140 additions & 36 deletions document/core/exec/modules.rst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -371,6 +371,66 @@ New instances of :ref:`functions <syntax-funcinst>`, :ref:`tables <syntax-tablei
\end{array}


.. index:: element, element instance, element address
.. _alloc-elem:

:ref:`Element segments <syntax-eleminst>`
.........................................

1. Let :math:`e` be the :ref:`element segment <syntax-elem>` to allocate.

2. If :math:`e` is of the form :math:`\{ \EINIT~x^\ast \}`, then:

@rossberg rossberg Jun 1, 2018

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

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

What does this algorithm return otherwise? Should it be epsilon, i.e., the algo returns an optional address?


a. Let :math:`a` be the first free :ref:`element address <syntax-elemaddr>` in :math:`S`.

b. For each :ref:`function index <syntax-funcidx>` :math:`x_i` in :math:`e.\EINIT`, do:

i. Let :math:`\funcaddr_i` be the :ref:`function address <syntax-funcaddr>` :math:`\moduleinst.\MIFUNCS[x_i]`.

c. Let :math:`\funcaddr^\ast` be the concatenation of the function addresses :math:`\funcaddr_i`.

d. Let :math:`\eleminst` be the :ref:`element instance <syntax-eleminst>` :math:`\{ \ESIINIT~\funcaddr^\ast \}`.

e. Append :math:`\eleminst` to the |SELEM| of :math:`S`.

.. math::
\begin{array}{rlll@{\qquad}l}
\allocelem(S, e, \moduleinst) &=& S', \elemaddr & (\iff e = \{ \EINIT~x^\ast \}) \\[1ex]
\allocelem(S, e, \moduleinst) &=& S & (\otherwise) \\[1ex]

@rossberg rossberg Jun 1, 2018

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

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

This only returns one thing, not a pair, which seems incoherent. I think it should be epsilon.

\mbox{where:} \hfill \\

@rossberg rossberg Jun 1, 2018

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

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

This should go one line above to the corresponding rule.

\elemaddr &=& |S.\SELEM| \\
\eleminst &=& \{ \ESIINIT~(\moduleinst.\MIFUNCS[x])^\ast \} \\
S' &=& S \compose \{\SELEM~\eleminst\} \\
\end{array}


.. index:: data, data instance, data address
.. _alloc-data:

:ref:`Data segments <syntax-datainst>`
......................................

1. Let :math:`d` be the :ref:`data segment <syntax-data>` to allocate.

2. If :math:`d` is of the form :math:`\{ \DINIT~b^\ast \}`, then:

@rossberg rossberg Jun 1, 2018

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

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

Same here.


a. Let :math:`a` be the first free :ref:`data address <syntax-dataaddr>` in :math:`S`.

b. Let :math:`\datainst` be the :ref:`data instance <syntax-datainst>` :math:`\{ \ESIINIT~d.\DINIT \}`.

c. Append :math:`\datainst` to the |SDATA| of :math:`S`.

.. math::
\begin{array}{rlll}
\allocdata(S, d, \moduleinst) &=& S', \dataaddr & (\iff d = \{ \DINIT~b^\ast \}) \\[1ex]
\allocdata(S, d, \moduleinst) &=& S & (\otherwise) \\[1ex]
\mbox{where:} \hfill \\
\dataaddr &=& |S.\SDATA| \\
\datainst &=& \{ \DSIINIT~d.\DINIT \} \\
S' &=& S \compose \{\SDATA~\datainst\} \\
\end{array}


.. index:: table, table instance, table address, grow, limits
.. _grow-table:

Expand Down Expand Up @@ -411,7 +471,7 @@ Growing :ref:`memories <syntax-meminst>`
\end{array}


.. index:: module, module instance, function instance, table instance, memory instance, global instance, export instance, function address, table address, memory address, global address, function index, table index, memory index, global index, type, function, table, memory, global, import, export, external value, external type, matching
.. index:: module, module instance, function instance, table instance, memory instance, global instance, export instance, function address, table address, memory address, global address, element address, data addresss, function index, table index, memory index, global index, element index, data index, type, function, table, memory, global, element, data, import, export, external value, external type, matching
.. _alloc-module:

:ref:`Modules <syntax-moduleinst>`
Expand Down Expand Up @@ -439,23 +499,35 @@ and :math:`\val^\ast` the initialization :ref:`values <syntax-val>` of the modul

a. Let :math:`\globaladdr_i` be the :ref:`global address <syntax-globaladdr>` resulting from :ref:`allocating <alloc-global>` :math:`\global_i.\GTYPE` with initializer value :math:`\val^\ast[i]`.

6. Let :math:`\funcaddr^\ast` be the the concatenation of the :ref:`function addresses <syntax-funcaddr>` :math:`\funcaddr_i` in index order.
6. For each :ref:`element segment <syntax-elem>` :math:`\elem_i` in :math:`\module.\MELEM`, do:

a. Let :math:`\elemaddr_i` be the :ref:`element address <syntax-elemaddr>` resulting from :ref:`allocating <alloc-elem>` :math:`\elem_i` for the :ref:`\module instance <syntax-moduleinst>` :math:`\moduleinst` defined below.

@rossberg rossberg Jun 1, 2018

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

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

Here you assume that the vector of elemaddr_i corresponds to elem_i, which is not the case because you only get addresses for passive elements. So I think what the module instance needs to store is not am elemaddr^* but an (elemaddr^?)^*. Otherwise all the indexing will be off, too.


7. For each :ref:`data segment <syntax-data>` :math:`\data_i` in :math:`\module.\MDATA`, do:

a. Let :math:`\dataaddr_i` be the :ref:`data address <syntax-dataaddr>` resulting from :ref:`allocating <alloc-data>` :math:`\data_i`.

7. Let :math:`\tableaddr^\ast` be the the concatenation of the :ref:`table addresses <syntax-tableaddr>` :math:`\tableaddr_i` in index order.
8. Let :math:`\funcaddr^\ast` be the the concatenation of the :ref:`function addresses <syntax-funcaddr>` :math:`\funcaddr_i` in index order.

8. Let :math:`\memaddr^\ast` be the the concatenation of the :ref:`memory addresses <syntax-memaddr>` :math:`\memaddr_i` in index order.
9. Let :math:`\tableaddr^\ast` be the the concatenation of the :ref:`table addresses <syntax-tableaddr>` :math:`\tableaddr_i` in index order.

9. Let :math:`\globaladdr^\ast` be the the concatenation of the :ref:`global addresses <syntax-globaladdr>` :math:`\globaladdr_i` in index order.
10. Let :math:`\memaddr^\ast` be the the concatenation of the :ref:`memory addresses <syntax-memaddr>` :math:`\memaddr_i` in index order.

10. Let :math:`\funcaddr_{\F{mod}}^\ast` be the list of :ref:`function addresses <syntax-funcaddr>` extracted from :math:`\externval_{\F{im}}^\ast`, concatenated with :math:`\funcaddr^\ast`.
11. Let :math:`\globaladdr^\ast` be the the concatenation of the :ref:`global addresses <syntax-globaladdr>` :math:`\globaladdr_i` in index order.

11. Let :math:`\tableaddr_{\F{mod}}^\ast` be the list of :ref:`table addresses <syntax-tableaddr>` extracted from :math:`\externval_{\F{im}}^\ast`, concatenated with :math:`\tableaddr^\ast`.
12. Let :math:`\elemaddr^\ast` be the the concatenation of the :ref:`element addresses <syntax-elemaddr>` :math:`\elemaddr_i` in index order.

12. Let :math:`\memaddr_{\F{mod}}^\ast` be the list of :ref:`memory addresses <syntax-memaddr>` extracted from :math:`\externval_{\F{im}}^\ast`, concatenated with :math:`\memaddr^\ast`.
13. Let :math:`\dataaddr^\ast` be the the concatenation of the :ref:`data addresses <syntax-dataaddr>` :math:`\dataaddr_i` in index order.

13. Let :math:`\globaladdr_{\F{mod}}^\ast` be the list of :ref:`global addresses <syntax-globaladdr>` extracted from :math:`\externval_{\F{im}}^\ast`, concatenated with :math:`\globaladdr^\ast`.
14. Let :math:`\funcaddr_{\F{mod}}^\ast` be the list of :ref:`function addresses <syntax-funcaddr>` extracted from :math:`\externval_{\F{im}}^\ast`, concatenated with :math:`\funcaddr^\ast`.

14. For each :ref:`export <syntax-export>` :math:`\export_i` in :math:`\module.\MEXPORTS`, do:
15. Let :math:`\tableaddr_{\F{mod}}^\ast` be the list of :ref:`table addresses <syntax-tableaddr>` extracted from :math:`\externval_{\F{im}}^\ast`, concatenated with :math:`\tableaddr^\ast`.

16. Let :math:`\memaddr_{\F{mod}}^\ast` be the list of :ref:`memory addresses <syntax-memaddr>` extracted from :math:`\externval_{\F{im}}^\ast`, concatenated with :math:`\memaddr^\ast`.

17. Let :math:`\globaladdr_{\F{mod}}^\ast` be the list of :ref:`global addresses <syntax-globaladdr>` extracted from :math:`\externval_{\F{im}}^\ast`, concatenated with :math:`\globaladdr^\ast`.

18. For each :ref:`export <syntax-export>` :math:`\export_i` in :math:`\module.\MEXPORTS`, do:

a. If :math:`\export_i` is a function export for :ref:`function index <syntax-funcidx>` :math:`x`, then let :math:`\externval_i` be the :ref:`external value <syntax-externval>` :math:`\EVFUNC~(\funcaddr_{\F{mod}}^\ast[x])`.

Expand All @@ -467,11 +539,11 @@ and :math:`\val^\ast` the initialization :ref:`values <syntax-val>` of the modul

e. Let :math:`\exportinst_i` be the :ref:`export instance <syntax-exportinst>` :math:`\{\EINAME~(\export_i.\ENAME), \EIVALUE~\externval_i\}`.

15. Let :math:`\exportinst^\ast` be the the concatenation of the :ref:`export instances <syntax-exportinst>` :math:`\exportinst_i` in index order.
19. Let :math:`\exportinst^\ast` be the the concatenation of the :ref:`export instances <syntax-exportinst>` :math:`\exportinst_i` in index order.

16. Let :math:`\moduleinst` be the :ref:`module instance <syntax-moduleinst>` :math:`\{\MITYPES~(\module.\MTYPES),` :math:`\MIFUNCS~\funcaddr_{\F{mod}}^\ast,` :math:`\MITABLES~\tableaddr_{\F{mod}}^\ast,` :math:`\MIMEMS~\memaddr_{\F{mod}}^\ast,` :math:`\MIGLOBALS~\globaladdr_{\F{mod}}^\ast,` :math:`\MIEXPORTS~\exportinst^\ast\}`.
20. Let :math:`\moduleinst` be the :ref:`module instance <syntax-moduleinst>` :math:`\{\MITYPES~(\module.\MTYPES),` :math:`\MIFUNCS~\funcaddr_{\F{mod}}^\ast,` :math:`\MITABLES~\tableaddr_{\F{mod}}^\ast,` :math:`\MIMEMS~\memaddr_{\F{mod}}^\ast,` :math:`\MIGLOBALS~\globaladdr_{\F{mod}}^\ast,` :math:`\MIELEMS~\elemaddr^\ast`, :math:`\MIDATAS~\dataaddr^\ast`, :math:`\MIEXPORTS~\exportinst^\ast\}`.

17. Return :math:`\moduleinst`.
21. Return :math:`\moduleinst`.


.. math::
Expand All @@ -490,15 +562,19 @@ where:
\MITABLES~\evtables(\externval_{\F{im}}^\ast)~\tableaddr^\ast, \\
\MIMEMS~\evmems(\externval_{\F{im}}^\ast)~\memaddr^\ast, \\
\MIGLOBALS~\evglobals(\externval_{\F{im}}^\ast)~\globaladdr^\ast, \\
\MIELEMS~\elemaddr^\ast, \\
\MIDATAS~\dataaddr^\ast, \\
\MIEXPORTS~\exportinst^\ast ~\}
\end{array} \\[1ex]
S_1, \funcaddr^\ast &=& \allocfunc^\ast(S, \module.\MFUNCS, \moduleinst) \\
S_2, \tableaddr^\ast &=& \alloctable^\ast(S_1, (\table.\TTYPE)^\ast)
\qquad\qquad\qquad~ (\where \table^\ast = \module.\MTABLES) \\
S_3, \memaddr^\ast &=& \allocmem^\ast(S_2, (\mem.\MTYPE)^\ast)
\qquad\qquad\qquad~ (\where \mem^\ast = \module.\MMEMS) \\
S', \globaladdr^\ast &=& \allocglobal^\ast(S_3, (\global.\GTYPE)^\ast, \val^\ast)
S_4, \globaladdr^\ast &=& \allocglobal^\ast(S_3, (\global.\GTYPE)^\ast, \val^\ast)
\qquad\quad~ (\where \global^\ast = \module.\MGLOBALS) \\
S_5, \elemaddr^\ast &=& \allocelem^\ast(S_4, \module.\MELEM, \moduleinst) \\
S', \dataaddr^\ast &=& \allocdata^\ast(S_5, \module.\MDATA) \\
\exportinst^\ast &=& \{ \EINAME~(\export.\ENAME), \EIVALUE~\externval_{\F{ex}} \}^\ast
\quad (\where \export^\ast = \module.\MEXPORTS) \\[1ex]
\evfuncs(\externval_{\F{ex}}^\ast) &=& (\moduleinst.\MIFUNCS[x])^\ast
Expand Down Expand Up @@ -537,6 +613,54 @@ Moreover, if the dots :math:`\dots` are a sequence :math:`A^n` (as for globals),
In an implementation, this recursion is easily unraveled by mutating one or the other in a secondary step.


.. index:: table, table instance, table address, initialize table
.. _initelem:

:math:`\INITELEM~\tableaddr~o~x^\ast`
.....................................

1. Let :math:`F` be the :ref:`current <exec-notation-textual>` :ref:`frame <syntax-frame>`.

2. For each :ref:`function index <syntax-funcidx>` :math:`x_i` of :math:`x^\ast`:

a. Let :math:`\funcaddr_i` be the :ref:`function address <syntax-funcaddr>` :math:`F.\AMODULE.\MIFUNCS[x_i]`.

b. Replace :math:`S.\STABLES[\tableaddr].\TIELEM[o + i]` with :math:`\funcaddr_i`.

.. math::
~\\[-1ex]
\begin{array}{l}
\begin{array}{lcl@{\qquad}l}
S; F; \INITELEM~\tableaddr~o~\epsilon &\stepto& S; F; \epsilon & \\
S; F; \INITELEM~\tableaddr~o~(x_0~x^\ast) &\stepto& S'; F; \INITELEM~\tableaddr~(o+1)~x^\ast
\end{array}
\\ \qquad
(\iff S' = S \with \STABLES[\tableaddr].\TIELEM[o] = F.\AMODULE.\MIFUNCS[x_0]) \\
\end{array}


.. index:: memory, memory instance, memory address, initialize memory
.. _initdata:

:math:`\INITDATA~\memaddr~o~b^\ast`
...................................

1. For each byte :math:`b_i` of :math:`b^\ast`:

a. Replace :math:`S.\SMEMS[\memaddr].\MIDATA[o + i]` with :math:`b_i`.

.. math::
~\\[-1ex]
\begin{array}{l}
\begin{array}{lcl@{\qquad}l}
S; F; \INITDATA~\memaddr~o~\epsilon &\stepto& S; F; \epsilon \\
S; F; \INITDATA~\memaddr~o~(b_0~b^\ast) &\stepto& S'; F; \INITDATA~\memaddr~(o+1)~b^\ast
\end{array}
\\ \qquad
(\iff S' = S \with \SMEMS[\memaddr].\MIDATA[o] = b_0) \\
\end{array}


.. index:: ! instantiation, module, instance, store, trap
.. _exec-module:
.. _exec-instantiation:
Expand Down Expand Up @@ -645,19 +769,11 @@ It is up to the :ref:`embedder <embedder>` to define how such conditions are rep

13. For each :ref:`element segment <syntax-elem>` :math:`\elem_i` in :math:`\module.\MELEM`, do:

a. For each :ref:`function index <syntax-funcidx>` :math:`\funcidx_{ij}` in :math:`\elem_i.\EINIT` (starting with :math:`j = 0`), do:

i. Assert: due to :ref:`validation <valid-elem>`, :math:`\moduleinst.\MIFUNCS[\funcidx_{ij}]` exists.

ii. Let :math:`\funcaddr_{ij}` be the :ref:`function address <syntax-funcaddr>` :math:`\moduleinst.\MIFUNCS[\funcidx_{ij}]`.

iii. Replace :math:`\tableinst_i.\TIELEM[\X{eo}_i + j]` with :math:`\funcaddr_{ij}`.
a. :ref:`Intialize <initelem>` the table instance at :math:`\tableaddr_i` starting from offset :math:`\X{eo}_i` with the :ref:`function index <syntax-funcidx>` sequence :math:`\elem_i.\EINIT`.

14. For each :ref:`data segment <syntax-data>` :math:`\data_i` in :math:`\module.\MDATA`, do:

a. For each :ref:`byte <syntax-byte>` :math:`b_{ij}` in :math:`\data_i.\DINIT` (starting with :math:`j = 0`), do:

i. Replace :math:`\meminst_i.\MIDATA[\X{do}_i + j]` with :math:`b_{ij}`.
a. :ref:`Initialize <initdata>` the memory instance at :math:`\memaddr_i` starting from offset :math:`\X{do}_i` with the :ref:`byte <syntax-byte>` sequence :math:`\data_i.\DINIT`.

15. If the :ref:`start function <syntax-start>` :math:`\module.\MSTART` is not empty, then:

Expand Down Expand Up @@ -696,18 +812,6 @@ It is up to the :ref:`embedder <embedder>` to define how such conditions are rep
&\wedge& (\tableaddr = \moduleinst.\MITABLES[\elem.\ETABLE])^\ast \\
&\wedge& (\memaddr = \moduleinst.\MIMEMS[\data.\DMEM])^\ast \\
&\wedge& (\funcaddr = \moduleinst.\MIFUNCS[\start.\SFUNC])^?)
\\[2ex]
S; F; \INITELEM~a~i~\epsilon &\stepto&
S; F; \epsilon \\
S; F; \INITELEM~a~i~(x_0~x^\ast) &\stepto&
S'; F; \INITELEM~a~(i+1)~x^\ast \\ &&
(\iff S' = S \with \STABLES[a].\TIELEM[i] = F.\AMODULE.\MIFUNCS[x_0])
\\[1ex]
S; F; \INITDATA~a~i~\epsilon &\stepto&
S; F; \epsilon \\
S; F; \INITDATA~a~i~(b_0~b^\ast) &\stepto&
S'; F; \INITDATA~a~(i+1)~b^\ast \\ &&
(\iff S' = S \with \SMEMS[a].\MIDATA[i] = b_0)
\end{array}

.. note::
Expand Down
Loading