Posit semantics of direct quotient prefixes #
The representation-independent quotient-prefix bracket determines Posit regime, exponent, fraction, and appended-bit rounding thresholds. Exact quotient-and-remainder bounds show that truncation brackets the rational quotient and that jamming preserves its comparison with the rounding threshold.
theorem
FloatLib.Floats.Formats.Posit.Model.DirectDyadicQuotient.lowerCodeForPositive_eq_lowerCandidateFromQuotient_positive
(format : Format)
(regime : ℤ)
(exponentField quotient remainder denominator leading : ℕ)
(hregime : 0 ≤ regime)
(hrun : regime.toNat + 1 < format.payloadBits)
(hleadingWidth : format.payloadBits ≤ leading)
(hexponent : exponentField < 4)
(hlower : 2 ^ leading ≤ quotient)
(hupper : quotient < 2 ^ (leading + 1))
(hdenominator : 0 < denominator)
(hremainder : remainder < denominator)
:
lowerCodeForPositive format
((↑quotient + ↑remainder / ↑denominator) / ↑(2 ^ leading) * 2 ^ Int.ofNat exponentField * 2 ^ (regime * 4)) = DirectDyadicPacking.lowerCandidateFromFields format regime exponentField
(StickyPrefix.jamRemainder quotient remainder) leading
An interior positive-regime quotient prefix is exactly the rational model's greatest lower code.
theorem
FloatLib.Floats.Formats.Posit.Model.DirectDyadicQuotient.lowerCodeForPositive_eq_lowerCandidateFromQuotient_negative
(format : Format)
(regime : ℤ)
(exponentField quotient remainder denominator leading : ℕ)
(hregime : regime < 0)
(hrun : (-regime).toNat < format.payloadBits)
(hleadingWidth : format.payloadBits ≤ leading)
(hexponent : exponentField < 4)
(hlower : 2 ^ leading ≤ quotient)
(hupper : quotient < 2 ^ (leading + 1))
(hdenominator : 0 < denominator)
(hremainder : remainder < denominator)
:
lowerCodeForPositive format
((↑quotient + ↑remainder / ↑denominator) / ↑(2 ^ leading) * 2 ^ Int.ofNat exponentField * 2 ^ (regime * 4)) = DirectDyadicPacking.lowerCandidateFromFields format regime exponentField
(StickyPrefix.jamRemainder quotient remainder) leading
An interior negative-regime quotient prefix is exactly the rational model's greatest lower code.
theorem
FloatLib.Floats.Formats.Posit.Model.DirectDyadicQuotient.roundInteriorCode_eq_quotientMidpointDecision_positive
(format : Format)
(regime : ℤ)
(exponentField quotient remainder denominator leading : ℕ)
(hregime : 0 ≤ regime)
(hrun : regime.toNat + 1 < format.payloadBits)
(hleadingWidth : format.payloadBits ≤ leading)
(hexponent : exponentField < 4)
(hlower : 2 ^ leading ≤ quotient)
(hupper : quotient < 2 ^ (leading + 1))
(hdenominator : 0 < denominator)
(hremainder : remainder < denominator)
:
GuardStickyRounding.roundInteriorCode format regime exponentField (StickyPrefix.jamRemainder quotient remainder) leading
(regime.toNat + 2) = have lower :=
DirectDyadicPacking.lowerCandidateFromFields format regime exponentField
(StickyPrefix.jamRemainder quotient remainder) leading;
have threshold := roundingThreshold format lower;
have target :=
(↑quotient + ↑remainder / ↑denominator) / ↑(2 ^ leading) * 2 ^ Int.ofNat exponentField * 2 ^ (regime * 4);
if target < threshold then lower
else if threshold < target then lower + 1 else if lower % 2 = 0 then lower else lower + 1
Interior positive-regime guard/sticky rounding makes the exact quotient threshold decision.
theorem
FloatLib.Floats.Formats.Posit.Model.DirectDyadicQuotient.roundInteriorCode_eq_quotientMidpointDecision_negative
(format : Format)
(regime : ℤ)
(exponentField quotient remainder denominator leading : ℕ)
(hregime : regime < 0)
(hrun : (-regime).toNat < format.payloadBits)
(hleadingWidth : format.payloadBits ≤ leading)
(hexponent : exponentField < 4)
(hlower : 2 ^ leading ≤ quotient)
(hupper : quotient < 2 ^ (leading + 1))
(hdenominator : 0 < denominator)
(hremainder : remainder < denominator)
:
GuardStickyRounding.roundInteriorCode format regime exponentField (StickyPrefix.jamRemainder quotient remainder) leading
((-regime).toNat + 1) = have lower :=
DirectDyadicPacking.lowerCandidateFromFields format regime exponentField
(StickyPrefix.jamRemainder quotient remainder) leading;
have threshold := roundingThreshold format lower;
have target :=
(↑quotient + ↑remainder / ↑denominator) / ↑(2 ^ leading) * 2 ^ Int.ofNat exponentField * 2 ^ (regime * 4);
if target < threshold then lower
else if threshold < target then lower + 1 else if lower % 2 = 0 then lower else lower + 1
Interior negative-regime guard/sticky rounding makes the exact quotient threshold decision.
theorem
FloatLib.Floats.Formats.Posit.Model.DirectDyadicQuotient.roundInteriorCode_eq_roundPositiveCode_positive
(format : Format)
(regime : ℤ)
(exponentField quotient remainder denominator leading : ℕ)
(hregime : 0 ≤ regime)
(hrun : regime.toNat + 1 < format.payloadBits)
(hleadingWidth : format.payloadBits ≤ leading)
(hexponent : exponentField < 4)
(hlower : 2 ^ leading ≤ quotient)
(hupper : quotient < 2 ^ (leading + 1))
(hdenominator : 0 < denominator)
(hremainder : remainder < denominator)
(hnotUnderflow :
¬(↑quotient + ↑remainder / ↑denominator) / ↑(2 ^ leading) * 2 ^ Int.ofNat exponentField * 2 ^ (regime * 4) < minPositiveRat format)
:
Interior positive-regime field rounding is the exact rational positive quotient rounder.
theorem
FloatLib.Floats.Formats.Posit.Model.DirectDyadicQuotient.roundInteriorCode_eq_roundPositiveCode_negative
(format : Format)
(regime : ℤ)
(exponentField quotient remainder denominator leading : ℕ)
(hregime : regime < 0)
(hrun : (-regime).toNat < format.payloadBits)
(hleadingWidth : format.payloadBits ≤ leading)
(hexponent : exponentField < 4)
(hlower : 2 ^ leading ≤ quotient)
(hupper : quotient < 2 ^ (leading + 1))
(hdenominator : 0 < denominator)
(hremainder : remainder < denominator)
(hnotUnderflow :
¬(↑quotient + ↑remainder / ↑denominator) / ↑(2 ^ leading) * 2 ^ Int.ofNat exponentField * 2 ^ (regime * 4) < minPositiveRat format)
:
Interior negative-regime field rounding is the exact rational positive quotient rounder.