Executable bounded fixed-point operations

Bounded fixed point stores an exact signed coefficient in a fixed-width two's-complement carrier. Conversion and arithmetic take an (overflow := ...) option: .reject, the default, returns none when the exact coefficient does not fit, .wrap reduces it modulo 2 ^ width, and .saturate clamps it to the signed range.

Multiplication also exposes the composed input scale and chosen destination width in its result type. The implementation reuses the generic fixed-integer kernels and their refinement theorems.

inductive FloatLib.Floats.ExecFloat.BoundedFixedPoint.OverflowPolicy : Type

What a bounded fixed-point conversion or operation does with a coefficient that does not fit.

• reject : OverflowPolicy

  Return none, or reject a conversion as outOfRange.

• wrap : OverflowPolicy

  Reduce the coefficient modulo 2 ^ width.

• saturate : OverflowPolicy

  Clamp the coefficient to the signed destination range.

@[instance_reducible]

instance FloatLib.Floats.ExecFloat.BoundedFixedPoint.instDecidableEqOverflowPolicy : DecidableEq OverflowPolicy

def FloatLib.Floats.ExecFloat.BoundedFixedPoint.instReprOverflowPolicy.repr : OverflowPolicy → ℕ → Std.Format

@[instance_reducible]

instance FloatLib.Floats.ExecFloat.BoundedFixedPoint.instReprOverflowPolicy : Repr OverflowPolicy

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

@[macro_inline]

def FloatLib.Floats.ExecFloat.BoundedFixedPoint.ofRat {radix : Numerics.Radix} {fractionalDigits width : ℕ} (value : ℚ) (overflow : OverflowPolicy := OverflowPolicy.reject) : match overflow with | OverflowPolicy.reject => Option (BoundedFixedPoint radix fractionalDigits width) | OverflowPolicy.wrap => BoundedFixedPoint radix fractionalDigits width | OverflowPolicy.saturate => BoundedFixedPoint radix fractionalDigits width

Round an exact rational to the nearest coefficient, ties to even, then apply the overflow policy when that coefficient does not fit.

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

@[macro_inline]

def FloatLib.Floats.ExecFloat.BoundedFixedPoint.add {radix : Numerics.Radix} {fractionalDigits width : ℕ} (left right : BoundedFixedPoint radix fractionalDigits width) (overflow : OverflowPolicy := OverflowPolicy.reject) : match overflow with | OverflowPolicy.reject => Option (BoundedFixedPoint radix fractionalDigits width) | OverflowPolicy.wrap => BoundedFixedPoint radix fractionalDigits width | OverflowPolicy.saturate => BoundedFixedPoint radix fractionalDigits width

Same-scale addition, applying the overflow policy when the exact coefficient sum does not fit.

@[macro_inline]

def FloatLib.Floats.ExecFloat.BoundedFixedPoint.sub {radix : Numerics.Radix} {fractionalDigits width : ℕ} (left right : BoundedFixedPoint radix fractionalDigits width) (overflow : OverflowPolicy := OverflowPolicy.reject) : match overflow with | OverflowPolicy.reject => Option (BoundedFixedPoint radix fractionalDigits width) | OverflowPolicy.wrap => BoundedFixedPoint radix fractionalDigits width | OverflowPolicy.saturate => BoundedFixedPoint radix fractionalDigits width

Same-scale subtraction, with the overflow options of add.

@[macro_inline]

def FloatLib.Floats.ExecFloat.BoundedFixedPoint.mul {radix : Numerics.Radix} {p q leftWidth rightWidth : ℕ} (outWidth : ℕ) (left : BoundedFixedPoint radix p leftWidth) (right : BoundedFixedPoint radix q rightWidth) (overflow : OverflowPolicy := OverflowPolicy.reject) : match overflow with | OverflowPolicy.reject => Option (BoundedFixedPoint radix (p + q) outWidth) | OverflowPolicy.wrap => BoundedFixedPoint radix (p + q) outWidth | OverflowPolicy.saturate => BoundedFixedPoint radix (p + q) outWidth

Multiplication into an outWidth-bit coefficient with exact scale composition, p + q fractional digits, and the overflow options of add at the destination width.