Representation semantics of fixed-width signed integers

The executable two's-complement carrier has a NumericalSystem interpretation. The representation laws characterize the signed interval, encoding and decoding, and the clamp used by saturating arithmetic.

Keeping this adapter separate from arithmetic is useful: generic operation contracts only need to know what a code denotes, while the implementation remains free to use BitVec overflow instructions and fixed-width storage.

def FloatLib.Numerics.Representations.FixedInt.numericalSystem (width : ℕ) : NumericalSystem

Fixed-width integers interpreted as their signed two's-complement values.

@[reducible, inline]

abbrev FloatLib.Numerics.Representations.FixedInt.AtFinite (width : ℕ) (value : ℤ) : Type

A fixed-width word with an erased proof of its signed value.

@[simp]

theorem FloatLib.Numerics.Representations.FixedInt.numericalSystem_represents_iff {width : ℕ} (code : FixedInt width) (value : ℤ) : (numericalSystem width).Represents code value ↔ code.toInt = value

Representation by a fixed-width integer is equality with its signed two's-complement value.

@[simp]

theorem FloatLib.Numerics.Representations.FixedInt.toInt_ofInt {width : ℕ} (value : ℤ) : (ofInt value).toInt = value.bmod (2 ^ width)

Converting an integer to fixed width denotes centered reduction modulo 2 ^ width.

@[simp]

theorem FloatLib.Numerics.Representations.FixedInt.ofInt_toInt {width : ℕ} (value : FixedInt width) : ofInt value.toInt = value

Re-encoding the signed value of a fixed-width integer recovers its original bits.

@[simp]

theorem FloatLib.Numerics.Representations.FixedInt.toInt_minCode {width : ℕ} : (minCode width).toInt = minValue width

The minimum fixed-width code denotes the signed lower bound.

@[simp]

theorem FloatLib.Numerics.Representations.FixedInt.toInt_maxCode {width : ℕ} : (maxCode width).toInt = maxValue width

The maximum fixed-width code denotes the signed upper bound.

theorem FloatLib.Numerics.Representations.FixedInt.minValue_eq {width : ℕ} (hwidth : 0 < width) : minValue width = -2 ^ (width - 1)

At positive width, the signed lower bound is -(2 ^ (width - 1)).

theorem FloatLib.Numerics.Representations.FixedInt.maxValue_eq (width : ℕ) : maxValue width = 2 ^ (width - 1) - 1

The signed upper bound is 2 ^ (width - 1) - 1.

theorem FloatLib.Numerics.Representations.FixedInt.minValue_le_maxValue {width : ℕ} (hwidth : 0 < width) : minValue width ≤ maxValue width

At positive width, the signed storage interval is nonempty.

theorem FloatLib.Numerics.Representations.FixedInt.clamp_inRange {width : ℕ} (hwidth : 0 < width) (value : ℤ) : InRange width (clamp width value)

Clamping at positive width always produces an in-range integer.

theorem FloatLib.Numerics.Representations.FixedInt.clamp_eq_self {width : ℕ} {value : ℤ} (hvalue : InRange width value) : clamp width value = value

Clamping fixes every integer already in the signed storage interval.

theorem FloatLib.Numerics.Representations.FixedInt.toInt_ofInt_eq_self {width : ℕ} (hwidth : 0 < width) {value : ℤ} (hvalue : InRange width value) : (ofInt value).toInt = value

Encoding an in-range integer at positive width preserves its exact signed value.

@[simp]

theorem FloatLib.Numerics.Representations.FixedInt.toInt_ofIntSaturating {width : ℕ} (hwidth : 0 < width) (value : ℤ) : (ofIntSaturating value).toInt = clamp width value

Saturating conversion denotes exact clamping to the signed storage interval.