P3109 representation proofs

A validated P3109 descriptor defines an exact-width NumericalSystem and ExecFloat carrier. These theorems connect their denotations to P3109 decoding. Descriptor validation supplies the field-width, special-encoding, and storage conditions used by the proofs.

theorem FloatLib.Floats.Formats.P3109.Format.trailingBits_add_one (format : Format) : format.trailingBits + 1 = format.precision

The stored trailing field and implicit leading bit make up the declared precision.

theorem FloatLib.Floats.Formats.P3109.Format.trailingBits_int (format : Format) : Int.ofNat format.trailingBits = Int.ofNat format.precision - 1

Integer form of trailingBits_add_one, used in exponent arithmetic.

theorem FloatLib.Floats.Formats.P3109.Format.bitWidth_pos (format : Format) : 0 < format.bitWidth

Every P3109 descriptor has a positive encoded width.

theorem FloatLib.Floats.Formats.P3109.Format.precision_lt_bitWidth_of_signed (format : Format) (signed : format.signedness = Signedness.signed) : format.precision < format.bitWidth

A signed descriptor carries the strict P < K requirement from P3109.

theorem FloatLib.Floats.Formats.P3109.Format.precision_le_bitWidth_of_unsigned (format : Format) (unsigned : format.signedness = Signedness.unsigned) : format.precision ≤ format.bitWidth

An unsigned descriptor carries the P ≤ K requirement from P3109.

theorem FloatLib.Floats.Formats.P3109.Format.exponentBits_pos (format : Format) : 0 < format.exponentBits

The P3109 exponent field is nonempty for every valid descriptor.

theorem FloatLib.Floats.Formats.P3109.Format.exponentBias_signed (format : Format) (signed : format.signedness = Signedness.signed) : format.exponentBias = 2 ^ (format.bitWidth - format.precision - 1)

Signed formats have the P3109 bias 2^(K-P-1).

theorem FloatLib.Floats.Formats.P3109.Format.exponentBias_unsigned (format : Format) (unsigned : format.signedness = Signedness.unsigned) : format.exponentBias = 2 ^ (format.bitWidth - format.precision)

Unsigned formats have the P3109 bias 2^(K-P).

theorem FloatLib.Floats.Formats.P3109.Format.signBoundary_lt_modulus (format : Format) : format.signBoundary < format.modulus

The signed/unsigned boundary lies strictly inside the K-bit code space.

theorem FloatLib.Floats.Formats.P3109.Format.modulus_eq_two_mul_signBoundary (format : Format) : format.modulus = 2 * format.signBoundary

The complete code-space size is twice the signed/unsigned boundary.

theorem FloatLib.Floats.Formats.P3109.Format.signBoundary_pos (format : Format) : 0 < format.signBoundary

The boundary of the signed half of the code space is nonzero.

theorem FloatLib.Floats.Formats.P3109.Format.one_lt_signBoundary (format : Format) : 1 < format.signBoundary

At least two positive finite code points lie below the signed boundary.

theorem FloatLib.Floats.Formats.P3109.Format.two_lt_modulus (format : Format) : 2 < format.modulus

Every valid P3109 format has more than two code points.

theorem FloatLib.Floats.Formats.P3109.Format.nanBits_pos (format : Format) : 0 < format.nanBits

The single P3109 NaN code is never the all-zero code.

theorem FloatLib.Floats.Formats.P3109.Format.positiveInfinityBits_pos (format : Format) : 0 < format.positiveInfinityBits

positiveInfinityBits is nonzero for every descriptor.

theorem FloatLib.Floats.Formats.P3109.Format.negativeInfinityBits_pos (format : Format) : 0 < format.negativeInfinityBits

negativeInfinityBits is nonzero for every descriptor.

theorem FloatLib.Floats.Formats.P3109.Format.nanBits_lt_modulus (format : Format) : format.nanBits < format.modulus

The sole P3109 NaN code fits in the declared code space.

theorem FloatLib.Floats.Formats.P3109.Format.positiveInfinityBits_lt_modulus (format : Format) : format.positiveInfinityBits < format.modulus

positiveInfinityBits fits in the declared code space for every descriptor.

theorem FloatLib.Floats.Formats.P3109.Format.negativeInfinityBits_lt_modulus (format : Format) : format.negativeInfinityBits < format.modulus

negativeInfinityBits fits in the declared code space for every descriptor.

