Executable standard posit quire model

The Posit Standard (2022) associates an n-bit posit with one 16n-bit quire. The quire stores a signed two's-complement coefficient whose least-significant bit has value 2^(16 - 8n). Its most-negative word is reserved for quire NaR.

This module contains only the representation, executable constructors, classifiers, and integer/dyadic conversion kernels. Their range and denotational theorems live in Model.Proof.

References

• Posit Working Group, Standard for Posit Arithmetic (2022), March 2, 2022, Sections 3.4 and 5.11, https://posithub.org/docs/posit_standard-2.pdf.

@[inline]

def FloatLib.Floats.Formats.Posit.Quire.width (format : Format) : ℕ

The standard quire width associated with an n-bit posit.

@[inline]

def FloatLib.Floats.Formats.Posit.Quire.scaleExponent (format : Format) : ℤ

Binary scale of the quire's least-significant bit.

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

Exact standard quire word for one posit descriptor.

• word : Numerics.Representations.FixedInt (width format)

  Complete signed fixed-point word.

@[instance_reducible]

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

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

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

@[instance_reducible]

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

@[inline]

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

Construct a standard quire from its complete unsigned word.

@[inline]

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

Read the standard quire's complete word as an unsigned natural number.

@[inline]

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

Read the signed two's-complement coefficient stored by a quire.

@[inline]

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

The all-zero standard quire.

@[inline]

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

Quire NaR, encoded as the most-negative 16n-bit two's-complement word.

@[inline]

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

Whether a quire contains the standard's reserved NaR word.

def FloatLib.Floats.Formats.Posit.Quire.Model.OrdinaryCoefficient (format : Format) (value : ℤ) : Prop

Signed coefficients available to ordinary quire values.

The lower inequality is strict because FixedInt.minValue is the reserved NaR encoding. The greatest two's-complement integer remains an ordinary quire coefficient.

@[instance_reducible]

instance FloatLib.Floats.Formats.Posit.Quire.Model.instDecidableOrdinaryCoefficient (format : Format) (value : ℤ) : Decidable (OrdinaryCoefficient format value)

@[inline]

def FloatLib.Floats.Formats.Posit.Quire.Model.ofCoefficient (format : Format) (value : ℤ) : Model format

Encode an exact quire coefficient, returning quire NaR on overflow or collision with the reserved most-negative word.

This is the common overflow boundary used by every standard quire operation.

@[inline]

def FloatLib.Floats.Formats.Posit.Quire.Model.coefficientOfDyadic (format : Format) (value : Numerics.Dyadic) : ℤ

Integer coefficient of a dyadic value at the quire's fixed binary scale.

When scaleExponent format ≤ value.exponent, as holds for every ordinary posit and every exact product of two ordinary posits, this is an exact left shift of the signed significand and Model.coefficientOfDyadic_denotes recovers value.toRat. When the stored exponent is below the quire scale, the shift count clamps to zero and the result need not denote value. Model.addDyadic rejects that case, and decoded posit inputs to Model.pToQ satisfy the bound.