Arithmetic semantics of fixed-width signed integers

These are the carrier-level correctness lemmas for wrapping, checked, and saturating signed arithmetic. They connect overflow predicates and BitVec operations to ordinary integer sums, differences, and products.

The file deliberately stops short of the library-wide operation interface. Refinement builds that reusable layer from these concrete facts, which keeps low-level overflow reasoning out of generic numerical proofs.

@[simp]

theorem FloatLib.Numerics.Representations.FixedInt.toInt_wrapAdd {width : ℕ} (left right : FixedInt width) : (left.wrapAdd right).toInt = (left.toInt + right.toInt).bmod (2 ^ width)

Wrapping addition denotes centered modular addition.

@[simp]

theorem FloatLib.Numerics.Representations.FixedInt.toInt_wrapSub {width : ℕ} (left right : FixedInt width) : (left.wrapSub right).toInt = (left.toInt - right.toInt).bmod (2 ^ width)

Wrapping subtraction denotes centered modular subtraction.

@[simp]

theorem FloatLib.Numerics.Representations.FixedInt.toInt_wrapMul {width : ℕ} (left right : FixedInt width) : (left.wrapMul right).toInt = (left.toInt * right.toInt).bmod (2 ^ width)

Wrapping multiplication denotes centered modular multiplication.

theorem FloatLib.Numerics.Representations.FixedInt.checkedAdd_eq_some {width : ℕ} (hwidth : 0 < width) (left right : FixedInt width) (hresult : InRange width (left.toInt + right.toInt)) : left.checkedAdd right = some (left.wrapAdd right)

Checked addition succeeds when the exact sum is in range.

theorem FloatLib.Numerics.Representations.FixedInt.checkedSub_eq_some {width : ℕ} (hwidth : 0 < width) (left right : FixedInt width) (hresult : InRange width (left.toInt - right.toInt)) : left.checkedSub right = some (left.wrapSub right)

Checked subtraction succeeds when the exact difference is in range.

theorem FloatLib.Numerics.Representations.FixedInt.checkedMul_eq_some {width : ℕ} (hwidth : 0 < width) (left right : FixedInt width) (hresult : InRange width (left.toInt * right.toInt)) : left.checkedMul right = some (left.wrapMul right)

Checked multiplication succeeds when the exact product is in range.

theorem FloatLib.Numerics.Representations.FixedInt.toInt_wrapAdd_of_inRange {width : ℕ} (hwidth : 0 < width) (left right : FixedInt width) (hresult : InRange width (left.toInt + right.toInt)) : (left.wrapAdd right).toInt = left.toInt + right.toInt

Wrapping addition is exact whenever its mathematical sum is in range.

theorem FloatLib.Numerics.Representations.FixedInt.toInt_wrapSub_of_inRange {width : ℕ} (hwidth : 0 < width) (left right : FixedInt width) (hresult : InRange width (left.toInt - right.toInt)) : (left.wrapSub right).toInt = left.toInt - right.toInt

Wrapping subtraction is exact whenever its mathematical difference is in range.

theorem FloatLib.Numerics.Representations.FixedInt.toInt_wrapMul_of_inRange {width : ℕ} (hwidth : 0 < width) (left right : FixedInt width) (hresult : InRange width (left.toInt * right.toInt)) : (left.wrapMul right).toInt = left.toInt * right.toInt

Wrapping multiplication is exact whenever its mathematical product is in range.

@[simp]

theorem FloatLib.Numerics.Representations.FixedInt.toInt_saturatingAdd {width : ℕ} (hwidth : 0 < width) (left right : FixedInt width) : (left.saturatingAdd right).toInt = clamp width (left.toInt + right.toInt)

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

@[simp]

theorem FloatLib.Numerics.Representations.FixedInt.toInt_saturatingSub {width : ℕ} (hwidth : 0 < width) (left right : FixedInt width) : (left.saturatingSub right).toInt = clamp width (left.toInt - right.toInt)

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

@[simp]

theorem FloatLib.Numerics.Representations.FixedInt.toInt_saturatingMul {width : ℕ} (hwidth : 0 < width) (left right : FixedInt width) : (left.saturatingMul right).toInt = clamp width (left.toInt * right.toInt)

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