theorem FloatLib.Floats.Formats.P3109.Format.positiveInfinityBits_ne_signBoundary_of_signed (format : Format) (signed : format.signedness = Signedness.signed) : format.positiveInfinityBits ≠ format.signBoundary

In a signed descriptor, positive infinity is distinct from the midpoint NaN code.

theorem FloatLib.Floats.Formats.P3109.Format.negativeInfinityBits_ne_signBoundary_of_signed (format : Format) (_signed : format.signedness = Signedness.signed) : format.negativeInfinityBits ≠ format.signBoundary

In a signed descriptor, negative infinity is distinct from the midpoint NaN code.

theorem FloatLib.Floats.Formats.P3109.Format.negativeInfinityBits_ne_positiveInfinityBits_of_signed (format : Format) (signed : format.signedness = Signedness.signed) : format.negativeInfinityBits ≠ format.positiveInfinityBits

The two infinity codes are distinct in every signed descriptor.

theorem FloatLib.Floats.Formats.P3109.Format.positiveInfinityBits_ne_nanBits_of_unsigned (format : Format) (unsigned : format.signedness = Signedness.unsigned) : format.positiveInfinityBits ≠ format.nanBits

In an unsigned descriptor, positive infinity is distinct from the terminal NaN code.

@[simp]

theorem FloatLib.Floats.Formats.P3109.Format.numericalSystem_denote (format : Format) (code : BitVec format.bitWidth) : format.numericalSystem.denote code = format.decode code

The generic numerical-system wrapper denotes exactly the P3109 decode function.

@[simp]

theorem FloatLib.Floats.Formats.P3109.Format.decodePositiveFinite_zero (format : Format) : format.decodePositiveFinite 0 = Numerics.Dyadic.zero

The all-zero positive finite code decodes to the unique P3109 zero.

theorem FloatLib.Floats.Formats.P3109.Format.decodePositiveFinite_of_biasedExponent_eq_zero (format : Format) (bits : ℕ) (bits_ne_zero : bits ≠ 0) (biasedExponent_eq_zero : bits / 2 ^ format.trailingBits = 0) : format.decodePositiveFinite bits = { negative := false, significand := bits % 2 ^ format.trailingBits, exponent := format.minimumQuantumExponent }

A nonzero code in biased-exponent row zero follows the P3109 subnormal formula.

theorem FloatLib.Floats.Formats.P3109.Format.decodePositiveFinite_of_biasedExponent_ne_zero (format : Format) (bits : ℕ) (bits_ne_zero : bits ≠ 0) (biasedExponent_ne_zero : bits / 2 ^ format.trailingBits ≠ 0) : format.decodePositiveFinite bits = { negative := false, significand := 2 ^ format.trailingBits + bits % 2 ^ format.trailingBits, exponent := Int.ofNat (bits / 2 ^ format.trailingBits) - Int.ofNat format.exponentBias + 1 - Int.ofNat format.precision }

A positive code outside biased-exponent row zero follows the P3109 normal formula.

@[simp]

theorem FloatLib.Floats.Formats.P3109.Format.decodePositiveFinite_significand_eq_zero_iff (format : Format) (bits : ℕ) : (format.decodePositiveFinite bits).significand = 0 ↔ bits = 0

Positive finite decoding has zero significand exactly at the all-zero code.

@[simp]

theorem FloatLib.Floats.Formats.P3109.Format.decodePositiveFinite_negative (format : Format) (bits : ℕ) : (format.decodePositiveFinite bits).negative = false

Positive finite decoding never introduces a negative sign.

theorem FloatLib.Floats.Formats.P3109.Format.minimumQuantumExponent_eq (format : Format) : format.minimumQuantumExponent = format.minimumNormalExponent - Int.ofNat format.trailingBits

The minimum quantum sits P - 1 binary places below the minimum normal exponent.

theorem FloatLib.Floats.Formats.P3109.Format.decodePositiveFinite_toRat_of_lt (format : Format) (bits : ℕ) (hbits : bits < 2 ^ format.trailingBits) : (format.decodePositiveFinite bits).toRat = ↑bits * 2 ^ format.minimumQuantumExponent

A code in biased-exponent row zero denotes that many minimum quanta.

