Correctness of P3109 projection

P3109 projection rounds first, saturates second, and encodes last. This module proves that the executable code decodes to the same datum as that exact round-then-saturate specification for every valid descriptor and every supported policy.

theorem FloatLib.Floats.Formats.P3109.Format.sameDatum_decode_encodeSaturate (format : Format) (mode : SaturationMode) (rounding : RoundingMode) (value : Numerics.NumericalValue Numerics.Dyadic) (hgrid : match value with | Numerics.NumericalValue.finite finite => format.FitsPrecisionGrid finite | x => True) : SameDatum (format.decode (BitVec.ofNat format.bitWidth (Internal.encodeDatumNat format (format.saturate mode rounding value)))) (format.saturate mode rounding value)

Encoding then decoding preserves a saturated datum whose finite branch lies on the descriptor's precision grid.

Dyadic projection, exact-rational projection, square roots and block roots all go through this theorem.

theorem FloatLib.Floats.Formats.P3109.Format.sameDatum_decode_projectCode (format : Format) (policy : ProjectionPolicy) (value : Numerics.NumericalValue Numerics.Dyadic) : SameDatum (format.decode (format.projectCode policy value)) (format.projectValue policy value)

Decoding an executable projection returns its round-then-saturate datum, for every valid P3109 descriptor and every rounding and saturation policy.

No descriptor width or named low-precision format is a special proof case.

@[simp]

theorem FloatLib.Floats.Formats.P3109.Format.encode?_projectValue (format : Format) (policy : ProjectionPolicy) (value : Numerics.NumericalValue Numerics.Dyadic) : format.encode? (format.projectValue policy value) = some (format.projectCode policy value)

Checked encoding accepts the exact datum produced by projection.

theorem FloatLib.Floats.ExecFloat.P3109.decode_project {format : Formats.P3109.Format} (value : Numerics.NumericalValue Numerics.Dyadic) (mode : Formats.P3109.RoundingMode) (saturation : Formats.P3109.SaturationMode) : Formats.P3109.Format.SameDatum (project value mode saturation).decode (format.projectValue { rounding := mode, saturation := saturation } value)

Decoding project gives the P3109 round-then-saturate specification.