Decimal interchange layouts

The named presets have the parameters of IEEE 754-2019, Table 3.6 and §3.5.2. The descriptor also permits custom layouts, without identifying them as standardized formats. Both BID and DPD represent the same datums, with an externally selected encoding. The quantum exponent bounds concern the stored coefficient, including its trailing zeros, rather than a normalized significand.

structure FloatLib.Floats.Formats.DecimalInterchange.Format : Type

A decimal layout with one sign bit, five combination bits, an exponent continuation, and a sequence of ten-bit declets. The positive exponent width separates NaN signaling from payload bits. Bias is unrestricted: the codec does not require quantum zero to be representable. Precision is 3 * declets + 1; this is an interchange descriptor, not a descriptor for every decimal precision. Custom layouts need not be IEEE formats.

• declets : ℕ

  Number of trailing groups of three decimal digits.

• exponentBits : ℕ

  Width of the exponent continuation field in the DPD encoding.

• bias : ℤ

  Bias subtracted from the encoded exponent to obtain the quantum exponent.

• exponentBits_pos : 0 < self.exponentBits

  At least one exponent-continuation bit separates NaN signaling from payload bits.

@[instance_reducible]

instance FloatLib.Floats.Formats.DecimalInterchange.instDecidableEqFormat : DecidableEq Format

def FloatLib.Floats.Formats.DecimalInterchange.instDecidableEqFormat.decEq (x✝ x✝¹ : Format) : Decidable (x✝ = x✝¹)

@[instance_reducible]

instance FloatLib.Floats.Formats.DecimalInterchange.instReprFormat : Repr Format

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

def FloatLib.Floats.Formats.DecimalInterchange.Format.decimal32 : Format

IEEE 754 decimal32 interchange parameters.

def FloatLib.Floats.Formats.DecimalInterchange.Format.decimal64 : Format

IEEE 754 decimal64 basic-format parameters.

def FloatLib.Floats.Formats.DecimalInterchange.Format.decimal128 : Format

IEEE 754 decimal128 basic-format parameters.

def FloatLib.Floats.Formats.DecimalInterchange.Format.bitWidth (f : Format) : ℕ

Total number of stored bits, including the sign and combination fields.

def FloatLib.Floats.Formats.DecimalInterchange.Format.precision (f : Format) : ℕ

Significand precision in decimal digits.

def FloatLib.Floats.Formats.DecimalInterchange.Format.trailingBase (f : Format) : ℕ

Radix of the trailing significand field.

def FloatLib.Floats.Formats.DecimalInterchange.Format.exponentBase (f : Format) : ℕ

Radix of the exponent continuation field.

def FloatLib.Floats.Formats.DecimalInterchange.Format.payloadBound (f : Format) : ℕ

Exclusive bound on a NaN payload or the trailing decimal digits.

def FloatLib.Floats.Formats.DecimalInterchange.Format.coefficientBound (f : Format) : ℕ

Exclusive bound on a finite coefficient, equal to 10 ^ precision.

def FloatLib.Floats.Formats.DecimalInterchange.Format.exponentBound (f : Format) : ℕ

Exclusive bound on the biased exponent. The fourth high-bit pair is reserved.

def FloatLib.Floats.Formats.DecimalInterchange.Format.signBase (f : Format) : ℕ

Place value of the sign bit.

def FloatLib.Floats.Formats.DecimalInterchange.Format.minQuantum (f : Format) : ℤ

Smallest quantum exponent, including subnormal datums.

def FloatLib.Floats.Formats.DecimalInterchange.Format.maxQuantum (f : Format) : ℤ

Largest quantum exponent for a stored coefficient.

class FloatLib.Floats.Formats.DecimalInterchange.Format.HasQuantumZero (f : Format) : Prop

An optional arithmetic assumption: quantum zero belongs to the representable interval. The codecs and general rounding operations do not require it.

• bias_nonneg : 0 ≤ f.bias

  Quantum zero is not below the smallest representable quantum.

• bias_lt : f.bias < ↑f.exponentBound

  Quantum zero is not above the largest representable quantum.

instance FloatLib.Floats.Formats.DecimalInterchange.Format.instHasQuantumZeroDecimal32 : decimal32.HasQuantumZero

instance FloatLib.Floats.Formats.DecimalInterchange.Format.instHasQuantumZeroDecimal64 : decimal64.HasQuantumZero

instance FloatLib.Floats.Formats.DecimalInterchange.Format.instHasQuantumZeroDecimal128 : decimal128.HasQuantumZero

theorem FloatLib.Floats.Formats.DecimalInterchange.Format.coefficientBound_eq (f : Format) : f.coefficientBound = 10 ^ f.precision

theorem FloatLib.Floats.Formats.DecimalInterchange.Format.twice_signBase (f : Format) : 2 * f.signBase = 2 ^ f.bitWidth

theorem FloatLib.Floats.Formats.DecimalInterchange.Format.trailingBase_pos (f : Format) : 0 < f.trailingBase

theorem FloatLib.Floats.Formats.DecimalInterchange.Format.exponentBase_pos (f : Format) : 0 < f.exponentBase

theorem FloatLib.Floats.Formats.DecimalInterchange.Format.payloadBound_pos (f : Format) : 0 < f.payloadBound

theorem FloatLib.Floats.Formats.DecimalInterchange.Format.payloadBound_le (f : Format) : f.payloadBound ≤ f.trailingBase

theorem FloatLib.Floats.Formats.DecimalInterchange.Format.precision_pos (f : Format) : 0 < f.precision

theorem FloatLib.Floats.Formats.DecimalInterchange.Format.coefficientBound_pos (f : Format) : 0 < f.coefficientBound

theorem FloatLib.Floats.Formats.DecimalInterchange.Format.exponentBound_pos (f : Format) : 0 < f.exponentBound

theorem FloatLib.Floats.Formats.DecimalInterchange.Format.signBase_pos (f : Format) : 0 < f.signBase

theorem FloatLib.Floats.Formats.DecimalInterchange.Format.minQuantum_nonpos (f : Format) [f.HasQuantumZero] : f.minQuantum ≤ 0

theorem FloatLib.Floats.Formats.DecimalInterchange.Format.maxQuantum_nonneg (f : Format) [f.HasQuantumZero] : 0 ≤ f.maxQuantum

theorem FloatLib.Floats.Formats.DecimalInterchange.Format.minQuantum_le_maxQuantum (f : Format) : f.minQuantum ≤ f.maxQuantum

theorem FloatLib.Floats.Formats.DecimalInterchange.Format.hasQuantumZero_iff (f : Format) : f.HasQuantumZero ↔ f.minQuantum ≤ 0 ∧ 0 ≤ f.maxQuantum

The optional bias bounds say exactly that quantum zero is representable.

theorem FloatLib.Floats.Formats.DecimalInterchange.Format.exponentBase_eq_two_mul (f : Format) : f.exponentBase = 2 * 2 ^ (f.exponentBits - 1)

The signaling-bit place value is a whole number of trailing significand fields.