From 8fb06d0cb5f142a254b17119534268d4ac30f61e Mon Sep 17 00:00:00 2001 From: Andreas Rossberg Date: Thu, 30 May 2024 16:38:01 +0200 Subject: [PATCH] Convert exec/conventions --- document/core/exec/conventions.rst | 38 ++++++++------------ document/core/util/macros.def | 1 - document/core/valid/conventions.rst | 12 +++---- spectec/spec/wasm-3.0/C-conventions.watsup | 40 +++++++++++++++------- spectec/src/backend-latex/render.ml | 2 +- 5 files changed, 49 insertions(+), 44 deletions(-) diff --git a/document/core/exec/conventions.rst b/document/core/exec/conventions.rst index 469350417b..b57de6d47a 100644 --- a/document/core/exec/conventions.rst +++ b/document/core/exec/conventions.rst @@ -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 ` :math:`S`, the :ref:`call frame ` :math:`F` of the current function, and the sequence of :ref:`instructions ` that is to be executed. +For WebAssembly, a configuration typically is a tuple ${:(s; f; instr*)} consisting of the current :ref:`store ` ${:s}, the :ref:`call frame ` ${:f} of the current function, and the sequence of :ref:`instructions ` that is to be executed. (A more precise definition is given :ref:`later `.) -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 `. Instead, it is conveniently represented as part of the configuration's instruction sequence. -In particular, :ref:`values ` 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 ` 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 ` for the :math:`\I32.\ADD` instruction can be given as follows: + For example, the :ref:`reduction rule ` 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