P3109 projection

P3109 projection has three distinct 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 directly. All integer widths, exponent bounds, and special codes come from Format; there are 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, intrinsically restricted to 0 ≤ R < 2^N.

@[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.

• towardZero : RoundingMode
• towardPositive : RoundingMode
• towardNegative : RoundingMode
• nearestTiesToAway : RoundingMode
• nearestTiesToEven : RoundingMode
• toOdd : RoundingMode
• stochasticA (random : RandomBits) : RoundingMode
• stochasticB (random : RandomBits) : RoundingMode
• stochasticC (random : RandomBits) : RoundingMode

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
• propagate : SaturationMode
• none : SaturationMode

@[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 used by one P3109 projection.

• 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

def FloatLib.Floats.Formats.P3109.ProjectionPolicy.nearestEven : ProjectionPolicy

FloatLib default projection: nearest-even rounding and no finite saturation request.

def FloatLib.Floats.Formats.P3109.ProjectionPolicy.finite : ProjectionPolicy

Nearest-even projection clamped to the finite range.

@[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 representation encoding.

Precision rounding is followed by saturation. The result gives the datum meaning before encoding.

@[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; it 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.

Unlike projection, this operation performs no rounding or saturation. It computes the direct P3109 code, decodes it, and accepts the result only when the numerical datum is unchanged.

@[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} (policy : Formats.P3109.ProjectionPolicy) (value : Numerics.NumericalValue Numerics.Dyadic) : P3109 format

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

The operation rounds once to P3109 precision, applies saturation, and encodes the result directly. It never routes through IEEE 754 or a host float.

@[inline]

def FloatLib.Floats.ExecFloat.P3109.ofDyadic {format : Formats.P3109.Format} (policy : Formats.P3109.ProjectionPolicy) (value : Numerics.Dyadic) : P3109 format

Project one exact finite dyadic into a P3109 descriptor.

@[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.