Exact-rational reference division for native binary32 words #
The exact-rational reference divider specifies the result against which the direct binary32 word divider is refined. It decodes finite binary32 operands, handles finite division by zero according to IEEE binary32, and delegates nonzero quotients to the exact rational rounder.
The optimized one-word divider and its proof live in Narrow.Division.Runtime and
Narrow.Division.Proof. Keeping the reference
operation independent prevents division-only clients from depending on the much larger
addition/FMA implementation core.
@[inline]
Finite binary32 division through the generic exact-rational rounder.