Correctness of the configured posit quire interface

The public raw-word operations are lossless, posit-to-quire conversion preserves exact rational meaning, and the distinguished zero and NaR values are preserved across both conversion directions. The fold theorems at the end transport the standard capacity guarantees to accumulation loops written against the configured carrier.

References

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

@[simp]

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

Re-encoding a configured quire's complete bit pattern preserves it.

@[simp]

theorem FloatLib.Floats.ExecFloat.Posit.Quire.toNatBits_ofNatBits_of_lt {format : Formats.Posit.Format} (bits : ℕ) (bits_lt : bits < 2 ^ Formats.Posit.Quire.width format) : toNatBits (ofNatBits bits) = bits

An in-range unsigned word is unchanged by configured-quire encoding.

@[simp]

theorem FloatLib.Floats.ExecFloat.Posit.Quire.pToQ_nar {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] : pToQ Posit.nar = nar

Converting posit NaR to its associated quire produces the reserved quire NaR.

@[simp]

theorem FloatLib.Floats.ExecFloat.Posit.Quire.pToQ_zero {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] : pToQ Posit.zero = zero

Converting posit zero to its associated quire produces the all-zero quire.

@[simp]

theorem FloatLib.Floats.ExecFloat.Posit.Quire.toRat?_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)) : toRat? (pToQ value) = Posit.toRat? value

Configured posit-to-quire conversion preserves the complete optional exact rational meaning.

The theorem is unconditional: ordinary values are proved to fit the standard quire exactly, and posit NaR maps to quire NaR.

@[simp]

theorem FloatLib.Floats.ExecFloat.Posit.Quire.qToP_nar {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] : qToP nar = Posit.nar

Rounding the reserved quire NaR to a posit produces posit NaR.

@[simp]

theorem FloatLib.Floats.ExecFloat.Posit.Quire.qToP_zero {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] : qToP zero = Posit.zero

Rounding the all-zero quire to a posit produces the unique posit zero.

Accumulation loops

theorem FloatLib.Floats.ExecFloat.Posit.Quire.exactValues?_eq_model {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] (addends : List (ExecFloat (Formats.Posit.Configured.Family format code plan))) : exactValues? addends = Formats.Posit.Quire.Model.exactValues? (List.map toModel addends)

Configured exact values are the model's exact values of the decoded posits.

theorem FloatLib.Floats.ExecFloat.Posit.Quire.exactProducts?_eq_model {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] (pairs : List (ExecFloat (Formats.Posit.Configured.Family format code plan) × ExecFloat (Formats.Posit.Configured.Family format code plan))) : exactProducts? pairs = Formats.Posit.Quire.Model.exactProducts? (List.map (fun (pair : ExecFloat (Formats.Posit.Configured.Family format code plan) × ExecFloat (Formats.Posit.Configured.Family format code plan)) => (toModel pair.1, toModel pair.2)) pairs)

Configured exact products are the model's exact products of the decoded posit pairs.

theorem FloatLib.Floats.ExecFloat.Posit.Quire.toRat?_foldl_qMulAdd_zero {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] (pairs : List (ExecFloat (Formats.Posit.Configured.Family format code plan) × ExecFloat (Formats.Posit.Configured.Family format code plan))) (products : List ℚ) (hproducts : exactProducts? pairs = some products) (hlength : pairs.length < Formats.Posit.Quire.Model.productSumTermLimit) : toRat? (List.foldl (fun (quire : Formats.Posit.Quire.Model format) (pair : ExecFloat (Formats.Posit.Configured.Family format code plan) × ExecFloat (Formats.Posit.Configured.Family format code plan)) => qMulAdd quire pair.1 pair.2) zero pairs) = some products.sum

Folding qMulAdd over fewer than 2^31 pairs of ordinary configured posits, starting from the zero quire, is exact: the result is not NaR and denotes the exact rational sum of the products.

exactProducts? pairs = some products records that no input is NaR and identifies the exact products. Callers need no additional bounds on the quire coefficients.

theorem FloatLib.Floats.ExecFloat.Posit.Quire.toRat?_foldl_qAddP_zero {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] (addends : List (ExecFloat (Formats.Posit.Configured.Family format code plan))) (values : List ℚ) (hvalues : exactValues? addends = some values) (hlength : addends.length < Formats.Posit.Quire.Model.positSumTermLimit format) : toRat? (List.foldl qAddP zero addends) = some values.sum

Folding qAddP over fewer than 2^(23 + 4n) ordinary configured posits, starting from the zero quire, is exact.