Basic policy-rounding facts

This module contains the facts needed by arithmetic and conversion proofs: deterministic nearest-even behavior, flush-to-zero behavior, IEEE dispatch, and overflow policy equations.

The independent proof that the general rational policy engine agrees with the directed dyadic engine lives in Rounding.Policy.Agreement, so ordinary finite arithmetic and conversion modules do not inherit its larger directed-semantics dependency graph.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Policy.roundQuot_nearest_eq_zero (sign : Bool) (entropy num den : ℕ) : roundQuot Numerics.RoundingMode.nearest sign entropy num den = roundQuot Numerics.RoundingMode.nearest sign 0 num den

Nearest-even quotient rounding does not inspect the entropy source.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Policy.roundDyadic_nearest_eq_zero (fmt : FloatFormat) (entropy : ℕ) (value : Numerics.Dyadic) : roundDyadic fmt Numerics.QuantizationPolicy.nearest entropy value = roundDyadic fmt Numerics.QuantizationPolicy.nearest 0 value

Nearest-even dyadic quantization is independent of the entropy argument.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Policy.roundDyadicGeneral_nearest_eq_zero (fmt : FloatFormat) (entropy : ℕ) (value : Numerics.Dyadic) : roundDyadicGeneral fmt Numerics.QuantizationPolicy.nearest entropy value = roundDyadicGeneral fmt Numerics.QuantizationPolicy.nearest 0 value

Nearest-even general quantization is independent of the entropy argument.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Policy.applyUnderflow_flush_of_subnormal (fmt : FloatFormat) (x : Model fmt) (hx : x.isSubnormal = true) : applyUnderflow fmt Numerics.UnderflowMode.flushToZero x = zero fmt x.signBit

Flushing a subnormal result produces the format's corresponding zero.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Policy.applyUnderflow_flush_of_not_subnormal (fmt : FloatFormat) (x : Model fmt) (hx : x.isSubnormal = false) : applyUnderflow fmt Numerics.UnderflowMode.flushToZero x = x

Flush-to-zero leaves every non-subnormal encoding unchanged.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Policy.roundRat_nearest_eq_execFloat (fmt : FloatFormat) (entropy : ℕ) (sign : Bool) (num den : ℕ) (hden : den ≠ 0) : roundRat fmt Numerics.QuantizationPolicy.nearest entropy sign num den = some (Model.roundRat fmt sign num den)

Default rational quantization is the canonical format-parameterized nearest-even rounder.

The entropy argument is irrelevant because nearest-even rounding is deterministic.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Policy.roundDyadic_nearest_eq_execFloat (fmt : FloatFormat) (entropy : ℕ) (value : Numerics.Dyadic) : roundDyadic fmt Numerics.QuantizationPolicy.nearest entropy value = Model.roundDyadic fmt value

Default dyadic quantization is the canonical format-parameterized nearest-even rounder.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Policy.ieeeRoundingMode?_toRoundingMode (mode : IEEERoundingMode) : ieeeRoundingMode? mode.toRoundingMode = some mode

Embedding an IEEE direction into the policy vocabulary and back is the identity.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Policy.policyIEEERoundingMode?_toRoundingMode (mode : IEEERoundingMode) : policyIEEERoundingMode? { rounding := mode.toRoundingMode } = some mode

A native-overflow, gradual-underflow policy built from an IEEE direction names that direction.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Policy.roundDyadic_toRoundingMode (fmt : FloatFormat) (mode : IEEERoundingMode) (entropy : ℕ) (value : Numerics.Dyadic) : roundDyadic fmt { rounding := mode.toRoundingMode } entropy value = Internal.Directed.roundDyadic fmt mode value

Each embedded IEEERoundingMode dispatches to the directed engine.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Policy.overflowRoundsMagnitudeUp_toRoundingMode (mode : IEEERoundingMode) (sign : Bool) : overflowRoundsMagnitudeUp mode.toRoundingMode sign = mode.overflowRoundsMagnitudeUp sign

The policy overflow direction of an embedded IEEE mode is the IEEE mode's own overflow direction.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Policy.overflowResult_native_eq_directedOverflow (fmt : FloatFormat) (rounding : Numerics.RoundingMode) (sign : Bool) : overflowResult fmt Numerics.OverflowMode.native rounding sign = directedOverflow fmt sign (overflowRoundsMagnitudeUp rounding sign)

Native policy overflow is the shared directed overflow rule.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Policy.overflowResult_native_nearest (fmt : FloatFormat) (sign : Bool) : overflowResult fmt Numerics.OverflowMode.native Numerics.RoundingMode.nearest sign = nativeOverflow fmt sign

Nearest rounding overflows to the format's native overflow value.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Policy.overflowResult_native_nearestAway (fmt : FloatFormat) (sign : Bool) : overflowResult fmt Numerics.OverflowMode.native Numerics.RoundingMode.nearestAway sign = nativeOverflow fmt sign

Nearest rounding with ties away from zero overflows to the format's native overflow value.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Policy.overflowResult_native_away (fmt : FloatFormat) (sign : Bool) : overflowResult fmt Numerics.OverflowMode.native Numerics.RoundingMode.away sign = nativeOverflow fmt sign

Rounding away from zero overflows to the format's native overflow value of either sign.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Policy.overflowResult_native_towardZero (fmt : FloatFormat) (sign : Bool) : overflowResult fmt Numerics.OverflowMode.native Numerics.RoundingMode.towardZero sign = maxFinite fmt sign

Toward-zero rounding saturates to the largest finite magnitude with the requested sign.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Policy.overflowResult_native_up (fmt : FloatFormat) (sign : Bool) : overflowResult fmt Numerics.OverflowMode.native Numerics.RoundingMode.up sign = if sign = true then maxFinite fmt true else nativeOverflow fmt false

Positive-direction rounding selects native positive overflow and saturates negative overflow.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Policy.overflowResult_native_down (fmt : FloatFormat) (sign : Bool) : overflowResult fmt Numerics.OverflowMode.native Numerics.RoundingMode.down sign = if sign = true then nativeOverflow fmt true else maxFinite fmt false

Negative-direction rounding selects native negative overflow and saturates positive overflow.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Policy.overflowResult_saturate (fmt : FloatFormat) (rounding : Numerics.RoundingMode) (sign : Bool) : overflowResult fmt Numerics.OverflowMode.saturate rounding sign = maxFinite fmt sign

Saturating overflow ignores the rounding direction.