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.

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.