theorem FloatLib.Floats.Formats.P3109.Format.decodePositiveFinite_toRat_add_mul (format : Format) (trailing biasedExponent : ℕ) (htrailing : trailing < 2 ^ format.trailingBits) (hbiased : biasedExponent ≠ 0) : (format.decodePositiveFinite (trailing + biasedExponent * 2 ^ format.trailingBits)).toRat = ↑(2 ^ format.trailingBits + trailing) * 2 ^ (↑biasedExponent - ↑format.exponentBias + 1 - ↑format.precision)

Rational value of a code written as trailing field plus a nonzero biased-exponent row.

@[simp]

theorem FloatLib.Floats.Formats.P3109.Format.decode_zero (format : Format) : format.decode 0#format.bitWidth = Numerics.NumericalValue.finite Numerics.Dyadic.zero

The all-zero code denotes P3109's unique zero.

@[simp]

theorem FloatLib.Floats.Formats.P3109.Format.decode_nanBits (format : Format) : format.decode (BitVec.ofNat format.bitWidth format.nanBits) = Numerics.NumericalValue.exceptional Numerics.ExceptionalValue.nan

Every signed or unsigned P3109 format decodes the P3109-specified NaN code as NaN.

theorem FloatLib.Floats.Formats.P3109.Format.decode_positiveInfinityBits (format : Format) (extended : format.domain = Domain.extended) : format.decode (BitVec.ofNat format.bitWidth format.positiveInfinityBits) = Numerics.NumericalValue.infinity false

Extended P3109 formats decode the P3109-specified positive-infinity code.

theorem FloatLib.Floats.Formats.P3109.Format.decode_negativeInfinityBits (format : Format) (signed : format.signedness = Signedness.signed) (extended : format.domain = Domain.extended) : format.decode (BitVec.ofNat format.bitWidth format.negativeInfinityBits) = Numerics.NumericalValue.infinity true

Signed extended P3109 formats decode the P3109-specified negative-infinity code.

theorem FloatLib.Floats.ExecFloat.P3109.decode_zero {format : Formats.P3109.Format} : zero.decode = Numerics.NumericalValue.finite Numerics.Dyadic.zero

The user-facing zero constructor denotes P3109's unique finite zero.

theorem FloatLib.Floats.ExecFloat.P3109.decode_nan {format : Formats.P3109.Format} : nan.decode = Numerics.NumericalValue.exceptional Numerics.ExceptionalValue.nan

The user-facing NaN constructor denotes the format's sole exceptional NaN value.

theorem FloatLib.Floats.ExecFloat.P3109.decode_positiveInfinity {format : Formats.P3109.Format} (extended : format.domain = Formats.P3109.Domain.extended) : (positiveInfinity extended).decode = Numerics.NumericalValue.infinity false

The positive-infinity constructor has its advertised meaning in every extended format.

theorem FloatLib.Floats.ExecFloat.P3109.decode_negativeInfinity {format : Formats.P3109.Format} (signed : format.signedness = Formats.P3109.Signedness.signed) (extended : format.domain = Formats.P3109.Domain.extended) : (negativeInfinity signed extended).decode = Numerics.NumericalValue.infinity true

The negative-infinity constructor has its advertised meaning in signed extended formats.

@[simp]

theorem FloatLib.Floats.ExecFloat.P3109.toNatBits_ofNatBits {format : Formats.P3109.Format} (bits : ℕ) : (ofNatBits bits).toNatBits = bits % 2 ^ format.bitWidth

Natural-number construction reduces modulo 2^K, where K is the encoded width.

@[simp]

theorem FloatLib.Floats.ExecFloat.P3109.decode_eq_format_decode {format : Formats.P3109.Format} (value : P3109 format) : value.decode = format.decode (Codebook.toCode value)

Executable P3109 decoding is definitionally the descriptor's exact decoding function.

theorem FloatLib.Floats.ExecFloat.P3109.exists_decode_finite_of_ofFiniteFields?_eq_some {format : Formats.P3109.Format} (negative : Bool) (biasedExponent trailing : ℕ) (value : P3109 format) (success : ofFiniteFields? negative biasedExponent trailing = some value) : ∃ (exact : Numerics.Dyadic), value.decode = Numerics.NumericalValue.finite exact

A successful structured-field construction is guaranteed to denote an ordinary finite value.

This theorem is the elimination rule for ofFiniteFields?: callers need not reason about the descriptor's reserved code points after the constructor succeeds.