Decimal codec correctness

The coefficient laws imply a round trip for every representable datum and semantic preservation and idempotence of word canonicalization. Equality here preserves each datum's quantum exponent, signed zero, and NaN metadata, not only the rational value of ordinary numbers.

structure FloatLib.Floats.Formats.DecimalInterchange.Codec.Lawful (codec : Codec) : Prop

The obligations for an actual coefficient encoding. BID and DPD each prove these laws for their executable field manipulations.

• encodeFinite_lt (f : Format) (c e : ℕ) : c < f.coefficientBound → e < f.exponentBound → codec.encodeFinite f c e < 30 * (f.exponentBase * f.trailingBase)
• decodeFinite_valid (f : Format) (n : ℕ) : n < 30 * (f.exponentBase * f.trailingBase) → (codec.decodeFinite f n).1 < f.coefficientBound ∧ (codec.decodeFinite f n).2 < f.exponentBound
• decodeFinite_encodeFinite (f : Format) (c e : ℕ) : c < f.coefficientBound → e < f.exponentBound → codec.decodeFinite f (codec.encodeFinite f c e) = (c, e)
• encodePayload_lt (f : Format) (p : ℕ) : p < f.payloadBound → codec.encodePayload f p < f.trailingBase
• decodePayload_lt (f : Format) (n : ℕ) : n < f.trailingBase → codec.decodePayload f n < f.payloadBound
• decodePayload_encodePayload (f : Format) (p : ℕ) : p < f.payloadBound → codec.decodePayload f (codec.encodePayload f p) = p

theorem FloatLib.Floats.Formats.DecimalInterchange.Codec.decode_valid (codec : Codec) (laws : codec.Lawful) (f : Format) (word : BitVec f.bitWidth) : Datum.Valid f (codec.decode f word)

Every bit pattern decodes to a representable datum, including noncanonical words.

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

Every representable datum survives encoding and decoding exactly.

theorem FloatLib.Floats.Formats.DecimalInterchange.Codec.decode_canonicalize (codec : Codec) (laws : codec.Lawful) (f : Format) (word : BitVec f.bitWidth) : codec.decode f (codec.canonicalize f word) = codec.decode f word

Canonicalization preserves all decoded information, including quantum and NaN payload.

theorem FloatLib.Floats.Formats.DecimalInterchange.Codec.canonicalize_idempotent (codec : Codec) (laws : codec.Lawful) (f : Format) (word : BitVec f.bitWidth) : codec.canonicalize f (codec.canonicalize f word) = codec.canonicalize f word

Applying canonicalization twice has the same result as applying it once.

theorem FloatLib.Floats.Formats.DecimalInterchange.Codec.decode_of_encode?_eq_some (codec : Codec) (laws : codec.Lawful) (f : Format) (d : Datum) (word : BitVec f.bitWidth) (h : codec.encode? f d = some word) : codec.decode f word = d

An accepted checked encoding always decodes to the original datum.