Merge remote-tracking branch 'spec/wasm-3.0'

Author: backes

document/core/exec/instructions.rst

@@ -1601,6 +1601,21 @@ Most other vector instructions are defined in terms of numeric operators that ar
    :math:`\lanes_{\K{i32x4}}(v_1)` and :math:`\lanes_{\K{i32x4}}(v_2)`
    respectively.
 
+For non-deterministic operators this definition is generalized to sets:
+
+.. math::
+   \begin{array}{lll}
+   \X{op}_{t\K{x}N}(n_1,\dots,n_k) &=&
+     \{ \lanes^{-1}_{t\K{x}N}(i^\ast) ~|~ i^\ast \in \Large\times\xref{Step_pure/instructions}{exec-instr-numeric}{\X{op}}_t(i_1,\dots,i_k)^\ast \land i_1^\ast = \lanes_{t\K{x}N}(n_1) \land \dots \land i_k^\ast = \lanes_{t\K{x}N}(n_k) \} \\
+   \end{array}
+
+where :math:`\Large\times \{x^\ast\}^N` transforms a sequence of :math:`N` sets of values into a set of sequences of :math:`N` values by computing the set product:
+
+.. math::
+   \begin{array}{lll}
+   \Large\times (S_1 \dots S_N) &=& \{ x_1 \dots x_N ~|~ x_1 \in S_1 \land \dots \land x_N \in S_N \}
+   \end{array}
+
 
 .. _exec-vconst:
 
@@ -2335,9 +2350,9 @@ where:
 
 3. Pop the value :math:`\V128.\VCONST~c_1` from the stack.
 
-4. Let :math:`(i_1~i_2)^8` be the result of computing :math:`\irelaxeddotmul_{8, 16}(\lanes_{\I8X16}(c_1), \lanes_{\I8X16}(c_2))`
+4. Let :math:`(i_1~i_2)^8` be the result of computing :math:`\irelaxeddotmul_{8,16}(\lanes_{\I8X16}(c_1), \lanes_{\I8X16}(c_2))`
 
-5. Let :math:`j^8` be the result of computing :math:`\sats_{16}(i_1 + i_2)^8`.
+5. Let :math:`j^8` be the result of computing :math:`\iaddsats_{16}(i_1, i_2)^8`.
 
 6. Let :math:`c` be the result of computing :math:`\lanes^{-1}_{\I16X8}(j^8)`.
 
@@ -2351,7 +2366,7 @@ where:
    \\ \qquad
      \begin{array}[t]{@{}r@{~}l@{}}
      (\iff & (i_1~i_2)^8 = \irelaxeddotmul_{8,16}(\lanes_{\I8X16}(c_1), \lanes_{\I8X16}(c_2)) \\
-     \wedge & j^8 = \sats_{16}(i_1, i_2)^8 \\
+     \wedge & j^8 = \iaddsats_{16}(i_1, i_2)^8 \\
      \wedge & c = \lanes^{-1}_{\I16X8}(j^8))
      \end{array}
    \end{array}
@@ -2370,11 +2385,11 @@ where:
 
 4. Pop the value :math:`\V128.\VCONST~c_1` from the stack.
 
-5. Let :math:`(i_1~i_2)^8` be the result of computing :math:`\irelaxeddotmul_{8, 16}(\lanes_{\I8X16}(c_1), \lanes_{\I8X16}(c_2))`
+5. Let :math:`(i_1~i_2)^8` be the result of computing :math:`\irelaxeddotmul_{8,16}(\lanes_{\I8X16}(c_1), \lanes_{\I8X16}(c_2))`
 
-6. Let :math:`(j_1~j_2)^4` be the result of computing :math:`\sats_{16}(i_1 + i_2)^8`.
+6. Let :math:`(j_1~j_2)^4` be the result of computing :math:`\iaddsats_{16}(i_1, i_2)^8`.
 
-7. Let :math:`j^4` be the result of computing :math:`\iadd_{32}(\extend^{s}_{16, 32}(j_1), \extend^{s}_{16, 32}(j_2))^4`.
+7. Let :math:`j^4` be the result of computing :math:`\iadd_{32}(\extends_{16,32}(j_1), \extends_{16,32}(j_2))^4`.
 
 8. Let :math:`k^4` be the result of computing :math:`\lanes_{\I32X4}(c_3)`.
 
@@ -2392,8 +2407,8 @@ where:
    \\ \qquad
      \begin{array}[t]{@{}r@{~}l@{}}
      (\iff & (i_1~i_2)^8 = \irelaxeddotmul_{8,16}(\lanes_{\I8X16}(c_1), \lanes_{\I8X16}(c_2)) \\
-     \wedge & (j_1~j_2)^4 = \sats_{16}(i_1 + i_2)^8 \\
-     \wedge & j^4 = \iadd_{32}(\extend^{s}_{16, 32}(j_1), \extend^{s}_{16, 32}(j_2))^4 \\
+     \wedge & (j_1~j_2)^4 = \iaddsats_{16}(i_1, i_2)^8 \\
+     \wedge & j^4 = \iadd_{32}(\extends_{16,32}(j_1), \extends_{16,32}(j_2))^4 \\
      \wedge & k^4 = \lanes_{\I32X4}(c_3) \\
      \wedge & l^4 = \iadd_{32}(j, k)^4 \\
      \wedge & c = \lanes^{-1}_{\I32X4}(l^4))

