Bounded fixed-point execution

A bounded fixed-point code stores its coefficient in FixedInt width and interprets that signed integer at a fixed radix scale. Arithmetic names state their overflow policy explicitly:

• wrapping addition and subtraction use direct BitVec arithmetic;
• wrapping multiplication sign-extends or truncates both inputs to the destination width before multiplying;
• checked operations return none when the exact coefficient is out of range;
• saturating operations clamp the exact coefficient to the destination range.

Multiplication composes scales: operands with p and q fractional digits produce p + q fractional digits. The destination width is independent of the two input widths.

@[reducible]

def FloatLib.Floats.Formats.FixedPoint.Bounded.Code (_radix : Numerics.Radix) (_fractionalDigits width : ℕ) : Type

A signed width-bit coefficient interpreted with a fixed radix scale.

This is a transparent type definition rather than an abbreviation. It has exactly the FixedInt width runtime representation, while retaining the radix and scale in elaborated type expressions so proof-aware tooling can identify the numerical format.

@[reducible, inline]

abbrev FloatLib.Floats.Formats.FixedPoint.Bounded.scale (radix : Numerics.Radix) (fractionalDigits : ℕ) : ℕ

Natural scaling denominator of a fixed-point format.

@[inline]

def FloatLib.Floats.Formats.FixedPoint.Bounded.coefficient {width : ℕ} (code : Numerics.Representations.FixedInt width) : ℤ

Signed integer coefficient stored by a bounded fixed-point code.

@[inline]

def FloatLib.Floats.Formats.FixedPoint.Bounded.toRat (radix : Numerics.Radix) (fractionalDigits : ℕ) {width : ℕ} (code : Numerics.Representations.FixedInt width) : ℚ

Exact rational value of a bounded fixed-point code.

@[inline]

def FloatLib.Floats.Formats.FixedPoint.Bounded.ofInt (width : ℕ) (value : ℤ) : Numerics.Representations.FixedInt width

Encode an integer coefficient modulo 2 ^ width.

@[inline]

def FloatLib.Floats.Formats.FixedPoint.Bounded.wrapAdd {width : ℕ} (left right : Numerics.Representations.FixedInt width) : Numerics.Representations.FixedInt width

Addition modulo 2 ^ width.

@[inline]

def FloatLib.Floats.Formats.FixedPoint.Bounded.wrapSub {width : ℕ} (left right : Numerics.Representations.FixedInt width) : Numerics.Representations.FixedInt width

Subtraction modulo 2 ^ width.

@[inline]

def FloatLib.Floats.Formats.FixedPoint.Bounded.wrapMul (outWidth : ℕ) {leftWidth rightWidth : ℕ} (left : Numerics.Representations.FixedInt leftWidth) (right : Numerics.Representations.FixedInt rightWidth) : Numerics.Representations.FixedInt outWidth

Multiplication modulo 2^outWidth.

Both coefficients are resized in two's-complement form before the native BitVec product. This implements exact multiplication followed by centered reduction at the destination width.

@[inline]

def FloatLib.Floats.Formats.FixedPoint.Bounded.checkedAdd {width : ℕ} (left right : Numerics.Representations.FixedInt width) : Option (Numerics.Representations.FixedInt width)

Return the exact same-scale sum when it fits the signed coefficient width.

@[inline]

def FloatLib.Floats.Formats.FixedPoint.Bounded.checkedSub {width : ℕ} (left right : Numerics.Representations.FixedInt width) : Option (Numerics.Representations.FixedInt width)

Return the exact same-scale difference when it fits the signed coefficient width.

@[inline]

def FloatLib.Floats.Formats.FixedPoint.Bounded.checkedMul (outWidth : ℕ) {leftWidth rightWidth : ℕ} (left : Numerics.Representations.FixedInt leftWidth) (right : Numerics.Representations.FixedInt rightWidth) : Option (Numerics.Representations.FixedInt outWidth)

Return the exact product when its coefficient fits outWidth signed bits.

@[inline]

def FloatLib.Floats.Formats.FixedPoint.Bounded.saturatingAdd {width : ℕ} (left right : Numerics.Representations.FixedInt width) : Numerics.Representations.FixedInt width

Same-scale addition with saturation at the signed coefficient bounds.

@[inline]

def FloatLib.Floats.Formats.FixedPoint.Bounded.saturatingSub {width : ℕ} (left right : Numerics.Representations.FixedInt width) : Numerics.Representations.FixedInt width

Same-scale subtraction with saturation at the signed coefficient bounds.

@[inline]

def FloatLib.Floats.Formats.FixedPoint.Bounded.saturatingMul (outWidth : ℕ) {leftWidth rightWidth : ℕ} (left : Numerics.Representations.FixedInt leftWidth) (right : Numerics.Representations.FixedInt rightWidth) : Numerics.Representations.FixedInt outWidth

Product with its exact coefficient saturated to outWidth signed bits.