DPD coefficient correctness and complete datum round trips

DPD coefficient and exponent packing recovers every valid datum after encoding. Decoding always produces a valid datum, and canonicalization preserves that datum while removing redundant encodings idempotently.

theorem FloatLib.Floats.Formats.DecimalInterchange.DPD.encodeFinite_lt (f : Format) (c e : ℕ) (hc : c < f.coefficientBound) (he : e < f.exponentBound) : encodeFinite f c e < 30 * (f.exponentBase * f.trailingBase)

theorem FloatLib.Floats.Formats.DecimalInterchange.DPD.decodeFinite_valid (f : Format) (n : ℕ) (hn : n < 30 * (f.exponentBase * f.trailingBase)) : (decodeFinite f n).1 < f.coefficientBound ∧ (decodeFinite f n).2 < f.exponentBound

theorem FloatLib.Floats.Formats.DecimalInterchange.DPD.decodeFinite_encodeFinite (f : Format) (c e : ℕ) (hc : c < f.coefficientBound) (he : e < f.exponentBound) : decodeFinite f (encodeFinite f c e) = (c, e)

DPD decoding recovers the coefficient and biased exponent of every finite datum.

theorem FloatLib.Floats.Formats.DecimalInterchange.DPD.lawful : codec.Lawful

The executable DPD fields satisfy the shared codec laws.

theorem FloatLib.Floats.Formats.DecimalInterchange.DPD.decode_encode (f : Format) (d : Datum) (h : Datum.Valid f d) : decode f (codec.encode f d) = d

DPD encoding and decoding preserve the complete datum, including its cohort.

theorem FloatLib.Floats.Formats.DecimalInterchange.DPD.decode_valid (f : Format) (word : BitVec f.bitWidth) : Datum.Valid f (decode f word)

theorem FloatLib.Floats.Formats.DecimalInterchange.DPD.decode_canonicalize (f : Format) (word : BitVec f.bitWidth) : decode f (canonicalize f word) = decode f word

Replacing redundant declets does not alter the represented datum.

theorem FloatLib.Floats.Formats.DecimalInterchange.DPD.canonicalize_idempotent (f : Format) (word : BitVec f.bitWidth) : canonicalize f (canonicalize f word) = canonicalize f word