Skip to content

Commit

Permalink
Convert exec/conventions
Browse files Browse the repository at this point in the history
  • Loading branch information
rossberg committed May 30, 2024
1 parent a835a0e commit 8fb06d0
Show file tree
Hide file tree
Showing 5 changed files with 49 additions and 44 deletions.
38 changes: 15 additions & 23 deletions document/core/exec/conventions.rst
Original file line number Diff line number Diff line change
Expand Up @@ -67,63 +67,55 @@ Formal Notation
The formal execution rules use a standard approach for specifying operational semantics, rendering them into *reduction rules*.
Every rule has the following general form:

.. math::
\X{configuration} \quad\stepto\quad \X{configuration}
$${: configuration ~> configuration}

A *configuration* is a syntactic description of a program state.
Each rule specifies one *step* of execution.
As long as there is at most one reduction rule applicable to a given configuration, reduction -- and thereby execution -- is *deterministic*.
WebAssembly has only very few exceptions to this, which are noted explicitly in this specification.

For WebAssembly, a configuration typically is a tuple :math:`(S; F; \instr^\ast)` consisting of the current :ref:`store <store>` :math:`S`, the :ref:`call frame <frame>` :math:`F` of the current function, and the sequence of :ref:`instructions <syntax-instr>` that is to be executed.
For WebAssembly, a configuration typically is a tuple ${:(s; f; instr*)} consisting of the current :ref:`store <store>` ${:s}, the :ref:`call frame <frame>` ${:f} of the current function, and the sequence of :ref:`instructions <syntax-instr>` that is to be executed.
(A more precise definition is given :ref:`later <syntax-config>`.)

To avoid unnecessary clutter, the store :math:`S` and the frame :math:`F` are omitted from reduction rules that do not touch them.
To avoid unnecessary clutter, the store ${:s} and the frame ${:f} are often combined into a *state* ${:z}, which is a pair ${:(s; f)}.
Moreover, ${:z} is omitted from reduction rules that do not touch them.

There is no separate representation of the :ref:`stack <stack>`.
Instead, it is conveniently represented as part of the configuration's instruction sequence.
In particular, :ref:`values <syntax-val>` are defined to coincide with |CONST| instructions,
and a sequence of |CONST| instructions can be interpreted as an operand "stack" that grows to the right.
In particular, :ref:`values <syntax-val>` are defined to coincide with ${:CONST} instructions,
and a sequence of ${:CONST} instructions can be interpreted as an operand "stack" that grows to the right.

.. note::
For example, the :ref:`reduction rule <exec-binop>` for the :math:`\I32.\ADD` instruction can be given as follows:
For example, the :ref:`reduction rule <exec-binop>` for the ${instr: BINOP I32 ADD} instruction can be given as follows:

.. math::
(\I32.\CONST~n_1)~(\I32.\CONST~n_2)~\I32.\ADD \quad\stepto\quad (\I32.\CONST~(n_1 + n_2) \mod 2^{32})
$${Step_pure: (CONST I32 n_1) (CONST I32 n_2) $($(BINOP I32 ADD)) ~> (CONST I32 $((n_1 + n_2) \ 2^32))}

Per this rule, two |CONST| instructions and the |ADD| instruction itself are removed from the instruction stream and replaced with one new |CONST| instruction.
Per this rule, two ${:CONST} instructions and the ${:ADD} instruction itself are removed from the instruction stream and replaced with one new ${:CONST} instruction.
This can be interpreted as popping two values off the stack and pushing the result.

When no result is produced, an instruction reduces to the empty sequence:

.. math::
\NOP \quad\stepto\quad \epsilon
$${Step_pure: NOP ~> eps}

:ref:`Labels <label>` and :ref:`frames <frame>` are similarly :ref:`defined <syntax-instr-admin>` to be part of an instruction sequence.

The order of reduction is determined by the definition of an appropriate :ref:`evaluation context <syntax-ctxt-eval>`.

