Representation-independent operation context

Rounding direction, overflow handling, and treatment of tiny outputs describe how an exact value is written into a finite numerical representation. They are operation context rather than properties of a binary bit layout, so they live in the family-independent operation layer.

A concrete format may support only part of this vocabulary. Its quantizer gives each policy a meaning or rejects unsupported combinations at a higher API layer.

inductive FloatLib.Numerics.RoundingMode : Type

Rule used when an exact value lies between adjacent representable values.

• nearest : RoundingMode

  Take the nearer neighbour, breaking a tie toward an even significand.

• nearestAway : RoundingMode

  Take the nearer neighbour, breaking a tie toward the neighbour of larger magnitude.

• towardZero : RoundingMode

  Take the neighbour of smaller magnitude.

• up : RoundingMode

  Take the neighbour toward positive infinity.

• down : RoundingMode

  Take the neighbour toward negative infinity.

• away : RoundingMode

  Take the neighbour of larger magnitude whenever the value is not representable. This is GNU MPFR's MPFR_RNDA, which is not an IEEE 754 rounding-direction attribute.

• stochastic : RoundingMode

  Randomized rounding driven by entropy supplied to the operation.

@[instance_reducible]

instance FloatLib.Numerics.instDecidableEqRoundingMode : DecidableEq RoundingMode

def FloatLib.Numerics.instReprRoundingMode.repr : RoundingMode → Nat → Std.Format

@[instance_reducible]

instance FloatLib.Numerics.instReprRoundingMode : Repr RoundingMode

inductive FloatLib.Numerics.OverflowMode : Type

Behavior when an exact magnitude lies outside the ordinary finite range.

• native : OverflowMode

  Use the representation's ordinary overflow result.

• saturate : OverflowMode

  Clamp to the nearest finite endpoint.

@[instance_reducible]

instance FloatLib.Numerics.instDecidableEqOverflowMode : DecidableEq OverflowMode

@[instance_reducible]

instance FloatLib.Numerics.instReprOverflowMode : Repr OverflowMode

def FloatLib.Numerics.instReprOverflowMode.repr : OverflowMode → Nat → Std.Format

inductive FloatLib.Numerics.UnderflowMode : Type

Behavior when a nonzero result lies below the normal range.

• gradual : UnderflowMode

  Preserve the representation's gradual-underflow values when they exist.

• flushToZero : UnderflowMode

  Replace tiny stored outputs with the representation's zero.

@[instance_reducible]

instance FloatLib.Numerics.instDecidableEqUnderflowMode : DecidableEq UnderflowMode

def FloatLib.Numerics.instReprUnderflowMode.repr : UnderflowMode → Nat → Std.Format

@[instance_reducible]

instance FloatLib.Numerics.instReprUnderflowMode : Repr UnderflowMode

structure FloatLib.Numerics.QuantizationPolicy : Type

Shared policy for converting an exact scalar to a finite numerical representation.

• rounding : RoundingMode

  Rule used to choose between adjacent representable values.

• overflow : OverflowMode

  Rule used when the exact magnitude exceeds the finite range.

• underflow : UnderflowMode

  Rule used for nonzero results below the normal range.

@[instance_reducible]

instance FloatLib.Numerics.instDecidableEqQuantizationPolicy : DecidableEq QuantizationPolicy

def FloatLib.Numerics.instDecidableEqQuantizationPolicy.decEq (x✝ x✝¹ : QuantizationPolicy) : Decidable (x✝ = x✝¹)

@[instance_reducible]

instance FloatLib.Numerics.instReprQuantizationPolicy : Repr QuantizationPolicy

def FloatLib.Numerics.instReprQuantizationPolicy.repr : QuantizationPolicy → Nat → Std.Format

def FloatLib.Numerics.QuantizationPolicy.nearest : QuantizationPolicy

Nearest-even rounding with native overflow and gradual underflow.

def FloatLib.Numerics.QuantizationPolicy.saturating : QuantizationPolicy

Nearest-even rounding with saturation and gradual underflow.

def FloatLib.Numerics.QuantizationPolicy.flushToZero : QuantizationPolicy

Nearest-even rounding with native overflow and output flush-to-zero.