P3109 projection

P3109 projection has three steps:

1. round finite dyadics to the descriptor's precision, preserve infinities, and map exceptions to NaN;
2. apply the selected saturation rule at the descriptor's finite endpoints;
3. encode the resulting datum.

This module follows that order. All integer widths, exponent bounds, and special codes come from Format, with no named-width branches or host floating-point conversions.

The stochastic modes receive a caller-supplied BitVec, whose width enforces the random-word range.

Reference

• IEEE Working Group P3109, Interim Report on Arithmetic Formats for Machine Learning, version 4.0.3 (1 September 2026), Sections 4.7.3--4.7.6, repository revision 34f5964, https://github.com/P3109/Public/tree/34f5964d9bb2382b2665d15467fc3517b990b308.

structure FloatLib.Floats.Formats.P3109.RandomBits : Type

Exact random bits supplied to one P3109 stochastic-rounding decision.

• width : ℕ

  Number of random bits (N in the report).

• bits : BitVec self.width

  Unsigned random integer R, with 0 ≤ R < 2^N by its type.

@[instance_reducible]

instance FloatLib.Floats.Formats.P3109.instReprRandomBits : Repr RandomBits

def FloatLib.Floats.Formats.P3109.instReprRandomBits.repr : RandomBits → ℕ → Std.Format

@[inline]

def FloatLib.Floats.Formats.P3109.RandomBits.ofNat (width value : ℕ) : RandomBits

Construct a supplied random word from the low width bits of a natural number.

@[inline]

def FloatLib.Floats.Formats.P3109.RandomBits.toNat (random : RandomBits) : ℕ

Read the supplied random bits as an unsigned natural number.

inductive FloatLib.Floats.Formats.P3109.RoundingMode : Type

Rounding modes defined by P3109 Section 4.7.4.

The five modes shared with IEEE 754 use the names of the binary IEEERoundingMode. The report's names are TowardZero, TowardPositive, TowardNegative, NearestTiesToAway, and NearestTiesToEven.

• towardZero : RoundingMode

  TowardZero: the neighbour of smaller magnitude.

• up : RoundingMode

  TowardPositive: the neighbour toward positive infinity.

• down : RoundingMode

  TowardNegative: the neighbour toward negative infinity.

• nearestAway : RoundingMode

  NearestTiesToAway: the nearer neighbour, ties to the larger magnitude.

• nearest : RoundingMode

  NearestTiesToEven: the nearer neighbour, ties to the candidate with an even code.

• toOdd : RoundingMode

  ToOdd: an inexact value takes the neighbour with an odd code.

• stochasticA (random : RandomBits) : RoundingMode

  StochasticA: round away when the scaled fraction plus random reaches 2^N.

• stochasticB (random : RandomBits) : RoundingMode

  StochasticB: as stochasticA with one more fraction bit and an offset of one half.

• stochasticC (random : RandomBits) : RoundingMode

  StochasticC: as stochasticA with the scaled fraction rounded to nearest-even.

def FloatLib.Floats.Formats.P3109.instReprRoundingMode.repr : RoundingMode → ℕ → Std.Format

@[instance_reducible]

instance FloatLib.Floats.Formats.P3109.instReprRoundingMode : Repr RoundingMode

inductive FloatLib.Floats.Formats.P3109.SaturationMode : Type

Saturation modes defined by P3109 Section 4.7.5.

• finite : SaturationMode

  SatFinite: clamp every out-of-range result, including infinities, to a finite endpoint.

• propagate : SaturationMode

  SatPropagate: clamp finite overflow but keep an infinity the format can represent.

• none : SaturationMode

  SatNone: overflow to infinity, or to NaN where the format has no infinity. A directed mode that rounds toward the finite range still returns its endpoint.

@[instance_reducible]

instance FloatLib.Floats.Formats.P3109.instDecidableEqSaturationMode : DecidableEq SaturationMode

@[instance_reducible]

instance FloatLib.Floats.Formats.P3109.instReprSaturationMode : Repr SaturationMode

