Runtime interface for configured posit quires

Configured posit quires support exact construction, decoding, accumulation, and final rounding. The executable definitions lift the standard quire model through the configured posit carrier. Quire arithmetic proofs and optional real/projective views are provided separately.

Accumulation returns NaR on exceptional input, overflow, or a result equal to the reserved NaR coefficient. Ordinary results preserve the exact sum.

References

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

@[inline]

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

Construct a configured quire from its complete unsigned word.

@[inline]

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

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

@[inline]

def FloatLib.Floats.ExecFloat.Posit.Quire.zero {format : Formats.Posit.Format} : Formats.Posit.Quire.Model format

All-zero configured quire.

@[inline]

def FloatLib.Floats.ExecFloat.Posit.Quire.nar {format : Formats.Posit.Format} : Formats.Posit.Quire.Model format

Reserved configured quire NaR.

@[inline]

def FloatLib.Floats.ExecFloat.Posit.Quire.decode {format : Formats.Posit.Format} (value : Formats.Posit.Quire.Model format) : Numerics.NumericalValue ℚ

Complete exact rational quire semantics.

@[inline]

def FloatLib.Floats.ExecFloat.Posit.Quire.toRat? {format : Formats.Posit.Format} (value : Formats.Posit.Quire.Model format) : Option ℚ

Ordinary exact rational quire value, or none precisely for quire NaR.

def FloatLib.Floats.ExecFloat.Posit.Quire.exactValues? {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] : List (ExecFloat (Formats.Posit.Configured.Family format code plan)) → Option (List ℚ)

Exact rational values of a list of configured posits, or none when some entry is NaR.

def FloatLib.Floats.ExecFloat.Posit.Quire.exactProducts? {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] : List (ExecFloat (Formats.Posit.Configured.Family format code plan) × ExecFloat (Formats.Posit.Configured.Family format code plan)) → Option (List ℚ)

Exact rational products of a list of configured posit pairs, or none when some entry is NaR.

@[inline]

def FloatLib.Floats.ExecFloat.Posit.Quire.pToQ {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] (value : ExecFloat (Formats.Posit.Configured.Family format code plan)) : Formats.Posit.Quire.Model format

Convert one configured posit exactly into its associated quire.

@[inline]

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

Standard quire negation.

@[inline]

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

Standard quire absolute value.

@[inline]

def FloatLib.Floats.ExecFloat.Posit.Quire.qAddP {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] (accumulator : Formats.Posit.Quire.Model format) (addend : ExecFloat (Formats.Posit.Configured.Family format code plan)) : Formats.Posit.Quire.Model format

Add a configured posit exactly to its associated quire.

@[inline]

def FloatLib.Floats.ExecFloat.Posit.Quire.qSubP {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] (accumulator : Formats.Posit.Quire.Model format) (subtrahend : ExecFloat (Formats.Posit.Configured.Family format code plan)) : Formats.Posit.Quire.Model format

Subtract a configured posit exactly from its associated quire.

@[inline]

def FloatLib.Floats.ExecFloat.Posit.Quire.qAddQ {format : Formats.Posit.Format} (left right : Formats.Posit.Quire.Model format) : Formats.Posit.Quire.Model format

Add two configured quires exactly.

@[inline]

def FloatLib.Floats.ExecFloat.Posit.Quire.qSubQ {format : Formats.Posit.Format} (left right : Formats.Posit.Quire.Model format) : Formats.Posit.Quire.Model format

Subtract two configured quires exactly.

@[inline]

def FloatLib.Floats.ExecFloat.Posit.Quire.qMulAdd {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] (accumulator : Formats.Posit.Quire.Model format) (left right : ExecFloat (Formats.Posit.Configured.Family format code plan)) : Formats.Posit.Quire.Model format

Accumulate one exact configured-posit product with no intermediate rounding.

@[inline]

def FloatLib.Floats.ExecFloat.Posit.Quire.qMulSub {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] (accumulator : Formats.Posit.Quire.Model format) (left right : ExecFloat (Formats.Posit.Configured.Family format code plan)) : Formats.Posit.Quire.Model format

Subtract one exact configured-posit product with no intermediate rounding.

@[inline]

def FloatLib.Floats.ExecFloat.Posit.Quire.qToP {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] (value : Formats.Posit.Quire.Model format) : ExecFloat (Formats.Posit.Configured.Family format code plan)

Round a configured quire once into its associated configured posit.