[conistonwater]

It should be zero, exactly zero, i.e., no rounding error. Because if you do long subtraction on the significands, the number of digits you need to store the result is at most the number of digits you had, because the numbers were within a factor of two from each other (so no shifting left or right).

Just to check, with sbv in haskell, using the Z3 SMT solver:

    λ> f (x::SFloat) (y::SFloat) = fpIsNormal x &&& fpIsNormal y &&& y/2 .<= x &&& x .<= 2*y ==> fromSFloat sRNE (x - y) .== (fromSFloat sRNE x :: SDouble) - (fromSFloat sRNE y :: SDouble)
    f :: SFloat -> SFloat -> SBool
    λ> prove (forAll_ f)
    Q.E.D.

Or without rounding through double, using the formula for exact rounding error of a sum:

    λ> g (x::SFloat) (y::SFloat) = fpIsNormal x &&& fpIsNormal y &&& 0 .<= x &&& y .<= x &&& x .<= 2*y ==> (x - ((x-y) + y)) .== 0
    g :: SFloat -> SFloat -> SBool
    λ> prove (forAll_ g)
    Q.E.D.