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 directly into the shared dyadic execution carrier.

The sign and complete encoded word are supplied separately so callers that already classified the word can reuse the same extraction. decodeFiniteDyadic below remains the model-facing boundary.

@[inline]

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

Decode a nonzero finite posit directly 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; the theorem below establishes their equality.

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 exactly with the proof-facing field decoder.

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.toDyadicImpl?]

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

Decode the ordinary value directly into the shared exact dyadic carrier.

none identifies NaR exactly. The unique posit zero maps to the canonical dyadic zero; all other words retain 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.