Decimal interchange interval endpoints

intervalRounding equips actual BID or DPD words with rational outward rounding. The descriptor may be decimal32, decimal64, decimal128, or a custom decimal layout. Directed decimal projection produces each endpoint, which is encoded with the selected codec and checked against the exact input after decoding. A successful enclosure therefore bounds the input using the actual stored words, not only the decimal datums before encoding.

NaNs and infinities have no rational interpretation. Overflow that needs an infinite endpoint returns none; it is not replaced by a finite bound that would exclude the input. The shared Numerics.Interval operations provide addition, subtraction, multiplication, and division away from zero using these endpoints.

@[reducible, inline]

abbrev FloatLib.Floats.Formats.DecimalInterchange.Interval (format : Format) : Type

An interval whose endpoints are complete decimal interchange words in one layout.

def FloatLib.Floats.Formats.DecimalInterchange.decodeIntervalEndpoint (format : Format) (encoding : Encoding) (word : BitVec format.bitWidth) : Option ℚ

Interpret a decimal endpoint as an exact rational, rejecting NaNs and infinities.

def FloatLib.Floats.Formats.DecimalInterchange.intervalCandidates (format : Format) (encoding : Encoding) (x : ℚ) : Interval format

Directed decimal projections encoded in the selected interchange representation.

def FloatLib.Floats.Formats.DecimalInterchange.intervalRounding (format : Format) (encoding : Encoding) : Numerics.OutwardRounding (BitVec format.bitWidth) ℚ

Checked outward rounding for decimal words, valid for every descriptor and either codec.

The exact endpoint check also covers exceptional outputs and catches any candidate that fails to bracket the target; the result never silently treats a saturated finite value as infinity.