Packing correctness for explicitly rounded configured binary operations

The decoding bridge theorems toModel_add through toModel_sqrt and their IEEEOutcome.toModel_*WithStatus companions state that decoding a configured result recovers the single descriptor-model operation used to compute it. They let proofs transfer results from the model without depending on the configured storage plan.

@[simp]

theorem FloatLib.Floats.ExecFloat.Binary.IEEEOutcome.toModel_ofModel {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (outcome : Formats.BinaryInterchange.Model.IEEEOutcome format) : (ofModel outcome).toModel = outcome

Repacking and then decoding a model outcome preserves both its value and status.

@[simp]

theorem FloatLib.Floats.ExecFloat.Binary.toModel_add {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (left right : ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)) (rounding : Formats.BinaryInterchange.Model.IEEERoundingMode) : toModel (add left right rounding) = Formats.BinaryInterchange.Model.addWithRounding rounding (toModel left) (toModel right)

Decoding configured addition gives model addition with the same rounding mode.

@[simp]

theorem FloatLib.Floats.ExecFloat.Binary.toModel_sub {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (left right : ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)) (rounding : Formats.BinaryInterchange.Model.IEEERoundingMode) : toModel (sub left right rounding) = Formats.BinaryInterchange.Model.subWithRounding rounding (toModel left) (toModel right)

Decoding configured subtraction gives model subtraction with the same rounding mode.

@[simp]

theorem FloatLib.Floats.ExecFloat.Binary.toModel_mul {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (left right : ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)) (rounding : Formats.BinaryInterchange.Model.IEEERoundingMode) : toModel (mul left right rounding) = Formats.BinaryInterchange.Model.mulWithRounding rounding (toModel left) (toModel right)

Decoding configured multiplication gives model multiplication with the same rounding mode.

@[simp]

theorem FloatLib.Floats.ExecFloat.Binary.toModel_div {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (left right : ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)) (rounding : Formats.BinaryInterchange.Model.IEEERoundingMode) : toModel (div left right rounding) = Formats.BinaryInterchange.Model.divWithRounding rounding (toModel left) (toModel right)

Decoding configured division gives model division with the same rounding mode.

@[simp]

theorem FloatLib.Floats.ExecFloat.Binary.toModel_fma {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (left right addend : ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)) (rounding : Formats.BinaryInterchange.Model.IEEERoundingMode) : toModel (fma left right addend rounding) = Formats.BinaryInterchange.Model.fmaWithRounding rounding (toModel left) (toModel right) (toModel addend)

Decoding configured FMA gives model FMA with the same rounding mode.

@[simp]

theorem FloatLib.Floats.ExecFloat.Binary.toModel_sqrt {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (value : ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)) (rounding : Formats.BinaryInterchange.Model.IEEERoundingMode) : toModel (sqrt value rounding) = Formats.BinaryInterchange.Model.sqrtWithRounding rounding (toModel value)

Decoding configured square root gives model square root with the same rounding mode.

@[simp]

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

Decoding configured addition preserves the model result and exception flags.

@[simp]

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

Decoding configured subtraction preserves the model result and exception flags.

@[simp]

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

Decoding configured multiplication preserves the model result and exception flags.

@[simp]

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

Decoding configured division preserves the model result and exception flags.

@[simp]

theorem FloatLib.Floats.ExecFloat.Binary.IEEEOutcome.toModel_fmaWithStatus {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (left right addend : ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)) (rounding : Formats.BinaryInterchange.Model.IEEERoundingMode) : (fmaWithStatus left right addend rounding).toModel = (Binary.toModel left).fmaWithStatus (Binary.toModel right) (Binary.toModel addend) rounding

Decoding configured FMA preserves the model result and exception flags.

@[simp]

theorem FloatLib.Floats.ExecFloat.Binary.IEEEOutcome.toModel_sqrtWithStatus {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (value : ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)) (rounding : Formats.BinaryInterchange.Model.IEEERoundingMode) : (sqrtWithStatus value rounding).toModel = (Binary.toModel value).sqrtWithStatus rounding

Decoding configured square root preserves the model result and exception flags.