Correctness of configured binary reductions

The configured API is a lossless carrier adaptation of the descriptor-model reducer. These theorems expose that connection directly, so proofs can reason about the one model definition without depending on byte, word, or wide storage choices.

theorem FloatLib.Floats.ExecFloat.Binary.IEEEOutcome.toModel_sumWithStatus {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (values : Array (ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan))) (rounding : Formats.BinaryInterchange.Model.IEEERoundingMode) : (sumWithStatus values rounding).toModel = Formats.BinaryInterchange.Model.sumWithStatus format (Array.map Binary.toModel values) rounding

Decoding a configured correctly rounded sum recovers the descriptor-model sum and all status indicators exactly.

@[simp]

theorem FloatLib.Floats.ExecFloat.Binary.toModel_sum {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (values : Array (ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan))) (rounding : Formats.BinaryInterchange.Model.IEEERoundingMode) : toModel (sum values rounding) = Formats.BinaryInterchange.Model.sum format (Array.map toModel values) rounding

Decoding the value-only configured sum gives the value component of the descriptor-model sum.

theorem FloatLib.Floats.ExecFloat.Binary.dotWithStatus_eq_model {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (left right : Array (ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan))) (rounding : Formats.BinaryInterchange.Model.IEEERoundingMode) : dotWithStatus left right rounding = Except.map IEEEOutcome.ofModel (Formats.BinaryInterchange.Model.dotWithStatus format (Array.map toModel left) (Array.map toModel right) rounding)

Configured dot-product execution is exactly the descriptor-model dot product, including a length-mismatch error and every IEEE status indicator.

theorem FloatLib.Floats.ExecFloat.Binary.toModel_dot_of_eq_ok {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (left right : Array (ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan))) (rounding : Formats.BinaryInterchange.Model.IEEERoundingMode) (result : ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)) (hresult : dot left right rounding = Except.ok result) : Formats.BinaryInterchange.Model.dot format (Array.map toModel left) (Array.map toModel right) rounding = Except.ok (toModel result)

On a successful configured dot product, decoding the delivered value gives the descriptor-model value exactly.