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)

Direct encoding and decoding preserve any saturated datum whose finite branch lies on the descriptor precision grid.

This theorem is the shared representation boundary for dyadic and exact-rational projection.

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 exact round-then-saturate datum.

The theorem is uniform over every valid P3109 descriptor and every rounding and saturation policy. No descriptor width or named low-precision format is treated as 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} (policy : Formats.P3109.ProjectionPolicy) (value : Numerics.NumericalValue Numerics.Dyadic) : Formats.P3109.Format.SameDatum (project policy value).decode (format.projectValue policy value)

Decoding project exposes the exact P3109 round-then-saturate specification.