Correctness of configured bounded fixed-point operations

Complete word conversions recover the stored code, and encoding preserves in-range words. Arithmetic with (overflow := .wrap) decodes to centered modular arithmetic on signed coefficients. The default .reject addition and subtraction are exact whenever they succeed, and so is multiplication at a positive destination width. At positive widths, (overflow := .saturate) decodes to the exact coefficient clamped to the signed 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_add_wrap {radix : Numerics.Radix} {fractionalDigits width : ℕ} (left right : BoundedFixedPoint radix fractionalDigits width) : toRat (left.add right OverflowPolicy.wrap) = Formats.FixedPoint.Bounded.valueOfCoefficient radix fractionalDigits ((left.coefficient + right.coefficient).bmod (2 ^ width))

Addition with .wrap decodes to the coefficient sum, centered modulo 2 ^ width.

@[simp]

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

Subtraction with .wrap decodes to the coefficient difference, centered modulo 2 ^ width.

@[simp]

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

Multiplication with .wrap decodes to the coefficient product, centered mod 2 ^ outWidth.

theorem FloatLib.Floats.ExecFloat.BoundedFixedPoint.add_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.add right = some (left.add right OverflowPolicy.wrap)

Addition succeeds with the wrapped sum when the exact coefficient sum fits.

theorem FloatLib.Floats.ExecFloat.BoundedFixedPoint.sub_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.sub right = some (left.sub right OverflowPolicy.wrap)

Subtraction succeeds with the wrapped difference when the exact coefficient fits.

theorem FloatLib.Floats.ExecFloat.BoundedFixedPoint.mul_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)) : mul outWidth left right = some (ofCoefficient (left.coefficient * right.coefficient))

Multiplication succeeds with the encoded product when the exact coefficient fits.

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

Rejecting 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_sub_eq_some {radix : Numerics.Radix} {fractionalDigits width : ℕ} {left right result : BoundedFixedPoint radix fractionalDigits width} (hsome : left.sub right = some result) : result.toRat = left.toRat - right.toRat

Rejecting 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_mul_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 : mul outWidth left right = some result) : result.toRat = left.toRat * right.toRat

Rejecting 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_add_saturate {radix : Numerics.Radix} {fractionalDigits width : ℕ} (hwidth : 0 < width) (left right : BoundedFixedPoint radix fractionalDigits width) : toRat (left.add right OverflowPolicy.saturate) = Formats.FixedPoint.Bounded.valueOfCoefficient radix fractionalDigits (Numerics.Representations.FixedInt.clamp width (left.coefficient + right.coefficient))

Addition with .saturate decodes to exact coefficient addition followed by clamping.

@[simp]

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

Subtraction with .saturate decodes to exact coefficient subtraction and clamping.

@[simp]

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

Multiplication with .saturate decodes to the clamped exact product at the composed scale.