[spec] Fix extmul & extadd execution

[702fbtngus]

At step 11 of the definition of extmul (below image), there is an expression $\text{imul}_{t_2 \times N}(k_1^*, k_2^*)$.

First solution

I guess it should be $\text{imul}_{|t_2|} (k_1^*, k_2^*)$.
The underscored argument of $\text{imul}$, which is $t_2 \times N$ is typed wrong. From the definition of $\text{imul}$, its argument should be an integer.

Here, from line 12, $k^*$ should be a sequence of length $N$ with its elements typed $t_2$. So I think the argument should be $|t_2|$.
Same problem occurs in the definition of extadd (below image).

I think the expression $\text{iadd}_N(j_1, j_2)^*$ at step 6 should be $\text{iadd}_{|t_2|} (j_1, j_2)^*$ instead, and fixed the document.

Second solution

Another solution (which I'm not so sure of) could be using the lane-wise applying notation.

With this notation, $\text{lanes}_{t_2 \times N}^{-1}(\text{imul}_{t_2 \times N} (k_1^*, k_2^*))$ from extmul can be replaced by $\text{mul}_{t_2 \times N} (k_1^*, k_2^*)$, and $\text{lanes}_{t_2 \times N}^{-1}(\text{iadd}_N(j_1, j_2)^*)$ from extadd by $\text{add}_{t_2 \times N}(j_1, j_2)^*$.

I'm not sure about the second solution nor which one is better, so I applied the first one to the document for now.

[rossberg]

Looks good to me, thanks!