Value-preserving Posit decimal conversion

The decimal string denotes exactly the decoded dyadic rational. Rounding that rational recovers the original posit word. This proves the decimal preservation guarantee of Posit Standard (2022), §6.3 for every descriptor width.

Exponent clamping

theorem FloatLib.Floats.Formats.Posit.Model.roundPositiveCode_of_lt_minPositive {format : Format} (target : ℚ) (hpos : 0 < target) (hlt : target < minPositiveRat format) : roundPositiveCode format target = 1

Every positive rational below minPos rounds to the code of minPos.

theorem FloatLib.Floats.Formats.Posit.Model.roundPositiveCode_of_maxPositive_le {format : Format} (target : ℚ) (hle : nonnegativeRatAt format (format.signMaskNat - 1) ≤ target) : roundPositiveCode format target = format.signMaskNat - 1

Every rational at or above maxPos rounds to the code of maxPos.

theorem FloatLib.Floats.Formats.Posit.Model.maxPositive_le_of_saturationExponent_le {format : Format} (s : ℕ) (e : ℤ) (hs : s ≠ 0) (he : decimalSaturationExponent format ≤ e) : nonnegativeRatAt format (format.signMaskNat - 1) ≤ ↑s * 10 ^ e

A nonzero significand scaled at or past the saturation exponent reaches maxPos.

theorem FloatLib.Floats.Formats.Posit.Model.lt_minPositive_of_le_vanishingExponent {format : Format} (s : ℕ) (e : ℤ) (he : e ≤ decimalVanishingExponent format s) : ↑s * 10 ^ e < minPositiveRat format

A significand scaled at or below its vanishing exponent lies strictly below minPos.

theorem FloatLib.Floats.Formats.Posit.Model.roundRat_clampDecimal {format : Format} (d : Numerics.DecimalText.Decimal) : roundRat format (clampDecimal format d).toRat = roundRat format d.toRat

Clamping the decimal exponent never changes the rounded posit.

theorem FloatLib.Floats.Formats.Posit.Model.parse_eq_roundRat {format : Format} (input : String) (value : ℚ) (hinput : Numerics.DecimalText.parse input = some value) : parse format input = Except.ok (roundRat format value)

Decimal parsing uses the standard exact-rational rounder once.

theorem FloatLib.Floats.Formats.Posit.Model.decimalParse_display {format : Format} (value : Model format) (exact : Numerics.Dyadic) (hexact : value.toDyadic? = some exact) : Numerics.DecimalText.parse value.display = some exact.toRat

An ordinary finite word's decimal display has exactly its decoded rational value.

@[simp]

theorem FloatLib.Floats.Formats.Posit.Model.parse_display {format : Format} (value : Model format) : parse format value.display = Except.ok value

Decimal display and parsing preserve every posit word, including zero and NaR.

@[simp]

theorem FloatLib.Floats.Formats.Posit.Model.parse_toString {format : Format} (value : Model format) : parse format (toString value) = Except.ok value

Exact decimal parsing inverts ToString.