Executable directed rounding

Exact rational intermediates support the four IEEERoundingMode choices; together with the dyadic rounders of Rounding.Directed.Dyadic, they implement addition, subtraction, multiplication, division, fused multiply-add, and square root.

Rounding thresholds, signed-zero behavior, and exceptional results follow the FloatFormat descriptor. Real and extended-real correctness theorems are provided separately by DirectedSemantics with their format and input hypotheses.

Directed rounding of exact rationals

def FloatLib.Floats.Formats.BinaryInterchange.Model.roundRatMagnitudeDirectedScaled (fmt : FloatFormat) (roundMagnitudeUp sign : Bool) (numerator denominator : ℕ) (exponent : ℤ) : Model fmt

Round a scaled positive rational magnitude to the adjacent lower or upper representable magnitude.

roundMagnitudeUp = false selects the lower magnitude and true selects the upper magnitude. The sign parameter supplies the sign to the format's packing, zero, and overflow constructors.

def FloatLib.Floats.Formats.BinaryInterchange.Model.roundRatWithRoundingScaled (fmt : FloatFormat) (mode : IEEERoundingMode) (sign : Bool) (numerator denominator : ℕ) (exponent : ℤ) : Model fmt

Round an exact scaled signed rational according to an IEEE rounding direction.

def FloatLib.Floats.Formats.BinaryInterchange.Model.roundRatWithRounding (fmt : FloatFormat) (mode : IEEERoundingMode) (sign : Bool) (numerator denominator : ℕ) : Model fmt

Round an exact signed rational according to an IEEE rounding direction.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.roundRatDownScaled (fmt : FloatFormat) (sign : Bool) (numerator denominator : ℕ) (exponent : ℤ) : Model fmt

Round an exact scaled signed rational toward negative infinity.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.roundRatUpScaled (fmt : FloatFormat) (sign : Bool) (numerator denominator : ℕ) (exponent : ℤ) : Model fmt

Round an exact scaled signed rational toward positive infinity.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.roundRatDown (fmt : FloatFormat) (sign : Bool) (numerator denominator : ℕ) : Model fmt

Round an exact signed rational toward negative infinity.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.roundRatUp (fmt : FloatFormat) (sign : Bool) (numerator denominator : ℕ) : Model fmt

Round an exact signed rational toward positive infinity.

Arithmetic under an explicit rounding direction

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.zeroForExactSum (fmt : FloatFormat) (mode : IEEERoundingMode) (leftSign rightSign : Bool) : Model fmt

Signed zero for an exact addition result under mode.

def FloatLib.Floats.Formats.BinaryInterchange.Model.addWithRounding {fmt : FloatFormat} (mode : IEEERoundingMode) (x y : Model fmt) : Model fmt

IEEE addition under an explicit rounding direction.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.subWithRounding {fmt : FloatFormat} (mode : IEEERoundingMode) (x y : Model fmt) : Model fmt

IEEE subtraction under an explicit rounding direction.

def FloatLib.Floats.Formats.BinaryInterchange.Model.mulWithRounding {fmt : FloatFormat} (mode : IEEERoundingMode) (x y : Model fmt) : Model fmt

IEEE multiplication under an explicit rounding direction.

def FloatLib.Floats.Formats.BinaryInterchange.Model.divWithRounding {fmt : FloatFormat} (mode : IEEERoundingMode) (x y : Model fmt) : Model fmt

IEEE division under an explicit rounding direction.

def FloatLib.Floats.Formats.BinaryInterchange.Model.fmaWithRounding {fmt : FloatFormat} (mode : IEEERoundingMode) (x y z : Model fmt) : Model fmt

IEEE fused multiply-add under an explicit rounding direction.

Directed square root

structure FloatLib.Floats.Formats.BinaryInterchange.Model.SqrtDyadicBracket : Type

Dyadic endpoint pair used to enclose a nonnegative square root.

• lower : Numerics.Dyadic

  Lower endpoint.

• upper : Numerics.Dyadic

  Upper endpoint.

def FloatLib.Floats.Formats.BinaryInterchange.Model.sqrtDyadicBracket (fmt : FloatFormat) (value : Numerics.Dyadic) : SqrtDyadicBracket

Compute a dyadic enclosure of the square root of a nonnegative exact dyadic.

def FloatLib.Floats.Formats.BinaryInterchange.Model.sqrtWithRounding {fmt : FloatFormat} (mode : IEEERoundingMode) (x : Model fmt) : Model fmt

IEEE square root under an explicit rounding direction.

Interval-friendly operation names

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.addDown {fmt : FloatFormat} (x y : Model fmt) : Model fmt

Addition rounded toward negative infinity.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.addUp {fmt : FloatFormat} (x y : Model fmt) : Model fmt

Addition rounded toward positive infinity.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.subDown {fmt : FloatFormat} (x y : Model fmt) : Model fmt

Subtraction rounded toward negative infinity.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.subUp {fmt : FloatFormat} (x y : Model fmt) : Model fmt

Subtraction rounded toward positive infinity.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.mulDown {fmt : FloatFormat} (x y : Model fmt) : Model fmt

Multiplication rounded toward negative infinity.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.mulUp {fmt : FloatFormat} (x y : Model fmt) : Model fmt

Multiplication rounded toward positive infinity.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.divDown {fmt : FloatFormat} (x y : Model fmt) : Model fmt

Division rounded toward negative infinity.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.divUp {fmt : FloatFormat} (x y : Model fmt) : Model fmt

Division rounded toward positive infinity.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.fmaDown {fmt : FloatFormat} (x y z : Model fmt) : Model fmt

Fused multiply-add rounded toward negative infinity.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.fmaUp {fmt : FloatFormat} (x y z : Model fmt) : Model fmt

Fused multiply-add rounded toward positive infinity.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.sqrtDown {fmt : FloatFormat} (x : Model fmt) : Model fmt

Square root rounded toward negative infinity.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.sqrtUp {fmt : FloatFormat} (x : Model fmt) : Model fmt

Square root rounded toward positive infinity.