Once-rounded binary squares

Model.square uses one operand decode in the specialized product kernels and returns exactly the complete encoding of Model.mul x x. The descriptor's rounding, overflow, zero, and NaN policies therefore apply at every width.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.square {fmt : FloatFormat} (x : Model fmt) : Model fmt

Square with one nearest-even rounding, preserving multiplication's NaN sign and payload.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.square_eq_mul {fmt : FloatFormat} (x : Model fmt) : x.square = x.mul x

Squaring and multiplying equal operands produce identical complete encodings.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.square_eq_spec {fmt : FloatFormat} (x : Model fmt) : x.square = Spec.mul x x

Squaring refines the exact dyadic product and the descriptor's exceptional-value policy.