Skip to content

Commit

Permalink
Fix CI
Browse files Browse the repository at this point in the history
  • Loading branch information
rossberg committed May 17, 2024
1 parent 8a19272 commit bc21b85
Show file tree
Hide file tree
Showing 10 changed files with 34 additions and 34 deletions.
2 changes: 1 addition & 1 deletion document/core/appendix/changes.rst
Original file line number Diff line number Diff line change
Expand Up @@ -216,7 +216,7 @@ Added more precise types for references. [#proposal-typedref]_

* Refined typing of :ref:`reference instruction <syntax-instr-ref>` |REFFUNC| with more precise result type

* Refined typing of :ref:`local instructions <valid-instr-variable>` and :ref:`instruction sequences <valid-instr-seq>` to track the :ref:`initialization status <syntax-init>` of :ref:`locals <syntax-local>` with non-defaultable type
* Refined typing of :ref:`local instructions <valid-instr-variable>` and :ref:`instruction sequences <valid-instrs>` to track the :ref:`initialization status <syntax-init>` of :ref:`locals <syntax-local>` with non-defaultable type

* Extended :ref:`table definitions <syntax-table>` with optional initializer expression

Expand Down
2 changes: 1 addition & 1 deletion document/core/appendix/index-rules.rst
Original file line number Diff line number Diff line change
Expand Up @@ -46,7 +46,7 @@ Typing of Static Constructs
Construct Judgement
=============================================== =================================================================================
:ref:`Instruction <valid-instr>` :math:`S;C \vdashinstr \instr : \functype`
:ref:`Instruction sequence <valid-instr-seq>` :math:`S;C \vdashinstrs \instr^\ast : \functype`
:ref:`Instruction sequence <valid-instrs>` :math:`S;C \vdashinstrs \instr^\ast : \functype`
:ref:`Expression <valid-expr>` :math:`C \vdashexpr \expr : \resulttype`
:ref:`Function <valid-func>` :math:`C \vdashfunc \func : \functype`
:ref:`Local <valid-local>` :math:`C \vdashlocal \local : \localtype`
Expand Down
10 changes: 5 additions & 5 deletions document/core/appendix/properties.rst
Original file line number Diff line number Diff line change
Expand Up @@ -870,7 +870,7 @@ Finally, :ref:`frames <syntax-frame>` are classified with *frame contexts*, whic
* Let :math:`C'` be the same :ref:`context <context>` as :math:`C`, but with |CRETURN| set to :math:`\resulttype^?`.

* Under context :math:`C'`,
the instruction sequence :math:`\instr^\ast` must be :ref:`valid <valid-instr-seq>` with some type :math:`[] \to [t^\ast]`.
the instruction sequence :math:`\instr^\ast` must be :ref:`valid <valid-instrs>` with some type :math:`[] \to [t^\ast]`.

* Then the thread is valid with the :ref:`result type <syntax-resulttype>` :math:`[t^\ast]`.

Expand Down Expand Up @@ -978,12 +978,12 @@ To that end, all previous typing judgements :math:`C \vdash \X{prop}` are genera
:math:`\LABEL_n\{\instr_0^\ast\}~\instr^\ast~\END`
..................................................

* The instruction sequence :math:`\instr_0^\ast` must be :ref:`valid <valid-instr-seq>` with some type :math:`[t_1^n] \to_{x^\ast} [t_2^*]`.
* The instruction sequence :math:`\instr_0^\ast` must be :ref:`valid <valid-instrs>` with some type :math:`[t_1^n] \to_{x^\ast} [t_2^*]`.

* Let :math:`C'` be the same :ref:`context <context>` as :math:`C`, but with the :ref:`result type <syntax-resulttype>` :math:`[t_1^n]` prepended to the |CLABELS| list.

* Under context :math:`C'`,
the instruction sequence :math:`\instr^\ast` must be :ref:`valid <valid-instr-seq>` with type :math:`[] \to_{{x'}^\ast} [t_2^*]`.
the instruction sequence :math:`\instr^\ast` must be :ref:`valid <valid-instrs>` with type :math:`[] \to_{{x'}^\ast} [t_2^*]`.

* Then the compound instruction is valid with type :math:`[] \to [t_2^*]`.

Expand Down Expand Up @@ -1464,7 +1464,7 @@ do not have common subtypes either (other than :math:`\BOT` or :math:`\REF~\BOT`
Compositionality
~~~~~~~~~~~~~~~~

:ref:`Valid <valid-instr-seq>` :ref:`instruction sequences <syntax-instr>` can be freely *composed*, as long as their types match up.
:ref:`Valid <valid-instrs>` :ref:`instruction sequences <syntax-instr>` can be freely *composed*, as long as their types match up.

**Theorem (Composition).**
If two instruction sequences :math:`\instr_1^\ast` and :math:`\instr_2^\ast` are valid with types :math:`[t_1^\ast] \to_{x_1^\ast} [t^\ast]` and :math:`[t^\ast] \to_{x_2^\ast} [t_2^\ast]`, respectively (i.e., :math:`C \vdashinstrs \instr_1^\ast : [t_1^\ast] \to_{x_1^\ast} [t^\ast]` and :math:`C \vdashinstrs \instr_1^\ast : [t^\ast] \to_{x_2^\ast} [t_2^\ast]`),
Expand All @@ -1474,7 +1474,7 @@ then the concatenated instruction sequence :math:`(\instr_1^\ast\;\instr_2^\ast)
More generally, instead of a shared type :math:`[t^\ast]`, it suffices if the output type of :math:`\instr_1^\ast` is a :ref:`subtype <match-resulttype>` of the input type of :math:`\instr_1^\ast`,
since the subtype can always be weakened to its supertype by subsumption.

Inversely, valid instruction sequences can also freely be *decomposed*, that is, splitting them anywhere produces two instruction sequences that are both :ref:`valid <valid-instr-seq>`.
Inversely, valid instruction sequences can also freely be *decomposed*, that is, splitting them anywhere produces two instruction sequences that are both :ref:`valid <valid-instrs>`.

**Theorem (Decomposition).**
If an instruction sequence :math:`\instr^\ast` that is valid with type :math:`[t_1^\ast] \to_{x^\ast} [t_2^\ast]` (i.e., :math:`C \vdashinstrs \instr^\ast : [t_1^\ast] \to_{x^\ast} [t_2^\ast]`)
Expand Down
4 changes: 2 additions & 2 deletions document/core/exec/conventions.rst
Original file line number Diff line number Diff line change
Expand Up @@ -47,9 +47,9 @@ The following conventions are adopted in stating these rules.
* The execution of an instruction may also end in a *jump* to a designated target,
which defines the next instruction to execute.

* Execution can *enter* and *exit* :ref:`instruction sequences <syntax-instr-seq>` that form :ref:`blocks <syntax-instr-control>`.
* Execution can *enter* and *exit* :ref:`instruction sequences <syntax-instrs>` that form :ref:`blocks <syntax-instr-control>`.

* :ref:`Instruction sequences <syntax-instr-seq>` are implicitly executed in order, unless a trap or jump occurs.
* :ref:`Instruction sequences <syntax-instrs>` are implicitly executed in order, unless a trap or jump occurs.

* In various places the rules contain *assertions* expressing crucial invariants about the program state.

Expand Down
14 changes: 7 additions & 7 deletions document/core/exec/instructions.rst
Original file line number Diff line number Diff line change
Expand Up @@ -2544,16 +2544,16 @@ $${rule: {Step_pure/return_call_indirect}}


.. index:: instruction, instruction sequence, block
.. _exec-instr-seq:
.. _exec-instrs:

Blocks
~~~~~~

The following auxiliary rules define the semantics of executing an :ref:`instruction sequence <syntax-instr-seq>`
The following auxiliary rules define the semantics of executing an :ref:`instruction sequence <syntax-instrs>`
that forms a :ref:`block <exec-instr-control>`.


.. _exec-instr-seq-enter:
.. _exec-instrs-enter:

Entering :math:`\instr^\ast` with label :math:`L`
.................................................
Expand All @@ -2567,7 +2567,7 @@ Entering :math:`\instr^\ast` with label :math:`L`
because the label :math:`L` is embedded in the :ref:`administrative instruction <syntax-instr-admin>` that structured control instructions reduce to directly.


.. _exec-instr-seq-exit:
.. _exec-instrs-exit:

Exiting :math:`\instr^\ast` with label :math:`L`
................................................
Expand All @@ -2576,7 +2576,7 @@ When the end of a block is reached without a jump or trap aborting it, then the

1. Pop all values :math:`\val^\ast` from the top of the stack.

2. Assert: due to :ref:`validation <valid-instr-seq>`, the label :math:`L` is now on the top of the stack.
2. Assert: due to :ref:`validation <valid-instrs>`, the label :math:`L` is now on the top of the stack.

3. Pop the label from the stack.

Expand Down Expand Up @@ -2626,7 +2626,7 @@ Invocation of :ref:`function reference <syntax-ref.func>` :math:`(\REFFUNCADDR~a

10. Let :math:`L` be the :ref:`label <syntax-label>` whose arity is :math:`m` and whose continuation is the end of the function.

11. :ref:`Enter <exec-instr-seq-enter>` the instruction sequence :math:`\instr^\ast` with label :math:`L`.
11. :ref:`Enter <exec-instrs-enter>` the instruction sequence :math:`\instr^\ast` with label :math:`L`.

$${rule: {Step_read/call_ref-func}}

Expand All @@ -2645,7 +2645,7 @@ When the end of a function is reached without a jump (i.e., |RETURN|) or trap ab

2. Let :math:`n` be the arity of the activation of :math:`F`.

3. Assert: due to :ref:`validation <valid-instr-seq>`, there are :math:`n` values on the top of the stack.
3. Assert: due to :ref:`validation <valid-instrs>`, there are :math:`n` values on the top of the stack.

4. Pop the results :math:`\val^n` from the stack.

Expand Down
4 changes: 2 additions & 2 deletions document/core/exec/modules.rst
Original file line number Diff line number Diff line change
Expand Up @@ -561,7 +561,7 @@ It is up to the :ref:`embedder <embedder>` to define how such conditions are rep

a. Let :math:`n` be the length of the list :math:`\elem_i.\EINIT`.

b. :ref:`Execute <exec-instr-seq>` the instruction sequence :math:`\X{einstr}^\ast_i`.
b. :ref:`Execute <exec-instrs>` the instruction sequence :math:`\X{einstr}^\ast_i`.

c. :ref:`Execute <exec-const>` the instruction :math:`\I32.\CONST~0`.

Expand All @@ -581,7 +581,7 @@ It is up to the :ref:`embedder <embedder>` to define how such conditions are rep

b. Let :math:`n` be the length of the list :math:`\data_i.\DINIT`.

c. :ref:`Execute <exec-instr-seq>` the instruction sequence :math:`\X{dinstr}^\ast_i`.
c. :ref:`Execute <exec-instrs>` the instruction sequence :math:`\X{dinstr}^\ast_i`.

d. :ref:`Execute <exec-const>` the instruction :math:`\I32.\CONST~0`.

Expand Down
2 changes: 1 addition & 1 deletion document/core/exec/runtime.rst
Original file line number Diff line number Diff line change
Expand Up @@ -665,7 +665,7 @@ It unifies the handling of different forms of calls.
Analogously, |RETURNINVOKE| represents the imminent tail invocation of a function instance.

The |LABEL| and |FRAME| instructions model :ref:`labels <syntax-label>` and :ref:`frames <syntax-frame>` :ref:`"on the stack" <exec-notation>`.
Moreover, the administrative syntax maintains the nesting structure of the original :ref:`structured control instruction <syntax-instr-control>` or :ref:`function body <syntax-func>` and their :ref:`instruction sequences <syntax-instr-seq>` with an |END| marker.
Moreover, the administrative syntax maintains the nesting structure of the original :ref:`structured control instruction <syntax-instr-control>` or :ref:`function body <syntax-func>` and their :ref:`instruction sequences <syntax-instrs>` with an |END| marker.
That way, the end of the inner instruction sequence is known when part of an outer sequence.

.. note::
Expand Down
2 changes: 1 addition & 1 deletion document/core/syntax/instructions.rst
Original file line number Diff line number Diff line change
Expand Up @@ -554,7 +554,7 @@ The ${:DATA.DROP} instruction prevents further use of a passive data segment. Th
.. _syntax-return:
.. _syntax-call:
.. _syntax-call_indirect:
.. _syntax-instr-seq:
.. _syntax-instrs:
.. _syntax-instr-control:

Control Instructions
Expand Down
14 changes: 7 additions & 7 deletions document/core/util/macros.def
Original file line number Diff line number Diff line change
Expand Up @@ -280,7 +280,7 @@
.. |globaltype| mathdef:: \xref{syntax/types}{syntax-globaltype}{\X{globaltype}}
.. |tabletype| mathdef:: \xref{syntax/types}{syntax-tabletype}{\X{tabletype}}
.. |memtype| mathdef:: \xref{syntax/types}{syntax-memtype}{\X{memtype}}
.. |datatype| mathdef:: \xref{syntax/types}{syntax-datatype}{\X{datatype}}
.. |datatype| mathdef:: \xref{valid/modules}{syntax-datatype}{\X{datatype}}

.. |limits| mathdef:: \xref{syntax/types}{syntax-limits}{\X{limits}}
.. |mut| mathdef:: \xref{syntax/types}{syntax-mut}{\X{mut}}
Expand Down Expand Up @@ -1205,12 +1205,12 @@
.. |vdashimportdesc| mathdef:: \xref{valid/modules}{valid-importdesc}{\vdash}
.. |vdashmodule| mathdef:: \xref{valid/modules}{valid-module}{\vdash}

.. |OKelemmode| mathdef:: \xref{valid/types}{valid-elemmode}{\K{ok}}
.. |OKdatamode| mathdef:: \xref{valid/types}{valid-datamode}{\K{ok}}
.. |OKdata| mathdef:: \xref{valid/types}{valid-data}{\K{ok}}
.. |OKstart| mathdef:: \xref{valid/types}{valid-start}{\K{ok}}
.. |OKtypes| mathdef:: \xref{valid/types}{valid-types}{\K{ok}}
.. |OKmodule| mathdef:: \xref{valid/types}{valid-module}{\K{ok}}
.. |OKelemmode| mathdef:: \xref{valid/modules}{valid-elemmode}{\K{ok}}
.. |OKdatamode| mathdef:: \xref{valid/modules}{valid-datamode}{\K{ok}}
.. |OKdata| mathdef:: \xref{valid/modules}{valid-data}{\K{ok}}
.. |OKstart| mathdef:: \xref{valid/modules}{valid-start}{\K{ok}}
.. |OKtypes| mathdef:: \xref{valid/modules}{valid-types}{\K{ok}}
.. |OKmodule| mathdef:: \xref{valid/modules}{valid-module}{\K{ok}}

.. |unpackshape| mathdef:: \xref{valid/instructions}{aux-unpackshape}{\F{unpack}}
.. |shlanetype| mathdef:: \xref{syntax/instructions}{aux-lanetype}{\F{lanetype}}
Expand Down
14 changes: 7 additions & 7 deletions document/core/valid/instructions.rst
Original file line number Diff line number Diff line change
Expand Up @@ -15,7 +15,7 @@ In most cases, this is empty.
consuming two ${:I32} values and producing one.
The instruction ${:LOCAL.SET x} has type ${instrtype: t ->_(x) eps}, provided ${:t} is the type declared for the local ${:x}.

Typing extends to :ref:`instruction sequences <valid-instr-seq>` ${:instr*}.
Typing extends to :ref:`instruction sequences <valid-instrs>` ${:instr*}.
Such a sequence has an instruction type ${instrtype: t_1* ->_(x*) t_2*} if the accumulative effect of executing the instructions is consuming values of types ${:t_1*} off the operand stack, pushing new values of types ${:t_2*}, and setting all locals ${:x*}.

.. _polymorphism:
Expand Down Expand Up @@ -1428,7 +1428,7 @@ Control Instructions
* Let :math:`C'` be the same :ref:`context <context>` as :math:`C`, but with the :ref:`result type <syntax-resulttype>` :math:`[t_2^\ast]` prepended to the |CLABELS| list.

* Under context :math:`C'`,
the instruction sequence :math:`\instr^\ast` must be :ref:`valid <valid-instr-seq>` with type :math:`[t_1^\ast] \to [t_2^\ast]`.
the instruction sequence :math:`\instr^\ast` must be :ref:`valid <valid-instrs>` with type :math:`[t_1^\ast] \to [t_2^\ast]`.

* Then the compound instruction is valid with type :math:`[t_1^\ast] \to [t_2^\ast]`.

Expand All @@ -1448,7 +1448,7 @@ $${rule: Instr_ok/block}
* Let :math:`C'` be the same :ref:`context <context>` as :math:`C`, but with the :ref:`result type <syntax-resulttype>` :math:`[t_1^\ast]` prepended to the |CLABELS| list.

* Under context :math:`C'`,
the instruction sequence :math:`\instr^\ast` must be :ref:`valid <valid-instr-seq>` with type :math:`[t_1^\ast] \to [t_2^\ast]`.
the instruction sequence :math:`\instr^\ast` must be :ref:`valid <valid-instrs>` with type :math:`[t_1^\ast] \to [t_2^\ast]`.

* Then the compound instruction is valid with type :math:`[t_1^\ast] \to [t_2^\ast]`.

Expand All @@ -1468,10 +1468,10 @@ $${rule: Instr_ok/loop}
* Let :math:`C'` be the same :ref:`context <context>` as :math:`C`, but with the :ref:`result type <syntax-resulttype>` :math:`[t_2^\ast]` prepended to the |CLABELS| list.

* Under context :math:`C'`,
the instruction sequence :math:`\instr_1^\ast` must be :ref:`valid <valid-instr-seq>` with type :math:`[t_1^\ast] \to [t_2^\ast]`.
the instruction sequence :math:`\instr_1^\ast` must be :ref:`valid <valid-instrs>` with type :math:`[t_1^\ast] \to [t_2^\ast]`.

* Under context :math:`C'`,
the instruction sequence :math:`\instr_2^\ast` must be :ref:`valid <valid-instr-seq>` with type :math:`[t_1^\ast] \to [t_2^\ast]`.
the instruction sequence :math:`\instr_2^\ast` must be :ref:`valid <valid-instrs>` with type :math:`[t_1^\ast] \to [t_2^\ast]`.

* Then the compound instruction is valid with type :math:`[t_1^\ast~\I32] \to [t_2^\ast]`.

Expand Down Expand Up @@ -1771,7 +1771,7 @@ $${rule: Instr_ok/return_call_indirect}


.. index:: instruction, instruction sequence, local type
.. _valid-instr-seq:
.. _valid-instrs:

Instruction Sequences
~~~~~~~~~~~~~~~~~~~~~
Expand Down Expand Up @@ -1849,7 +1849,7 @@ Expressions ${:expr} are classified by :ref:`result types <syntax-resulttype>` $
:math:`\instr^\ast~\END`
........................

* The instruction sequence :math:`\instr^\ast` must be :ref:`valid <valid-instr-seq>` with :ref:`type <syntax-instrtype>` :math:`[] \to [t^\ast]`.
* The instruction sequence :math:`\instr^\ast` must be :ref:`valid <valid-instrs>` with :ref:`type <syntax-instrtype>` :math:`[] \to [t^\ast]`.

* Then the expression is valid with :ref:`result type <syntax-resulttype>` :math:`[t^\ast]`.

Expand Down

0 comments on commit bc21b85

Please sign in to comment.