Tapered posit field decoding

Posit field decoding recovers the variable-length regime, tapered exponent, fraction, significand, and binary scale from a model word. The resulting DecodedFields structure is the common proof-facing boundary for exact semantics and optimized arithmetic.

@[inline]

def FloatLib.Floats.Formats.Posit.Model.countLeadingRun (value width : ℕ) : Bool → ℕ

Count a leading run in exactly width low bits of value, starting at bit width - 1.

theorem FloatLib.Floats.Formats.Posit.Model.countLeadingRun_le (value width : ℕ) (bit : Bool) : countLeadingRun value width bit ≤ width

A leading run cannot consume more bits than the width being inspected.

theorem FloatLib.Floats.Formats.Posit.Model.countLeadingRun_self_pos (value width : ℕ) (hwidth : 0 < width) : 0 < countLeadingRun value width (value.testBit (width - 1))

Inspecting a nonempty word from its actual first bit finds a nonempty run.

@[inline]

def FloatLib.Floats.Formats.Posit.Model.regimeBit {format : Format} (value : Model format) : Bool

First regime bit in the magnitude payload.

@[inline]

def FloatLib.Floats.Formats.Posit.Model.regimeRunLength {format : Format} (value : Model format) : ℕ

Number of equal leading regime bits.

theorem FloatLib.Floats.Formats.Posit.Model.regimeRunLength_le_payload {format : Format} (value : Model format) : value.regimeRunLength ≤ format.payloadBits

The tapered regime consumes at most the complete payload.

theorem FloatLib.Floats.Formats.Posit.Model.regimeRunLength_pos {format : Format} (value : Model format) : 0 < value.regimeRunLength

Every posit word has a nonempty leading regime run.

@[inline]

def FloatLib.Floats.Formats.Posit.Model.hasRegimeTerminator {format : Format} (value : Model format) : Bool

Whether an opposite regime-terminator bit is present.

@[inline]

def FloatLib.Floats.Formats.Posit.Model.trailingBits {format : Format} (value : Model format) : ℕ

Bits available after the regime and its optional terminator.

theorem FloatLib.Floats.Formats.Posit.Model.regimeRunLength_add_trailingBits_le_payload {format : Format} (value : Model format) : value.regimeRunLength + value.trailingBits ≤ format.payloadBits

Regime and trailing fields together fit inside the payload.

@[inline]

def FloatLib.Floats.Formats.Posit.Model.usedExponentBits {format : Format} (value : Model format) : ℕ

Number of exponent bits actually present in this tapered encoding.

@[inline]

def FloatLib.Floats.Formats.Posit.Model.fractionBits {format : Format} (value : Model format) : ℕ

Number of explicit fraction bits present in this tapered encoding.

theorem FloatLib.Floats.Formats.Posit.Model.fractionBits_le_trailingBits {format : Format} (value : Model format) : value.fractionBits ≤ value.trailingBits

The explicit fraction is a subfield of the trailing payload.

theorem FloatLib.Floats.Formats.Posit.Model.regimeRunLength_add_fractionBits_le_payload {format : Format} (value : Model format) : value.regimeRunLength + value.fractionBits ≤ format.payloadBits

Regime and explicit fraction together never exceed the payload.

@[inline]

def FloatLib.Floats.Formats.Posit.Model.fractionField {format : Format} (value : Model format) : ℕ

Low explicit fraction field.

@[inline]

def FloatLib.Floats.Formats.Posit.Model.storedExponentField {format : Format} (value : Model format) : ℕ

Exponent bits physically present between the regime and fraction.

@[inline]

def FloatLib.Floats.Formats.Posit.Model.exponentField {format : Format} (value : Model format) : ℕ

Full exponent value after restoring unavailable low bits as zeros.

Exponent bits are consumed most-significant first. Tapering therefore removes low exponent bits, which is represented by this left shift.

theorem FloatLib.Floats.Formats.Posit.Model.usedExponentBits_le_exponentBits {format : Format} (value : Model format) : value.usedExponentBits ≤ format.exponentBits

At most the descriptor's two standard exponent bits are physically present.

theorem FloatLib.Floats.Formats.Posit.Model.exponentField_lt_four {format : Format} (value : Model format) : value.exponentField < 4

The restored standard exponent field is always below four.

@[inline]

def FloatLib.Floats.Formats.Posit.Model.regimeValue {format : Format} (value : Model format) : ℤ

Signed regime value k.

@[inline]

def FloatLib.Floats.Formats.Posit.Model.scale {format : Format} (value : Model format) : ℤ

