Correctness of configured exact fixed-point operations

Wrapping is an equivalence with the complete code, and each arithmetic operation agrees with its exact rational interpretation.

@[simp]

theorem FloatLib.Floats.ExecFloat.FixedPoint.toCode_ofCode {radix : Numerics.Radix} {fractionalDigits : ℕ} (code : Formats.FixedPoint.Code radix fractionalDigits) : (ofCode code).toCode = code

Unwrapping a freshly wrapped exact fixed-point code returns the original code.

@[simp]

theorem FloatLib.Floats.ExecFloat.FixedPoint.ofCode_toCode {radix : Numerics.Radix} {fractionalDigits : ℕ} (value : FixedPoint radix fractionalDigits) : ofCode value.toCode = value

Rewrapping the code of an exact fixed-point value returns the original value.

@[simp]

theorem FloatLib.Floats.ExecFloat.FixedPoint.coefficient_ofCoefficient {radix : Numerics.Radix} {fractionalDigits : ℕ} (stored : ℤ) : (ofCoefficient stored).coefficient = stored

Constructing from a coefficient stores that coefficient exactly.

@[simp]

theorem FloatLib.Floats.ExecFloat.FixedPoint.coefficient_roundRat {radix : Numerics.Radix} {fractionalDigits : ℕ} (value : ℚ) : (roundRat value).coefficient = Numerics.roundRatEven (value * ↑(scale radix fractionalDigits))

roundRat stores the ties-to-even rounded grid coefficient.

@[simp]

theorem FloatLib.Floats.ExecFloat.FixedPoint.toRat_add {radix : Numerics.Radix} {fractionalDigits : ℕ} (left right : FixedPoint radix fractionalDigits) : (left.add right).toRat = left.toRat + right.toRat

Exact same-scale addition agrees with addition of the decoded rationals.

@[simp]

theorem FloatLib.Floats.ExecFloat.FixedPoint.toRat_neg {radix : Numerics.Radix} {fractionalDigits : ℕ} (value : FixedPoint radix fractionalDigits) : value.neg.toRat = -value.toRat

Exact fixed-point negation agrees with negation of the decoded rational.

@[simp]

theorem FloatLib.Floats.ExecFloat.FixedPoint.toRat_sub {radix : Numerics.Radix} {fractionalDigits : ℕ} (left right : FixedPoint radix fractionalDigits) : (left.sub right).toRat = left.toRat - right.toRat

Exact same-scale subtraction agrees with subtraction of the decoded rationals.

@[simp]

theorem FloatLib.Floats.ExecFloat.FixedPoint.toRat_mul {radix : Numerics.Radix} {p q : ℕ} (left : FixedPoint radix p) (right : FixedPoint radix q) : (left.mul right).toRat = left.toRat * right.toRat

Scale-composing multiplication agrees with multiplication of the decoded rationals.