Fill out spec text for new instructions

Done to the best of my ability understanding how the spec all works.
Probably needs editing/spot-checking.

README.md

@@ -8,6 +8,9 @@ support for wide arithmetic instructions for WebAssembly.
 * See the [overview](./proposals/wide-arithmetic/Overview.md) for a
   high-level summary and rationale of the proposal.
 
+* See the [modified spec](https://webassembly.github.io/wide-arithmetic/core/)
+  for the formalization of this proposal.
+
 Original README from upstream repository follows...
 
 --------------------------------------------------------------------------------

document/core/binary/instructions.rst

@@ -461,6 +461,18 @@ whereas the actual opcode is encoded by a variable-length :ref:`unsigned integer
      \hex{FC}~~7{:}\Bu32 &\Rightarrow& \I64.\TRUNC\K{\_sat\_}\F64\K{\_u} \\
    \end{array}
 
+Wide arithmetic instructions are encoded similarly to saturating instructions
+above.
+
+.. math::
+   \begin{array}{llclll}
+   \production{instruction} & \Binstr &::=& \dots && \phantom{thisshouldbeenough} \\&&|&
+     \hex{FC}~~19{:}\Bu32 &\Rightarrow& \I64.\ADD128 \\ &&|&
+     \hex{FC}~~20{:}\Bu32 &\Rightarrow& \I64.\SUB128 \\ &&|&
+     \hex{FC}~~21{:}\Bu32 &\Rightarrow& \I64.\MULWIDE\K{\_s} \\ &&|&
+     \hex{FC}~~22{:}\Bu32 &\Rightarrow& \I64.\MULWIDE\K{\_u} \\
+   \end{array}
+
 
 .. index:: vector instruction
    pair: binary format; instruction

document/core/exec/instructions.rst

@@ -181,6 +181,80 @@ Where the underlying operators are non-deterministic, because they may return on
      & (\iff \cvtop^{\sx^?}_{t_1,t_2}(c_1) = \{\})
    \end{array}
 
+.. _exec-binop128:
+
+:math:`\I64\K{.}\binop\K{128}`
+..........................................
+
+1. Assert: due to :ref:`validation <valid-binop128>`, four values of :ref:`value type <syntax-valtype>` :math:`\I64` are on the top of the stack.
+
+2. Pop the value :math:`\I64.\CONST~c_4` from the stack.
+
+3. Pop the value :math:`\I64.\CONST~c_3` from the stack.
+
+4. Pop the value :math:`\I64.\CONST~c_2` from the stack.
+
+5. Pop the value :math:`\I64.\CONST~c_1` from the stack.
+
+6. Let :math:`l` be the result of computing :math:`\iconcat_\K{64,128}(c_1, c_2)`
+
+7. Let :math:`r` be the result of computing :math:`\iconcat_\K{64,128}(c_3, c_4)`
+
+8. Let :math:`c` be the result of computing :math:`\binopF_\K{i128}(l, r)`
+
+9. Let :math:`c_l, c_h` be the result of computing :math:`\isplit_\K{128,64}(c)`
+
+10. Push the value :math:`\I64.\CONST~c_l` to the stack.
+
+11. Push the value :math:`\I64.\CONST~c_h` to the stack.
+
+.. math::
+   \begin{array}{lcl@{\qquad}l}
+   (\I64\K{.}\CONST~c_1)~
+   (\I64\K{.}\CONST~c_2)~
+   (\I64\K{.}\CONST~c_3)~
+   (\I64\K{.}\CONST~c_4)~
+   \I64\K{.}\binop\K{128}
+     &\stepto&
+     (\I64\K{.}\CONST~c_l)~
+     (\I64\K{.}\CONST~c_h)
+     & (\iff c_l, c_h = \isplit_\K{128,64}(\binop_\K{i128}(\iconcat_\K{64,128}(c_1, c_2), \iconcat_\K{64,128}(c_3, c_4))) \\
+   \end{array}
+
+:math:`\I64\K{.}\MULWIDE\K{\_}\sx`
+..........................................
+
+1. Assert: due to :ref:`validation <valid-binop128>`, two values of :ref:`value type <syntax-valtype>` :math:`\I64` are on the top of the stack.
+
+2. Pop the value :math:`\I64.\CONST~c_2` from the stack.
+
+3. Pop the value :math:`\I64.\CONST~c_1` from the stack.
+
+4. Let :math:`l` be the result of computing :math:`\extend^{sx}_{\K{i64},\K{i128}}(c_1)`
+
+5. Let :math:`r` be the result of computing :math:`\extend^{sx}_{\K{i64},\K{i128}}(c_2)`
+
+5. Let :math:`c` be the result of computing :math:`\imul_\K{128}(l, r)`
+
+6. Let :math:`c_l, c_h` be the result of computing :math:`\isplit_\K{128,64}(c)`
+
+7. Push the value :math:`\I64.\CONST~c_l` to the stack.
+
+8. Push the value :math:`\I64.\CONST~c_h` to the stack.
+
+.. math::
+   \begin{array}{lcl@{\qquad}l}
+   (\I64\K{.}\CONST~c_1)~
+   (\I64\K{.}\CONST~c_2)~
+   \I64\K{.}\MULWIDE\K{\_}\sx
+     &\stepto&
+     (\I64\K{.}\CONST~c_l)~
+     (\I64\K{.}\CONST~c_h)
+     & (\iff c_l, c_h = \isplit_\K{128,64}(\imul_\K{128}(
+          \extend^{sx}_{\K{i64},\K{i128}}(c_1),
+          \extend^{sx}_{\K{i64},\K{i128}}(c_2)))) \\
+   \end{array}
+
 
 .. index:: reference instructions, reference
    pair: execution; instruction

document/core/exec/numerics.rst

@@ -1767,9 +1767,9 @@ Conversions
 :math:`\truncu_{M,N}(z)`
 ........................
 
-* If :math:`z` is a NaN, then the result is undefined. 
+* If :math:`z` is a NaN, then the result is undefined.
 
-* Else if :math:`z` is an infinity, then the result is undefined. 
+* Else if :math:`z` is an infinity, then the result is undefined.
 
 * Else if :math:`z` is a number and :math:`\trunc(z)` is a value within range of the target type, then return that value.
 
@@ -1793,9 +1793,9 @@ Conversions
 :math:`\truncs_{M,N}(z)`
 ........................
 
-* If :math:`z` is a NaN, then the result is undefined. 
+* If :math:`z` is a NaN, then the result is undefined.
 
-* Else if :math:`z` is an infinity, then the result is undefined. 
+* Else if :math:`z` is an infinity, then the result is undefined.
 
 * If :math:`z` is a number and :math:`\trunc(z)` is a value within range of the target type, then return that value.
 
@@ -1973,3 +1973,35 @@ Conversions
    \begin{array}{lll@{\qquad}l}
    \narrowu_{M,N}(i) &=& \satu_N(\signed_M(i))
    \end{array}
+
+
+.. _op-iconcat:
+
+:math:`\iconcat_{M,N}(i_1, i_2)`
+.................................
+
+* Let :math:`h` be the result of :math:`\ishl_N(\extend^u_{M,N}(i_2), M)`
+
+* Return the result of :math:`\ior_N(\extend^u_{M,N}(i_1), h)`
+
+.. math::
+   \begin{array}{lll@{\qquad}l}
+   \iconcat_{M,N}(i_1, i_2) &=& \ior_N(\extend^u_{M,N}(i_1), \ishl_N(\extend^u_{M,N}(i_2), M))
+   \end{array}
+
+
+.. _op-isplit:
+
+:math:`\isplit_{M,N}(i)`
+.................................
+
+* Let :math:`l` be the result of :math:`\wrap_{M,N}(i)`
+
+* Let :math:`h` be the result of :math:`\wrap_{M,N}(\ishru_M(i, N))`
+
+* Return :math:`l, h`
+
+.. math::
+   \begin{array}{lll@{\qquad}l}
+   \isplit_{M,N}(i) &=& \wrap_{M,N}(i), \wrap_{M,N}(\ishru_M(i, N))
+   \end{array}

document/core/syntax/instructions.rst

@@ -66,6 +66,8 @@ These operations closely match respective operations available in hardware.
      \K{f}\X{nn}\K{.}\CONVERT\K{\_i}\X{mm}\K{\_}\sx \\&&|&
      \K{i}\X{nn}\K{.}\REINTERPRET\K{\_f}\X{nn} ~|~
      \K{f}\X{nn}\K{.}\REINTERPRET\K{\_i}\X{nn} \\&&|&
+     \K{i64.}\binop\K{128} ~|~
+     \K{i64.}\MULWIDE\K{\_}\sx \\&&|&
      \dots \\
    \production{integer unary operator} & \iunop &::=&
      \K{clz} ~|~
@@ -88,9 +90,9 @@ These operations closely match respective operations available in hardware.
      \K{abs} ~|~
      \K{neg} ~|~
      \K{sqrt} ~|~
-     \K{ceil} ~|~ 
-     \K{floor} ~|~ 
-     \K{trunc} ~|~ 
+     \K{ceil} ~|~
+     \K{floor} ~|~
+     \K{trunc} ~|~
      \K{nearest} \\
    \production{floating-point binary operator} & \fbinop &::=&
      \K{add} ~|~

document/core/text/instructions.rst

@@ -537,6 +537,15 @@ Numeric Instructions
      \text{i64.extend32\_s} &\Rightarrow& \I64.\EXTEND\K{32\_s} \\
    \end{array}
 
+.. math::
+   \begin{array}{llclll}
+   \phantom{\production{instruction}} & \phantom{\Tplaininstr_I} &\phantom{::=}& \phantom{thisisenough} && \phantom{thisshouldbeenough} \\[-2ex] &&|&
+     \text{i64.add128} &\Rightarrow& \I64.\ADD128 \\ &&|&
+     \text{i64.sub128} &\Rightarrow& \I64.\SUB128 \\ &&|&
+     \text{i64.mul\_wide\_s} &\Rightarrow& \I64.\MULWIDE\K{\_s} \\ &&|&
+     \text{i64.mul\_wide\_u} &\Rightarrow& \I64.\MULWIDE\K{\_u} \\
+   \end{array}
+
 
 .. index:: vector instruction
    pair: text format; instruction

document/core/util/macros.def

@@ -439,6 +439,10 @@
 .. |DEMOTE| mathdef:: \xref{syntax/instructions}{syntax-instr-numeric}{\K{demote}}
 .. |REINTERPRET| mathdef:: \xref{syntax/instructions}{syntax-instr-numeric}{\K{reinterpret}}
 
+.. |ADD128| mathdef:: \xref{syntax/instructions}{syntax-instr-numeric}{\K{add128}}
+.. |SUB128| mathdef:: \xref{syntax/instructions}{syntax-instr-numeric}{\K{sub128}}
+.. |MULWIDE| mathdef:: \xref{syntax/instructions}{syntax-instr-numeric}{\K{mul\_wide}}
+
 .. |VCONST| mathdef:: \xref{syntax/instructions}{syntax-instr-vec}{\K{const}}
 .. |SHUFFLE| mathdef:: \xref{syntax/instructions}{syntax-instr-vec}{\K{shuffle}}
 .. |SWIZZLE| mathdef:: \xref{syntax/instructions}{syntax-instr-vec}{\K{swizzle}}
@@ -1176,6 +1180,8 @@
 .. |narrow| mathdef:: \xref{exec/numerics}{op-narrow_u}{\F{narrow}}
 .. |narrowu| mathdef:: \xref{exec/numerics}{op-narrow_u}{\F{narrow}^{\K{u}}}
 .. |narrows| mathdef:: \xref{exec/numerics}{op-narrow_s}{\F{narrow}^{\K{s}}}
+.. |isplit| mathdef:: \xref{exec/numerics}{op-isplit}{\F{isplit}}
+.. |iconcat| mathdef:: \xref{exec/numerics}{op-iconcat}{\F{iconcat}}
 
 
 .. Numerics, meta functions

document/core/valid/instructions.rst

@@ -189,6 +189,30 @@ Numeric Instructions
      C \vdashinstr t_2\K{.}\cvtop\K{\_}t_1\K{\_}\sx^? : [t_1] \to [t_2]
    }
 
+.. _valid-binop128:
+
+:math:`\I64\K{.}\binop\K{128}`
+..........................................
+
+* The instruction is valid with type :math:`[\I64~\I64~\I64~\I64] \to [\I64~\I64]`.
+
+.. math::
+   \frac{
+   }{
+     C \vdashinstr t\K{.}\binop\K{128} : [\I64~\I64~\I64~\I64] \to [\I64~\I64]
+   }
+
+:math:`\I64\K{.}\MULWIDE\K{\_}\sx`
+..........................................
+
+* The instruction is valid with type :math:`[\I64~\I64] \to [\I64~\I64]`.
+
+.. math::
+   \frac{
+   }{
+     C \vdashinstr t\K{.}\MULWIDE\K{\_}\sx : [\I64~\I64] \to [\I64~\I64]
+   }
+
 
 .. index:: reference instructions, reference type
    pair: validation; instruction