Decimal interchange public runtime

Choose a Format, such as decimal32, decimal64, or decimal128, and explicitly select BID or DPD: a word does not identify its own encoding. Encoding.encode? preserves the exact datum or rejects it; Encoding.decode accepts every word.

transcode implements the same-width encoding conversion of IEEE 754-2019 §5.5.2, preserving the sign, quantum exponent, and NaN metadata. Conversion between different encodings canonicalizes redundant words; conversion to the same encoding copies the word. Neither performs arithmetic or rounding.

Import DecimalInterchange.Basic for the codec and cohort proofs. Arithmetic.Operations provides executable decimal arithmetic, preferred-exponent selection, rounding modes, and exception flags.

inductive FloatLib.Floats.Formats.DecimalInterchange.Encoding : Type

The two alternative decimal encodings specified by IEEE 754-2019 §3.5.2.

• bid : Encoding
• dpd : Encoding

@[instance_reducible]

instance FloatLib.Floats.Formats.DecimalInterchange.instDecidableEqEncoding : DecidableEq Encoding

@[instance_reducible]

instance FloatLib.Floats.Formats.DecimalInterchange.instReprEncoding : Repr Encoding

def FloatLib.Floats.Formats.DecimalInterchange.instReprEncoding.repr : Encoding → ℕ → Std.Format

def FloatLib.Floats.Formats.DecimalInterchange.Encoding.codec : Encoding → Codec

Coefficient codec selected externally to the interchange word.

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

Decode any word, including its sign, quantum exponent, and special-value metadata.

def FloatLib.Floats.Formats.DecimalInterchange.Encoding.encode? (encoding : Encoding) (f : Format) (datum : Datum) : Option (BitVec f.bitWidth)

Encode the complete datum exactly, or reject it if it is invalid for the chosen format.

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

Canonical representative of the datum denoted by a word.

def FloatLib.Floats.Formats.DecimalInterchange.transcode (source target : Encoding) (f : Format) (word : BitVec f.bitWidth) : BitVec f.bitWidth

Convert between BID and DPD at the same width, preserving the complete datum. Equal source and target encodings copy the word, following IEEE 754-2019 §5.5.2.