Exact posit decoding

Every posit word is classified, and ordinary values decode into the shared exact dyadic carrier. The one-pass compiled decoder is proved equal to the transparent field-based definition.

@[noinline]

def FloatLib.Floats.Formats.Posit.Model.decodeFiniteDyadicCode (format : Format) (negative : Bool) (code : ℕ) : Numerics.Dyadic

Decode a nonzero finite posit code into the shared dyadic execution carrier.

The sign and the encoded word are separate arguments, so callers that already classified the word can reuse the extraction. decodeFiniteDyadic below is the model-facing entry point.

@[inline]

def FloatLib.Floats.Formats.Posit.Model.decodeFiniteDyadic {format : Format} (value : Model format) : Numerics.Dyadic

Decode a nonzero finite posit into the shared dyadic execution carrier.

This decoder computes sign restoration, regime scanning, and trailing-field powers once. decodeFields exposes the same quantities as independent projections for proofs, and the theorem below proves the two agree.

theorem FloatLib.Floats.Formats.Posit.Model.decodeFiniteDyadic_eq_decodeFields_toDyadic {format : Format} (value : Model format) : value.decodeFiniteDyadic = value.decodeFields.toDyadic

The one-pass execution decoder agrees with the field decoder used in proofs.

inductive FloatLib.Floats.Formats.Posit.Model.ExactValue (format : Format) : Type

Complete exact interpretation of a posit word.

• zero {format : Format} : ExactValue format

  The unique zero word.

• finite {format : Format} (fields : DecodedFields format) : ExactValue format

  A nonzero finite dyadic rational together with its tapered fields.

• nar {format : Format} : ExactValue format

  The unique Not-a-Real word.

@[instance_reducible]

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

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

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

@[instance_reducible]

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

@[inline]

def FloatLib.Floats.Formats.Posit.Model.decodeExact {format : Format} (value : Model format) : ExactValue format

Decode every posit word, retaining its exact tapered fields.

theorem FloatLib.Floats.Formats.Posit.Model.decodeExact_eq_finite_iff {format : Format} (value : Model format) (fields : DecodedFields format) : value.decodeExact = ExactValue.finite fields ↔ value.isNaR = false ∧ value.isZero = false ∧ value.decodeFields = fields

Characterize the nonzero finite branch of exact posit decoding.

@[inline, implemented_by _private.FloatLib.Floats.Formats.Posit.Model.Decode.0.FloatLib.Floats.Formats.Posit.Model.Internal.toDyadic?]

def FloatLib.Floats.Formats.Posit.Model.toDyadic? {format : Format} (value : Model format) : Option Numerics.Dyadic

Decode the ordinary value into the shared exact dyadic carrier.

none means NaR and nothing else. The unique posit zero maps to the canonical dyadic zero, and all other words keep their exact sign, integer significand, and binary scale.

@[simp]

theorem FloatLib.Floats.Formats.Posit.Model.decodeExact_zero (format : Format) : (zero format).decodeExact = ExactValue.zero

Exact decoding recognizes the unique posit zero word.

@[simp]

theorem FloatLib.Floats.Formats.Posit.Model.decodeExact_nar (format : Format) : (nar format).decodeExact = ExactValue.nar

Exact decoding recognizes the unique posit NaR word.

@[simp]

theorem FloatLib.Floats.Formats.Posit.Model.toDyadic?_zero (format : Format) : (zero format).toDyadic? = some Numerics.Dyadic.zero

The unique posit zero maps to the canonical shared dyadic zero.

@[simp]

theorem FloatLib.Floats.Formats.Posit.Model.toDyadic?_nar (format : Format) : (nar format).toDyadic? = none

NaR has no ordinary dyadic interpretation.

theorem FloatLib.Floats.Formats.Posit.Model.toDyadic?_eq_some_decodeFields {format : Format} (value : Model format) (hnar : value.isNaR = false) (hzero : value.isZero = false) : value.toDyadic? = some value.decodeFields.toDyadic

An ordinary posit decodes to the dyadic value of its exact tapered fields.