def FloatLib.Floats.Formats.P3109.instReprSaturationMode.repr : SaturationMode → ℕ → Std.Format

structure FloatLib.Floats.Formats.P3109.ProjectionPolicy : Type

Complete policy of one P3109 projection.

The default {} is nearest-even rounding with no saturation request. Executable operations take the two fields as their mode and saturation options. This record is the conversion context of P3109 destinations and the parameter of the specification functions such as projectValue.

• rounding : RoundingMode

  Rule used when precision rounding discards nonzero low bits.

• saturation : SaturationMode

  Rule used after rounding produces a value outside the target datum set.

def FloatLib.Floats.Formats.P3109.instReprProjectionPolicy.repr : ProjectionPolicy → ℕ → Std.Format

@[instance_reducible]

instance FloatLib.Floats.Formats.P3109.instReprProjectionPolicy : Repr ProjectionPolicy

@[inline]

def FloatLib.Floats.Formats.P3109.Format.maxFiniteBits (format : Format) : ℕ

Largest finite positive code point for this descriptor.

@[inline]

def FloatLib.Floats.Formats.P3109.Format.maxFinite (format : Format) : Numerics.Dyadic

Exact largest finite value in this descriptor.

@[inline]

def FloatLib.Floats.Formats.P3109.Format.minFinite (format : Format) : Numerics.Dyadic

Exact smallest finite value in this descriptor.

@[inline]

def FloatLib.Floats.Formats.P3109.Format.lowerCodeIsEven (format : Format) (quantumExponent : ℤ) (lowerSignificand : ℕ) : Bool

Whether the lower candidate has an even P3109 code at a rounding boundary.

For P > 1, code parity is ordinary significand parity. The P = 1 branch is the special rule from Section 4.7.4: zero is even, and a nonzero code is even exactly when Q + B is even.

@[inline]

def FloatLib.Floats.Formats.P3109.Format.Internal.scaleFractionFloor (remainder discardedBits outputBits : ℕ) : ℕ

Floor of (remainder / 2^discardedBits) * 2^outputBits.

@[inline]

def FloatLib.Floats.Formats.P3109.Format.Internal.scaleFractionNearestEven (remainder discardedBits outputBits : ℕ) : ℕ

Nearest-even integer to (remainder / 2^discardedBits) * 2^outputBits.

@[inline]

def FloatLib.Floats.Formats.P3109.Format.Internal.roundAway (format : Format) (mode : RoundingMode) (negative : Bool) (quantumExponent : ℤ) (lower remainder discardedBits : ℕ) : Bool

Decide whether precision rounding selects the integer above the floor candidate.

@[inline]

def FloatLib.Floats.Formats.P3109.Format.roundFiniteToPrecision (format : Format) (mode : RoundingMode) (value : Numerics.Dyadic) : Numerics.Dyadic

Round one exact finite dyadic to P3109 precision before saturation.

The quantum is max(floor(log2 |X|), 1 - B) - P + 1, so the same implementation handles normals, subnormals, P = 1, and arbitrary descriptor widths.

@[inline]

def FloatLib.Floats.Formats.P3109.Format.roundToPrecision (format : Format) (mode : RoundingMode) (value : Numerics.NumericalValue Numerics.Dyadic) : Numerics.NumericalValue Numerics.Dyadic

Apply P3109 precision rounding while preserving infinities and mapping exceptions to NaN.

@[inline]

def FloatLib.Floats.Formats.P3109.Format.Internal.saturateBelow (format : Format) (mode : SaturationMode) (rounding : RoundingMode) : Numerics.NumericalValue Numerics.Dyadic

Saturate a rounded value below the finite range.

@[inline]

def FloatLib.Floats.Formats.P3109.Format.Internal.saturateAbove (format : Format) (mode : SaturationMode) (rounding : RoundingMode) : Numerics.NumericalValue Numerics.Dyadic

Saturate a rounded value above the finite range.

@[inline]

