Correctness of configured binary reductions

The configured API is a lossless carrier adaptation of the descriptor-model reducer. These theorems state that connection, 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_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))) (mode : Formats.BinaryInterchange.Model.IEEERoundingMode) : toModel (sum values mode true) = Formats.BinaryInterchange.Model.sum format (Array.map Binary.toModel values) mode true

Decoding a configured correctly rounded sum gives the descriptor-model sum, status indicators included.

@[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))) (mode : Formats.BinaryInterchange.Model.IEEERoundingMode) : toModel (sum values mode) = Formats.BinaryInterchange.Model.sum format (Array.map toModel values) mode

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

@[simp]

theorem FloatLib.Floats.ExecFloat.Binary.value_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))) (mode : Formats.BinaryInterchange.Model.IEEERoundingMode) : (sum values mode true).value = sum values mode

The configured sum with status := true delivers the value of the configured sum.

theorem FloatLib.Floats.ExecFloat.Binary.dot_status_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))) (mode : Formats.BinaryInterchange.Model.IEEERoundingMode) : dot left right mode true = Except.map IEEEOutcome.ofModel (Formats.BinaryInterchange.Model.dot format (Array.map toModel left) (Array.map toModel right) mode true)

Configured dot-product execution with status := true is 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))) (mode : Formats.BinaryInterchange.Model.IEEERoundingMode) (result : ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)) (hresult : dot left right mode = Except.ok result) : Formats.BinaryInterchange.Model.dot format (Array.map toModel left) (Array.map toModel right) mode = Except.ok (toModel result)

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

@[simp]

theorem FloatLib.Floats.ExecFloat.Binary.map_value_dot {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))) (mode : Formats.BinaryInterchange.Model.IEEERoundingMode) : Except.map (fun (x : match true with | true => IEEEOutcome | false => Binary format.expWidth format.fracWidth format.encoding format.exponentBias ⋯ ⋯ ⋯ ⋯ plan code) => x.value) (dot left right mode true) = dot left right mode

The configured dot product with status := true has the value and the length check of the value-only configured dot product.