Binary IR conversion semantics

The interpreter's conversion returns FloatLib's specified directed rounding of the exact source encoding. This statement includes exceptional encodings; it does not assign a real value to NaN or infinity. FloatLib supplies the finite rounding and error theorems applicable when their additional hypotheses hold.

theorem NN.IR.Binary.cast_value (source target : FloatLib.Floats.Formats.BinaryInterchange.FloatFormat) (rounding : FloatLib.Floats.Formats.BinaryInterchange.Model.IEEERoundingMode) (value : Scalar source) (converted : Scalar target) (flags : FloatLib.Floats.ExecFloat.ConversionStatus) (h : cast (DType.binary source) (DType.binary target) rounding value = Except.ok (converted, flags)) : FloatLib.Floats.ExecFloat.Binary.toModel converted = FloatLib.Floats.Formats.BinaryInterchange.Model.cast source target (FloatLib.Floats.ExecFloat.Binary.toModel value) rounding

A successful interpreter cast delivers exactly FloatLib's directed binary conversion.