Bounded fixed-point conversion proofs

The fixed-integer codec theorems connect each conversion policy to its signed coefficient: rejecting conversion preserves an in-range coefficient, wrapping takes centered reduction, and saturation clamps to the signed range. These relations retain the complete outcome and status.

theorem FloatLib.Floats.ExecFloat.BoundedFixedPoint.Conversion.coefficient_ofRat_wrap {radix : Numerics.Radix} {fractionalDigits width : ℕ} (exact : ℚ) : coefficient (ofRat exact OverflowPolicy.wrap) = (Numerics.roundRatEven (exact * ↑(Formats.FixedPoint.scale radix fractionalDigits))).bmod (2 ^ width)

Wrapping delivers the centered remainder of the nearest-even coefficient.

theorem FloatLib.Floats.ExecFloat.BoundedFixedPoint.Conversion.coefficient_ofCoefficient_of_inRange {radix : Numerics.Radix} {fractionalDigits width : ℕ} (stored : ℤ) (h : Numerics.Representations.FixedInt.InRange width stored) : (ofCoefficient stored).coefficient = stored

An in-range coefficient is preserved, including the sole zero-width coefficient.

theorem FloatLib.Floats.ExecFloat.BoundedFixedPoint.Conversion.coefficient_ofRat_saturate {radix : Numerics.Radix} {fractionalDigits width : ℕ} (exact : ℚ) : coefficient (ofRat exact OverflowPolicy.saturate) = Numerics.Representations.FixedInt.clamp width (Numerics.roundRatEven (exact * ↑(Formats.FixedPoint.scale radix fractionalDigits)))

Saturating conversion delivers the clamped nearest-even coefficient at every width.

@[simp]

theorem FloatLib.Floats.ExecFloat.BoundedFixedPoint.Conversion.run_finite {radix : Numerics.Radix} {fractionalDigits width : ℕ} (policy : OverflowPolicy) (exact : ℚ) : run policy (Numerics.NumericalValue.finite exact) = quantizeFinite policy exact

Finite observations are handled by the selected bounded-overflow policy.

@[simp]

theorem FloatLib.Floats.ExecFloat.BoundedFixedPoint.Conversion.run_infinity {radix : Numerics.Radix} {fractionalDigits width : ℕ} (policy : OverflowPolicy) (negative : Bool) : run policy (Numerics.NumericalValue.infinity negative) = ConversionOutcome.failure (ConversionFailure.infinity InputPosition.source negative)

Bounded fixed point has no infinity code.

@[simp]

theorem FloatLib.Floats.ExecFloat.BoundedFixedPoint.Conversion.run_exceptional {radix : Numerics.Radix} {fractionalDigits width : ℕ} (policy : OverflowPolicy) (exceptional : Numerics.ExceptionalValue) : run policy (Numerics.NumericalValue.exceptional exceptional) = ConversionOutcome.failure (ConversionFailure.exceptional InputPosition.source exceptional)

Bounded fixed point has no exceptional code.

theorem FloatLib.Floats.ExecFloat.BoundedFixedPoint.Conversion.implements_run {radix : Numerics.Radix} {fractionalDigits width : ℕ} : spec.Implements run

run meets spec: its outcomes satisfy the coefficient, range, and status clauses.

theorem FloatLib.Floats.ExecFloat.BoundedFixedPoint.Conversion.spec_deterministic {radix : Numerics.Radix} {fractionalDigits width : ℕ} : spec.Deterministic

For each policy and input, spec admits at most one outcome.

theorem FloatLib.Floats.ExecFloat.BoundedFixedPoint.Conversion.spec_iff_eq_run {radix : Numerics.Radix} {fractionalDigits width : ℕ} (policy : OverflowPolicy) (input : Numerics.NumericalValue ℚ) (outcome : ConversionOutcome (BoundedFixedPoint radix fractionalDigits width)) : spec policy input outcome ↔ outcome = run policy input

An outcome meets spec exactly when it is the outcome of run.

@[simp]

theorem FloatLib.Floats.ExecFloat.BoundedFixedPoint.Conversion.exactDecoder_run {radix : Numerics.Radix} {fractionalDigits width : ℕ} (value : BoundedFixedPoint radix fractionalDigits width) : ExactDecoder.run value = Numerics.NumericalValue.finite value.toRat

The installed decoder exposes the exact stored rational.

theorem FloatLib.Floats.ExecFloat.BoundedFixedPoint.Conversion.run_reject_eq {radix : Numerics.Radix} {fractionalDigits width : ℕ} (exact : ℚ) : run OverflowPolicy.reject (Numerics.NumericalValue.finite exact) = match ofRat exact with | some rounded => ConversionOutcome.success rounded (finiteStatus OverflowPolicy.reject exact rounded) | none => ConversionOutcome.failure ConversionFailure.outOfRange

Rejecting conversion reports outOfRange exactly when the rejecting constructor fails.