Configured posit decimal preservation

Exact model preservation and the codec inverse law imply decimal round trips for every supported storage carrier and posit width.

@[simp]

theorem FloatLib.Floats.ExecFloat.Posit.parse_display {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] (value : ExecFloat (Formats.Posit.Configured.Family format code plan)) : parse (display value) = Except.ok value

Parsing the exact decimal display preserves the complete configured posit value.

theorem FloatLib.Floats.ExecFloat.Posit.toModel_parse {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] (input : String) : Except.map toModel (parse input) = Formats.Posit.Model.parse format input

A successful decimal input has precisely the model rounder's result after decoding.

@[simp]

theorem FloatLib.Floats.ExecFloat.Posit.parse_toString {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] (value : ExecFloat (Formats.Posit.Configured.Family format code plan)) : parse (toString value) = Except.ok value

Exact decimal parsing inverts the configured ToString display.