[spec] i32x4.relaxed_dot_i8x16_i7x16_add_s disagrees with the reference interpreter and the test suite #2311

Summary

The spec defines i32x4.relaxed_dot_i8x16_i7x16_add_s as RELAXED_DOT (the i16x8 relaxed dot product), then EXTADD_PAIRWISE, then ADD (3.2-numerics.vector.spectec L401-L406, numerics.rst L2236-L2252). Since #2252, RELAXED_DOT allows two behaviours (L371-L372, L381-L382). In both, the first operand is read as signed.

• $R_idot = 0 (also the deterministic profile): second operand read as signed, 16-bit pair sums wrapped
• $R_idot = 1: second operand read as unsigned, 16-bit pair sums saturated

RELAXED_DOT_ADD inherits exactly these two. This leads to two mismatches:

1. When a signed pair sum overflows i16, the spec excludes the reference interpreter's result (Example 1). This is new since Fix i16x8.relaxed_dot_i8x16_i7x16_s pairwise add #2252. Before it, RELAXED_DOT always saturated, so (signed, saturated) was allowed, which is what the reference interpreter's dot_add_s implements.
2. The spec excludes two of the four results that relaxed_dot_product.wast accepts (Example 2). This was already the case before Fix i16x8.relaxed_dot_i8x16_i7x16_s pairwise add #2252.

Example 1: the reference interpreter's result is outside the spec

(module
  (func (export "dot") (result v128)
    (i32x4.relaxed_dot_i8x16_i7x16_add_s
      (v128.const i8x16 -128 -128 -128 -128 0 0 0 0 0 0 0 0 0 0 0 0)   ;; a
      (v128.const i8x16 -128 -128 -128 -128 0 0 0 0 0 0 0 0 0 0 0 0)   ;; b
      (v128.const i32x4 0 0 0 0))))                                    ;; c
(invoke "dot")

This input is not from the test suite. It differs from the add_s case at relaxed_dot_product.wast L82-L90 only in b (-128 instead of -127). With b = -127, a signed pair sum is 32512 and fits in i16, so none of the add_s tests has a signed pair sum that overflows.

Lane 0 is the sum of two pair sums, each (-128)·b + (-128)·b:

So the spec allows only -65536, for either value of $R_idot. The reference interpreter prints 65_534 0 0 0 : [v128]. Its i16x8 dot_s (v128.ml L387-L396) wraps, which matches $R_idot = 0. Only dot_add_s saturates.

Example 2: results listed in the test suite are not allowed

relaxed_dot_product.wast L76-L90 accepts four results in lane 0 for a = -128 ×4, b = -127 ×4, c = (1, 2, 3, 4):

-66047 needs an unsigned b with a pair sum wider than 16 bits. 66049 reads a as unsigned, which the proposal pseudo-code does not allow either (lhs = as_signed(a[i])).

The test passes on both the SpecTec interpreter and the reference interpreter, which both return 65025. An either assertion only checks that the result is in the list. It does not check that every listed result is allowed by the spec.

Questions

1. Is the 16-bit intermediate part of the intended semantics? In the proposal pseudo-code, each pair sum tmp is either the plain sum or the sum saturated to i16, but the width of tmp is not stated. If tmp is 16 bits, the plain sum wraps (-65536 in Example 1). If it is wider, it stays exact (65536, as with SDOT/VPDPBSSD). The spec takes the 16-bit reading, and so do the tests proposed in test/relaxed_dot: add i16-intermediate overflow boundary cases #2228.
2. Depending on the answer, which should change?
   • the allowed results of RELAXED_DOT_ADD (e.g. add signed + saturate, and possibly the exact sum)
   • the reference interpreter's dot_add_s (e.g. wrap, as its i16x8 dot_s does)
   • the either list in relaxed_dot_product.wast: -66047 (if the 16-bit intermediate is intended) and 66049 (which the proposal does not allow)

cc @brendandahl, since you mentioned in #2252 that there are also issues with i32x4.relaxed_dot_i8x16_i7x16_add_s to address in a separate PR.