Direct generic dyadic rounding

Generic dyadic rounding executes directly with integer arithmetic. RoundDyadicImpl.Proof proves that these functions refine the logical float model and registers the compiler substitutions. Keeping the implementation here lets runtime backends avoid importing the substantially larger normalization proof.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.ieeeRoundDyadicImpl (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.roundDyadicImpl (fmt : FloatFormat) (d : Numerics.Dyadic) : Model fmt

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