Operation refinements for fixed-width signed integers

Fixed-width arithmetic has three useful policies: wrapping returns centered modular arithmetic, checked arithmetic returns a result only when the exact integer is representable, and saturating arithmetic clamps at the signed endpoints.

This module exposes all three through the same generic Operation contracts used by the rest of the library. Algorithms can therefore state the policy they require without depending on BitVec internals, while execution still uses the compact two's-complement carrier.

theorem FloatLib.Numerics.Representations.FixedInt.wrapAdd_refines (width : ℕ) : Operation.Finite2 (numericalSystem width) (numericalSystem width) (numericalSystem width) wrapAdd fun (left right : ℤ) => (left + right).bmod (2 ^ width)

Wrapping addition refines centered reduction modulo 2 ^ width.

theorem FloatLib.Numerics.Representations.FixedInt.wrapSub_refines (width : ℕ) : Operation.Finite2 (numericalSystem width) (numericalSystem width) (numericalSystem width) wrapSub fun (left right : ℤ) => (left - right).bmod (2 ^ width)

Wrapping subtraction refines centered reduction modulo 2 ^ width.

theorem FloatLib.Numerics.Representations.FixedInt.wrapMul_refines (width : ℕ) : Operation.Finite2 (numericalSystem width) (numericalSystem width) (numericalSystem width) wrapMul fun (left right : ℤ) => (left * right).bmod (2 ^ width)

Wrapping multiplication refines centered reduction modulo 2 ^ width.

theorem FloatLib.Numerics.Representations.FixedInt.checkedAdd_refines {width : ℕ} (hwidth : 0 < width) : Operation.Checked2On (numericalSystem width) (numericalSystem width) (numericalSystem width) checkedAdd (fun (left right : ℤ) => NumericalValue.finite (left + right)) fun (left right : ℤ) => InRange width (left + right)

Checked addition returns the exact sum whenever it is representable.

theorem FloatLib.Numerics.Representations.FixedInt.checkedSub_refines {width : ℕ} (hwidth : 0 < width) : Operation.Checked2On (numericalSystem width) (numericalSystem width) (numericalSystem width) checkedSub (fun (left right : ℤ) => NumericalValue.finite (left - right)) fun (left right : ℤ) => InRange width (left - right)

Checked subtraction returns the exact difference whenever it is representable.

theorem FloatLib.Numerics.Representations.FixedInt.checkedMul_refines {width : ℕ} (hwidth : 0 < width) : Operation.Checked2On (numericalSystem width) (numericalSystem width) (numericalSystem width) checkedMul (fun (left right : ℤ) => NumericalValue.finite (left * right)) fun (left right : ℤ) => InRange width (left * right)

Checked multiplication returns the exact product whenever it is representable.

theorem FloatLib.Numerics.Representations.FixedInt.saturatingAdd_refines {width : ℕ} (hwidth : 0 < width) : Operation.Finite2 (numericalSystem width) (numericalSystem width) (numericalSystem width) saturatingAdd fun (left right : ℤ) => clamp width (left + right)

Saturating addition refines exact addition followed by signed-range clamping.

theorem FloatLib.Numerics.Representations.FixedInt.saturatingSub_refines {width : ℕ} (hwidth : 0 < width) : Operation.Finite2 (numericalSystem width) (numericalSystem width) (numericalSystem width) saturatingSub fun (left right : ℤ) => clamp width (left - right)

Saturating subtraction refines exact subtraction followed by signed-range clamping.

theorem FloatLib.Numerics.Representations.FixedInt.saturatingMul_refines {width : ℕ} (hwidth : 0 < width) : Operation.Finite2 (numericalSystem width) (numericalSystem width) (numericalSystem width) saturatingMul fun (left right : ℤ) => clamp width (left * right)

Saturating multiplication refines exact multiplication followed by signed-range clamping.