Correctness of bounded fixed-point semantics

The bounded fixed-point kernels satisfy the rational contracts defined in Semantics.Core. The operation contracts distinguish three policies:

• wrapping operations denote centered reduction of the exact coefficient;
• checked operations denote exact rational arithmetic when the destination coefficient fits;
• saturating operations denote exact coefficient arithmetic followed by signed-range clamping.

The wrapping addition, subtraction, and multiplication kernels use direct BitVec operations.

theorem FloatLib.Floats.Formats.FixedPoint.Bounded.scale_pos (radix : Numerics.Radix) (fractionalDigits : ℕ) : 0 < scale radix fractionalDigits

The storage scale is always positive.

theorem FloatLib.Floats.Formats.FixedPoint.Bounded.scale_ne_zero (radix : Numerics.Radix) (fractionalDigits : ℕ) : scale radix fractionalDigits ≠ 0

The storage scale is nonzero.

@[simp]

theorem FloatLib.Floats.Formats.FixedPoint.Bounded.toRat_eq_valueOfCoefficient {radix : Numerics.Radix} {fractionalDigits width : ℕ} (code : Code radix fractionalDigits width) : toRat radix fractionalDigits code = valueOfCoefficient radix fractionalDigits (coefficient code)

Bounded decoding is valueOfCoefficient applied to the stored signed coefficient.

theorem FloatLib.Floats.Formats.FixedPoint.Bounded.coefficientOf_toRat {radix : Numerics.Radix} {fractionalDigits width : ℕ} (code : Code radix fractionalDigits width) : coefficientOf radix fractionalDigits (toRat radix fractionalDigits code) = coefficient code

Coefficient recovery is exact on every bounded fixed-point code.

@[simp]

theorem FloatLib.Floats.Formats.FixedPoint.Bounded.toUnbounded_toRat {radix : Numerics.Radix} {fractionalDigits width : ℕ} (code : Code radix fractionalDigits width) : (toUnbounded code).toRat = toRat radix fractionalDigits code

Forgetting the coefficient bound preserves the exact rational value.

@[simp]

theorem FloatLib.Floats.Formats.FixedPoint.Bounded.numericalSystem_represents_iff {radix : Numerics.Radix} {fractionalDigits width : ℕ} (code : Code radix fractionalDigits width) (value : ℚ) : (numericalSystem radix fractionalDigits width).Represents code value ↔ toRat radix fractionalDigits code = value

Representation in the bounded system is equality of decoded rational values.

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

Decoding wrapping addition exposes centered coefficient reduction modulo 2 ^ width.

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

Decoding wrapping subtraction exposes centered coefficient reduction modulo 2 ^ width.

theorem FloatLib.Floats.Formats.FixedPoint.Bounded.coefficient_wrapMul {leftWidth rightWidth outWidth : ℕ} (left : Numerics.Representations.FixedInt leftWidth) (right : Numerics.Representations.FixedInt rightWidth) : coefficient (wrapMul outWidth left right) = (coefficient left * coefficient right).bmod (2 ^ outWidth)

Wrapping multiplication stores the exact coefficient product modulo 2 ^ outWidth.

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

Decoding wrapping multiplication exposes the reduced product at the composed scale.

theorem FloatLib.Floats.Formats.FixedPoint.Bounded.checkedMul_eq_some {leftWidth rightWidth outWidth : ℕ} (left : Numerics.Representations.FixedInt leftWidth) (right : Numerics.Representations.FixedInt rightWidth) (hresult : Numerics.Representations.FixedInt.InRange outWidth (coefficient left * coefficient right)) : checkedMul outWidth left right = some (Numerics.Representations.FixedInt.ofInt (coefficient left * coefficient right))

Checked multiplication returns the exact product when it fits the destination width.

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

Decoding saturating addition exposes exact coefficient addition followed by clamping.

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

Decoding saturating subtraction exposes exact coefficient subtraction followed by clamping.

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

Decoding saturating multiplication exposes the clamped product at the composed scale.

