Fixed-width signed integers

FixedInt width stores a two's-complement integer in exactly width bits. The policy is explicit in every arithmetic name:

• wrapAdd, wrapSub, and wrapMul compute modulo 2^width;
• checked operations return none on signed overflow;
• saturating operations clamp to the signed range.

The wrapping kernels operate directly on BitVec. Checked operations use Lean's signed-overflow tests. Saturating operations compute the exact Int result, clamp it to the signed range, and encode it.

structure FloatLib.Numerics.Representations.FixedInt (width : ℕ) : Type

A two's-complement integer stored in exactly width bits.

• bits : BitVec width

  Complete two's-complement bit pattern.

@[instance_reducible]

instance FloatLib.Numerics.Representations.instDecidableEqFixedInt {width✝ : ℕ} : DecidableEq (FixedInt width✝)

def FloatLib.Numerics.Representations.instDecidableEqFixedInt.decEq {width✝ : ℕ} (x✝ x✝¹ : FixedInt width✝) : Decidable (x✝ = x✝¹)

@[instance_reducible]

instance FloatLib.Numerics.Representations.instReprFixedInt {width✝ : ℕ} : Repr (FixedInt width✝)

def FloatLib.Numerics.Representations.instReprFixedInt.repr {width✝ : ℕ} : FixedInt width✝ → ℕ → Std.Format

@[inline]

def FloatLib.Numerics.Representations.FixedInt.ofNatBits {width : ℕ} (value : ℕ) : FixedInt width

Construct a fixed-width integer from the low width bits of a natural number.

@[inline]

def FloatLib.Numerics.Representations.FixedInt.toNatBits {width : ℕ} (value : FixedInt width) : ℕ

Extract the unsigned bit pattern.

theorem FloatLib.Numerics.Representations.FixedInt.toNatBits_lt_modulus {width : ℕ} (value : FixedInt width) : value.toNatBits < 2 ^ width

Every exact-width word lies below its unsigned modulus.

@[simp]

theorem FloatLib.Numerics.Representations.FixedInt.ofNatBits_toNatBits {width : ℕ} (value : FixedInt width) : ofNatBits value.toNatBits = value

Re-encoding a fixed integer's complete bit pattern preserves it.

@[simp]

theorem FloatLib.Numerics.Representations.FixedInt.toNatBits_ofNatBits_of_lt {width : ℕ} (bits : ℕ) (bits_lt : bits < 2 ^ width) : (ofNatBits bits).toNatBits = bits

An in-range unsigned bit pattern is unchanged by exact-width encoding.

@[inline]

def FloatLib.Numerics.Representations.FixedInt.toInt {width : ℕ} (value : FixedInt width) : ℤ

Interpret a word as a signed two's-complement integer.

@[inline]

def FloatLib.Numerics.Representations.FixedInt.ofInt {width : ℕ} (value : ℤ) : FixedInt width

Encode an integer modulo 2^width.

@[inline]

def FloatLib.Numerics.Representations.FixedInt.minValue (width : ℕ) : ℤ

Least signed integer representable at width.

@[inline]

def FloatLib.Numerics.Representations.FixedInt.maxValue (width : ℕ) : ℤ

Greatest signed integer representable at width.

def FloatLib.Numerics.Representations.FixedInt.InRange (width : ℕ) (value : ℤ) : Prop

Whether an integer lies in the signed range of width bits.

@[instance_reducible]

instance FloatLib.Numerics.Representations.FixedInt.instDecidableInRange (width : ℕ) (value : ℤ) : Decidable (InRange width value)

@[inline]

def FloatLib.Numerics.Representations.FixedInt.clamp (width : ℕ) (value : ℤ) : ℤ

Clamp an integer to the signed range of width bits, the shared Saturating.clamp applied to the range endpoints.

@[inline]

def FloatLib.Numerics.Representations.FixedInt.minCode (width : ℕ) : FixedInt width

The least representable word, denoting minValue width.

@[inline]

def FloatLib.Numerics.Representations.FixedInt.maxCode (width : ℕ) : FixedInt width

The greatest representable word, denoting maxValue width.

@[inline]

def FloatLib.Numerics.Representations.FixedInt.wrapAdd {width : ℕ} (left right : FixedInt width) : FixedInt width

Two's-complement addition modulo 2^width.

@[inline]

def FloatLib.Numerics.Representations.FixedInt.wrapSub {width : ℕ} (left right : FixedInt width) : FixedInt width

Two's-complement subtraction modulo 2^width.

@[inline]

def FloatLib.Numerics.Representations.FixedInt.wrapMul {width : ℕ} (left right : FixedInt width) : FixedInt width

Two's-complement multiplication modulo 2^width.

@[inline]

def FloatLib.Numerics.Representations.FixedInt.checkedAdd {width : ℕ} (left right : FixedInt width) : Option (FixedInt width)

Return the exact sum when it fits in width signed bits.

@[inline]

def FloatLib.Numerics.Representations.FixedInt.checkedSub {width : ℕ} (left right : FixedInt width) : Option (FixedInt width)

Return the exact difference when it fits in width signed bits.

@[inline]

def FloatLib.Numerics.Representations.FixedInt.checkedMul {width : ℕ} (left right : FixedInt width) : Option (FixedInt width)

Return the exact product when it fits in width signed bits.

@[inline]

def FloatLib.Numerics.Representations.FixedInt.ofIntSaturating {width : ℕ} (value : ℤ) : FixedInt width

Encode an exact integer, clamping it to the signed range when necessary.

@[inline]

def FloatLib.Numerics.Representations.FixedInt.saturatingAdd {width : ℕ} (left right : FixedInt width) : FixedInt width

Signed addition with saturation at the destination bounds.

@[inline]

def FloatLib.Numerics.Representations.FixedInt.saturatingSub {width : ℕ} (left right : FixedInt width) : FixedInt width

Signed subtraction with saturation at the destination bounds.

@[inline]

def FloatLib.Numerics.Representations.FixedInt.saturatingMul {width : ℕ} (left right : FixedInt width) : FixedInt width

Signed multiplication with saturation at the destination bounds.