Correctness of configured bounded fixed-point operations

Complete word conversions recover the stored code, and encoding preserves in-range words. Wrapping arithmetic decodes to centered modular arithmetic on signed coefficients. Checked addition and subtraction are exact whenever they succeed; the corresponding multiplication theorem assumes a positive destination width. At positive widths, saturating arithmetic decodes to the exact coefficient clamped to the signed destination range.

@[simp]

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

Unwrapping a freshly wrapped bounded fixed-point code returns the original code.

@[simp]

theorem FloatLib.Floats.ExecFloat.BoundedFixedPoint.ofCode_toCode {radix : Numerics.Radix} {fractionalDigits width : ℕ} (value : BoundedFixedPoint radix fractionalDigits width) : ofCode value.toCode = value

Rewrapping the code of a bounded fixed-point value returns the original value.

@[simp]

theorem FloatLib.Floats.ExecFloat.BoundedFixedPoint.ofNatBits_toNatBits {radix : Numerics.Radix} {fractionalDigits width : ℕ} (value : BoundedFixedPoint radix fractionalDigits width) : ofNatBits value.toNatBits = value

Reconstructing a value from its complete word preserves the value.

@[simp]

theorem FloatLib.Floats.ExecFloat.BoundedFixedPoint.toNatBits_ofNatBits_of_lt {radix : Numerics.Radix} {fractionalDigits width : ℕ} (bits : ℕ) (bits_lt : bits < 2 ^ width) : (ofNatBits bits).toNatBits = bits

An in-range word is unchanged by bounded fixed-point encoding and decoding.

@[simp]

theorem FloatLib.Floats.ExecFloat.BoundedFixedPoint.coefficient_ofCoefficient {radix : Numerics.Radix} {fractionalDigits width : ℕ} (stored : ℤ) : (ofCoefficient stored).coefficient = (Numerics.Representations.FixedInt.ofInt stored).toInt

Constructing from an integer stores its two's-complement residue at the selected width.

@[simp]

theorem FloatLib.Floats.ExecFloat.BoundedFixedPoint.toRat_wrapAdd {radix : Numerics.Radix} {fractionalDigits width : ℕ} (left right : BoundedFixedPoint radix fractionalDigits width) : (left.wrapAdd right).toRat = Formats.FixedPoint.Bounded.valueOfCoefficient radix fractionalDigits ((left.coefficient + right.coefficient).bmod (2 ^ width))

Wrapping addition decodes to coefficient addition modulo 2 ^ width.

@[simp]

theorem FloatLib.Floats.ExecFloat.BoundedFixedPoint.toRat_wrapSub {radix : Numerics.Radix} {fractionalDigits width : ℕ} (left right : BoundedFixedPoint radix fractionalDigits width) : (left.wrapSub right).toRat = Formats.FixedPoint.Bounded.valueOfCoefficient radix fractionalDigits ((left.coefficient - right.coefficient).bmod (2 ^ width))

Wrapping subtraction decodes to coefficient subtraction modulo 2 ^ width.

@[simp]

theorem FloatLib.Floats.ExecFloat.BoundedFixedPoint.toRat_wrapMul {radix : Numerics.Radix} {p q leftWidth rightWidth outWidth : ℕ} (left : BoundedFixedPoint radix p leftWidth) (right : BoundedFixedPoint radix q rightWidth) : (wrapMul outWidth left right).toRat = Formats.FixedPoint.Bounded.valueOfCoefficient radix (p + q) ((left.coefficient * right.coefficient).bmod (2 ^ outWidth))

Wrapping multiplication decodes to coefficient multiplication modulo 2 ^ outWidth.

theorem FloatLib.Floats.ExecFloat.BoundedFixedPoint.checkedAdd_eq_some {radix : Numerics.Radix} {fractionalDigits width : ℕ} (hwidth : 0 < width) (left right : BoundedFixedPoint radix fractionalDigits width) (hresult : Numerics.Representations.FixedInt.InRange width (left.coefficient + right.coefficient)) : left.checkedAdd right = some (left.wrapAdd right)

Checked addition succeeds with the wrapped sum when the exact coefficient sum fits.

