defined integer behavior for OpCooperativeMatrixMulAddKHR

I have some questions about defined integer behavior for OpCooperativeMatrixMulAddKHR in SPV_KHR_cooperative_matrix. Here's what I see in the instruction description, numbered for reference:

1. Integer operations used in the multiplication of A by B are performed at the precision of the Result Type and the resulting value will equal the low-order N bits of the correct result R, where N is the result width and R is computed with enough precision to avoid overflow and underflow if the SaturatingAccumulation Cooperative Matrix Operand is not present.
2. If the SaturatingAccumulation Cooperative Matrix Operand is present and overflow or underflow occurs as part of calculating that intermediate result, the result of the instruction is undefined. Integer additions of the elements of that intermediate result with those of C are performed at the precision of Result Type, are exact, and are saturating if the SaturatingAccumulation Cooperative Matrix Operand is present, with the signedness of the saturation being that of the components of Result Type.
3. If the SaturatingAccumulation Cooperative Matrix Operand is not present then the resulting value will equal the low-order N bits of the correct result R, where N is the result width and R is computed with enough precision to avoid overflow and underflow.

I read this as saying:

* (1) is defining the behavior of the multiplication between A and B (but NOT the addition of C?) when SaturatingAccumulation is not present.
* If this is the case though, shouldn't R be called the "intermediate result"? The use of "correct result" is ambiguous.
* (2) seems reasonably clear: When SaturatingAccumulation is present, if the intermediate result overflow or underflows, the result is undefined, and if the intermediate result plus C overflows or underflows, the result is saturated.
* Note: I suspect "the result of the instruction is undefined" was chosen on purpose, and is different than the usual "behavior is undefined".
* (3) is a little confusing again though, because it describes the resulting value as the bits of R from (1), which did not have the addition of C (I think).
* Assuming there is an addition of C, though, I think this means that the results "wrap"?

I wonder if there might be an easier way to describe this. I think there are four possible overflow/underflow scenarios:

1. If SaturatingAccumulation is present, then...
a. If the intermediate multiplication between A and B overflows or underflows, then the result value is undefined.
b. If the addition of the intermediate result and C overflows, then the result value is saturated.
2. Otherwise, when SaturatingAccumulation is not present, then...
a. If the intermediate multiplication between A and B overflows or underflows, then the intermediate result value is the low N bits of the correctly computed intermediate result (first "wrap").
b. If the addition of the intermediate result and C overflows, then the result value is the low N bits of the correctly computed result (second "wrap").

Is this correct?

Start by reviewing the SPV_KHR_cooperative_matrix instruction description for OpCooperativeMatrixMulAddKHR, focusing on the three numbered integer-behavior paragraphs and the SaturatingAccumulation operand. Resolve whether the text distinguishes multiplication from addition and define the intended overflow behavior; done means the specification wording is unambiguous.

Written by the indexing model from the issue text.