Posit words and exceptional encodings

The exact-width posit carrier, zero, and Not-a-Real words. These definitions support storage, equality, and bitwise reasoning. Regime parsing and finite decoding are defined in later modules.

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

Exact-width proof model for one posit descriptor.

• bits : BitVec format.bits

  Complete encoded word.

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

@[instance_reducible]

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

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

@[instance_reducible]

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

@[inline]

def FloatLib.Floats.Formats.Posit.Model.ofBits {format : Format} (bits : BitVec format.bits) : Model format

Wrap an exact-width bit vector.

@[inline]

def FloatLib.Floats.Formats.Posit.Model.ofNatBits {format : Format} (bits : ℕ) : Model format

Encode the low format.bits bits of a natural number.

@[inline]

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

Read the complete encoded word as a natural number.

theorem FloatLib.Floats.Formats.Posit.Model.toNatBits_lt_modulus {format : Format} (value : Model format) : value.toNatBits < format.modulus

Every exact-width posit word lies below its descriptor's modulus.

@[simp]

theorem FloatLib.Floats.Formats.Posit.Model.ofNatBits_toNatBits {format : Format} (value : Model format) : ofNatBits value.toNatBits = value

Re-encoding a model's exact bit pattern preserves it.

@[simp]

theorem FloatLib.Floats.Formats.Posit.Model.toNatBits_ofNatBits_of_lt {format : Format} (bits : ℕ) (hbits : bits < format.modulus) : (ofNatBits bits).toNatBits = bits

In-range natural bits are unchanged by exact-width encoding.

@[instance_reducible]

instance FloatLib.Floats.Formats.Posit.Model.instInhabited {format : Format} : Inhabited (Model format)

@[inline]

def FloatLib.Floats.Formats.Posit.Model.zero (format : Format) : Model format

The unique zero encoding.

@[inline]

def FloatLib.Floats.Formats.Posit.Model.nar (format : Format) : Model format

The unique Not-a-Real encoding, 100...0.

@[simp]

theorem FloatLib.Floats.Formats.Posit.Model.zero_toNatBits (format : Format) : (zero format).toNatBits = 0

The unique zero value encodes as the all-zero word.

@[simp]

theorem FloatLib.Floats.Formats.Posit.Model.nar_toNatBits (format : Format) : (nar format).toNatBits = format.signMaskNat

The unique NaR value encodes as the word containing only the sign bit.

theorem FloatLib.Floats.Formats.Posit.Model.zero_ne_nar (format : Format) : zero format ≠ nar format

Zero and NaR are distinct for every valid posit width.

@[inline]

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

Whether this is the unique zero code.

@[inline]

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

Whether this is the unique Not-a-Real code.

@[simp]

theorem FloatLib.Floats.Formats.Posit.Model.isZero_zero (format : Format) : (zero format).isZero = true

The zero predicate recognizes the canonical zero value.

@[simp]

theorem FloatLib.Floats.Formats.Posit.Model.isNaR_nar (format : Format) : (nar format).isNaR = true

The NaR predicate recognizes the canonical NaR value.

@[simp]

theorem FloatLib.Floats.Formats.Posit.Model.isNaR_zero (format : Format) : (zero format).isNaR = false

The canonical zero value is not NaR.

@[simp]

theorem FloatLib.Floats.Formats.Posit.Model.isZero_nar (format : Format) : (nar format).isZero = false

The canonical NaR value is not zero.

@[simp]

theorem FloatLib.Floats.Formats.Posit.Model.isNaR_eq_true_iff {format : Format} (value : Model format) : value.isNaR = true ↔ value = nar format

The NaR predicate recognizes exactly the standard's unique NaR word.

@[simp]

theorem FloatLib.Floats.Formats.Posit.Model.isZero_eq_true_iff {format : Format} (value : Model format) : value.isZero = true ↔ value = zero format

The zero predicate recognizes exactly the standard's unique zero word.