Direct generic dyadic rounding

Generic dyadic rounding runs on integer arithmetic. RoundingKernel.Proof proves that these functions refine the logical float model and registers the compiler substitutions. With the implementation here, runtime backends need not import the much larger normalization proof.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.Internal.ieeeRoundDyadic (fmt : FloatFormat) (d : Numerics.Dyadic) : Model fmt

Direct integer implementation of nearest-even IEEE dyadic rounding.

This is the compiled counterpart of ieeeRoundDyadic. It handles subnormal alignment, normalization carry, signed underflow to zero, and overflow without constructing a logical model value.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.Internal.roundDyadic (fmt : FloatFormat) (d : Numerics.Dyadic) : Model fmt

Compiled nearest-even dyadic rounding for every complete format descriptor.