def FloatLib.Floats.Formats.P3109.Format.saturate (format : Format) (mode : SaturationMode) (rounding : RoundingMode) (value : Numerics.NumericalValue Numerics.Dyadic) : Numerics.NumericalValue Numerics.Dyadic

Apply P3109 Section 4.7.5 to a value that has already been rounded to precision.

@[inline]

def FloatLib.Floats.Formats.P3109.Format.projectValue (format : Format) (policy : ProjectionPolicy) (value : Numerics.NumericalValue Numerics.Dyadic) : Numerics.NumericalValue Numerics.Dyadic

Mathematical result of P3109 projection before encoding: precision rounding, then saturation.

@[inline]

def FloatLib.Floats.Formats.P3109.Format.Internal.encodePositiveFinite (format : Format) (value : Numerics.Dyadic) : ℕ

Encode a positive finite datum.

The caller supplies a value already rounded to precision and inside the finite range. This is the integer form of Section 4.7.6 and does not enumerate the codebook.

@[inline]

def FloatLib.Floats.Formats.P3109.Format.Internal.encodeDatumNat (format : Format) (value : Numerics.NumericalValue Numerics.Dyadic) : ℕ

Encode a value known to be in this descriptor's datum set.

def FloatLib.Floats.Formats.P3109.Format.SameDatum : Numerics.NumericalValue Numerics.Dyadic → Numerics.NumericalValue Numerics.Dyadic → Prop

P3109 equality of datum meanings.

Finite values are equal numerically, infinity signs must match, and every NaN payload denotes the format's single NaN datum. Other exceptional categories are not P3109 datums.

@[inline]

def FloatLib.Floats.Formats.P3109.Format.datumEqual : Numerics.NumericalValue Numerics.Dyadic → Numerics.NumericalValue Numerics.Dyadic → Bool

Executable equality of P3109 datum meanings.

Finite dyadics are compared numerically, so harmless differences in significand normalization do not make a representable value fail the checked encoder. P3109 has one NaN, so its optional payload is not semantically observable here.

@[inline]

def FloatLib.Floats.Formats.P3109.Format.encode? (format : Format) (value : Numerics.NumericalValue Numerics.Dyadic) : Option (BitVec format.bitWidth)

Encode a value only when it belongs to this descriptor's datum set.

There is no rounding or saturation. The operation computes the P3109 code, decodes it, and accepts the code only when the decoded datum has the same P3109 numerical meaning as value (SameDatum).

@[inline]

def FloatLib.Floats.Formats.P3109.Format.projectCode (format : Format) (policy : ProjectionPolicy) (value : Numerics.NumericalValue Numerics.Dyadic) : BitVec format.bitWidth

Project one exact closed value and return its descriptor-width code.

@[inline]

def FloatLib.Floats.ExecFloat.P3109.project {format : Formats.P3109.Format} (value : Numerics.NumericalValue Numerics.Dyadic) (mode : Formats.P3109.RoundingMode := Formats.P3109.RoundingMode.nearest) (saturation : Formats.P3109.SaturationMode := Formats.P3109.SaturationMode.none) : P3109 format

Project an exact finite, infinite, or NaN value into a P3109 descriptor.

The operation rounds once to P3109 precision in mode, applies saturation, and encodes the result, never going through IEEE 754 or a host float.

@[inline]

def FloatLib.Floats.ExecFloat.P3109.ofDyadic {format : Formats.P3109.Format} (value : Numerics.Dyadic) (mode : Formats.P3109.RoundingMode := Formats.P3109.RoundingMode.nearest) (saturation : Formats.P3109.SaturationMode := Formats.P3109.SaturationMode.none) : P3109 format

Project one exact finite dyadic into a P3109 descriptor, with the options of project.

@[inline]

def FloatLib.Floats.ExecFloat.P3109.encode? {format : Formats.P3109.Format} (value : Numerics.NumericalValue Numerics.Dyadic) : Option (P3109 format)

Encode an already representable P3109 datum without rounding it.