Decimal interchange codecs and proofs

The executable BID and DPD implementations satisfy exact datum round trips for every Format descriptor, including decimal32, decimal64, and decimal128. Every word decodes to a representable datum. Canonicalization and conversion between encodings preserve that datum, including cohort exponent, signed zero, infinity sign, and NaN sign, signaling bit, and payload.

The specifications are IEEE 754-2019 §§3.3, 3.5 and 5.5.2, Tables 3.3–3.4 and 3.6, and Mike Cowlishaw's Densely Packed Decimal Encoding: https://speleotrove.com/decimal/DPDecimal.html. The IEEE standard is identified by DOI 10.1109/IEEESTD.2019.8766229.

These are representation guarantees. Import Arithmetic.Basic for decimal arithmetic and its rounding, preferred-exponent, and exception theorems.

theorem FloatLib.Floats.Formats.DecimalInterchange.Encoding.lawful (encoding : Encoding) : encoding.codec.Lawful

Both supported encodings satisfy the shared laws through their actual field codecs.

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

theorem FloatLib.Floats.Formats.DecimalInterchange.Encoding.decode_of_encode?_eq_some (encoding : Encoding) (f : Format) (datum : Datum) (word : BitVec f.bitWidth) (h : encoding.encode? f datum = some word) : encoding.decode f word = datum

Successful checked encoding retains every component of the input datum.

theorem FloatLib.Floats.Formats.DecimalInterchange.Encoding.encode?_decode (encoding : Encoding) (f : Format) (word : BitVec f.bitWidth) : encoding.encode? f (encoding.decode f word) = some (encoding.canonicalize f word)

Re-encoding any decoded word succeeds and produces its canonical representative.

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

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

@[simp]

theorem FloatLib.Floats.Formats.DecimalInterchange.transcode_self (encoding : Encoding) (f : Format) (word : BitVec f.bitWidth) : transcode encoding encoding f word = word

Re-encoding to the same encoding is a bit-for-bit copy, including noncanonical words.

theorem FloatLib.Floats.Formats.DecimalInterchange.decode_transcode (source target : Encoding) (f : Format) (word : BitVec f.bitWidth) : target.decode f (transcode source target f word) = source.decode f word

Conversion preserves the complete datum, including special values.

theorem FloatLib.Floats.Formats.DecimalInterchange.transcode_transcode (source target : Encoding) (f : Format) (word : BitVec f.bitWidth) : transcode target source f (transcode source target f word) = if source = target then word else source.canonicalize f word

Conversion to the other encoding and back recovers the canonical source word. An originally redundant encoding need not be recovered bit for bit.