link operational and axiomatic semantics (todo: coinductive syntax)

Author: conrad-watt

document/core/exec/relaxed.rst

@@ -15,7 +15,18 @@ Relaxed Memory Model
 Traces
 ~~~~~~
 
-.. todo:: define, explain
+.. todo:: novel notation here?
+
+A trace is a coinductive set of :ref:`events <syntax-evt>`. A trace is considered to be a *pre-execution* of a given :ref:`global configuration <syntax-config>` if it can be derived from the events emitted by the coinductive closure of the :ref:`global reduction relation <syntax-reduction>` on that configuration, and all the :ref:`time stamps <syntax-time>` of its constituent events are distinct.
+
+.. math::
+   \frac{
+     \config \stepto^{\evt} \config' \qquad \vdash \config' : \X{tr} \qquad \F{time}(\evt) \notin \F{time}(\X{tr})
+   }{
+     \vdash \config : \evt~\X{tr}
+   }
+
+When a WebAssembly program is executed, all behaviours observed during that execution must correspond to a single :ref:`consistent <relaxed-consistent>` pre-execution of that execution's starting :ref:`configuration <syntax-config>`.
 
 
 .. _relaxed-consistent:

document/core/exec/runtime.rst

@@ -782,6 +782,7 @@ Convention
 
 
 .. index:: ! reduction, configuration, ! termination
+.. _syntax-reduction:
 
 Reduction
 ~~~~~~~~~
@@ -799,7 +800,7 @@ It emits a (possibly empty) set of events that are produced by the corresponding
 Formally, global reduction is a relation
 
 .. math::
-   \config \stepto^{\evt^\ast} \config
+   \config \stepto^{\evt} \config
 
 defined by inductive rewrite rules on global configurations.
 
@@ -823,7 +824,7 @@ The following rule for global reduction describes the creation of a new thread b
 .. math::
    \begin{array}{@{}c@{}}
    S; P_1^\ast~(F; \instr^\ast \AT h)~P_2^\ast
-     \qquad \stepto \qquad
+     \qquad \stepto^{\epsilon~\AT~h'} \qquad
      S'; P_1^\ast~(F'; {\instr'}^\ast \AT h')~P_2^\ast~(\epsilon; (\HOSTE~[\epsilon]) \AT h'') \\
      \qquad
        \begin{array}[t]{@{}r@{~}l@{}}