Exact accumulation loops in a standard posit quire

Capacity bounds one signed coefficient sum. This module turns those bounds into statements about the loops a program actually runs: folding qMulAdd over a list of posit pairs, or qAddP over a list of posits, starting from the zero quire.

Below the Posit Standard's term limits (productSumTermLimit = 2^31 exact products, or positSumTermLimit format = 2^(23 + 4n) posit addends) every intermediate quire stays ordinary, so the loop never produces quire NaR and the final quire denotes the exact rational sum.

The helpers exactValues? and exactProducts? collect the exact rational terms of a list; they are some exactly when no input is NaR, which is the only hypothesis a caller must supply besides the term count.

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.

def FloatLib.Floats.Formats.Posit.Quire.Model.exactValues? {format : Format} : List (Posit.Model format) → Option (List ℚ)

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

def FloatLib.Floats.Formats.Posit.Quire.Model.exactProducts? {format : Format} : List (Posit.Model format × Posit.Model format) → Option (List ℚ)

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

@[inline]

def FloatLib.Floats.Formats.Posit.Quire.Model.foldMulAdd {format : Format} (accumulator : Model format) (pairs : List (Posit.Model format × Posit.Model format)) : Model format

Fold exact product accumulation over a list of posit pairs.

@[inline]

def FloatLib.Floats.Formats.Posit.Quire.Model.foldAddP {format : Format} (accumulator : Model format) (addends : List (Posit.Model format)) : Model format

Fold exact posit accumulation over a list of posits.

Helpers

Fused product accumulation

theorem FloatLib.Floats.Formats.Posit.Quire.Model.toRat?_foldMulAdd {format : Format} (pairs : List (Posit.Model format × Posit.Model format)) (products : List ℚ) (hproducts : exactProducts? pairs = some products) (accumulator : Model format) (value : ℚ) (consumed : ℕ) (haccumulator : accumulator.toRat? = some value) (hcoefficient : accumulator.coefficient.natAbs ≤ consumed * productCoefficientBound format) (hlength : consumed + pairs.length < productSumTermLimit) : (accumulator.foldMulAdd pairs).toRat? = some (value + products.sum)

Loop invariant for exact product accumulation.

The accumulator denotes value and its coefficient magnitude is bounded by consumed product bounds; after folding pairs with consumed + pairs.length below the product limit, the result denotes value plus the exact sum of the products.

theorem FloatLib.Floats.Formats.Posit.Quire.Model.toRat?_foldMulAdd_zero {format : Format} (pairs : List (Posit.Model format × Posit.Model format)) (products : List ℚ) (hproducts : exactProducts? pairs = some products) (hlength : pairs.length < productSumTermLimit) : ((zero format).foldMulAdd pairs).toRat? = some products.sum

Fewer than 2^31 exact products of ordinary posits accumulate exactly from the zero quire.

exactProducts? pairs = some products says that no input is NaR and names the exact rational products; the final quire is ordinary and denotes their sum with no rounding at any step.

theorem FloatLib.Floats.Formats.Posit.Quire.Model.isNaR_foldMulAdd_zero {format : Format} (pairs : List (Posit.Model format × Posit.Model format)) (products : List ℚ) (hproducts : exactProducts? pairs = some products) (hlength : pairs.length < productSumTermLimit) : ((zero format).foldMulAdd pairs).isNaR = false

Below the product limit, accumulating ordinary products never produces quire NaR.

Posit accumulation

theorem FloatLib.Floats.Formats.Posit.Quire.Model.toRat?_foldAddP {format : Format} (addends : List (Posit.Model format)) (values : List ℚ) (hvalues : exactValues? addends = some values) (accumulator : Model format) (value : ℚ) (consumed : ℕ) (haccumulator : accumulator.toRat? = some value) (hcoefficient : accumulator.coefficient.natAbs ≤ consumed * positCoefficientBound format) (hlength : consumed + addends.length < positSumTermLimit format) : (accumulator.foldAddP addends).toRat? = some (value + values.sum)

Loop invariant for exact posit accumulation.

The accumulator denotes value and its coefficient magnitude is bounded by consumed posit bounds; after folding addends with consumed + addends.length below the addend limit, the result denotes value plus the exact sum of the addends.

theorem FloatLib.Floats.Formats.Posit.Quire.Model.toRat?_foldAddP_zero {format : Format} (addends : List (Posit.Model format)) (values : List ℚ) (hvalues : exactValues? addends = some values) (hlength : addends.length < positSumTermLimit format) : ((zero format).foldAddP addends).toRat? = some values.sum

Fewer than 2^(23 + 4n) ordinary posits accumulate exactly from the zero quire.

exactValues? addends = some values says that no input is NaR and names the exact rational addends; the final quire is ordinary and denotes their sum.

theorem FloatLib.Floats.Formats.Posit.Quire.Model.isNaR_foldAddP_zero {format : Format} (addends : List (Posit.Model format)) (values : List ℚ) (hvalues : exactValues? addends = some values) (hlength : addends.length < positSumTermLimit format) : ((zero format).foldAddP addends).isNaR = false

Below the addend limit, accumulating ordinary posits never produces quire NaR.