Correctly rounded pi

Model.pi fmt rounds an enclosure of pi from the shared constants cache of Numerics.Enclosure.Constants, at the fraction width plus 64 bits. When both endpoints round to the same finite encoding, which fails only for a descriptor other than IEEE or when pi lies within 2 ^ -(fracWidth + 62) of a rounding boundary, that encoding is the result. Otherwise exact comparisons of atan 1 = π / 4 with each candidate decide the rounding. After the first use of a precision, the enclosure costs one shift and two endpoint roundings.

Pi.Proof proves that for every IEEE descriptor the result is finite and is the nearest-even rounding of Real.pi.

def FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.piBits (fmt : FloatFormat) : ℕ

Fractional bits of the cached π / 2 that pi rounds: the fraction width plus 64.

def FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.piScaledEnclosure (bits : ℕ) : Numerics.RationalInterval

The enclosure [2 T, 2 T + 4] of π * 2 ^ bits, where T is the cached lower bound of π / 2 * 2 ^ bits.

def FloatLib.Floats.Formats.BinaryInterchange.Model.pi (fmt : FloatFormat) : Model fmt

Pi rounded to nearest-even in fmt. For an IEEE descriptor the result is proved finite and correctly rounded (toReal_pi, isFinite_pi).

The cached enclosure is checked first. An enclosure that straddles a rounding boundary falls back to AlgebraicRounding.round with exact arctangent comparisons. A descriptor other than IEEE always takes that comparator path, which has no theorem.