document/core/exec/numerics.rst

@@ -88,17 +88,17 @@ Conventions:
 
     .. math::
        \begin{array}{lll@{\qquad}l}
-       \satu_N(i) &=& 2^N-1 & (\iff i > 2^N-1)\\
        \satu_N(i) &=& 0 & (\iff i < 0) \\
+       \satu_N(i) &=& 2^N-1 & (\iff i > 2^N-1)\\
        \satu_N(i) &=& i & (\otherwise) \\
        \end{array}
 
   * Signed saturation, :math:`\sats_N(i)` clamps :math:`i` to between :math:`-2^{N-1}` and :math:`2^{N-1}-1`:
 
   .. math::
      \begin{array}{lll@{\qquad}l}
-     \sats_N(i) &=& \signed_N^{-1}(-2^{N-1}) & (\iff i < -2^{N-1})\\
-     \sats_N(i) &=& \signed_N^{-1}(2^{N-1}-1) & (\iff i > 2^{N-1}-1)\\
+     \sats_N(i) &=& -2^{N-1} & (\iff i < -2^{N-1})\\
+     \sats_N(i) &=& 2^{N-1}-1 & (\iff i > 2^{N-1}-1)\\
      \sats_N(i) &=& i & (\otherwise)
      \end{array}
 
@@ -860,11 +860,11 @@ The integer result of predicates -- i.e., :ref:`tests <syntax-testop>` and :ref:
 
 * Let :math:`j` be the result of adding :math:`j_1` and :math:`j_2`.
 
-* Return :math:`\sats_N(j)`.
+* Return the value whose signed interpretation is :math:`\sats_N(j)`.
 
 .. math::
    \begin{array}{lll@{\qquad}l}
-   \iaddsats_N(i_1, i_2) &=& \sats_N(\signed_N(i_1) + \signed_N(i_2))
+   \iaddsats_N(i_1, i_2) &=& \signed_N^{-1}(\sats_N(\signed_N(i_1) + \signed_N(i_2)))
    \end{array}
 
 
@@ -894,11 +894,11 @@ The integer result of predicates -- i.e., :ref:`tests <syntax-testop>` and :ref:
 
 * Let :math:`j` be the result of subtracting :math:`j_2` from :math:`j_1`.
 
-* Return :math:`\sats_N(j)`.
+* Return the value whose signed interpretation is :math:`\sats_N(j)`.
 
 .. math::
    \begin{array}{lll@{\qquad}l}
-   \isubsats_N(i_1, i_2) &=& \sats_N(\signed_N(i_1) - \signed_N(i_2))
+   \isubsats_N(i_1, i_2) &=& \signed_N^{-1}(\sats_N(\signed_N(i_1) - \signed_N(i_2)))
    \end{array}
 
 
@@ -922,11 +922,11 @@ The integer result of predicates -- i.e., :ref:`tests <syntax-testop>` and :ref:
 :math:`\iq15mulrsats_N(i_1, i_2)`
 .................................
 
-* Return the result of :math:`\sats_N(\ishrs_N(i_1 \cdot i_2 + 2^{14}, 15))`.
+* Return the whose signed interpretation is the result of :math:`\sats_N(\ishrs_N(i_1 \cdot i_2 + 2^{14}, 15))`.
 
 .. math::
    \begin{array}{lll@{\qquad}l}
-   \iq15mulrsats_N(i_1, i_2) &=& \sats_N(\ishrs_N(i_1 \cdot i_2 + 2^{14}, 15))
+   \iq15mulrsats_N(i_1, i_2) &=& \signed_N^{-1}(\sats_N(\ishrs_N(i_1 \cdot i_2 + 2^{14}, 15)))
    \end{array}
 
 
@@ -1901,14 +1901,14 @@ Conversions
 
 * Else if :math:`z` is positive infinity, then return :math:`2^{N-1} - 1`.
 
-* Else, return :math:`\sats_N(\trunc(z))`.
+* Else, return the value whose signed interpretation is :math:`\sats_N(\trunc(z))`.
 
 .. math::
    \begin{array}{lll@{\qquad}l}
    \truncsats_{M,N}(\pm \NAN(n)) &=& 0 \\
    \truncsats_{M,N}(- \infty) &=& -2^{N-1} \\
    \truncsats_{M,N}(+ \infty) &=& 2^{N-1}-1 \\
-   \truncsats_{M,N}(z) &=& \sats_N(\trunc(z)) \\
+   \truncsats_{M,N}(z) &=& \signed_N^{-1}(\sats_N(\trunc(z))) \\
    \end{array}
 
 
@@ -2006,11 +2006,11 @@ Conversions
 
 * Let :math:`j` be the :ref:`signed interpretation <aux-signed>` of :math:`i` of size :math:`M`.
 
