Exact dyadic rounding

This is the executable one-rounding boundary for exact binary values. It classifies an exact dyadic against descriptor-derived overflow, normal, and subnormal regions, retains only the target significand bits, and applies nearest-even to the discarded part.

Conventional IEEE descriptors may reuse Lean's logical float model as a proof-facing route. roundDyadicGeneral handles custom bias and every supported exceptional-value encoding directly. The public selector keeps those implementations under one descriptor-level contract.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.ieeeRoundDyadic (fmt : FloatFormat) (d : Numerics.Dyadic) : Model fmt

Round an exact dyadic through Lean's conventional IEEE logical model.

This is the proof-facing specification for formats with ordinary IEEE bias and exceptional-value encoding. roundDyadic below selects it only when fmt.isIEEE.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.zero_extendedMantissa_shiftRight (shift : ℕ) : { mantissa := 0, roundBit := false, stickyBit := false } >>> shift = { mantissa := 0, roundBit := false, stickyBit := false }

Right shifts preserve a zero mantissa with clear round and sticky bits.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.round_exact_zero (spec : Float.Model.Format) (sign : Float.Model.UnpackedFloat.Sign) (exponent : ℤ) : Float.Model.UnpackedFloat.round spec sign 0 exponent = Float.Model.UnpackedFloat.zero sign

Rounding in Lean's IEEE model preserves signed zero for every model format.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.ieeeRoundDyadic_significand_zero (fmt : FloatFormat) (sign : Bool) (exponent : ℤ) : ieeeRoundDyadic fmt { negative := sign, significand := 0, exponent := exponent } = ofModel fmt (Float.Model.UnpackedFloat.zero (modelSign sign))

Rounding an exact zero through Lean's logical model packs the corresponding signed zero.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.nativeOverflow (fmt : FloatFormat) (sign : Bool) : Model fmt

Default overflow result: infinity, NaN, or saturation according to the encoding.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.nativeOverflow_eq_signedInf_of_isIEEE (fmt : FloatFormat) (hfmt : fmt.isIEEE = true) (sign : Bool) : nativeOverflow fmt sign = if sign = true then negInf fmt else posInf fmt

Conventional IEEE native overflow is the usual signed infinity.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.directedOverflow (fmt : FloatFormat) (sign roundMagnitudeUp : Bool) : Model fmt

Overflow result for a signed magnitude under a known rounding direction.

IEEE 754-2019 Section 7.4 rounds an overflowing magnitude to the format's overflow value when the direction carries the magnitude upward and to the largest finite value when it carries the magnitude downward. roundMagnitudeUp records that direction after the sign has been taken into account: toward zero never rounds up, toward positive infinity rounds a positive magnitude up, and toward negative infinity rounds a negative magnitude up. Nearest modes always round up. The directed and policy rounders share this definition so that a finite-with-NaN encoding saturates in the truncating direction under both engines.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.packRoundedSubnormal (fmt : FloatFormat) (sign : Bool) (zeroResult : Model fmt) (fraction : ℕ) : Model fmt

Pack a rounded subnormal significand.

The caller supplies the zero result because some directed algorithms know that a nonzero exact input must round to the least subnormal, while rational rounding uses the format's zero policy. Keeping the common boundary logic here prevents those algorithms from drifting apart.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.packRoundedNormal (fmt : FloatFormat) (sign : Bool) (overflow : Model fmt) (totalExponent : ℤ) (roundedMantissa : ℕ) : Model fmt

Pack a rounded normal significand, including carry into the exponent and descriptor-specific overflow words.

This helper accepts an already rounded significand. Callers remain responsible for proving that their rounding decision and supplied overflow result match the requested policy.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.roundDyadicGeneral (fmt : FloatFormat) (d : Numerics.Dyadic) : Model fmt

Round an exact dyadic according to the complete format descriptor.

Only the retained significand and the discarded-bit rounding decision are materialized. The implementation supports custom exponent bias and every FloatFormat.Encoding; it does not pass through Lean's conventional IEEE model.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.roundDyadic (fmt : FloatFormat) (d : Numerics.Dyadic) : Model fmt

Round an exact dyadic to Model fmt using round-to-nearest, ties-to-even.

Conventional IEEE formats retain the established logical-model specification and its checked native implementation. Other static formats use the descriptor-aware integer algorithm directly.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.addDyadic (a b : Numerics.Dyadic) : Numerics.Dyadic

Exact addition at the binary-format API boundary.

The implementation is shared with posit arithmetic and exact reductions through Numerics.Dyadic.add; binary operations keep this name so their specifications read naturally. No rounding occurs until the result is passed to roundDyadic.