P3109 arithmetic with external binary destinations

The report's projection uses the external format's actual precision, bias, and finite endpoints. It retains all nine rounding modes and all three saturation modes, with explicit stochastic bits. Finite overflow under SaturationMode.propagate clamps, while an infinite exact input remains infinite. The destination encoder writes positive zero and canonical quiet NaN, as required by §4.8.2.

Finite encoding uses the proved binary dyadic encoder on an already rounded, in-range datum; the proof facet establishes that this encoding does not introduce another rounding error. The adapters accept IEEE-style encoding descriptors, including binary16, binary32, binary64, and BFloat16. They do not change the ordinary IEEE arithmetic or signed-zero conversion APIs.

Reference: P3109 unapproved interim report 4.0.3, revision 34f5964, §§4.7–4.10 and 4.14.

def FloatLib.Floats.Formats.P3109.Arithmetic.External.roundFinite (format : BinaryInterchange.FloatFormat) (mode : RoundingMode) (exact : ℚ) : Numerics.Dyadic

Round an exact rational with the external format's precision and exponent bias.

def FloatLib.Floats.Formats.P3109.Arithmetic.External.roundValue (format : BinaryInterchange.FloatFormat) (mode : RoundingMode) : Numerics.NumericalValue ℚ → Numerics.NumericalValue Numerics.Dyadic

Apply precision rounding, retaining infinity and canonicalizing NaN.

def FloatLib.Floats.Formats.P3109.Arithmetic.External.endpoint (format : BinaryInterchange.FloatFormat) (negative : Bool) : Numerics.Dyadic

Exact largest finite external binary value, with a supplied sign.

def FloatLib.Floats.Formats.P3109.Arithmetic.External.finiteOverflow (format : BinaryInterchange.FloatFormat) (policy : ProjectionPolicy) (negative : Bool) : Numerics.NumericalValue Numerics.Dyadic

Saturate a finite overflow under the external format's signed, extended domain.

def FloatLib.Floats.Formats.P3109.Arithmetic.External.saturate (format : BinaryInterchange.FloatFormat) (policy : ProjectionPolicy) : Numerics.NumericalValue Numerics.Dyadic → Numerics.NumericalValue Numerics.Dyadic

Saturate after rounding; .propagate distinguishes finite overflow from infinity.

def FloatLib.Floats.Formats.P3109.Arithmetic.External.projectValue (format : BinaryInterchange.FloatFormat) (policy : ProjectionPolicy) (value : Numerics.NumericalValue ℚ) : Numerics.NumericalValue Numerics.Dyadic

Exact rounded and saturated result, before external encoding.

def FloatLib.Floats.Formats.P3109.Arithmetic.External.encode (format : BinaryInterchange.FloatFormat) : Numerics.NumericalValue Numerics.Dyadic → BinaryInterchange.Model format

Encode a projected external datum, using positive zero and canonical quiet NaN.

def FloatLib.Floats.Formats.P3109.Arithmetic.External.project (format : BinaryInterchange.FloatFormat) (_ieee : format.isIEEE = true) (policy : ProjectionPolicy) (value : Numerics.NumericalValue ℚ) : BinaryInterchange.Model format

External report projection; the evidence excludes non-IEEE exceptional encodings.

def FloatLib.Floats.Formats.P3109.Arithmetic.External.decode {format : BinaryInterchange.FloatFormat} (value : BinaryInterchange.Model format) : Numerics.NumericalValue ℚ

Complete exact external decoding with zero signs and NaN payloads erased.

@[instance_reducible]

instance FloatLib.Floats.Formats.P3109.Arithmetic.External.modelDecoder (format : BinaryInterchange.FloatFormat) : ExecFloat.ExactDecoder (BinaryInterchange.Model format) ℚ

A binary model can be an external source of mixed report arithmetic.

def FloatLib.Floats.Formats.P3109.Arithmetic.External.destination (format : BinaryInterchange.FloatFormat) (ieee : format.isIEEE = true := by decide) : Destination (BinaryInterchange.Model format)

Report projection into an external model, with no storage-plan requirements.

def FloatLib.Floats.Formats.P3109.Arithmetic.External.configuredDestination (format : BinaryInterchange.FloatFormat) (plan : BinaryInterchange.Configured.StoragePlan format) (code : Type) [ExecFloat.ModelCodec plan (BinaryInterchange.Model format) code] (ieee : format.isIEEE = true := by decide) : Destination (ExecFloat (BinaryInterchange.Configured.Family format code plan))

Report projection into a configured external carrier through its exact model codec.

@[inline]

def FloatLib.Floats.Formats.P3109.Arithmetic.External.bitwidthOf (format : BinaryInterchange.FloatFormat) : ℕ

External bit width from the complete binary descriptor.

@[inline]

def FloatLib.Floats.Formats.P3109.Arithmetic.External.precisionOf (format : BinaryInterchange.FloatFormat) : ℕ

External precision includes the implicit leading bit.

@[inline]

def FloatLib.Floats.Formats.P3109.Arithmetic.External.signednessOf (_format : BinaryInterchange.FloatFormat) : Signedness

External IEEE formats are signed.

@[inline]

def FloatLib.Floats.Formats.P3109.Arithmetic.External.domainOf (_format : BinaryInterchange.FloatFormat) : Domain

External IEEE formats have the extended domain.

@[inline]

def FloatLib.Floats.Formats.P3109.Arithmetic.External.exponentBitwidthOf (format : BinaryInterchange.FloatFormat) : ℕ

External exponent-field width.

@[inline]

def FloatLib.Floats.Formats.P3109.Arithmetic.External.trailingSignificandBitwidthOf (format : BinaryInterchange.FloatFormat) : ℕ

External fraction-field width.

@[inline]

def FloatLib.Floats.Formats.P3109.Arithmetic.External.exponentBiasOf (format : BinaryInterchange.FloatFormat) : ℕ

The actual external bias; no P3109 bias is substituted.

@[inline]

def FloatLib.Floats.Formats.P3109.Arithmetic.External.maxFiniteOf (format : BinaryInterchange.FloatFormat) : BinaryInterchange.Model format

Largest finite external datum.

@[inline]

def FloatLib.Floats.Formats.P3109.Arithmetic.External.minFiniteOf (format : BinaryInterchange.FloatFormat) : BinaryInterchange.Model format

Smallest finite external datum.

@[inline]

def FloatLib.Floats.Formats.P3109.Arithmetic.External.minPositiveOf (format : BinaryInterchange.FloatFormat) : BinaryInterchange.Model format

Smallest strictly positive external datum.

@[inline]

def FloatLib.Floats.Formats.P3109.Arithmetic.External.maxSubnormalOf (format : BinaryInterchange.FloatFormat) : BinaryInterchange.Model format

Largest positive external subnormal.

@[inline]

def FloatLib.Floats.Formats.P3109.Arithmetic.External.minNormalOf (format : BinaryInterchange.FloatFormat) : BinaryInterchange.Model format

Smallest positive external normal.