Emulating round-to-nearest-ties-to-zero "augmented" floating-point operations using round-to-nearest-ties-to-even arithmetic

The 2019 version of the IEEE 754 Standard for Floating-Point Arithmetic recommends that new “augmented” operations should be provided for the binary formats. These operations use a new “rounding direction”: round-to-nearest ties-to-zero. We show how they can be implemented using the currently available operations, using round-to-nearest ties-to-even with a partial formal proof of correctness.