We do discuss signaling/quiet propagation behavior briefly in the LangRef Floating-Point Environment section, although it’s not as clear as it could be. For example, I thought we had decided that the constrained intrinsics are required to convert sNaN input to qNaN output as required by IEEE754, but that’s not explicitly stated.
Anyhow, your modified version looks pretty good. We should make sure not to conflict with requirements on determinism of signal/quiet bit, but that could be an aside on the third bullet, e.g. “(Except on constrained intrinsics, since they cannot result in a signaling-NaN output)”
I’m not certain we really need to make such an exception. We might want to check how these operations are lowered in LLVM today, first. We know that the spidermonkey JIT implementation got more complex when it realized this requirement, because it had previously been "bitwise-or"ing operands to create a NaN with an arbitrary payload. But, if that technique hasn’t been used in LLVM IR before today, maybe we don’t really need to allow it to be used in the future…it’d certainly be simpler to not make an exception here.
That seems like a fine answer to me – do you see a particular issue with that? That is, on wasm “If any input operand is a NaN with a non-preferred payload, then an output payload may additionally be any value with the the quiet bit set to 1.”