fp_aliasing_semantics.md

x64 addss:

VADDSS (EVEX encoded versions)
    IF (EVEX.b = 1) AND SRC2 *is a register*
        THEN
            SET_RM(EVEX.RC);
        ELSE
            SET_RM(MXCSR.RM);
    FI;
    IF k1[0] or *no writemask*
        THEN DEST[31:0]←SRC1[31:0] + SRC2[31:0]
        ELSE
            IF *merging-masking* ; merging-masking
                THEN *DEST[31:0] remains unchanged*
                ELSE ; zeroing-masking
                    THEN DEST[31:0]←0
            FI;
    FI;
    DEST[127:32] ← SRC1[127:32]
    DEST[MAXVL-1:128] ← 0

VADDSS DEST, SRC1, SRC2 (VEX.128 encoded version)
    DEST[31:0]←SRC1[31:0] + SRC2[31:0]
    DEST[127:32] ←SRC1[127:32]
    DEST[MAXVL-1:128] ←0

ADDSS DEST, SRC (128-bit Legacy SSE version)
    DEST[31:0]←DEST[31:0] + SRC[31:0]
    DEST[MAXVL-1:32] (Unmodified)

ARM64 fadd (scalar):

CheckFPEnabled64();
bits(esize) operand1 = V[n];
bits(esize) operand2 = V[m];
FPCRType fpcr = FPCR[];
boolean merge = IsMerging(fpcr);
bits(128) result = if merge then V[n] else Zeros();
Elem[result, 0, esize] = FPAdd(operand1, operand2, fpcr);
V[d] = result;

RISC-V D extension:

When multiple floating-point precisions are supported, then valid values of narrower n-bit types,
n < FLEN, are represented in the lower n bits of an FLEN-bit NaN value, in a process termed
NaN-boxing. The upper bits of a valid NaN-boxed value must be all 1s. Valid NaN-boxed n-bit
values therefore appear as negative quiet NaNs (qNaNs) when viewed as any wider m-bit value,
n < m ≤ FLEN.