theorem FloatLib.Floats.Formats.FixedPoint.Bounded.toRat_wrapAdd_of_inRange {radix : Numerics.Radix} {fractionalDigits width : ℕ} (hwidth : 0 < width) (left right : Code radix fractionalDigits width) (hresult : Numerics.Representations.FixedInt.InRange width (coefficient left + coefficient right)) : toRat radix fractionalDigits (wrapAdd left right) = toRat radix fractionalDigits left + toRat radix fractionalDigits right

Decoding a wrapped sum whose exact coefficient fits the width gives the exact rational sum.

theorem FloatLib.Floats.Formats.FixedPoint.Bounded.toRat_wrapSub_of_inRange {radix : Numerics.Radix} {fractionalDigits width : ℕ} (hwidth : 0 < width) (left right : Code radix fractionalDigits width) (hresult : Numerics.Representations.FixedInt.InRange width (coefficient left - coefficient right)) : toRat radix fractionalDigits (wrapSub left right) = toRat radix fractionalDigits left - toRat radix fractionalDigits right

Decoding a wrapped difference whose exact coefficient fits the width gives the exact rational difference.

theorem FloatLib.Floats.Formats.FixedPoint.Bounded.toRat_ofInt_mul_of_inRange {radix : Numerics.Radix} {p q leftWidth rightWidth outWidth : ℕ} (houtWidth : 0 < outWidth) (left : Code radix p leftWidth) (right : Code radix q rightWidth) (hresult : Numerics.Representations.FixedInt.InRange outWidth (coefficient left * coefficient right)) : toRat radix (p + q) (Numerics.Representations.FixedInt.ofInt (coefficient left * coefficient right)) = toRat radix p left * toRat radix q right

Encoding an exact coefficient product that fits the destination width decodes to the rational product at the composed scale.

theorem FloatLib.Floats.Formats.FixedPoint.Bounded.checked2On_of_toRat_eq {radix : Numerics.Radix} {p q r leftWidth rightWidth outWidth : ℕ} {run : Code radix p leftWidth → Code radix q rightWidth → Option (Code radix r outWidth)} {spec : ℚ → ℚ → ℚ} {pre : ℚ → ℚ → Prop} (h : ∀ (left : Numerics.Representations.FixedInt leftWidth) (right : Numerics.Representations.FixedInt rightWidth), pre (toRat radix p left) (toRat radix q right) → ∃ (result : Code radix r outWidth), run left right = some result ∧ toRat radix r result = spec (toRat radix p left) (toRat radix q right)) : Numerics.Operation.Checked2On (numericalSystem radix p leftWidth) (numericalSystem radix q rightWidth) (numericalSystem radix r outWidth) run (fun (left : (numericalSystem radix p leftWidth).Scalar) (right : (numericalSystem radix q rightWidth).Scalar) => Numerics.NumericalValue.finite (spec left right)) pre

A checked binary kernel satisfies a rational specification under a precondition once, on operands meeting the precondition, it returns a code decoding to the specified value.

theorem FloatLib.Floats.Formats.FixedPoint.Bounded.wrapAdd_refines (radix : Numerics.Radix) (fractionalDigits width : ℕ) : Numerics.Operation.Finite2 (numericalSystem radix fractionalDigits width) (numericalSystem radix fractionalDigits width) (numericalSystem radix fractionalDigits width) wrapAdd (wrapAddValue radix fractionalDigits width)

Wrapping addition refines centered coefficient reduction.

theorem FloatLib.Floats.Formats.FixedPoint.Bounded.wrapSub_refines (radix : Numerics.Radix) (fractionalDigits width : ℕ) : Numerics.Operation.Finite2 (numericalSystem radix fractionalDigits width) (numericalSystem radix fractionalDigits width) (numericalSystem radix fractionalDigits width) wrapSub (wrapSubValue radix fractionalDigits width)

Wrapping subtraction refines centered coefficient reduction.

theorem FloatLib.Floats.Formats.FixedPoint.Bounded.wrapMul_refines (radix : Numerics.Radix) (p q leftWidth rightWidth outWidth : ℕ) : Numerics.Operation.Finite2 (numericalSystem radix p leftWidth) (numericalSystem radix q rightWidth) (numericalSystem radix (p + q) outWidth) (wrapMul outWidth) (wrapMulValue radix p q outWidth)