Exact binary scale after accounting for the explicit fraction denominator.

theorem FloatLib.Floats.Formats.Posit.Model.neg_four_payloadBits_le_scale {format : Format} (value : Model format) : -(4 * Int.ofNat format.payloadBits) ≤ value.scale

Every decoded posit scale is no smaller than -4 times its payload width.

theorem FloatLib.Floats.Formats.Posit.Model.scale_lt_four_bits {format : Format} (value : Model format) : value.scale < 4 * Int.ofNat format.bits

Every decoded posit scale is strictly below four times its total encoded width.

theorem FloatLib.Floats.Formats.Posit.Model.zero_or_nar_or_scale_eq_zero_of_bits_eq_two {format : Format} (value : Model format) (hbits : format.bits = 2) : value = zero format ∨ value = nar format ∨ value.scale = 0

At the minimum standard width, every word is zero, NaR, or one of the two encodings of unit magnitude. The latter therefore has dyadic scale zero.

This boundary case complements the uniform payload bound used in quire proofs for widths of at least three.

structure FloatLib.Floats.Formats.Posit.Model.DecodedFields (format : Format) : Type

Complete decoded fields of a nonzero finite posit.

• negative : Bool

  Sign of the represented finite value.

• regimeBit : Bool

  First bit of the variable-length regime.

• regimeRunLength : ℕ

  Number of repeated regime bits.

• regimeValue : ℤ

  Signed regime value.

• usedExponentBits : ℕ

  Number of exponent bits physically present.

• exponentField : ℕ

  Exponent after omitted low bits are restored as zero.

• fractionBits : ℕ

  Number of explicit fraction bits.

• fractionField : ℕ

  Explicit fraction field.

• significand : ℕ

  Positive integer significand, including its implicit leading bit.

• scale : ℤ

  Binary exponent applied to significand.

def FloatLib.Floats.Formats.Posit.Model.instDecidableEqDecodedFields.decEq {format✝ : Format} (x✝ x✝¹ : DecodedFields format✝) : Decidable (x✝ = x✝¹)

@[instance_reducible]

instance FloatLib.Floats.Formats.Posit.Model.instDecidableEqDecodedFields {format✝ : Format} : DecidableEq (DecodedFields format✝)

def FloatLib.Floats.Formats.Posit.Model.instReprDecodedFields.repr {format✝ : Format} : DecodedFields format✝ → ℕ → Std.Format

@[instance_reducible]

instance FloatLib.Floats.Formats.Posit.Model.instReprDecodedFields {format✝ : Format} : Repr (DecodedFields format✝)

@[inline]

def FloatLib.Floats.Formats.Posit.Model.decodeFields {format : Format} (value : Model format) : DecodedFields format

Decode all fields of a nonzero finite posit word.

theorem FloatLib.Floats.Formats.Posit.Model.decodeFields_significand_lt_modulus {format : Format} (value : Model format) : value.decodeFields.significand < format.modulus

A decoded posit significand fits within the complete posit word's width.

theorem FloatLib.Floats.Formats.Posit.Model.decodeFields_significand_lt_two_pow_payloadBits {format : Format} (value : Model format) : value.decodeFields.significand < 2 ^ format.payloadBits

A decoded posit significand fits in the format payload.

The regime always consumes at least one payload bit, so the implicit leading significand bit together with every explicit fraction bit occupies at most payloadBits positions.

@[inline]

def FloatLib.Floats.Formats.Posit.Model.DecodedFields.signedSignificand {format : Format} (fields : DecodedFields format) : ℤ

Signed integer significand before applying the binary scale.

@[inline]

def FloatLib.Floats.Formats.Posit.Model.DecodedFields.toDyadic {format : Format} (fields : DecodedFields format) : Numerics.Dyadic

Format-independent exact dyadic value represented by these decoded fields.

Integer kernels use this value after the posit decoder recovers the tapered fields. Other radix-two families use the same exact-number representation.

@[inline]

def FloatLib.Floats.Formats.Posit.Model.DecodedFields.toRat {format : Format} (fields : DecodedFields format) : ℚ

Exact dyadic rational represented by these decoded fields.

@[simp]

theorem FloatLib.Floats.Formats.Posit.Model.DecodedFields.toDyadic_fields {format : Format} (fields : DecodedFields format) : fields.toDyadic = { negative := fields.negative, significand := fields.significand, exponent := fields.scale }

Expanding toDyadic exposes the decoded sign, significand, and binary scale unchanged.