theorem FloatLib.Floats.ExecFloat.BoundedFixedPoint.checkedSub_eq_some {radix : Numerics.Radix} {fractionalDigits width : ℕ} (hwidth : 0 < width) (left right : BoundedFixedPoint radix fractionalDigits width) (hresult : Numerics.Representations.FixedInt.InRange width (left.coefficient - right.coefficient)) : left.checkedSub right = some (left.wrapSub right)

Checked subtraction succeeds with the wrapped difference when the exact coefficient fits.

theorem FloatLib.Floats.ExecFloat.BoundedFixedPoint.checkedMul_eq_some {radix : Numerics.Radix} {p q leftWidth rightWidth outWidth : ℕ} (left : BoundedFixedPoint radix p leftWidth) (right : BoundedFixedPoint radix q rightWidth) (hresult : Numerics.Representations.FixedInt.InRange outWidth (left.coefficient * right.coefficient)) : checkedMul outWidth left right = some (ofCoefficient (left.coefficient * right.coefficient))

Checked multiplication succeeds with the encoded product when the exact coefficient fits.

theorem FloatLib.Floats.ExecFloat.BoundedFixedPoint.toRat_of_checkedAdd_eq_some {radix : Numerics.Radix} {fractionalDigits width : ℕ} {left right result : BoundedFixedPoint radix fractionalDigits width} (hsome : left.checkedAdd right = some result) : result.toRat = left.toRat + right.toRat

Checked addition is exact: whenever it returns a value, that value decodes to the rational sum of the operands. No width hypothesis is needed because success already certifies the absence of signed overflow.

theorem FloatLib.Floats.ExecFloat.BoundedFixedPoint.toRat_of_checkedSub_eq_some {radix : Numerics.Radix} {fractionalDigits width : ℕ} {left right result : BoundedFixedPoint radix fractionalDigits width} (hsome : left.checkedSub right = some result) : result.toRat = left.toRat - right.toRat

Checked subtraction is exact: whenever it returns a value, that value decodes to the rational difference of the operands.

theorem FloatLib.Floats.ExecFloat.BoundedFixedPoint.toRat_of_checkedMul_eq_some {radix : Numerics.Radix} {p q leftWidth rightWidth outWidth : ℕ} (houtWidth : 0 < outWidth) {left : BoundedFixedPoint radix p leftWidth} {right : BoundedFixedPoint radix q rightWidth} {result : BoundedFixedPoint radix (p + q) outWidth} (hsome : checkedMul outWidth left right = some result) : result.toRat = left.toRat * right.toRat

Checked multiplication is exact: whenever it returns a value at a positive destination width, that value decodes to the rational product of the operands at the composed scale.

@[simp]

theorem FloatLib.Floats.ExecFloat.BoundedFixedPoint.toRat_saturatingAdd {radix : Numerics.Radix} {fractionalDigits width : ℕ} (hwidth : 0 < width) (left right : BoundedFixedPoint radix fractionalDigits width) : (left.saturatingAdd right).toRat = Formats.FixedPoint.Bounded.valueOfCoefficient radix fractionalDigits (Numerics.Representations.FixedInt.clamp width (left.coefficient + right.coefficient))

Saturating addition decodes to exact coefficient addition followed by clamping.

@[simp]

theorem FloatLib.Floats.ExecFloat.BoundedFixedPoint.toRat_saturatingSub {radix : Numerics.Radix} {fractionalDigits width : ℕ} (hwidth : 0 < width) (left right : BoundedFixedPoint radix fractionalDigits width) : (left.saturatingSub right).toRat = Formats.FixedPoint.Bounded.valueOfCoefficient radix fractionalDigits (Numerics.Representations.FixedInt.clamp width (left.coefficient - right.coefficient))

Saturating subtraction decodes to exact coefficient subtraction followed by clamping.

@[simp]

theorem FloatLib.Floats.ExecFloat.BoundedFixedPoint.toRat_saturatingMul {radix : Numerics.Radix} {p q leftWidth rightWidth outWidth : ℕ} (houtWidth : 0 < outWidth) (left : BoundedFixedPoint radix p leftWidth) (right : BoundedFixedPoint radix q rightWidth) : (saturatingMul outWidth left right).toRat = Formats.FixedPoint.Bounded.valueOfCoefficient radix (p + q) (Numerics.Representations.FixedInt.clamp outWidth (left.coefficient * right.coefficient))

Saturating multiplication decodes to the clamped exact product at the composed scale.