-* Return :math:`\sats_N(j)`.
+* Return the value whose signed interpretation is :math:`\sats_N(j)`.
 
 .. math::
    \begin{array}{lll@{\qquad}l}
-   \narrows_{M,N}(i) &=& \sats_N(\signed_M(i))
+   \narrows_{M,N}(i) &=& \signed_N^{-1}(\sats_N(\signed_M(i)))
    \end{array}
 
 
@@ -2163,11 +2163,11 @@ This is an auxiliary operator for the specification of |RELAXEDDOT|.
 
 The implementation-specific behaviour of this operation is determined by the global parameter :math:`R_{\F{idot}} \in \{0, 1\}`.
 
-* Return :math:`\relaxed(R_{\F{idot}})[ \imul_N(\extends_{M,N}(i_1), extends_{M,N}), \imul_N(\extends_{M,N}(i_1), \extendu_{M,N}(i_2)) ]`.
+* Return :math:`\relaxed(R_{\F{idot}})[ \imul_N(\extends_{M,N}(i_1), \extends_{M,N}(i_2)), \imul_N(\extends_{M,N}(i_1), \extendu_{M,N}(i_2)) ]`.
 
 .. math::
    \begin{array}{@{}lcll}
-   \irelaxeddotmul_{M,N}(i_1, i_2) &=& \relaxed(R_{\F{idot}})[ \imul_N(\extends_{M,N}(i_1), extends_{M,N}), \imul_N(\extends_{M,N}(i_1), \extendu_{M,N}(i_2)) ] \\
+   \irelaxeddotmul_{M,N}(i_1, i_2) &=& \relaxed(R_{\F{idot}})[ \imul_N(\extends_{M,N}(i_1), \extends_{M,N}(i_2)), \imul_N(\extends_{M,N}(i_1), \extendu_{M,N}(i_2)) ] \\
    \end{array}
 
 .. note::
@@ -2220,7 +2220,7 @@ The implementation-specific behaviour of this operation is determined by the glo
 .. note::
    Relaxed unsigned truncation is implementation-dependent for NaNs and out-of-range values.
    In the :ref:`deterministic profile <profile-deterministic>`,
-   it behaves like regular :math:`\truncu`.
+   it behaves like regular :math:`\truncsatu`.
 
 
 .. _op-relaxed_trunc_s:
@@ -2243,7 +2243,7 @@ The implementation-specific behaviour of this operation is determined by the glo
 .. note::
    Relaxed signed truncation is implementation-dependent for NaNs and out-of-range values.
    In the :ref:`deterministic profile <profile-deterministic>`,
-   it behaves like regular :math:`\truncs`.
+   it behaves like regular :math:`\truncsats`.
 
 
 .. _op-irelaxed_swizzle:

interpreter/script/js.ml

@@ -236,7 +236,7 @@ let env () : env =
 let current_mod (env : env) = "$$" ^ string_of_int env.current_mod
 let of_mod_opt (env : env) = function
   | None -> current_mod env
-  | Some x -> x.it
+  | Some x -> "$" ^ x.it
 
 let current_inst (env : env) = "$" ^ string_of_int env.current_inst
 let of_inst_opt (env : env) = function
@@ -622,9 +622,6 @@ let rec of_definition def =
     try of_definition (snd (Parse.Module.parse_string ~offset:s.at s.it))
     with Parse.Syntax _ | Custom.Syntax _ -> of_bytes "<malformed quote>"
 
-let of_instance env x_opt =
-  "instance(" ^ of_mod_opt env x_opt ^ ")"
-
 let of_wrapper env x_opt name wrap_action wrap_assertion at =
   let x = of_inst_opt env x_opt in
   let bs = wrap name wrap_action wrap_assertion at in
@@ -677,9 +674,9 @@ let of_assertion env ass =
   | AssertInvalidCustom (def, _) ->
     "assert_invalid_custom(" ^ of_definition def ^ ");"
   | AssertUnlinkable (x_opt, _) ->
-    "assert_unlinkable(" ^ of_instance env x_opt ^ ");"
+    "assert_unlinkable(" ^ of_mod_opt env x_opt ^ ");"
   | AssertUninstantiable (x_opt, _) ->
-    "assert_uninstantiable(" ^ of_instance env x_opt ^ ");"
+    "assert_uninstantiable(" ^ of_mod_opt env x_opt ^ ");"
   | AssertReturn (act, ress) ->
     of_assertion' env act "assert_return" (List.map of_result ress)
       (Some (assert_return ress))
@@ -702,7 +699,7 @@ let of_command env cmd =
       | Quoted (_, s) ->
         unquote (snd (Parse.Module.parse_string ~offset:s.at s.it))
     in bind_mod env x_opt (unquote def);
-    "let " ^ current_mod env ^ " = " ^ of_definition def ^ ";\n" ^
+    "let " ^ current_mod env ^ " = module(" ^ of_definition def ^ ");\n" ^
     (if x_opt = None then "" else
     "let " ^ of_mod_opt env x_opt ^ " = " ^ current_mod env ^ ";\n")
   | Instance (x1_opt, x2_opt) ->