Executable bounded fixed-point operations

Bounded fixed point stores an exact signed coefficient in a fixed-width two's-complement carrier. Wrapping, checked, and saturating conversions and operations have distinct names.

Multiplication also exposes the composed input scale and chosen destination width in its result type. This makes the numerical policy visible at the call site while the implementation reuses the generic fixed-integer kernels and their refinement theorems.

@[inline]

def FloatLib.Floats.ExecFloat.BoundedFixedPoint.ofCode {radix : Numerics.Radix} {fractionalDigits width : ℕ} (code : Formats.FixedPoint.Bounded.Code radix fractionalDigits width) : BoundedFixedPoint radix fractionalDigits width

Wrap a complete bounded fixed-point code without conversion.

@[inline]

def FloatLib.Floats.ExecFloat.BoundedFixedPoint.toCode {radix : Numerics.Radix} {fractionalDigits width : ℕ} (value : BoundedFixedPoint radix fractionalDigits width) : Formats.FixedPoint.Bounded.Code radix fractionalDigits width

Recover the complete bounded fixed-point code without conversion.

@[inline]

def FloatLib.Floats.ExecFloat.BoundedFixedPoint.ofNatBits {radix : Numerics.Radix} {fractionalDigits width : ℕ} (bits : ℕ) : BoundedFixedPoint radix fractionalDigits width

Construct a bounded fixed-point value from its complete unsigned word.

@[inline]

def FloatLib.Floats.ExecFloat.BoundedFixedPoint.toNatBits {radix : Numerics.Radix} {fractionalDigits width : ℕ} (value : BoundedFixedPoint radix fractionalDigits width) : ℕ

Read the complete bounded fixed-point word as an unsigned natural number.

@[inline]

def FloatLib.Floats.ExecFloat.BoundedFixedPoint.ofCoefficient {radix : Numerics.Radix} {fractionalDigits width : ℕ} (coefficient : ℤ) : BoundedFixedPoint radix fractionalDigits width

Encode an integer coefficient modulo 2 ^ width.

@[inline]

def FloatLib.Floats.ExecFloat.BoundedFixedPoint.ofRatWrapping {radix : Numerics.Radix} {fractionalDigits width : ℕ} (value : ℚ) : BoundedFixedPoint radix fractionalDigits width

Round an exact rational to the nearest coefficient, ties to even, then wrap it modulo 2 ^ width.

@[inline]

def FloatLib.Floats.ExecFloat.BoundedFixedPoint.ofRat? {radix : Numerics.Radix} {fractionalDigits width : ℕ} (value : ℚ) : Option (BoundedFixedPoint radix fractionalDigits width)

Round an exact rational to the nearest coefficient, ties to even, and return it only when that coefficient fits the destination width.

@[inline]

def FloatLib.Floats.ExecFloat.BoundedFixedPoint.ofRatSaturating {radix : Numerics.Radix} {fractionalDigits width : ℕ} (value : ℚ) : BoundedFixedPoint radix fractionalDigits width

Round an exact rational to the nearest coefficient, ties to even, then clamp it to the signed destination range.

@[inline]

def FloatLib.Floats.ExecFloat.BoundedFixedPoint.coefficient {radix : Numerics.Radix} {fractionalDigits width : ℕ} (value : BoundedFixedPoint radix fractionalDigits width) : ℤ

Recover the stored signed integer coefficient.

@[inline]

def FloatLib.Floats.ExecFloat.BoundedFixedPoint.toRat {radix : Numerics.Radix} {fractionalDigits width : ℕ} (value : BoundedFixedPoint radix fractionalDigits width) : ℚ

Decode a bounded fixed-point value to its exact rational meaning.

@[inline]

def FloatLib.Floats.ExecFloat.BoundedFixedPoint.wrapAdd {radix : Numerics.Radix} {fractionalDigits width : ℕ} (left right : BoundedFixedPoint radix fractionalDigits width) : BoundedFixedPoint radix fractionalDigits width

Same-scale addition modulo 2 ^ width.

@[inline]

def FloatLib.Floats.ExecFloat.BoundedFixedPoint.wrapSub {radix : Numerics.Radix} {fractionalDigits width : ℕ} (left right : BoundedFixedPoint radix fractionalDigits width) : BoundedFixedPoint radix fractionalDigits width

Same-scale subtraction modulo 2 ^ width.

@[inline]

def FloatLib.Floats.ExecFloat.BoundedFixedPoint.wrapMul {radix : Numerics.Radix} {p q leftWidth rightWidth : ℕ} (outWidth : ℕ) (left : BoundedFixedPoint radix p leftWidth) (right : BoundedFixedPoint radix q rightWidth) : BoundedFixedPoint radix (p + q) outWidth

Multiplication modulo 2^outWidth, with exact scale composition.

@[inline]

def FloatLib.Floats.ExecFloat.BoundedFixedPoint.checkedAdd {radix : Numerics.Radix} {fractionalDigits width : ℕ} (left right : BoundedFixedPoint radix fractionalDigits width) : Option (BoundedFixedPoint radix fractionalDigits width)

Return the exact same-scale sum when its coefficient fits.

@[inline]

def FloatLib.Floats.ExecFloat.BoundedFixedPoint.checkedSub {radix : Numerics.Radix} {fractionalDigits width : ℕ} (left right : BoundedFixedPoint radix fractionalDigits width) : Option (BoundedFixedPoint radix fractionalDigits width)

Return the exact same-scale difference when its coefficient fits.

@[inline]

def FloatLib.Floats.ExecFloat.BoundedFixedPoint.checkedMul {radix : Numerics.Radix} {p q leftWidth rightWidth : ℕ} (outWidth : ℕ) (left : BoundedFixedPoint radix p leftWidth) (right : BoundedFixedPoint radix q rightWidth) : Option (BoundedFixedPoint radix (p + q) outWidth)

Return the exact product when its coefficient fits the destination width.

@[inline]

def FloatLib.Floats.ExecFloat.BoundedFixedPoint.saturatingAdd {radix : Numerics.Radix} {fractionalDigits width : ℕ} (left right : BoundedFixedPoint radix fractionalDigits width) : BoundedFixedPoint radix fractionalDigits width

Same-scale addition clamped to the signed coefficient bounds.

@[inline]

def FloatLib.Floats.ExecFloat.BoundedFixedPoint.saturatingSub {radix : Numerics.Radix} {fractionalDigits width : ℕ} (left right : BoundedFixedPoint radix fractionalDigits width) : BoundedFixedPoint radix fractionalDigits width

Same-scale subtraction clamped to the signed coefficient bounds.

@[inline]

def FloatLib.Floats.ExecFloat.BoundedFixedPoint.saturatingMul {radix : Numerics.Radix} {p q leftWidth rightWidth : ℕ} (outWidth : ℕ) (left : BoundedFixedPoint radix p leftWidth) (right : BoundedFixedPoint radix q rightWidth) : BoundedFixedPoint radix (p + q) outWidth

Product clamped to the signed destination range, with exact scale composition.