Reduction *terminates* when no more reduction rules are applicable.
:ref:`Soundness <soundness>` of the WebAssembly :ref:`type system <type-system>` guarantees that this is only the case when the original instruction sequence has either been reduced to a sequence of |CONST| instructions, which can be interpreted as the :ref:`values <syntax-val>` of the resulting operand stack,
:ref:`Soundness <soundness>` of the WebAssembly :ref:`type system <type-system>` guarantees that this is only the case when the original instruction sequence has either been reduced to a sequence of ${:CONST} instructions, which can be interpreted as the :ref:`values <syntax-val>` of the resulting operand stack,
or if a :ref:`trap <syntax-trap>` occurred.

.. note::
For example, the following instruction sequence,

.. math::
(\F64.\CONST~x_1)~(\F64.\CONST~x_2)~\F64.\NEG~(\F64.\CONST~x_3)~\F64.\ADD~\F64.\MUL
$${instr*: (CONST F64 q_1) (CONST F64 q_2) $($(UNOP F64 NEG)) (CONST F64 q_3) $($(BINOP F64 ADD)) $($(BINOP F64 MUL))}

terminates after three steps:

.. math::
\begin{array}{ll}
& (\F64.\CONST~x_1)~(\F64.\CONST~x_2)~\F64.\NEG~(\F64.\CONST~x_3)~\F64.\ADD~\F64.\MUL \\
\stepto & (\F64.\CONST~x_1)~(\F64.\CONST~x_4)~(\F64.\CONST~x_3)~\F64.\ADD~\F64.\MUL \\
\stepto & (\F64.\CONST~x_1)~(\F64.\CONST~x_5)~\F64.\MUL \\
\stepto & (\F64.\CONST~x_6) \\
\end{array}
$${rule: {NotationReduct/*}}
$${relation-ignore: NotationReduct}
where :math:`x_4 = -x_2` and :math:`x_5 = -x_2 + x_3` and :math:`x_6 = x_1 \cdot (-x_2 + x_3)`.
where ${:q_4 = $(-q_2)} and ${:q_5 = $(-q_2 + q_3)} and ${:q_6 = $(q_1 * (-q_2 + q_3))}.


.. [#cite-pldi2017]
Expand Down
1 change: 0 additions & 1 deletion document/core/util/macros.def
Original file line number Diff line number Diff line change
Expand Up @@ -1233,7 +1233,6 @@
.. |vdashdatamode| mathdef:: \xref{valid/modules}{valid-datamode}{\vdash}
.. |vdashstart| mathdef:: \xref{valid/modules}{valid-start}{\vdash}
.. |vdashexport| mathdef:: \xref{valid/modules}{valid-export}{\vdash}
.. |vdashexternidx| mathdef:: \xref{valid/modules}{valid-externidx}{\vdash}
.. |vdashexportdesc| mathdef:: \xref{valid/modules}{valid-exportdesc}{\vdash}
.. |vdashimport| mathdef:: \xref{valid/modules}{valid-import}{\vdash}
.. |vdashimportdesc| mathdef:: \xref{valid/modules}{valid-importdesc}{\vdash}
Expand Down
12 changes: 6 additions & 6 deletions document/core/valid/conventions.rst
Original file line number Diff line number Diff line change
Expand Up @@ -301,8 +301,8 @@ which says that ${:A `: T} holds under the assumptions encoded in ${:C}.
The formal typing rules use a standard approach for specifying type systems, rendering them into *deduction rules*.
Every rule has the following general form:

$${rule: Scheme}
$${relation-ignore: Scheme}
$${rule: NotationTypingScheme}
$${relation-ignore: NotationTypingScheme}

Such a rule is read as a big implication: if all premises hold, then the conclusion holds.
Some rules have no premises; they are *axioms* whose conclusion holds unconditionally.
Expand All @@ -312,15 +312,15 @@ and there is one respective rule for each relevant construct ${:A} of the abstra
.. note::
For example, the typing rule for the ${instr: BINOP I32 ADD} instruction can be given as an axiom:

$${rule: InstrScheme/i32.add}
$${rule: NotationTypingInstrScheme/i32.add}

The instruction is always valid with type ${instrtype: I32 I32 -> I32}
(saying that it consumes two ${numtype: I32} values and produces one),
independent of any side conditions.

An instruction like ${:GLOBAL.GET} can be typed as follows:

$${rule: InstrScheme/global.get}
$${rule: NotationTypingInstrScheme/global.get}

Here, the premise enforces that the immediate :ref:`global index <syntax-globalidx>` ${:x} exists in the context.
The instruction produces a value of its respective type ${:t}
Expand All @@ -331,15 +331,15 @@ and there is one respective rule for each relevant construct ${:A} of the abstra
Finally, a :ref:`structured <syntax-instr-control>` instruction requires
a recursive rule, where the premise is itself a typing judgement:

$${rule: InstrScheme/block}
$${rule: NotationTypingInstrScheme/block}

A ${:BLOCK} instruction is only valid when the instruction sequence in its body is.
Moreover, the result type must match the block's annotation ${:blocktype}.
If so, then the ${:BLOCK} instruction has the same type as the body.
Inside the body an additional label of the corresponding result type is available,
which is expressed by extending the context ${:C} with the additional label information for the premise.

$${relation-ignore: InstrScheme}
$${relation-ignore: NotationTypingInstrScheme}


.. [#cite-pldi2017]
Expand Down
40 changes: 27 additions & 13 deletions spectec/spec/wasm-3.0/C-conventions.watsup
Original file line number Diff line number Diff line change
Expand Up @@ -24,27 +24,41 @@ syntax pth hint(macro none) = PTHSYNTAX hint(show (`[i] `| !%.FIELD)+)

syntax T hint(macro none) = nat

relation Premise: nat
relation Premisedots: `... hint(macro none)
relation Scheme: nat
relation NotationTypingPremise: nat
relation NotationTypingPremisedots: `... hint(macro none)
relation NotationTypingScheme: nat

rule Scheme:
rule NotationTypingScheme:
conclusion
-- Premise: premise_1
-- Premise: premise_2
-- Premisedots: `...
-- Premise: premise_n
-- NotationTypingPremise: premise_1
-- NotationTypingPremise: premise_2
-- NotationTypingPremisedots: `...
-- NotationTypingPremise: premise_n

relation InstrScheme: context |- instr* : functype hint(macro none)
relation NotationTypingInstrScheme: context |- instr* : functype hint(macro none)

rule InstrScheme/i32.add:
rule NotationTypingInstrScheme/i32.add:
C |- BINOP I32 ADD : I32 I32 -> I32

rule InstrScheme/global.get:
rule NotationTypingInstrScheme/global.get:
C |- GLOBAL.GET x : eps -> t
-- if C.GLOBALS[x] = mut t

rule InstrScheme/block:
rule NotationTypingInstrScheme/block:
C |- BLOCK blocktype instr* : t_1* -> t_2*
-- Blocktype_ok: C |- blocktype : t_1* -> t_2*
-- InstrScheme: C, LABELS (t_2*) |- instr* : t_1* -> t_2*
-- NotationTypingInstrScheme: C, LABELS (t_2*) |- instr* : t_1* -> t_2*


;; Execution notation

relation NotationReduct: ~> instr*

rule NotationReduct/2:
~> (CONST F64 q_1) (CONST F64 q_4) (CONST F64 q_3) $($(BINOP F64 ADD)) $($(BINOP F64 MUL))

rule NotationReduct/3:
~> (CONST F64 q_1) (CONST F64 q_5) $($(BINOP F64 MUL))

rule NotationReduct/4:
~> (CONST F64 q_6)
2 changes: 1 addition & 1 deletion spectec/src/backend-latex/render.ml
Original file line number Diff line number Diff line change
Expand Up @@ -830,7 +830,7 @@ let render_binop = function
| SubOp -> "-"
| MulOp -> "\\cdot"
| DivOp -> "/"
| ModOp -> "\\mathbin{mod}"
| ModOp -> "\\mathbin{\\mathrm{mod}}"
| ExpOp -> assert false

let render_cmpop = function
Expand Down

0 comments on commit 8fb06d0

Please sign in to comment.