Packing correctness for configured standard operations

Every theorem states that decoding a configured result recovers the single descriptor-model operation used to compute it. Status-bearing operations preserve all five indicators exactly.

The arithmetic properties are proved for the descriptor-model operations. These theorems transport their results through the storage codec, giving the same equations for values and exception flags with every storage plan.

@[simp]

theorem FloatLib.Floats.ExecFloat.Binary.toModel_remainder {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (dividend divisor : ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)) : toModel (remainder dividend divisor) = (toModel dividend).remainder (toModel divisor)

Decoding configured IEEE remainder gives the descriptor-model remainder.

@[simp]

theorem FloatLib.Floats.ExecFloat.Binary.IEEEOutcome.toModel_remainderWithStatus {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (dividend divisor : ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)) : (remainderWithStatus dividend divisor).toModel = (Binary.toModel dividend).remainderWithStatus (Binary.toModel divisor)

Decoding configured remainder preserves both its value and all IEEE status indicators.

@[simp]

theorem FloatLib.Floats.ExecFloat.Binary.toModel_roundToIntegral {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 (roundToIntegral value rounding) = (toModel value).roundToIntegral rounding

Decoding configured integral rounding gives integral rounding in the descriptor model.

@[simp]

theorem FloatLib.Floats.ExecFloat.Binary.IEEEOutcome.toModel_roundToIntegralExactWithStatus {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) : (roundToIntegralExactWithStatus value rounding).toModel = (Binary.toModel value).roundToIntegralExactWithStatus rounding

Configured integral rounding preserves the descriptor-model value and IEEE status.

@[simp]

theorem FloatLib.Floats.ExecFloat.Binary.toModel_scaleB {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)) (scale : ℤ) (rounding : Formats.BinaryInterchange.Model.IEEERoundingMode) : toModel (scaleB value scale rounding) = (toModel value).scaleB scale rounding

Decoding configured power-of-two scaling gives descriptor-model scaling.

@[simp]

theorem FloatLib.Floats.ExecFloat.Binary.IEEEOutcome.toModel_scaleBWithStatus {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)) (scale : ℤ) (rounding : Formats.BinaryInterchange.Model.IEEERoundingMode) : (scaleBWithStatus value scale rounding).toModel = (Binary.toModel value).scaleBWithStatus scale rounding

Configured power-of-two scaling preserves the descriptor-model value and IEEE status.

@[simp]

theorem FloatLib.Floats.ExecFloat.Binary.toModel_logB {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)) : toModel (logB value) = (toModel value).logB

Decoding configured logB gives the descriptor-model leading binary exponent.

@[simp]

theorem FloatLib.Floats.ExecFloat.Binary.IEEEOutcome.toModel_logBWithStatus {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)) : (logBWithStatus value).toModel = (Binary.toModel value).logBWithStatus

Configured logB preserves the descriptor-model value and IEEE status.

@[simp]

theorem FloatLib.Floats.ExecFloat.Binary.toModel_copySign {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (magnitude signSource : ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)) : toModel (copySign magnitude signSource) = (toModel magnitude).copySign (toModel signSource)

Decoding configured sign copying gives descriptor-model sign copying.

@[simp]

theorem FloatLib.Floats.ExecFloat.Binary.toModel_abs {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)) : toModel (abs value) = (toModel value).abs

Decoding configured absolute value gives descriptor-model absolute value.

@[simp]

theorem FloatLib.Floats.ExecFloat.Binary.toModel_nextUp {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)) : toModel (nextUp value) = (toModel value).nextUp

Decoding the configured upward neighbor gives the descriptor-model upward neighbor.

@[simp]

theorem FloatLib.Floats.ExecFloat.Binary.toModel_nextDown {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)) : toModel (nextDown value) = (toModel value).nextDown

Decoding the configured downward neighbor gives the descriptor-model downward neighbor.

@[simp]

theorem FloatLib.Floats.ExecFloat.Binary.toModel_minNum {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)) : toModel (minNum left right) = (toModel left).minNum (toModel right)

Decoding configured minNum gives descriptor-model minNum.

@[simp]

theorem FloatLib.Floats.ExecFloat.Binary.toModel_maxNum {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)) : toModel (maxNum left right) = (toModel left).maxNum (toModel right)

Decoding configured maxNum gives descriptor-model maxNum.