research!rsc: Fast Unrounded Scaling: Proof by Ivy (Floating Point Formatting, Part 4)

DRANK

My post “Floating-Point Printing and Parsing Can Be Simple And Fast” depends on fast unrounded scaling, defined as:The unrounded form of , , is the integer value of concatenated with two more bits: first, the “½ bit” from the binary representation of (the bit representing ; if ; or equivalently, ); and second, a “sticky bit” that is 1 if any bits beyond the ½ bit were 1.These are all equivalent definitions, using the convention that a boolean condition is 1 for true, 0 for false:The operation computes the unrounded form of , so it needs to compute the integer and then also whether the floor truncated any bits. One approach would be to compute as an exact rational, but we want to avoid arbitrary-precision math. A faster approach is to use a floating-point approximation for : , where is 128 bits. Assuming , this requires a single 64×128→192-bit multiplication, implemented by two full-width 64×64→128-bit multplications on a 64-bit computer.The algorithm, which we will call , is g…