Cross-width wrapping multiplication refines centered coefficient reduction.

theorem FloatLib.Floats.Formats.FixedPoint.Bounded.checkedAdd_refines {radix : Numerics.Radix} {fractionalDigits width : ℕ} (hwidth : 0 < width) : Numerics.Operation.Checked2On (numericalSystem radix fractionalDigits width) (numericalSystem radix fractionalDigits width) (numericalSystem radix fractionalDigits width) checkedAdd (fun (left right : ℚ) => Numerics.NumericalValue.finite (left + right)) fun (left right : (numericalSystem radix fractionalDigits width).Scalar) => Numerics.Representations.FixedInt.InRange width (coefficientOf radix fractionalDigits left + coefficientOf radix fractionalDigits right)

Checked addition returns the exact rational sum whenever its coefficient fits.

theorem FloatLib.Floats.Formats.FixedPoint.Bounded.checkedSub_refines {radix : Numerics.Radix} {fractionalDigits width : ℕ} (hwidth : 0 < width) : Numerics.Operation.Checked2On (numericalSystem radix fractionalDigits width) (numericalSystem radix fractionalDigits width) (numericalSystem radix fractionalDigits width) checkedSub (fun (left right : ℚ) => Numerics.NumericalValue.finite (left - right)) fun (left right : (numericalSystem radix fractionalDigits width).Scalar) => Numerics.Representations.FixedInt.InRange width (coefficientOf radix fractionalDigits left - coefficientOf radix fractionalDigits right)

Checked subtraction returns the exact rational difference whenever its coefficient fits.

theorem FloatLib.Floats.Formats.FixedPoint.Bounded.checkedMul_refines {radix : Numerics.Radix} {p q leftWidth rightWidth outWidth : ℕ} (houtWidth : 0 < outWidth) : Numerics.Operation.Checked2On (numericalSystem radix p leftWidth) (numericalSystem radix q rightWidth) (numericalSystem radix (p + q) outWidth) (checkedMul outWidth) (fun (left right : ℚ) => Numerics.NumericalValue.finite (left * right)) fun (left : (numericalSystem radix p leftWidth).Scalar) (right : (numericalSystem radix q rightWidth).Scalar) => Numerics.Representations.FixedInt.InRange outWidth (coefficientOf radix p left * coefficientOf radix q right)

Checked multiplication returns the exact rational product whenever its coefficient fits.

theorem FloatLib.Floats.Formats.FixedPoint.Bounded.saturatingAdd_refines {radix : Numerics.Radix} {fractionalDigits width : ℕ} (hwidth : 0 < width) : Numerics.Operation.Finite2 (numericalSystem radix fractionalDigits width) (numericalSystem radix fractionalDigits width) (numericalSystem radix fractionalDigits width) saturatingAdd (saturatingAddValue radix fractionalDigits width)

Saturating addition refines exact coefficient addition followed by clamping.

theorem FloatLib.Floats.Formats.FixedPoint.Bounded.saturatingSub_refines {radix : Numerics.Radix} {fractionalDigits width : ℕ} (hwidth : 0 < width) : Numerics.Operation.Finite2 (numericalSystem radix fractionalDigits width) (numericalSystem radix fractionalDigits width) (numericalSystem radix fractionalDigits width) saturatingSub (saturatingSubValue radix fractionalDigits width)

Saturating subtraction refines exact coefficient subtraction followed by clamping.

theorem FloatLib.Floats.Formats.FixedPoint.Bounded.saturatingMul_refines {radix : Numerics.Radix} {p q leftWidth rightWidth outWidth : ℕ} (houtWidth : 0 < outWidth) : Numerics.Operation.Finite2 (numericalSystem radix p leftWidth) (numericalSystem radix q rightWidth) (numericalSystem radix (p + q) outWidth) (saturatingMul outWidth) (saturatingMulValue radix p q outWidth)

Saturating multiplication refines exact coefficient multiplication followed by clamping.